# HG changeset patch
# User haftmann
# Date 1157350680 -7200
# Node ID 7c20ddbd911b148a927db5628bd29da0f147d5d2
# Parent  95f6d354b0edc6ef4861bac0601450a5e92254f9
explicit table with constant types

diff -r 95f6d354b0ed -r 7c20ddbd911b src/Pure/Tools/codegen_package.ML
--- a/src/Pure/Tools/codegen_package.ML	Mon Sep 04 08:17:28 2006 +0200
+++ b/src/Pure/Tools/codegen_package.ML	Mon Sep 04 08:18:00 2006 +0200
@@ -106,7 +106,7 @@
 
 (* theory data  *)
 
-type appgen = theory -> Sorts.algebra * (sort -> sort) -> CodegenTheorems.thmtab
+type appgen = theory -> ((sort -> sort) * Sorts.algebra) * Consts.T -> CodegenTheorems.thmtab
   -> bool * string list option -> (string * typ) * term list -> transact -> iterm * transact;
 
 type appgens = (int * (appgen * stamp)) Symtab.table;
@@ -302,7 +302,7 @@
 
 fun ensure_def_class thy algbr thmtab strct cls trns =
   let
-    fun defgen_class thy (algbr as (_, proj_sort)) thmtab strct cls trns =
+    fun defgen_class thy (algbr as ((proj_sort, _), _)) thmtab strct cls trns =
       case class_of_idf thy cls
        of SOME cls =>
             let
@@ -356,7 +356,7 @@
         ("generating type constructor " ^ quote tyco) tyco'
     |> pair tyco'
   end
-and exprgen_tyvar_sort thy (algbr as (_, proj_sort)) thmtab strct (v, sort) trns =
+and exprgen_tyvar_sort thy (algbr as ((proj_sort, _), _)) thmtab strct (v, sort) trns =
   trns
   |> fold_map (ensure_def_class thy algbr thmtab strct) (proj_sort sort)
   |-> (fn sort => pair (unprefix "'" v, sort))
@@ -377,7 +377,7 @@
       ||>> fold_map (exprgen_type thy algbr thmtab strct) tys
       |-> (fn (tyco, tys) => pair (tyco `%% tys));
 
-fun exprgen_typinst thy (algbr as (algebra, proj_sort)) thmtab strct (ty_ctxt, sort_decl) trns =
+fun exprgen_typinst thy (algbr as ((proj_sort, algebra), consts)) thmtab strct (ty_ctxt, sort_decl) trns =
   let
     val pp = Sign.pp thy;
     datatype inst =
@@ -410,28 +410,19 @@
     trns
     |> fold_map mk_dict insts
   end
-and exprgen_typinst_const thy algbr thmtab strct (c, ty_ctxt) trns =
-  let
-    val ty_decl = case CodegenTheorems.get_fun_thms thmtab (c, ty_ctxt)
-     of thms as thm :: _ => CodegenTheorems.extr_typ thy thm
-      | [] => (case AxClass.class_of_param thy c
-         of SOME class => (case ClassPackage.the_consts_sign thy class of (v, cs) =>
-              (Logic.varifyT o map_type_tfree (fn u as (w, _) =>
-                if w = v then TFree (v, [class]) else TFree u))
-              ((the o AList.lookup (op =) cs) c))
-          | NONE => Sign.the_const_type thy c);
-    val insts =
-      Vartab.empty
-      |> Sign.typ_match thy (ty_decl, ty_ctxt)
-      |> Vartab.dest
-      |> map (fn (_, (sort, ty)) => (ty, sort))
+and exprgen_typinst_const thy (algbr as (_, consts)) thmtab strct (c, ty_ctxt) trns =
+  let 
+    val idf = idf_of_const thy thmtab (c, ty_ctxt)
+    val ty_decl = Consts.declaration consts idf;
+    val insts = (op ~~ o apsnd (map (snd o dest_TVar)) oo pairself)
+      (curry (Consts.typargs consts) idf) (ty_ctxt, ty_decl);
   in
     trns
     |> fold_map (exprgen_typinst thy algbr thmtab strct) insts
   end
 and ensure_def_inst thy algbr thmtab strct (cls, tyco) trns =
   let
-    fun defgen_inst thy (algbr as (_, proj_sort)) thmtab strct inst trns =
+    fun defgen_inst thy (algbr as ((proj_sort, _), _)) thmtab strct inst trns =
       case inst_of_idf thy inst
        of SOME (class, tyco) =>
             let
@@ -442,7 +433,8 @@
               fun gen_suparity supclass trns =
                 trns
                 |> ensure_def_class thy algbr thmtab strct supclass
-                ||>> exprgen_typinst thy algbr thmtab strct (arity_typ, [supclass]);
+                ||>> exprgen_typinst thy algbr thmtab strct (arity_typ, [supclass])
+                |-> (fn (supclass, [Instance (supints, lss)]) => pair (supclass, (supints, lss)));
               fun gen_membr ((m0, ty0), (m, ty)) trns =
                 trns
                 |> ensure_def_const thy algbr thmtab strct (m0, ty0)
@@ -492,18 +484,17 @@
             |-> (fn _ => succeed Bot)
         | _ =>
             trns |> fail ("No class found for " ^ (quote o CodegenConsts.string_of_const_typ thy) (c, ty))
-    fun defgen_funs thy algbr thmtab strct c' trns =
+    fun defgen_funs thy (algbr as (_, consts)) thmtab strct c' trns =
       case CodegenTheorems.get_fun_thms thmtab ((the o const_of_idf thy) c')
        of eq_thms as eq_thm :: _ =>
             let
               val msg = cat_lines ("generating code for theorems " :: map string_of_thm eq_thms);
               val ty = (Logic.unvarifyT o CodegenTheorems.extr_typ thy) eq_thm;
-              val vs = (rev ooo fold_atyps)
-                (fn TFree v_sort => insert (op =) v_sort | _ => I) ty [];
+              val vs = (map dest_TFree o Consts.typargs consts) (c', ty);
               fun dest_eqthm eq_thm =
                 let
                   val ((t, args), rhs) =
-                    (apfst strip_comb o Logic.dest_equals o Logic.legacy_unvarify o prop_of) eq_thm;
+                    (apfst strip_comb o Logic.dest_equals o Logic.unvarify o prop_of) eq_thm;
                 in case t
                  of Const (c', _) => if c' = c then (args, rhs)
                      else error ("Illegal function equation for " ^ quote c
@@ -700,13 +691,35 @@
 (** code generation interfaces **)
 
 fun generate cs targets init gen it thy =
-  thy
-  |> CodegenTheorems.notify_dirty
-  |> `Code.get
-  |> (fn (modl, thy) =>
-        (start_transact init (gen thy (ClassPackage.operational_algebra thy) (CodegenTheorems.mk_thmtab thy cs)
-          (true, targets) it) modl, thy))
-  |-> (fn (x, modl) => Code.map (K modl) #> pair x);
+  let
+    val thmtab = CodegenTheorems.mk_thmtab thy cs;
+    val qnaming = NameSpace.qualified_names NameSpace.default_naming
+    val algebr = ClassPackage.operational_algebra thy;
+    fun ops_of_class class =
+      let
+        val (v, ops) = ClassPackage.the_consts_sign thy class;
+        val ops_tys = map (fn (c, ty) =>
+          (c, (Logic.varifyT o map_type_tfree (fn u as (w, _) =>
+            if w = v then TFree (v, [class]) else TFree u)) ty)) ops;
+      in
+        map (fn (c, ty) => (idf_of_const thy thmtab (c, ty), ty)) ops_tys
+      end;
+    val classops = maps ops_of_class (Sorts.classes (snd algebr));
+    val consttab = Consts.empty
+      |> fold (fn (c, ty) => Consts.declare qnaming
+           (((idf_of_const thy thmtab o CodegenConsts.typ_of_typinst thy) c, ty), true))
+           (CodegenTheorems.get_fun_typs thmtab)
+      |> fold (Consts.declare qnaming o rpair true) classops;
+    val algbr = (algebr, consttab);
+  in   
+    thy
+    |> CodegenTheorems.notify_dirty
+    |> `Code.get
+    |> (fn (modl, thy) =>
+          (start_transact init (gen thy algbr thmtab
+            (true, targets) it) modl, thy))
+    |-> (fn (x, modl) => Code.map (K modl) #> pair x)
+  end;
 
 fun consts_of t =
   fold_aterms (fn Const c => cons c | _ => I) t [];
diff -r 95f6d354b0ed -r 7c20ddbd911b src/Pure/Tools/codegen_serializer.ML
--- a/src/Pure/Tools/codegen_serializer.ML	Mon Sep 04 08:17:28 2006 +0200
+++ b/src/Pure/Tools/codegen_serializer.ML	Mon Sep 04 08:18:00 2006 +0200
@@ -738,11 +738,11 @@
       | ml_from_def (name, CodegenThingol.Classinst ((class, (tyco, arity)), (suparities, memdefs))) =
           let
             val definer = if null arity then "val" else "fun"
-            fun from_supclass (supclass, ls) =
+            fun from_supclass (supclass, (supinst, lss)) =
               (Pretty.block o Pretty.breaks) [
                 ml_from_label supclass,
                 str "=",
-                ml_from_insts NOBR ls
+                ml_from_insts NOBR [Instance (supinst, lss)]
               ];
             fun from_memdef (m, e) =
               (Pretty.block o Pretty.breaks) [
diff -r 95f6d354b0ed -r 7c20ddbd911b src/Pure/Tools/codegen_theorems.ML
--- a/src/Pure/Tools/codegen_theorems.ML	Mon Sep 04 08:17:28 2006 +0200
+++ b/src/Pure/Tools/codegen_theorems.ML	Mon Sep 04 08:18:00 2006 +0200
@@ -33,6 +33,7 @@
   val get_dtyp_of_cons: thmtab -> string * typ -> string option;
   val get_dtyp_spec: thmtab -> string
     -> ((string * sort) list * (string * typ list) list) option;
+  val get_fun_typs: thmtab -> ((string * typ list) * typ) list;
   val get_fun_thms: thmtab -> string * typ -> thm list;
 
   val pretty_funtab: theory -> thm list CodegenConsts.Consttab.table -> Pretty.T;
@@ -766,6 +767,18 @@
   (check_thms c o these o Consttab.lookup funtab
     o CodegenConsts.norminst_of_typ thy) c_ty;
 
+fun get_fun_typs (thy, (funtab, dtcotab), _) =
+  (Consttab.dest funtab
+  |> map (fn (c, thm :: _) => (c, extr_typ thy thm)
+           | (c as (name, _), []) => (c, case AxClass.class_of_param thy name
+         of SOME class => (case ClassPackage.the_consts_sign thy class of (v, cs) =>
+              (Logic.varifyT o map_type_tfree (fn u as (w, _) =>
+                if w = v then TFree (v, [class]) else TFree u))
+              ((the o AList.lookup (op =) cs) name))
+          | NONE => Sign.the_const_type thy name)))
+  @ (Consttab.keys dtcotab
+  |> AList.make (Sign.const_instance thy));
+
 fun pretty_funtab thy funtab =
   funtab
   |> CodegenConsts.Consttab.dest
diff -r 95f6d354b0ed -r 7c20ddbd911b src/Pure/Tools/codegen_thingol.ML
--- a/src/Pure/Tools/codegen_thingol.ML	Mon Sep 04 08:17:28 2006 +0200
+++ b/src/Pure/Tools/codegen_thingol.ML	Mon Sep 04 08:18:00 2006 +0200
@@ -71,7 +71,7 @@
     | Class of class list * (vname * (string * itype) list)
     | Classmember of class
     | Classinst of (class * (string * (vname * sort) list))
-          * ((class * inst list) list
+          * ((class * (string * inst list list)) list
         * (string * iterm) list);
   type module;
   type transact;
@@ -388,7 +388,7 @@
   | Class of class list * (vname * (string * itype) list)
   | Classmember of class
   | Classinst of (class * (string * (vname * sort) list))
-        * ((class * inst list) list
+        * ((class * (string * inst list list)) list
       * (string * iterm) list);
 
 datatype node = Def of def | Module of node Graph.T;
@@ -698,56 +698,124 @@
   ) ((AList.make (Graph.get_node modl) o flat o Graph.strong_conn) modl)
 
 (*
+(*FIXME: graph-based approach is better.
+* build graph
+* implement flat_classops on sort level, not class level
+* flat_instances bleibt wie es ist
+*)
+fun flat_classops modl =
+  let
+    fun add_ancestry class anc =
+      let
+        val SOME (Class (super_classes, (v, ops))) = AList.lookup (op =) modl class
+        val super_classees' = filter (not o member (fn (c', (c, _)) => c = c') anc) super_classes;
+      in
+        [(class, ops)] @ anc
+        |> fold add_ancestry super_classees'
+      end;
+  in
+    Symtab.empty
+    |> fold (
+         fn (class, Class _) =>
+              Symtab.update_new (class, maps snd (add_ancestry class []))
+           | _ => I
+       ) modl
+    |> the oo Symtab.lookup
+  end;
+
+fun flat_instances modl =
+  let
+    fun add_ancestry instance instsss anc =
+      let
+        val SOME (Classinst (_, (super_instances, ops))) = AList.lookup (op =) modl instance;
+        val super_instances' = filter (not o member (eq_fst (op =)) anc) super_instances;
+        val ops' = map (apsnd (rpair instsss)) ops;
+        (*FIXME: build types*)
+      in
+        [(instance, ops')] @ anc
+        |> fold (fn (_, (instance, instss)) => add_ancestry instance (instss :: instsss)) super_instances'
+      end;
+  in
+    Symtab.empty
+    |> fold (
+         fn (instance, Classinst _) =>
+              Symtab.update_new (instance, maps snd (add_ancestry instance [] []))
+           | _ => I
+       ) modl
+    |> the oo Symtab.lookup
+  end;
+
+fun flat_fundef classops instdefs is_classop (eqs, (vs, ty)) =
+  let
+    fun fold_map_snd' f (x, ys) = fold_map (f x) ys;
+    fun fold_map_snd f (x, ys) = fold_map f ys #-> (fn zs => pair (x, zs));
+    val names =
+      Name.context
+      |> fold Name.declare
+           (fold (fn (rhs, lhs) => fold add_varnames rhs #> add_varnames lhs) eqs []);
+    val opmap = [] : (string * (string * (string * itype) list) list) list;
+    val (params, tys) = (split_list o maps snd o maps snd) opmap;
+    (*fun name_ops v' class = 
+      (fold_map o fold_map_snd')
+        (fn (class, v) => fn (c, ty) => Name.variants [c] #-> (fn [p] =>
+          pair (class, v') (c, (ty, p))))
+          (classops class);
+    val (opsmap, _) = (fold_map o fold_map_snd') name_ops vs names;
+    (* --> (iterm * itype) list *)*)
+    fun flat_inst (Instance (instance, instss)) =
+          let
+            val xs : (string * (iterm * (itype * inst list list list))) list = instdefs instance
+            fun mk_t (t, (ty, instsss)) =
+              (Library.foldl (fn (t, instss) => t `$$ map (fst o snd) ((maps o maps) flat_inst instss))
+                (t, instss :: instsss), ty)
+          in
+            map (apsnd mk_t) xs
+          end
+      | flat_inst (Context (classes, (v, k))) =
+          let
+            val _ : 'a = classops (hd classes);
+          in
+            []
+          end
+          (*
+            val parm_map = nth ((the o AList.lookup (op =) octxt) v)
+              (if k = ~1 then 0 else k);
+          in map (apfst IVar o swap o snd) (case classes
+           of class::_ => (the o AList.lookup (op =) parm_map) class
+            | _ => (snd o hd) parm_map)*)
+    and flat_iterm (e as IConst (c, (lss, ty))) =
+          if is_classop c then let
+            val tab = (maps o maps) flat_inst lss;
+            val SOME (t, _) = AList.lookup (op =) tab c;
+          in t end else let
+            val (es, tys) = (split_list o map snd) ((maps o maps) flat_inst lss)
+          in IConst (c, (replicate (length lss) [], tys `--> ty)) `$$ es end
+      | flat_iterm (e as IVar _) =
+          e
+      | flat_iterm (e1 `$ e2) =
+          flat_iterm e1 `$ flat_iterm e2
+      | flat_iterm (v_ty `|-> e) =
+          v_ty `|-> flat_iterm e
+      | flat_iterm (INum (k, e)) =
+          INum (k, flat_iterm e)
+      | flat_iterm (IChar (s, e)) =
+          IChar (s, flat_iterm e)
+      | flat_iterm (ICase (((de, dty), es), e)) =
+          ICase (((flat_iterm de, dty), map (pairself flat_iterm) es), flat_iterm e);
+    fun flat_eq (lhs, rhs) = (map IVar params @ lhs, flat_iterm rhs);
+  in (map flat_eq eqs, (map (apsnd (K [])) vs, tys `--> ty)) end;
+
 fun flat_funs_datatypes modl =
-  map (
-   fn def as (_, Datatype _) => def
-    | (name, Fun (eqs, (vs, ty))) => let
-          val vs = fold (fn (rhs, lhs) => fold add_varnames rhs #> add_varnames lhs) eqs [];
-          fun fold_map_snd f (x, ys) = fold_map f ys #-> (fn zs => pair (x, zs));
-          fun all_ops_of class = [] : (class * (string * itype) list) list
-            (*FIXME; itype within current context*);
-          fun name_ops class = 
-            (fold_map o fold_map_snd)
-              (fn (c, ty) => Name.variants [c] #-> (fn [v] => pair (c, (ty, v)))) (all_ops_of class);
-          (*FIXME: should contain superclasses only once*)
-          val (octxt, _) = (fold_map o fold_map_snd) name_ops vs
-            (Name.make_context vs);
-          (* --> (iterm * itype) list *)
-          fun flat_classlookup (Instance (inst, lss)) =
-                (case get_def modl inst
-                 of (Classinst (_, (suparities, ops)))
-                      => maps (maps flat_classlookup o snd) suparities @ map (apsnd flat_iterm) ops
-                  | _ => error ("Bad instance: " ^ quote inst))
-            | flat_classlookup (Context (classes, (v, k))) =
-                let
-                  val parm_map = nth ((the o AList.lookup (op =) octxt) v)
-                    (if k = ~1 then 0 else k);
-                in map (apfst IVar o swap o snd) (case classes
-                 of class::_ => (the o AList.lookup (op =) parm_map) class
-                  | _ => (snd o hd) parm_map)
-                end
-          and flat_iterm (e as IConst (c, (lss, ty))) =
-                let
-                  val (es, tys) = split_list ((maps o maps) flat_classlookup lss)
-                in IConst (c, ([], tys `--> ty)) `$$ es end
-                (*FIXME Eliminierung von Projektionen*)
-            | flat_iterm (e as IVar _) =
-                e
-            | flat_iterm (e1 `$ e2) =
-                flat_iterm e1 `$ flat_iterm e2
-            | flat_iterm (v_ty `|-> e) =
-                v_ty `|-> flat_iterm e
-            | flat_iterm (INum (k, e)) =
-                INum (k, flat_iterm e)
-            | flat_iterm (IChar (s, e)) =
-                IChar (s, flat_iterm e)
-            | flat_iterm (ICase (((de, dty), es), e)) =
-                ICase (((flat_iterm de, dty), map (pairself flat_iterm) es), flat_iterm e);
-        in
-          (name, Fun (map (fn (lhs, rhs) => (map flat_iterm lhs, flat_iterm rhs)) eqs,
-            ([], maps ((maps o maps) (map (fst o snd) o snd) o snd) octxt `--> ty)))
-        end
-  ) (flat_module modl);
+  let
+    val modl = flat_module modl;
+    val classops = flat_classops modl;
+    val instdefs = flat_instances modl;
+    val is_classop = is_some o AList.lookup (op =) modl;
+  in map_filter (
+   fn def as (_, Datatype _) => SOME def
+    | (name, Fun funn) => SOME (name, (Fun (flat_fundef classops instdefs is_classop funn)))
+    | _ => NONE
+  ) end;
 *)
 
 val add_deps_of_typparms =
@@ -817,9 +885,10 @@
       |> insert (op =) class
       |> insert (op =) tyco
       |> add_deps_of_typparms vs
-      |> fold (fn (supclass, ls) =>
+      |> fold (fn (supclass, (supinst, lss)) =>
             insert (op =) supclass
-            #> fold add_deps_of_classlookup ls
+            #> insert (op =) supinst
+            #> (fold o fold) add_deps_of_classlookup lss
       ) suparities
       |> fold (fn (name, e) =>
             insert (op =) name