# HG changeset patch
# User haftmann
# Date 1464269270 -7200
# Node ID 65a81a4ef7f84738cebeb1e53393bf7c0fff38b7
# Parent  3cb84e4469a76de644d2b7673784e911543eff5a
clarified naming conventions and code for code evaluation sandwiches

diff -r 3cb84e4469a7 -r 65a81a4ef7f8 src/HOL/Library/code_test.ML
--- a/src/HOL/Library/code_test.ML	Thu May 26 15:27:50 2016 +0200
+++ b/src/HOL/Library/code_test.ML	Thu May 26 15:27:50 2016 +0200
@@ -177,7 +177,7 @@
     val with_dir = if debug then with_overlord_dir else Isabelle_System.with_tmp_dir
     fun evaluate f = with_dir "Code_Test" (driver ctxt f) |> parse_result compiler
     fun evaluator program _ vs_ty deps =
-      Exn.interruptible_capture evaluate (Code_Target.evaluator ctxt target program deps true vs_ty);
+      Exn.interruptible_capture evaluate (Code_Target.computation_text ctxt target program deps true vs_ty);
     fun postproc f = map (apsnd (map_option (map f)))
   in
     Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t)
diff -r 3cb84e4469a7 -r 65a81a4ef7f8 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu May 26 15:27:50 2016 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu May 26 15:27:50 2016 +0200
@@ -311,7 +311,7 @@
   let
     fun evaluator program _ vs_ty_t deps =
       Exn.interruptible_capture (value opts ctxt cookie)
-        (Code_Target.evaluator ctxt target program deps true vs_ty_t)
+        (Code_Target.computation_text ctxt target program deps true vs_ty_t)
   in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t) end
 
 
diff -r 3cb84e4469a7 -r 65a81a4ef7f8 src/HOL/Tools/code_evaluation.ML
--- a/src/HOL/Tools/code_evaluation.ML	Thu May 26 15:27:50 2016 +0200
+++ b/src/HOL/Tools/code_evaluation.ML	Thu May 26 15:27:50 2016 +0200
@@ -185,19 +185,19 @@
 
 fun term_of_const_for thy = Axclass.unoverload_const thy o dest_Const o HOLogic.term_of_const;
 
-fun gen_dynamic_value dynamic_value ctxt t =
-  dynamic_value cookie ctxt NONE I (mk_term_of t) [];
+fun gen_dynamic_value computation ctxt t =
+  computation cookie ctxt NONE I (mk_term_of t) [];
 
 val dynamic_value = gen_dynamic_value Code_Runtime.dynamic_value;
 val dynamic_value_strict = gen_dynamic_value Code_Runtime.dynamic_value_strict;
 val dynamic_value_exn = gen_dynamic_value Code_Runtime.dynamic_value_exn;
 
-fun gen_static_value static_value { ctxt, consts, Ts } =
+fun gen_static_value computation { ctxt, consts, Ts } =
   let
-    val static_value' = static_value cookie
+    val computation' = computation cookie
       { ctxt = ctxt, target = NONE, lift_postproc = I, consts =
         union (op =) (map (term_of_const_for (Proof_Context.theory_of ctxt)) Ts) consts }
-  in fn ctxt' => fn t => static_value' ctxt' (mk_term_of t) end;
+  in fn ctxt' => computation' ctxt' o mk_term_of end;
 
 val static_value = gen_static_value Code_Runtime.static_value;
 val static_value_strict = gen_static_value Code_Runtime.static_value_strict;
diff -r 3cb84e4469a7 -r 65a81a4ef7f8 src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Thu May 26 15:27:50 2016 +0200
+++ b/src/Tools/Code/code_preproc.ML	Thu May 26 15:27:50 2016 +0200
@@ -127,7 +127,7 @@
   val chain: T -> T -> T
   val lift: (Proof.context -> cterm -> (cterm -> thm) * thm) -> T
   val conversion: T -> (Proof.context -> term -> conv) -> Proof.context -> conv;
-  val evaluation: T -> ((term -> term) -> 'a -> 'b) ->
+  val computation: T -> ((term -> term) -> 'a -> 'b) ->
     (Proof.context -> term -> 'a) -> Proof.context -> term -> 'b;
 end = struct
 
@@ -151,7 +151,7 @@
     val (postproc, ct') = sandwich ctxt ct;
   in postproc (conv ctxt (Thm.term_of ct') ct') end;
 
-fun evaluation sandwich lift_postproc eval ctxt t =
+fun computation sandwich lift_postproc eval ctxt t =
   let
     val (postproc, ct') = sandwich ctxt (Thm.cterm_of ctxt t);
   in
@@ -538,32 +538,45 @@
 
 (** retrieval and evaluation interfaces **)
 
+(*
+  naming conventions
+  * evaluator "eval" is either
+    * conversion "conv"
+    * value computation "comp"
+  * "evaluation" is a lifting of an evaluator
+*)
+
 fun obtain ignore_cache ctxt consts ts = apsnd snd
   (Wellsorted.change_yield (if ignore_cache then NONE else SOME (Proof_Context.theory_of ctxt))
     (extend_arities_eqngr ctxt consts ts));
 
-fun dynamic_evaluator eval ctxt t =
+fun dynamic_evaluation eval ctxt t =
   let
     val consts = fold_aterms
       (fn Const (c, _) => insert (op =) c | _ => I) t [];
     val (algebra, eqngr) = obtain false ctxt consts [t];
   in eval algebra eqngr t end;
 
+fun static_evaluation ctxt consts eval =
+  let
+    val (algebra, eqngr) = obtain true ctxt consts [];
+  in eval { algebra = algebra, eqngr = eqngr } end;
+
 fun dynamic_conv ctxt conv =
-  Sandwich.conversion (value_sandwich ctxt) (dynamic_evaluator conv) ctxt;
+  Sandwich.conversion (value_sandwich ctxt)
+    (dynamic_evaluation conv) ctxt;
 
 fun dynamic_value ctxt lift_postproc evaluator =
-  Sandwich.evaluation (value_sandwich ctxt) lift_postproc (dynamic_evaluator evaluator) ctxt;
+  Sandwich.computation (value_sandwich ctxt) lift_postproc
+    (dynamic_evaluation evaluator) ctxt;
 
 fun static_conv { ctxt, consts } conv =
-  let
-    val (algebra, eqngr) = obtain true ctxt consts [];
-  in Sandwich.conversion (value_sandwich ctxt) (conv { algebra = algebra, eqngr = eqngr }) end;
+  Sandwich.conversion (value_sandwich ctxt)
+    (static_evaluation ctxt consts conv);
 
-fun static_value { ctxt, lift_postproc, consts } evaluator =
-  let
-    val (algebra, eqngr) = obtain true ctxt consts [];
-  in Sandwich.evaluation (value_sandwich ctxt) lift_postproc (evaluator { algebra = algebra, eqngr = eqngr }) end;
+fun static_value { ctxt, lift_postproc, consts } comp =
+  Sandwich.computation (value_sandwich ctxt) lift_postproc
+    (static_evaluation ctxt consts comp);
 
 
 (** setup **)
diff -r 3cb84e4469a7 -r 65a81a4ef7f8 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Thu May 26 15:27:50 2016 +0200
+++ b/src/Tools/Code/code_runtime.ML	Thu May 26 15:27:50 2016 +0200
@@ -53,7 +53,7 @@
 
 open Basic_Code_Symbol;
 
-(** evaluation **)
+(** computation **)
 
 (* technical prerequisites *)
 
@@ -90,29 +90,25 @@
       prelude ^ "\nval _ = Context.put_generic_context (SOME (Context.map_proof (" ^
       put_ml ^ " (fn () => " ^ value ^ ")) (Context.the_generic_context ())))";
     val ctxt' = ctxt
-      |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
+      |> put (fn () => error ("Bad computation for " ^ quote put_ml))
       |> Context.proof_map (exec ctxt false code);
   in get ctxt' () end;
 
 
-(* evaluation into target language values *)
+(* computation as evaluation into ML language values *)
 
 type 'a cookie = (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string;
 
 fun reject_vars ctxt t =
   ((Sign.no_frees ctxt o Sign.no_vars ctxt o map_types (K dummyT)) t; t);
 
-fun obtain_evaluator ctxt some_target program consts =
+fun build_computation_text ctxt some_target program consts =
+  Code_Target.computation_text ctxt (the_default target some_target) program consts false
+  #>> (fn ml_modules => space_implode "\n\n" (map snd ml_modules));
+
+fun run_computation_text cookie ctxt comp vs_t args =
   let
-    val evaluator' = Code_Target.evaluator ctxt (the_default target some_target) program consts false;
-  in
-    evaluator'
-    #> apfst (fn ml_modules => space_implode "\n\n" (map snd ml_modules))
-  end;
-
-fun evaluation cookie ctxt evaluator vs_t args =
-  let
-    val (program_code, value_name) = evaluator vs_t;
+    val (program_code, value_name) = comp vs_t;
     val value_code = space_implode " "
       (value_name :: "()" :: map (enclose "(" ")") args);
   in Exn.interruptible_capture (value ctxt cookie) (program_code, value_code) end;
@@ -128,9 +124,9 @@
     val _ = if Config.get ctxt trace
       then tracing ("Evaluation of term " ^ quote (Syntax.string_of_term ctxt t))
       else ()
-    fun evaluator program _ vs_ty_t deps =
-      evaluation cookie ctxt (obtain_evaluator ctxt some_target program deps) vs_ty_t args;
-  in Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t end;
+    fun comp program _ vs_ty_t deps =
+      run_computation_text cookie ctxt (build_computation_text ctxt some_target program deps) vs_ty_t args;
+  in Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) comp t end;
 
 fun dynamic_value_strict cookie ctxt some_target postproc t args =
   Exn.release (dynamic_value_exn cookie ctxt some_target postproc t args);
@@ -138,18 +134,17 @@
 fun dynamic_value cookie ctxt some_target postproc t args =
   partiality_as_none (dynamic_value_exn cookie ctxt some_target postproc t args);
 
-fun static_evaluator cookie ctxt some_target { program, deps } =
-  let
-    val evaluator = obtain_evaluator ctxt some_target program (map Constant deps);
-    val evaluation' = evaluation cookie ctxt evaluator;
-  in fn _ => fn _ => fn vs_ty_t => fn _ => evaluation' vs_ty_t [] end;
-
 fun static_value_exn cookie { ctxt, target, lift_postproc, consts } =
   let
-    val evaluator = Code_Thingol.static_value { ctxt = ctxt,
+    fun computation' { program, deps } =
+      let
+        val computation'' = run_computation_text cookie ctxt
+          (build_computation_text ctxt target program (map Constant deps));
+      in fn _ => fn _ => fn vs_ty_t => fn _ => computation'' vs_ty_t [] end;
+    val computation = Code_Thingol.static_value { ctxt = ctxt,
       lift_postproc = Exn.map_res o lift_postproc, consts = consts }
-      (static_evaluator cookie ctxt target);
-  in fn ctxt' => evaluator ctxt' o reject_vars ctxt' end;
+      computation';
+  in fn ctxt' => computation ctxt' o reject_vars ctxt' end;
 
 fun static_value_strict cookie = Exn.release ooo static_value_exn cookie;
 
@@ -178,7 +173,7 @@
       then error ("Not a proposition: " ^ Syntax.string_of_term ctxt t)
       else ();
     val iff = Thm.cterm_of ctxt (Term.Const (@{const_name Pure.eq}, propT --> propT --> propT));
-    val result = case partiality_as_none (evaluation truth_cookie ctxt evaluator vs_t [])
+    val result = case partiality_as_none (run_computation_text truth_cookie ctxt evaluator vs_t [])
      of SOME Holds => true
       | _ => false;
   in
@@ -196,12 +191,12 @@
 
 fun dynamic_holds_conv ctxt = Code_Thingol.dynamic_conv ctxt
   (fn program => fn vs_t => fn deps =>
-    check_holds_oracle ctxt (obtain_evaluator ctxt NONE program deps) vs_t)
+    check_holds_oracle ctxt (build_computation_text ctxt NONE program deps) vs_t)
       o reject_vars ctxt;
 
 fun static_holds_conv (ctxt_consts as { ctxt, ... }) =
   Code_Thingol.static_conv_thingol ctxt_consts (fn { program, deps } => fn ctxt' => fn vs_t =>
-    K (check_holds_oracle ctxt' (obtain_evaluator ctxt NONE program (map Constant deps)) vs_t o reject_vars ctxt'));
+    K (check_holds_oracle ctxt' (build_computation_text ctxt NONE program (map Constant deps)) vs_t o reject_vars ctxt'));
 
 end; (*local*)
 
diff -r 3cb84e4469a7 -r 65a81a4ef7f8 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Thu May 26 15:27:50 2016 +0200
+++ b/src/Tools/Code/code_target.ML	Thu May 26 15:27:50 2016 +0200
@@ -28,7 +28,7 @@
     -> ((string * bool) * Token.T list) list -> unit
 
   val generatedN: string
-  val evaluator: Proof.context -> string -> Code_Thingol.program
+  val computation_text: Proof.context -> string -> Code_Thingol.program
     -> Code_Symbol.T list -> bool -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
     -> (string * string) list * string
 
@@ -396,7 +396,7 @@
     else Isabelle_System.with_tmp_dir "Code_Test" ext_check
   end;
 
-fun subevaluator mounted_serializer prepared_program syms all_public ((vs, ty), t) =
+fun dynamic_computation_text mounted_serializer prepared_program syms all_public ((vs, ty), t) =
   let
     val _ = if Code_Thingol.contains_dict_var t then
       error "Term to be evaluated contains free dictionaries" else ();
@@ -413,11 +413,11 @@
     val value_name = the (deresolve Code_Symbol.value);
   in (program_code, value_name) end;
 
-fun evaluator ctxt target_name program syms =
+fun computation_text ctxt target_name program syms =
   let
     val (mounted_serializer, (_, prepared_program)) =
       mount_serializer ctxt target_name NONE generatedN [] program syms;
-  in subevaluator mounted_serializer prepared_program syms end;
+  in dynamic_computation_text mounted_serializer prepared_program syms end;
 
 end; (* local *)
 
diff -r 3cb84e4469a7 -r 65a81a4ef7f8 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Thu May 26 15:27:50 2016 +0200
+++ b/src/Tools/Code/code_thingol.ML	Thu May 26 15:27:50 2016 +0200
@@ -839,49 +839,59 @@
     #> term_value
   end;
 
-fun dynamic_evaluator ctxt evaluator algebra eqngr t =
+fun dynamic_evaluation eval ctxt algebra eqngr t =
   let
     val ((program, (vs_ty_t', deps)), _) =
-      invoke_generation false (Proof_Context.theory_of ctxt) (algebra, eqngr) ensure_value t;
-  in evaluator program t vs_ty_t' deps end;
+      invoke_generation false (Proof_Context.theory_of ctxt)
+        (algebra, eqngr) ensure_value t;
+  in eval program t vs_ty_t' deps end;
 
 fun dynamic_conv ctxt conv =
-  Code_Preproc.dynamic_conv ctxt (dynamic_evaluator ctxt (fn program => fn _ => conv program));
-
-fun dynamic_value ctxt postproc evaluator =
-  Code_Preproc.dynamic_value ctxt postproc (dynamic_evaluator ctxt evaluator);
+  Code_Preproc.dynamic_conv ctxt
+    (dynamic_evaluation (fn program => fn _ => conv program) ctxt);
 
-fun static_subevaluator ctxt subevaluator algebra eqngr program t =
-  let
-    val ((_, ((vs_ty', t'), deps)), _) =
-      ensure_value ctxt algebra eqngr t ([], program);
-  in subevaluator ctxt t (vs_ty', t') deps end;
+fun dynamic_value ctxt postproc comp =
+  Code_Preproc.dynamic_value ctxt postproc
+    (dynamic_evaluation comp ctxt);
 
-fun static_evaluator_thingol ctxt evaluator consts { algebra, eqngr } =
+fun static_evaluation ctxt consts algebra eqngr static_eval =
   let
     fun generate_consts ctxt algebra eqngr =
       fold_map (ensure_const ctxt algebra eqngr false);
     val (deps, program) =
-      invoke_generation true (Proof_Context.theory_of ctxt) (algebra, eqngr) generate_consts consts;
-    val subevaluator = evaluator { program = program, deps = deps };
-  in fn ctxt' => static_subevaluator ctxt' subevaluator algebra eqngr program end;
+      invoke_generation true (Proof_Context.theory_of ctxt)
+        (algebra, eqngr) generate_consts consts;
+  in static_eval { program = program, deps = deps } end;
 
-fun static_evaluator_isa ctxt evaluator consts { algebra, eqngr } =
+fun static_evaluation_thingol ctxt consts algebra eqngr static_eval =
   let
-    fun generate_consts ctxt algebra eqngr =
-      fold_map (ensure_const ctxt algebra eqngr false);
-    val (_, program) =
-      invoke_generation true (Proof_Context.theory_of ctxt) (algebra, eqngr) generate_consts consts;
-  in evaluator (program: program) end;
+    fun evaluation' program dynamic_eval ctxt t =
+      let
+        val ((_, ((vs_ty', t'), deps)), _) =
+          ensure_value ctxt algebra eqngr t ([], program);
+      in dynamic_eval ctxt t (vs_ty', t') deps end;
+    fun evaluation static_eval { program, deps } =
+      evaluation' program (static_eval { program = program, deps = deps });
+  in
+    static_evaluation ctxt consts algebra eqngr
+      (evaluation static_eval)
+  end;
+
+fun static_evaluation_isa ctxt consts algebra eqngr static_eval =
+  static_evaluation ctxt consts algebra eqngr
+    (fn { program, ... } => static_eval (program: program));
 
 fun static_conv_thingol (ctxt_consts as { ctxt, consts }) conv =
-  Code_Preproc.static_conv ctxt_consts (static_evaluator_thingol ctxt (K oo conv) consts);
+  Code_Preproc.static_conv ctxt_consts (fn { algebra, eqngr } =>
+    static_evaluation_thingol ctxt consts algebra eqngr (K oo conv));
 
 fun static_conv_isa (ctxt_consts as { ctxt, consts }) conv =
-  Code_Preproc.static_conv ctxt_consts (static_evaluator_isa ctxt conv consts);
+  Code_Preproc.static_conv ctxt_consts (fn { algebra, eqngr } =>
+    static_evaluation_isa ctxt consts algebra eqngr conv);
 
-fun static_value (ctxt_postproc_consts as { ctxt, consts, ... }) evaluator =
-  Code_Preproc.static_value ctxt_postproc_consts (static_evaluator_thingol ctxt evaluator consts);
+fun static_value (ctxt_postproc_consts as { ctxt, consts, ... }) comp =
+  Code_Preproc.static_value ctxt_postproc_consts (fn { algebra, eqngr } =>
+    static_evaluation_thingol ctxt consts algebra eqngr comp);
 
 
 (** constant expressions **)
diff -r 3cb84e4469a7 -r 65a81a4ef7f8 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Thu May 26 15:27:50 2016 +0200
+++ b/src/Tools/nbe.ML	Thu May 26 15:27:50 2016 +0200
@@ -487,9 +487,9 @@
   end;
 
 
-(** evaluation **)
+(** normalization **)
 
-(* term evaluation by compilation *)
+(* term normalization by compilation *)
 
 fun compile_term ctxt nbe_program deps (vs : (string * sort) list, t) =
   let 
@@ -537,9 +537,9 @@
   in of_univ 0 t 0 |> fst end;
 
 
-(* evaluation with type reconstruction *)
+(* normalize with type reconstruction *)
 
-fun eval_term (nbe_program, idx_tab) raw_ctxt t_original ((vs, ty) : typscheme, t) deps =
+fun normalize (nbe_program, idx_tab) raw_ctxt t_original ((vs, ty) : typscheme, t) deps =
   let
     val ctxt = Syntax.init_pretty_global (Proof_Context.theory_of raw_ctxt);
     val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
@@ -591,27 +591,29 @@
 val (_, raw_oracle) = Context.>>> (Context.map_theory_result
   (Thm.add_oracle (@{binding normalization_by_evaluation},
     fn (nbe_program_idx_tab, ctxt, vs_ty_t, deps, ct) =>
-      mk_equals ctxt ct (eval_term nbe_program_idx_tab ctxt (Thm.term_of ct) vs_ty_t deps))));
+      mk_equals ctxt ct (normalize nbe_program_idx_tab ctxt (Thm.term_of ct) vs_ty_t deps))));
 
 fun oracle nbe_program_idx_tab ctxt vs_ty_t deps ct =
   raw_oracle (nbe_program_idx_tab, ctxt, vs_ty_t, deps, ct);
 
 fun dynamic_conv ctxt = lift_triv_classes_conv ctxt
-  (Code_Thingol.dynamic_conv ctxt (fn program => oracle (compile false ctxt program) ctxt));
+  (Code_Thingol.dynamic_conv ctxt (fn program =>
+    oracle (compile false ctxt program) ctxt));
 
 fun dynamic_value ctxt = lift_triv_classes_rew ctxt
-  (Code_Thingol.dynamic_value ctxt I (fn program => eval_term (compile false ctxt program) ctxt));
+  (Code_Thingol.dynamic_value ctxt I (fn program =>
+    normalize (compile false ctxt program) ctxt));
 
 fun static_conv (ctxt_consts as { ctxt, ... }) =
   let
-    val evaluator = Code_Thingol.static_conv_thingol ctxt_consts
+    val conv = Code_Thingol.static_conv_thingol ctxt_consts
       (fn { program, ... } => oracle (compile true ctxt program));
-  in fn ctxt' => lift_triv_classes_conv ctxt' (evaluator ctxt') end;
+  in fn ctxt' => lift_triv_classes_conv ctxt' (conv ctxt') end;
 
 fun static_value { ctxt, consts } =
   let
-    val evaluator = Code_Thingol.static_value { ctxt = ctxt, lift_postproc = I, consts = consts }
-      (fn { program, ... } => eval_term (compile false ctxt program));
-  in fn ctxt' => lift_triv_classes_rew ctxt' (evaluator ctxt') end;
+    val comp = Code_Thingol.static_value { ctxt = ctxt, lift_postproc = I, consts = consts }
+      (fn { program, ... } => normalize (compile false ctxt program));
+  in fn ctxt' => lift_triv_classes_rew ctxt' (comp ctxt') end;
 
 end;