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. Best wishes, Daniel Kirchner
signature.asc
Description: This is a digitally signed message part.
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
