src/Tools/nbe.ML
changeset 56973 62da80041afd
parent 56972 f64730f667b9
child 56974 4ab498f41eee
     1.1 --- a/src/Tools/nbe.ML	Thu May 15 16:38:31 2014 +0200
     1.2 +++ b/src/Tools/nbe.ML	Thu May 15 16:38:31 2014 +0200
     1.3 @@ -8,8 +8,8 @@
     1.4  sig
     1.5    val dynamic_conv: Proof.context -> conv
     1.6    val dynamic_value: Proof.context -> term -> term
     1.7 -  val static_conv: Proof.context -> string list -> Proof.context -> conv
     1.8 -  val static_value: Proof.context -> string list -> Proof.context -> term -> term
     1.9 +  val static_conv: { ctxt: Proof.context, consts: string list } -> Proof.context -> conv
    1.10 +  val static_value: { ctxt: Proof.context, consts: string list } -> Proof.context -> term -> term
    1.11  
    1.12    datatype Univ =
    1.13        Const of int * Univ list               (*named (uninterpreted) constants*)
    1.14 @@ -597,16 +597,16 @@
    1.15  fun dynamic_value ctxt = lift_triv_classes_rew ctxt
    1.16    (Code_Thingol.dynamic_value ctxt I (eval_term ctxt o compile false ctxt));
    1.17  
    1.18 -fun static_conv ctxt consts =
    1.19 +fun static_conv (ctxt_consts as { ctxt, ... }) =
    1.20    let
    1.21 -    val evaluator = Code_Thingol.static_conv ctxt consts
    1.22 -      (fn program => fn _ => fn ctxt' => oracle ctxt' (compile true ctxt program));
    1.23 +    val evaluator = Code_Thingol.static_conv ctxt_consts
    1.24 +      (fn { program, ... } => fn ctxt' => oracle ctxt' (compile true ctxt program));
    1.25    in fn ctxt' => lift_triv_classes_conv ctxt' (evaluator ctxt') end;
    1.26  
    1.27 -fun static_value ctxt consts =
    1.28 +fun static_value { ctxt, consts } =
    1.29    let
    1.30 -    val evaluator = Code_Thingol.static_value ctxt I consts
    1.31 -      (fn program => fn _ => fn ctxt' => eval_term ctxt' (compile false ctxt program));
    1.32 +    val evaluator = Code_Thingol.static_value { ctxt = ctxt, lift_postproc = I, consts = consts }
    1.33 +      (fn { program, ... } => fn ctxt' => eval_term ctxt' (compile false ctxt program));
    1.34    in fn ctxt' => lift_triv_classes_rew ctxt' (evaluator ctxt') end;
    1.35  
    1.36  end;