accurate separation of static and dynamic context
authorhaftmann
Thu May 15 16:38:32 2014 +0200 (2014-05-15)
changeset 569744ab498f41eee
parent 56973 62da80041afd
child 56975 1f3e60572081
accurate separation of static and dynamic context
src/Tools/nbe.ML
     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:32 2014 +0200
     1.3 @@ -536,7 +536,7 @@
     1.4  
     1.5  (* evaluation with type reconstruction *)
     1.6  
     1.7 -fun eval_term raw_ctxt (nbe_program, idx_tab) t_original ((vs, ty), t) deps =
     1.8 +fun eval_term (nbe_program, idx_tab) raw_ctxt t_original ((vs, ty), t) deps =
     1.9    let
    1.10      val ctxt = Syntax.init_pretty_global (Proof_Context.theory_of raw_ctxt);
    1.11      val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
    1.12 @@ -585,28 +585,28 @@
    1.13  
    1.14  val (_, raw_oracle) = Context.>>> (Context.map_theory_result
    1.15    (Thm.add_oracle (@{binding normalization_by_evaluation},
    1.16 -    fn (ctxt, nbe_program_idx_tab, vs_ty_t, deps, ct) =>
    1.17 -      mk_equals ctxt ct (eval_term ctxt nbe_program_idx_tab (term_of ct) vs_ty_t deps))));
    1.18 +    fn (nbe_program_idx_tab, ctxt, vs_ty_t, deps, ct) =>
    1.19 +      mk_equals ctxt ct (eval_term nbe_program_idx_tab ctxt (term_of ct) vs_ty_t deps))));
    1.20  
    1.21 -fun oracle ctxt nbe_program_idx_tab vs_ty_t deps ct =
    1.22 -  raw_oracle (ctxt, nbe_program_idx_tab, vs_ty_t, deps, ct);
    1.23 +fun oracle nbe_program_idx_tab ctxt vs_ty_t deps ct =
    1.24 +  raw_oracle (nbe_program_idx_tab, ctxt, vs_ty_t, deps, ct);
    1.25  
    1.26  fun dynamic_conv ctxt = lift_triv_classes_conv ctxt
    1.27 -  (Code_Thingol.dynamic_conv ctxt (oracle ctxt o compile false ctxt));
    1.28 +  (Code_Thingol.dynamic_conv ctxt (fn program => oracle (compile false ctxt program) ctxt));
    1.29  
    1.30  fun dynamic_value ctxt = lift_triv_classes_rew ctxt
    1.31 -  (Code_Thingol.dynamic_value ctxt I (eval_term ctxt o compile false ctxt));
    1.32 +  (Code_Thingol.dynamic_value ctxt I (fn program => eval_term (compile false ctxt program) ctxt));
    1.33  
    1.34  fun static_conv (ctxt_consts as { ctxt, ... }) =
    1.35    let
    1.36      val evaluator = Code_Thingol.static_conv ctxt_consts
    1.37 -      (fn { program, ... } => fn ctxt' => oracle ctxt' (compile true ctxt program));
    1.38 +      (fn { program, ... } => oracle (compile true ctxt program));
    1.39    in fn ctxt' => lift_triv_classes_conv ctxt' (evaluator ctxt') end;
    1.40  
    1.41  fun static_value { ctxt, consts } =
    1.42    let
    1.43      val evaluator = Code_Thingol.static_value { ctxt = ctxt, lift_postproc = I, consts = consts }
    1.44 -      (fn { program, ... } => fn ctxt' => eval_term ctxt' (compile false ctxt program));
    1.45 +      (fn { program, ... } => eval_term (compile false ctxt program));
    1.46    in fn ctxt' => lift_triv_classes_rew ctxt' (evaluator ctxt') end;
    1.47  
    1.48  end;