--- a/src/HOL/Tools/code_evaluation.ML Mon Feb 27 20:44:25 2017 +0100
+++ b/src/HOL/Tools/code_evaluation.ML Tue Feb 28 08:18:12 2017 +0100
@@ -9,15 +9,6 @@
val dynamic_value: Proof.context -> term -> term option
val dynamic_value_strict: Proof.context -> term -> term
val dynamic_value_exn: Proof.context -> term -> term Exn.result
- val static_value: { ctxt: Proof.context, consts: string list }
- -> Proof.context -> term -> term option
- val static_value_strict: { ctxt: Proof.context, consts: string list }
- -> Proof.context -> term -> term
- val static_value_exn: { ctxt: Proof.context, consts: string list }
- -> Proof.context -> term -> term Exn.result
- val dynamic_conv: Proof.context -> conv
- val static_conv: { ctxt: Proof.context, consts: string list }
- -> Proof.context -> conv
val put_term: (unit -> term) -> Proof.context -> Proof.context
val tracing: string -> 'a -> 'a
end;
@@ -190,42 +181,6 @@
val dynamic_value_strict = gen_dynamic_value Code_Runtime.dynamic_value_strict;
val dynamic_value_exn = gen_dynamic_value Code_Runtime.dynamic_value_exn;
-fun gen_static_value computation { ctxt, consts } =
- let
- val computation' = computation cookie
- { ctxt = ctxt, target = NONE, lift_postproc = I, consts = consts }
- in fn ctxt' => computation' ctxt' o mk_term_of end;
-
-val static_value = gen_static_value Code_Runtime.static_value;
-val static_value_strict = gen_static_value Code_Runtime.static_value_strict;
-val static_value_exn = gen_static_value Code_Runtime.static_value_exn;
-
-fun certify_eval ctxt value conv ct =
- let
- val t = Thm.term_of ct;
- val T = fastype_of t;
- val mk_eq =
- Thm.mk_binop (Thm.cterm_of ctxt (Const (@{const_name Pure.eq}, T --> T --> propT)));
- in case value ctxt t
- of NONE => Thm.reflexive ct
- | SOME t' => conv ctxt (mk_eq ct (Thm.cterm_of ctxt t')) RS @{thm eq_eq_TrueD}
- handle THM _ =>
- error ("Failed to certify evaluation result of " ^ Syntax.string_of_term ctxt t)
- end;
-
-fun dynamic_conv ctxt = certify_eval ctxt dynamic_value
- Code_Runtime.dynamic_holds_conv;
-
-fun static_conv { ctxt, consts } =
- let
- val value = static_value { ctxt = ctxt, consts = consts };
- val holds = Code_Runtime.static_holds_conv { ctxt = ctxt,
- consts = insert (op =) @{const_name Pure.eq} consts
- (*assumes particular code equation for Pure.eq*) };
- in
- fn ctxt' => certify_eval ctxt' value holds
- end;
-
(** diagnostic **)
--- a/src/HOL/ex/Code_Timing.thy Mon Feb 27 20:44:25 2017 +0100
+++ b/src/HOL/ex/Code_Timing.thy Tue Feb 28 08:18:12 2017 +0100
@@ -27,8 +27,6 @@
{ ctxt = ctxt, consts = consts, simpset = NONE };
val nbe = Nbe.static_conv
{ ctxt = ctxt, consts = consts };
- val eval = Code_Evaluation.static_conv
- { ctxt = ctxt, consts = consts };
end;
\<close>
@@ -52,12 +50,4 @@
nbe @{context} @{cterm "primes_upto 600"}
\<close>
-ML_val \<open>
- eval @{context} @{cterm "primes_upto 800"}
-\<close>
-
-ML_val \<open>
- eval @{context} @{cterm "primes_upto 1000"}
-\<close>
-
end
--- a/src/Tools/Code/code_runtime.ML Mon Feb 27 20:44:25 2017 +0100
+++ b/src/Tools/Code/code_runtime.ML Tue Feb 28 08:18:12 2017 +0100
@@ -17,17 +17,7 @@
-> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a
val dynamic_value_exn: 'a cookie -> Proof.context -> string option
-> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a Exn.result
- val static_value: 'a cookie -> { ctxt: Proof.context, target: string option,
- lift_postproc: (term -> term) -> 'a -> 'a, consts: string list }
- -> Proof.context -> term -> 'a option
- val static_value_strict: 'a cookie -> { ctxt: Proof.context, target: string option,
- lift_postproc: (term -> term) -> 'a -> 'a, consts: string list }
- -> Proof.context -> term -> 'a
- val static_value_exn: 'a cookie -> { ctxt: Proof.context, target: string option,
- lift_postproc: (term -> term) -> 'a -> 'a, consts: string list }
- -> Proof.context -> term -> 'a Exn.result
val dynamic_holds_conv: Proof.context -> conv
- val static_holds_conv: { ctxt: Proof.context, consts: string list } -> Proof.context -> conv
val code_reflect: (string * string list option) list -> string list -> string
-> string option -> theory -> theory
datatype truth = Holds
@@ -130,22 +120,6 @@
fun dynamic_value cookie ctxt some_target postproc t args =
partiality_as_none (dynamic_value_exn cookie ctxt some_target postproc t args);
-fun static_value_exn cookie { ctxt, target, lift_postproc, consts } =
- let
- fun compilation' { program, deps } =
- let
- val compilation'' = run_compilation_text cookie ctxt
- (build_compilation_text ctxt target program (map Constant deps));
- in fn _ => fn _ => fn vs_ty_t => fn _ => compilation'' vs_ty_t [] end;
- val compilation = Code_Thingol.static_value { ctxt = ctxt,
- lift_postproc = Exn.map_res o lift_postproc, consts = consts }
- compilation';
- in fn ctxt' => compilation ctxt' o reject_vars ctxt' end;
-
-fun static_value_strict cookie x = Exn.release oo static_value_exn cookie x;
-
-fun static_value cookie x = partiality_as_none oo static_value_exn cookie x;
-
(* evaluation for truth or nothing *)
@@ -190,10 +164,6 @@
check_holds_oracle ctxt (build_compilation_text ctxt NONE program deps) vs_t)
o reject_vars ctxt;
-fun static_holds_conv (ctxt_consts as { ctxt, ... }) =
- Code_Thingol.static_conv_thingol ctxt_consts (fn { program, deps } => fn ctxt' => fn vs_t =>
- K (check_holds_oracle ctxt' (build_compilation_text ctxt NONE program (map Constant deps)) vs_t o reject_vars ctxt'));
-
end; (*local*)