signature TYPED_EVALUATION = sig

type 'a token

val token: ('a -> exn) -> (exn -> 'a option) -> int -> string -> 'a token (* internal *)

val fulfill: 'a token -> 'a Exn.result -> Context.generic -> Context.generic (* internal *)

val register: binding -> Input.source -> generic_theory -> generic_theory

val register_cmd: bstring * Position.T -> Input.source -> generic_theory -> generic_theory

val antiq: Proof.context -> (bstring * Position.T) -> string

val eval: 'a token -> Input.source -> Proof.context -> 'a

val eval_exn: 'a token -> Input.source -> Proof.context -> 'a Exn.result

val setup: theory -> theory

end

structure Typed_Evaluation: TYPED_EVALUATION = struct

structure Data = Generic_Data

(

type T = (Any.T Exn.result option * int Name_Space.table)

val empty = (NONE, Name_Space.empty_table "typed_evaluation_slot")

val extend = I

fun merge ((NONE, tab1), (NONE, tab2)) = (NONE, Name_Space.merge_tables (tab1, tab2))

| merge _ = raise Fail "Typed_Evaluation.Pending.merge"

)

fun register binding source context =

let

val parsed = ML_Lex.read_source false source

val pos = Input.pos_of source

val id = serial ()

val slots = snd (Data.get context)

val (_, slots') = Name_Space.define context true (binding, id) slots

val decl =

ML_Lex.read ("val typed_evaluation_token" ^ ML_Syntax.print_int id ^ ": (") @ parsed @ ML_Lex.read ") Typed_Evaluation.token =" @

ML_Lex.read "(let exception Data of" @ parsed @ ML_Lex.read ";" @

ML_Lex.read "val wrap = Data;" @

ML_Lex.read "fun unwrap exn = (case exn of Data data => SOME data | _ => NONE);" @

ML_Lex.read ("val id = " ^ ML_Syntax.print_int id ^ ";") @

ML_Lex.read ("val ml_type = " ^ ML_Syntax.print_string (Input.source_content source) ^ ";") @

ML_Lex.read "in Typed_Evaluation.token wrap unwrap id ml_type end)"

in

Data.map (apsnd (K slots')) context

|> ML_Context.exec (fn () => ML_Context.eval ML_Compiler.flags pos decl)

|> Local_Theory.propagate_ml_env

end

val register_cmd =

register o Binding.make

fun antiq ctxt name =

let

val context = Context.Proof ctxt

val table = snd (Data.get context)

val (_, id) = Name_Space.check context table name

in

"typed_evaluation_token" ^ ML_Syntax.print_int id

end

abstype

'a token = Token of {wrap: 'a -> exn, unwrap: exn -> 'a option, id: int, ml_type: string}

with

fun token wrap unwrap id ml_type =

Token {wrap = wrap, unwrap = unwrap, id = id, ml_type = ml_type}

fun fulfill (Token {wrap, ...}) = Data.map o apfst o K o SOME o Exn.map_result wrap

fun eval_exn (Token {id, ml_type, unwrap, ...}) source ctxt =

let

val parsed =

ML_Lex.read "Exn.capture (fn () => " @

ML_Lex.read_source false source @

ML_Lex.read ") ()"

val action =

"Typed_Evaluation.fulfill typed_evaluation_token" ^

ML_Syntax.print_int id ^ " typed_evaluation_result"

val context = Context.Proof ctxt

val result =

ML_Context.expression (Input.range_of source)

"typed_evaluation_result" ("(" ^ ml_type ^ ") Exn.result") action parsed context

|> Data.get |> fst

fun err () = raise Fail "Typed_Evaluation.eval_exn"

in

case result of

NONE => err ()

| SOME (Exn.Res r) =>

(case unwrap r of

NONE => err ()

| SOME r => Exn.Res r)

| SOME (Exn.Exn exn) =>

if Exn.is_interrupt exn then

reraise exn

else

Exn.Exn exn

end

fun eval token =

Exn.release oo eval_exn token

end

val _ =

Outer_Syntax.command @{command_keyword typed_evaluation} "register new typed evaluation slot"

(Parse.position Parse.name -- Parse.!!! (@{keyword "="} |-- Parse.ML_source)

>> (fn (name, source) => Toplevel.generic_theory (register_cmd name source)))

val setup =

ML_Antiquotation.inline @{binding token}

(Args.context -- Scan.lift (Parse.position Parse.name)

>> (fn (thy, name) => antiq thy name))

end