# HG changeset patch
# User haftmann
# Date 1151498151 -7200
# Node ID f992e507020e6c0efa4c5b5fac721a2a89e54310
# Parent  b171fac592bbc50a93b304a587d2b156eb18263b
slight improvements in code generation

diff -r b171fac592bb -r f992e507020e src/Pure/Tools/codegen_package.ML
--- a/src/Pure/Tools/codegen_package.ML	Wed Jun 28 14:35:10 2006 +0200
+++ b/src/Pure/Tools/codegen_package.ML	Wed Jun 28 14:35:51 2006 +0200
@@ -106,6 +106,42 @@
   |> Option.map (alias_rev thy);
 
 
+(* theory name lookup *)
+
+fun thyname_of thy f x =
+  let
+    fun thy_of thy =
+      if f thy x
+      then SOME (the_default thy (get_first thy_of (Theory.parents_of thy)))
+      else NONE;
+  in Option.map Context.theory_name (thy_of thy) end;
+
+fun thyname_of_instance thy inst =
+  let
+    fun test_instance thy (class, tyco) =
+      can (Sorts.mg_domain (Sign.classes_of thy) tyco) [class]
+  in case thyname_of thy test_instance inst
+   of SOME name => name
+    | NONE => error ("thyname_of_instance: no such instance: " ^ quote (fst inst) ^ ", " ^ quote (snd inst))
+  end;
+
+fun thyname_of_tyco thy tyco =
+  case thyname_of thy Sign.declared_tyname tyco
+   of SOME name => name
+    | NONE => error ("thyname_of_tyco: no such type constructor: " ^ quote tyco);
+
+fun thyname_of_thm thy thm =
+  let
+    fun thy_of thy =
+      if member eq_thm ((flat o map snd o NameSpace.dest_table o PureThy.theorems_of) thy) thm
+      then SOME thy
+      else get_first thy_of (Theory.parents_of thy)
+  in case thy_of thy
+   of SOME thy => Context.theory_name thy
+    | NONE => error ("thyname_of_thm: no such thm: " ^ string_of_thm thm)
+  end;
+
+
 (* code generator basics *)
 
 type deftab = (typ * thm) list Symtab.table;
@@ -117,11 +153,10 @@
 
 structure InstNameMangler = NameManglerFun (
   type ctxt = theory;
-  type src = string * (class * string);
-  val ord = prod_ord string_ord (prod_ord string_ord string_ord);
-  fun mk thy ((thyname, (cls, tyco)), i) =
-    (NameSpace.base o alias_get thy) cls ^ "_" ^ (NameSpace.base o alias_get thy) tyco ^ implode (replicate i "'")
-    |> NameSpace.append thyname;
+  type src = class * string;
+  val ord = prod_ord string_ord string_ord;
+  fun mk thy ((cls, tyco), i) =
+    (NameSpace.base o alias_get thy) cls ^ "_" ^ (NameSpace.base o alias_get thy) tyco ^ implode (replicate i "'");
   fun is_valid _ _ = true;
   fun maybe_unique _ _ = NONE;
   fun re_mangle _ dst = error ("no such instance: " ^ quote dst);
@@ -141,7 +176,7 @@
           | NONE => if c = "op ="
               then
                 NameSpace.append
-                  (((fn s => Codegen.thyname_of_type s thy) o fst o dest_Type o hd o fst o strip_type) ty)
+                  ((thyname_of_tyco thy o fst o dest_Type o hd o fst o strip_type) ty)
                   nsp_overl
               else
                 NameSpace.drop_base c';
@@ -198,7 +233,7 @@
 );
 
 type auxtab = (bool * string list option * deftab)
-  * (InstNameMangler.T * (typ list Symtab.table * ConstNameMangler.T)
+  * ((InstNameMangler.T * string Symtab.table Symtab.table) * (typ list Symtab.table * ConstNameMangler.T)
   * DatatypeconsNameMangler.T);
 type eqextr = theory -> auxtab
   -> string * typ -> (thm list * typ) option;
@@ -360,6 +395,7 @@
 
 val print_code = CodegenData.print;
 
+
 (* advanced name handling *)
 
 fun add_alias (src, dst) =
@@ -414,7 +450,7 @@
    of SOME idf => idf
     | NONE => case get_overloaded (c, ty)
    of SOME idf => idf
-    | NONE => case ClassPackage.lookup_const_class thy c
+    | NONE => case AxClass.class_of thy c
    of SOME _ => idf_of_name thy nsp_mem c
     | NONE => idf_of_name thy nsp_const c
   end;
@@ -432,7 +468,7 @@
         | _ => NONE)
   in case get_overloaded (c, ty)
    of SOME idf => idf
-    | NONE => case ClassPackage.lookup_const_class thy c
+    | NONE => case AxClass.class_of thy c
    of SOME _ => idf_of_name thy nsp_mem c
     | NONE => idf_of_name thy nsp_const c
   end;
@@ -536,7 +572,7 @@
 
 fun ensure_def_class thy tabs cls trns =
   let
-    fun defgen_class thy (tabs as (_, (insttab, _, _))) cls trns =
+    fun defgen_class thy (tabs as (_, ((insttab, thynametab), _, _))) cls trns =
       case name_of_idf thy nsp_class cls
        of SOME cls =>
             let
@@ -651,11 +687,12 @@
           |-> (fn ((eqs, sortctxt), ty) => (pair o SOME) ((eqs, (sortctxt, ty)), map snd sortcontext)))
         end
     | [] => (NONE, trns)
-and ensure_def_inst thy (tabs as (_, (insttab, _, _))) (cls, tyco) trns =
+and ensure_def_inst thy (tabs as (_, ((insttab, thynametab), _, _))) (cls, tyco) trns =
   let
-    fun defgen_inst thy (tabs as (_, (insttab, _, _))) inst trns =
-      case Option.map (InstNameMangler.rev thy insttab) (name_of_idf thy nsp_inst inst)
-       of SOME (_, (class, tyco)) =>
+    fun defgen_inst thy (tabs as (_, ((insttab, thynametab), _, _))) inst trns =
+      case Option.map (InstNameMangler.rev thy insttab o NameSpace.base)
+            (name_of_idf thy nsp_inst inst)
+       of SOME (class, tyco) =>
             let
               val (arity, memdefs) = ClassPackage.the_inst_sign thy (class, tyco);
               val arity_typ = Type (tyco, (map TFree arity));
@@ -669,13 +706,16 @@
                       (ClassPackage.sortlookup thy ([supclass], arity_typ));
               fun gen_membr (m, ty) trns =
                 trns
+                |> tap (fn _ => writeln ("(1) " ^ m))
                 |> mk_fun thy tabs (m, ty)
+                |> tap (fn _ => writeln "(2)")
                 |-> (fn NONE => error ("could not derive definition for member "
                           ^ quote m ^ " :: " ^ Sign.string_of_typ thy ty)
                       | SOME (funn, sorts) => fold_map (fn (sort, sort_ctxt) =>
                           fold_map (exprgen_classlookup thy tabs)
                             (ClassPackage.sortlookup thy (sort, TFree sort_ctxt)))
-                            (sorts ~~ operational_arity)
+                            (print sorts ~~ print operational_arity)
+                #> tap (fn _ => writeln "(3)")
                 #-> (fn lss =>
                        pair (idf_of_name thy nsp_mem m, ((idf_of_name thy nsp_instmem m, funn), lss))));
             in
@@ -692,8 +732,9 @@
             end
         | _ =>
             trns |> fail ("no class instance found for " ^ quote inst);
-    val (_, thyname) = (the o AList.lookup (op =) (ClassPackage.the_instances thy cls)) tyco;
-    val inst = idf_of_name thy nsp_inst (InstNameMangler.get thy insttab (thyname, (cls, tyco)));
+    val thyname = (the o Symtab.lookup ((the o Symtab.lookup thynametab) cls)) tyco;
+    val inst = (idf_of_name thy nsp_inst o NameSpace.append thyname o InstNameMangler.get thy insttab)
+      (cls, tyco);
   in
     trns
     |> debug_msg (fn _ => "generating instance " ^ quote cls ^ " / " ^ quote tyco)
@@ -719,7 +760,7 @@
        of SOME m =>
             trns
             |> debug_msg (fn _ => "trying defgen class member for " ^ quote m)
-            |> ensure_def_class thy tabs ((the o ClassPackage.lookup_const_class thy) m)
+            |> ensure_def_class thy tabs ((the o AxClass.class_of thy) m)
             |-> (fn cls => succeed Bot)
         | _ =>
             trns |> fail ("no class member found for " ^ quote m)
@@ -932,20 +973,32 @@
 
 fun mk_tabs thy targets =
   let
-    fun mk_insttab thy =
-      InstNameMangler.empty
-      |> Symtab.fold_map
-          (fn (cls, clsinsts) => fold_map
-            (fn (tyco, thyname) => InstNameMangler.declare thy (thyname, (cls, tyco))) clsinsts)
-                 (ClassPackage.get_classtab thy)
-      |-> (fn _ => I);
+    fun mk_insttab thy = 
+      let
+        val insts = Symtab.fold
+          (fn (tyco, classes) => cons (tyco, map fst classes))
+          ((#arities o Sorts.rep_algebra o Sign.classes_of) thy)
+          []
+      in (
+        InstNameMangler.empty
+        |> fold
+            (fn (tyco, classes) => fold
+              (fn class => InstNameMangler.declare thy (class, tyco) #> snd) classes)
+                insts,
+        Symtab.empty
+        |> fold
+            (fn (tyco, classes) => fold
+              (fn class => Symtab.default (class, Symtab.empty)
+                #> Symtab.map_entry class (Symtab.update (tyco, thyname_of_instance thy (class, tyco)))) classes)
+                  insts
+      ) end;
     fun mk_overltabs thy =
       (Symtab.empty, ConstNameMangler.empty)
       |> Symtab.fold
           (fn (c, _) =>
             let
               val deftab = Theory.definitions_of thy c
-              val is_overl = (is_none o ClassPackage.lookup_const_class thy) c
+              val is_overl = (is_none o AxClass.class_of thy) c
                andalso case deftab   (* is_overloaded (!?) *)
                of [] => false
                 | [{lhs = ty, ...}] => not (Sign.typ_equiv thy (ty, Sign.the_const_type thy c))
diff -r b171fac592bb -r f992e507020e src/Pure/Tools/codegen_thingol.ML
--- a/src/Pure/Tools/codegen_thingol.ML	Wed Jun 28 14:35:10 2006 +0200
+++ b/src/Pure/Tools/codegen_thingol.ML	Wed Jun 28 14:35:51 2006 +0200
@@ -834,13 +834,17 @@
     fun prep_def def modl =
       (check_prep_def modl def, modl);
     fun invoke_generator name defgen modl =
-      defgen name (SOME name, modl)
-      handle FAIL (msgs, exc) =>
+      if ! soft_exc (*that's ! isn't a "not"...*)
+      then defgen name (SOME name, modl)
+        handle FAIL (msgs, exc) =>
+                if strict then raise FAIL (msg' :: msgs, exc)
+                else (Bot, modl)
+             | e => raise 
+                FAIL (["definition generator for " ^ quote name, msg'], SOME e)
+      else defgen name (SOME name, modl)
+        handle FAIL (msgs, exc) =>
               if strict then raise FAIL (msg' :: msgs, exc)
-              else (Bot, modl)
-           | e => raise if ! soft_exc
-                then FAIL (["definition generator for " ^ quote name, msg'], SOME e)
-                else e;
+              else (Bot, modl);
   in
     modl
     |> (if can (get_def modl) name