more general evaluation combinators

--- a/src/Tools/code/code_funcgr.ML	Tue Apr 22 22:00:25 2008 +0200
+++ b/src/Tools/code/code_funcgr.ML	Tue Apr 22 22:00:31 2008 +0200
@@ -16,8 +16,8 @@
   val pretty: theory -> T -> Pretty.T
   val make: theory -> string list -> T
   val make_consts: theory -> string list -> string list * T
-  val eval_conv: theory -> (T -> cterm -> thm) -> cterm -> thm
-  val eval_term: theory -> (T -> term -> 'a) -> term -> 'a
+  val eval_conv: theory -> (term -> term * (T -> term -> thm)) -> cterm -> thm
+  val eval_term: theory -> (term -> term * (T -> term -> 'a)) -> term -> 'a
 end
 
 structure CodeFuncgr : CODE_FUNCGR =
@@ -276,55 +276,42 @@
     val (consts', funcgr') = fold_map try_const consts funcgr;
   in (map_filter I consts', funcgr') end;
 
-fun raw_eval thy f ct funcgr =
+fun proto_eval thy cterm_of evaluator_fr evaluator proto_ct funcgr =
   let
-    val algebra = Code.coregular_algebra thy;
-    fun consts_of ct = fold_aterms (fn Const c_ty => cons c_ty | _ => I)
-      (Thm.term_of ct) [];
+    val ct = cterm_of proto_ct;
     val _ = Sign.no_vars (Sign.pp thy) (Thm.term_of ct);
     val _ = Term.fold_types (Type.no_tvars #> K I) (Thm.term_of ct) ();
-    val thm1 = Code.preprocess_conv ct;
-    val ct' = Thm.rhs_of thm1;
-    val cs = map fst (consts_of ct');
-    val funcgr' = ensure_consts thy algebra cs funcgr;
-    val (_, thm2) = Thm.varifyT' [] thm1;
-    val thm3 = Thm.reflexive (Thm.rhs_of thm2);
-    val [thm4] = resort_thms algebra (try (fst o Graph.get_node funcgr')) [thm3]
-      handle CLASS_ERROR (_, msg) => error msg;
-    val tfrees = Term.add_tfrees (Thm.prop_of thm1) [];
-    fun inst thm =
+    fun consts_of t = fold_aterms (fn Const c_ty => cons c_ty | _ => I)
+      t [];
+    val algebra = Code.coregular_algebra thy;
+    val thm = Code.preprocess_conv ct;
+    val ct' = Thm.rhs_of thm;
+    val t' = Thm.term_of ct';
+    val consts = map fst (consts_of t');
+    val funcgr' = ensure_consts thy algebra consts funcgr;
+    val (t'', evaluator') = apsnd evaluator_fr (evaluator t');
+    val consts' = consts_of t'';
+    val dicts = instances_of_consts thy algebra funcgr' consts';
+    val funcgr'' = ensure_consts thy algebra dicts funcgr';
+  in (evaluator' thm funcgr'' t'', funcgr'') end;
+
+fun proto_eval_conv thy =
+  let
+    fun evaluator evaluator' thm1 funcgr t =
       let
-        val tvars = Term.add_tvars (Thm.prop_of thm) [];
-        val instmap = map2 (fn (v_i, sort) => fn (v, _) => pairself (Thm.ctyp_of thy)
-          (TVar (v_i, sort), TFree (v, sort))) tvars tfrees;
-      in Thm.instantiate (instmap, []) thm end;
-    val thm5 = inst thm2;
-    val thm6 = inst thm4;
-    val ct'' = Thm.rhs_of thm6;
-    val c_exprs = consts_of ct'';
-    val drop = drop_classes thy tfrees;
-    val instdefs = instances_of_consts thy algebra funcgr' c_exprs;
-    val funcgr'' = ensure_consts thy algebra instdefs funcgr';
-  in (f drop thm5 funcgr'' ct'', funcgr'') end;
-
-fun raw_eval_conv thy conv =
-  let
-    fun conv' drop_classes thm1 funcgr ct =
-      let
-        val thm2 = conv funcgr ct;
+        val thm2 = evaluator' funcgr t;
         val thm3 = Code.postprocess_conv (Thm.rhs_of thm2);
-        val thm23 = drop_classes (Thm.transitive thm2 thm3);
       in
-        Thm.transitive thm1 thm23 handle THM _ =>
-          error ("could not construct proof:\n"
+        Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
+          error ("could not construct evaluation proof (probably due to wellsortedness problem):\n"
           ^ (cat_lines o map string_of_thm) [thm1, thm2, thm3])
       end;
-  in raw_eval thy conv' end;
+  in proto_eval thy I evaluator end;
 
-fun raw_eval_term thy f t =
+fun proto_eval_term thy =
   let
-    fun f' _ _ funcgr ct = f funcgr (Thm.term_of ct);
-  in raw_eval thy f' (Thm.cterm_of thy t) end;
+    fun evaluator evaluator' _ funcgr t = evaluator' funcgr t;
+  in proto_eval thy (Thm.cterm_of thy) evaluator end;
 
 end; (*local*)
 
@@ -346,9 +333,9 @@
   Funcgr.change_yield thy o check_consts thy;
 
 fun eval_conv thy f =
-  fst o Funcgr.change_yield thy o raw_eval_conv thy f;
+  fst o Funcgr.change_yield thy o proto_eval_conv thy f;
 
 fun eval_term thy f =
-  fst o Funcgr.change_yield thy o raw_eval_term thy f;
+  fst o Funcgr.change_yield thy o proto_eval_term thy f;
 
 end; (*struct*)

--- a/src/Tools/code/code_package.ML	Tue Apr 22 22:00:25 2008 +0200
+++ b/src/Tools/code/code_package.ML	Tue Apr 22 22:00:31 2008 +0200
@@ -8,12 +8,12 @@
 signature CODE_PACKAGE =
 sig
   val evaluate_conv: theory
-    -> (CodeThingol.code -> CodeThingol.typscheme * CodeThingol.iterm
-       -> string list -> cterm -> thm)
+    -> (term -> term * (CodeThingol.code -> CodeThingol.typscheme * CodeThingol.iterm
+       -> string list -> thm))
     -> cterm -> thm;
   val evaluate_term: theory
-    -> (CodeThingol.code -> CodeThingol.typscheme * CodeThingol.iterm
-       -> string list -> term -> 'a)
+    -> (term -> term * (CodeThingol.code -> CodeThingol.typscheme * CodeThingol.iterm
+       -> string list -> 'a))
     -> term -> 'a;
   val eval_conv: string * (unit -> thm) option ref
     -> theory -> cterm -> string list -> thm;
@@ -103,24 +103,31 @@
 
 (* evaluation machinery *)
 
-fun evaluate eval_kind term_of thy eval = eval_kind thy (fn funcgr => fn ct =>
+fun evaluate eval_kind thy evaluator =
   let
-    val ((code, (vs_ty_t, deps)), _) = generate thy funcgr
-      CodeThingol.ensure_value (term_of ct)
-  in eval code vs_ty_t deps ct end);
+    fun evaluator'' evaluator''' funcgr t =
+      let
+        val ((code, (vs_ty_t, deps)), _) =
+          generate thy funcgr CodeThingol.ensure_value t;
+      in evaluator''' code vs_ty_t deps end;
+    fun evaluator' t =
+      let
+        val (t', evaluator''') = evaluator t;
+      in (t', evaluator'' evaluator''') end;
+  in eval_kind thy evaluator' end
 
-fun evaluate_conv thy = evaluate CodeFuncgr.eval_conv Thm.term_of thy;
-fun evaluate_term thy = evaluate CodeFuncgr.eval_term I thy;
+fun evaluate_conv thy = evaluate CodeFuncgr.eval_conv thy;
+fun evaluate_term thy = evaluate CodeFuncgr.eval_term thy;
 
-fun eval_ml reff args thy code ((vs, ty), t) deps _ =
+fun eval_ml reff args thy code ((vs, ty), t) deps =
   CodeTarget.eval thy reff code (t, ty) args;
 
 fun eval evaluate term_of reff thy ct args =
   let
     val _ = if null (term_frees (term_of ct)) then () else error ("Term "
       ^ quote (Sign.string_of_term thy (term_of ct))
-      ^ " to be evaluated containts free variables");
-  in evaluate thy (eval_ml reff args thy) ct end;
+      ^ " to be evaluated contains free variables");
+  in evaluate thy (fn t => (t, eval_ml reff args thy)) ct end;
 
 fun eval_conv reff = eval evaluate_conv Thm.term_of reff;
 fun eval_term reff = eval evaluate_term I reff;