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
end

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 =
  let
    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 ")")
  in
    Synchronized.change_result var (fn tab =>
      let val result = the (!(the (Inttab.lookup tab id))) in
        (result, Inttab.delete id tab)
      end)
  end

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

fun term_translation ctxt args =
  let
    fun err () = raise TERM ("Splice.term_translation", args)
    fun input s pos =
      let
        val content = Symbol_Pos.cartouche_content (Symbol_Pos.explode (s, pos))
        val (text, range) = Symbol_Pos.implode_range (Symbol_Pos.range content) content
      in
        Input.source true text range
      end
  in
    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 ()
  end

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

end