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@58643: val static_value': (Proof.context -> term -> 'a) cookie haftmann@58643: -> { ctxt: Proof.context, lift_postproc: (term -> term) -> 'a -> 'a, haftmann@58643: consts: (string * typ) list, T: typ } haftmann@58643: -> Proof.context -> term -> 'a option (*EXPERIMENTAL!*) haftmann@58643: val static_value_strict': (Proof.context -> term -> 'a) cookie haftmann@58643: -> { ctxt: Proof.context, lift_postproc: (term -> term) -> 'a -> 'a, haftmann@58643: consts: (string * typ) list, T: typ } haftmann@58643: -> Proof.context -> term -> 'a (*EXPERIMENTAL!*) haftmann@58558: val static_value_exn': (Proof.context -> term -> 'a) cookie haftmann@58558: -> { ctxt: Proof.context, lift_postproc: (term -> term) -> 'a -> 'a, haftmann@58558: consts: (string * typ) list, T: typ } haftmann@58558: -> Proof.context -> term -> 'a Exn.result (*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@39404: (** evaluation **) 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@44663: val structure_generated = "Generated_Code"; 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@57435: fun exec ctxt verbose code = wenzelm@60956: (if Config.get ctxt trace then tracing code else (); wenzelm@60956: ML_Context.exec (fn () => wenzelm@62495: ML_Compiler0.use_text ML_Env.context wenzelm@60956: {line = 0, file = "generated code", verbose = verbose, debug = false} code)); haftmann@39912: haftmann@39912: fun value ctxt (get, put, put_ml) (prelude, value) = haftmann@39912: let haftmann@39912: val code = (prelude haftmann@39912: ^ "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml wenzelm@62876: ^ " (fn () => " ^ value ^ ")) (Context.the_generic_context ())))"); haftmann@39912: val ctxt' = ctxt haftmann@39912: |> put (fn () => error ("Bad evaluation for " ^ quote put_ml)) haftmann@57435: |> Context.proof_map (exec ctxt false code); haftmann@39912: in get ctxt' () end; haftmann@39912: haftmann@39473: haftmann@39473: (* evaluation into target 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@55757: fun obtain_evaluator ctxt some_target program consts = haftmann@55757: let haftmann@55757: val evaluator' = Code_Target.evaluator ctxt (the_default target some_target) program consts false; haftmann@55757: in haftmann@55757: evaluator' haftmann@55757: #> apfst (fn ml_modules => space_implode "\n\n" (map snd ml_modules)) haftmann@55757: end; haftmann@39485: haftmann@55757: fun evaluation cookie ctxt evaluator vs_t args = haftmann@39404: let haftmann@41347: val (program_code, value_name) = evaluator 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@56920: fun evaluator program _ vs_ty_t deps = haftmann@56920: evaluation cookie ctxt (obtain_evaluator ctxt some_target program deps) vs_ty_t args; wenzelm@61077: in Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator 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_evaluator cookie ctxt some_target { program, deps } = haftmann@39473: let haftmann@56973: val evaluator = obtain_evaluator ctxt some_target program (map Constant deps); haftmann@55757: val evaluation' = evaluation cookie ctxt evaluator; haftmann@56920: in fn _ => fn _ => fn vs_ty_t => fn _ => evaluation' vs_ty_t [] end; haftmann@39473: haftmann@56973: fun static_value_exn cookie { ctxt, target, lift_postproc, consts } = haftmann@55757: let haftmann@56973: val evaluator = Code_Thingol.static_value { ctxt = ctxt, wenzelm@61077: lift_postproc = Exn.map_res o lift_postproc, consts = consts } haftmann@56973: (static_evaluator cookie ctxt target); haftmann@55757: in fn ctxt' => evaluator ctxt' o reject_vars ctxt' end; haftmann@39473: haftmann@56973: fun static_value_strict cookie = Exn.release ooo static_value_exn cookie; haftmann@41347: haftmann@56973: fun static_value cookie = partiality_as_none ooo static_value_exn cookie; 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@55757: val result = case partiality_as_none (evaluation 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@56920: check_holds_oracle ctxt (obtain_evaluator 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@56973: Code_Thingol.static_conv ctxt_consts (fn { program, deps } => fn ctxt' => fn vs_t => haftmann@56973: K (check_holds_oracle ctxt' (obtain_evaluator ctxt NONE program (map Constant deps)) vs_t o reject_vars ctxt')); haftmann@41349: haftmann@41349: end; (*local*) haftmann@39404: haftmann@39404: haftmann@58558: (** full static evaluation -- still with limited coverage! **) 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@58558: fun typ_signatures_for T = haftmann@58558: let haftmann@58558: val (Ts, T') = strip_type T; haftmann@58558: in map_range (fn n => (drop n Ts ---> T', take n Ts)) (length Ts + 1) end; haftmann@28054: haftmann@58558: fun typ_signatures cTs = haftmann@58558: let haftmann@58558: fun add (c, T) = haftmann@58558: fold (fn (T, Ts) => Typtab.map_default (T, []) (cons (c, Ts))) haftmann@58558: (typ_signatures_for T); haftmann@58558: in haftmann@58558: Typtab.empty haftmann@58558: |> fold add cTs haftmann@58558: |> Typtab.lookup_list haftmann@58558: end; haftmann@58558: haftmann@58558: fun print_of_term_funs { typ_sign_for, ml_name_for_const, ml_name_for_typ } Ts = haftmann@58558: let haftmann@58558: val var_names = map_range (fn n => "t" ^ string_of_int (n + 1)); haftmann@58558: fun print_lhs c xs = "Const (" ^ quote c ^ ", _)" haftmann@58558: |> fold (fn x => fn s => s ^ " $ " ^ x) xs haftmann@58558: |> enclose "(" ")" haftmann@58558: |> prefix "ctxt "; haftmann@58558: fun print_rhs c Ts xs = ml_name_for_const c haftmann@58558: |> fold2 (fn T => fn x => fn s => haftmann@58558: s ^ (" (" ^ ml_name_for_typ T ^ " ctxt " ^ x ^ ")")) Ts xs haftmann@58558: fun print_eq (c, Ts) = haftmann@58558: let haftmann@58558: val xs = var_names (length Ts); haftmann@58558: in print_lhs c xs ^ " = " ^ print_rhs c Ts xs end; haftmann@58558: val err_eq = haftmann@58558: "ctxt t = error (" ^ quote "Bad term: " ^ " ^ Syntax.string_of_term ctxt t)"; haftmann@58558: fun print_eqs T = haftmann@58558: let haftmann@58558: val typ_signs = typ_sign_for T; haftmann@58558: val name = ml_name_for_typ T; haftmann@58558: in haftmann@58558: (map print_eq typ_signs @ [err_eq]) haftmann@58558: |> map (prefix (name ^ " ")) haftmann@58558: |> space_implode "\n | " haftmann@58558: end; haftmann@58558: in haftmann@58558: map print_eqs Ts haftmann@58558: |> space_implode "\nand " haftmann@58558: |> prefix "fun " haftmann@58558: |> pair (map ml_name_for_typ Ts) haftmann@58558: end; haftmann@58558: haftmann@58558: fun print_of_term ctxt ml_name_for_const T cTs = haftmann@58558: let haftmann@58558: val typ_sign_for = typ_signatures cTs; haftmann@58558: fun add_typ T Ts = haftmann@58558: if member (op =) Ts T haftmann@58558: then Ts haftmann@58558: else Ts haftmann@58558: |> cons T haftmann@58558: |> fold (fold add_typ o snd) (typ_sign_for T); haftmann@58558: val Ts = add_typ T []; haftmann@58558: fun tycos_of (Type (tyco, Ts)) = maps tycos_of Ts @ [tyco] haftmann@58558: | tycos_of _ = []; haftmann@58558: val ml_name_of = Name.desymbolize NONE o Long_Name.base_name; haftmann@58558: val ml_names = map (suffix "_of_term" o space_implode "_" o map ml_name_of o tycos_of) Ts haftmann@58558: |> Name.variant_list []; haftmann@58558: val ml_name_for_typ = the o AList.lookup (op =) (Ts ~~ ml_names); haftmann@58558: in haftmann@58558: print_of_term_funs { typ_sign_for = typ_sign_for, haftmann@58558: ml_name_for_const = ml_name_for_const, haftmann@58558: ml_name_for_typ = ml_name_for_typ } Ts haftmann@58558: end; haftmann@58558: haftmann@58558: fun compile_evaluator cookie ctxt cs_code cTs T { program, deps } = haftmann@58558: let haftmann@58558: val (context_code, (_, const_map)) = haftmann@58558: evaluation_code ctxt structure_generated program [] cs_code; haftmann@58558: val ml_name_for_const = the o AList.lookup (op =) const_map; haftmann@58558: val (ml_names, of_term_code) = print_of_term ctxt ml_name_for_const T cTs haftmann@58558: val of_term = value ctxt cookie (context_code ^ "\n" ^ of_term_code, List.last ml_names); haftmann@58558: in fn ctxt' => fn t => fn _ => fn _ => Exn.interruptible_capture (of_term ctxt') t end; haftmann@58558: haftmann@58558: fun static_value_exn' cookie { ctxt, lift_postproc, consts, T } = haftmann@58558: let haftmann@58558: val thy = Proof_Context.theory_of ctxt; haftmann@58558: val cs_code = map (Axclass.unoverload_const thy) consts; haftmann@58558: val cTs = map2 (fn (_, T) => fn c => (c, T)) consts cs_code; haftmann@58558: val evaluator = Code_Thingol.static_value { ctxt = ctxt, wenzelm@61077: lift_postproc = Exn.map_res o lift_postproc, consts = cs_code } haftmann@58558: (compile_evaluator cookie ctxt cs_code cTs T); haftmann@58558: in fn ctxt' => haftmann@58558: evaluator ctxt' o reject_vars ctxt' o Syntax.check_term ctxt' o Type.constraint T haftmann@58558: end; haftmann@58558: haftmann@58643: fun static_value_strict' cookie = Exn.release ooo static_value_exn' cookie; haftmann@58643: haftmann@58643: fun static_value' cookie = partiality_as_none ooo static_value_exn' cookie; haftmann@58643: haftmann@58558: haftmann@58558: (** code antiquotation **) 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@58557: val program = Code_Thingol.consts_program (Proof_Context.theory_of ctxt) consts'; haftmann@38930: val acc_code = Lazy.lazy (fn () => haftmann@58557: evaluation_code ctxt structure_generated 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@40726: val constrs = (map fst o snd o fst o Code.get_type thy) tyco; haftmann@40421: val _ = case some_consts haftmann@40421: of SOME consts => haftmann@40421: let haftmann@40421: val missing_constrs = subtract (op =) consts 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@40421: val false_constrs = subtract (op =) 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@40421: in () end haftmann@40421: | NONE => (); 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@57435: |> Context.theory_map (exec (Proof_Context.init_global thy (*FIXME*)) 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@58557: val program = Code_Thingol.consts_program (Proof_Context.theory_of 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 = wenzelm@46949: Parse.name --| @{keyword "="} -- haftmann@40711: (((Parse.sym_ident || Parse.string) >> (fn "_" => NONE | _ => Scan.fail ())) wenzelm@46949: || ((Parse.term ::: (Scan.repeat (@{keyword "|"} |-- Parse.term))) >> 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@52434: (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; haftmann@39816: val _ = Context.set_thread_data ((SOME o Context.Theory) thy'); wenzelm@60956: val _ = wenzelm@62494: ML_Compiler0.use_text 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 haftmann@39816: |> 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@55757: #> tap (fn thy => Code_Target.produce_code (Proof_Context.init_global thy) false [const] target NONE structure_generated [])); 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*)