Re: [isabelle] Splicing runtime ML values into Isar



On Tue, 9 Jun 2015, Lars Hupel wrote:

we've had antiquotations for a while now -- a syntactic method to embed
formal entities into ML code. I've been wondering about the opposite
direction -- embedding (properly typed) ML values into a formal context.

Disclaimer: Do not use this for production purposes.

Comments welcome!

Cartouches were indeed introduced to make arbitrary nesting of languages synactically easy, although the concept of sublanguages has been there in Isabelle from early on.

There are endless possibilities, but it also needs some efforts to make concrete applications work robustly with the endless features we have already accumulated.

Just a few notes on this particular experiment:

  * There is no need to poke into global refs.  The implicit ML context
    can be used to transport values in and out of ML "eval" in a
    value-oriented manner.  See the implementation of the "tactic" proof
    method, with its Method.set_tactic slot.

  * Term translations operate on rather raw parse trees.  You have already
    discovered that in the examples: referring to a local "x" is not
    immediately clear.  It would require some mechanism to "protect"
    already internal terms within the parse tree, but that would have to
    cooperate properly with the other syntax phases and the term "check"
    phases (type inference etc.).

  * Morphisms, which are particularly important for attribute expressions,
    introduce another dimension of higher abstract nonsense.  One needs to
    look closely that embedded ML works with that, but not all aspects are
    properly implemented in the system and existing antiquotations.
    E.g. ML antiquotations themselves ignore morphisms.


Isabelle/ML in Isabelle2015 also provides literal token syntax for formal input source. Here is an example of this madness, used together with the SPLICE inner syntax:


theory Scratch
imports Main "~/tmp/Splice"
begin

ML â
  val ctxt = @{context};
  val input = âÎx. x + y + SPLICE âBound 0ââ;

  val t = Syntax.read_term ctxt (Syntax.implode_input input);
â

end


You see how the nested source inside the ML block gets formally annotated by PIDE markup.


	Makarius


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