[isabelle] Splicing runtime ML values into Isar

Dear list,

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.
With the arrival of cartouches, this is actually possible now. The
attached theory allows one to write:

  term "(Îx. SPLICE âBound 0â)"

... which results in a formal expression logically equivalent to

  term "(Îx. x)"

This also works with theorems:

  MLâval mythm = @{thm conjI[where P = True]}â
  lemmas mythm = [[splice âmythmâ]]

Of course, this is not very useful by itself. But it can also be used to
compute larger terms using ML, e.g. for lemma statements:

  lemma "0 < SPLICE âHOLogic.mk_number @{typ nat} (1+1)â"

... produces the goal "0 < 2". There might be use cases in program
synthesis here.

A nice side effect of using cartouches is that markup works out of the
box, i.e. all the ML entities (and embedded antiquotations) can be

Disclaimer: Do not use this for production purposes.

Comments welcome!

signature SPLICE = sig
  val fulfill_term: int -> term -> unit
  val eval_term: Proof.context -> Input.source -> term
  val term_translation: Proof.context -> term list -> term

  val fulfill_thm: int -> thm -> unit
  val eval_thm: Proof.context -> Input.source -> thm
  val thm_attribute: Input.source -> Thm.attribute

structure Splice: SPLICE = struct

val term_splices: term option Unsynchronized.ref Inttab.table Synchronized.var =
  Synchronized.var "term_splices" Inttab.empty

val thm_splices: thm option Unsynchronized.ref Inttab.table Synchronized.var =
  Synchronized.var "thm_splices" Inttab.empty

fun fulfill var id result =
  the (Inttab.lookup (Synchronized.value var) id) := SOME result

val fulfill_term = fulfill term_splices
val fulfill_thm = fulfill thm_splices

fun eval var name ctxt source =
    val id = serial ()
    val cell = Unsynchronized.ref NONE
    val _ = Synchronized.change var (Inttab.update_new (id, cell))
    val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of source)
      (ML_Lex.read ("Splice." ^ name ^ " " ^ ML_Syntax.print_int id ^ "(") @
        ML_Lex.read_source false source @
        ML_Lex.read ")")
    Synchronized.change_result var (fn tab =>
      let val result = the (!(the (Inttab.lookup tab id))) in
        (result, Inttab.delete id tab)

val eval_term = eval term_splices "fulfill_term"
val eval_thm = eval thm_splices "fulfill_thm"

fun term_translation ctxt args =
    fun err () = raise TERM ("Splice.term_translation", args)
    fun input s pos =
        val content = Symbol_Pos.cartouche_content (Symbol_Pos.explode (s, pos))
        val (text, range) = Symbol_Pos.implode_range (Symbol_Pos.range content) content
        Input.source true text range
    case args of
      [(c as Const (@{syntax_const "_constrain"}, _)) $ Free (s, _) $ p] =>
        (case Term_Position.decode_position p of
          SOME (pos, _) => c $ eval_term ctxt (input s pos) $ p
        | NONE => err ())
    | _ => err ()

fun thm_attribute input =
  Thm.rule_attribute (fn context => K (eval_thm (Context.proof_of context) input))


Attachment: Splice.thy
Description: application/extension-thy

Attachment: Splice_Examples.thy
Description: application/extension-thy

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