re-engineering of evaluation conversions

--- a/src/HOL/Code_Eval.thy	Fri Apr 17 14:29:55 2009 +0200
+++ b/src/HOL/Code_Eval.thy	Fri Apr 17 14:29:56 2009 +0200
@@ -175,8 +175,7 @@
 fun eval_term thy t =
   t 
   |> Eval.mk_term_of (fastype_of t)
-  |> (fn t => Code_ML.eval_term ("Eval.eval_ref", eval_ref) thy t [])
-  |> Code.postprocess_term thy;
+  |> (fn t => Code_ML.eval_term NONE ("Eval.eval_ref", eval_ref) thy t []);
 
 end;
 *}

--- a/src/HOL/HOL.thy	Fri Apr 17 14:29:55 2009 +0200
+++ b/src/HOL/HOL.thy	Fri Apr 17 14:29:56 2009 +0200
@@ -1885,7 +1885,7 @@
     val t = Thm.term_of ct;
     val dummy = @{cprop True};
   in case try HOLogic.dest_Trueprop t
-   of SOME t' => if Code_ML.eval_term
+   of SOME t' => if Code_ML.eval NONE
          ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy t' [] 
        then Thm.capply (Thm.capply @{cterm "op \<equiv> \<Colon> prop \<Rightarrow> prop \<Rightarrow> prop"} ct) dummy
        else dummy

--- a/src/HOL/Library/Eval_Witness.thy	Fri Apr 17 14:29:55 2009 +0200
+++ b/src/HOL/Library/Eval_Witness.thy	Fri Apr 17 14:29:56 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_term ("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) thy t ws
   then Thm.cterm_of thy goal
   else @{cprop True} (*dummy*)
 end

--- a/src/Tools/code/code_ml.ML	Fri Apr 17 14:29:55 2009 +0200
+++ b/src/Tools/code/code_ml.ML	Fri Apr 17 14:29:56 2009 +0200
@@ -6,8 +6,11 @@
 
 signature CODE_ML =
 sig
-  val eval_term: string * (unit -> 'a) option ref
+  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
+  val target_Eval: string
   val setup: theory -> theory
 end;
 
@@ -22,6 +25,7 @@
 
 val target_SML = "SML";
 val target_OCaml = "OCaml";
+val target_Eval = "Eval";
 
 datatype ml_stmt =
     MLExc of string * int
@@ -944,20 +948,20 @@
 
 (** ML (system language) code for evaluation and instrumentalization **)
 
-fun ml_code_of thy = Code_Target.serialize_custom thy (target_SML,
+fun eval_code_of some_target thy = Code_Target.serialize_custom thy (the_default target_Eval some_target,
     (fn _ => fn [] => serialize_ml target_SML (SOME (K ())) (K Pretty.chunks) pr_sml_stmt (SOME ""),
   literals_sml));
 
 
 (* evaluation *)
 
-fun eval_term reff thy t args =
+fun gen_eval eval some_target reff thy t args =
   let
     val ctxt = ProofContext.init thy;
     val _ = if null (Term.add_frees t []) then () else error ("Term "
       ^ quote (Syntax.string_of_term_global thy t)
       ^ " to be evaluated contains free variables");
-    fun evaluator _ naming program ((_, ty), t) deps =
+    fun evaluator naming program (((_, (_, ty)), _), t) deps =
       let
         val _ = if Code_Thingol.contains_dictvar t then
           error "Term to be evaluated contains free dictionaries" else ();
@@ -966,11 +970,14 @@
           |> Graph.new_node (value_name,
               Code_Thingol.Fun (Term.dummy_patternN, (([], ty), [(([], t), (Drule.dummy_thm, true))])))
           |> fold (curry Graph.add_edge value_name) deps;
-        val (value_code, [SOME value_name']) = ml_code_of thy naming program' [value_name];
+        val (value_code, [SOME value_name']) = eval_code_of some_target thy naming program' [value_name];
         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_term thy I evaluator t 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;
 
 
 (* instrumentalization by antiquotation *)
@@ -988,7 +995,7 @@
 fun delayed_code thy consts () =
   let
     val (consts', (naming, program)) = Code_Thingol.consts_program thy consts;
-    val (ml_code, consts'') = ml_code_of thy naming program consts';
+    val (ml_code, consts'') = eval_code_of NONE thy naming program consts';
     val const_tab = map2 (fn const => fn NONE =>
       error ("Constant " ^ (quote o Code_Unit.string_of_const thy) const
         ^ "\nhas a user-defined serialization")
@@ -1046,6 +1053,7 @@
 val setup =
   Code_Target.add_target (target_SML, (isar_seri_sml, literals_sml))
   #> Code_Target.add_target (target_OCaml, (isar_seri_ocaml, literals_ocaml))
+  #> Code_Target.extend_target (target_Eval, (target_SML, K I))
   #> Code_Target.add_syntax_tyco target_SML "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
       brackify_infix (1, R) fxy [
         pr_typ (INFX (1, X)) ty1,

--- a/src/Tools/code/code_thingol.ML	Fri Apr 17 14:29:55 2009 +0200
+++ b/src/Tools/code/code_thingol.ML	Fri Apr 17 14:29:56 2009 +0200
@@ -83,11 +83,14 @@
 
   val consts_program: theory -> string list -> string list * (naming * program)
   val cached_program: theory -> naming * program
-  val eval_conv: theory
-    -> (term -> term) -> (term -> naming -> program -> typscheme * iterm -> string list -> thm)
+  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
-    -> (term -> term) -> (term -> naming -> program -> typscheme * iterm -> string list -> 'a)
+  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)
+    -> (naming -> program -> (((string * sort) list * typscheme) * (string * itype) list) * iterm -> string list -> 'a)
     -> term -> 'a
 end;
 
@@ -740,7 +743,7 @@
 
 (* value evaluation *)
 
-fun ensure_value thy algbr funcgr t =
+fun ensure_value thy algbr funcgr (fs, t) =
   let
     val ty = fastype_of t;
     val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
@@ -751,29 +754,34 @@
       ##>> translate_term thy algbr funcgr NONE t
       #>> (fn ((vs, ty), t) => Fun
         (Term.dummy_patternN, ((vs, ty), [(([], t), (Drule.dummy_thm, true))])));
-    fun term_value (dep, (naming, program1)) =
+    fun term_value fs (dep, (naming, program1)) =
       let
-        val Fun (_, ((vs, ty), [(([], t), _)])) =
+        val Fun (_, (vs_ty, [(([], t), _)])) =
           Graph.get_node program1 Term.dummy_patternN;
         val deps = Graph.imm_succs program1 Term.dummy_patternN;
         val program2 = Graph.del_nodes [Term.dummy_patternN] program1;
         val deps_all = Graph.all_succs program2 deps;
         val program3 = Graph.subgraph (member (op =) deps_all) program2;
-      in (((naming, program3), (((vs, ty), t), deps)), (dep, (naming, program2))) end;
+      in (((naming, program3), (((vs_ty, fs), t), deps)), (dep, (naming, program2))) end;
   in
     ensure_stmt ((K o K) NONE) pair stmt_value Term.dummy_patternN
     #> snd
-    #> term_value
+    #> fold_map (fn (v, ty) => translate_typ thy algbr funcgr ty
+         #-> (fn ty' => pair (v, ty'))) fs
+    #-> (fn fs' => term_value fs')
   end;
 
-fun eval thy evaluator raw_t algebra funcgr t =
+fun base_evaluator thy evaluator algebra funcgr vs t =
   let
-    val (((naming, program), (vs_ty_t, deps)), _) =
-      invoke_generation thy (algebra, funcgr) ensure_value t;
-  in evaluator raw_t naming program vs_ty_t deps end;
+    val fs = Term.add_frees t [];
+    val (((naming, program), ((((vs', ty'), fs'), t'), deps)), _) =
+      invoke_generation thy (algebra, funcgr) ensure_value (fs, t);
+    val vs'' = map (fn (v, _) => (v, (the o AList.lookup (op =) vs o prefix "'") v)) vs';
+  in evaluator naming program (((vs'', (vs', ty')), fs'), t') deps end;
 
-fun eval_conv thy preproc = Code_Wellsorted.eval_conv thy preproc o eval thy;
-fun eval_term thy preproc = Code_Wellsorted.eval_term thy preproc o eval thy;
+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;
 
 
 (** diagnostic commands **)

--- a/src/Tools/code/code_wellsorted.ML	Fri Apr 17 14:29:55 2009 +0200
+++ b/src/Tools/code/code_wellsorted.ML	Fri Apr 17 14:29:56 2009 +0200
@@ -7,26 +7,28 @@
 
 signature CODE_WELLSORTED =
 sig
-  type T
-  val eqns: T -> string -> (thm * bool) list
-  val typ: T -> string -> (string * sort) list * typ
-  val all: T -> string list
-  val pretty: theory -> T -> Pretty.T
-  val obtain: theory -> string list -> term list -> ((sort -> sort) * Sorts.algebra) * T
-  val preprocess: theory -> cterm list -> (cterm * (thm -> thm)) list
-  val preprocess_term: theory -> term list -> (term * (term -> term)) list
-  val eval_conv: theory
-    -> (term -> term) -> (term -> (sort -> sort) * Sorts.algebra -> T -> term -> thm) -> cterm -> thm
-  val eval_term: theory
-    -> (term -> term) -> (term -> (sort -> sort) * Sorts.algebra -> T -> term -> 'a) -> term -> 'a
+  type code_algebra
+  type code_graph
+  val eqns: code_graph -> string -> (thm * bool) list
+  val typ: code_graph -> string -> (string * sort) list * typ
+  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)
+    -> (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)
+    -> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a
 end
 
 structure Code_Wellsorted : CODE_WELLSORTED =
 struct
 
-(** the equation graph type **)
+(** the algebra and code equation graph types **)
 
-type T = (((string * sort) list * typ) * (thm * bool) list) Graph.T;
+type code_algebra = (sort -> sort) * Sorts.algebra;
+type code_graph = (((string * sort) list * typ) * (thm * bool) list) Graph.T;
 
 fun eqns eqngr = these o Option.map snd o try (Graph.get_node eqngr);
 fun typ eqngr = fst o Graph.get_node eqngr;
@@ -271,7 +273,7 @@
 
 structure Wellsorted = CodeDataFun
 (
-  type T = ((string * class) * sort list) list * T;
+  type T = ((string * class) * sort list) list * code_graph;
   val empty = ([], Graph.empty);
   fun purge thy cs (arities, eqngr) =
     let
@@ -293,47 +295,36 @@
 fun obtain thy cs ts = apsnd snd
   (Wellsorted.change_yield thy (extend_arities_eqngr thy cs ts));
 
-fun preprocess thy cts =
-  let
-    val ts = map Thm.term_of cts;
-    val _ = map
-      (Sign.no_vars (Syntax.pp_global thy) o Term.map_types Type.no_tvars) ts;
-    fun make thm1 = (Thm.rhs_of thm1, fn thm2 =>
-      let
-        val thm3 = Code.postprocess_conv thy (Thm.rhs_of thm2);
-      in
-        Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
-          error ("could not construct evaluation proof:\n"
-          ^ (cat_lines o map Display.string_of_thm) [thm1, thm2, thm3])
-      end);
-  in map (make o Code.preprocess_conv thy) cts end;
+fun prepare_sorts prep_sort (Const (c, ty)) = Const (c, map_type_tfree
+      (fn (v, sort) => TFree (v, prep_sort sort)) ty)
+  | prepare_sorts prep_sort (t1 $ t2) =
+      prepare_sorts prep_sort t1 $ prepare_sorts prep_sort t2
+  | prepare_sorts prep_sort (Abs (v, ty, t)) =
+      Abs (v, Type.strip_sorts ty, prepare_sorts prep_sort t)
+  | prepare_sorts _ (Term.Free (v, ty)) = Term.Free (v, Type.strip_sorts ty)
+  | prepare_sorts _ (t as Bound _) = t;
 
-fun preprocess_term thy ts =
-  let
-    val cts = map (Thm.cterm_of thy) ts;
-    val postprocess = Code.postprocess_term thy;
-  in map (fn (ct, _) => (Thm.term_of ct, postprocess)) (preprocess thy cts) end;
-
-(*FIXME rearrange here*)
-
-fun proto_eval thy cterm_of evaluator_lift preproc evaluator proto_ct =
+fun gen_eval thy cterm_of conclude_evaluation prep_sort evaluator proto_ct =
   let
     val ct = cterm_of proto_ct;
-    val _ = Sign.no_vars (Syntax.pp_global thy) (Thm.term_of ct);
-    val _ = Term.map_types Type.no_tvars (Thm.term_of ct);
-    fun consts_of t =
-      fold_aterms (fn Const c_ty => cons c_ty | _ => I) t [];
+    val _ = (Term.map_types Type.no_tvars o Sign.no_vars (Syntax.pp_global thy))
+      (Thm.term_of ct);
     val thm = Code.preprocess_conv thy ct;
     val ct' = Thm.rhs_of thm;
     val t' = Thm.term_of ct';
-    val consts = map fst (consts_of t');
-    val t'' = preproc t';
+    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 (algebra', eqngr') = obtain thy consts [t''];
-  in evaluator_lift (evaluator t' algebra' eqngr' t'') 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 =
   let
-    fun evaluator_lift thm2 thm1 =
+    fun conclude_evaluation thm2 thm1 =
       let
         val thm3 = Code.postprocess_conv thy (Thm.rhs_of thm2);
       in
@@ -341,8 +332,12 @@
           error ("could not construct evaluation proof:\n"
           ^ (cat_lines o map Display.string_of_thm) [thm1, thm2, thm3])
       end;
-  in proto_eval thy I evaluator_lift end;
+  in gen_eval thy I conclude_evaluation end;
 
-fun eval_term thy = proto_eval thy (Thm.cterm_of thy) (fn t => K t);
+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);
 
 end; (*struct*)

--- a/src/Tools/nbe.ML	Fri Apr 17 14:29:55 2009 +0200
+++ b/src/Tools/nbe.ML	Fri Apr 17 14:29:56 2009 +0200
@@ -350,7 +350,7 @@
 
 (* term evaluation *)
 
-fun eval_term ctxt gr deps ((vs, ty) : typscheme, t) =
+fun eval_term ctxt gr deps (vs : (string * sort) list, t) =
   let 
     val frees = Code_Thingol.fold_unbound_varnames (insert (op =)) t []
     val frees' = map (fn v => Free (v, [])) frees;
@@ -364,6 +364,15 @@
 
 (* reification *)
 
+fun typ_of_itype program vs (ityco `%% itys) =
+      let
+        val Code_Thingol.Datatype (tyco, _) = Graph.get_node program ityco;
+      in Type (tyco, map (typ_of_itype program vs) itys) end
+  | typ_of_itype program vs (ITyVar v) =
+      let
+        val sort = (the o AList.lookup (op =) vs) v;
+      in TFree ("'" ^ v, sort) end;
+
 fun term_of_univ thy program idx_tab t =
   let
     fun take_until f [] = []
@@ -418,41 +427,40 @@
 
 (* compilation, evaluation and reification *)
 
-fun compile_eval thy naming program vs_ty_t deps =
+fun compile_eval thy naming program vs_t deps =
   let
     val ctxt = ProofContext.init thy;
     val (_, (gr, (_, idx_tab))) =
       Nbe_Functions.change thy (ensure_stmts ctxt naming program o snd);
   in
-    vs_ty_t
+    vs_t
     |> eval_term ctxt gr deps
     |> term_of_univ thy program idx_tab
   end;
 
 (* evaluation with type reconstruction *)
 
-fun norm thy t naming program vs_ty_t deps =
+fun norm 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);
-    val subst_triv_consts = subst_const (Code_Unit.resubst_alias thy);
-    val ty = type_of t;
-    val type_free = AList.lookup (op =)
-      (map (fn (s, T) => (s, Term.Free (s, T))) (Term.add_frees t []));
-    val type_frees = Term.map_aterms
-      (fn (t as Term.Free (s, _)) => the_default t (type_free s) | t => t);
+    val resubst_triv_consts = subst_const (Code_Unit.resubst_alias thy);
+    val ty' = typ_of_itype program vs0 ty;
+    val fs' = (map o apsnd) (typ_of_itype program vs0) fs;
+    val type_frees = Term.map_aterms (fn (t as Term.Free (s, _)) =>
+      Term.Free (s, (the o AList.lookup (op =) fs') s) | t => t);
     fun type_infer t =
       singleton (TypeInfer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I
         (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE) Name.context 0)
-      (TypeInfer.constrain ty t);
+      (TypeInfer.constrain ty' t);
     fun check_tvars t = if null (Term.add_tvars t []) then t else
       error ("Illegal schematic type variables in normalized term: "
         ^ setmp show_types true (Syntax.string_of_term_global thy) t);
     val string_of_term = setmp show_types true (Syntax.string_of_term_global thy);
   in
-    compile_eval thy naming program vs_ty_t deps
+    compile_eval thy naming program (vs, t) deps
     |> tracing (fn t => "Normalized:\n" ^ string_of_term t)
-    |> subst_triv_consts
+    |> resubst_triv_consts
     |> type_frees
     |> tracing (fn t => "Vars typed:\n" ^ string_of_term t)
     |> type_infer
@@ -463,21 +471,22 @@
 
 (* evaluation oracle *)
 
-fun add_triv_classes thy =
+fun add_triv_classes thy = curry (Sorts.inter_sort (Sign.classes_of thy))
+  (Code_Unit.triv_classes thy);
+
+fun mk_equals thy lhs raw_rhs =
   let
-    val inters = curry (Sorts.inter_sort (Sign.classes_of thy))
-      (Code_Unit.triv_classes thy);
-    fun map_sorts f = (map_types o map_atyps)
-      (fn TVar (v, sort) => TVar (v, f sort)
-        | TFree (v, sort) => TFree (v, f sort));
-  in map_sorts inters end;
+    val ty = Thm.typ_of (Thm.ctyp_of_term lhs);
+    val eq = Thm.cterm_of thy (Term.Const ("==", ty --> ty --> propT));
+    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
-  (Thm.add_oracle (Binding.name "norm", fn (thy, t, naming, program, vs_ty_t, deps) =>
-    Thm.cterm_of thy (Logic.mk_equals (t, norm thy t naming program vs_ty_t deps)))));
+  (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))));
 
-fun norm_oracle thy t naming program vs_ty_t deps =
-  raw_norm_oracle (thy, t, naming, program, vs_ty_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);
 
 fun norm_conv ct =
   let