refined and unified naming convention for dynamic code evaluation techniques

--- a/src/HOL/HOL.thy	Mon Aug 23 11:09:48 2010 +0200
+++ b/src/HOL/HOL.thy	Mon Aug 23 11:09:49 2010 +0200
@@ -1998,7 +1998,7 @@
   "solve goal by evaluation"
 
 method_setup normalization = {*
-  Scan.succeed (K (SIMPLE_METHOD' (CONVERSION Nbe.norm_conv THEN' (fn k => TRY (rtac TrueI k)))))
+  Scan.succeed (K (SIMPLE_METHOD' (CONVERSION Nbe.dynamic_eval_conv THEN' (fn k => TRY (rtac TrueI k)))))
 *} "solve goal by normalization"
 
 

--- a/src/Tools/Code/code_eval.ML	Mon Aug 23 11:09:48 2010 +0200
+++ b/src/Tools/Code/code_eval.ML	Mon Aug 23 11:09:49 2010 +0200
@@ -62,7 +62,7 @@
         val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name'
           ^ space_implode " " (map (enclose "(" ")") args) ^ " end";
       in ML_Context.evaluate ctxt false reff sml_code end;
-  in Code_Thingol.eval thy postproc evaluator t end;
+  in Code_Thingol.dynamic_eval_value thy postproc evaluator t end;
 
 
 (** instrumentalization by antiquotation **)

--- a/src/Tools/Code/code_preproc.ML	Mon Aug 23 11:09:48 2010 +0200
+++ b/src/Tools/Code/code_preproc.ML	Mon Aug 23 11:09:49 2010 +0200
@@ -24,9 +24,9 @@
   val all: code_graph -> string list
   val pretty: theory -> code_graph -> Pretty.T
   val obtain: theory -> string list -> term list -> code_algebra * code_graph
-  val eval_conv: theory
+  val dynamic_eval_conv: theory
     -> (code_algebra -> code_graph -> (string * sort) list -> term -> cterm -> thm) -> cterm -> thm
-  val eval: theory -> ((term -> term) -> 'a -> 'a)
+  val dynamic_eval_value: theory -> ((term -> term) -> 'a -> 'a)
     -> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a
   val pre_post_conv: theory -> (cterm -> thm) -> cterm -> thm
 
@@ -74,8 +74,7 @@
   if AList.defined (op =) xs key then AList.delete (op =) key xs
   else error ("No such " ^ msg ^ ": " ^ quote key);
 
-fun map_data f = Code.purge_data
-  #> (Code_Preproc_Data.map o map_thmproc) f;
+val map_data = Code_Preproc_Data.map o map_thmproc;
 
 val map_pre_post = map_data o apfst;
 val map_pre = map_pre_post o apfst;
@@ -425,7 +424,7 @@
 fun obtain thy cs ts = apsnd snd
   (Wellsorted.change_yield thy (extend_arities_eqngr thy cs ts));
 
-fun gen_eval thy cterm_of conclude_evaluation evaluator proto_ct =
+fun dynamic_eval thy cterm_of conclude_evaluation evaluator proto_ct =
   let
     val pp = Syntax.pp_global thy;
     val ct = cterm_of proto_ct;
@@ -440,10 +439,7 @@
     val (algebra', eqngr') = obtain thy consts [t'];
   in conclude_evaluation (evaluator algebra' eqngr' vs t' ct') thm end;
 
-fun simple_evaluator evaluator algebra eqngr vs t ct =
-  evaluator algebra eqngr vs t;
-
-fun eval_conv thy =
+fun dynamic_eval_conv thy =
   let
     fun conclude_evaluation thm2 thm1 =
       let
@@ -453,10 +449,10 @@
           error ("could not construct evaluation proof:\n"
           ^ (cat_lines o map (Display.string_of_thm_global thy)) [thm1, thm2, thm3])
       end;
-  in gen_eval thy I conclude_evaluation end;
+  in dynamic_eval thy I conclude_evaluation end;
 
-fun eval thy postproc evaluator = gen_eval thy (Thm.cterm_of thy)
-  (K o postproc (postprocess_term thy)) (simple_evaluator evaluator);
+fun dynamic_eval_value thy postproc evaluator = dynamic_eval thy (Thm.cterm_of thy)
+  (K o postproc (postprocess_term thy)) (K oooo evaluator);
 
 fun pre_post_conv thy conv = (preprocess_conv thy) then_conv conv then_conv (postprocess_conv thy);
 

--- a/src/Tools/Code/code_simp.ML	Mon Aug 23 11:09:48 2010 +0200
+++ b/src/Tools/Code/code_simp.ML	Mon Aug 23 11:09:49 2010 +0200
@@ -8,11 +8,11 @@
 sig
   val no_frees_conv: conv -> conv
   val map_ss: (simpset -> simpset) -> theory -> theory
-  val current_conv: theory -> conv
-  val current_tac: theory -> int -> tactic
-  val current_value: theory -> term -> term
-  val make_conv: theory -> simpset option -> string list -> conv
-  val make_tac: theory -> simpset option -> string list -> int -> tactic
+  val dynamic_eval_conv: theory -> conv
+  val dynamic_eval_tac: theory -> int -> tactic
+  val dynamic_eval_value: theory -> term -> term
+  val static_eval_conv: theory -> simpset option -> string list -> conv
+  val static_eval_tac: theory -> simpset option -> string list -> int -> tactic
   val setup: theory -> theory
 end;
 
@@ -67,25 +67,25 @@
 
 (* evaluation with current code context *)
 
-fun current_conv thy = no_frees_conv (Code_Thingol.eval_conv thy
+fun dynamic_eval_conv thy = no_frees_conv (Code_Thingol.dynamic_eval_conv thy
   (fn naming => fn program => fn t => fn deps => rewrite_modulo thy NONE program));
 
-fun current_tac thy = CONVERSION (current_conv thy) THEN' conclude_tac thy NONE;
+fun dynamic_eval_tac thy = CONVERSION (dynamic_eval_conv thy) THEN' conclude_tac thy NONE;
 
-fun current_value thy = snd o Logic.dest_equals o Thm.prop_of o current_conv thy o Thm.cterm_of thy;
+fun dynamic_eval_value thy = snd o Logic.dest_equals o Thm.prop_of o dynamic_eval_conv thy o Thm.cterm_of thy;
 
 val setup = Method.setup (Binding.name "code_simp")
-  (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo current_tac o ProofContext.theory_of)))
+  (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_eval_tac o ProofContext.theory_of)))
   "simplification with code equations"
-  #> Value.add_evaluator ("simp", current_value o ProofContext.theory_of);
+  #> Value.add_evaluator ("simp", dynamic_eval_value o ProofContext.theory_of);
 
 
 (* evaluation with freezed code context *)
 
-fun make_conv thy some_ss consts = no_frees_conv (Code_Preproc.pre_post_conv thy
+fun static_eval_conv thy some_ss consts = no_frees_conv (Code_Preproc.pre_post_conv thy
   ((rewrite_modulo thy some_ss o snd o snd o Code_Thingol.consts_program thy false) consts));
 
-fun make_tac thy some_ss consts = CONVERSION (make_conv thy some_ss consts)
+fun static_eval_tac thy some_ss consts = CONVERSION (static_eval_conv thy some_ss consts)
   THEN' conclude_tac thy some_ss;
 
 end;

--- a/src/Tools/Code/code_thingol.ML	Mon Aug 23 11:09:48 2010 +0200
+++ b/src/Tools/Code/code_thingol.ML	Mon Aug 23 11:09:49 2010 +0200
@@ -92,10 +92,10 @@
 
   val read_const_exprs: theory -> string list -> string list * string list
   val consts_program: theory -> bool -> string list -> string list * (naming * program)
-  val eval_conv: theory
+  val dynamic_eval_conv: theory
     -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> cterm -> thm)
     -> cterm -> thm
-  val eval: theory -> ((term -> term) -> 'a -> 'a)
+  val dynamic_eval_value: theory -> ((term -> term) -> 'a -> 'a)
     -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
     -> term -> 'a
 end;
@@ -895,8 +895,8 @@
     val vs'' = map (fn (v, _) => (v, (the o AList.lookup (op =) vs o prefix "'") v)) vs';
   in evaluator naming program ((vs'', (vs', ty')), t') deps end;
 
-fun eval_conv thy = Code_Preproc.eval_conv thy o base_evaluator thy;
-fun eval thy postproc = Code_Preproc.eval thy postproc o base_evaluator thy;
+fun dynamic_eval_conv thy = Code_Preproc.dynamic_eval_conv thy o base_evaluator thy;
+fun dynamic_eval_value thy postproc = Code_Preproc.dynamic_eval_value thy postproc o base_evaluator thy;
 
 
 (** diagnostic commands **)

--- a/src/Tools/nbe.ML	Mon Aug 23 11:09:48 2010 +0200
+++ b/src/Tools/nbe.ML	Mon Aug 23 11:09:49 2010 +0200
@@ -6,8 +6,8 @@
 
 signature NBE =
 sig
-  val norm_conv: cterm -> thm
-  val norm: theory -> term -> term
+  val dynamic_eval_conv: cterm -> thm
+  val dynamic_eval_value: theory -> term -> term
 
   datatype Univ =
       Const of int * Univ list               (*named (uninterpreted) constants*)
@@ -574,12 +574,11 @@
     val rhs = Thm.cterm_of thy raw_rhs;
   in Thm.mk_binop eq lhs rhs end;
 
-val (_, raw_norm_oracle) = Context.>>> (Context.map_theory_result
+val (_, raw_oracle) = Context.>>> (Context.map_theory_result
   (Thm.add_oracle (Binding.name "norm", fn (thy, program, vsp_ty_t, deps, ct) =>
     mk_equals thy ct (normalize thy program vsp_ty_t deps))));
 
-fun norm_oracle thy program vsp_ty_t deps ct =
-  raw_norm_oracle (thy, program, vsp_ty_t, deps, ct);
+fun oracle thy program vsp_ty_t deps ct = raw_oracle (thy, program, vsp_ty_t, deps, ct);
 
 fun no_frees_rew rew t =
   let
@@ -591,12 +590,11 @@
     |> (fn t' => Term.betapplys (t', frees))
   end;
 
-val norm_conv = Code_Simp.no_frees_conv (fn ct =>
-  let
-    val thy = Thm.theory_of_cterm ct;
-  in lift_triv_classes_conv thy (Code_Thingol.eval_conv thy (K (norm_oracle thy))) ct end);
+val dynamic_eval_conv = Code_Simp.no_frees_conv (Conv.tap_thy
+  (fn thy => lift_triv_classes_conv thy (Code_Thingol.dynamic_eval_conv thy (K (oracle thy)))));
 
-fun norm thy = lift_triv_classes_rew thy (no_frees_rew (Code_Thingol.eval thy I (K (normalize thy))));
+fun dynamic_eval_value thy = lift_triv_classes_rew thy
+  (no_frees_rew (Code_Thingol.dynamic_eval_value thy I (K (normalize thy))));
 
 
 (* evaluation command *)
@@ -604,7 +602,7 @@
 fun norm_print_term ctxt modes t =
   let
     val thy = ProofContext.theory_of ctxt;
-    val t' = norm thy t;
+    val t' = dynamic_eval_value thy t;
     val ty' = Term.type_of t';
     val ctxt' = Variable.auto_fixes t ctxt;
     val p = Print_Mode.with_modes modes (fn () =>
@@ -619,7 +617,7 @@
   let val ctxt = Toplevel.context_of state
   in norm_print_term ctxt modes (Syntax.read_term ctxt s) end;
 
-val setup = Value.add_evaluator ("nbe", norm o ProofContext.theory_of);
+val setup = Value.add_evaluator ("nbe", dynamic_eval_value o ProofContext.theory_of);
 
 val opt_modes =
   Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.xname --| Parse.$$$ ")")) [];