haftmann@39401: (* Title: Tools/Code/code_runtime.ML haftmann@28054: Author: Florian Haftmann, TU Muenchen haftmann@28054: haftmann@34028: Runtime services building on code generation into implementation language SML. haftmann@28054: *) haftmann@28054: haftmann@39401: signature CODE_RUNTIME = haftmann@28054: sig haftmann@34028: val target: string haftmann@39912: val value: Proof.context -> haftmann@39912: (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string -> haftmann@39912: string * string -> 'a haftmann@39473: type 'a cookie = (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string haftmann@55757: val dynamic_value: 'a cookie -> Proof.context -> string option haftmann@39473: -> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a option haftmann@55757: val dynamic_value_strict: 'a cookie -> Proof.context -> string option haftmann@39473: -> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a haftmann@55757: val dynamic_value_exn: 'a cookie -> Proof.context -> string option haftmann@39473: -> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a Exn.result haftmann@56973: val static_value: 'a cookie -> { ctxt: Proof.context, target: string option, haftmann@56973: lift_postproc: (term -> term) -> 'a -> 'a, consts: string list } haftmann@56973: -> Proof.context -> term -> 'a option haftmann@56973: val static_value_strict: 'a cookie -> { ctxt: Proof.context, target: string option, haftmann@56973: lift_postproc: (term -> term) -> 'a -> 'a, consts: string list } haftmann@56973: -> Proof.context -> term -> 'a haftmann@56973: val static_value_exn: 'a cookie -> { ctxt: Proof.context, target: string option, haftmann@56973: lift_postproc: (term -> term) -> 'a -> 'a, consts: string list } haftmann@56973: -> Proof.context -> term -> 'a Exn.result haftmann@55757: val dynamic_holds_conv: Proof.context -> conv haftmann@56973: val static_holds_conv: { ctxt: Proof.context, consts: string list } -> Proof.context -> conv haftmann@64943: val experimental_computation: (term -> 'a) cookie haftmann@58643: -> { ctxt: Proof.context, lift_postproc: (term -> term) -> 'a -> 'a, haftmann@64940: terms: term list, T: typ } haftmann@58643: -> Proof.context -> term -> 'a (*EXPERIMENTAL!*) haftmann@40421: val code_reflect: (string * string list option) list -> string list -> string haftmann@40421: -> string option -> theory -> theory haftmann@39473: datatype truth = Holds haftmann@39473: val put_truth: (unit -> truth) -> Proof.context -> Proof.context haftmann@57435: val trace: bool Config.T haftmann@39816: val polyml_as_definition: (binding * typ) list -> Path.T list -> theory -> theory haftmann@28054: end; haftmann@28054: haftmann@39401: structure Code_Runtime : CODE_RUNTIME = haftmann@28054: struct haftmann@28054: haftmann@55150: open Basic_Code_Symbol; haftmann@39473: haftmann@63157: (** computation **) haftmann@33992: haftmann@39473: (* technical prerequisites *) haftmann@39473: haftmann@39473: val this = "Code_Runtime"; haftmann@39473: val s_truth = Long_Name.append this "truth"; haftmann@39473: val s_Holds = Long_Name.append this "Holds"; haftmann@39473: haftmann@34028: val target = "Eval"; haftmann@28054: haftmann@39473: datatype truth = Holds; haftmann@39422: wenzelm@53171: val _ = Theory.setup haftmann@59104: (Code_Target.add_derived_target (target, [(Code_ML.target_SML, I)]) haftmann@55150: #> Code_Target.set_printings (Type_Constructor (@{type_name prop}, haftmann@52435: [(target, SOME (0, (K o K o K) (Code_Printer.str s_truth)))])) haftmann@55150: #> Code_Target.set_printings (Constant (@{const_name Code_Generator.holds}, haftmann@52435: [(target, SOME (Code_Printer.plain_const_syntax s_Holds))])) haftmann@39473: #> Code_Target.add_reserved target this wenzelm@53171: #> fold (Code_Target.add_reserved target) ["oo", "ooo", "oooo", "upto", "downto", "orf", "andf"]); haftmann@39485: (*avoid further pervasive infix names*) haftmann@39473: haftmann@57435: val trace = Attrib.setup_config_bool @{binding "code_runtime_trace"} (K false); haftmann@40150: haftmann@63163: fun compile_ML verbose code context = haftmann@63163: (if Config.get_generic context trace then tracing code else (); haftmann@63164: Code_Preproc.timed "compiling ML" Context.proof_of haftmann@63164: (ML_Context.exec (fn () => ML_Compiler0.ML ML_Env.context haftmann@63163: {line = 0, file = "generated code", verbose = verbose, haftmann@63164: debug = false} code)) context); haftmann@39912: haftmann@39912: fun value ctxt (get, put, put_ml) (prelude, value) = haftmann@39912: let wenzelm@62889: val code = wenzelm@62889: prelude ^ "\nval _ = Context.put_generic_context (SOME (Context.map_proof (" ^ wenzelm@62889: put_ml ^ " (fn () => " ^ value ^ ")) (Context.the_generic_context ())))"; haftmann@39912: val ctxt' = ctxt haftmann@63157: |> put (fn () => error ("Bad computation for " ^ quote put_ml)) haftmann@63163: |> Context.proof_map (compile_ML false code); haftmann@63164: val computator = get ctxt'; haftmann@63164: in Code_Preproc.timed_exec "running ML" computator ctxt' end; haftmann@39912: haftmann@39473: haftmann@63157: (* computation as evaluation into ML language values *) haftmann@39473: haftmann@39473: type 'a cookie = (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string; haftmann@39473: haftmann@55757: fun reject_vars ctxt t = haftmann@55757: ((Sign.no_frees ctxt o Sign.no_vars ctxt o map_types (K dummyT)) t; t); haftmann@39605: haftmann@63157: fun build_computation_text ctxt some_target program consts = haftmann@63157: Code_Target.computation_text ctxt (the_default target some_target) program consts false haftmann@63157: #>> (fn ml_modules => space_implode "\n\n" (map snd ml_modules)); haftmann@63157: haftmann@63157: fun run_computation_text cookie ctxt comp vs_t args = haftmann@55757: let haftmann@63157: val (program_code, value_name) = comp vs_t; haftmann@39473: val value_code = space_implode " " haftmann@41347: (value_name :: "()" :: map (enclose "(" ")") args); wenzelm@40235: in Exn.interruptible_capture (value ctxt cookie) (program_code, value_code) end; haftmann@39473: haftmann@39473: fun partiality_as_none e = SOME (Exn.release e) haftmann@39473: handle General.Match => NONE haftmann@39473: | General.Bind => NONE haftmann@39473: | General.Fail _ => NONE; haftmann@39473: haftmann@55757: fun dynamic_value_exn cookie ctxt some_target postproc t args = haftmann@39473: let haftmann@55757: val _ = reject_vars ctxt t; haftmann@57435: val _ = if Config.get ctxt trace haftmann@55757: then tracing ("Evaluation of term " ^ quote (Syntax.string_of_term ctxt t)) haftmann@41099: else () haftmann@63157: fun comp program _ vs_ty_t deps = haftmann@63157: run_computation_text cookie ctxt (build_computation_text ctxt some_target program deps) vs_ty_t args; haftmann@63157: in Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) comp t end; haftmann@39473: haftmann@55757: fun dynamic_value_strict cookie ctxt some_target postproc t args = haftmann@55757: Exn.release (dynamic_value_exn cookie ctxt some_target postproc t args); haftmann@39473: haftmann@55757: fun dynamic_value cookie ctxt some_target postproc t args = haftmann@55757: partiality_as_none (dynamic_value_exn cookie ctxt some_target postproc t args); haftmann@39473: haftmann@56973: fun static_value_exn cookie { ctxt, target, lift_postproc, consts } = haftmann@55757: let haftmann@63157: fun computation' { program, deps } = haftmann@63157: let haftmann@63157: val computation'' = run_computation_text cookie ctxt haftmann@63157: (build_computation_text ctxt target program (map Constant deps)); haftmann@63157: in fn _ => fn _ => fn vs_ty_t => fn _ => computation'' vs_ty_t [] end; haftmann@63157: val computation = Code_Thingol.static_value { ctxt = ctxt, wenzelm@61077: lift_postproc = Exn.map_res o lift_postproc, consts = consts } haftmann@63157: computation'; haftmann@63157: in fn ctxt' => computation ctxt' o reject_vars ctxt' end; haftmann@39473: haftmann@64928: fun static_value_strict cookie x = Exn.release oo static_value_exn cookie x; haftmann@41347: haftmann@64928: fun static_value cookie x = partiality_as_none oo static_value_exn cookie x; haftmann@39473: haftmann@39473: haftmann@39473: (* evaluation for truth or nothing *) haftmann@39473: wenzelm@39820: structure Truth_Result = Proof_Data wenzelm@39820: ( wenzelm@59155: type T = unit -> truth; wenzelm@59155: val empty: T = fn () => raise Fail "Truth_Result"; wenzelm@59155: fun init _ = empty; haftmann@39473: ); haftmann@39473: val put_truth = Truth_Result.put; haftmann@39473: val truth_cookie = (Truth_Result.get, put_truth, Long_Name.append this "put_truth"); haftmann@39473: haftmann@58558: local haftmann@39605: haftmann@58558: val reject_vars = fn ctxt => tap (reject_vars ctxt o Thm.term_of); haftmann@41349: haftmann@55757: fun check_holds ctxt evaluator vs_t ct = haftmann@39473: let haftmann@39473: val t = Thm.term_of ct; haftmann@39473: val _ = if fastype_of t <> propT wenzelm@59633: then error ("Not a proposition: " ^ Syntax.string_of_term ctxt t) haftmann@39473: else (); wenzelm@59633: val iff = Thm.cterm_of ctxt (Term.Const (@{const_name Pure.eq}, propT --> propT --> propT)); haftmann@63157: val result = case partiality_as_none (run_computation_text truth_cookie ctxt evaluator vs_t []) haftmann@39473: of SOME Holds => true haftmann@39473: | _ => false; haftmann@39473: in haftmann@39473: Thm.mk_binop iff ct (if result then @{cprop "PROP Code_Generator.holds"} else ct) haftmann@39473: end; haftmann@39473: haftmann@39473: val (_, raw_check_holds_oracle) = Context.>>> (Context.map_theory_result wenzelm@43619: (Thm.add_oracle (@{binding holds_by_evaluation}, haftmann@55757: fn (ctxt, evaluator, vs_t, ct) => check_holds ctxt evaluator vs_t ct))); haftmann@39473: haftmann@56920: fun check_holds_oracle ctxt evaluator vs_ty_t ct = haftmann@56920: raw_check_holds_oracle (ctxt, evaluator, vs_ty_t, ct); haftmann@41349: haftmann@41349: in haftmann@39485: haftmann@55757: fun dynamic_holds_conv ctxt = Code_Thingol.dynamic_conv ctxt haftmann@56969: (fn program => fn vs_t => fn deps => haftmann@63157: check_holds_oracle ctxt (build_computation_text ctxt NONE program deps) vs_t) haftmann@55757: o reject_vars ctxt; haftmann@39473: haftmann@56973: fun static_holds_conv (ctxt_consts as { ctxt, ... }) = haftmann@63156: Code_Thingol.static_conv_thingol ctxt_consts (fn { program, deps } => fn ctxt' => fn vs_t => haftmann@63157: K (check_holds_oracle ctxt' (build_computation_text ctxt NONE program (map Constant deps)) vs_t o reject_vars ctxt')); haftmann@41349: haftmann@41349: end; (*local*) haftmann@39404: haftmann@39404: haftmann@64940: (** computations -- experimental! **) haftmann@64940: haftmann@64943: fun monomorphic T = fold_atyps ((K o K) false) T true; haftmann@64943: haftmann@64940: fun typ_signatures_for T = haftmann@64940: let haftmann@64940: val (Ts, T') = strip_type T; haftmann@64940: in map_range (fn n => (drop n Ts ---> T', take n Ts)) (length Ts + 1) end; haftmann@64940: haftmann@64940: fun typ_signatures cTs = haftmann@64940: let haftmann@64940: fun add (c, T) = haftmann@64940: fold (fn (T, Ts) => Typtab.map_default (T, []) (cons (c, Ts))) haftmann@64940: (typ_signatures_for T); haftmann@64940: in haftmann@64940: Typtab.empty haftmann@64940: |> fold add cTs haftmann@64940: |> Typtab.lookup_list haftmann@64940: end; haftmann@64940: haftmann@64940: fun print_of_term_funs { typ_sign_for, eval_for_const, of_term_for_typ } Ts = haftmann@64940: let haftmann@64940: val var_names = map_range (fn n => "t" ^ string_of_int (n + 1)); haftmann@64940: fun print_lhs c xs = "Const (" ^ quote c ^ ", _)" haftmann@64940: |> fold (fn x => fn s => s ^ " $ " ^ x) xs haftmann@64943: |> enclose "(" ")"; haftmann@64940: fun print_rhs c Ts T xs = eval_for_const (c, Ts ---> T) haftmann@64940: |> fold2 (fn T' => fn x => fn s => haftmann@64943: s ^ (" (" ^ of_term_for_typ T' ^ " " ^ x ^ ")")) Ts xs haftmann@64940: fun print_eq T (c, Ts) = haftmann@64940: let haftmann@64940: val xs = var_names (length Ts); haftmann@64940: in print_lhs c xs ^ " = " ^ print_rhs c Ts T xs end; haftmann@64940: fun print_eqs T = haftmann@64940: let haftmann@64940: val typ_signs = typ_sign_for T; haftmann@64940: val name = of_term_for_typ T; haftmann@64940: in haftmann@64943: map (print_eq T) typ_signs haftmann@64940: |> map (prefix (name ^ " ")) haftmann@64940: |> space_implode "\n | " haftmann@64940: end; haftmann@64940: in haftmann@64940: map print_eqs Ts haftmann@64940: |> space_implode "\nand " haftmann@64940: |> prefix "fun " haftmann@64940: end; haftmann@64940: haftmann@64940: local haftmann@64940: haftmann@64940: fun tycos_of (Type (tyco, Ts)) = maps tycos_of Ts @ [tyco] haftmann@64940: | tycos_of _ = []; haftmann@64940: haftmann@64940: val ml_name_of = Name.desymbolize NONE o Long_Name.base_name; haftmann@64940: haftmann@64940: in haftmann@64940: haftmann@64940: fun of_term_for_typ Ts = haftmann@64940: let haftmann@64940: val names = Ts haftmann@64940: |> map (suffix "_of_term" o space_implode "_" o map ml_name_of o tycos_of) haftmann@64940: |> Name.variant_list []; haftmann@64940: in the o AList.lookup (op =) (Ts ~~ names) end; haftmann@64940: haftmann@64940: fun eval_for_const ctxt cTs = haftmann@64940: let haftmann@64940: fun symbol_list (c, T) = c :: maps tycos_of (Sign.const_typargs (Proof_Context.theory_of ctxt) (c, T)) haftmann@64940: val names = cTs haftmann@64940: |> map (prefix "eval_" o space_implode "_" o map ml_name_of o symbol_list) haftmann@64940: |> Name.variant_list []; haftmann@64940: in the o AList.lookup (op =) (cTs ~~ names) end; haftmann@64940: haftmann@64940: end; haftmann@64940: haftmann@64940: val generated_computationN = "Generated_Computation"; haftmann@64940: haftmann@64944: fun print_computation_code ctxt compiled_value requested_Ts cTs = haftmann@64940: let haftmann@64945: val proper_cTs = map_filter I cTs; haftmann@64945: val typ_sign_for = typ_signatures proper_cTs; haftmann@64940: fun add_typ T Ts = haftmann@64940: if member (op =) Ts T haftmann@64940: then Ts haftmann@64940: else Ts haftmann@64940: |> cons T haftmann@64940: |> fold (fold add_typ o snd) (typ_sign_for T); haftmann@64944: val required_Ts = fold add_typ requested_Ts []; haftmann@64944: val of_term_for_typ' = of_term_for_typ required_Ts; haftmann@64945: val eval_for_const' = eval_for_const ctxt proper_cTs; haftmann@64945: val eval_for_const'' = the_default "_" o Option.map eval_for_const'; haftmann@64945: val eval_tuple = enclose "(" ")" (commas (map eval_for_const' proper_cTs)); haftmann@64945: fun mk_abs s = "fn " ^ s ^ " => "; haftmann@64945: val eval_abs = space_implode "" haftmann@64945: (map (mk_abs o eval_for_const'') cTs); haftmann@64940: val of_term_code = print_of_term_funs { haftmann@64940: typ_sign_for = typ_sign_for, haftmann@64940: eval_for_const = eval_for_const', haftmann@64944: of_term_for_typ = of_term_for_typ' } required_Ts; haftmann@64940: in haftmann@64940: (cat_lines [ haftmann@64940: "structure " ^ generated_computationN ^ " =", haftmann@64940: "struct", haftmann@64940: "", haftmann@64940: "val " ^ eval_tuple ^ " = " ^ compiled_value ^ " ()", haftmann@64940: " (" ^ eval_abs, haftmann@64940: " " ^ eval_tuple ^ ");", haftmann@64940: "", haftmann@64940: of_term_code, haftmann@64940: "", haftmann@64940: "end" haftmann@64944: ], map (prefix (generated_computationN ^ ".") o of_term_for_typ') requested_Ts) haftmann@64940: end; haftmann@64940: haftmann@64943: fun check_typ ctxt T t = haftmann@64943: Syntax.check_term ctxt (Type.constraint T t); haftmann@64943: haftmann@64943: fun check_computation_input ctxt cTs t = haftmann@64943: let haftmann@64943: fun check t = check_comb (strip_comb t) haftmann@64943: and check_comb (t as Abs _, _) = haftmann@64943: error ("Bad term, contains abstraction: " ^ Syntax.string_of_term ctxt t) haftmann@64943: | check_comb (t as Const (cT as (c, T)), ts) = haftmann@64943: let haftmann@64943: val _ = if not (member (op =) cTs cT) haftmann@64943: then error ("Bad term, computation cannot proceed on constant " ^ Syntax.string_of_term ctxt t) haftmann@64943: else (); haftmann@64943: val _ = if not (monomorphic T) haftmann@64943: then error ("Bad term, contains polymorphic constant " ^ Syntax.string_of_term ctxt t) haftmann@64943: else (); haftmann@64943: val _ = map check ts; haftmann@64943: in () end; haftmann@64943: val _ = check t; haftmann@64943: in t end; haftmann@64943: haftmann@64940: fun compile_computation cookie ctxt T program evals vs_ty_evals deps = haftmann@64940: let haftmann@64945: fun the_const (Const cT) = cT haftmann@64945: | the_const t = error ("No constant after preprocessing: " ^ Syntax.string_of_term ctxt t) haftmann@64940: val raw_cTs = case evals of haftmann@64945: Abs (_, _, t) => (map the_const o snd o strip_comb) t haftmann@64940: | _ => error ("Bad term after preprocessing: " ^ Syntax.string_of_term ctxt evals); haftmann@64945: val cTs = fold_rev (fn cT => fn cTs => haftmann@64945: (if member (op =) cTs (SOME cT) then NONE else SOME cT) :: cTs) raw_cTs []; haftmann@64940: fun comp' vs_ty_evals = haftmann@64940: let haftmann@64940: val (generated_code, compiled_value) = haftmann@64940: build_computation_text ctxt NONE program deps vs_ty_evals; haftmann@64944: val (of_term_code, [of_term]) = print_computation_code ctxt compiled_value [T] cTs; haftmann@64940: in haftmann@64940: (generated_code ^ "\n" ^ of_term_code, haftmann@64944: enclose "(" ")" ("fn () => " ^ of_term)) haftmann@64940: end; haftmann@64940: val compiled_computation = haftmann@64940: Exn.release (run_computation_text cookie ctxt comp' vs_ty_evals []); haftmann@64940: in fn ctxt' => haftmann@64943: check_typ ctxt' T haftmann@64943: #> reject_vars ctxt' haftmann@64945: #> check_computation_input ctxt (map_filter I cTs) haftmann@64943: #> compiled_computation haftmann@64940: end; haftmann@64940: haftmann@64940: fun experimental_computation cookie { ctxt, lift_postproc, terms = ts, T } = haftmann@64940: let haftmann@64944: val _ = if not (monomorphic T) haftmann@64944: then error ("Polymorphic type: " ^ Syntax.string_of_typ ctxt T) haftmann@64944: else (); haftmann@64943: val cTs = (fold o fold_aterms) haftmann@64943: (fn (t as Const (cT as (_, T))) => haftmann@64943: if not (monomorphic T) then error ("Polymorphic constant:" ^ Syntax.string_of_term ctxt t) haftmann@64943: else insert (op =) cT | _ => I) ts []; haftmann@64944: val evals = Abs ("eval", map snd cTs ---> TFree (Name.aT, []), list_comb (Bound 0, map Const cTs)); haftmann@64940: val computation = Code_Thingol.dynamic_value ctxt haftmann@64940: (K I) (compile_computation cookie ctxt T) evals; haftmann@64940: in haftmann@64940: Code_Preproc.static_value { ctxt = ctxt, lift_postproc = lift_postproc, consts = [] } haftmann@64940: (K computation) haftmann@64940: end; haftmann@64940: haftmann@64940: haftmann@64940: (** code antiquotation **) haftmann@39404: haftmann@58557: fun evaluation_code ctxt module_name program tycos consts = haftmann@33992: let haftmann@55757: val thy = Proof_Context.theory_of ctxt; haftmann@48568: val (ml_modules, target_names) = haftmann@55757: Code_Target.produce_code_for ctxt haftmann@55683: target NONE module_name [] program false (map Constant consts @ map Type_Constructor tycos); haftmann@48568: val ml_code = space_implode "\n\n" (map snd ml_modules); haftmann@55147: val (consts', tycos') = chop (length consts) target_names; wenzelm@42359: val consts_map = map2 (fn const => wenzelm@42359: fn NONE => wenzelm@42359: error ("Constant " ^ (quote o Code.string_of_const thy) const ^ wenzelm@42359: "\nhas a user-defined serialization") haftmann@55147: | SOME const' => (const, const')) consts consts' wenzelm@42359: val tycos_map = map2 (fn tyco => wenzelm@42359: fn NONE => wenzelm@55304: error ("Type " ^ quote (Proof_Context.markup_type ctxt tyco) ^ wenzelm@42359: "\nhas a user-defined serialization") haftmann@55147: | SOME tyco' => (tyco, tyco')) tycos tycos'; haftmann@34028: in (ml_code, (tycos_map, consts_map)) end; haftmann@28054: haftmann@28054: local haftmann@28054: haftmann@38930: structure Code_Antiq_Data = Proof_Data haftmann@28054: ( haftmann@38930: type T = (string list * string list) * (bool haftmann@40421: * (string * (string * string) list) lazy); wenzelm@59150: val empty: T = (([], []), (true, (Lazy.value ("", [])))); wenzelm@59150: fun init _ = empty; haftmann@28054: ); haftmann@28054: haftmann@38930: val is_first_occ = fst o snd o Code_Antiq_Data.get; haftmann@28054: haftmann@30962: fun register_code new_tycos new_consts ctxt = haftmann@28054: let haftmann@38930: val ((tycos, consts), _) = Code_Antiq_Data.get ctxt; haftmann@30962: val tycos' = fold (insert (op =)) new_tycos tycos; haftmann@30962: val consts' = fold (insert (op =)) new_consts consts; haftmann@63159: val program = Code_Thingol.consts_program ctxt consts'; haftmann@38930: val acc_code = Lazy.lazy (fn () => haftmann@64940: evaluation_code ctxt Code_Target.generatedN program tycos' consts' haftmann@40422: |> apsnd snd); haftmann@38930: in Code_Antiq_Data.put ((tycos', consts'), (false, acc_code)) ctxt end; haftmann@30962: haftmann@30962: fun register_const const = register_code [] [const]; haftmann@28054: haftmann@40421: fun print_code is_first const ctxt = haftmann@30962: let haftmann@38930: val (_, (_, acc_code)) = Code_Antiq_Data.get ctxt; haftmann@40421: val (ml_code, consts_map) = Lazy.force acc_code; haftmann@40422: val ml_code = if is_first then ml_code else ""; wenzelm@59127: val body = ML_Context.struct_name ctxt ^ "." ^ the (AList.lookup (op =) consts_map const); wenzelm@41376: in (ml_code, body) end; haftmann@28054: haftmann@28054: in haftmann@28054: wenzelm@56069: fun ml_code_antiq raw_const ctxt = haftmann@28054: let wenzelm@53169: val thy = Proof_Context.theory_of ctxt; wenzelm@53169: val const = Code.check_const thy raw_const; wenzelm@53169: val is_first = is_first_occ ctxt; wenzelm@56069: in (print_code is_first const, register_const const ctxt) end; haftmann@30962: haftmann@28054: end; (*local*) haftmann@28054: haftmann@28054: haftmann@58558: (** reflection support **) haftmann@36470: haftmann@40421: fun check_datatype thy tyco some_consts = haftmann@36470: let haftmann@63174: val declared_constrs = (map fst o snd o fst o Code.get_type thy) tyco; haftmann@63174: val constrs = case some_consts haftmann@63174: of SOME [] => [] haftmann@63174: | SOME consts => haftmann@40421: let haftmann@63174: val missing_constrs = subtract (op =) consts declared_constrs; haftmann@40421: val _ = if null missing_constrs then [] wenzelm@45430: else error ("Missing constructor(s) " ^ commas_quote missing_constrs haftmann@40421: ^ " for datatype " ^ quote tyco); haftmann@63174: val false_constrs = subtract (op =) declared_constrs consts; haftmann@40421: val _ = if null false_constrs then [] wenzelm@45430: else error ("Non-constructor(s) " ^ commas_quote false_constrs haftmann@40421: ^ " for datatype " ^ quote tyco) haftmann@63174: in consts end haftmann@63174: | NONE => declared_constrs; haftmann@40421: in (tyco, constrs) end; haftmann@36470: haftmann@36470: fun add_eval_tyco (tyco, tyco') thy = haftmann@36470: let haftmann@36470: val k = Sign.arity_number thy tyco; haftmann@40421: fun pr pr' _ [] = tyco' haftmann@40421: | pr pr' _ [ty] = haftmann@36470: Code_Printer.concat [pr' Code_Printer.BR ty, tyco'] haftmann@40421: | pr pr' _ tys = haftmann@36470: Code_Printer.concat [Code_Printer.enum "," "(" ")" (map (pr' Code_Printer.BR) tys), tyco'] haftmann@36470: in haftmann@36470: thy haftmann@55150: |> Code_Target.set_printings (Type_Constructor (tyco, [(target, SOME (k, pr))])) haftmann@36470: end; haftmann@36470: haftmann@36514: fun add_eval_constr (const, const') thy = haftmann@36514: let haftmann@36514: val k = Code.args_number thy const; haftmann@36514: fun pr pr' fxy ts = Code_Printer.brackify fxy haftmann@38922: (const' :: the_list (Code_Printer.tuplify pr' Code_Printer.BR (map fst ts))); haftmann@36514: in haftmann@36514: thy haftmann@55150: |> Code_Target.set_printings (Constant (const, haftmann@52435: [(target, SOME (Code_Printer.simple_const_syntax (k, pr)))])) haftmann@36514: end; haftmann@36514: haftmann@55150: fun add_eval_const (const, const') = Code_Target.set_printings (Constant haftmann@52435: (const, [(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K) const')))])); haftmann@36470: haftmann@39912: fun process_reflection (code, (tyco_map, (constr_map, const_map))) module_name NONE thy = haftmann@38935: thy haftmann@38935: |> Code_Target.add_reserved target module_name haftmann@63163: |> Context.theory_map (compile_ML true code) haftmann@38935: |> fold (add_eval_tyco o apsnd Code_Printer.str) tyco_map haftmann@38935: |> fold (add_eval_constr o apsnd Code_Printer.str) constr_map haftmann@38935: |> fold (add_eval_const o apsnd Code_Printer.str) const_map haftmann@39912: | process_reflection (code, _) _ (SOME file_name) thy = haftmann@36470: let wenzelm@37950: val preamble = wenzelm@46737: "(* Generated from " ^ wenzelm@56208: Path.implode (Resources.thy_path (Path.basic (Context.theory_name thy))) ^ wenzelm@46737: "; DO NOT EDIT! *)"; haftmann@39912: val _ = File.write (Path.explode file_name) (preamble ^ "\n\n" ^ code); haftmann@36470: in haftmann@36470: thy haftmann@36470: end; haftmann@36470: haftmann@36470: fun gen_code_reflect prep_type prep_const raw_datatypes raw_functions module_name some_file thy = haftmann@36470: let haftmann@55757: val ctxt = Proof_Context.init_global thy; haftmann@36470: val datatypes = map (fn (raw_tyco, raw_cos) => haftmann@55757: (prep_type ctxt raw_tyco, (Option.map o map) (prep_const thy) raw_cos)) raw_datatypes; haftmann@40421: val (tycos, constrs) = map_split (uncurry (check_datatype thy)) datatypes haftmann@40421: |> apsnd flat; haftmann@36470: val functions = map (prep_const thy) raw_functions; haftmann@58557: val consts = constrs @ functions; haftmann@63159: val program = Code_Thingol.consts_program ctxt consts; haftmann@58557: val result = evaluation_code ctxt module_name program tycos consts haftmann@36514: |> (apsnd o apsnd) (chop (length constrs)); haftmann@36470: in haftmann@36470: thy haftmann@39485: |> process_reflection result module_name some_file haftmann@36470: end; haftmann@36470: haftmann@39422: val code_reflect = gen_code_reflect Code_Target.cert_tyco (K I); haftmann@36470: val code_reflect_cmd = gen_code_reflect Code_Target.read_tyco Code.read_const; haftmann@36470: haftmann@36470: haftmann@28054: (** Isar setup **) haftmann@28054: wenzelm@56069: val _ = wenzelm@56205: Theory.setup (ML_Antiquotation.declaration @{binding code} Args.term (fn _ => ml_code_antiq)); haftmann@28054: haftmann@36470: local haftmann@36470: wenzelm@36960: val parse_datatype = haftmann@63174: Parse.name -- Scan.optional (@{keyword "="} |-- haftmann@40711: (((Parse.sym_ident || Parse.string) >> (fn "_" => NONE | _ => Scan.fail ())) haftmann@63174: || ((Parse.term ::: (Scan.repeat (@{keyword "|"} |-- Parse.term))) >> SOME))) (SOME []); haftmann@36470: haftmann@36470: in haftmann@36470: haftmann@36470: val _ = wenzelm@59936: Outer_Syntax.command @{command_keyword code_reflect} wenzelm@46961: "enrich runtime environment with generated code" haftmann@63174: (Parse.name -- Scan.optional (@{keyword "datatypes"} |-- Parse.!!! (parse_datatype wenzelm@46949: ::: Scan.repeat (@{keyword "and"} |-- parse_datatype))) [] haftmann@52434: -- Scan.optional (@{keyword "functions"} |-- Parse.!!! (Scan.repeat1 Parse.name)) [] haftmann@52434: -- Scan.option (@{keyword "file"} |-- Parse.!!! Parse.name) wenzelm@46961: >> (fn (((module_name, raw_datatypes), raw_functions), some_file) => Toplevel.theory wenzelm@46961: (code_reflect_cmd raw_datatypes raw_functions module_name some_file))); haftmann@36470: haftmann@36470: end; (*local*) haftmann@36470: haftmann@39816: haftmann@39816: (** using external SML files as substitute for proper definitions -- only for polyml! **) haftmann@39816: haftmann@39816: local haftmann@39816: wenzelm@39820: structure Loaded_Values = Theory_Data wenzelm@39820: ( haftmann@39816: type T = string list haftmann@39816: val empty = [] wenzelm@41472: val extend = I wenzelm@39820: fun merge data : T = Library.merge (op =) data haftmann@39816: ); haftmann@39816: haftmann@39816: fun notify_val (string, value) = haftmann@39816: let wenzelm@62495: val _ = #enterVal ML_Env.name_space (string, value); wenzelm@53171: val _ = Theory.setup (Loaded_Values.map (insert (op =) string)); haftmann@39816: in () end; haftmann@39816: haftmann@39816: fun abort _ = error "Only value bindings allowed."; haftmann@39816: wenzelm@62494: val notifying_context : ML_Compiler0.context = wenzelm@62354: {name_space = wenzelm@62495: {lookupVal = #lookupVal ML_Env.name_space, wenzelm@62495: lookupType = #lookupType ML_Env.name_space, wenzelm@62495: lookupFix = #lookupFix ML_Env.name_space, wenzelm@62495: lookupStruct = #lookupStruct ML_Env.name_space, wenzelm@62495: lookupSig = #lookupSig ML_Env.name_space, wenzelm@62495: lookupFunct = #lookupFunct ML_Env.name_space, haftmann@39816: enterVal = notify_val, haftmann@39816: enterType = abort, haftmann@39816: enterFix = abort, haftmann@39816: enterStruct = abort, haftmann@39816: enterSig = abort, haftmann@39816: enterFunct = abort, wenzelm@62495: allVal = #allVal ML_Env.name_space, wenzelm@62495: allType = #allType ML_Env.name_space, wenzelm@62495: allFix = #allFix ML_Env.name_space, wenzelm@62495: allStruct = #allStruct ML_Env.name_space, wenzelm@62495: allSig = #allSig ML_Env.name_space, wenzelm@62495: allFunct = #allFunct ML_Env.name_space}, wenzelm@62716: print_depth = NONE, wenzelm@62495: here = #here ML_Env.context, wenzelm@62495: print = #print ML_Env.context, wenzelm@62495: error = #error ML_Env.context}; haftmann@39816: haftmann@39816: in haftmann@39816: haftmann@39816: fun use_file filepath thy = haftmann@39816: let haftmann@39816: val thy' = Loaded_Values.put [] thy; wenzelm@62889: val _ = Context.put_generic_context ((SOME o Context.Theory) thy'); wenzelm@60956: val _ = wenzelm@62902: ML_Compiler0.ML notifying_context wenzelm@60956: {line = 0, file = Path.implode filepath, verbose = false, debug = false} wenzelm@60956: (File.read filepath); wenzelm@62876: val thy'' = Context.the_global_context (); haftmann@39912: val names = Loaded_Values.get thy''; haftmann@40320: in (names, thy'') end; haftmann@39816: haftmann@39816: end; haftmann@39816: haftmann@39816: fun add_definiendum (ml_name, (b, T)) thy = haftmann@39816: thy haftmann@39816: |> Code_Target.add_reserved target ml_name wenzelm@63178: |> Specification.axiomatization [(b, SOME T, NoSyn)] [] [] [] haftmann@39816: |-> (fn ([Const (const, _)], _) => haftmann@55150: Code_Target.set_printings (Constant (const, haftmann@52435: [(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name)))])) haftmann@64940: #> tap (fn thy => Code_Target.produce_code (Proof_Context.init_global thy) false [const] target NONE Code_Target.generatedN [])); haftmann@39816: haftmann@39816: fun process_file filepath (definienda, thy) = haftmann@39816: let haftmann@39816: val (ml_names, thy') = use_file filepath thy; haftmann@39816: val superfluous = subtract (fn ((name1, _), name2) => name1 = name2) definienda ml_names; haftmann@39816: val _ = if null superfluous then () haftmann@39816: else error ("Value binding(s) " ^ commas_quote superfluous wenzelm@41944: ^ " found in external file " ^ Path.print filepath haftmann@39816: ^ " not present among the given contants binding(s)."); haftmann@39816: val these_definienda = AList.make (the o AList.lookup (op =) definienda) ml_names; haftmann@39816: val thy'' = fold add_definiendum these_definienda thy'; haftmann@39816: val definienda' = fold (AList.delete (op =)) ml_names definienda; haftmann@39816: in (definienda', thy'') end; haftmann@39816: haftmann@39816: fun polyml_as_definition bTs filepaths thy = haftmann@39816: let haftmann@39816: val definienda = map (fn bT => ((Binding.name_of o fst) bT, bT)) bTs; haftmann@39816: val (remaining, thy') = fold process_file filepaths (definienda, thy); haftmann@39816: val _ = if null remaining then () haftmann@39816: else error ("Constant binding(s) " ^ commas_quote (map fst remaining) haftmann@39816: ^ " not present in external file(s)."); haftmann@39816: in thy' end; haftmann@39816: haftmann@28054: end; (*struct*)