Balazs Toth (Mar 23 2024 at 14:26): Balazs Toth (Mar 23 2024 at 14:26):Where can I find the Grammar for the Isabelle Theory files (as BNF or something similar)?
I started searching at https://isabelle-dev.sketis.net/source/isabelle/browse/default/src/Tools/, but it seems like I'm in the wrong place
Mathias Fleury (Mar 23 2024 at 18:05):As the grammar can be extended on the fly, there is no BNF…
Dmitriy Traytel (Mar 25 2024 at 10:49):Although print_syntax gives you something that is not to far from a grammar specification and reflects the current state of known syntax.
Mathias Fleury (Mar 25 2024 at 10:54):I tried it, but it seems to give only the inner syntax. Is there a version for the outer syntax?
Manuel Eberl (Mar 25 2024 at 10:59):That might be tricky because when you create a new tactic, command, or attribute you can specify a parser as arbitrary ML code.
Manuel Eberl (Mar 25 2024 at 11:01):But even for the inner syntax, there are parse translations that can modify the parsed inner syntax AST and the inner syntax arbitrarily. But I suppose there is at least some kind of grammar for the inner syntax AST…
Dmitriy Traytel (Mar 25 2024 at 20:01):Yes, print_syntax is inner syntax only. It also lists the parse_translations, but of course not what they actually do (arbitrary ML code).
Last updated: Apr 28 2024 at 12:28 UTC