cleaned up

--- a/src/Pure/Tools/codegen_consts.ML	Mon Sep 25 17:04:20 2006 +0200
+++ b/src/Pure/Tools/codegen_consts.ML	Mon Sep 25 17:04:21 2006 +0200
@@ -18,10 +18,9 @@
   val norm_of_typ: theory -> string * typ -> const
   val find_def: theory -> const
     -> ((string (*theory name*) * thm) * typ list) option
-  val sortinsts: theory -> typ * typ -> (typ * sort) list
-  val class_of_classop: theory -> const -> class option
-  val insts_of_classop: theory -> const -> const list
-  val typ_of_classop: theory -> const -> typ
+  val disc_typ_of_classop: theory -> const -> typ
+  val disc_typ_of_const: theory -> (const -> typ) -> const -> typ
+  val consts_of: theory -> term -> const list * (string * typ) list
   val read_const: theory -> string -> const
   val string_of_const: theory -> const -> string
   val raw_string_of_const: const -> string
@@ -73,12 +72,6 @@
     get_first get_def specs
   end;
 
-fun sortinsts thy (ty, ty_decl) =
-  Vartab.empty
-  |> Sign.typ_match thy (ty_decl, ty) 
-  |> Vartab.dest
-  |> map (fn (_, (sort, ty)) => (ty, sort));
-
 fun mk_classop_typinst thy (c, tyco) =
   (c, [Type (tyco, map (fn v => TVar ((v, 0), Sign.defaultS thy (*for monotonicity*)))
     (Name.invents Name.context "'a" (Sign.arity_number thy tyco)))]);
@@ -101,28 +94,15 @@
 fun norm_of_typ thy (c, ty) =
   norm thy (c, Consts.typargs (Sign.consts_of thy) (c, ty));
 
-fun class_of_classop thy (c, [TVar _]) = 
-      AxClass.class_of_param thy c
-  | class_of_classop thy (c, [TFree _]) = 
-      AxClass.class_of_param thy c
-  | class_of_classop thy (c, _) = NONE;
-
-fun insts_of_classop thy (c_tys as (c, tys)) =
-  (*get rid of this finally*)
-  case AxClass.class_of_param thy c
-   of NONE => [c_tys]
-    | SOME class => let
-        val cs = maps (AxClass.params_of thy)
-          (Graph.all_succs ((#classes o Sorts.rep_algebra o Sign.classes_of) thy) [class])
-        fun add_tyco (tyco, classes) =
-          if member (op = o apsnd fst) classes class
-          then cons tyco else I;
-        val tycos =
-          Symtab.fold add_tyco
-            ((#arities o Sorts.rep_algebra o Sign.classes_of) thy) [];
-      in maps (fn c => map (fn tyco => mk_classop_typinst thy (c, tyco)) tycos) cs end;
-
-fun typ_of_classop thy (c, [TVar _]) = 
+fun disc_typ_of_classop thy (c, [TVar _]) = 
+      let
+        val class = (the o AxClass.class_of_param thy) c;
+        val (v, cs) = ClassPackage.the_consts_sign thy class
+      in
+        (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)
+      end
+  | disc_typ_of_classop thy (c, [TFree _]) = 
       let
         val class = (the o AxClass.class_of_param thy) c;
         val (v, cs) = ClassPackage.the_consts_sign thy class
@@ -130,15 +110,7 @@
         (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)
       end
-  | typ_of_classop thy (c, [TFree _]) = 
-      let
-        val class = (the o AxClass.class_of_param thy) c;
-        val (v, cs) = ClassPackage.the_consts_sign thy class
-      in
-        (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)
-      end
-  | typ_of_classop thy (c, [Type (tyco, _)]) =
+  | disc_typ_of_classop thy (c, [Type (tyco, _)]) =
       let
         val class = (the o AxClass.class_of_param thy) c;
         val (_, cs) = ClassPackage.the_inst_sign thy (class, tyco);
@@ -146,6 +118,16 @@
         Logic.varifyT ((the o AList.lookup (op =) cs) c)
       end;
 
+fun disc_typ_of_const thy f (const as (c, [ty])) =
+      if (is_some o AxClass.class_of_param thy) c
+      then disc_typ_of_classop thy const
+      else f const
+  | disc_typ_of_const thy f const = f const;
+
+fun consts_of thy t =
+  fold_aterms (fn Const c => cons (norm_of_typ thy c, c) | _ => I) t []
+  |> split_list;
+
 
 (* reading constants as terms *)
 

--- a/src/Pure/Tools/codegen_data.ML	Mon Sep 25 17:04:20 2006 +0200
+++ b/src/Pure/Tools/codegen_data.ML	Mon Sep 25 17:04:21 2006 +0200
@@ -26,7 +26,6 @@
   val get_datatype: theory -> string
     -> ((string * sort) list * (string * typ list) list) option
   val get_datatype_of_constr: theory -> CodegenConsts.const -> string option
-  val the_datatype_constrs: theory -> CodegenConsts.const list
 
   val print_thms: theory -> unit
 
@@ -130,9 +129,8 @@
           let
             val is_classop = (is_some o AxClass.class_of_param thy) c;
             val const = CodegenConsts.norm_of_typ thy c_ty;
-            val ty_decl = if is_classop
-              then CodegenConsts.typ_of_classop thy const
-              else snd (CodegenConsts.typ_of_inst thy const);
+            val ty_decl = CodegenConsts.disc_typ_of_const thy
+                (snd o CodegenConsts.typ_of_inst thy) const;
             val string_of_typ = setmp show_sorts true (Sign.string_of_typ thy);
           in if Sign.typ_equiv thy (ty_decl, ty)
             then (const, thm)
@@ -154,7 +152,7 @@
     fun constrain thm0 thm = case AxClass.class_of_param thy (fst c)
      of SOME _ =>
           let
-            val ty_decl = CodegenConsts.typ_of_classop thy c;
+            val ty_decl = CodegenConsts.disc_typ_of_classop thy c;
             val max = maxidx_of_typ ty_decl + 1;
             val thm = Thm.incr_indexes max thm;
             val ty = typ_func thy thm;
@@ -676,9 +674,6 @@
   Consttab.lookup ((the_dcontrs o get_exec) thy) c
   |> (Option.map o tap) (fn dtco => get_datatype thy dtco);
 
-fun the_datatype_constrs thy =
-  Consttab.keys ((the_dcontrs o get_exec) thy);
-
 
 
 (** code attributes **)