Hi Antony, On Sun, Dec 4, 2022 at 5:46 PM Glauco wrote: > >> here >> >> https://github.com/glacode/yamma/blob/master/server/src/grammar/GrammarManager.ts >> I'm creating the grammar rules for set.mm that I will then use for >> diagnostics, unification, etc. for .mmp files >> The rules are for Nearly.js >> > > Yes, if I've read the Yamma source code correctly, you parse assertions > (i.e. axioms, definitions, and the part of the proof that asserts the thing > being proved). >
I use the "syntax axioms" (see pag. 127 of the Metamath book) to dynamically build the grammar for the specific theory (i.e. $a statements with a typecode other than '|-' ) The mm parser itself is hand coded, not Nearley-generated. That's what > took me a while to figure out even though it's all there in your email, and > why I first said I was investigating your parsers, then later said I'm > writing my own based upon Nearley and EBNF at the back of the Metamath > book. Sorry for any consternation I might have caused while I was trying > to get myself orientated around a parsing strategy. > To parse the .mm file, I use a TypeScript "translation" of the csharp version, that's a translation of the python version (I guess). It is hardcoded, and it should be linear w.r.t. the file size. > > The grammar created (for my local set.mm file) has 1624 rules (but 3 > are for working vars), so I'm pretty sure, Nearly.js has no problem with > large-ish grammars. > > No, it's the size of the file it's parsing, not the size of the grammar, > that I'm saying may be problematic. > Is it problematic in time or in space? (for what I read, if you can express the grammar left-recursively, even early parsers should be linear in time) Glauco -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/5ddcce1c-6801-498b-93be-5309cbe44a11n%40googlegroups.com.
