clarified naming conventions and code for code evaluation sandwiches
authorhaftmann
Thu May 26 15:27:50 2016 +0200 (2016-05-26)
changeset 6315765a81a4ef7f8
parent 63156 3cb84e4469a7
child 63158 534f16b0ca39
clarified naming conventions and code for code evaluation sandwiches
src/HOL/Library/code_test.ML
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/HOL/Tools/code_evaluation.ML
src/Tools/Code/code_preproc.ML
src/Tools/Code/code_runtime.ML
src/Tools/Code/code_target.ML
src/Tools/Code/code_thingol.ML
src/Tools/nbe.ML
     1.1 --- a/src/HOL/Library/code_test.ML	Thu May 26 15:27:50 2016 +0200
     1.2 +++ b/src/HOL/Library/code_test.ML	Thu May 26 15:27:50 2016 +0200
     1.3 @@ -177,7 +177,7 @@
     1.4      val with_dir = if debug then with_overlord_dir else Isabelle_System.with_tmp_dir
     1.5      fun evaluate f = with_dir "Code_Test" (driver ctxt f) |> parse_result compiler
     1.6      fun evaluator program _ vs_ty deps =
     1.7 -      Exn.interruptible_capture evaluate (Code_Target.evaluator ctxt target program deps true vs_ty);
     1.8 +      Exn.interruptible_capture evaluate (Code_Target.computation_text ctxt target program deps true vs_ty);
     1.9      fun postproc f = map (apsnd (map_option (map f)))
    1.10    in
    1.11      Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t)
     2.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu May 26 15:27:50 2016 +0200
     2.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu May 26 15:27:50 2016 +0200
     2.3 @@ -311,7 +311,7 @@
     2.4    let
     2.5      fun evaluator program _ vs_ty_t deps =
     2.6        Exn.interruptible_capture (value opts ctxt cookie)
     2.7 -        (Code_Target.evaluator ctxt target program deps true vs_ty_t)
     2.8 +        (Code_Target.computation_text ctxt target program deps true vs_ty_t)
     2.9    in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t) end
    2.10  
    2.11  
     3.1 --- a/src/HOL/Tools/code_evaluation.ML	Thu May 26 15:27:50 2016 +0200
     3.2 +++ b/src/HOL/Tools/code_evaluation.ML	Thu May 26 15:27:50 2016 +0200
     3.3 @@ -185,19 +185,19 @@
     3.4  
     3.5  fun term_of_const_for thy = Axclass.unoverload_const thy o dest_Const o HOLogic.term_of_const;
     3.6  
     3.7 -fun gen_dynamic_value dynamic_value ctxt t =
     3.8 -  dynamic_value cookie ctxt NONE I (mk_term_of t) [];
     3.9 +fun gen_dynamic_value computation ctxt t =
    3.10 +  computation cookie ctxt NONE I (mk_term_of t) [];
    3.11  
    3.12  val dynamic_value = gen_dynamic_value Code_Runtime.dynamic_value;
    3.13  val dynamic_value_strict = gen_dynamic_value Code_Runtime.dynamic_value_strict;
    3.14  val dynamic_value_exn = gen_dynamic_value Code_Runtime.dynamic_value_exn;
    3.15  
    3.16 -fun gen_static_value static_value { ctxt, consts, Ts } =
    3.17 +fun gen_static_value computation { ctxt, consts, Ts } =
    3.18    let
    3.19 -    val static_value' = static_value cookie
    3.20 +    val computation' = computation cookie
    3.21        { ctxt = ctxt, target = NONE, lift_postproc = I, consts =
    3.22          union (op =) (map (term_of_const_for (Proof_Context.theory_of ctxt)) Ts) consts }
    3.23 -  in fn ctxt' => fn t => static_value' ctxt' (mk_term_of t) end;
    3.24 +  in fn ctxt' => computation' ctxt' o mk_term_of end;
    3.25  
    3.26  val static_value = gen_static_value Code_Runtime.static_value;
    3.27  val static_value_strict = gen_static_value Code_Runtime.static_value_strict;
     4.1 --- a/src/Tools/Code/code_preproc.ML	Thu May 26 15:27:50 2016 +0200
     4.2 +++ b/src/Tools/Code/code_preproc.ML	Thu May 26 15:27:50 2016 +0200
     4.3 @@ -127,7 +127,7 @@
     4.4    val chain: T -> T -> T
     4.5    val lift: (Proof.context -> cterm -> (cterm -> thm) * thm) -> T
     4.6    val conversion: T -> (Proof.context -> term -> conv) -> Proof.context -> conv;
     4.7 -  val evaluation: T -> ((term -> term) -> 'a -> 'b) ->
     4.8 +  val computation: T -> ((term -> term) -> 'a -> 'b) ->
     4.9      (Proof.context -> term -> 'a) -> Proof.context -> term -> 'b;
    4.10  end = struct
    4.11  
    4.12 @@ -151,7 +151,7 @@
    4.13      val (postproc, ct') = sandwich ctxt ct;
    4.14    in postproc (conv ctxt (Thm.term_of ct') ct') end;
    4.15  
    4.16 -fun evaluation sandwich lift_postproc eval ctxt t =
    4.17 +fun computation sandwich lift_postproc eval ctxt t =
    4.18    let
    4.19      val (postproc, ct') = sandwich ctxt (Thm.cterm_of ctxt t);
    4.20    in
    4.21 @@ -538,32 +538,45 @@
    4.22  
    4.23  (** retrieval and evaluation interfaces **)
    4.24  
    4.25 +(*
    4.26 +  naming conventions
    4.27 +  * evaluator "eval" is either
    4.28 +    * conversion "conv"
    4.29 +    * value computation "comp"
    4.30 +  * "evaluation" is a lifting of an evaluator
    4.31 +*)
    4.32 +
    4.33  fun obtain ignore_cache ctxt consts ts = apsnd snd
    4.34    (Wellsorted.change_yield (if ignore_cache then NONE else SOME (Proof_Context.theory_of ctxt))
    4.35      (extend_arities_eqngr ctxt consts ts));
    4.36  
    4.37 -fun dynamic_evaluator eval ctxt t =
    4.38 +fun dynamic_evaluation eval ctxt t =
    4.39    let
    4.40      val consts = fold_aterms
    4.41        (fn Const (c, _) => insert (op =) c | _ => I) t [];
    4.42      val (algebra, eqngr) = obtain false ctxt consts [t];
    4.43    in eval algebra eqngr t end;
    4.44  
    4.45 +fun static_evaluation ctxt consts eval =
    4.46 +  let
    4.47 +    val (algebra, eqngr) = obtain true ctxt consts [];
    4.48 +  in eval { algebra = algebra, eqngr = eqngr } end;
    4.49 +
    4.50  fun dynamic_conv ctxt conv =
    4.51 -  Sandwich.conversion (value_sandwich ctxt) (dynamic_evaluator conv) ctxt;
    4.52 +  Sandwich.conversion (value_sandwich ctxt)
    4.53 +    (dynamic_evaluation conv) ctxt;
    4.54  
    4.55  fun dynamic_value ctxt lift_postproc evaluator =
    4.56 -  Sandwich.evaluation (value_sandwich ctxt) lift_postproc (dynamic_evaluator evaluator) ctxt;
    4.57 +  Sandwich.computation (value_sandwich ctxt) lift_postproc
    4.58 +    (dynamic_evaluation evaluator) ctxt;
    4.59  
    4.60  fun static_conv { ctxt, consts } conv =
    4.61 -  let
    4.62 -    val (algebra, eqngr) = obtain true ctxt consts [];
    4.63 -  in Sandwich.conversion (value_sandwich ctxt) (conv { algebra = algebra, eqngr = eqngr }) end;
    4.64 +  Sandwich.conversion (value_sandwich ctxt)
    4.65 +    (static_evaluation ctxt consts conv);
    4.66  
    4.67 -fun static_value { ctxt, lift_postproc, consts } evaluator =
    4.68 -  let
    4.69 -    val (algebra, eqngr) = obtain true ctxt consts [];
    4.70 -  in Sandwich.evaluation (value_sandwich ctxt) lift_postproc (evaluator { algebra = algebra, eqngr = eqngr }) end;
    4.71 +fun static_value { ctxt, lift_postproc, consts } comp =
    4.72 +  Sandwich.computation (value_sandwich ctxt) lift_postproc
    4.73 +    (static_evaluation ctxt consts comp);
    4.74  
    4.75  
    4.76  (** setup **)
     5.1 --- a/src/Tools/Code/code_runtime.ML	Thu May 26 15:27:50 2016 +0200
     5.2 +++ b/src/Tools/Code/code_runtime.ML	Thu May 26 15:27:50 2016 +0200
     5.3 @@ -53,7 +53,7 @@
     5.4  
     5.5  open Basic_Code_Symbol;
     5.6  
     5.7 -(** evaluation **)
     5.8 +(** computation **)
     5.9  
    5.10  (* technical prerequisites *)
    5.11  
    5.12 @@ -90,29 +90,25 @@
    5.13        prelude ^ "\nval _ = Context.put_generic_context (SOME (Context.map_proof (" ^
    5.14        put_ml ^ " (fn () => " ^ value ^ ")) (Context.the_generic_context ())))";
    5.15      val ctxt' = ctxt
    5.16 -      |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
    5.17 +      |> put (fn () => error ("Bad computation for " ^ quote put_ml))
    5.18        |> Context.proof_map (exec ctxt false code);
    5.19    in get ctxt' () end;
    5.20  
    5.21  
    5.22 -(* evaluation into target language values *)
    5.23 +(* computation as evaluation into ML language values *)
    5.24  
    5.25  type 'a cookie = (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string;
    5.26  
    5.27  fun reject_vars ctxt t =
    5.28    ((Sign.no_frees ctxt o Sign.no_vars ctxt o map_types (K dummyT)) t; t);
    5.29  
    5.30 -fun obtain_evaluator ctxt some_target program consts =
    5.31 +fun build_computation_text ctxt some_target program consts =
    5.32 +  Code_Target.computation_text ctxt (the_default target some_target) program consts false
    5.33 +  #>> (fn ml_modules => space_implode "\n\n" (map snd ml_modules));
    5.34 +
    5.35 +fun run_computation_text cookie ctxt comp vs_t args =
    5.36    let
    5.37 -    val evaluator' = Code_Target.evaluator ctxt (the_default target some_target) program consts false;
    5.38 -  in
    5.39 -    evaluator'
    5.40 -    #> apfst (fn ml_modules => space_implode "\n\n" (map snd ml_modules))
    5.41 -  end;
    5.42 -
    5.43 -fun evaluation cookie ctxt evaluator vs_t args =
    5.44 -  let
    5.45 -    val (program_code, value_name) = evaluator vs_t;
    5.46 +    val (program_code, value_name) = comp vs_t;
    5.47      val value_code = space_implode " "
    5.48        (value_name :: "()" :: map (enclose "(" ")") args);
    5.49    in Exn.interruptible_capture (value ctxt cookie) (program_code, value_code) end;
    5.50 @@ -128,9 +124,9 @@
    5.51      val _ = if Config.get ctxt trace
    5.52        then tracing ("Evaluation of term " ^ quote (Syntax.string_of_term ctxt t))
    5.53        else ()
    5.54 -    fun evaluator program _ vs_ty_t deps =
    5.55 -      evaluation cookie ctxt (obtain_evaluator ctxt some_target program deps) vs_ty_t args;
    5.56 -  in Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t end;
    5.57 +    fun comp program _ vs_ty_t deps =
    5.58 +      run_computation_text cookie ctxt (build_computation_text ctxt some_target program deps) vs_ty_t args;
    5.59 +  in Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) comp t end;
    5.60  
    5.61  fun dynamic_value_strict cookie ctxt some_target postproc t args =
    5.62    Exn.release (dynamic_value_exn cookie ctxt some_target postproc t args);
    5.63 @@ -138,18 +134,17 @@
    5.64  fun dynamic_value cookie ctxt some_target postproc t args =
    5.65    partiality_as_none (dynamic_value_exn cookie ctxt some_target postproc t args);
    5.66  
    5.67 -fun static_evaluator cookie ctxt some_target { program, deps } =
    5.68 -  let
    5.69 -    val evaluator = obtain_evaluator ctxt some_target program (map Constant deps);
    5.70 -    val evaluation' = evaluation cookie ctxt evaluator;
    5.71 -  in fn _ => fn _ => fn vs_ty_t => fn _ => evaluation' vs_ty_t [] end;
    5.72 -
    5.73  fun static_value_exn cookie { ctxt, target, lift_postproc, consts } =
    5.74    let
    5.75 -    val evaluator = Code_Thingol.static_value { ctxt = ctxt,
    5.76 +    fun computation' { program, deps } =
    5.77 +      let
    5.78 +        val computation'' = run_computation_text cookie ctxt
    5.79 +          (build_computation_text ctxt target program (map Constant deps));
    5.80 +      in fn _ => fn _ => fn vs_ty_t => fn _ => computation'' vs_ty_t [] end;
    5.81 +    val computation = Code_Thingol.static_value { ctxt = ctxt,
    5.82        lift_postproc = Exn.map_res o lift_postproc, consts = consts }
    5.83 -      (static_evaluator cookie ctxt target);
    5.84 -  in fn ctxt' => evaluator ctxt' o reject_vars ctxt' end;
    5.85 +      computation';
    5.86 +  in fn ctxt' => computation ctxt' o reject_vars ctxt' end;
    5.87  
    5.88  fun static_value_strict cookie = Exn.release ooo static_value_exn cookie;
    5.89  
    5.90 @@ -178,7 +173,7 @@
    5.91        then error ("Not a proposition: " ^ Syntax.string_of_term ctxt t)
    5.92        else ();
    5.93      val iff = Thm.cterm_of ctxt (Term.Const (@{const_name Pure.eq}, propT --> propT --> propT));
    5.94 -    val result = case partiality_as_none (evaluation truth_cookie ctxt evaluator vs_t [])
    5.95 +    val result = case partiality_as_none (run_computation_text truth_cookie ctxt evaluator vs_t [])
    5.96       of SOME Holds => true
    5.97        | _ => false;
    5.98    in
    5.99 @@ -196,12 +191,12 @@
   5.100  
   5.101  fun dynamic_holds_conv ctxt = Code_Thingol.dynamic_conv ctxt
   5.102    (fn program => fn vs_t => fn deps =>
   5.103 -    check_holds_oracle ctxt (obtain_evaluator ctxt NONE program deps) vs_t)
   5.104 +    check_holds_oracle ctxt (build_computation_text ctxt NONE program deps) vs_t)
   5.105        o reject_vars ctxt;
   5.106  
   5.107  fun static_holds_conv (ctxt_consts as { ctxt, ... }) =
   5.108    Code_Thingol.static_conv_thingol ctxt_consts (fn { program, deps } => fn ctxt' => fn vs_t =>
   5.109 -    K (check_holds_oracle ctxt' (obtain_evaluator ctxt NONE program (map Constant deps)) vs_t o reject_vars ctxt'));
   5.110 +    K (check_holds_oracle ctxt' (build_computation_text ctxt NONE program (map Constant deps)) vs_t o reject_vars ctxt'));
   5.111  
   5.112  end; (*local*)
   5.113  
     6.1 --- a/src/Tools/Code/code_target.ML	Thu May 26 15:27:50 2016 +0200
     6.2 +++ b/src/Tools/Code/code_target.ML	Thu May 26 15:27:50 2016 +0200
     6.3 @@ -28,7 +28,7 @@
     6.4      -> ((string * bool) * Token.T list) list -> unit
     6.5  
     6.6    val generatedN: string
     6.7 -  val evaluator: Proof.context -> string -> Code_Thingol.program
     6.8 +  val computation_text: Proof.context -> string -> Code_Thingol.program
     6.9      -> Code_Symbol.T list -> bool -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
    6.10      -> (string * string) list * string
    6.11  
    6.12 @@ -396,7 +396,7 @@
    6.13      else Isabelle_System.with_tmp_dir "Code_Test" ext_check
    6.14    end;
    6.15  
    6.16 -fun subevaluator mounted_serializer prepared_program syms all_public ((vs, ty), t) =
    6.17 +fun dynamic_computation_text mounted_serializer prepared_program syms all_public ((vs, ty), t) =
    6.18    let
    6.19      val _ = if Code_Thingol.contains_dict_var t then
    6.20        error "Term to be evaluated contains free dictionaries" else ();
    6.21 @@ -413,11 +413,11 @@
    6.22      val value_name = the (deresolve Code_Symbol.value);
    6.23    in (program_code, value_name) end;
    6.24  
    6.25 -fun evaluator ctxt target_name program syms =
    6.26 +fun computation_text ctxt target_name program syms =
    6.27    let
    6.28      val (mounted_serializer, (_, prepared_program)) =
    6.29        mount_serializer ctxt target_name NONE generatedN [] program syms;
    6.30 -  in subevaluator mounted_serializer prepared_program syms end;
    6.31 +  in dynamic_computation_text mounted_serializer prepared_program syms end;
    6.32  
    6.33  end; (* local *)
    6.34  
     7.1 --- a/src/Tools/Code/code_thingol.ML	Thu May 26 15:27:50 2016 +0200
     7.2 +++ b/src/Tools/Code/code_thingol.ML	Thu May 26 15:27:50 2016 +0200
     7.3 @@ -839,49 +839,59 @@
     7.4      #> term_value
     7.5    end;
     7.6  
     7.7 -fun dynamic_evaluator ctxt evaluator algebra eqngr t =
     7.8 +fun dynamic_evaluation eval ctxt algebra eqngr t =
     7.9    let
    7.10      val ((program, (vs_ty_t', deps)), _) =
    7.11 -      invoke_generation false (Proof_Context.theory_of ctxt) (algebra, eqngr) ensure_value t;
    7.12 -  in evaluator program t vs_ty_t' deps end;
    7.13 +      invoke_generation false (Proof_Context.theory_of ctxt)
    7.14 +        (algebra, eqngr) ensure_value t;
    7.15 +  in eval program t vs_ty_t' deps end;
    7.16  
    7.17  fun dynamic_conv ctxt conv =
    7.18 -  Code_Preproc.dynamic_conv ctxt (dynamic_evaluator ctxt (fn program => fn _ => conv program));
    7.19 -
    7.20 -fun dynamic_value ctxt postproc evaluator =
    7.21 -  Code_Preproc.dynamic_value ctxt postproc (dynamic_evaluator ctxt evaluator);
    7.22 +  Code_Preproc.dynamic_conv ctxt
    7.23 +    (dynamic_evaluation (fn program => fn _ => conv program) ctxt);
    7.24  
    7.25 -fun static_subevaluator ctxt subevaluator algebra eqngr program t =
    7.26 -  let
    7.27 -    val ((_, ((vs_ty', t'), deps)), _) =
    7.28 -      ensure_value ctxt algebra eqngr t ([], program);
    7.29 -  in subevaluator ctxt t (vs_ty', t') deps end;
    7.30 +fun dynamic_value ctxt postproc comp =
    7.31 +  Code_Preproc.dynamic_value ctxt postproc
    7.32 +    (dynamic_evaluation comp ctxt);
    7.33  
    7.34 -fun static_evaluator_thingol ctxt evaluator consts { algebra, eqngr } =
    7.35 +fun static_evaluation ctxt consts algebra eqngr static_eval =
    7.36    let
    7.37      fun generate_consts ctxt algebra eqngr =
    7.38        fold_map (ensure_const ctxt algebra eqngr false);
    7.39      val (deps, program) =
    7.40 -      invoke_generation true (Proof_Context.theory_of ctxt) (algebra, eqngr) generate_consts consts;
    7.41 -    val subevaluator = evaluator { program = program, deps = deps };
    7.42 -  in fn ctxt' => static_subevaluator ctxt' subevaluator algebra eqngr program end;
    7.43 +      invoke_generation true (Proof_Context.theory_of ctxt)
    7.44 +        (algebra, eqngr) generate_consts consts;
    7.45 +  in static_eval { program = program, deps = deps } end;
    7.46  
    7.47 -fun static_evaluator_isa ctxt evaluator consts { algebra, eqngr } =
    7.48 +fun static_evaluation_thingol ctxt consts algebra eqngr static_eval =
    7.49    let
    7.50 -    fun generate_consts ctxt algebra eqngr =
    7.51 -      fold_map (ensure_const ctxt algebra eqngr false);
    7.52 -    val (_, program) =
    7.53 -      invoke_generation true (Proof_Context.theory_of ctxt) (algebra, eqngr) generate_consts consts;
    7.54 -  in evaluator (program: program) end;
    7.55 +    fun evaluation' program dynamic_eval ctxt t =
    7.56 +      let
    7.57 +        val ((_, ((vs_ty', t'), deps)), _) =
    7.58 +          ensure_value ctxt algebra eqngr t ([], program);
    7.59 +      in dynamic_eval ctxt t (vs_ty', t') deps end;
    7.60 +    fun evaluation static_eval { program, deps } =
    7.61 +      evaluation' program (static_eval { program = program, deps = deps });
    7.62 +  in
    7.63 +    static_evaluation ctxt consts algebra eqngr
    7.64 +      (evaluation static_eval)
    7.65 +  end;
    7.66 +
    7.67 +fun static_evaluation_isa ctxt consts algebra eqngr static_eval =
    7.68 +  static_evaluation ctxt consts algebra eqngr
    7.69 +    (fn { program, ... } => static_eval (program: program));
    7.70  
    7.71  fun static_conv_thingol (ctxt_consts as { ctxt, consts }) conv =
    7.72 -  Code_Preproc.static_conv ctxt_consts (static_evaluator_thingol ctxt (K oo conv) consts);
    7.73 +  Code_Preproc.static_conv ctxt_consts (fn { algebra, eqngr } =>
    7.74 +    static_evaluation_thingol ctxt consts algebra eqngr (K oo conv));
    7.75  
    7.76  fun static_conv_isa (ctxt_consts as { ctxt, consts }) conv =
    7.77 -  Code_Preproc.static_conv ctxt_consts (static_evaluator_isa ctxt conv consts);
    7.78 +  Code_Preproc.static_conv ctxt_consts (fn { algebra, eqngr } =>
    7.79 +    static_evaluation_isa ctxt consts algebra eqngr conv);
    7.80  
    7.81 -fun static_value (ctxt_postproc_consts as { ctxt, consts, ... }) evaluator =
    7.82 -  Code_Preproc.static_value ctxt_postproc_consts (static_evaluator_thingol ctxt evaluator consts);
    7.83 +fun static_value (ctxt_postproc_consts as { ctxt, consts, ... }) comp =
    7.84 +  Code_Preproc.static_value ctxt_postproc_consts (fn { algebra, eqngr } =>
    7.85 +    static_evaluation_thingol ctxt consts algebra eqngr comp);
    7.86  
    7.87  
    7.88  (** constant expressions **)
     8.1 --- a/src/Tools/nbe.ML	Thu May 26 15:27:50 2016 +0200
     8.2 +++ b/src/Tools/nbe.ML	Thu May 26 15:27:50 2016 +0200
     8.3 @@ -487,9 +487,9 @@
     8.4    end;
     8.5  
     8.6  
     8.7 -(** evaluation **)
     8.8 +(** normalization **)
     8.9  
    8.10 -(* term evaluation by compilation *)
    8.11 +(* term normalization by compilation *)
    8.12  
    8.13  fun compile_term ctxt nbe_program deps (vs : (string * sort) list, t) =
    8.14    let 
    8.15 @@ -537,9 +537,9 @@
    8.16    in of_univ 0 t 0 |> fst end;
    8.17  
    8.18  
    8.19 -(* evaluation with type reconstruction *)
    8.20 +(* normalize with type reconstruction *)
    8.21  
    8.22 -fun eval_term (nbe_program, idx_tab) raw_ctxt t_original ((vs, ty) : typscheme, t) deps =
    8.23 +fun normalize (nbe_program, idx_tab) raw_ctxt t_original ((vs, ty) : typscheme, t) deps =
    8.24    let
    8.25      val ctxt = Syntax.init_pretty_global (Proof_Context.theory_of raw_ctxt);
    8.26      val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
    8.27 @@ -591,27 +591,29 @@
    8.28  val (_, raw_oracle) = Context.>>> (Context.map_theory_result
    8.29    (Thm.add_oracle (@{binding normalization_by_evaluation},
    8.30      fn (nbe_program_idx_tab, ctxt, vs_ty_t, deps, ct) =>
    8.31 -      mk_equals ctxt ct (eval_term nbe_program_idx_tab ctxt (Thm.term_of ct) vs_ty_t deps))));
    8.32 +      mk_equals ctxt ct (normalize nbe_program_idx_tab ctxt (Thm.term_of ct) vs_ty_t deps))));
    8.33  
    8.34  fun oracle nbe_program_idx_tab ctxt vs_ty_t deps ct =
    8.35    raw_oracle (nbe_program_idx_tab, ctxt, vs_ty_t, deps, ct);
    8.36  
    8.37  fun dynamic_conv ctxt = lift_triv_classes_conv ctxt
    8.38 -  (Code_Thingol.dynamic_conv ctxt (fn program => oracle (compile false ctxt program) ctxt));
    8.39 +  (Code_Thingol.dynamic_conv ctxt (fn program =>
    8.40 +    oracle (compile false ctxt program) ctxt));
    8.41  
    8.42  fun dynamic_value ctxt = lift_triv_classes_rew ctxt
    8.43 -  (Code_Thingol.dynamic_value ctxt I (fn program => eval_term (compile false ctxt program) ctxt));
    8.44 +  (Code_Thingol.dynamic_value ctxt I (fn program =>
    8.45 +    normalize (compile false ctxt program) ctxt));
    8.46  
    8.47  fun static_conv (ctxt_consts as { ctxt, ... }) =
    8.48    let
    8.49 -    val evaluator = Code_Thingol.static_conv_thingol ctxt_consts
    8.50 +    val conv = Code_Thingol.static_conv_thingol ctxt_consts
    8.51        (fn { program, ... } => oracle (compile true ctxt program));
    8.52 -  in fn ctxt' => lift_triv_classes_conv ctxt' (evaluator ctxt') end;
    8.53 +  in fn ctxt' => lift_triv_classes_conv ctxt' (conv ctxt') end;
    8.54  
    8.55  fun static_value { ctxt, consts } =
    8.56    let
    8.57 -    val evaluator = Code_Thingol.static_value { ctxt = ctxt, lift_postproc = I, consts = consts }
    8.58 -      (fn { program, ... } => eval_term (compile false ctxt program));
    8.59 -  in fn ctxt' => lift_triv_classes_rew ctxt' (evaluator ctxt') end;
    8.60 +    val comp = Code_Thingol.static_value { ctxt = ctxt, lift_postproc = I, consts = consts }
    8.61 +      (fn { program, ... } => normalize (compile false ctxt program));
    8.62 +  in fn ctxt' => lift_triv_classes_rew ctxt' (comp ctxt') end;
    8.63  
    8.64  end;