# HG changeset patch # User haftmann # Date 1488266292 -3600 # Node ID dc746d43f40ed1788583d96e794988b06d27fb7a # Parent 1803a9787eca4dba17aed052a7c00f1c5dbe7be7 stripped unused / obsolete material diff -r 1803a9787eca -r dc746d43f40e src/HOL/Tools/code_evaluation.ML --- 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 **) diff -r 1803a9787eca -r dc746d43f40e src/HOL/ex/Code_Timing.thy --- 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; \ @@ -52,12 +50,4 @@ nbe @{context} @{cterm "primes_upto 600"} \ -ML_val \ - eval @{context} @{cterm "primes_upto 800"} -\ - -ML_val \ - eval @{context} @{cterm "primes_upto 1000"} -\ - end diff -r 1803a9787eca -r dc746d43f40e src/Tools/Code/code_runtime.ML --- 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*)