--- a/src/Tools/Code/code_runtime.ML Thu May 26 09:05:00 2016 +0200
+++ b/src/Tools/Code/code_runtime.ML Thu May 26 15:27:50 2016 +0200
@@ -200,7 +200,7 @@
o reject_vars ctxt;
fun static_holds_conv (ctxt_consts as { ctxt, ... }) =
- Code_Thingol.static_conv ctxt_consts (fn { program, deps } => fn ctxt' => fn vs_t =>
+ Code_Thingol.static_conv_thingol ctxt_consts (fn { program, deps } => fn ctxt' => fn vs_t =>
K (check_holds_oracle ctxt' (obtain_evaluator ctxt NONE program (map Constant deps)) vs_t o reject_vars ctxt'));
end; (*local*)
--- a/src/Tools/Code/code_simp.ML Thu May 26 09:05:00 2016 +0200
+++ b/src/Tools/Code/code_simp.ML Thu May 26 15:27:50 2016 +0200
@@ -94,7 +94,7 @@
(* evaluation with static code context *)
fun static_conv { ctxt, simpset, consts } =
- Code_Thingol.static_conv_simple { ctxt = ctxt, consts = consts }
+ Code_Thingol.static_conv_isa { ctxt = ctxt, consts = consts }
(K oo rewrite_modulo ctxt simpset);
fun static_tac { ctxt, simpset, consts } =
--- a/src/Tools/Code/code_thingol.ML Thu May 26 09:05:00 2016 +0200
+++ b/src/Tools/Code/code_thingol.ML Thu May 26 15:27:50 2016 +0200
@@ -91,11 +91,11 @@
val dynamic_value: Proof.context -> ((term -> term) -> 'a -> 'a) -> (program
-> term -> typscheme * iterm -> Code_Symbol.T list -> 'a)
-> term -> 'a
- val static_conv: { ctxt: Proof.context, consts: string list }
+ val static_conv_thingol: { ctxt: Proof.context, consts: string list }
-> ({ program: program, deps: string list }
-> Proof.context -> typscheme * iterm -> Code_Symbol.T list -> conv)
-> Proof.context -> conv
- val static_conv_simple: { ctxt: Proof.context, consts: string list }
+ val static_conv_isa: { ctxt: Proof.context, consts: string list }
-> (program -> Proof.context -> term -> conv)
-> Proof.context -> conv
val static_value: { ctxt: Proof.context, lift_postproc: ((term -> term) -> 'a -> 'a), consts: string list }
@@ -857,7 +857,7 @@
ensure_value ctxt algebra eqngr t ([], program);
in subevaluator ctxt t (vs_ty', t') deps end;
-fun static_evaluator ctxt evaluator consts { algebra, eqngr } =
+fun static_evaluator_thingol ctxt evaluator consts { algebra, eqngr } =
let
fun generate_consts ctxt algebra eqngr =
fold_map (ensure_const ctxt algebra eqngr false);
@@ -866,7 +866,7 @@
val subevaluator = evaluator { program = program, deps = deps };
in fn ctxt' => static_subevaluator ctxt' subevaluator algebra eqngr program end;
-fun static_evaluator_simple ctxt evaluator consts { algebra, eqngr } =
+fun static_evaluator_isa ctxt evaluator consts { algebra, eqngr } =
let
fun generate_consts ctxt algebra eqngr =
fold_map (ensure_const ctxt algebra eqngr false);
@@ -874,14 +874,14 @@
invoke_generation true (Proof_Context.theory_of ctxt) (algebra, eqngr) generate_consts consts;
in evaluator (program: program) end;
-fun static_conv (ctxt_consts as { ctxt, consts }) conv =
- Code_Preproc.static_conv ctxt_consts (static_evaluator ctxt (K oo conv) consts);
+fun static_conv_thingol (ctxt_consts as { ctxt, consts }) conv =
+ Code_Preproc.static_conv ctxt_consts (static_evaluator_thingol ctxt (K oo conv) consts);
-fun static_conv_simple (ctxt_consts as { ctxt, consts }) conv =
- Code_Preproc.static_conv ctxt_consts (static_evaluator_simple ctxt conv consts);
+fun static_conv_isa (ctxt_consts as { ctxt, consts }) conv =
+ Code_Preproc.static_conv ctxt_consts (static_evaluator_isa ctxt conv consts);
fun static_value (ctxt_postproc_consts as { ctxt, consts, ... }) evaluator =
- Code_Preproc.static_value ctxt_postproc_consts (static_evaluator ctxt evaluator consts);
+ Code_Preproc.static_value ctxt_postproc_consts (static_evaluator_thingol ctxt evaluator consts);
(** constant expressions **)
--- a/src/Tools/nbe.ML Thu May 26 09:05:00 2016 +0200
+++ b/src/Tools/nbe.ML Thu May 26 15:27:50 2016 +0200
@@ -604,7 +604,7 @@
fun static_conv (ctxt_consts as { ctxt, ... }) =
let
- val evaluator = Code_Thingol.static_conv ctxt_consts
+ val evaluator = Code_Thingol.static_conv_thingol ctxt_consts
(fn { program, ... } => oracle (compile true ctxt program));
in fn ctxt' => lift_triv_classes_conv ctxt' (evaluator ctxt') end;