Hi Jim, Il giorno sabato 31 maggio 2025 alle 02:06:55 UTC+2 [email protected] wrote:
> Has anyone done any work on a tool to automatically check the metamath > grammar for ambiguities? I guess you are asking for set.mm ambiguity, am I right? Or are you actually asking for the metamath language ambiguity? Yamma uses Nearly.js to parse every wff in the theory (and every single proof step formula, when you build the model for step suggestions). Here https://nearley.js.org/ they state "nearley handles *ambiguous grammars* gracefully. Ambiguous grammars can be parsed in multiple ways: instead of getting confused, nearley gives you all the parsings (in a deterministic order!)" In other words, if a wff happened to have multiple possible parsing trees, Nearly.js should return them all. I check for ambiguity here https://github.com/glacode/yamma/blob/b7a76cb1992d047c9c425fff8c345c04ad41f255/server/src/mmp/MmpParser.ts#L440 I’m not quite as graceful — I throw an exception that would crash the language server — but that means I’d be able to trace it down easily. So far, with *set.mm*, that exception has never been triggered. I’d feel much more confident setting up a unit test with an intentionally ambiguous theory. If anyone has one handy and wants to open an issue in Yamma’s repo, they’re very welcome to do so. 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 visit https://groups.google.com/d/msgid/metamath/b16e8aa2-fcf1-4a46-9805-9eeb29b15447n%40googlegroups.com.
