search

sorear / smetamath-rs

sorear's Metamath system engine - version 3 Rust
Apache License 2.0
22 stars 6 forks source link

Add a grammatical analyser #3

Open sorear opened 8 years ago

sorear commented 8 years ago

@digama0's KLR does some very nice things, but it's a semialgorithm (not guaranteed to halt on failure) which makes me very reluctant to include it. Could alternatively port SMM2's packrat parser, which does not certify unambiguity.

digama0 commented 8 years ago

I'm not sure if I mentioned this, but you can view compositing depth as a parameter to the algorithm, that is, the maximum number of rules that can be nested. This gives a family KLR(n) of parse algorithms, each of which have guaranteed halting, and any KLR grammar is KLR(n) for some n. If this was annotated in the unambiguous directive in set.mm, you could resolve this issue. (I think you need 4 or 5 composites to get all the variations on df-oprab.)

sorear commented 8 years ago

Ah, that works for me. (Will have to understand the algorithm a little bit better before I can start on it; I wrote an LR(0) parser for JSON once but that's about it.)