stripped unused / obsolete material
authorhaftmann
Tue Feb 28 08:18:12 2017 +0100 (2017-02-28)
changeset 65062dc746d43f40e
parent 65061 1803a9787eca
child 65063 862157c7e78f
child 65064 a4abec71279a
stripped unused / obsolete material
src/HOL/Tools/code_evaluation.ML
src/HOL/ex/Code_Timing.thy
src/Tools/Code/code_runtime.ML
     1.1 --- a/src/HOL/Tools/code_evaluation.ML	Mon Feb 27 20:44:25 2017 +0100
     1.2 +++ b/src/HOL/Tools/code_evaluation.ML	Tue Feb 28 08:18:12 2017 +0100
     1.3 @@ -9,15 +9,6 @@
     1.4    val dynamic_value: Proof.context -> term -> term option
     1.5    val dynamic_value_strict: Proof.context -> term -> term
     1.6    val dynamic_value_exn: Proof.context -> term -> term Exn.result
     1.7 -  val static_value: { ctxt: Proof.context, consts: string list }
     1.8 -    -> Proof.context -> term -> term option
     1.9 -  val static_value_strict: { ctxt: Proof.context, consts: string list }
    1.10 -    -> Proof.context -> term -> term
    1.11 -  val static_value_exn: { ctxt: Proof.context, consts: string list }
    1.12 -    -> Proof.context -> term -> term Exn.result
    1.13 -  val dynamic_conv: Proof.context -> conv
    1.14 -  val static_conv: { ctxt: Proof.context, consts: string list }
    1.15 -    -> Proof.context -> conv
    1.16    val put_term: (unit -> term) -> Proof.context -> Proof.context
    1.17    val tracing: string -> 'a -> 'a
    1.18  end;
    1.19 @@ -190,42 +181,6 @@
    1.20  val dynamic_value_strict = gen_dynamic_value Code_Runtime.dynamic_value_strict;
    1.21  val dynamic_value_exn = gen_dynamic_value Code_Runtime.dynamic_value_exn;
    1.22  
    1.23 -fun gen_static_value computation { ctxt, consts } =
    1.24 -  let
    1.25 -    val computation' = computation cookie
    1.26 -      { ctxt = ctxt, target = NONE, lift_postproc = I, consts = consts }
    1.27 -  in fn ctxt' => computation' ctxt' o mk_term_of end;
    1.28 -
    1.29 -val static_value = gen_static_value Code_Runtime.static_value;
    1.30 -val static_value_strict = gen_static_value Code_Runtime.static_value_strict;
    1.31 -val static_value_exn = gen_static_value Code_Runtime.static_value_exn;
    1.32 -
    1.33 -fun certify_eval ctxt value conv ct =
    1.34 -  let
    1.35 -    val t = Thm.term_of ct;
    1.36 -    val T = fastype_of t;
    1.37 -    val mk_eq =
    1.38 -      Thm.mk_binop (Thm.cterm_of ctxt (Const (@{const_name Pure.eq}, T --> T --> propT)));
    1.39 -  in case value ctxt t
    1.40 -   of NONE => Thm.reflexive ct
    1.41 -    | SOME t' => conv ctxt (mk_eq ct (Thm.cterm_of ctxt t')) RS @{thm eq_eq_TrueD}
    1.42 -        handle THM _ =>
    1.43 -          error ("Failed to certify evaluation result of " ^ Syntax.string_of_term ctxt t)
    1.44 -  end;
    1.45 -
    1.46 -fun dynamic_conv ctxt = certify_eval ctxt dynamic_value
    1.47 -  Code_Runtime.dynamic_holds_conv;
    1.48 -
    1.49 -fun static_conv { ctxt, consts }  =
    1.50 -  let
    1.51 -    val value = static_value { ctxt = ctxt, consts = consts };
    1.52 -    val holds = Code_Runtime.static_holds_conv { ctxt = ctxt,
    1.53 -      consts = insert (op =) @{const_name Pure.eq} consts
    1.54 -        (*assumes particular code equation for Pure.eq*) };
    1.55 -  in
    1.56 -    fn ctxt' => certify_eval ctxt' value holds
    1.57 -  end;
    1.58 -
    1.59  
    1.60  (** diagnostic **)
    1.61  
     2.1 --- a/src/HOL/ex/Code_Timing.thy	Mon Feb 27 20:44:25 2017 +0100
     2.2 +++ b/src/HOL/ex/Code_Timing.thy	Tue Feb 28 08:18:12 2017 +0100
     2.3 @@ -27,8 +27,6 @@
     2.4      { ctxt = ctxt, consts = consts, simpset = NONE };
     2.5    val nbe = Nbe.static_conv
     2.6      { ctxt = ctxt, consts = consts };
     2.7 -  val eval = Code_Evaluation.static_conv
     2.8 -    { ctxt = ctxt, consts = consts };
     2.9  end;
    2.10  \<close>
    2.11  
    2.12 @@ -52,12 +50,4 @@
    2.13    nbe @{context} @{cterm "primes_upto 600"}
    2.14  \<close>
    2.15  
    2.16 -ML_val \<open>
    2.17 -  eval @{context} @{cterm "primes_upto 800"}
    2.18 -\<close>
    2.19 -
    2.20 -ML_val \<open>
    2.21 -  eval @{context} @{cterm "primes_upto 1000"}
    2.22 -\<close>
    2.23 -
    2.24  end
     3.1 --- a/src/Tools/Code/code_runtime.ML	Mon Feb 27 20:44:25 2017 +0100
     3.2 +++ b/src/Tools/Code/code_runtime.ML	Tue Feb 28 08:18:12 2017 +0100
     3.3 @@ -17,17 +17,7 @@
     3.4      -> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a
     3.5    val dynamic_value_exn: 'a cookie -> Proof.context -> string option
     3.6      -> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a Exn.result
     3.7 -  val static_value: 'a cookie -> { ctxt: Proof.context, target: string option,
     3.8 -    lift_postproc: (term -> term) -> 'a -> 'a, consts: string list }
     3.9 -    -> Proof.context -> term -> 'a option
    3.10 -  val static_value_strict: 'a cookie -> { ctxt: Proof.context, target: string option,
    3.11 -    lift_postproc: (term -> term) -> 'a -> 'a, consts: string list }
    3.12 -    -> Proof.context -> term -> 'a
    3.13 -  val static_value_exn: 'a cookie -> { ctxt: Proof.context, target: string option,
    3.14 -    lift_postproc: (term -> term) -> 'a -> 'a, consts: string list }
    3.15 -    -> Proof.context -> term -> 'a Exn.result
    3.16    val dynamic_holds_conv: Proof.context -> conv
    3.17 -  val static_holds_conv: { ctxt: Proof.context, consts: string list } -> Proof.context -> conv
    3.18    val code_reflect: (string * string list option) list -> string list -> string
    3.19      -> string option -> theory -> theory
    3.20    datatype truth = Holds
    3.21 @@ -130,22 +120,6 @@
    3.22  fun dynamic_value cookie ctxt some_target postproc t args =
    3.23    partiality_as_none (dynamic_value_exn cookie ctxt some_target postproc t args);
    3.24  
    3.25 -fun static_value_exn cookie { ctxt, target, lift_postproc, consts } =
    3.26 -  let
    3.27 -    fun compilation' { program, deps } =
    3.28 -      let
    3.29 -        val compilation'' = run_compilation_text cookie ctxt
    3.30 -          (build_compilation_text ctxt target program (map Constant deps));
    3.31 -      in fn _ => fn _ => fn vs_ty_t => fn _ => compilation'' vs_ty_t [] end;
    3.32 -    val compilation = Code_Thingol.static_value { ctxt = ctxt,
    3.33 -      lift_postproc = Exn.map_res o lift_postproc, consts = consts }
    3.34 -      compilation';
    3.35 -  in fn ctxt' => compilation ctxt' o reject_vars ctxt' end;
    3.36 -
    3.37 -fun static_value_strict cookie x = Exn.release oo static_value_exn cookie x;
    3.38 -
    3.39 -fun static_value cookie x = partiality_as_none oo static_value_exn cookie x;
    3.40 -
    3.41  
    3.42  (* evaluation for truth or nothing *)
    3.43  
    3.44 @@ -190,10 +164,6 @@
    3.45      check_holds_oracle ctxt (build_compilation_text ctxt NONE program deps) vs_t)
    3.46        o reject_vars ctxt;
    3.47  
    3.48 -fun static_holds_conv (ctxt_consts as { ctxt, ... }) =
    3.49 -  Code_Thingol.static_conv_thingol ctxt_consts (fn { program, deps } => fn ctxt' => fn vs_t =>
    3.50 -    K (check_holds_oracle ctxt' (build_compilation_text ctxt NONE program (map Constant deps)) vs_t o reject_vars ctxt'));
    3.51 -
    3.52  end; (*local*)
    3.53  
    3.54