# HG changeset patch # User haftmann # Date 1284648694 -7200 # Node ID 33638f4883ac72be3f4885ae2be4af8162cf91fe # Parent 1cf49add5b400b811eb3a50575aed24154b58b9f dynamic and static value computation; built-in evaluation of propositions diff -r 1cf49add5b40 -r 33638f4883ac src/Tools/Code/code_runtime.ML --- a/src/Tools/Code/code_runtime.ML Thu Sep 16 16:51:33 2010 +0200 +++ b/src/Tools/Code/code_runtime.ML Thu Sep 16 16:51:34 2010 +0200 @@ -7,41 +7,139 @@ signature CODE_RUNTIME = sig val target: string - val value: string option - -> (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string - -> ((term -> term) -> 'a -> 'a) -> theory -> term -> string list -> 'a + type 'a cookie = (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string + val dynamic_value: 'a cookie -> theory -> string option + -> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a option + val dynamic_value_strict: 'a cookie -> theory -> string option + -> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a + val dynamic_value_exn: 'a cookie -> theory -> string option + -> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a Exn.result + val static_value: 'a cookie -> theory -> string option + -> ((term -> term) -> 'a -> 'a) -> string list -> term -> 'a option + val static_value_strict: 'a cookie -> theory -> string option + -> ((term -> term) -> 'a -> 'a) -> string list -> term -> 'a + val static_value_exn: 'a cookie -> theory -> string option + -> ((term -> term) -> 'a -> 'a) -> string list -> term -> 'a Exn.result + val dynamic_holds_conv: conv + val static_holds_conv: theory -> string list -> conv val code_reflect: (string * string list) list -> string list -> string -> string option -> theory -> theory - val setup: theory -> theory + datatype truth = Holds + val put_truth: (unit -> truth) -> Proof.context -> Proof.context end; structure Code_Runtime : CODE_RUNTIME = struct +open Basic_Code_Thingol; + (** evaluation **) +(* technical prerequisites *) + +val this = "Code_Runtime"; +val s_truth = Long_Name.append this "truth"; +val s_Holds = Long_Name.append this "Holds"; + val target = "Eval"; -val truth_struct = "Code_Truth"; +datatype truth = Holds; -fun value some_target cookie postproc thy t args = +val _ = Context.>> (Context.map_theory + (Code_Target.extend_target (target, (Code_ML.target_SML, K I)) + #> Code_Target.add_tyco_syntax target @{type_name prop} (SOME (0, (K o K o K) (Code_Printer.str s_truth))) + #> Code_Target.add_const_syntax target @{const_name Code_Generator.holds} (SOME (Code_Printer.plain_const_syntax s_Holds)) + #> Code_Target.add_reserved target this + #> fold (Code_Target.add_reserved target) ["oo", "ooo", "oooo", "upto", "downto", "orf", "andf"])); (*avoid further pervasive infix names*) + + +(* evaluation into target language values *) + +type 'a cookie = (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string; + +fun base_evaluator cookie thy some_target naming program ((_, (vs, ty)), t) deps args = let val ctxt = ProofContext.init_global thy; - fun evaluator naming program ((_, (_, ty)), t) deps = - let - val _ = if Code_Thingol.contains_dictvar t then - error "Term to be evaluated contains free dictionaries" else (); - val value_name = "Value.VALUE.value" - val program' = program - |> Graph.new_node (value_name, - Code_Thingol.Fun (Term.dummy_patternN, ((([], ty), [(([], t), (NONE, true))]), NONE))) - |> fold (curry Graph.add_edge value_name) deps; - val (program_code, [SOME value_name']) = Code_Target.produce_code_for thy - (the_default target some_target) NONE "Code" [] naming program' [value_name]; - val value_code = space_implode " " - (value_name' :: map (enclose "(" ")") args); - in ML_Context.value ctxt cookie (program_code, value_code) end; - in Code_Thingol.dynamic_eval_value thy postproc evaluator t end; + val _ = if Code_Thingol.contains_dictvar t then + error "Term to be evaluated contains free dictionaries" else (); + val v' = Name.variant (map fst vs) "a"; + val vs' = (v', []) :: vs + val ty' = Code_Thingol.fun_tyco `%% [ITyVar v', ty]; + val value_name = "Value.value.value" + val program' = program + |> Graph.new_node (value_name, + Code_Thingol.Fun (Term.dummy_patternN, (((vs', ty'), [(([IVar NONE], t), (NONE, true))]), NONE))) + |> fold (curry Graph.add_edge value_name) deps; + val (program_code, [SOME value_name']) = Code_Target.produce_code_for thy + (the_default target some_target) NONE "Code" [] naming program' [value_name]; + val value_code = space_implode " " + (value_name' :: "()" :: map (enclose "(" ")") args); + in Exn.capture (ML_Context.value ctxt cookie) (program_code, value_code) end; + +fun partiality_as_none e = SOME (Exn.release e) + handle General.Match => NONE + | General.Bind => NONE + | General.Fail _ => NONE; + +fun dynamic_value_exn cookie thy some_target postproc t args = + let + fun evaluator naming program expr deps = + base_evaluator cookie thy some_target naming program expr deps args; + in Code_Thingol.dynamic_eval_value thy (Exn.map_result o postproc) evaluator t end; + +fun dynamic_value_strict cookie thy some_target postproc t args = + Exn.release (dynamic_value_exn cookie thy some_target postproc t args); + +fun dynamic_value cookie thy some_target postproc t args = + partiality_as_none (dynamic_value_exn cookie thy some_target postproc t args); + +fun static_value_exn cookie thy some_target postproc consts = + let + fun evaluator naming program thy expr deps = + base_evaluator cookie thy some_target naming program expr deps []; + in Code_Thingol.static_eval_value thy (Exn.map_result o postproc) consts evaluator end; + +fun static_value_strict cookie thy some_target postproc consts t = + Exn.release (static_value_exn cookie thy some_target postproc consts t); + +fun static_value cookie thy some_target postproc consts t = + partiality_as_none (static_value_exn cookie thy some_target postproc consts t); + + +(* evaluation for truth or nothing *) + +structure Truth_Result = Proof_Data ( + type T = unit -> truth + fun init _ () = error "Truth_Result" +); +val put_truth = Truth_Result.put; +val truth_cookie = (Truth_Result.get, put_truth, Long_Name.append this "put_truth"); + +fun check_holds thy naming program expr deps ct = + let + val t = Thm.term_of ct; + val _ = if fastype_of t <> propT + then error ("Not a proposition: " ^ Syntax.string_of_term_global thy t) + else (); + val iff = Thm.cterm_of thy (Term.Const ("==", propT --> propT --> propT)); + val result = case partiality_as_none (base_evaluator truth_cookie thy NONE naming program expr deps []) + of SOME Holds => true + | _ => false; + in + Thm.mk_binop iff ct (if result then @{cprop "PROP Code_Generator.holds"} else ct) + end; + +val (_, raw_check_holds_oracle) = Context.>>> (Context.map_theory_result + (Thm.add_oracle (Binding.name "holds_by_evaluation", + fn (thy, naming, program, expr, deps, ct) => check_holds thy naming program expr deps ct))); + +fun check_holds_oracle thy naming program expr deps ct = + raw_check_holds_oracle (thy, naming, program, expr, deps, ct); + +val dynamic_holds_conv = Conv.tap_thy (fn thy => Code_Thingol.dynamic_eval_conv thy (check_holds_oracle thy)); + +fun static_holds_conv thy consts = Code_Thingol.static_eval_conv thy consts + (fn naming => fn program => fn thy => check_holds_oracle thy naming program); (** instrumentalization **) @@ -221,6 +319,4 @@ end; (*local*) -val setup = Code_Target.extend_target (target, (Code_ML.target_SML, K I)); - end; (*struct*)