--- 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*)