# HG changeset patch
# User haftmann
# Date 1175264343 -7200
# Node ID d1499fff65d8794cbd4f5d57ee388a0a09cf7382
# Parent  b860975e47b493c849baee928741f7b773c8403c
simplified constant representation in code generator

diff -r b860975e47b4 -r d1499fff65d8 src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Fri Mar 30 16:19:02 2007 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML	Fri Mar 30 16:19:03 2007 +0200
@@ -620,11 +620,10 @@
     fun add_eq_thms (dtco, (_, (vs, cs))) thy =
       let
         val thy_ref = Theory.self_ref thy;
-        val ty = Type (dtco, map TFree vs) |> Logic.varifyT;
-        val c = CodegenConsts.norm thy ("op =", [ty]);
+        val const = ("op =", SOME dtco);
         val get_thms = (fn () => get_eq (Theory.deref thy_ref) dtco |> rev);
       in
-        CodegenData.add_funcl (c, CodegenData.lazy get_thms) thy
+        CodegenData.add_funcl (const, CodegenData.lazy get_thms) thy
       end;
   in
     prove_codetypes_arities (ClassPackage.intro_classes_tac [])
diff -r b860975e47b4 -r d1499fff65d8 src/Pure/Tools/codegen_consts.ML
--- a/src/Pure/Tools/codegen_consts.ML	Fri Mar 30 16:19:02 2007 +0200
+++ b/src/Pure/Tools/codegen_consts.ML	Fri Mar 30 16:19:03 2007 +0200
@@ -8,17 +8,15 @@
 
 signature CODEGEN_CONSTS =
 sig
-  type const = string * typ list (*type instantiations*)
+  type const = string * string option (* constant name, possibly instance *)
   val const_ord: const * const -> order
   val eq_const: const * const -> bool
   structure Consttab: TABLE
-  val inst_of_typ: theory -> string * typ -> const
-  val typ_of_inst: theory -> const -> string * typ
-  val norm: theory -> const -> const
-  val norm_of_typ: theory -> string * typ -> const
-  val typ_sort_inst: Sorts.algebra -> typ * sort
-    -> sort Vartab.table -> sort Vartab.table
-  val typargs: theory -> string * typ -> typ list
+  val const_of_cexpr: theory -> string * typ -> const
+  val string_of_typ: theory -> typ -> string
+  val string_of_const: theory -> const -> string
+  val read_const: theory -> string -> const
+
   val co_of_const: theory -> const
     -> string * ((string * sort) list * (string * typ list))
   val co_of_const': theory -> const
@@ -29,13 +27,10 @@
     -> string * typ list -> const
   val consts_of_cos: theory -> string -> (string * sort) list
     -> (string * typ list) list -> const list
-  val find_def: theory -> const -> (string (*theory name*) * thm) option
-  val consts_of: theory -> term -> const list
-  val read_const: theory -> string -> const
-  val string_of_const: theory -> const -> string
-  val raw_string_of_const: const -> string
-  val string_of_const_typ: theory -> string * typ -> string
-  val string_of_typ: theory -> typ -> string
+
+  val typargs: theory -> string * typ -> typ list
+  val typ_sort_inst: Sorts.algebra -> typ * sort
+    -> sort Vartab.table -> sort Vartab.table
 end;
 
 structure CodegenConsts: CODEGEN_CONSTS =
@@ -44,124 +39,79 @@
 
 (* basic data structures *)
 
-type const = string * typ list (*type instantiations*);
-val const_ord = prod_ord fast_string_ord (list_ord Term.typ_ord);
+type const = string * string option;
+val const_ord = prod_ord fast_string_ord (option_ord string_ord);
 val eq_const = is_equal o const_ord;
 
 structure Consttab =
   TableFun(
-    type key = string * typ list;
+    type key = const;
     val ord = const_ord;
   );
 
-
-(* type instantiations, overloading, dictionary values *)
-
 fun string_of_typ thy = setmp show_sorts true (Sign.string_of_typ thy);
 
-fun inst_of_typ thy (c_ty as (c, ty)) =
-  (c, Sign.const_typargs thy c_ty);
 
-fun typ_of_inst thy (c_tys as (c, tys)) =
-  (c, Sign.const_instance thy c_tys);
+(* conversion between constant expressions and constants *)
 
-fun find_def thy (c, tys) =
-  let
-    val specs = Defs.specifications_of (Theory.defs_of thy) c;
-    val typ_instance = case AxClass.class_of_param thy c
-     of SOME _ => let
-          fun instance_tycos (Type (tyco1, _), Type (tyco2, _)) = tyco1 = tyco2
-            | instance_tycos (_ , TVar _) = true
-            | instance_tycos ty_ty = Sign.typ_instance thy ty_ty;
-        in instance_tycos end
-      | NONE =>  Sign.typ_instance thy;
-    fun get_def (_, { is_def, thyname, name, lhs, rhs }) =
-      if is_def andalso forall typ_instance (tys ~~ lhs) then
-        case try (Thm.get_axiom_i thy) name
-         of SOME thm => SOME (thyname, thm)
-          | NONE => NONE
-      else NONE
-  in
-    get_first get_def specs
-  end;
+fun const_of_cexpr thy (c_ty as (c, _)) =
+  case AxClass.class_of_param thy c
+   of SOME class => (case Sign.const_typargs thy c_ty
+       of [Type (tyco, _)] => if can (Sorts.mg_domain (Sign.classes_of thy) tyco) [class]
+              then (c, SOME tyco)
+              else (c, NONE)
+        | [_] => (c, NONE))
+    | NONE => (c, NONE);
 
-fun norm thy (c, insts) =
+fun string_of_const thy (c, NONE) = Sign.extern_const thy c
+  | string_of_const thy (c, SOME tyco) = Sign.extern_const thy c
+      ^ " " ^ enclose "[" "]" (Sign.extern_type thy tyco);
+
+
+(* reading constants as terms *)
+
+fun read_const thy raw_t =
   let
-    fun disciplined class [ty as Type (tyco, _)] =
-          let
-            val sorts = Sorts.mg_domain (Sign.classes_of thy) tyco [class]
-              handle CLASS_ERROR => error ("No such instance: " ^ tyco ^ " :: " ^ class
-                ^ ",\nrequired for overloaded constant " ^ c);
-            val vs = Name.invents Name.context "'a" (length sorts);
-          in
-            (c, [Type (tyco, map (fn v => TVar ((v, 0), [])) vs)])
-          end
-      | disciplined class _ =
-          (c, [TVar (("'a", 0), [class])]);
-  in case AxClass.class_of_param thy c
-   of SOME class => disciplined class insts
-    | NONE => inst_of_typ thy (c, Sign.the_const_type thy c)
-  end;
-
-fun norm_of_typ thy (c, ty) =
-  norm thy (c, Sign.const_typargs thy (c, ty));
-
-fun consts_of thy t =
-  fold_aterms (fn Const c => cons (norm_of_typ thy c) | _ => I) t []
-
-fun typ_sort_inst algebra =
-  let
-    val inters = Sorts.inter_sort algebra;
-    fun match _ [] = I
-      | match (TVar (v, S)) S' = Vartab.map_default (v, []) (fn S'' => inters (S, inters (S', S'')))
-      | match (Type (a, Ts)) S =
-          fold2 match Ts (Sorts.mg_domain algebra a S)
-  in uncurry match end;
-
-fun typargs thy (c_ty as (c, ty)) =
-  let
-    val opt_class = AxClass.class_of_param thy c;
-    val tys = Sign.const_typargs thy (c, ty);
-  in case (opt_class, tys)
-   of (SOME _, [Type (_, tys')]) => tys'
-    | _ => tys
+    val t = Sign.read_term thy raw_t;
+  in case try dest_Const t
+   of SOME c_ty => const_of_cexpr thy c_ty
+    | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t)
   end;
 
 
-(* printing *)
-
-fun string_of_const thy (c, tys) =
-  space_implode " " (Sign.extern_const thy c
-    :: map (enclose "[" "]" o Sign.string_of_typ thy) tys);
-
-fun raw_string_of_const (c, tys) =
-  space_implode " " (c
-    :: map (enclose "[" "]" o Display.raw_string_of_typ) tys);
-
-fun string_of_const_typ thy (c, ty) =
-  string_of_const thy (c, Consts.typargs (Sign.consts_of thy) (c, ty));
-
-
-(* conversion between constants and datatype constructors *)
+(* conversion between constants, constant expressions and datatype constructors *)
 
 fun const_of_co thy tyco vs (co, tys) =
-  norm_of_typ thy (co, tys ---> Type (tyco, map TFree vs));
+  const_of_cexpr thy (co, tys ---> Type (tyco, map TFree vs));
 
 fun consts_of_cos thy tyco vs cos =
   let
     val dty = Type (tyco, map TFree vs);
-    fun mk_co (co, tys) = norm_of_typ thy (co, tys ---> dty);
+    fun mk_co (co, tys) = const_of_cexpr thy (co, tys ---> dty);
   in map mk_co cos end;
 
 local
 
 exception BAD of string;
 
+fun mg_typ_of_const thy (c, NONE) = Sign.the_const_type thy c
+  | mg_typ_of_const thy (c, SOME tyco) =
+      let
+        val SOME class = AxClass.class_of_param thy c;
+        val ty = Sign.the_const_type thy c;
+          (*an approximation*)
+        val sorts = Sorts.mg_domain (Sign.classes_of thy) tyco [class]
+          handle CLASS_ERROR => raise BAD ("No such instance: " ^ tyco ^ " :: " ^ class
+            ^ ",\nrequired for overloaded constant " ^ c);
+        val vs = Name.invents Name.context "'a" (length sorts);
+      in map_atyps (K (Type (tyco, map (fn v => TVar ((v, 0), [])) vs))) ty end;
+
 fun gen_co_of_const thy const =
   let
-    val (c, ty) = (apsnd Logic.unvarifyT o typ_of_inst thy) const;
+    val (c, _) = const;
+    val ty = (Logic.unvarifyT o mg_typ_of_const thy) const;
     fun err () = raise BAD
-     ("Illegal type for datatype constructor: " ^ Sign.string_of_typ thy ty);
+     ("Illegal type for datatype constructor: " ^ string_of_typ thy ty);
     val (tys, ty') = strip_type ty;
     val (tyco, vs) = ((apsnd o map) dest_TFree o dest_Type) ty'
       handle TYPE _ => err ();
@@ -197,18 +147,26 @@
   in (tyco, (vs, cos)) end;
 
 
-(* reading constants as terms *)
+(* dictionary values *)
 
-fun read_const_typ thy raw_t =
+fun typargs thy (c_ty as (c, ty)) =
   let
-    val t = Sign.read_term thy raw_t
-  in case try dest_Const t
-   of SOME c_ty => (typ_of_inst thy o norm_of_typ thy) c_ty
-    | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t)
+    val opt_class = AxClass.class_of_param thy c;
+    val tys = Sign.const_typargs thy (c, ty);
+  in case (opt_class, tys)
+   of (SOME class, ty as [Type (tyco, tys')]) =>
+        if can (Sorts.mg_domain (Sign.classes_of thy) tyco) [class]
+        then tys' else ty
+    | _ => tys
   end;
 
-fun read_const thy =
-  norm_of_typ thy o read_const_typ thy;
-
+fun typ_sort_inst algebra =
+  let
+    val inters = Sorts.inter_sort algebra;
+    fun match _ [] = I
+      | match (TVar (v, S)) S' = Vartab.map_default (v, []) (fn S'' => inters (S, inters (S', S'')))
+      | match (Type (a, Ts)) S =
+          fold2 match Ts (Sorts.mg_domain algebra a S)
+  in uncurry match end;
 
 end;
diff -r b860975e47b4 -r d1499fff65d8 src/Pure/Tools/codegen_data.ML
--- a/src/Pure/Tools/codegen_data.ML	Fri Mar 30 16:19:02 2007 +0200
+++ b/src/Pure/Tools/codegen_data.ML	Fri Mar 30 16:19:03 2007 +0200
@@ -27,10 +27,9 @@
   val coregular_algebra: theory -> Sorts.algebra
   val operational_algebra: theory -> (sort -> sort) * Sorts.algebra
   val these_funcs: theory -> CodegenConsts.const -> thm list
-  val tap_typ: theory -> CodegenConsts.const -> typ option
   val get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list)
   val get_datatype_of_constr: theory -> CodegenConsts.const -> string option
-  val get_constr_typ: theory -> CodegenConsts.const -> typ option
+  val default_typ: theory -> CodegenConsts.const -> typ
 
   val preprocess_cterm: cterm -> thm
 
@@ -454,7 +453,7 @@
     val vs = Name.invents Name.context "" (Sign.arity_number thy tyco);
     val clsops = (these o Option.map snd o try (AxClass.params_of_class thy)) class;
     val funcs = clsops
-      |> map (fn (clsop, _) => CodegenConsts.norm thy (clsop, [Type (tyco, map (TFree o rpair []) vs)]))
+      |> map (fn (clsop, _) => (clsop, SOME tyco))
       |> map (Consttab.lookup ((the_funcs o get_exec) thy))
       |> (map o Option.map) (Susp.force o fst)
       |> maps these
@@ -518,7 +517,7 @@
     val thy = Thm.theory_of_thm thm;
     val raw_funcs = CodegenFunc.mk_func strict thm;
     val error_warning = if strict then error else warning #> K NONE;
-    fun check_typ_classop class (const as (c, [Type (tyco, _)]), thm) =
+    fun check_typ_classop class (const as (c, SOME tyco), thm) =
           let
             val ((_, ty), _) = CodegenFunc.dest_func thm;
             val ty_decl = classop_weakest_typ thy class (c, tyco);
@@ -547,7 +546,7 @@
               ^ "\nis incompatible with permitted least general type\n"
               ^ CodegenConsts.string_of_typ thy ty_strongest)
           end
-      | check_typ_classop class ((c, [_]), thm) =
+      | check_typ_classop class ((c, NONE), thm) =
           error_warning ("Illegal type for class operation " ^ quote c
            ^ "\nin defining equation\n"
            ^ string_of_thm thm);
@@ -563,7 +562,7 @@
            ^ "\nis incompatible declared function type\n"
            ^ CodegenConsts.string_of_typ thy ty_decl)
       end;
-    fun check_typ (const as (c, tys), thm) =
+    fun check_typ (const as (c, _), thm) =
       case AxClass.class_of_param thy c
        of SOME class => check_typ_classop class (const, thm)
         | NONE => check_typ_fun (const, thm);
@@ -599,12 +598,12 @@
        (del_thm thm)) funcs)) thy
   end;
 
-fun add_funcl (c, lthms) thy =
+fun add_funcl (const, lthms) thy =
   let
-    val c' = CodegenConsts.norm thy c;
-    val lthms' = certificate thy (fn thy => certify_const thy c' o maps (CodegenFunc.mk_func true)) lthms;
+    val lthms' = certificate thy (fn thy => certify_const thy const
+      o maps (CodegenFunc.mk_func true)) lthms;
   in
-    map_exec_purge (SOME [c]) (map_funcs (Consttab.map_default (c', (Susp.value [], []))
+    map_exec_purge (SOME [const]) (map_funcs (Consttab.map_default (const, (Susp.value [], []))
       (add_lthms lthms'))) thy
   end;
 
@@ -682,8 +681,8 @@
   | apply_preproc thy f (thms as (thm :: _)) =
       let
         val thms' = f thy thms;
-        val c = (CodegenConsts.norm_of_typ thy o fst o CodegenFunc.dest_func) thm;
-      in (certify_const thy c o map CodegenFunc.mk_head) thms' end;
+        val thms'' as ((const, _) :: _) = map CodegenFunc.mk_head thms'
+      in (certify_const thy const o map CodegenFunc.mk_head) thms' end;
 
 fun cmp_thms thy =
   make_ord (fn (thm1, thm2) => not (Sign.typ_instance thy (CodegenFunc.typ_func thm1, CodegenFunc.typ_func thm2)));
@@ -716,44 +715,6 @@
 
 end; (*local*)
 
-local
-
-fun get_funcs thy const =
-  Consttab.lookup ((the_funcs o get_exec) thy) const
-  |> Option.map (Susp.force o fst)
-  |> these
-  |> map (Thm.transfer thy);
-
-in
-
-fun these_funcs thy const =
-  let
-    fun get_prim_def_funcs (const as (c, tys)) =
-      case CodegenConsts.find_def thy const
-       of SOME (_, thm) =>
-            thm
-            |> Thm.transfer thy
-            |> gen_mk_func_typ false
-            |> map (CodegenFunc.expand_eta ~1 o snd)
-        | NONE => []
-    fun drop_refl thy = filter_out (is_equal o Term.fast_term_ord o Logic.dest_equals
-      o ObjectLogic.drop_judgment thy o Drule.plain_prop_of);
-    val funcs = case get_funcs thy const
-     of [] => get_prim_def_funcs const
-    | funcs => funcs
-  in
-    funcs
-    |> preprocess thy
-    |> drop_refl thy
-  end;
-
-fun tap_typ thy const =
-  case get_funcs thy const
-   of thm :: _ => SOME (CodegenFunc.typ_func thm)
-    | [] => NONE;
-
-end; (*local*)
-
 fun get_datatype thy tyco =
   case Symtab.lookup ((the_dtyps o get_exec) thy) tyco
    of SOME spec => spec
@@ -781,6 +742,65 @@
         |> SOME end
     | NONE => NONE;
 
+fun default_typ_proto thy (const as (c, SOME tyco)) = classop_weakest_typ thy
+      ((the o AxClass.class_of_param thy) c) (c, tyco) |> SOME
+  | default_typ_proto thy (const as (c, NONE)) = case AxClass.class_of_param thy c
+       of SOME class => SOME (Term.map_type_tvar
+            (K (TVar (("'a", 0), [class]))) (Sign.the_const_type thy c))
+        | NONE => get_constr_typ thy const;
+
+local
+
+fun get_funcs thy const =
+  Consttab.lookup ((the_funcs o get_exec) thy) const
+  |> Option.map (Susp.force o fst)
+  |> these
+  |> map (Thm.transfer thy);
+
+fun find_def thy (const as (c, _)) =
+  let
+    val specs = Defs.specifications_of (Theory.defs_of thy) c;
+    val ty = case try (default_typ_proto thy) const
+     of NONE => NONE
+      | SOME ty => ty;
+    val tys = Sign.const_typargs thy (c, ty |> the_default (Sign.the_const_type thy c));
+    fun get_def (_, { is_def, name, lhs, rhs, thyname }) =
+      if is_def andalso forall (Sign.typ_instance thy) (tys ~~ lhs) then
+        try (Thm.get_axiom_i thy) name
+      else NONE
+  in get_first get_def specs end;
+
+in
+
+fun these_funcs thy const =
+  let
+    fun get_prim_def_funcs (const as (c, tys)) =
+      case find_def thy const
+       of SOME thm =>
+            thm
+            |> Thm.transfer thy
+            |> gen_mk_func_typ false
+            |> map (CodegenFunc.expand_eta ~1 o snd)
+        | NONE => []
+    fun drop_refl thy = filter_out (is_equal o Term.fast_term_ord o Logic.dest_equals
+      o ObjectLogic.drop_judgment thy o Drule.plain_prop_of);
+    val funcs = case get_funcs thy const
+     of [] => get_prim_def_funcs const
+    | funcs => funcs
+  in
+    funcs
+    |> preprocess thy
+    |> drop_refl thy
+  end;
+
+fun default_typ thy (const as (c, _)) = case default_typ_proto thy const
+ of SOME ty => ty
+  | NONE => (case get_funcs thy const
+     of thm :: _ => CodegenFunc.typ_func thm
+      | [] => Sign.the_const_type thy c);
+
+end; (*local*)
+
 
 (** code attributes **)
 
diff -r b860975e47b4 -r d1499fff65d8 src/Pure/Tools/codegen_func.ML
--- a/src/Pure/Tools/codegen_func.ML	Fri Mar 30 16:19:02 2007 +0200
+++ b/src/Pure/Tools/codegen_func.ML	Fri Mar 30 16:19:03 2007 +0200
@@ -75,7 +75,7 @@
   o Drule.fconv_rule Drule.beta_eta_conversion);
 
 val mk_head = lift_thm_thy (fn thy => fn thm =>
-  ((CodegenConsts.norm_of_typ thy o fst o dest_func) thm, thm));
+  ((CodegenConsts.const_of_cexpr thy o fst o dest_func) thm, thm));
 
 local
 
diff -r b860975e47b4 -r d1499fff65d8 src/Pure/Tools/codegen_funcgr.ML
--- a/src/Pure/Tools/codegen_funcgr.ML	Fri Mar 30 16:19:02 2007 +0200
+++ b/src/Pure/Tools/codegen_funcgr.ML	Fri Mar 30 16:19:03 2007 +0200
@@ -80,7 +80,7 @@
       let
         val thy = Thm.theory_of_thm thm;
         val is_refl = curry CodegenConsts.eq_const const;
-        fun the_const c = case try (CodegenConsts.norm_of_typ thy) c
+        fun the_const c = case try (CodegenConsts.const_of_cexpr thy) c
          of SOME const => if is_refl const then I else insert CodegenConsts.eq_const const
           | NONE => I
       in fold_consts the_const thms [] end;
@@ -147,7 +147,7 @@
 
 fun resort_funcss thy algebra funcgr =
   let
-    val typ_funcgr = try (fst o Constgraph.get_node funcgr o CodegenConsts.norm_of_typ thy);
+    val typ_funcgr = try (fst o Constgraph.get_node funcgr o CodegenConsts.const_of_cexpr thy);
     fun resort_dep (const, thms) = (const, resort_thms algebra typ_funcgr thms)
       handle Sorts.CLASS_ERROR e => raise INVALID ([const], Sorts.msg_class_error (Sign.pp thy) e
                     ^ ",\nfor constant " ^ CodegenConsts.string_of_const thy const
@@ -162,7 +162,7 @@
           in (Sign.typ_equiv thy (ty, ty'), (const, thms')) end;
     fun resort_recs funcss =
       let
-        fun tap_typ c_ty = case try (CodegenConsts.norm_of_typ thy) c_ty
+        fun tap_typ c_ty = case try (CodegenConsts.const_of_cexpr thy) c_ty
          of SOME const => AList.lookup (CodegenConsts.eq_const) funcss const
               |> these
               |> try hd
@@ -177,14 +177,6 @@
       in if unchanged then funcss' else resort_rec_until funcss' end;
   in map resort_dep #> resort_rec_until end;
 
-fun classop_const thy algebra class classop tyco =
-  let
-    val sorts = Sorts.mg_domain algebra tyco [class]
-    val (var, _) = try (AxClass.params_of_class thy) class |> the_default ("'a", []);
-    val vs = Name.names (Name.declare var Name.context) "'a" sorts;
-    val arity_typ = Type (tyco, map TFree vs);
-  in (classop, [arity_typ]) end;
-
 fun instances_of thy algebra insts =
   let
     val thy_classes = (#classes o Sorts.rep_algebra o Sign.classes_of) thy;
@@ -192,8 +184,7 @@
       try (AxClass.params_of_class thy) class
       |> Option.map snd
       |> these
-      |> map (fn (c, _) => classop_const thy algebra class c tyco)
-      |> map (CodegenConsts.norm thy)
+      |> map (fn (c, _) => (c, SOME tyco))
   in
     Symtab.empty
     |> fold (fn (tyco, class) =>
@@ -204,9 +195,9 @@
 
 fun instances_of_consts thy algebra funcgr consts =
   let
-    fun inst (const as (c, ty)) = case try (CodegenConsts.norm_of_typ thy) const
-     of SOME const => insts_of thy algebra c (fst (Constgraph.get_node funcgr const)) ty
-      | NONE => [];
+    fun inst (cexpr as (c, ty)) = insts_of thy algebra c
+      ((fst o Constgraph.get_node funcgr o CodegenConsts.const_of_cexpr thy) cexpr)
+      ty handle CLASS_ERROR => [];
   in
     []
     |> fold (fold (insert (op =)) o inst) consts
@@ -248,44 +239,23 @@
     val funcss = raw_funcss
       |> resort_funcss thy algebra funcgr
       |> filter_out (can (Constgraph.get_node funcgr) o fst);
-    fun classop_typ (c, [typarg]) class =
-      let
-        val ty = Sign.the_const_type thy c;
-        val inst = case typarg
-         of Type (tyco, _) => classop_const thy algebra class c tyco
-              |> snd
-              |> the_single
-              |> Logic.varifyT
-          | _ => TVar (("'a", 0), [class]);
-      in Term.map_type_tvar (K inst) ty end;
-    fun default_typ (const as (c, tys)) = case AxClass.class_of_param thy c
-         of SOME class => classop_typ const class
-          | NONE => (case CodegenData.tap_typ thy const
-             of SOME ty => ty
-              | NONE => (case CodegenData.get_constr_typ thy const
-                 of SOME ty => ty
-                  | NONE => Sign.the_const_type thy c))
-    fun typ_func (const as (c, tys)) thms thm =
-      let
-        val ty = CodegenFunc.typ_func thm;
-      in case AxClass.class_of_param thy c
-       of SOME class => (case tys
-           of [Type _] => let val ty_decl = classop_typ const class
-              in if Sign.typ_equiv thy (ty, ty_decl) then ty
-              else raise raise INVALID ([const], "Illegal instantation for class operation "
-                    ^ CodegenConsts.string_of_const thy const
-                    ^ ":\n" ^ CodegenConsts.string_of_typ thy ty_decl
-                    ^ "\nto " ^ CodegenConsts.string_of_typ thy ty
-                    ^ "\nin defining equations\n"
-                    ^ (cat_lines o map string_of_thm) thms)
-              end
-            | _ => ty)
-        | NONE => ty
-      end;
-    fun add_funcs (const, thms as thm :: _) =
-          Constgraph.new_node (const, (typ_func const thms thm, thms))
-      | add_funcs (const, []) =
-          Constgraph.new_node (const, (default_typ const, []));
+    fun typ_func const [] = CodegenData.default_typ thy const
+      | typ_func (_, NONE) (thm :: _) = CodegenFunc.typ_func thm
+      | typ_func (const as (c, SOME tyco)) (thms as (thm :: _)) =
+          let
+            val ty = CodegenFunc.typ_func thm;
+            val SOME class = AxClass.class_of_param thy c;
+            val sorts_decl = Sorts.mg_domain algebra tyco [class];
+            val tys = CodegenConsts.typargs thy (c, ty);
+            val sorts = map (snd o dest_TVar) tys;
+          in if sorts = sorts_decl then ty
+            else raise INVALID ([const], "Illegal instantation for class operation "
+              ^ CodegenConsts.string_of_const thy const
+              ^ "\nin defining equations\n"
+              ^ (cat_lines o map string_of_thm) thms)
+          end;
+    fun add_funcs (const, thms) =
+      Constgraph.new_node (const, (typ_func const thms, thms));
     fun add_deps (funcs as (const, thms)) funcgr =
       let
         val deps = consts_of funcs;
@@ -339,6 +309,8 @@
 
 fun ensure_consts_term rewrites thy f ct funcgr =
   let
+    fun consts_of thy t =
+      fold_aterms (fn Const c => cons (CodegenConsts.const_of_cexpr thy c) | _ => I) t []
     fun rhs_conv conv thm =
       let
         val thm' = (conv o snd o Drule.dest_equals o Thm.cprop_of) thm;
@@ -348,12 +320,12 @@
     val thm1 = CodegenData.preprocess_cterm ct
       |> fold (rhs_conv o MetaSimplifier.rewrite false o single) (rewrites thy);
     val ct' = Drule.dest_equals_rhs (Thm.cprop_of thm1);
-    val consts = CodegenConsts.consts_of thy (Thm.term_of ct');
+    val consts = consts_of thy (Thm.term_of ct');
     val funcgr' = ensure_consts rewrites thy consts funcgr;
     val algebra = CodegenData.coregular_algebra thy;
     val (_, thm2) = Thm.varifyT' [] thm1;
     val thm3 = Thm.reflexive (Drule.dest_equals_rhs (Thm.cprop_of thm2));
-    val typ_funcgr = try (fst o Constgraph.get_node funcgr' o CodegenConsts.norm_of_typ thy);
+    val typ_funcgr = try (fst o Constgraph.get_node funcgr' o CodegenConsts.const_of_cexpr thy);
     val [thm4] = resort_thms algebra typ_funcgr [thm3];
     val tfrees = Term.add_tfrees (Thm.prop_of thm1) [];
     fun inst thm =
diff -r b860975e47b4 -r d1499fff65d8 src/Pure/Tools/codegen_names.ML
--- a/src/Pure/Tools/codegen_names.ML	Fri Mar 30 16:19:02 2007 +0200
+++ b/src/Pure/Tools/codegen_names.ML	Fri Mar 30 16:19:03 2007 +0200
@@ -216,23 +216,21 @@
 fun instance_policy thy = policy thy (fn (class, tyco) => 
   NameSpace.base class ^ "_" ^ NameSpace.base tyco) thyname_of_instance;
 
-fun force_thyname thy (const as (c, tys)) =
+fun force_thyname thy (const as (c, opt_tyco)) =
   case AxClass.class_of_param thy c
-   of SOME class => (case tys
-       of [Type (tyco, _)] => SOME (thyname_of_instance thy (class, tyco))
-        | _ => SOME (thyname_of_class thy class))
+   of SOME class => (case opt_tyco
+       of SOME tyco => SOME (thyname_of_instance thy (class, tyco))
+        | NONE => SOME (thyname_of_class thy class))
     | NONE => (case CodegenData.get_datatype_of_constr thy const
    of SOME dtco => SOME (thyname_of_tyco thy dtco)
-    | NONE => (case CodegenConsts.find_def thy const
-   of SOME (thyname, _) => SOME thyname
-    | NONE => NONE));
+    | NONE => NONE);
 
-fun const_policy thy (c, tys) =
-  case force_thyname thy (c, tys)
+fun const_policy thy (const as (c, opt_tyco)) =
+  case force_thyname thy const
    of NONE => policy thy NameSpace.base thyname_of_const c
     | SOME thyname => let
         val prefix = (purify_prefix o NameSpace.explode o dotify) thyname;
-        val tycos = map_filter (fn Type (tyco, _) => SOME tyco | _ => NONE) tys;
+        val tycos = the_list opt_tyco;
         val base = map (purify_base o NameSpace.base) (c :: tycos);
       in NameSpace.implode (prefix @ [space_implode "_" base]) end;
 
@@ -307,7 +305,7 @@
 structure ConstName = CodeDataFun
 (struct
   val name = "Pure/codegen_names";
-  type T = const Consttab.table * (string * typ list) Symtab.table;
+  type T = const Consttab.table * (string * string option) Symtab.table;
   val empty = (Consttab.empty, Symtab.empty);
   fun merge _ ((const1, constrev1), (const2, constrev2)) =
     (Consttab.merge eq_string (const1, const2),
@@ -395,8 +393,7 @@
   get thy #instance StringPairTab.lookup map_instance StringPairTab.update instance_policy
   #> add_idf idf_instance;
 fun const thy =
-  CodegenConsts.norm thy
-  #> get_const thy
+  get_const thy
   #> add_idf idf_const;
 
 fun class_rev thy =
diff -r b860975e47b4 -r d1499fff65d8 src/Pure/Tools/codegen_package.ML
--- a/src/Pure/Tools/codegen_package.ML	Fri Mar 30 16:19:02 2007 +0200
+++ b/src/Pure/Tools/codegen_package.ML	Fri Mar 30 16:19:03 2007 +0200
@@ -141,7 +141,7 @@
     val (v, cs) = AxClass.params_of_class thy class;
     val class' = CodegenNames.class thy class;
     val classrels' = map (curry (CodegenNames.classrel thy) class) superclasses;
-    val classops' = map (CodegenNames.const thy o CodegenConsts.norm_of_typ thy) cs;
+    val classops' = map (CodegenNames.const thy o CodegenConsts.const_of_cexpr thy) cs;
     val defgen_class =
       fold_map (ensure_def_class thy algbr funcgr strct) superclasses
       ##>> (fold_map (exprgen_type thy algbr funcgr strct) o map snd) cs
@@ -170,7 +170,7 @@
             ||>> fold_map (fn (c, tys) =>
               fold_map (exprgen_type thy algbr funcgr strct) tys
               #-> (fn tys' =>
-                pair ((CodegenNames.const thy o CodegenConsts.norm_of_typ thy)
+                pair ((CodegenNames.const thy o CodegenConsts.const_of_cexpr thy)
                   (c, tys ---> Type (tyco, map TFree vs)), tys'))) cos
             |-> (fn (vs, cos) => succeed (CodegenThingol.Datatype (vs, cos)))
           end;
@@ -235,7 +235,7 @@
   end
 and exprgen_dict_parms thy (algbr as (_, consts)) funcgr strct (c, ty_ctxt) =
   let
-    val c' = CodegenConsts.norm_of_typ thy (c, ty_ctxt)
+    val c' = CodegenConsts.const_of_cexpr thy (c, ty_ctxt)
     val idf = CodegenNames.const thy c';
     val ty_decl = Consts.the_declaration consts idf;
     val (tys, tys_decl) = pairself (curry (Consts.typargs consts) idf) (ty_ctxt, ty_decl);
@@ -258,7 +258,7 @@
             (superclass, (classrel, (inst, dss))));
     fun gen_classop_def (classop as (c, ty)) trns =
       trns
-      |> ensure_def_const thy algbr funcgr strct (CodegenConsts.norm_of_typ thy classop)
+      |> ensure_def_const thy algbr funcgr strct (CodegenConsts.const_of_cexpr thy classop)
       ||>> exprgen_term thy algbr funcgr strct (Const (c, map_type_tfree (K arity_typ) ty));
     fun defgen_inst trns =
       trns
@@ -276,13 +276,13 @@
     |> ensure_def thy defgen_inst true ("generating instance " ^ quote class ^ " / " ^ quote tyco) inst
     |> pair inst
   end
-and ensure_def_const thy (algbr as (_, consts)) funcgr strct (c_tys as (c, tys)) trns =
+and ensure_def_const thy (algbr as (_, consts)) funcgr strct (const as (c, opt_tyco)) trns =
   let
-    val c' = CodegenNames.const thy c_tys;
+    val c' = CodegenNames.const thy const;
     fun defgen_datatypecons trns =
       trns
       |> ensure_def_tyco thy algbr funcgr strct
-          ((the o CodegenData.get_datatype_of_constr thy) c_tys)
+          ((the o CodegenData.get_datatype_of_constr thy) const)
       |-> (fn _ => succeed CodegenThingol.Bot);
     fun defgen_classop trns =
       trns
@@ -290,7 +290,7 @@
       |-> (fn _ => succeed CodegenThingol.Bot);
     fun defgen_fun trns =
       case CodegenFuncgr.funcs funcgr
-        (perhaps (Consttab.lookup ((snd o snd o CodegenPackageData.get) thy)) c_tys)
+        (perhaps (Consttab.lookup ((snd o snd o CodegenPackageData.get) thy)) const)
        of thms as _ :: _ =>
             let
               val (ty, eq_thms) = prep_eqs thy thms;
@@ -315,20 +315,20 @@
         | [] =>
               trns
               |> fail ("No defining equations found for "
-                   ^ (quote o CodegenConsts.string_of_const thy) c_tys);
-    val defgen = if (is_some o CodegenData.get_datatype_of_constr thy) c_tys
+                   ^ (quote o CodegenConsts.string_of_const thy) const);
+    val defgen = if (is_some o CodegenData.get_datatype_of_constr thy) const
       then defgen_datatypecons
-      else if (is_some o AxClass.class_of_param thy) c andalso
-        case tys of [TFree _] => true | [TVar _] => true | _ => false
-      then defgen_classop
-      else defgen_fun
+      else if is_some opt_tyco
+        orelse (not o is_some o AxClass.class_of_param thy) c
+      then defgen_fun
+      else defgen_classop
     val strict = check_strict strct (CodegenSerializer.const_has_serialization thy) c';
   in
     trns
     |> tracing (fn _ => "generating constant "
-        ^ (quote o CodegenConsts.string_of_const thy) c_tys)
+        ^ (quote o CodegenConsts.string_of_const thy) const)
     |> ensure_def thy defgen strict ("generating constant "
-         ^ CodegenConsts.string_of_const thy c_tys) c'
+         ^ CodegenConsts.string_of_const thy const) c'
     |> pair c'
   end
 and exprgen_term thy algbr funcgr strct (Const (c, ty)) trns =
@@ -359,7 +359,7 @@
             |>> (fn (t, ts) => t `$$ ts)
 and appgen_default thy algbr funcgr strct ((c, ty), ts) trns =
   trns
-  |> ensure_def_const thy algbr funcgr strct (CodegenConsts.norm_of_typ thy (c, ty))
+  |> ensure_def_const thy algbr funcgr strct (CodegenConsts.const_of_cexpr thy (c, ty))
   ||>> fold_map (exprgen_type thy algbr funcgr strct) ((fst o Term.strip_type) ty)
   ||>> exprgen_type thy algbr funcgr strct ((snd o Term.strip_type) ty)
   ||>> exprgen_dict_parms thy algbr funcgr strct (c, ty)
@@ -483,14 +483,11 @@
 
 local
 
-fun add_consts thy f (c1, c2 as (c, tys)) =
+fun add_consts thy f (c1, c2 as (c, opt_tyco)) =
   let
-    val _ = case tys
-     of [TVar _] => if is_some (AxClass.class_of_param thy c)
-          then error ("Not a function: " ^ CodegenConsts.string_of_const thy c2)
-          else ()
-      | _ => ();
-    val _ = if is_some (CodegenData.get_datatype_of_constr thy c2)
+    val _ = if
+        is_some (AxClass.class_of_param thy c) andalso is_none opt_tyco
+        orelse is_some (CodegenData.get_datatype_of_constr thy c2)
       then error ("Not a function: " ^ CodegenConsts.string_of_const thy c2)
       else ();
     val funcgr = Funcgr.make thy [c1, c2];
@@ -548,10 +545,10 @@
 
 in
 
-val abstyp = gen_abstyp CodegenConsts.norm Sign.certify_typ;
+val abstyp = gen_abstyp (K I) Sign.certify_typ;
 val abstyp_e = gen_abstyp CodegenConsts.read_const (fn thy => Sign.read_typ (thy, K NONE));
 
-val constsubst = gen_constsubst CodegenConsts.norm;
+val constsubst = gen_constsubst (K I);
 val constsubst_e = gen_constsubst CodegenConsts.read_const;
 
 end; (*local*)
@@ -608,16 +605,27 @@
 fun consts_of thy thyname =
   let
     val this_thy = Option.map theory thyname |> the_default thy;
-    val defs = (#defs o rep_theory) this_thy;
-    val cs_names = (Symtab.keys o snd o #constants o Consts.dest o #consts o Sign.rep_sg) this_thy;
-    val consts = maps (fn c => (map (fn tys => CodegenConsts.norm thy (c, tys))
-      o map #lhs o filter #is_def o map snd o Defs.specifications_of defs) c) cs_names;
-    fun is_const thyname (c, _) =
-      (*this is an approximation*)
-      not (exists (fn thy => Sign.declared_const thy c) (Theory.parents_of this_thy))
+    val defs = (#defs o rep_theory) thy;
+    val cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
+      ((snd o #constants o Consts.dest o #consts o Sign.rep_sg) this_thy) [];
+    fun classop c = case AxClass.class_of_param thy c
+     of NONE => [(c, NONE)]
+      | SOME class => Symtab.fold
+          (fn (tyco, classes) => if AList.defined (op =) classes class
+            then cons (c, SOME tyco) else I)
+          ((#arities o Sorts.rep_algebra o Sign.classes_of) this_thy)
+          [(c, NONE)];
+    val consts = maps classop cs;
+    fun test_instance thy (class, tyco) =
+      can (Sorts.mg_domain (Sign.classes_of thy) tyco) [class]
+    fun belongs_here thyname (c, NONE) =
+          not (exists (fn thy => Sign.declared_const thy c) (Theory.parents_of this_thy))
+      | belongs_here thyname (c, SOME tyco) =
+          not (exists (fn thy => test_instance thy ((the o AxClass.class_of_param thy) c, tyco))
+            (Theory.parents_of this_thy))
   in case thyname
    of NONE => consts
-    | SOME thyname => filter (is_const thyname) consts
+    | SOME thyname => filter (belongs_here thyname) consts
   end;
 
 fun filter_generatable thy targets consts =
diff -r b860975e47b4 -r d1499fff65d8 src/Pure/Tools/codegen_serializer.ML
--- a/src/Pure/Tools/codegen_serializer.ML	Fri Mar 30 16:19:02 2007 +0200
+++ b/src/Pure/Tools/codegen_serializer.ML	Fri Mar 30 16:19:03 2007 +0200
@@ -11,7 +11,7 @@
   include BASIC_CODEGEN_THINGOL;
 
   val add_syntax_class: string -> class
-    -> (string * ((string * typ list) * string) list) option -> theory -> theory;
+    -> (string * (CodegenConsts.const * string) list) option -> theory -> theory;
   val add_syntax_inst: string -> string * class -> bool -> theory -> theory;
   val add_syntax_tycoP: string -> string -> OuterParse.token list
     -> (theory -> theory) * OuterParse.token list;
@@ -422,7 +422,7 @@
     and pr_bind' ((NONE, NONE), _) = str "_"
       | pr_bind' ((SOME v, NONE), _) = str v
       | pr_bind' ((NONE, SOME p), _) = p
-      | pr_bind' ((SOME v, SOME p), _) = concat [str v, str "as", p]
+      | pr_bind' ((SOME v, SOME p), _) = 
     and pr_bind fxy = gen_pr_bind pr_bind' pr_term fxy;
     fun pr_def (MLFuns (funns as (funn :: funns'))) =
           let
@@ -889,7 +889,7 @@
 val code_width = ref 80;
 fun code_output p = Pretty.setmp_margin (!code_width) Pretty.output p ^ "\n";
 
-fun seri_ml pr_def pr_modl output labelled_name reserved_user module_alias module_prolog
+fun seri_ml pr_def pr_modl reserved_ml output labelled_name reserved_user module_alias module_prolog
   (_ : string -> class_syntax option) tyco_syntax const_syntax code =
   let
     val is_cons = fn node => case CodegenThingol.get_def code node
@@ -898,7 +898,7 @@
     datatype node =
         Def of string * ml_def option
       | Module of string * ((Name.context * Name.context) * node Graph.T);
-    val empty_names = ML_Syntax.reserved |> fold Name.declare reserved_user;
+    val empty_names = reserved_ml |> fold Name.declare reserved_user;
     val empty_module = ((empty_names, empty_names), Graph.empty);
     fun map_node [] f = f
       | map_node (m::ms) f =
@@ -1064,9 +1064,17 @@
     parse_args ((Args.$$$ "-" >> K output_diag
       || Args.$$$ "#" >> K output_internal
       || Args.name >> output_file)
-    >> (fn output => seri_ml pr_sml pr_sml_modl output))
+    >> (fn output => seri_ml pr_sml pr_sml_modl ML_Syntax.reserved output))
   end;
 
+val reserved_ocaml = Name.make_context ["and", "as", "assert", "begin", "class",
+  "constraint", "do", "done", "downto", "else", "end", "exception",
+  "external", "false", "for", "fun", "function", "functor", "if",
+  "in", "include", "inherit", "initializer", "lazy", "let", "match", "method",
+  "module", "mutable", "new", "object", "of", "open", "or", "private", "rec",
+  "sig", "struct", "then", "to", "true", "try", "type", "val",
+  "virtual", "when", "while", "with", "mod"];
+
 val isar_seri_ocaml =
   let
     fun output_file file = File.write (Path.explode file) o code_output;
@@ -1074,7 +1082,7 @@
   in
     parse_args ((Args.$$$ "-" >> K output_diag
       || Args.name >> output_file)
-    >> (fn output => seri_ml pr_ocaml pr_ocaml_modl output))
+    >> (fn output => seri_ml pr_ocaml pr_ocaml_modl reserved_ocaml output))
   end;
 
 
@@ -1662,7 +1670,8 @@
     |> CodegenThingol.project_code
         (Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const)
           (SOME [val_name])
-    |> seri_ml pr_sml pr_sml_modl I (labelled_name thy) reserved (Symtab.lookup alias) (Symtab.lookup prolog)
+    |> seri_ml pr_sml pr_sml_modl ML_Syntax.reserved I (labelled_name thy) reserved
+        (Symtab.lookup alias) (Symtab.lookup prolog)
         (fun_of class) (fun_of tyco) (fun_of const)
     |> eval
   end;
@@ -1790,7 +1799,7 @@
 fun idfs_of_const thy c =
   let
     val c' = (c, Sign.the_const_type thy c);
-    val c'' = CodegenConsts.norm_of_typ thy c';
+    val c'' = CodegenConsts.const_of_cexpr thy c';
   in (c'', CodegenNames.const thy c'') end;
 
 fun no_bindings x = (Option.map o apsnd)
@@ -1798,16 +1807,11 @@
 
 fun gen_add_haskell_monad prep_const c_run c_mbind c_kbind thy =
   let
-    val c_run' =
-      (CodegenConsts.norm thy o prep_const thy) c_run;
-    val c_mbind' =
-      (CodegenConsts.norm thy o prep_const thy) c_mbind;
-    val c_mbind'' =
-      CodegenNames.const thy c_mbind';
-    val c_kbind' =
-      (CodegenConsts.norm thy o prep_const thy) c_kbind;
-    val c_kbind'' =
-      CodegenNames.const thy c_kbind';
+    val c_run' = prep_const thy c_run;
+    val c_mbind' = prep_const thy c_mbind;
+    val c_mbind'' = CodegenNames.const thy c_mbind';
+    val c_kbind' = prep_const thy c_kbind;
+    val c_kbind'' = CodegenNames.const thy c_kbind';
     val pr = pretty_haskell_monad c_mbind'' c_kbind''
   in
     thy
diff -r b860975e47b4 -r d1499fff65d8 src/Pure/Tools/nbe.ML
--- a/src/Pure/Tools/nbe.ML	Fri Mar 30 16:19:02 2007 +0200
+++ b/src/Pure/Tools/nbe.ML	Fri Mar 30 16:19:03 2007 +0200
@@ -121,7 +121,9 @@
 
 fun ensure_funs thy funcgr t =
   let
-    val consts = CodegenConsts.consts_of thy t;
+    fun consts_of thy t =
+      fold_aterms (fn Const c => cons (CodegenConsts.const_of_cexpr thy c) | _ => I) t []
+    val consts = consts_of thy t;
     val nbe_tab = NBE_Data.get thy;
   in
     CodegenFuncgr.deps funcgr consts
diff -r b860975e47b4 -r d1499fff65d8 src/Pure/Tools/nbe_codegen.ML
--- a/src/Pure/Tools/nbe_codegen.ML	Fri Mar 30 16:19:02 2007 +0200
+++ b/src/Pure/Tools/nbe_codegen.ML	Fri Mar 30 16:19:03 2007 +0200
@@ -150,7 +150,8 @@
   let
     fun to_term bounds (C s) tcount =
           let
-            val (c, ty) = (CodegenConsts.typ_of_inst thy o the o CodegenNames.const_rev thy) s;
+            val SOME (const as (c, _)) = CodegenNames.const_rev thy s;
+            val ty = CodegenData.default_typ thy const;
             val ty' = map_type_tvar (fn ((s,i),S) => TypeInfer.param (tcount + i) (s,S)) ty;
             val tcount' = tcount + maxidx_of_typ ty + 1;
           in (Const (c, ty'), tcount') end
diff -r b860975e47b4 -r d1499fff65d8 src/Pure/Tools/nbe_eval.ML
--- a/src/Pure/Tools/nbe_eval.ML	Fri Mar 30 16:19:02 2007 +0200
+++ b/src/Pure/Tools/nbe_eval.ML	Fri Mar 30 16:19:03 2007 +0200
@@ -112,7 +112,8 @@
 
 (* ------------------ evaluation with greetings to Tarski ------------------ *)
 
-fun prep_term thy (Const c) = Const (CodegenNames.const thy (CodegenConsts.norm_of_typ thy c), dummyT)
+fun prep_term thy (Const c) = Const (CodegenNames.const thy
+      (CodegenConsts.const_of_cexpr thy c), dummyT)
   | prep_term thy (Free v_ty) = Free v_ty
   | prep_term thy (s $ t) = prep_term thy s $ prep_term thy t
   | prep_term thy (Abs (raw_v, ty, raw_t)) =