merged

--- a/src/HOL/HOL.thy	Tue Aug 24 08:22:17 2010 +0200
+++ b/src/HOL/HOL.thy	Tue Aug 24 10:07:14 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/Pure/Isar/code.ML	Tue Aug 24 08:22:17 2010 +0200
+++ b/src/Pure/Isar/code.ML	Tue Aug 24 10:07:14 2010 +0200
@@ -78,7 +78,6 @@
 
   (*infrastructure*)
   val set_code_target_attr: (string -> thm -> theory -> theory) -> theory -> theory
-  val purge_data: theory -> theory
 end;
 
 signature CODE_DATA_ARGS =
@@ -266,8 +265,6 @@
 
 fun map_exec_purge f = Code_Data.map (fn (exec, _) => (f exec, empty_dataref ()));
 
-val purge_data = (Code_Data.map o apsnd) (fn _ => empty_dataref ());
-
 fun change_fun_spec delete c f = (map_exec_purge o map_functions
   o (if delete then Symtab.map_entry c else Symtab.map_default (c, ((false, empty_fun_spec), [])))
     o apfst) (fn (_, spec) => (true, f spec));

--- a/src/Pure/conv.ML	Tue Aug 24 08:22:17 2010 +0200
+++ b/src/Pure/conv.ML	Tue Aug 24 10:07:14 2010 +0200
@@ -48,6 +48,7 @@
   val concl_conv: int -> conv -> conv
   val fconv_rule: conv -> thm -> thm
   val gconv_rule: conv -> int -> thm -> thm
+  val tap_thy: (theory -> conv) -> conv
 end;
 
 structure Conv: CONV =
@@ -211,6 +212,9 @@
       end
   | NONE => raise THM ("gconv_rule", i, [th]));
 
+
+fun tap_thy conv ct = conv (Thm.theory_of_cterm ct) ct;
+
 end;
 
 structure Basic_Conv: BASIC_CONV = Conv;

--- a/src/Tools/Code/code_eval.ML	Tue Aug 24 08:22:17 2010 +0200
+++ b/src/Tools/Code/code_eval.ML	Tue Aug 24 10:07:14 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	Tue Aug 24 08:22:17 2010 +0200
+++ b/src/Tools/Code/code_preproc.ML	Tue Aug 24 10:07:14 2010 +0200
@@ -24,11 +24,12 @@
   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
-    -> (code_algebra -> code_graph -> (string * sort) list -> term -> cterm -> thm) -> cterm -> thm
-  val eval: theory -> ((term -> term) -> 'a -> 'a)
+  val dynamic_eval_conv: theory
+    -> (code_algebra -> code_graph -> (string * sort) list -> term -> conv) -> conv
+  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
+  val static_eval_conv: theory -> string list
+    -> (code_algebra -> code_graph -> (string * sort) list -> term -> conv) -> conv
 
   val setup: theory -> theory
 end
@@ -74,8 +75,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;
@@ -422,10 +422,12 @@
 
 (** retrieval and evaluation interfaces **)
 
-fun obtain thy cs ts = apsnd snd
-  (Wellsorted.change_yield thy (extend_arities_eqngr thy cs ts));
+fun obtain thy consts ts = apsnd snd
+  (Wellsorted.change_yield thy (extend_arities_eqngr thy consts ts));
 
-fun gen_eval thy cterm_of conclude_evaluation evaluator proto_ct =
+fun dest_cterm ct = let val t = Thm.term_of ct in (Term.add_tfrees t [], t) end;
+
+fun dynamic_eval thy cterm_of conclude_evaluation evaluator proto_ct =
   let
     val pp = Syntax.pp_global thy;
     val ct = cterm_of proto_ct;
@@ -433,17 +435,13 @@
       (Thm.term_of ct);
     val thm = preprocess_conv thy ct;
     val ct' = Thm.rhs_of thm;
-    val t' = Thm.term_of ct';
-    val vs = Term.add_tfrees t' [];
+    val (vs', t') = dest_cterm ct';
     val consts = fold_aterms
       (fn Const (c, _) => insert (op =) c | _ => I) t' [];
     val (algebra', eqngr') = obtain thy consts [t'];
-  in conclude_evaluation (evaluator algebra' eqngr' vs t' ct') thm end;
+  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,12 +451,22 @@
           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 dynamic_eval_value thy postproc evaluator = dynamic_eval thy (Thm.cterm_of thy)
+  (K o postproc (postprocess_term thy)) (K oooo evaluator);
 
-fun eval thy postproc evaluator = gen_eval thy (Thm.cterm_of thy)
-  (K o postproc (postprocess_term thy)) (simple_evaluator evaluator);
-
-fun pre_post_conv thy conv = (preprocess_conv thy) then_conv conv then_conv (postprocess_conv thy);
+fun static_eval_conv thy consts conv =
+  let
+    val (algebra, eqngr) = obtain thy consts [];
+    fun conv' ct =
+      let
+        val (vs, t) = dest_cterm ct;
+      in
+        Conv.tap_thy (fn thy => (preprocess_conv thy)
+          then_conv (conv algebra eqngr vs t) then_conv (postprocess_conv thy)) ct
+      end;
+  in conv' end;
 
 
 (** setup **)

--- a/src/Tools/Code/code_simp.ML	Tue Aug 24 08:22:17 2010 +0200
+++ b/src/Tools/Code/code_simp.ML	Tue Aug 24 10:07:14 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
-  ((rewrite_modulo thy some_ss o snd o snd o Code_Thingol.consts_program thy false) consts));
+fun static_eval_conv thy some_ss consts = no_frees_conv
+  (Code_Thingol.static_eval_conv_simple thy consts (rewrite_modulo thy some_ss));
 
-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	Tue Aug 24 08:22:17 2010 +0200
+++ b/src/Tools/Code/code_thingol.ML	Tue Aug 24 10:07:14 2010 +0200
@@ -92,12 +92,17 @@
 
   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
-    -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> cterm -> thm)
-    -> cterm -> thm
-  val eval: theory -> ((term -> term) -> 'a -> 'a)
+  val dynamic_eval_conv: theory
+    -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> conv)
+    -> conv
+  val dynamic_eval_value: theory -> ((term -> term) -> 'a -> 'a)
     -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
     -> term -> 'a
+  val static_eval_conv: theory -> string list
+    -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> conv)
+    -> conv
+  val static_eval_conv_simple: theory -> string list
+    -> (program -> conv) -> conv
 end;
 
 structure Code_Thingol: CODE_THINGOL =
@@ -846,7 +851,7 @@
 
 fun consts_program thy permissive cs =
   let
-    fun project_consts cs (naming, program) =
+    fun project_consts cs (naming, program) = (*FIXME only necessary for cache_generation*)
       let
         val cs_all = Graph.all_succs program cs;
       in (cs, (naming, Graph.subgraph (member (op =) cs_all) program)) end;
@@ -895,8 +900,17 @@
     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;
+
+fun static_eval_conv thy consts conv =
+  Code_Preproc.static_eval_conv thy consts (base_evaluator thy conv); (*FIXME avoid re-generation*)
+
+fun static_eval_conv_simple thy consts conv =
+  Code_Preproc.static_eval_conv thy consts (fn algebra => fn eqngr => fn _ => fn _ => fn ct =>
+    conv ((NONE, (empty_naming, Graph.empty)) (*FIXME provide abstraction for this kind of invocation*)
+      |> fold_map (ensure_const thy algebra eqngr false) consts
+      |> (snd o snd o snd)) ct);
 
 
 (** diagnostic commands **)

--- a/src/Tools/nbe.ML	Tue Aug 24 08:22:17 2010 +0200
+++ b/src/Tools/nbe.ML	Tue Aug 24 10:07:14 2010 +0200
@@ -6,8 +6,8 @@
 
 signature NBE =
 sig
-  val norm_conv: cterm -> thm
-  val norm: theory -> term -> term
+  val dynamic_eval_conv: conv
+  val dynamic_eval_value: theory -> term -> term
 
   datatype Univ =
       Const of int * Univ list               (*named (uninterpreted) constants*)
@@ -530,12 +530,12 @@
 
 (* compilation, evaluation and reification *)
 
-fun compile_eval thy program vs_t deps =
+fun compile_eval thy program =
   let
     val ctxt = ProofContext.init_global thy;
     val (gr, (_, idx_tab)) =
       Nbe_Functions.change thy (ensure_stmts ctxt program);
-  in
+  in fn vs_t => fn deps =>
     vs_t
     |> eval_term ctxt gr deps
     |> term_of_univ thy program idx_tab
@@ -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
@@ -588,15 +587,14 @@
     t
     |> fold_rev lambda frees
     |> rew
-    |> (fn t' => Term.betapplys (t', frees))
+    |> curry (Term.betapplys o swap) 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.$$$ ")")) [];