generic postprocessing scheme for term evaluations

--- a/src/HOL/Code_Eval.thy	Fri Apr 24 08:24:52 2009 +0200
+++ b/src/HOL/Code_Eval.thy	Fri Apr 24 08:24:54 2009 +0200
@@ -161,6 +161,7 @@
 signature EVAL =
 sig
   val mk_term: ((string * typ) -> term) -> (typ -> term) -> term -> term
+  val mk_term_of: typ -> term -> term
   val eval_ref: (unit -> term) option ref
   val eval_term: theory -> term -> term
 end;
@@ -175,7 +176,7 @@
 fun eval_term thy t =
   t 
   |> Eval.mk_term_of (fastype_of t)
-  |> (fn t => Code_ML.eval_term NONE ("Eval.eval_ref", eval_ref) thy t []);
+  |> (fn t => Code_ML.eval NONE ("Eval.eval_ref", eval_ref) I thy t []);
 
 end;
 *}

--- a/src/HOL/HOL.thy	Fri Apr 24 08:24:52 2009 +0200
+++ b/src/HOL/HOL.thy	Fri Apr 24 08:24:54 2009 +0200
@@ -1889,7 +1889,7 @@
     val dummy = @{cprop True};
   in case try HOLogic.dest_Trueprop t
    of SOME t' => if Code_ML.eval NONE
-         ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy t' [] 
+         ("Eval_Method.eval_ref", Eval_Method.eval_ref) (K I) thy t' [] 
        then Thm.capply (Thm.capply @{cterm "op \<equiv> \<Colon> prop \<Rightarrow> prop \<Rightarrow> prop"} ct) dummy
        else dummy
     | NONE => dummy

--- a/src/HOL/Library/Eval_Witness.thy	Fri Apr 24 08:24:52 2009 +0200
+++ b/src/HOL/Library/Eval_Witness.thy	Fri Apr 24 08:24:54 2009 +0200
@@ -68,7 +68,7 @@
     | dest_exs _ _ = sys_error "dest_exs";
   val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal);
 in
-  if Code_ML.eval NONE ("Eval_Witness_Method.eval_ref", Eval_Witness_Method.eval_ref) thy t ws
+  if Code_ML.eval NONE ("Eval_Witness_Method.eval_ref", Eval_Witness_Method.eval_ref) (K I) thy t ws
   then Thm.cterm_of thy goal
   else @{cprop True} (*dummy*)
 end

--- a/src/HOL/Library/Quickcheck.thy	Fri Apr 24 08:24:52 2009 +0200
+++ b/src/HOL/Library/Quickcheck.thy	Fri Apr 24 08:24:54 2009 +0200
@@ -74,8 +74,9 @@
   let
     val tys = (map snd o fst o strip_abs) t;
     val t' = mk_generator_expr thy t tys;
-    val f = Code_ML.eval (SOME target) ("Quickcheck.eval_ref", eval_ref) thy t' [];
-  in f #> Random_Engine.run #> (Option.map o map) (Code.postprocess_term thy) end;
+    val f = Code_ML.eval (SOME target) ("Quickcheck.eval_ref", eval_ref)
+      (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) thy t' [];
+  in f #> Random_Engine.run end;
 
 end
 *}

--- a/src/Tools/code/code_ml.ML	Fri Apr 24 08:24:52 2009 +0200
+++ b/src/Tools/code/code_ml.ML	Fri Apr 24 08:24:54 2009 +0200
@@ -6,10 +6,8 @@
 
 signature CODE_ML =
 sig
-  val eval_term: string option -> string * (unit -> term) option ref
-    -> theory -> term -> string list -> term
   val eval: string option -> string * (unit -> 'a) option ref
-    -> theory -> term -> string list -> 'a
+    -> ((term -> term) -> 'a -> 'a) -> theory -> term -> string list -> 'a
   val target_Eval: string
   val setup: theory -> theory
 end;
@@ -957,7 +955,7 @@
 
 (* evaluation *)
 
-fun gen_eval eval some_target reff thy t args =
+fun eval some_target reff postproc thy t args =
   let
     val ctxt = ProofContext.init thy;
     val _ = if null (Term.add_frees t []) then () else error ("Term "
@@ -976,10 +974,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 eval thy I evaluator t end;
-
-fun eval_term thy = gen_eval Code_Thingol.eval_term thy;
-fun eval thy = gen_eval Code_Thingol.eval thy;
+  in Code_Thingol.eval thy I postproc evaluator t end;
 
 
 (* instrumentalization by antiquotation *)

--- a/src/Tools/code/code_thingol.ML	Fri Apr 24 08:24:52 2009 +0200
+++ b/src/Tools/code/code_thingol.ML	Fri Apr 24 08:24:54 2009 +0200
@@ -86,10 +86,7 @@
   val eval_conv: theory -> (sort -> sort)
     -> (naming -> program -> (((string * sort) list * typscheme) * (string * itype) list) * iterm -> string list -> cterm -> thm)
     -> cterm -> thm
-  val eval_term: theory -> (sort -> sort)
-    -> (naming -> program -> (((string * sort) list * typscheme) * (string * itype) list) * iterm -> string list -> term)
-    -> term -> term
-  val eval: theory -> (sort -> sort)
+  val eval: theory -> (sort -> sort) -> ((term -> term) -> 'a -> 'a)
     -> (naming -> program -> (((string * sort) list * typscheme) * (string * itype) list) * iterm -> string list -> 'a)
     -> term -> 'a
 end;
@@ -780,8 +777,7 @@
   in evaluator naming program (((vs'', (vs', ty')), fs'), t') deps end;
 
 fun eval_conv thy prep_sort = Code_Wellsorted.eval_conv thy prep_sort o base_evaluator thy;
-fun eval_term thy prep_sort = Code_Wellsorted.eval_term thy prep_sort o base_evaluator thy;
-fun eval thy prep_sort = Code_Wellsorted.eval thy prep_sort o base_evaluator thy;
+fun eval thy prep_sort postproc = Code_Wellsorted.eval thy prep_sort postproc o base_evaluator thy;
 
 
 (** diagnostic commands **)

--- a/src/Tools/code/code_wellsorted.ML	Fri Apr 24 08:24:52 2009 +0200
+++ b/src/Tools/code/code_wellsorted.ML	Fri Apr 24 08:24:54 2009 +0200
@@ -16,9 +16,7 @@
   val obtain: theory -> string list -> term list -> code_algebra * code_graph
   val eval_conv: theory -> (sort -> sort)
     -> (code_algebra -> code_graph -> (string * sort) list -> term -> cterm -> thm) -> cterm -> thm
-  val eval_term: theory -> (sort -> sort)
-    -> (code_algebra -> code_graph -> (string * sort) list -> term -> term) -> term -> term
-  val eval: theory -> (sort -> sort)
+  val eval: theory -> (sort -> sort) -> ((term -> term) -> 'a -> 'a)
     -> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a
 end
 
@@ -334,10 +332,7 @@
       end;
   in gen_eval thy I conclude_evaluation end;
 
-fun eval_term thy prep_sort evaluator = gen_eval thy (Thm.cterm_of thy)
-  (fn t => K (Code.postprocess_term thy t)) prep_sort (simple_evaluator evaluator);
-
-fun eval thy prep_sort evaluator = gen_eval thy (Thm.cterm_of thy)
-  (fn t => K t) prep_sort (simple_evaluator evaluator);
+fun eval thy prep_sort postproc evaluator = gen_eval thy (Thm.cterm_of thy)
+  (K o postproc (Code.postprocess_term thy)) prep_sort (simple_evaluator evaluator);
 
 end; (*struct*)

--- a/src/Tools/nbe.ML	Fri Apr 24 08:24:52 2009 +0200
+++ b/src/Tools/nbe.ML	Fri Apr 24 08:24:54 2009 +0200
@@ -7,7 +7,7 @@
 signature NBE =
 sig
   val norm_conv: cterm -> thm
-  val norm_term: theory -> term -> term
+  val norm: theory -> term -> term
 
   datatype Univ =
       Const of int * Univ list               (*named (uninterpreted) constants*)
@@ -440,7 +440,7 @@
 
 (* evaluation with type reconstruction *)
 
-fun norm thy naming program (((vs0, (vs, ty)), fs), t) deps =
+fun normalize thy naming program (((vs0, (vs, ty)), fs), t) deps =
   let
     fun subst_const f = map_aterms (fn t as Term.Const (c, ty) => Term.Const (f c, ty)
       | t => t);
@@ -483,7 +483,7 @@
 
 val (_, raw_norm_oracle) = Context.>>> (Context.map_theory_result
   (Thm.add_oracle (Binding.name "norm", fn (thy, naming, program, vsp_ty_fs_t, deps, ct) =>
-    mk_equals thy ct (norm thy naming program vsp_ty_fs_t deps))));
+    mk_equals thy ct (normalize thy naming program vsp_ty_fs_t deps))));
 
 fun norm_oracle thy naming program vsp_ty_fs_t deps ct =
   raw_norm_oracle (thy, naming, program, vsp_ty_fs_t, deps, ct);
@@ -493,15 +493,14 @@
     val thy = Thm.theory_of_cterm ct;
   in Code_Thingol.eval_conv thy (add_triv_classes thy) (norm_oracle thy) ct end;
 
-fun norm_term thy = Code.postprocess_term thy
-  o Code_Thingol.eval_term thy (add_triv_classes thy) (norm thy);
+fun norm thy = Code_Thingol.eval thy (add_triv_classes thy) I (normalize thy);
 
 (* evaluation command *)
 
 fun norm_print_term ctxt modes t =
   let
     val thy = ProofContext.theory_of ctxt;
-    val t' = norm_term thy t;
+    val t' = norm thy t;
     val ty' = Term.type_of t';
     val ctxt' = Variable.auto_fixes t ctxt;
     val p = PrintMode.with_modes modes (fn () =>
@@ -516,8 +515,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_term o ProofContext.theory_of);
+val setup = Value.add_evaluator ("nbe", norm o ProofContext.theory_of);
 
 local structure P = OuterParse and K = OuterKeyword in