integrated add_triv_classes into evaluation stack

--- a/src/Tools/Code/code_ml.ML	Tue Jul 21 15:44:31 2009 +0200
+++ b/src/Tools/Code/code_ml.ML	Tue Jul 21 15:44:31 2009 +0200
@@ -966,7 +966,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 I postproc evaluator t end;
+  in Code_Thingol.eval thy postproc evaluator t end;
 
 
 (* instrumentalization by antiquotation *)

--- a/src/Tools/Code/code_preproc.ML	Tue Jul 21 15:44:31 2009 +0200
+++ b/src/Tools/Code/code_preproc.ML	Tue Jul 21 15:44:31 2009 +0200
@@ -23,9 +23,10 @@
   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 -> (sort -> sort)
+  val resubst_triv_consts: theory -> term -> term
+  val eval_conv: theory
     -> (code_algebra -> code_graph -> (string * sort) list -> term -> cterm -> thm) -> cterm -> thm
-  val eval: theory -> (sort -> sort) -> ((term -> term) -> 'a -> 'a)
+  val eval: theory -> ((term -> term) -> 'a -> 'a)
     -> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a
 
   val setup: theory -> theory
@@ -161,7 +162,10 @@
     |> rhs_conv (Simplifier.rewrite post)
   end;
 
-fun postprocess_term thy = term_of_conv thy (postprocess_conv thy);
+fun resubst_triv_consts thy = map_aterms (fn t as Const (c, ty) => Const (Code.resubst_alias thy c, ty)
+  | t => t);
+
+fun postprocess_term thy = term_of_conv thy (postprocess_conv thy) #> resubst_triv_consts thy;
 
 fun print_codeproc thy =
   let
@@ -495,7 +499,7 @@
       Abs (v, prepare_sorts_typ prep_sort ty, prepare_sorts prep_sort t)
   | prepare_sorts _ (t as Bound _) = t;
 
-fun gen_eval thy cterm_of conclude_evaluation prep_sort evaluator proto_ct =
+fun gen_eval thy cterm_of conclude_evaluation evaluator proto_ct =
   let
     val pp = Syntax.pp_global thy;
     val ct = cterm_of proto_ct;
@@ -507,8 +511,10 @@
     val vs = Term.add_tfrees t' [];
     val consts = fold_aterms
       (fn Const (c, _) => insert (op =) c | _ => I) t' [];
- 
-    val t'' = prepare_sorts prep_sort t';
+
+    val add_triv_classes = curry (Sorts.inter_sort (Sign.classes_of thy))
+      (Code.triv_classes thy);
+    val t'' = prepare_sorts add_triv_classes t';
     val (algebra', eqngr') = obtain thy consts [t''];
   in conclude_evaluation (evaluator algebra' eqngr' vs t'' ct') thm end;
 
@@ -527,8 +533,8 @@
       end;
   in gen_eval thy I conclude_evaluation end;
 
-fun eval thy prep_sort postproc evaluator = gen_eval thy (Thm.cterm_of thy)
-  (K o postproc (postprocess_term thy)) prep_sort (simple_evaluator evaluator);
+fun eval thy postproc evaluator = gen_eval thy (Thm.cterm_of thy)
+  (K o postproc (postprocess_term thy)) (simple_evaluator evaluator);
 
 
 (** setup **)

--- a/src/Tools/Code/code_thingol.ML	Tue Jul 21 15:44:31 2009 +0200
+++ b/src/Tools/Code/code_thingol.ML	Tue Jul 21 15:44:31 2009 +0200
@@ -82,10 +82,10 @@
   val read_const_exprs: theory -> string list -> string list * string list
   val consts_program: theory -> string list -> string list * (naming * program)
   val cached_program: theory -> naming * program
-  val eval_conv: theory -> (sort -> sort)
+  val eval_conv: theory
     -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> cterm -> thm)
     -> cterm -> thm
-  val eval: theory -> (sort -> sort) -> ((term -> term) -> 'a -> 'a)
+  val eval: theory -> ((term -> term) -> 'a -> 'a)
     -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
     -> term -> 'a
 end;
@@ -803,8 +803,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 prep_sort = Code_Preproc.eval_conv thy prep_sort o base_evaluator thy;
-fun eval thy prep_sort postproc = Code_Preproc.eval thy prep_sort postproc o base_evaluator thy;
+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;
 
 
 (** diagnostic commands **)

--- a/src/Tools/nbe.ML	Tue Jul 21 15:44:31 2009 +0200
+++ b/src/Tools/nbe.ML	Tue Jul 21 15:44:31 2009 +0200
@@ -439,9 +439,6 @@
 
 fun normalize thy naming program ((vs0, (vs, ty)), t) deps =
   let
-    fun subst_const f = map_aterms (fn t as Term.Const (c, ty) => Term.Const (f c, ty)
-      | t => t);
-    val resubst_triv_consts = subst_const (Code.resubst_alias thy);
     val ty' = typ_of_itype program vs0 ty;
     fun type_infer t =
       singleton (TypeInfer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I
@@ -453,8 +450,8 @@
     val string_of_term = setmp show_types true (Syntax.string_of_term_global thy);
   in
     compile_eval thy naming program (vs, t) deps
+    |> Code_Preproc.resubst_triv_consts thy
     |> tracing (fn t => "Normalized:\n" ^ string_of_term t)
-    |> resubst_triv_consts
     |> type_infer
     |> tracing (fn t => "Types inferred:\n" ^ string_of_term t)
     |> check_tvars
@@ -463,9 +460,6 @@
 
 (* evaluation oracle *)
 
-fun add_triv_classes thy = curry (Sorts.inter_sort (Sign.classes_of thy))
-  (Code.triv_classes thy);
-
 fun mk_equals thy lhs raw_rhs =
   let
     val ty = Thm.typ_of (Thm.ctyp_of_term lhs);
@@ -506,9 +500,9 @@
 val norm_conv = no_frees_conv (fn ct =>
   let
     val thy = Thm.theory_of_cterm ct;
-  in Code_Thingol.eval_conv thy (add_triv_classes thy) (norm_oracle thy) ct end);
+  in Code_Thingol.eval_conv thy (norm_oracle thy) ct end);
 
-fun norm thy = no_frees_rew (Code_Thingol.eval thy (add_triv_classes thy) I (normalize thy));
+fun norm thy = no_frees_rew (Code_Thingol.eval thy I (normalize thy));
 
 (* evaluation command *)