[isabelle-dev] Custom inner syntax parsing in ML.
daniel at ekpyron.org
Thu Sep 26 15:42:20 CEST 2019
Dear Isabelle mailing list,
Is there a reason why the ML function "Syntax_Phases.parsetree_to_ast" is not exposed as public API?
I haven't seen another way to translate a parse tree to an AST or to further process a parse tree in any way using the ML API for that matter. It looks like the exposed API allows to generate a parse tree, but I haven't seen a way to continue from there. Currently I work around that problem by just copying "Syntax_Phases.parsetree_to_ast", but that's of course not particularly nice. Or am I missing another way to do this?
To provide some background for the question:
I'm currently working on implementing a custom parser for inner syntax packed in string constants for implementing an embedded object logic with a syntactic structure that cannot be parsed otherwise (e.g. single letter identifiers with no whitespace delimiters, etc., requiring a customized parsing process). The idea is to end up with a syntax like " ⊨ ''<formula of embedded logic>'' ". This is already working quite well, basically using "Syntax.tokenize -> Syntax.parse -> Syntax_Phases.parsetree_to_ast" with some custom adjustments between the steps, but unfortunately "Syntax_Phases.parsetree_to_ast" seems to be private to "Syntax_Phases" at the moment.
On a related note: packing formulas in custom syntax plus a string constant is the only way to prevent the parsing process from trying to parse children first and to be able to intervene on string or token level using a "parse_ast_translation", right? The otherwise very great tutorial at https://nms.kcl.ac.uk/christian.urban/Cookbook/ is unfortunately still lacking information on parse translations and generally on intervening on the inner syntax parsing process - in fact I'm considering to contribute to it once my own project is done.
I wasn't sure whether to post this on the isabelle-users or the isabelle-dev mailing list, so I went with the suggestion at https://nms.kcl.ac.uk/christian.urban/Cookbook/, I hope that's fine.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 833 bytes
Desc: This is a digitally signed message part.
More information about the isabelle-dev