Re: [isabelle] Custom inner syntax parsing in ML.



On 26/09/2019 15:58, Daniel Kirchner wrote:
> 
> Is there a reason why the ML function "Syntax_Phases.parsetree_to_ast" is not 
> exposed as public API?

Usually to prevent violation of implicit structural assumptions about
the system. Note that many of these modules are more open than they
should. Low-level tinkering with "syntax phases" is unlikely to work out
properly -- now and in the longer run.

It requires very careful study of the overall situation to figure out if
previously unintended applications of certain modules can be made official.


> 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.

The standard way to embed sublanguages is via cartouches, e.g. see
Isabelle2019/HOL/ex/Cartouche_Examples.thy for some experiments and
examples.

This does not solve the problem of imitation the Isabelle term language.
At some point there might be more official ways to do that, e.g.
something like antiquotations with control symbol and cartouch within terms.


> 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.

That document is "fan-fiction". In its early years, I tried to
contribute to it and rectify its somewhat misleading approach at
"Isabelle system hacking", but I've given up on it long ago.


	Makarius

Attachment: signature.asc
Description: OpenPGP digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.