--- a/src/HOL/Code_Evaluation.thy Thu Sep 16 17:42:49 2010 +0200
+++ b/src/HOL/Code_Evaluation.thy Thu Sep 16 17:51:16 2010 +0200
@@ -315,8 +315,8 @@
fun tracing s x = (Output.tracing s; x);
-fun eval_term thy t = Code_Runtime.value NONE (Evaluation.get, put_term, "Code_Evaluation.put_term")
- I thy (HOLogic.mk_term_of (fastype_of t) t) [];
+fun eval_term thy t = Code_Runtime.dynamic_value_strict (Evaluation.get, put_term, "Code_Evaluation.put_term")
+ thy NONE I (HOLogic.mk_term_of (fastype_of t) t) [];
end
*}
--- a/src/HOL/HOL.thy Thu Sep 16 17:42:49 2010 +0200
+++ b/src/HOL/HOL.thy Thu Sep 16 17:51:16 2010 +0200
@@ -1958,42 +1958,17 @@
subsubsection {* Evaluation and normalization by evaluation *}
-text {* Avoid some named infixes in evaluation environment *}
-
-code_reserved Eval oo ooo oooo upto downto orf andf
-
setup {*
Value.add_evaluator ("SML", Codegen.eval_term o ProofContext.theory_of)
*}
ML {*
-structure Eval_Method = Proof_Data(
- type T = unit -> bool
- fun init thy () = error "Eval_Method"
-)
-*}
-
-oracle eval_oracle = {* fn ct =>
- let
- val thy = Thm.theory_of_cterm ct;
- val t = Thm.term_of ct;
- val dummy = @{cprop True};
- in case try HOLogic.dest_Trueprop t
- of SOME t' => if Code_Runtime.value NONE
- (Eval_Method.get, Eval_Method.put, "Eval_Method.put") (K I) thy t' []
- then Thm.capply (Thm.capply @{cterm "op \<equiv> \<Colon> prop \<Rightarrow> prop \<Rightarrow> prop"} ct) dummy
- else dummy
- | NONE => dummy
- end
-*}
-
-ML {*
fun gen_eval_method conv ctxt = SIMPLE_METHOD'
(CONVERSION (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt)
THEN' rtac TrueI)
*}
-method_setup eval = {* Scan.succeed (gen_eval_method eval_oracle) *}
+method_setup eval = {* Scan.succeed (gen_eval_method Code_Runtime.dynamic_holds_conv) *}
"solve goal by evaluation"
method_setup evaluation = {* Scan.succeed (gen_eval_method Codegen.evaluation_conv) *}
--- a/src/HOL/Library/Eval_Witness.thy Thu Sep 16 17:42:49 2010 +0200
+++ b/src/HOL/Library/Eval_Witness.thy Thu Sep 16 17:51:16 2010 +0200
@@ -44,6 +44,13 @@
instance bool :: ml_equiv ..
instance list :: (ml_equiv) ml_equiv ..
+ML {*
+structure Eval_Method = Proof_Data (
+ type T = unit -> bool
+ fun init _ () = error "Eval_Method"
+)
+*}
+
oracle eval_witness_oracle = {* fn (cgoal, ws) =>
let
val thy = Thm.theory_of_cterm cgoal;
@@ -59,7 +66,7 @@
| dest_exs _ _ = sys_error "dest_exs";
val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal);
in
- if Code_Runtime.value NONE (Eval_Method.get, Eval_Method.put, "Eval_Method.put") (K I) thy t ws
+ if Code_Runtime.dynamic_value_strict (Eval_Method.get, Eval_Method.put, "Eval_Method.put") thy NONE (K I) t ws
then Thm.cterm_of thy goal
else @{cprop True} (*dummy*)
end
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Sep 16 17:42:49 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Sep 16 17:51:16 2010 +0200
@@ -3278,16 +3278,16 @@
val [nrandom, size, depth] = arguments
in
rpair NONE (fst (DSequence.yieldn k
- (Code_Runtime.value NONE (Dseq_Random_Result.get, put_dseq_random_result, "Predicate_Compile_Core.put_dseq_random_result")
- (fn proc => fn g => fn nrandom => fn size => fn s => g nrandom size s |>> DSequence.map proc)
- thy t' [] nrandom size
+ (Code_Runtime.dynamic_value_strict (Dseq_Random_Result.get, put_dseq_random_result, "Predicate_Compile_Core.put_dseq_random_result")
+ thy NONE (fn proc => fn g => fn nrandom => fn size => fn s => g nrandom size s |>> DSequence.map proc)
+ t' [] nrandom size
|> Random_Engine.run)
depth true))
end
| DSeq =>
rpair NONE (fst (DSequence.yieldn k
- (Code_Runtime.value NONE (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Core.put_dseq_result")
- DSequence.map thy t' []) (the_single arguments) true))
+ (Code_Runtime.dynamic_value_strict (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Core.put_dseq_result")
+ thy NONE DSequence.map t' []) (the_single arguments) true))
| New_Pos_Random_DSeq =>
let
val [nrandom, size, depth] = arguments
@@ -3296,23 +3296,25 @@
if stats then
apsnd (SOME o accumulate) (split_list
(fst (Lazy_Sequence.yieldn k
- (Code_Runtime.value NONE
+ (Code_Runtime.dynamic_value_strict
(Lseq_Random_Stats_Result.get, put_lseq_random_stats_result, "Predicate_Compile_Core.put_lseq_random_stats_result")
+ thy NONE
(fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
|> Lazy_Sequence.mapa (apfst proc))
- thy t' [] nrandom size seed depth))))
+ t' [] nrandom size seed depth))))
else rpair NONE
(fst (Lazy_Sequence.yieldn k
- (Code_Runtime.value NONE
+ (Code_Runtime.dynamic_value_strict
(Lseq_Random_Result.get, put_lseq_random_result, "Predicate_Compile_Core.put_lseq_random_result")
+ thy NONE
(fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
|> Lazy_Sequence.mapa proc)
- thy t' [] nrandom size seed depth)))
+ t' [] nrandom size seed depth)))
end
| _ =>
rpair NONE (fst (Predicate.yieldn k
- (Code_Runtime.value NONE (Pred_Result.get, put_pred_result, "Predicate_Compile_Core.put_pred_result")
- Predicate.map thy t' [])))
+ (Code_Runtime.dynamic_value_strict (Pred_Result.get, put_pred_result, "Predicate_Compile_Core.put_pred_result")
+ thy NONE Predicate.map t' [])))
in ((T, ts), statistics) end;
fun values ctxt param_user_modes ((raw_expected, stats), comp_options) k t_compr =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Thu Sep 16 17:42:49 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Thu Sep 16 17:51:16 2010 +0200
@@ -272,9 +272,10 @@
Pos_Random_DSeq =>
let
val compiled_term =
- Code_Runtime.value (SOME target) (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Quickcheck.put_dseq_result")
+ Code_Runtime.dynamic_value_strict (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Quickcheck.put_dseq_result")
+ thy4 (SOME target)
(fn proc => fn g => fn n => fn size => fn s => g n size s |>> (DSequence.map o map) proc)
- thy4 qc_term []
+ qc_term []
in
(fn size => fn nrandom => fn depth =>
Option.map fst (DSequence.yield
@@ -283,11 +284,12 @@
| New_Pos_Random_DSeq =>
let
val compiled_term =
- Code_Runtime.value (SOME target)
+ Code_Runtime.dynamic_value_strict
(Lseq_Result.get, put_lseq_result, "Predicate_Compile_Quickcheck.put_lseq_result")
+ thy4 (SOME target)
(fn proc => fn g => fn nrandom => fn size => fn s => fn depth =>
g nrandom size s depth |> (Lazy_Sequence.mapa o map) proc)
- thy4 qc_term []
+ qc_term []
in
fn size => fn nrandom => fn depth => Option.map fst (Lazy_Sequence.yield
(
@@ -297,11 +299,11 @@
end
| Depth_Limited_Random =>
let
- val compiled_term = Code_Runtime.value (SOME target)
+ val compiled_term = Code_Runtime.dynamic_value_strict
(Pred_Result.get, put_pred_result, "Predicate_Compile_Quickcheck.put_pred_result")
- (fn proc => fn g => fn depth => fn nrandom => fn size => fn seed =>
+ thy4 (SOME target) (fn proc => fn g => fn depth => fn nrandom => fn size => fn seed =>
g depth nrandom size seed |> (Predicate.map o map) proc)
- thy4 qc_term []
+ qc_term []
in
fn size => fn nrandom => fn depth => Option.map fst (Predicate.yield
(compiled_term depth nrandom size (Random_Engine.run (fn s => (s, s)))))
--- a/src/HOL/Tools/quickcheck_generators.ML Thu Sep 16 17:42:49 2010 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML Thu Sep 16 17:51:16 2010 +0200
@@ -392,16 +392,16 @@
in if Quickcheck.report ctxt then
let
val t' = mk_reporting_generator_expr thy t Ts;
- val compile = Code_Runtime.value (SOME target)
+ val compile = Code_Runtime.dynamic_value_strict
(Counterexample_Report.get, put_counterexample_report, "Quickcheck_Generators.put_counterexample_report")
- (fn proc => fn g => fn s => g s #>> (apfst o Option.map o map) proc) thy t' [];
+ thy (SOME target) (fn proc => fn g => fn s => g s #>> (apfst o Option.map o map) proc) t' [];
in compile #> Random_Engine.run end
else
let
val t' = mk_generator_expr thy t Ts;
- val compile = Code_Runtime.value (SOME target)
+ val compile = Code_Runtime.dynamic_value_strict
(Counterexample.get, put_counterexample, "Quickcheck_Generators.put_counterexample")
- (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) thy t' [];
+ thy (SOME target) (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) t' [];
val dummy_report = ([], false)
in compile #> Random_Engine.run #> rpair dummy_report end
end;
--- a/src/Pure/General/exn.ML Thu Sep 16 17:42:49 2010 +0200
+++ b/src/Pure/General/exn.ML Thu Sep 16 17:51:16 2010 +0200
@@ -11,6 +11,7 @@
val get_exn: 'a result -> exn option
val capture: ('a -> 'b) -> 'a -> 'b result
val release: 'a result -> 'a
+ val map_result: ('a -> 'a) -> 'a result -> 'a result
exception Interrupt
val interrupt: unit -> 'a
val is_interrupt: exn -> bool
@@ -43,6 +44,9 @@
fun release (Result y) = y
| release (Exn e) = reraise e;
+fun map_result f (Result x) = Result (f x)
+ | map_result f e = e;
+
(* interrupts *)
--- a/src/Tools/Code/code_preproc.ML Thu Sep 16 17:42:49 2010 +0200
+++ b/src/Tools/Code/code_preproc.ML Thu Sep 16 17:51:16 2010 +0200
@@ -29,7 +29,9 @@
val dynamic_eval_value: theory -> ((term -> term) -> 'a -> 'a)
-> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a
val static_eval_conv: theory -> string list
- -> (code_algebra -> code_graph -> (string * sort) list -> term -> conv) -> conv
+ -> (code_algebra -> code_graph -> theory -> (string * sort) list -> term -> conv) -> conv
+ val static_eval_value: theory -> ((term -> term) -> 'a -> 'a) -> string list
+ -> (code_algebra -> code_graph -> theory -> (string * sort) list -> term -> 'a) -> term -> 'a
val setup: theory -> theory
end
@@ -138,6 +140,8 @@
fun preprocess_conv thy ct =
let
+ val ctxt = ProofContext.init_global thy;
+ val _ = (Sign.no_frees ctxt o map_types (K dummyT) o Sign.no_vars ctxt) (Thm.term_of ct);
val pre = (Simplifier.global_context thy o #pre o the_thmproc) thy;
in
ct
@@ -145,6 +149,8 @@
|> trans_conv_rule (AxClass.unoverload_conv thy)
end;
+fun preprocess_term thy = term_of_conv thy (preprocess_conv thy);
+
fun postprocess_conv thy ct =
let
val post = (Simplifier.global_context thy o #post o the_thmproc) thy;
@@ -427,43 +433,56 @@
fun dest_cterm ct = let val t = Thm.term_of ct in (Term.add_tfrees t [], t) end;
-fun dynamic_eval thy cterm_of conclude_evaluation evaluator proto_ct =
+fun dynamic_eval_conv thy conv ct =
let
- val ctxt = Syntax.init_pretty_global thy;
- val ct = cterm_of proto_ct;
- val _ = (Sign.no_frees ctxt o map_types (K dummyT) o Sign.no_vars ctxt) (Thm.term_of ct);
- val thm = preprocess_conv thy ct;
- val ct' = Thm.rhs_of thm;
+ val thm1 = preprocess_conv thy ct;
+ val ct' = Thm.rhs_of thm1;
val (vs', t') = dest_cterm ct';
val consts = fold_aterms
(fn Const (c, _) => insert (op =) c | _ => I) t' [];
val (algebra', eqngr') = obtain false thy consts [t'];
- in conclude_evaluation (evaluator algebra' eqngr' vs' t' ct') thm end;
+ val thm2 = conv algebra' eqngr' vs' t' ct';
+ val thm3 = postprocess_conv thy (Thm.rhs_of thm2);
+ in
+ Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
+ error ("could not construct evaluation proof:\n"
+ ^ (cat_lines o map (Display.string_of_thm_global thy)) [thm1, thm2, thm3])
+ end;
-fun dynamic_eval_conv thy =
+fun dynamic_eval_value thy postproc evaluator t =
let
- fun conclude_evaluation thm2 thm1 =
- let
- val thm3 = postprocess_conv thy (Thm.rhs_of thm2);
- in
- Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
- error ("could not construct evaluation proof:\n"
- ^ (cat_lines o map (Display.string_of_thm_global thy)) [thm1, thm2, thm3])
- end;
- in dynamic_eval thy I conclude_evaluation end;
-
-fun dynamic_eval_value thy postproc evaluator = dynamic_eval thy (Thm.cterm_of thy)
- (K o postproc (postprocess_term thy)) (K oooo evaluator);
+ val t' = preprocess_term thy t;
+ val vs' = Term.add_tfrees t' [];
+ val consts = fold_aterms
+ (fn Const (c, _) => insert (op =) c | _ => I) t' [];
+ val (algebra', eqngr') = obtain false thy consts [t'];
+ val result = evaluator algebra' eqngr' vs' t';
+ in
+ evaluator algebra' eqngr' vs' t'
+ |> postproc (postprocess_term thy)
+ end;
fun static_eval_conv thy consts conv =
let
val (algebra, eqngr) = obtain true thy consts [];
+ val conv' = conv algebra eqngr;
in
Conv.tap_thy (fn thy => (preprocess_conv thy)
- then_conv (fn ct => uncurry (conv algebra eqngr) (dest_cterm ct) ct)
+ then_conv (fn ct => uncurry (conv' thy) (dest_cterm ct) ct)
then_conv (postprocess_conv thy))
end;
+fun static_eval_value thy postproc consts evaluator =
+ let
+ val (algebra, eqngr) = obtain true thy consts [];
+ val evaluator' = evaluator algebra eqngr;
+ in fn t =>
+ t
+ |> preprocess_term thy
+ |> (fn t => evaluator' thy (Term.add_tfrees t []) t)
+ |> postproc (postprocess_term thy)
+ end;
+
(** setup **)
--- a/src/Tools/Code/code_runtime.ML Thu Sep 16 17:42:49 2010 +0200
+++ b/src/Tools/Code/code_runtime.ML Thu Sep 16 17:51:16 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*)
--- a/src/Tools/Code/code_simp.ML Thu Sep 16 17:42:49 2010 +0200
+++ b/src/Tools/Code/code_simp.ML Thu Sep 16 17:51:16 2010 +0200
@@ -84,7 +84,8 @@
(* evaluation with freezed code context *)
fun static_eval_conv thy some_ss consts = no_frees_conv
- (Code_Thingol.static_eval_conv_simple thy consts (rewrite_modulo thy some_ss));
+ (Code_Thingol.static_eval_conv_simple thy consts
+ (fn program => fn thy => rewrite_modulo thy some_ss program));
fun static_eval_tac thy some_ss consts = CONVERSION (static_eval_conv thy some_ss consts)
THEN' conclude_tac thy some_ss;
--- a/src/Tools/Code/code_thingol.ML Thu Sep 16 17:42:49 2010 +0200
+++ b/src/Tools/Code/code_thingol.ML Thu Sep 16 17:51:16 2010 +0200
@@ -99,10 +99,13 @@
-> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
-> term -> 'a
val static_eval_conv: theory -> string list
- -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> conv)
+ -> (naming -> program -> theory -> ((string * sort) list * typscheme) * iterm -> string list -> conv)
-> conv
val static_eval_conv_simple: theory -> string list
- -> (program -> conv) -> conv
+ -> (program -> theory -> conv) -> conv
+ val static_eval_value: theory -> ((term -> term) -> 'a -> 'a) -> string list
+ -> (naming -> program -> theory -> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
+ -> term -> 'a
end;
structure Code_Thingol: CODE_THINGOL =
@@ -884,25 +887,34 @@
#> term_value
end;
-fun base_evaluator thy evaluator algebra eqngr vs t =
+fun base_evaluator evaluator algebra eqngr thy vs t =
let
val (((naming, program), (((vs', ty'), t'), deps)), _) =
invoke_generation false thy (algebra, eqngr) ensure_value t;
val vs'' = map (fn (v, _) => (v, (the o AList.lookup (op =) vs o prefix "'") v)) vs';
- in evaluator naming program ((vs'', (vs', ty')), t') deps end;
+ in evaluator naming program thy ((vs'', (vs', ty')), t') deps end;
+
+fun dynamic_evaluator thy evaluator algebra eqngr vs t =
+ base_evaluator (fn naming => fn program => fn _ => evaluator naming program) algebra eqngr thy vs t;
-fun dynamic_eval_conv thy = Code_Preproc.dynamic_eval_conv thy o base_evaluator thy;
-fun dynamic_eval_value thy postproc = Code_Preproc.dynamic_eval_value thy postproc o base_evaluator thy;
+fun dynamic_eval_conv thy evaluator =
+ Code_Preproc.dynamic_eval_conv thy (dynamic_evaluator thy evaluator);
+
+fun dynamic_eval_value thy postproc evaluator =
+ Code_Preproc.dynamic_eval_value thy postproc (dynamic_evaluator thy evaluator);
fun static_eval_conv thy consts conv =
- Code_Preproc.static_eval_conv thy consts (base_evaluator thy conv); (*FIXME avoid re-generation*)
+ Code_Preproc.static_eval_conv thy consts (base_evaluator conv); (*FIXME avoid re-generation*)
fun static_eval_conv_simple thy consts conv =
- Code_Preproc.static_eval_conv thy consts (fn algebra => fn eqngr => fn _ => fn _ => fn ct =>
+ Code_Preproc.static_eval_conv thy consts (fn algebra => fn eqngr => fn thy => fn _ => fn _ => fn ct =>
conv ((NONE, (empty_naming, Graph.empty)) (*FIXME provide abstraction for this kind of invocation*)
|> fold_map (ensure_const thy algebra eqngr false) consts
- |> (snd o snd o snd)) ct);
+ |> (snd o snd o snd)) thy ct);
+fun static_eval_value thy postproc consts conv =
+ Code_Preproc.static_eval_value thy postproc consts (base_evaluator conv); (*FIXME avoid re-generation*)
+
(** diagnostic commands **)
--- a/src/Tools/Code_Generator.thy Thu Sep 16 17:42:49 2010 +0200
+++ b/src/Tools/Code_Generator.thy Thu Sep 16 17:51:16 2010 +0200
@@ -21,8 +21,8 @@
"~~/src/Tools/Code/code_ml.ML"
"~~/src/Tools/Code/code_haskell.ML"
"~~/src/Tools/Code/code_scala.ML"
- "~~/src/Tools/Code/code_runtime.ML"
"~~/src/Tools/nbe.ML"
+ ("~~/src/Tools/Code/code_runtime.ML")
begin
setup {*
@@ -32,7 +32,6 @@
#> Code_ML.setup
#> Code_Haskell.setup
#> Code_Scala.setup
- #> Code_Runtime.setup
#> Nbe.setup
#> Quickcheck.setup
*}
@@ -64,6 +63,8 @@
by rule (rule holds)+
qed
+use "~~/src/Tools/Code/code_runtime.ML"
+
hide_const (open) holds
end
--- a/src/Tools/nbe.ML Thu Sep 16 17:42:49 2010 +0200
+++ b/src/Tools/nbe.ML Thu Sep 16 17:51:16 2010 +0200
@@ -609,7 +609,8 @@
fun static_eval_conv thy consts = Code_Simp.no_frees_conv
(lift_triv_classes_conv thy (Code_Thingol.static_eval_conv thy consts
- (K (fn program => oracle thy program (compile true thy program)))));
+ (K (fn program => let val nbe_program = compile true thy program
+ in fn thy => oracle thy program nbe_program end))));
(** setup **)