It sounds like the algorithm is quite similar to the LRParser implementation (that I have called "KLR" before on the list). It is almost an LR(0) parse, but then set.mm has certain "ambiguities" (not really the right word, more like a garden path sentence) that require the grammar to have some productions duplicated in order to keep to the LR fragment. Currently, there is a $j comment that says something like "unambiguous 'klr 5';" which is supposed to indicate that compositing depth 5 is sufficient to eliminate all ambiguities in the grammar (without this, parse table generation is only a semi-decision procedure for unambiguity, there is no guarantee of termination).
On Sun, Aug 15, 2021 at 12:00 PM Thierry Arnoux <[email protected]> wrote: > Below are parser commands I needed to add to set.mm, in order to give > hints to the parser about those ambiguities: > > $( Warn the parser about which particular formula prefixes are ambiguous > $) > $( $j ambiguous_prefix ( A => ( ph ; > type_conversions; > ambiguous_prefix ( x e. A => ( ph ; > ambiguous_prefix { <. => { A ; > ambiguous_prefix { <. <. => { A ; > $) > > It might have been possible to detect them automatically, but I took the > shortcut to specify them in set.mm. I'll kindly ask those lines to be > included in the official set.mm so that the parser works! > What's the syntax of these commands? Meaning aside, I would request that it stick to only keywords (identifiers) and quoted strings before the semicolon. Arbitrary tokens will make a mess of things - what if you need a token that is a semicolon? E.g.: $( $j ambiguous_prefix '(' 'A' to '(' 'ph' ; type_conversions; ambiguous_prefix '(' 'x' 'e.' 'A' to '(' 'ph' ; ambiguous_prefix '{' '<.' to '{' 'A' ; ambiguous_prefix '{' '<.' '<.' to '{' 'A' ; $) But I'm not sure how to read them beyond this. The parser I wrote would just composite more whenever a conflict is detected during parse table generation (and it can't help but detect the conflict since it interferes with the generation), so it didn't need hints and can just figure this out. All other things equal I think it would be better for the parser to do this itself, since they will have to be kept up to date with the database and most people won't be in a position to know how to adjust the hints. Mario -- 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/CAFXXJSsVMwevtMAR8i0OB3zbni%3D7g3xho3u17soXpBKYnUw6Rg%40mail.gmail.com.
