[isabelle-dev] Custom inner syntax parsing in ML.

[Daniel Kirchner]

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: This is a digitally signed message part.
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20190926/5f5a8e68/attachment-0001.sig>