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@55757: val dynamic_holds_conv: Proof.context -> conv 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@64987: val mount_computation: Proof.context -> (string * typ) list -> typ haftmann@64988: -> (term -> 'ml) -> ((term -> term) -> 'ml option -> 'a) -> Proof.context -> term -> 'a haftmann@64989: val mount_computation_conv: Proof.context -> (string * typ) list -> typ haftmann@65043: -> (term -> 'ml) -> (Proof.context -> 'ml -> conv) -> Proof.context -> conv haftmann@64989: val mount_computation_check: Proof.context -> (string * typ) list haftmann@64989: -> (term -> truth) -> Proof.context -> conv haftmann@64987: val polyml_as_definition: (binding * typ) list -> Path.T list -> theory -> theory haftmann@57435: val trace: bool Config.T 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@64957: (** ML compiler as evaluation environment **) haftmann@33992: haftmann@39473: (* technical prerequisites *) haftmann@39473: haftmann@64959: val thisN = "Code_Runtime"; haftmann@64987: val prefix_this = Long_Name.append thisN; haftmann@64987: val truthN = prefix_this "truth"; haftmann@64987: val HoldsN = prefix_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@64959: [(target, SOME (0, (K o K o K) (Code_Printer.str truthN)))])) haftmann@55150: #> Code_Target.set_printings (Constant (@{const_name Code_Generator.holds}, haftmann@64959: [(target, SOME (Code_Printer.plain_const_syntax HoldsN))])) haftmann@64959: #> Code_Target.add_reserved target thisN 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@64957: |> put (fn () => error ("Bad compilation 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@64957: (* 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@64957: fun build_compilation_text ctxt some_target program consts = haftmann@64957: Code_Target.compilation_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@64957: fun run_compilation_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@64957: run_compilation_text cookie ctxt (build_compilation_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@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@64987: val truth_cookie = (Truth_Result.get, put_truth, prefix_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@64957: val result = case partiality_as_none (run_compilation_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@64957: check_holds_oracle ctxt (build_compilation_text ctxt NONE program deps) vs_t) haftmann@55757: o reject_vars ctxt; haftmann@39473: haftmann@41349: end; (*local*) haftmann@39404: haftmann@39404: haftmann@64957: (** generator for computations -- partial implementations of the universal morphism from Isabelle to ML terms **) haftmann@64957: haftmann@64957: (* auxiliary *) haftmann@64940: haftmann@64957: val generated_computationN = "Generated_Computation"; haftmann@64957: haftmann@64957: haftmann@64957: (* possible type signatures of constants *) haftmann@64943: haftmann@64990: fun typ_signatures' 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@64990: (typ_signatures' T); haftmann@64940: in haftmann@64940: Typtab.empty haftmann@64940: |> fold add cTs haftmann@64940: |> Typtab.lookup_list haftmann@64940: end; haftmann@64940: haftmann@64957: haftmann@64957: (* name mangling *) haftmann@64957: haftmann@64957: local haftmann@64957: haftmann@64957: fun tycos_of (Type (tyco, Ts)) = maps tycos_of Ts @ [tyco] haftmann@64957: | tycos_of _ = []; haftmann@64957: haftmann@64957: val ml_name_of = Name.desymbolize NONE o Long_Name.base_name; haftmann@64957: haftmann@64957: in haftmann@64957: haftmann@64959: val covered_constsN = "covered_consts"; haftmann@64959: haftmann@64957: fun of_term_for_typ Ts = haftmann@64957: let haftmann@64957: val names = Ts haftmann@64957: |> map (suffix "_of_term" o space_implode "_" o map ml_name_of o tycos_of) haftmann@64957: |> Name.variant_list []; haftmann@64957: in the o AList.lookup (op =) (Ts ~~ names) end; haftmann@64957: haftmann@64957: fun eval_for_const ctxt cTs = haftmann@64957: let haftmann@64957: fun symbol_list (c, T) = c :: maps tycos_of (Sign.const_typargs (Proof_Context.theory_of ctxt) (c, T)) haftmann@64957: val names = cTs haftmann@64957: |> map (prefix "eval_" o space_implode "_" o map ml_name_of o symbol_list) haftmann@64957: |> Name.variant_list []; haftmann@64957: in the o AList.lookup (op =) (cTs ~~ names) end; haftmann@64957: haftmann@64957: end; haftmann@64957: haftmann@64957: haftmann@64957: (* checks for input terms *) haftmann@64957: haftmann@64957: fun monomorphic T = fold_atyps ((K o K) false) T true; haftmann@64957: haftmann@64957: fun check_typ ctxt T t = haftmann@64957: Syntax.check_term ctxt (Type.constraint T t); haftmann@64957: haftmann@64957: fun check_computation_input ctxt cTs t = haftmann@64957: let haftmann@64957: fun check t = check_comb (strip_comb t) haftmann@64957: and check_comb (t as Abs _, _) = haftmann@64957: error ("Bad term, contains abstraction: " ^ Syntax.string_of_term ctxt t) haftmann@64957: | check_comb (t as Const (cT as (c, T)), ts) = haftmann@64957: let haftmann@64957: val _ = if not (member (op =) cTs cT) haftmann@64957: then error ("Bad term, computation cannot proceed on constant " ^ Syntax.string_of_term ctxt t) haftmann@64957: else (); haftmann@64957: val _ = if not (monomorphic T) haftmann@64957: then error ("Bad term, contains polymorphic constant " ^ Syntax.string_of_term ctxt t) haftmann@64957: else (); haftmann@64957: val _ = map check ts; haftmann@64957: in () end; haftmann@64957: val _ = check t; haftmann@64957: in t end; haftmann@64957: haftmann@64957: haftmann@64957: (* code generation for of the universal morphism *) haftmann@64957: haftmann@64959: val print_const = ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_typ; haftmann@64959: haftmann@64990: fun print_of_term_funs { typ_signatures_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@64990: val typ_signs = typ_signatures_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@64990: fun print_computation_code ctxt compiled_value [] requested_Ts = haftmann@64990: if null requested_Ts then ("", []) haftmann@64990: else error ("No equation available for requested type " haftmann@64990: ^ Syntax.string_of_typ ctxt (hd requested_Ts)) haftmann@64959: | print_computation_code ctxt compiled_value cTs requested_Ts = haftmann@64959: let haftmann@64959: val proper_cTs = map_filter I cTs; haftmann@64990: val typ_signatures_for = typ_signatures proper_cTs; haftmann@64959: fun add_typ T Ts = haftmann@64959: if member (op =) Ts T haftmann@64959: then Ts haftmann@64990: else case typ_signatures_for T of haftmann@64990: [] => error ("No equation available for requested type " haftmann@64990: ^ Syntax.string_of_typ ctxt T) haftmann@64990: | typ_signs => haftmann@64990: Ts haftmann@64990: |> cons T haftmann@64990: |> fold (fold add_typ o snd) typ_signs; haftmann@64959: val required_Ts = fold add_typ requested_Ts []; haftmann@64959: val of_term_for_typ' = of_term_for_typ required_Ts; haftmann@64959: val eval_for_const' = eval_for_const ctxt proper_cTs; haftmann@64959: val eval_for_const'' = the_default "_" o Option.map eval_for_const'; haftmann@64959: val eval_tuple = enclose "(" ")" (commas (map eval_for_const' proper_cTs)); haftmann@64959: fun mk_abs s = "fn " ^ s ^ " => "; haftmann@64959: val eval_abs = space_implode "" haftmann@64959: (map (mk_abs o eval_for_const'') cTs); haftmann@64959: val of_term_code = print_of_term_funs { haftmann@64990: typ_signatures_for = typ_signatures_for, haftmann@64959: eval_for_const = eval_for_const', haftmann@64959: of_term_for_typ = of_term_for_typ' } required_Ts; haftmann@64959: val of_term_names = map (Long_Name.append generated_computationN haftmann@64959: o of_term_for_typ') requested_Ts; haftmann@64959: in haftmann@64959: cat_lines [ haftmann@64959: "structure " ^ generated_computationN ^ " =", haftmann@64959: "struct", haftmann@64959: "", haftmann@64959: "val " ^ covered_constsN ^ " = " ^ ML_Syntax.print_list print_const proper_cTs ^ ";", haftmann@64959: "", haftmann@64959: "val " ^ eval_tuple ^ " = " ^ compiled_value ^ " ()", haftmann@64959: " (" ^ eval_abs, haftmann@64959: " " ^ eval_tuple ^ ");", haftmann@64959: "", haftmann@64959: of_term_code, haftmann@64959: "", haftmann@64959: "end" haftmann@64959: ] |> rpair of_term_names haftmann@64959: end; haftmann@64940: haftmann@64993: haftmann@64993: (* dedicated preprocessor for computations *) haftmann@64993: haftmann@64993: structure Computation_Preproc_Data = Theory_Data haftmann@64993: ( haftmann@64993: type T = thm list; haftmann@64993: val empty = []; haftmann@64993: val extend = I; haftmann@64993: val merge = Library.merge Thm.eq_thm_prop; haftmann@64993: ); haftmann@64993: haftmann@64993: local haftmann@64993: haftmann@64993: fun add thm thy = haftmann@64993: let haftmann@64993: val thms = Simplifier.mksimps (Proof_Context.init_global thy) thm; haftmann@64993: in haftmann@64993: thy haftmann@64993: |> Computation_Preproc_Data.map (union Thm.eq_thm_prop thms) haftmann@64993: end; haftmann@64993: haftmann@64993: fun get ctxt = Computation_Preproc_Data.get (Proof_Context.theory_of ctxt); haftmann@64993: haftmann@64993: in haftmann@64993: haftmann@64995: fun preprocess_conv { ctxt } = haftmann@64995: let haftmann@64995: val rules = get ctxt; haftmann@64995: in fn ctxt' => Raw_Simplifier.rewrite ctxt' false rules end; haftmann@64993: haftmann@64995: fun preprocess_term { ctxt } = haftmann@64995: let haftmann@64995: val rules = map (Logic.dest_equals o Thm.plain_prop_of) (get ctxt); haftmann@64995: in fn ctxt' => Pattern.rewrite_term (Proof_Context.theory_of ctxt') rules [] end; haftmann@64993: haftmann@64993: val _ = Theory.setup haftmann@64993: (Attrib.setup @{binding code_computation_unfold} haftmann@64993: (Scan.succeed (Thm.declaration_attribute (fn thm => Context.mapping (add thm) I))) haftmann@64993: "preprocessing equations for computation"); haftmann@64993: haftmann@64993: end; haftmann@64993: haftmann@64993: haftmann@64993: (* mounting computations *) haftmann@64993: haftmann@64991: fun prechecked_computation T raw_computation ctxt = haftmann@64987: check_typ ctxt T haftmann@64987: #> reject_vars ctxt haftmann@64991: #> raw_computation ctxt; haftmann@64991: haftmann@64991: fun prechecked_conv T raw_conv ctxt = haftmann@64991: tap (check_typ ctxt T o reject_vars ctxt o Thm.term_of) haftmann@64991: #> raw_conv ctxt; haftmann@64991: haftmann@64991: fun checked_computation cTs raw_computation ctxt = haftmann@64991: check_computation_input ctxt cTs haftmann@65005: #> Exn.interruptible_capture raw_computation haftmann@64988: #> partiality_as_none; haftmann@64987: haftmann@64957: fun mount_computation ctxt cTs T raw_computation lift_postproc = haftmann@64993: let haftmann@64995: val preprocess = preprocess_term { ctxt = ctxt }; haftmann@64993: val computation = prechecked_computation T (Code_Preproc.static_value haftmann@64993: { ctxt = ctxt, lift_postproc = lift_postproc, consts = [] } haftmann@64993: (K (checked_computation cTs raw_computation))); haftmann@64995: in fn ctxt' => preprocess ctxt' #> computation ctxt' end; haftmann@64943: haftmann@64989: fun mount_computation_conv ctxt cTs T raw_computation conv = haftmann@64993: let haftmann@64995: val preprocess = preprocess_conv { ctxt = ctxt }; haftmann@64993: val computation_conv = prechecked_conv T (Code_Preproc.static_conv haftmann@64993: { ctxt = ctxt, consts = [] } haftmann@64993: (K (fn ctxt' => fn t => haftmann@64993: case checked_computation cTs raw_computation ctxt' t of haftmann@65043: SOME x => conv ctxt' x haftmann@64993: | NONE => Conv.all_conv))); haftmann@64995: in fn ctxt' => preprocess ctxt' then_conv computation_conv ctxt' end; haftmann@64989: haftmann@64989: local haftmann@64989: haftmann@64989: fun holds ct = Thm.mk_binop @{cterm "Pure.eq :: prop \ prop \ prop"} haftmann@64989: ct @{cprop "PROP Code_Generator.holds"}; haftmann@64989: haftmann@64989: val (_, holds_oracle) = Context.>>> (Context.map_theory_result haftmann@64989: (Thm.add_oracle (@{binding holds}, holds))); haftmann@64989: haftmann@64989: in haftmann@64989: haftmann@64989: fun mount_computation_check ctxt cTs raw_computation = haftmann@64989: mount_computation_conv ctxt cTs @{typ prop} raw_computation haftmann@65043: ((K o K) holds_oracle); haftmann@64989: haftmann@64989: end; haftmann@64989: haftmann@64959: haftmann@64959: (** variants of universal runtime code generation **) haftmann@64940: haftmann@64959: (*FIXME consolidate variants*) haftmann@64940: haftmann@64959: fun runtime_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@64959: fun runtime_code' ctxt some_module_name named_tycos named_consts computation_Ts program evals vs_ty_evals deps = haftmann@64959: let haftmann@64959: val thy = Proof_Context.theory_of ctxt; haftmann@64959: fun the_const (Const cT) = cT haftmann@64959: | the_const t = error ("No constant after preprocessing: " ^ Syntax.string_of_term ctxt t) haftmann@64959: val raw_computation_cTs = case evals of haftmann@64959: Abs (_, _, t) => (map the_const o snd o strip_comb) t haftmann@64959: | _ => error ("Bad term after preprocessing: " ^ Syntax.string_of_term ctxt evals); haftmann@64959: val computation_cTs = fold_rev (fn cT => fn cTs => haftmann@64959: (if member (op =) cTs (SOME cT) then NONE else SOME cT) :: cTs) raw_computation_cTs []; haftmann@64959: val consts' = fold (fn NONE => I | SOME (c, _) => insert (op =) c) haftmann@64959: computation_cTs named_consts; haftmann@64959: val program' = Code_Thingol.consts_program ctxt consts'; haftmann@64959: (*FIXME insufficient interfaces require double invocation of code generator*) haftmann@65034: val program'' = Code_Symbol.Graph.merge (K true) (program, program'); haftmann@64959: val ((ml_modules, compiled_value), deresolve) = haftmann@65034: Code_Target.compilation_text' ctxt target some_module_name program'' haftmann@64959: (map Code_Symbol.Type_Constructor named_tycos @ map Code_Symbol.Constant consts' @ deps) true vs_ty_evals; haftmann@64959: (*FIXME constrain signature*) haftmann@67328: fun deresolve_tyco tyco = case (deresolve o Code_Symbol.Type_Constructor) tyco of haftmann@67328: NONE => error ("Type " ^ quote (Proof_Context.markup_type ctxt tyco) ^ haftmann@67328: "\nhas a user-defined serialization") haftmann@67328: | SOME c' => c'; haftmann@64959: fun deresolve_const c = case (deresolve o Code_Symbol.Constant) c of haftmann@64959: NONE => error ("Constant " ^ (quote o Code.string_of_const thy) c ^ haftmann@64959: "\nhas a user-defined serialization") haftmann@64959: | SOME c' => c'; haftmann@67328: val tyco_names = map deresolve_tyco named_tycos; haftmann@64959: val const_names = map deresolve_const named_consts; haftmann@64959: val generated_code = space_implode "\n\n" (map snd ml_modules); haftmann@64959: val (of_term_code, of_term_names) = haftmann@64959: print_computation_code ctxt compiled_value computation_cTs computation_Ts; haftmann@64959: val compiled_computation = generated_code ^ "\n" ^ of_term_code; haftmann@64959: in haftmann@64959: compiled_computation haftmann@64959: |> rpair { tyco_map = named_tycos ~~ tyco_names, haftmann@64959: const_map = named_consts ~~ const_names, haftmann@64959: of_term_map = computation_Ts ~~ of_term_names } haftmann@64959: end; haftmann@64959: haftmann@64959: fun funs_of_maps { tyco_map, const_map, of_term_map } = haftmann@64959: { name_for_tyco = the o AList.lookup (op =) tyco_map, haftmann@64959: name_for_const = the o AList.lookup (op =) const_map, haftmann@64959: of_term_for_typ = the o AList.lookup (op =) of_term_map }; haftmann@64959: haftmann@64959: fun runtime_code ctxt some_module_name named_tycos named_consts computation_Ts program evals vs_ty_evals deps = haftmann@64959: runtime_code' ctxt some_module_name named_tycos named_consts computation_Ts program evals vs_ty_evals deps haftmann@64959: ||> funs_of_maps; haftmann@64959: haftmann@64959: haftmann@64959: (** code and computation antiquotations **) haftmann@64959: haftmann@64989: local haftmann@64959: haftmann@64989: val mount_computationN = prefix_this "mount_computation"; haftmann@64989: val mount_computation_convN = prefix_this "mount_computation_conv"; haftmann@64989: val mount_computation_checkN = prefix_this "mount_computation_check"; haftmann@28054: haftmann@38930: structure Code_Antiq_Data = Proof_Data haftmann@28054: ( haftmann@64955: type T = { named_consts: string list, haftmann@64959: computation_Ts: typ list, computation_cTs: (string * typ) list, haftmann@64959: position_index: int, haftmann@64959: generated_code: (string * { haftmann@64959: name_for_tyco: string -> string, haftmann@64959: name_for_const: string -> string, haftmann@64959: of_term_for_typ: typ -> string haftmann@64959: }) lazy haftmann@64955: }; haftmann@64955: val empty: T = { named_consts = [], haftmann@64959: computation_Ts = [], computation_cTs = [], haftmann@64959: position_index = 0, haftmann@64959: generated_code = Lazy.lazy (fn () => raise Fail "empty") haftmann@64955: }; wenzelm@59150: fun init _ = empty; haftmann@28054: ); haftmann@28054: haftmann@64959: val current_position_index = #position_index o Code_Antiq_Data.get; haftmann@64955: haftmann@64959: fun register { named_consts, computation_Ts, computation_cTs } ctxt = haftmann@64955: let haftmann@64959: val data = Code_Antiq_Data.get ctxt; haftmann@64959: val named_consts' = union (op =) named_consts (#named_consts data); haftmann@64959: val computation_Ts' = union (op =) computation_Ts (#computation_Ts data); haftmann@64959: val computation_cTs' = union (op =) computation_cTs (#computation_cTs data); haftmann@64959: val position_index' = #position_index data + 1; haftmann@64959: fun generated_code' () = haftmann@64959: let haftmann@64959: val evals = Abs ("eval", map snd computation_cTs' ---> haftmann@64993: TFree (Name.aT, []), list_comb (Bound 0, map Const computation_cTs')) haftmann@64995: |> preprocess_term { ctxt = ctxt } ctxt haftmann@64959: in Code_Thingol.dynamic_value ctxt haftmann@64959: (K I) (runtime_code ctxt NONE [] named_consts' computation_Ts') evals haftmann@64959: end; haftmann@64955: in haftmann@64955: ctxt haftmann@64955: |> Code_Antiq_Data.put { haftmann@64959: named_consts = named_consts', haftmann@64959: computation_Ts = computation_Ts', haftmann@64959: computation_cTs = computation_cTs', haftmann@64959: position_index = position_index', haftmann@64959: generated_code = Lazy.lazy generated_code' haftmann@64955: } haftmann@64955: end; haftmann@30962: haftmann@64959: fun register_const const = haftmann@64959: register { named_consts = [const], haftmann@64959: computation_Ts = [], haftmann@64959: computation_cTs = [] }; haftmann@64959: haftmann@64959: fun register_computation cTs T = haftmann@64959: register { named_consts = [], haftmann@64959: computation_Ts = [T], haftmann@64959: computation_cTs = cTs }; haftmann@64959: haftmann@64959: fun print body_code_for ctxt ctxt' = haftmann@30962: let haftmann@64959: val position_index = current_position_index ctxt; haftmann@64959: val (code, name_ofs) = (Lazy.force o #generated_code o Code_Antiq_Data.get) ctxt'; haftmann@64959: val context_code = if position_index = 0 then code else ""; haftmann@64989: val body_code = body_code_for name_ofs (ML_Context.struct_name ctxt'); haftmann@64958: in (context_code, body_code) end; haftmann@28054: haftmann@64959: fun print_code ctxt const = haftmann@64989: print (fn { name_for_const, ... } => fn prfx => haftmann@64959: Long_Name.append prfx (name_for_const const)) ctxt; haftmann@64959: haftmann@64989: fun print_computation kind ctxt T = haftmann@64989: print (fn { of_term_for_typ, ... } => fn prfx => haftmann@64959: space_implode " " [ haftmann@64989: kind, haftmann@64959: "(Context.proof_of (Context.the_generic_context ()))", haftmann@64959: Long_Name.implode [prfx, generated_computationN, covered_constsN], haftmann@64959: (ML_Syntax.atomic o ML_Syntax.print_typ) T, haftmann@64959: Long_Name.append prfx (of_term_for_typ T) haftmann@64959: ]) ctxt; haftmann@64959: haftmann@64989: fun print_computation_check ctxt = haftmann@64989: print (fn { of_term_for_typ, ... } => fn prfx => haftmann@64989: space_implode " " [ haftmann@64989: mount_computation_checkN, haftmann@64989: "(Context.proof_of (Context.the_generic_context ()))", haftmann@64989: Long_Name.implode [prfx, generated_computationN, covered_constsN], haftmann@64989: Long_Name.append prfx (of_term_for_typ @{typ prop}) haftmann@64989: ]) ctxt; haftmann@64989: haftmann@64992: haftmann@64992: fun add_all_constrs ctxt (dT as Type (tyco, Ts)) = haftmann@67327: case Code.get_type (Proof_Context.theory_of ctxt) tyco of haftmann@67327: ((vs, constrs), false) => haftmann@67327: let haftmann@67327: val subst_TFree = the o AList.lookup (op =) (map fst vs ~~ Ts); haftmann@67327: val cs = map (fn (c, (_, Ts')) => haftmann@67327: (c, (map o map_atyps) (fn TFree (v, _) => subst_TFree v) Ts' haftmann@67327: ---> dT)) constrs; haftmann@67327: in haftmann@67327: union (op =) cs haftmann@67327: #> fold (add_all_constrs ctxt) Ts haftmann@67327: end haftmann@67327: | (_, true) => I; haftmann@64992: haftmann@64992: fun prep_spec ctxt (raw_ts, raw_dTs) = haftmann@64989: let haftmann@64989: val ts = map (Syntax.check_term ctxt) raw_ts; haftmann@64992: val dTs = map (Syntax.check_typ ctxt) raw_dTs; haftmann@64989: in haftmann@64992: [] haftmann@64992: |> (fold o fold_aterms) haftmann@64989: (fn (t as Const (cT as (_, T))) => haftmann@64989: if not (monomorphic T) then error ("Polymorphic constant: " ^ Syntax.string_of_term ctxt t) haftmann@64992: else insert (op =) cT | _ => I) ts haftmann@64992: |> fold (fn dT => haftmann@64992: if not (monomorphic dT) then error ("Polymorphic datatype: " ^ Syntax.string_of_typ ctxt dT) haftmann@64992: else add_all_constrs ctxt dT) dTs haftmann@64989: end; haftmann@64989: 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; haftmann@64959: in (print_code ctxt const, register_const const ctxt) end; haftmann@64959: haftmann@64992: fun gen_ml_computation_antiq kind (raw_T, raw_spec) ctxt = haftmann@64959: let haftmann@64992: val cTs = prep_spec ctxt raw_spec; haftmann@64959: val T = Syntax.check_typ ctxt raw_T; haftmann@64959: val _ = if not (monomorphic T) haftmann@64959: then error ("Polymorphic type: " ^ Syntax.string_of_typ ctxt T) haftmann@64959: else (); haftmann@64989: in (print_computation kind ctxt T, register_computation cTs T ctxt) end; haftmann@64989: haftmann@64989: val ml_computation_antiq = gen_ml_computation_antiq mount_computationN; haftmann@64989: haftmann@64989: val ml_computation_conv_antiq = gen_ml_computation_antiq mount_computation_convN; haftmann@64989: haftmann@64992: fun ml_computation_check_antiq raw_spec ctxt = haftmann@64989: let haftmann@64992: val cTs = insert (op =) (dest_Const @{const holds}) (prep_spec ctxt raw_spec); haftmann@64989: in (print_computation_check ctxt, register_computation cTs @{typ prop} 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@64959: val result = runtime_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: haftmann@64992: local haftmann@64992: haftmann@64992: val parse_consts_spec = haftmann@64992: Scan.optional (Scan.lift (Args.$$$ "terms" -- Args.colon) |-- Scan.repeat1 Args.term) [] haftmann@64992: -- Scan.optional (Scan.lift (Args.$$$ "datatypes" -- Args.colon) |-- Scan.repeat1 Args.typ) []; haftmann@64992: haftmann@64992: in haftmann@64992: haftmann@64993: val _ = Theory.setup haftmann@64993: (ML_Antiquotation.declaration @{binding code} haftmann@64993: Args.term (K ml_code_antiq) haftmann@64993: #> ML_Antiquotation.declaration @{binding computation} haftmann@64993: (Args.typ -- parse_consts_spec) (K ml_computation_antiq) haftmann@64993: #> ML_Antiquotation.declaration @{binding computation_conv} haftmann@64993: (Args.typ -- parse_consts_spec) (K ml_computation_conv_antiq) haftmann@64993: #> ML_Antiquotation.declaration @{binding computation_check} haftmann@64993: parse_consts_spec (K ml_computation_check_antiq)); haftmann@64989: haftmann@64992: end; haftmann@64992: 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*)