src/Tools/Code/code_runtime.ML
changeset 65062 dc746d43f40e
parent 65043 fd753468786f
child 67327 89be5a4f514b
     1.1 --- a/src/Tools/Code/code_runtime.ML	Mon Feb 27 20:44:25 2017 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Tue Feb 28 08:18:12 2017 +0100
     1.3 @@ -17,17 +17,7 @@
     1.4      -> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a
     1.5    val dynamic_value_exn: 'a cookie -> Proof.context -> string option
     1.6      -> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a Exn.result
     1.7 -  val static_value: 'a cookie -> { ctxt: Proof.context, target: string option,
     1.8 -    lift_postproc: (term -> term) -> 'a -> 'a, consts: string list }
     1.9 -    -> Proof.context -> term -> 'a option
    1.10 -  val static_value_strict: 'a cookie -> { ctxt: Proof.context, target: string option,
    1.11 -    lift_postproc: (term -> term) -> 'a -> 'a, consts: string list }
    1.12 -    -> Proof.context -> term -> 'a
    1.13 -  val static_value_exn: 'a cookie -> { ctxt: Proof.context, target: string option,
    1.14 -    lift_postproc: (term -> term) -> 'a -> 'a, consts: string list }
    1.15 -    -> Proof.context -> term -> 'a Exn.result
    1.16    val dynamic_holds_conv: Proof.context -> conv
    1.17 -  val static_holds_conv: { ctxt: Proof.context, consts: string list } -> Proof.context -> conv
    1.18    val code_reflect: (string * string list option) list -> string list -> string
    1.19      -> string option -> theory -> theory
    1.20    datatype truth = Holds
    1.21 @@ -130,22 +120,6 @@
    1.22  fun dynamic_value cookie ctxt some_target postproc t args =
    1.23    partiality_as_none (dynamic_value_exn cookie ctxt some_target postproc t args);
    1.24  
    1.25 -fun static_value_exn cookie { ctxt, target, lift_postproc, consts } =
    1.26 -  let
    1.27 -    fun compilation' { program, deps } =
    1.28 -      let
    1.29 -        val compilation'' = run_compilation_text cookie ctxt
    1.30 -          (build_compilation_text ctxt target program (map Constant deps));
    1.31 -      in fn _ => fn _ => fn vs_ty_t => fn _ => compilation'' vs_ty_t [] end;
    1.32 -    val compilation = Code_Thingol.static_value { ctxt = ctxt,
    1.33 -      lift_postproc = Exn.map_res o lift_postproc, consts = consts }
    1.34 -      compilation';
    1.35 -  in fn ctxt' => compilation ctxt' o reject_vars ctxt' end;
    1.36 -
    1.37 -fun static_value_strict cookie x = Exn.release oo static_value_exn cookie x;
    1.38 -
    1.39 -fun static_value cookie x = partiality_as_none oo static_value_exn cookie x;
    1.40 -
    1.41  
    1.42  (* evaluation for truth or nothing *)
    1.43  
    1.44 @@ -190,10 +164,6 @@
    1.45      check_holds_oracle ctxt (build_compilation_text ctxt NONE program deps) vs_t)
    1.46        o reject_vars ctxt;
    1.47  
    1.48 -fun static_holds_conv (ctxt_consts as { ctxt, ... }) =
    1.49 -  Code_Thingol.static_conv_thingol ctxt_consts (fn { program, deps } => fn ctxt' => fn vs_t =>
    1.50 -    K (check_holds_oracle ctxt' (build_compilation_text ctxt NONE program (map Constant deps)) vs_t o reject_vars ctxt'));
    1.51 -
    1.52  end; (*local*)
    1.53  
    1.54