# HG changeset patch
# User haftmann
# Date 1228130222 -3600
# Node ID 5c8781b7d6a4b574255722e0c160379423b0fd06
# Parent  0a981c596372b66b65aa7677994196a4f01f74c3
code_funcgr interface includes also sort algebra

diff -r 0a981c596372 -r 5c8781b7d6a4 src/Tools/code/code_funcgr.ML
--- a/src/Tools/code/code_funcgr.ML	Mon Dec 01 12:17:01 2008 +0100
+++ b/src/Tools/code/code_funcgr.ML	Mon Dec 01 12:17:02 2008 +0100
@@ -13,9 +13,12 @@
   val typ: T -> string -> (string * sort) list * typ
   val all: T -> string list
   val pretty: theory -> T -> Pretty.T
-  val make: theory -> string list -> T
-  val eval_conv: theory -> (term -> term * (T -> thm)) -> cterm -> thm
-  val eval_term: theory -> (term -> term * (T -> 'a)) -> term -> 'a
+  val make: theory -> string list
+    -> ((sort -> sort) * Sorts.algebra) * T
+  val eval_conv: theory
+    -> (term -> term * (((sort -> sort) * Sorts.algebra) -> T -> thm)) -> cterm -> thm
+  val eval_term: theory
+    -> (term -> term * (((sort -> sort) * Sorts.algebra) -> T -> 'a)) -> term -> 'a
   val timing: bool ref
 end
 
@@ -235,7 +238,7 @@
     val consts' = consts_of t'';
     val dicts = instances_of_consts thy algebra funcgr' consts';
     val funcgr'' = ensure_consts thy algebra dicts funcgr';
-  in (evaluator_lift evaluator_funcgr thm funcgr'', funcgr'') end;
+  in (evaluator_lift (evaluator_funcgr (Code.operational_algebra thy)) thm funcgr'', funcgr'') end;
 
 fun proto_eval_conv thy =
   let
@@ -267,7 +270,8 @@
 );
 
 fun make thy =
-  Funcgr.change thy o ensure_consts thy (Code.coregular_algebra thy);
+  pair (Code.operational_algebra thy)
+  o Funcgr.change thy o ensure_consts thy (Code.coregular_algebra thy);
 
 fun eval_conv thy f =
   fst o Funcgr.change_yield thy o proto_eval_conv thy f;
@@ -280,7 +284,7 @@
 
 fun code_depgr thy consts =
   let
-    val gr = make thy consts;
+    val (_, gr) = make thy consts;
     val select = Graph.all_succs gr consts;
   in
     gr
diff -r 0a981c596372 -r 5c8781b7d6a4 src/Tools/code/code_thingol.ML
--- a/src/Tools/code/code_thingol.ML	Mon Dec 01 12:17:01 2008 +0100
+++ b/src/Tools/code/code_thingol.ML	Mon Dec 01 12:17:02 2008 +0100
@@ -489,7 +489,7 @@
 
 fun ensure_class thy (algbr as (_, algebra)) funcgr class =
   let
-    val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
+    val superclasses = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
     val cs = #params (AxClass.get_info thy class);
     val stmt_class =
       fold_map (fn superclass => ensure_class thy algbr funcgr superclass
@@ -538,8 +538,16 @@
           Global ((class, tyco), yss)
       | class_relation (Local (classrels, v), subclass) superclass =
           Local ((subclass, superclass) :: classrels, v);
+    fun norm_typargs ys =
+      let
+        val raw_sort = map snd ys;
+        val sort = Sorts.minimize_sort algebra raw_sort;
+      in
+        map_filter (fn (y, class) =>
+          if member (op =) sort class then SOME y else NONE) ys
+      end;
     fun type_constructor tyco yss class =
-      Global ((class, tyco), (map o map) fst yss);
+      Global ((class, tyco), map norm_typargs yss);
     fun type_variable (TFree (v, sort)) =
       let
         val sort' = proj_sort sort;
@@ -567,7 +575,7 @@
   end
 and ensure_inst thy (algbr as (_, algebra)) funcgr (class, tyco) =
   let
-    val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
+    val superclasses = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
     val classparams = these (try (#params o AxClass.get_info thy) class);
     val vs = Name.names Name.context "'a" (Sorts.mg_domain algebra tyco [class]);
     val sorts' = Sorts.mg_domain (Sign.classes_of thy) tyco [class];
@@ -736,9 +744,9 @@
 
 val cached_program = Program.get;
 
-fun invoke_generation thy funcgr f name =
+fun invoke_generation thy (algebra, funcgr) f name =
   Program.change_yield thy (fn naming_program => (NONE, naming_program)
-    |> f thy (Code.operational_algebra thy) funcgr name
+    |> f thy algebra funcgr name
     |-> (fn name => fn (_, naming_program) => (name, naming_program)));
 
 
@@ -789,9 +797,10 @@
 fun eval thy evaluator t =
   let
     val (t', evaluator'') = evaluator t;
-    fun evaluator' funcgr =
+    fun evaluator' algebra funcgr =
       let
-        val (((naming, program), (vs_ty_t, deps)), _) = invoke_generation thy funcgr ensure_value t';
+        val (((naming, program), (vs_ty_t, deps)), _) =
+          invoke_generation thy (algebra, funcgr) ensure_value t';
       in evaluator'' naming program vs_ty_t deps end;
   in (t', evaluator') end