[isabelle] Embedded languages in Isabelle



On 01/10/2019 15:16, Makarius wrote:
> On 26/09/2019 15:58, Daniel Kirchner wrote:
> 
>> 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.

Here are further examples for embedded languages in Isabelle:

  Isabelle2019/src/Pure/Tools/rail.ML
  Isabelle2019/src/Pure/Syntax/simple_syntax.ML

Both is based on Isabelle parser combinators. There is also proper
support for formal positions and Prover IDE markup in the rail
application -- without that an Isabelle language is not complete.

(Note on browsing sources in Isabelle/Pure: Documentation panel, entry
src/Pure/ROOT.ML + its explanation at the top of the file.)


I don't think that your first idea to change the Isabelle term language
will work out in general: certain assumptions about lexical syntax and
identifiers are deeply rooted in the system. There are some explanations
on formal names in section 1.2 of the "implementation" manual (see the
Documentation panel in Isabelle/jEdit). In particular, the system may
transform names within a term in certain situation, e.g. "x" could
become "x_" or "xa" or "?xa" later on.

You did not say anything about the application context nor the overall
motivation. There might be more plain and basic approaches, e.g. an
application notation \<app> where this newly allocated Isabelle symbol
is rendered as a thin space.


	Makarius

Attachment: signature.asc
Description: OpenPGP digital signature



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