On the KLR parser

[Giovanni Mascellani]

Dear Matamath developers,

according to a comment in the file set.mm (the one containing the $j
token), the parsing grammar of set.mm can be shown to be unambiguous
using a "KLR parser with compositing depth 5". I am not an expert in
parsing an could not find anything related to the KLR parser. Do you
have any resource for it? Or is that a way to express what is commonly
known as LR(5)?

Thanks for your help, Giovanni.
--
Giovanni Mascellani <g.masc...@gmail.com>
PhD Student - Scuola Normale Superiore, Pisa, Italy

http://poisson.phc.unipi.it/~mascellani

[Mario Carneiro]

It's a variant of the LR parser I developed which adjusts the input grammar whenever something that a normal LR parser couldn't handle is found, by composing rules together to skip the offending state. Depth 5 means that compositing is repeated until the most complicated composed rules have 5 rules of the original grammar before the grammar becomes LR(0). The post https://groups.google.com/d/msg/metamath/yNdxi71vN68/hWCJXsztEgAJ describes the initial ideas that lead to the parser, and you can also look at https://github.com/digama0/mmj2/blob/master/src/mmj/verify/LRParser.java for an implementation of the technique.

A more natural informal proof of unambiguity can also be found at http://us2.metamath.org:88/downloads/grammar-ambiguity.txt .

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 metamath+unsubscribe@googlegroups.com.
To post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.

[David A. Wheeler]

On April 9, 2017 2:14:05 PM EDT, Mario Carneiro <di....@gmail.com> wrote:
>It's a variant of the LR parser I developed which adjusts the input
>grammar
>whenever something that a normal LR parser couldn't handle is found, by
>composing rules together to skip the offending state. Depth 5 means
>that
>compositing is repeated until the most complicated composed rules have
>5
>rules of the original grammar before the grammar becomes LR(0). The
>post
>https://groups.google.com/d/msg/metamath/yNdxi71vN68/hWCJXsztEgAJ
>describes
>the initial ideas that lead to the parser, and you can also look at
>https://github.com/digama0/mmj2/blob/master/src/mmj/verify/LRParser.java
>for an implementation of the technique.

It might be useful to have a fixed URL that explains it. Then Google can actually find it.


--- David A.Wheeler