simplified constant representation in code generator
authorhaftmann
Fri Mar 30 16:19:03 2007 +0200 (2007-03-30)
changeset 22554d1499fff65d8
parent 22553 b860975e47b4
child 22555 d04a4c1b6ab2
simplified constant representation in code generator
src/HOL/Tools/datatype_codegen.ML
src/Pure/Tools/codegen_consts.ML
src/Pure/Tools/codegen_data.ML
src/Pure/Tools/codegen_func.ML
src/Pure/Tools/codegen_funcgr.ML
src/Pure/Tools/codegen_names.ML
src/Pure/Tools/codegen_package.ML
src/Pure/Tools/codegen_serializer.ML
src/Pure/Tools/nbe.ML
src/Pure/Tools/nbe_codegen.ML
src/Pure/Tools/nbe_eval.ML
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Fri Mar 30 16:19:02 2007 +0200
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Fri Mar 30 16:19:03 2007 +0200
     1.3 @@ -620,11 +620,10 @@
     1.4      fun add_eq_thms (dtco, (_, (vs, cs))) thy =
     1.5        let
     1.6          val thy_ref = Theory.self_ref thy;
     1.7 -        val ty = Type (dtco, map TFree vs) |> Logic.varifyT;
     1.8 -        val c = CodegenConsts.norm thy ("op =", [ty]);
     1.9 +        val const = ("op =", SOME dtco);
    1.10          val get_thms = (fn () => get_eq (Theory.deref thy_ref) dtco |> rev);
    1.11        in
    1.12 -        CodegenData.add_funcl (c, CodegenData.lazy get_thms) thy
    1.13 +        CodegenData.add_funcl (const, CodegenData.lazy get_thms) thy
    1.14        end;
    1.15    in
    1.16      prove_codetypes_arities (ClassPackage.intro_classes_tac [])
     2.1 --- a/src/Pure/Tools/codegen_consts.ML	Fri Mar 30 16:19:02 2007 +0200
     2.2 +++ b/src/Pure/Tools/codegen_consts.ML	Fri Mar 30 16:19:03 2007 +0200
     2.3 @@ -8,17 +8,15 @@
     2.4  
     2.5  signature CODEGEN_CONSTS =
     2.6  sig
     2.7 -  type const = string * typ list (*type instantiations*)
     2.8 +  type const = string * string option (* constant name, possibly instance *)
     2.9    val const_ord: const * const -> order
    2.10    val eq_const: const * const -> bool
    2.11    structure Consttab: TABLE
    2.12 -  val inst_of_typ: theory -> string * typ -> const
    2.13 -  val typ_of_inst: theory -> const -> string * typ
    2.14 -  val norm: theory -> const -> const
    2.15 -  val norm_of_typ: theory -> string * typ -> const
    2.16 -  val typ_sort_inst: Sorts.algebra -> typ * sort
    2.17 -    -> sort Vartab.table -> sort Vartab.table
    2.18 -  val typargs: theory -> string * typ -> typ list
    2.19 +  val const_of_cexpr: theory -> string * typ -> const
    2.20 +  val string_of_typ: theory -> typ -> string
    2.21 +  val string_of_const: theory -> const -> string
    2.22 +  val read_const: theory -> string -> const
    2.23 +
    2.24    val co_of_const: theory -> const
    2.25      -> string * ((string * sort) list * (string * typ list))
    2.26    val co_of_const': theory -> const
    2.27 @@ -29,13 +27,10 @@
    2.28      -> string * typ list -> const
    2.29    val consts_of_cos: theory -> string -> (string * sort) list
    2.30      -> (string * typ list) list -> const list
    2.31 -  val find_def: theory -> const -> (string (*theory name*) * thm) option
    2.32 -  val consts_of: theory -> term -> const list
    2.33 -  val read_const: theory -> string -> const
    2.34 -  val string_of_const: theory -> const -> string
    2.35 -  val raw_string_of_const: const -> string
    2.36 -  val string_of_const_typ: theory -> string * typ -> string
    2.37 -  val string_of_typ: theory -> typ -> string
    2.38 +
    2.39 +  val typargs: theory -> string * typ -> typ list
    2.40 +  val typ_sort_inst: Sorts.algebra -> typ * sort
    2.41 +    -> sort Vartab.table -> sort Vartab.table
    2.42  end;
    2.43  
    2.44  structure CodegenConsts: CODEGEN_CONSTS =
    2.45 @@ -44,124 +39,79 @@
    2.46  
    2.47  (* basic data structures *)
    2.48  
    2.49 -type const = string * typ list (*type instantiations*);
    2.50 -val const_ord = prod_ord fast_string_ord (list_ord Term.typ_ord);
    2.51 +type const = string * string option;
    2.52 +val const_ord = prod_ord fast_string_ord (option_ord string_ord);
    2.53  val eq_const = is_equal o const_ord;
    2.54  
    2.55  structure Consttab =
    2.56    TableFun(
    2.57 -    type key = string * typ list;
    2.58 +    type key = const;
    2.59      val ord = const_ord;
    2.60    );
    2.61  
    2.62 -
    2.63 -(* type instantiations, overloading, dictionary values *)
    2.64 -
    2.65  fun string_of_typ thy = setmp show_sorts true (Sign.string_of_typ thy);
    2.66  
    2.67 -fun inst_of_typ thy (c_ty as (c, ty)) =
    2.68 -  (c, Sign.const_typargs thy c_ty);
    2.69  
    2.70 -fun typ_of_inst thy (c_tys as (c, tys)) =
    2.71 -  (c, Sign.const_instance thy c_tys);
    2.72 +(* conversion between constant expressions and constants *)
    2.73  
    2.74 -fun find_def thy (c, tys) =
    2.75 -  let
    2.76 -    val specs = Defs.specifications_of (Theory.defs_of thy) c;
    2.77 -    val typ_instance = case AxClass.class_of_param thy c
    2.78 -     of SOME _ => let
    2.79 -          fun instance_tycos (Type (tyco1, _), Type (tyco2, _)) = tyco1 = tyco2
    2.80 -            | instance_tycos (_ , TVar _) = true
    2.81 -            | instance_tycos ty_ty = Sign.typ_instance thy ty_ty;
    2.82 -        in instance_tycos end
    2.83 -      | NONE =>  Sign.typ_instance thy;
    2.84 -    fun get_def (_, { is_def, thyname, name, lhs, rhs }) =
    2.85 -      if is_def andalso forall typ_instance (tys ~~ lhs) then
    2.86 -        case try (Thm.get_axiom_i thy) name
    2.87 -         of SOME thm => SOME (thyname, thm)
    2.88 -          | NONE => NONE
    2.89 -      else NONE
    2.90 -  in
    2.91 -    get_first get_def specs
    2.92 -  end;
    2.93 +fun const_of_cexpr thy (c_ty as (c, _)) =
    2.94 +  case AxClass.class_of_param thy c
    2.95 +   of SOME class => (case Sign.const_typargs thy c_ty
    2.96 +       of [Type (tyco, _)] => if can (Sorts.mg_domain (Sign.classes_of thy) tyco) [class]
    2.97 +              then (c, SOME tyco)
    2.98 +              else (c, NONE)
    2.99 +        | [_] => (c, NONE))
   2.100 +    | NONE => (c, NONE);
   2.101  
   2.102 -fun norm thy (c, insts) =
   2.103 +fun string_of_const thy (c, NONE) = Sign.extern_const thy c
   2.104 +  | string_of_const thy (c, SOME tyco) = Sign.extern_const thy c
   2.105 +      ^ " " ^ enclose "[" "]" (Sign.extern_type thy tyco);
   2.106 +
   2.107 +
   2.108 +(* reading constants as terms *)
   2.109 +
   2.110 +fun read_const thy raw_t =
   2.111    let
   2.112 -    fun disciplined class [ty as Type (tyco, _)] =
   2.113 -          let
   2.114 -            val sorts = Sorts.mg_domain (Sign.classes_of thy) tyco [class]
   2.115 -              handle CLASS_ERROR => error ("No such instance: " ^ tyco ^ " :: " ^ class
   2.116 -                ^ ",\nrequired for overloaded constant " ^ c);
   2.117 -            val vs = Name.invents Name.context "'a" (length sorts);
   2.118 -          in
   2.119 -            (c, [Type (tyco, map (fn v => TVar ((v, 0), [])) vs)])
   2.120 -          end
   2.121 -      | disciplined class _ =
   2.122 -          (c, [TVar (("'a", 0), [class])]);
   2.123 -  in case AxClass.class_of_param thy c
   2.124 -   of SOME class => disciplined class insts
   2.125 -    | NONE => inst_of_typ thy (c, Sign.the_const_type thy c)
   2.126 -  end;
   2.127 -
   2.128 -fun norm_of_typ thy (c, ty) =
   2.129 -  norm thy (c, Sign.const_typargs thy (c, ty));
   2.130 -
   2.131 -fun consts_of thy t =
   2.132 -  fold_aterms (fn Const c => cons (norm_of_typ thy c) | _ => I) t []
   2.133 -
   2.134 -fun typ_sort_inst algebra =
   2.135 -  let
   2.136 -    val inters = Sorts.inter_sort algebra;
   2.137 -    fun match _ [] = I
   2.138 -      | match (TVar (v, S)) S' = Vartab.map_default (v, []) (fn S'' => inters (S, inters (S', S'')))
   2.139 -      | match (Type (a, Ts)) S =
   2.140 -          fold2 match Ts (Sorts.mg_domain algebra a S)
   2.141 -  in uncurry match end;
   2.142 -
   2.143 -fun typargs thy (c_ty as (c, ty)) =
   2.144 -  let
   2.145 -    val opt_class = AxClass.class_of_param thy c;
   2.146 -    val tys = Sign.const_typargs thy (c, ty);
   2.147 -  in case (opt_class, tys)
   2.148 -   of (SOME _, [Type (_, tys')]) => tys'
   2.149 -    | _ => tys
   2.150 +    val t = Sign.read_term thy raw_t;
   2.151 +  in case try dest_Const t
   2.152 +   of SOME c_ty => const_of_cexpr thy c_ty
   2.153 +    | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t)
   2.154    end;
   2.155  
   2.156  
   2.157 -(* printing *)
   2.158 -
   2.159 -fun string_of_const thy (c, tys) =
   2.160 -  space_implode " " (Sign.extern_const thy c
   2.161 -    :: map (enclose "[" "]" o Sign.string_of_typ thy) tys);
   2.162 -
   2.163 -fun raw_string_of_const (c, tys) =
   2.164 -  space_implode " " (c
   2.165 -    :: map (enclose "[" "]" o Display.raw_string_of_typ) tys);
   2.166 -
   2.167 -fun string_of_const_typ thy (c, ty) =
   2.168 -  string_of_const thy (c, Consts.typargs (Sign.consts_of thy) (c, ty));
   2.169 -
   2.170 -
   2.171 -(* conversion between constants and datatype constructors *)
   2.172 +(* conversion between constants, constant expressions and datatype constructors *)
   2.173  
   2.174  fun const_of_co thy tyco vs (co, tys) =
   2.175 -  norm_of_typ thy (co, tys ---> Type (tyco, map TFree vs));
   2.176 +  const_of_cexpr thy (co, tys ---> Type (tyco, map TFree vs));
   2.177  
   2.178  fun consts_of_cos thy tyco vs cos =
   2.179    let
   2.180      val dty = Type (tyco, map TFree vs);
   2.181 -    fun mk_co (co, tys) = norm_of_typ thy (co, tys ---> dty);
   2.182 +    fun mk_co (co, tys) = const_of_cexpr thy (co, tys ---> dty);
   2.183    in map mk_co cos end;
   2.184  
   2.185  local
   2.186  
   2.187  exception BAD of string;
   2.188  
   2.189 +fun mg_typ_of_const thy (c, NONE) = Sign.the_const_type thy c
   2.190 +  | mg_typ_of_const thy (c, SOME tyco) =
   2.191 +      let
   2.192 +        val SOME class = AxClass.class_of_param thy c;
   2.193 +        val ty = Sign.the_const_type thy c;
   2.194 +          (*an approximation*)
   2.195 +        val sorts = Sorts.mg_domain (Sign.classes_of thy) tyco [class]
   2.196 +          handle CLASS_ERROR => raise BAD ("No such instance: " ^ tyco ^ " :: " ^ class
   2.197 +            ^ ",\nrequired for overloaded constant " ^ c);
   2.198 +        val vs = Name.invents Name.context "'a" (length sorts);
   2.199 +      in map_atyps (K (Type (tyco, map (fn v => TVar ((v, 0), [])) vs))) ty end;
   2.200 +
   2.201  fun gen_co_of_const thy const =
   2.202    let
   2.203 -    val (c, ty) = (apsnd Logic.unvarifyT o typ_of_inst thy) const;
   2.204 +    val (c, _) = const;
   2.205 +    val ty = (Logic.unvarifyT o mg_typ_of_const thy) const;
   2.206      fun err () = raise BAD
   2.207 -     ("Illegal type for datatype constructor: " ^ Sign.string_of_typ thy ty);
   2.208 +     ("Illegal type for datatype constructor: " ^ string_of_typ thy ty);
   2.209      val (tys, ty') = strip_type ty;
   2.210      val (tyco, vs) = ((apsnd o map) dest_TFree o dest_Type) ty'
   2.211        handle TYPE _ => err ();
   2.212 @@ -197,18 +147,26 @@
   2.213    in (tyco, (vs, cos)) end;
   2.214  
   2.215  
   2.216 -(* reading constants as terms *)
   2.217 +(* dictionary values *)
   2.218  
   2.219 -fun read_const_typ thy raw_t =
   2.220 +fun typargs thy (c_ty as (c, ty)) =
   2.221    let
   2.222 -    val t = Sign.read_term thy raw_t
   2.223 -  in case try dest_Const t
   2.224 -   of SOME c_ty => (typ_of_inst thy o norm_of_typ thy) c_ty
   2.225 -    | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t)
   2.226 +    val opt_class = AxClass.class_of_param thy c;
   2.227 +    val tys = Sign.const_typargs thy (c, ty);
   2.228 +  in case (opt_class, tys)
   2.229 +   of (SOME class, ty as [Type (tyco, tys')]) =>
   2.230 +        if can (Sorts.mg_domain (Sign.classes_of thy) tyco) [class]
   2.231 +        then tys' else ty
   2.232 +    | _ => tys
   2.233    end;
   2.234  
   2.235 -fun read_const thy =
   2.236 -  norm_of_typ thy o read_const_typ thy;
   2.237 -
   2.238 +fun typ_sort_inst algebra =
   2.239 +  let
   2.240 +    val inters = Sorts.inter_sort algebra;
   2.241 +    fun match _ [] = I
   2.242 +      | match (TVar (v, S)) S' = Vartab.map_default (v, []) (fn S'' => inters (S, inters (S', S'')))
   2.243 +      | match (Type (a, Ts)) S =
   2.244 +          fold2 match Ts (Sorts.mg_domain algebra a S)
   2.245 +  in uncurry match end;
   2.246  
   2.247  end;
     3.1 --- a/src/Pure/Tools/codegen_data.ML	Fri Mar 30 16:19:02 2007 +0200
     3.2 +++ b/src/Pure/Tools/codegen_data.ML	Fri Mar 30 16:19:03 2007 +0200
     3.3 @@ -27,10 +27,9 @@
     3.4    val coregular_algebra: theory -> Sorts.algebra
     3.5    val operational_algebra: theory -> (sort -> sort) * Sorts.algebra
     3.6    val these_funcs: theory -> CodegenConsts.const -> thm list
     3.7 -  val tap_typ: theory -> CodegenConsts.const -> typ option
     3.8    val get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list)
     3.9    val get_datatype_of_constr: theory -> CodegenConsts.const -> string option
    3.10 -  val get_constr_typ: theory -> CodegenConsts.const -> typ option
    3.11 +  val default_typ: theory -> CodegenConsts.const -> typ
    3.12  
    3.13    val preprocess_cterm: cterm -> thm
    3.14  
    3.15 @@ -454,7 +453,7 @@
    3.16      val vs = Name.invents Name.context "" (Sign.arity_number thy tyco);
    3.17      val clsops = (these o Option.map snd o try (AxClass.params_of_class thy)) class;
    3.18      val funcs = clsops
    3.19 -      |> map (fn (clsop, _) => CodegenConsts.norm thy (clsop, [Type (tyco, map (TFree o rpair []) vs)]))
    3.20 +      |> map (fn (clsop, _) => (clsop, SOME tyco))
    3.21        |> map (Consttab.lookup ((the_funcs o get_exec) thy))
    3.22        |> (map o Option.map) (Susp.force o fst)
    3.23        |> maps these
    3.24 @@ -518,7 +517,7 @@
    3.25      val thy = Thm.theory_of_thm thm;
    3.26      val raw_funcs = CodegenFunc.mk_func strict thm;
    3.27      val error_warning = if strict then error else warning #> K NONE;
    3.28 -    fun check_typ_classop class (const as (c, [Type (tyco, _)]), thm) =
    3.29 +    fun check_typ_classop class (const as (c, SOME tyco), thm) =
    3.30            let
    3.31              val ((_, ty), _) = CodegenFunc.dest_func thm;
    3.32              val ty_decl = classop_weakest_typ thy class (c, tyco);
    3.33 @@ -547,7 +546,7 @@
    3.34                ^ "\nis incompatible with permitted least general type\n"
    3.35                ^ CodegenConsts.string_of_typ thy ty_strongest)
    3.36            end
    3.37 -      | check_typ_classop class ((c, [_]), thm) =
    3.38 +      | check_typ_classop class ((c, NONE), thm) =
    3.39            error_warning ("Illegal type for class operation " ^ quote c
    3.40             ^ "\nin defining equation\n"
    3.41             ^ string_of_thm thm);
    3.42 @@ -563,7 +562,7 @@
    3.43             ^ "\nis incompatible declared function type\n"
    3.44             ^ CodegenConsts.string_of_typ thy ty_decl)
    3.45        end;
    3.46 -    fun check_typ (const as (c, tys), thm) =
    3.47 +    fun check_typ (const as (c, _), thm) =
    3.48        case AxClass.class_of_param thy c
    3.49         of SOME class => check_typ_classop class (const, thm)
    3.50          | NONE => check_typ_fun (const, thm);
    3.51 @@ -599,12 +598,12 @@
    3.52         (del_thm thm)) funcs)) thy
    3.53    end;
    3.54  
    3.55 -fun add_funcl (c, lthms) thy =
    3.56 +fun add_funcl (const, lthms) thy =
    3.57    let
    3.58 -    val c' = CodegenConsts.norm thy c;
    3.59 -    val lthms' = certificate thy (fn thy => certify_const thy c' o maps (CodegenFunc.mk_func true)) lthms;
    3.60 +    val lthms' = certificate thy (fn thy => certify_const thy const
    3.61 +      o maps (CodegenFunc.mk_func true)) lthms;
    3.62    in
    3.63 -    map_exec_purge (SOME [c]) (map_funcs (Consttab.map_default (c', (Susp.value [], []))
    3.64 +    map_exec_purge (SOME [const]) (map_funcs (Consttab.map_default (const, (Susp.value [], []))
    3.65        (add_lthms lthms'))) thy
    3.66    end;
    3.67  
    3.68 @@ -682,8 +681,8 @@
    3.69    | apply_preproc thy f (thms as (thm :: _)) =
    3.70        let
    3.71          val thms' = f thy thms;
    3.72 -        val c = (CodegenConsts.norm_of_typ thy o fst o CodegenFunc.dest_func) thm;
    3.73 -      in (certify_const thy c o map CodegenFunc.mk_head) thms' end;
    3.74 +        val thms'' as ((const, _) :: _) = map CodegenFunc.mk_head thms'
    3.75 +      in (certify_const thy const o map CodegenFunc.mk_head) thms' end;
    3.76  
    3.77  fun cmp_thms thy =
    3.78    make_ord (fn (thm1, thm2) => not (Sign.typ_instance thy (CodegenFunc.typ_func thm1, CodegenFunc.typ_func thm2)));
    3.79 @@ -716,44 +715,6 @@
    3.80  
    3.81  end; (*local*)
    3.82  
    3.83 -local
    3.84 -
    3.85 -fun get_funcs thy const =
    3.86 -  Consttab.lookup ((the_funcs o get_exec) thy) const
    3.87 -  |> Option.map (Susp.force o fst)
    3.88 -  |> these
    3.89 -  |> map (Thm.transfer thy);
    3.90 -
    3.91 -in
    3.92 -
    3.93 -fun these_funcs thy const =
    3.94 -  let
    3.95 -    fun get_prim_def_funcs (const as (c, tys)) =
    3.96 -      case CodegenConsts.find_def thy const
    3.97 -       of SOME (_, thm) =>
    3.98 -            thm
    3.99 -            |> Thm.transfer thy
   3.100 -            |> gen_mk_func_typ false
   3.101 -            |> map (CodegenFunc.expand_eta ~1 o snd)
   3.102 -        | NONE => []
   3.103 -    fun drop_refl thy = filter_out (is_equal o Term.fast_term_ord o Logic.dest_equals
   3.104 -      o ObjectLogic.drop_judgment thy o Drule.plain_prop_of);
   3.105 -    val funcs = case get_funcs thy const
   3.106 -     of [] => get_prim_def_funcs const
   3.107 -    | funcs => funcs
   3.108 -  in
   3.109 -    funcs
   3.110 -    |> preprocess thy
   3.111 -    |> drop_refl thy
   3.112 -  end;
   3.113 -
   3.114 -fun tap_typ thy const =
   3.115 -  case get_funcs thy const
   3.116 -   of thm :: _ => SOME (CodegenFunc.typ_func thm)
   3.117 -    | [] => NONE;
   3.118 -
   3.119 -end; (*local*)
   3.120 -
   3.121  fun get_datatype thy tyco =
   3.122    case Symtab.lookup ((the_dtyps o get_exec) thy) tyco
   3.123     of SOME spec => spec
   3.124 @@ -781,6 +742,65 @@
   3.125          |> SOME end
   3.126      | NONE => NONE;
   3.127  
   3.128 +fun default_typ_proto thy (const as (c, SOME tyco)) = classop_weakest_typ thy
   3.129 +      ((the o AxClass.class_of_param thy) c) (c, tyco) |> SOME
   3.130 +  | default_typ_proto thy (const as (c, NONE)) = case AxClass.class_of_param thy c
   3.131 +       of SOME class => SOME (Term.map_type_tvar
   3.132 +            (K (TVar (("'a", 0), [class]))) (Sign.the_const_type thy c))
   3.133 +        | NONE => get_constr_typ thy const;
   3.134 +
   3.135 +local
   3.136 +
   3.137 +fun get_funcs thy const =
   3.138 +  Consttab.lookup ((the_funcs o get_exec) thy) const
   3.139 +  |> Option.map (Susp.force o fst)
   3.140 +  |> these
   3.141 +  |> map (Thm.transfer thy);
   3.142 +
   3.143 +fun find_def thy (const as (c, _)) =
   3.144 +  let
   3.145 +    val specs = Defs.specifications_of (Theory.defs_of thy) c;
   3.146 +    val ty = case try (default_typ_proto thy) const
   3.147 +     of NONE => NONE
   3.148 +      | SOME ty => ty;
   3.149 +    val tys = Sign.const_typargs thy (c, ty |> the_default (Sign.the_const_type thy c));
   3.150 +    fun get_def (_, { is_def, name, lhs, rhs, thyname }) =
   3.151 +      if is_def andalso forall (Sign.typ_instance thy) (tys ~~ lhs) then
   3.152 +        try (Thm.get_axiom_i thy) name
   3.153 +      else NONE
   3.154 +  in get_first get_def specs end;
   3.155 +
   3.156 +in
   3.157 +
   3.158 +fun these_funcs thy const =
   3.159 +  let
   3.160 +    fun get_prim_def_funcs (const as (c, tys)) =
   3.161 +      case find_def thy const
   3.162 +       of SOME thm =>
   3.163 +            thm
   3.164 +            |> Thm.transfer thy
   3.165 +            |> gen_mk_func_typ false
   3.166 +            |> map (CodegenFunc.expand_eta ~1 o snd)
   3.167 +        | NONE => []
   3.168 +    fun drop_refl thy = filter_out (is_equal o Term.fast_term_ord o Logic.dest_equals
   3.169 +      o ObjectLogic.drop_judgment thy o Drule.plain_prop_of);
   3.170 +    val funcs = case get_funcs thy const
   3.171 +     of [] => get_prim_def_funcs const
   3.172 +    | funcs => funcs
   3.173 +  in
   3.174 +    funcs
   3.175 +    |> preprocess thy
   3.176 +    |> drop_refl thy
   3.177 +  end;
   3.178 +
   3.179 +fun default_typ thy (const as (c, _)) = case default_typ_proto thy const
   3.180 + of SOME ty => ty
   3.181 +  | NONE => (case get_funcs thy const
   3.182 +     of thm :: _ => CodegenFunc.typ_func thm
   3.183 +      | [] => Sign.the_const_type thy c);
   3.184 +
   3.185 +end; (*local*)
   3.186 +
   3.187  
   3.188  (** code attributes **)
   3.189  
     4.1 --- a/src/Pure/Tools/codegen_func.ML	Fri Mar 30 16:19:02 2007 +0200
     4.2 +++ b/src/Pure/Tools/codegen_func.ML	Fri Mar 30 16:19:03 2007 +0200
     4.3 @@ -75,7 +75,7 @@
     4.4    o Drule.fconv_rule Drule.beta_eta_conversion);
     4.5  
     4.6  val mk_head = lift_thm_thy (fn thy => fn thm =>
     4.7 -  ((CodegenConsts.norm_of_typ thy o fst o dest_func) thm, thm));
     4.8 +  ((CodegenConsts.const_of_cexpr thy o fst o dest_func) thm, thm));
     4.9  
    4.10  local
    4.11  
     5.1 --- a/src/Pure/Tools/codegen_funcgr.ML	Fri Mar 30 16:19:02 2007 +0200
     5.2 +++ b/src/Pure/Tools/codegen_funcgr.ML	Fri Mar 30 16:19:03 2007 +0200
     5.3 @@ -80,7 +80,7 @@
     5.4        let
     5.5          val thy = Thm.theory_of_thm thm;
     5.6          val is_refl = curry CodegenConsts.eq_const const;
     5.7 -        fun the_const c = case try (CodegenConsts.norm_of_typ thy) c
     5.8 +        fun the_const c = case try (CodegenConsts.const_of_cexpr thy) c
     5.9           of SOME const => if is_refl const then I else insert CodegenConsts.eq_const const
    5.10            | NONE => I
    5.11        in fold_consts the_const thms [] end;
    5.12 @@ -147,7 +147,7 @@
    5.13  
    5.14  fun resort_funcss thy algebra funcgr =
    5.15    let
    5.16 -    val typ_funcgr = try (fst o Constgraph.get_node funcgr o CodegenConsts.norm_of_typ thy);
    5.17 +    val typ_funcgr = try (fst o Constgraph.get_node funcgr o CodegenConsts.const_of_cexpr thy);
    5.18      fun resort_dep (const, thms) = (const, resort_thms algebra typ_funcgr thms)
    5.19        handle Sorts.CLASS_ERROR e => raise INVALID ([const], Sorts.msg_class_error (Sign.pp thy) e
    5.20                      ^ ",\nfor constant " ^ CodegenConsts.string_of_const thy const
    5.21 @@ -162,7 +162,7 @@
    5.22            in (Sign.typ_equiv thy (ty, ty'), (const, thms')) end;
    5.23      fun resort_recs funcss =
    5.24        let
    5.25 -        fun tap_typ c_ty = case try (CodegenConsts.norm_of_typ thy) c_ty
    5.26 +        fun tap_typ c_ty = case try (CodegenConsts.const_of_cexpr thy) c_ty
    5.27           of SOME const => AList.lookup (CodegenConsts.eq_const) funcss const
    5.28                |> these
    5.29                |> try hd
    5.30 @@ -177,14 +177,6 @@
    5.31        in if unchanged then funcss' else resort_rec_until funcss' end;
    5.32    in map resort_dep #> resort_rec_until end;
    5.33  
    5.34 -fun classop_const thy algebra class classop tyco =
    5.35 -  let
    5.36 -    val sorts = Sorts.mg_domain algebra tyco [class]
    5.37 -    val (var, _) = try (AxClass.params_of_class thy) class |> the_default ("'a", []);
    5.38 -    val vs = Name.names (Name.declare var Name.context) "'a" sorts;
    5.39 -    val arity_typ = Type (tyco, map TFree vs);
    5.40 -  in (classop, [arity_typ]) end;
    5.41 -
    5.42  fun instances_of thy algebra insts =
    5.43    let
    5.44      val thy_classes = (#classes o Sorts.rep_algebra o Sign.classes_of) thy;
    5.45 @@ -192,8 +184,7 @@
    5.46        try (AxClass.params_of_class thy) class
    5.47        |> Option.map snd
    5.48        |> these
    5.49 -      |> map (fn (c, _) => classop_const thy algebra class c tyco)
    5.50 -      |> map (CodegenConsts.norm thy)
    5.51 +      |> map (fn (c, _) => (c, SOME tyco))
    5.52    in
    5.53      Symtab.empty
    5.54      |> fold (fn (tyco, class) =>
    5.55 @@ -204,9 +195,9 @@
    5.56  
    5.57  fun instances_of_consts thy algebra funcgr consts =
    5.58    let
    5.59 -    fun inst (const as (c, ty)) = case try (CodegenConsts.norm_of_typ thy) const
    5.60 -     of SOME const => insts_of thy algebra c (fst (Constgraph.get_node funcgr const)) ty
    5.61 -      | NONE => [];
    5.62 +    fun inst (cexpr as (c, ty)) = insts_of thy algebra c
    5.63 +      ((fst o Constgraph.get_node funcgr o CodegenConsts.const_of_cexpr thy) cexpr)
    5.64 +      ty handle CLASS_ERROR => [];
    5.65    in
    5.66      []
    5.67      |> fold (fold (insert (op =)) o inst) consts
    5.68 @@ -248,44 +239,23 @@
    5.69      val funcss = raw_funcss
    5.70        |> resort_funcss thy algebra funcgr
    5.71        |> filter_out (can (Constgraph.get_node funcgr) o fst);
    5.72 -    fun classop_typ (c, [typarg]) class =
    5.73 -      let
    5.74 -        val ty = Sign.the_const_type thy c;
    5.75 -        val inst = case typarg
    5.76 -         of Type (tyco, _) => classop_const thy algebra class c tyco
    5.77 -              |> snd
    5.78 -              |> the_single
    5.79 -              |> Logic.varifyT
    5.80 -          | _ => TVar (("'a", 0), [class]);
    5.81 -      in Term.map_type_tvar (K inst) ty end;
    5.82 -    fun default_typ (const as (c, tys)) = case AxClass.class_of_param thy c
    5.83 -         of SOME class => classop_typ const class
    5.84 -          | NONE => (case CodegenData.tap_typ thy const
    5.85 -             of SOME ty => ty
    5.86 -              | NONE => (case CodegenData.get_constr_typ thy const
    5.87 -                 of SOME ty => ty
    5.88 -                  | NONE => Sign.the_const_type thy c))
    5.89 -    fun typ_func (const as (c, tys)) thms thm =
    5.90 -      let
    5.91 -        val ty = CodegenFunc.typ_func thm;
    5.92 -      in case AxClass.class_of_param thy c
    5.93 -       of SOME class => (case tys
    5.94 -           of [Type _] => let val ty_decl = classop_typ const class
    5.95 -              in if Sign.typ_equiv thy (ty, ty_decl) then ty
    5.96 -              else raise raise INVALID ([const], "Illegal instantation for class operation "
    5.97 -                    ^ CodegenConsts.string_of_const thy const
    5.98 -                    ^ ":\n" ^ CodegenConsts.string_of_typ thy ty_decl
    5.99 -                    ^ "\nto " ^ CodegenConsts.string_of_typ thy ty
   5.100 -                    ^ "\nin defining equations\n"
   5.101 -                    ^ (cat_lines o map string_of_thm) thms)
   5.102 -              end
   5.103 -            | _ => ty)
   5.104 -        | NONE => ty
   5.105 -      end;
   5.106 -    fun add_funcs (const, thms as thm :: _) =
   5.107 -          Constgraph.new_node (const, (typ_func const thms thm, thms))
   5.108 -      | add_funcs (const, []) =
   5.109 -          Constgraph.new_node (const, (default_typ const, []));
   5.110 +    fun typ_func const [] = CodegenData.default_typ thy const
   5.111 +      | typ_func (_, NONE) (thm :: _) = CodegenFunc.typ_func thm
   5.112 +      | typ_func (const as (c, SOME tyco)) (thms as (thm :: _)) =
   5.113 +          let
   5.114 +            val ty = CodegenFunc.typ_func thm;
   5.115 +            val SOME class = AxClass.class_of_param thy c;
   5.116 +            val sorts_decl = Sorts.mg_domain algebra tyco [class];
   5.117 +            val tys = CodegenConsts.typargs thy (c, ty);
   5.118 +            val sorts = map (snd o dest_TVar) tys;
   5.119 +          in if sorts = sorts_decl then ty
   5.120 +            else raise INVALID ([const], "Illegal instantation for class operation "
   5.121 +              ^ CodegenConsts.string_of_const thy const
   5.122 +              ^ "\nin defining equations\n"
   5.123 +              ^ (cat_lines o map string_of_thm) thms)
   5.124 +          end;
   5.125 +    fun add_funcs (const, thms) =
   5.126 +      Constgraph.new_node (const, (typ_func const thms, thms));
   5.127      fun add_deps (funcs as (const, thms)) funcgr =
   5.128        let
   5.129          val deps = consts_of funcs;
   5.130 @@ -339,6 +309,8 @@
   5.131  
   5.132  fun ensure_consts_term rewrites thy f ct funcgr =
   5.133    let
   5.134 +    fun consts_of thy t =
   5.135 +      fold_aterms (fn Const c => cons (CodegenConsts.const_of_cexpr thy c) | _ => I) t []
   5.136      fun rhs_conv conv thm =
   5.137        let
   5.138          val thm' = (conv o snd o Drule.dest_equals o Thm.cprop_of) thm;
   5.139 @@ -348,12 +320,12 @@
   5.140      val thm1 = CodegenData.preprocess_cterm ct
   5.141        |> fold (rhs_conv o MetaSimplifier.rewrite false o single) (rewrites thy);
   5.142      val ct' = Drule.dest_equals_rhs (Thm.cprop_of thm1);
   5.143 -    val consts = CodegenConsts.consts_of thy (Thm.term_of ct');
   5.144 +    val consts = consts_of thy (Thm.term_of ct');
   5.145      val funcgr' = ensure_consts rewrites thy consts funcgr;
   5.146      val algebra = CodegenData.coregular_algebra thy;
   5.147      val (_, thm2) = Thm.varifyT' [] thm1;
   5.148      val thm3 = Thm.reflexive (Drule.dest_equals_rhs (Thm.cprop_of thm2));
   5.149 -    val typ_funcgr = try (fst o Constgraph.get_node funcgr' o CodegenConsts.norm_of_typ thy);
   5.150 +    val typ_funcgr = try (fst o Constgraph.get_node funcgr' o CodegenConsts.const_of_cexpr thy);
   5.151      val [thm4] = resort_thms algebra typ_funcgr [thm3];
   5.152      val tfrees = Term.add_tfrees (Thm.prop_of thm1) [];
   5.153      fun inst thm =
     6.1 --- a/src/Pure/Tools/codegen_names.ML	Fri Mar 30 16:19:02 2007 +0200
     6.2 +++ b/src/Pure/Tools/codegen_names.ML	Fri Mar 30 16:19:03 2007 +0200
     6.3 @@ -216,23 +216,21 @@
     6.4  fun instance_policy thy = policy thy (fn (class, tyco) => 
     6.5    NameSpace.base class ^ "_" ^ NameSpace.base tyco) thyname_of_instance;
     6.6  
     6.7 -fun force_thyname thy (const as (c, tys)) =
     6.8 +fun force_thyname thy (const as (c, opt_tyco)) =
     6.9    case AxClass.class_of_param thy c
    6.10 -   of SOME class => (case tys
    6.11 -       of [Type (tyco, _)] => SOME (thyname_of_instance thy (class, tyco))
    6.12 -        | _ => SOME (thyname_of_class thy class))
    6.13 +   of SOME class => (case opt_tyco
    6.14 +       of SOME tyco => SOME (thyname_of_instance thy (class, tyco))
    6.15 +        | NONE => SOME (thyname_of_class thy class))
    6.16      | NONE => (case CodegenData.get_datatype_of_constr thy const
    6.17     of SOME dtco => SOME (thyname_of_tyco thy dtco)
    6.18 -    | NONE => (case CodegenConsts.find_def thy const
    6.19 -   of SOME (thyname, _) => SOME thyname
    6.20 -    | NONE => NONE));
    6.21 +    | NONE => NONE);
    6.22  
    6.23 -fun const_policy thy (c, tys) =
    6.24 -  case force_thyname thy (c, tys)
    6.25 +fun const_policy thy (const as (c, opt_tyco)) =
    6.26 +  case force_thyname thy const
    6.27     of NONE => policy thy NameSpace.base thyname_of_const c
    6.28      | SOME thyname => let
    6.29          val prefix = (purify_prefix o NameSpace.explode o dotify) thyname;
    6.30 -        val tycos = map_filter (fn Type (tyco, _) => SOME tyco | _ => NONE) tys;
    6.31 +        val tycos = the_list opt_tyco;
    6.32          val base = map (purify_base o NameSpace.base) (c :: tycos);
    6.33        in NameSpace.implode (prefix @ [space_implode "_" base]) end;
    6.34  
    6.35 @@ -307,7 +305,7 @@
    6.36  structure ConstName = CodeDataFun
    6.37  (struct
    6.38    val name = "Pure/codegen_names";
    6.39 -  type T = const Consttab.table * (string * typ list) Symtab.table;
    6.40 +  type T = const Consttab.table * (string * string option) Symtab.table;
    6.41    val empty = (Consttab.empty, Symtab.empty);
    6.42    fun merge _ ((const1, constrev1), (const2, constrev2)) =
    6.43      (Consttab.merge eq_string (const1, const2),
    6.44 @@ -395,8 +393,7 @@
    6.45    get thy #instance StringPairTab.lookup map_instance StringPairTab.update instance_policy
    6.46    #> add_idf idf_instance;
    6.47  fun const thy =
    6.48 -  CodegenConsts.norm thy
    6.49 -  #> get_const thy
    6.50 +  get_const thy
    6.51    #> add_idf idf_const;
    6.52  
    6.53  fun class_rev thy =
     7.1 --- a/src/Pure/Tools/codegen_package.ML	Fri Mar 30 16:19:02 2007 +0200
     7.2 +++ b/src/Pure/Tools/codegen_package.ML	Fri Mar 30 16:19:03 2007 +0200
     7.3 @@ -141,7 +141,7 @@
     7.4      val (v, cs) = AxClass.params_of_class thy class;
     7.5      val class' = CodegenNames.class thy class;
     7.6      val classrels' = map (curry (CodegenNames.classrel thy) class) superclasses;
     7.7 -    val classops' = map (CodegenNames.const thy o CodegenConsts.norm_of_typ thy) cs;
     7.8 +    val classops' = map (CodegenNames.const thy o CodegenConsts.const_of_cexpr thy) cs;
     7.9      val defgen_class =
    7.10        fold_map (ensure_def_class thy algbr funcgr strct) superclasses
    7.11        ##>> (fold_map (exprgen_type thy algbr funcgr strct) o map snd) cs
    7.12 @@ -170,7 +170,7 @@
    7.13              ||>> fold_map (fn (c, tys) =>
    7.14                fold_map (exprgen_type thy algbr funcgr strct) tys
    7.15                #-> (fn tys' =>
    7.16 -                pair ((CodegenNames.const thy o CodegenConsts.norm_of_typ thy)
    7.17 +                pair ((CodegenNames.const thy o CodegenConsts.const_of_cexpr thy)
    7.18                    (c, tys ---> Type (tyco, map TFree vs)), tys'))) cos
    7.19              |-> (fn (vs, cos) => succeed (CodegenThingol.Datatype (vs, cos)))
    7.20            end;
    7.21 @@ -235,7 +235,7 @@
    7.22    end
    7.23  and exprgen_dict_parms thy (algbr as (_, consts)) funcgr strct (c, ty_ctxt) =
    7.24    let
    7.25 -    val c' = CodegenConsts.norm_of_typ thy (c, ty_ctxt)
    7.26 +    val c' = CodegenConsts.const_of_cexpr thy (c, ty_ctxt)
    7.27      val idf = CodegenNames.const thy c';
    7.28      val ty_decl = Consts.the_declaration consts idf;
    7.29      val (tys, tys_decl) = pairself (curry (Consts.typargs consts) idf) (ty_ctxt, ty_decl);
    7.30 @@ -258,7 +258,7 @@
    7.31              (superclass, (classrel, (inst, dss))));
    7.32      fun gen_classop_def (classop as (c, ty)) trns =
    7.33        trns
    7.34 -      |> ensure_def_const thy algbr funcgr strct (CodegenConsts.norm_of_typ thy classop)
    7.35 +      |> ensure_def_const thy algbr funcgr strct (CodegenConsts.const_of_cexpr thy classop)
    7.36        ||>> exprgen_term thy algbr funcgr strct (Const (c, map_type_tfree (K arity_typ) ty));
    7.37      fun defgen_inst trns =
    7.38        trns
    7.39 @@ -276,13 +276,13 @@
    7.40      |> ensure_def thy defgen_inst true ("generating instance " ^ quote class ^ " / " ^ quote tyco) inst
    7.41      |> pair inst
    7.42    end
    7.43 -and ensure_def_const thy (algbr as (_, consts)) funcgr strct (c_tys as (c, tys)) trns =
    7.44 +and ensure_def_const thy (algbr as (_, consts)) funcgr strct (const as (c, opt_tyco)) trns =
    7.45    let
    7.46 -    val c' = CodegenNames.const thy c_tys;
    7.47 +    val c' = CodegenNames.const thy const;
    7.48      fun defgen_datatypecons trns =
    7.49        trns
    7.50        |> ensure_def_tyco thy algbr funcgr strct
    7.51 -          ((the o CodegenData.get_datatype_of_constr thy) c_tys)
    7.52 +          ((the o CodegenData.get_datatype_of_constr thy) const)
    7.53        |-> (fn _ => succeed CodegenThingol.Bot);
    7.54      fun defgen_classop trns =
    7.55        trns
    7.56 @@ -290,7 +290,7 @@
    7.57        |-> (fn _ => succeed CodegenThingol.Bot);
    7.58      fun defgen_fun trns =
    7.59        case CodegenFuncgr.funcs funcgr
    7.60 -        (perhaps (Consttab.lookup ((snd o snd o CodegenPackageData.get) thy)) c_tys)
    7.61 +        (perhaps (Consttab.lookup ((snd o snd o CodegenPackageData.get) thy)) const)
    7.62         of thms as _ :: _ =>
    7.63              let
    7.64                val (ty, eq_thms) = prep_eqs thy thms;
    7.65 @@ -315,20 +315,20 @@
    7.66          | [] =>
    7.67                trns
    7.68                |> fail ("No defining equations found for "
    7.69 -                   ^ (quote o CodegenConsts.string_of_const thy) c_tys);
    7.70 -    val defgen = if (is_some o CodegenData.get_datatype_of_constr thy) c_tys
    7.71 +                   ^ (quote o CodegenConsts.string_of_const thy) const);
    7.72 +    val defgen = if (is_some o CodegenData.get_datatype_of_constr thy) const
    7.73        then defgen_datatypecons
    7.74 -      else if (is_some o AxClass.class_of_param thy) c andalso
    7.75 -        case tys of [TFree _] => true | [TVar _] => true | _ => false
    7.76 -      then defgen_classop
    7.77 -      else defgen_fun
    7.78 +      else if is_some opt_tyco
    7.79 +        orelse (not o is_some o AxClass.class_of_param thy) c
    7.80 +      then defgen_fun
    7.81 +      else defgen_classop
    7.82      val strict = check_strict strct (CodegenSerializer.const_has_serialization thy) c';
    7.83    in
    7.84      trns
    7.85      |> tracing (fn _ => "generating constant "
    7.86 -        ^ (quote o CodegenConsts.string_of_const thy) c_tys)
    7.87 +        ^ (quote o CodegenConsts.string_of_const thy) const)
    7.88      |> ensure_def thy defgen strict ("generating constant "
    7.89 -         ^ CodegenConsts.string_of_const thy c_tys) c'
    7.90 +         ^ CodegenConsts.string_of_const thy const) c'
    7.91      |> pair c'
    7.92    end
    7.93  and exprgen_term thy algbr funcgr strct (Const (c, ty)) trns =
    7.94 @@ -359,7 +359,7 @@
    7.95              |>> (fn (t, ts) => t `$$ ts)
    7.96  and appgen_default thy algbr funcgr strct ((c, ty), ts) trns =
    7.97    trns
    7.98 -  |> ensure_def_const thy algbr funcgr strct (CodegenConsts.norm_of_typ thy (c, ty))
    7.99 +  |> ensure_def_const thy algbr funcgr strct (CodegenConsts.const_of_cexpr thy (c, ty))
   7.100    ||>> fold_map (exprgen_type thy algbr funcgr strct) ((fst o Term.strip_type) ty)
   7.101    ||>> exprgen_type thy algbr funcgr strct ((snd o Term.strip_type) ty)
   7.102    ||>> exprgen_dict_parms thy algbr funcgr strct (c, ty)
   7.103 @@ -483,14 +483,11 @@
   7.104  
   7.105  local
   7.106  
   7.107 -fun add_consts thy f (c1, c2 as (c, tys)) =
   7.108 +fun add_consts thy f (c1, c2 as (c, opt_tyco)) =
   7.109    let
   7.110 -    val _ = case tys
   7.111 -     of [TVar _] => if is_some (AxClass.class_of_param thy c)
   7.112 -          then error ("Not a function: " ^ CodegenConsts.string_of_const thy c2)
   7.113 -          else ()
   7.114 -      | _ => ();
   7.115 -    val _ = if is_some (CodegenData.get_datatype_of_constr thy c2)
   7.116 +    val _ = if
   7.117 +        is_some (AxClass.class_of_param thy c) andalso is_none opt_tyco
   7.118 +        orelse is_some (CodegenData.get_datatype_of_constr thy c2)
   7.119        then error ("Not a function: " ^ CodegenConsts.string_of_const thy c2)
   7.120        else ();
   7.121      val funcgr = Funcgr.make thy [c1, c2];
   7.122 @@ -548,10 +545,10 @@
   7.123  
   7.124  in
   7.125  
   7.126 -val abstyp = gen_abstyp CodegenConsts.norm Sign.certify_typ;
   7.127 +val abstyp = gen_abstyp (K I) Sign.certify_typ;
   7.128  val abstyp_e = gen_abstyp CodegenConsts.read_const (fn thy => Sign.read_typ (thy, K NONE));
   7.129  
   7.130 -val constsubst = gen_constsubst CodegenConsts.norm;
   7.131 +val constsubst = gen_constsubst (K I);
   7.132  val constsubst_e = gen_constsubst CodegenConsts.read_const;
   7.133  
   7.134  end; (*local*)
   7.135 @@ -608,16 +605,27 @@
   7.136  fun consts_of thy thyname =
   7.137    let
   7.138      val this_thy = Option.map theory thyname |> the_default thy;
   7.139 -    val defs = (#defs o rep_theory) this_thy;
   7.140 -    val cs_names = (Symtab.keys o snd o #constants o Consts.dest o #consts o Sign.rep_sg) this_thy;
   7.141 -    val consts = maps (fn c => (map (fn tys => CodegenConsts.norm thy (c, tys))
   7.142 -      o map #lhs o filter #is_def o map snd o Defs.specifications_of defs) c) cs_names;
   7.143 -    fun is_const thyname (c, _) =
   7.144 -      (*this is an approximation*)
   7.145 -      not (exists (fn thy => Sign.declared_const thy c) (Theory.parents_of this_thy))
   7.146 +    val defs = (#defs o rep_theory) thy;
   7.147 +    val cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
   7.148 +      ((snd o #constants o Consts.dest o #consts o Sign.rep_sg) this_thy) [];
   7.149 +    fun classop c = case AxClass.class_of_param thy c
   7.150 +     of NONE => [(c, NONE)]
   7.151 +      | SOME class => Symtab.fold
   7.152 +          (fn (tyco, classes) => if AList.defined (op =) classes class
   7.153 +            then cons (c, SOME tyco) else I)
   7.154 +          ((#arities o Sorts.rep_algebra o Sign.classes_of) this_thy)
   7.155 +          [(c, NONE)];
   7.156 +    val consts = maps classop cs;
   7.157 +    fun test_instance thy (class, tyco) =
   7.158 +      can (Sorts.mg_domain (Sign.classes_of thy) tyco) [class]
   7.159 +    fun belongs_here thyname (c, NONE) =
   7.160 +          not (exists (fn thy => Sign.declared_const thy c) (Theory.parents_of this_thy))
   7.161 +      | belongs_here thyname (c, SOME tyco) =
   7.162 +          not (exists (fn thy => test_instance thy ((the o AxClass.class_of_param thy) c, tyco))
   7.163 +            (Theory.parents_of this_thy))
   7.164    in case thyname
   7.165     of NONE => consts
   7.166 -    | SOME thyname => filter (is_const thyname) consts
   7.167 +    | SOME thyname => filter (belongs_here thyname) consts
   7.168    end;
   7.169  
   7.170  fun filter_generatable thy targets consts =
     8.1 --- a/src/Pure/Tools/codegen_serializer.ML	Fri Mar 30 16:19:02 2007 +0200
     8.2 +++ b/src/Pure/Tools/codegen_serializer.ML	Fri Mar 30 16:19:03 2007 +0200
     8.3 @@ -11,7 +11,7 @@
     8.4    include BASIC_CODEGEN_THINGOL;
     8.5  
     8.6    val add_syntax_class: string -> class
     8.7 -    -> (string * ((string * typ list) * string) list) option -> theory -> theory;
     8.8 +    -> (string * (CodegenConsts.const * string) list) option -> theory -> theory;
     8.9    val add_syntax_inst: string -> string * class -> bool -> theory -> theory;
    8.10    val add_syntax_tycoP: string -> string -> OuterParse.token list
    8.11      -> (theory -> theory) * OuterParse.token list;
    8.12 @@ -422,7 +422,7 @@
    8.13      and pr_bind' ((NONE, NONE), _) = str "_"
    8.14        | pr_bind' ((SOME v, NONE), _) = str v
    8.15        | pr_bind' ((NONE, SOME p), _) = p
    8.16 -      | pr_bind' ((SOME v, SOME p), _) = concat [str v, str "as", p]
    8.17 +      | pr_bind' ((SOME v, SOME p), _) = 
    8.18      and pr_bind fxy = gen_pr_bind pr_bind' pr_term fxy;
    8.19      fun pr_def (MLFuns (funns as (funn :: funns'))) =
    8.20            let
    8.21 @@ -889,7 +889,7 @@
    8.22  val code_width = ref 80;
    8.23  fun code_output p = Pretty.setmp_margin (!code_width) Pretty.output p ^ "\n";
    8.24  
    8.25 -fun seri_ml pr_def pr_modl output labelled_name reserved_user module_alias module_prolog
    8.26 +fun seri_ml pr_def pr_modl reserved_ml output labelled_name reserved_user module_alias module_prolog
    8.27    (_ : string -> class_syntax option) tyco_syntax const_syntax code =
    8.28    let
    8.29      val is_cons = fn node => case CodegenThingol.get_def code node
    8.30 @@ -898,7 +898,7 @@
    8.31      datatype node =
    8.32          Def of string * ml_def option
    8.33        | Module of string * ((Name.context * Name.context) * node Graph.T);
    8.34 -    val empty_names = ML_Syntax.reserved |> fold Name.declare reserved_user;
    8.35 +    val empty_names = reserved_ml |> fold Name.declare reserved_user;
    8.36      val empty_module = ((empty_names, empty_names), Graph.empty);
    8.37      fun map_node [] f = f
    8.38        | map_node (m::ms) f =
    8.39 @@ -1064,9 +1064,17 @@
    8.40      parse_args ((Args.$$$ "-" >> K output_diag
    8.41        || Args.$$$ "#" >> K output_internal
    8.42        || Args.name >> output_file)
    8.43 -    >> (fn output => seri_ml pr_sml pr_sml_modl output))
    8.44 +    >> (fn output => seri_ml pr_sml pr_sml_modl ML_Syntax.reserved output))
    8.45    end;
    8.46  
    8.47 +val reserved_ocaml = Name.make_context ["and", "as", "assert", "begin", "class",
    8.48 +  "constraint", "do", "done", "downto", "else", "end", "exception",
    8.49 +  "external", "false", "for", "fun", "function", "functor", "if",
    8.50 +  "in", "include", "inherit", "initializer", "lazy", "let", "match", "method",
    8.51 +  "module", "mutable", "new", "object", "of", "open", "or", "private", "rec",
    8.52 +  "sig", "struct", "then", "to", "true", "try", "type", "val",
    8.53 +  "virtual", "when", "while", "with", "mod"];
    8.54 +
    8.55  val isar_seri_ocaml =
    8.56    let
    8.57      fun output_file file = File.write (Path.explode file) o code_output;
    8.58 @@ -1074,7 +1082,7 @@
    8.59    in
    8.60      parse_args ((Args.$$$ "-" >> K output_diag
    8.61        || Args.name >> output_file)
    8.62 -    >> (fn output => seri_ml pr_ocaml pr_ocaml_modl output))
    8.63 +    >> (fn output => seri_ml pr_ocaml pr_ocaml_modl reserved_ocaml output))
    8.64    end;
    8.65  
    8.66  
    8.67 @@ -1662,7 +1670,8 @@
    8.68      |> CodegenThingol.project_code
    8.69          (Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const)
    8.70            (SOME [val_name])
    8.71 -    |> seri_ml pr_sml pr_sml_modl I (labelled_name thy) reserved (Symtab.lookup alias) (Symtab.lookup prolog)
    8.72 +    |> seri_ml pr_sml pr_sml_modl ML_Syntax.reserved I (labelled_name thy) reserved
    8.73 +        (Symtab.lookup alias) (Symtab.lookup prolog)
    8.74          (fun_of class) (fun_of tyco) (fun_of const)
    8.75      |> eval
    8.76    end;
    8.77 @@ -1790,7 +1799,7 @@
    8.78  fun idfs_of_const thy c =
    8.79    let
    8.80      val c' = (c, Sign.the_const_type thy c);
    8.81 -    val c'' = CodegenConsts.norm_of_typ thy c';
    8.82 +    val c'' = CodegenConsts.const_of_cexpr thy c';
    8.83    in (c'', CodegenNames.const thy c'') end;
    8.84  
    8.85  fun no_bindings x = (Option.map o apsnd)
    8.86 @@ -1798,16 +1807,11 @@
    8.87  
    8.88  fun gen_add_haskell_monad prep_const c_run c_mbind c_kbind thy =
    8.89    let
    8.90 -    val c_run' =
    8.91 -      (CodegenConsts.norm thy o prep_const thy) c_run;
    8.92 -    val c_mbind' =
    8.93 -      (CodegenConsts.norm thy o prep_const thy) c_mbind;
    8.94 -    val c_mbind'' =
    8.95 -      CodegenNames.const thy c_mbind';
    8.96 -    val c_kbind' =
    8.97 -      (CodegenConsts.norm thy o prep_const thy) c_kbind;
    8.98 -    val c_kbind'' =
    8.99 -      CodegenNames.const thy c_kbind';
   8.100 +    val c_run' = prep_const thy c_run;
   8.101 +    val c_mbind' = prep_const thy c_mbind;
   8.102 +    val c_mbind'' = CodegenNames.const thy c_mbind';
   8.103 +    val c_kbind' = prep_const thy c_kbind;
   8.104 +    val c_kbind'' = CodegenNames.const thy c_kbind';
   8.105      val pr = pretty_haskell_monad c_mbind'' c_kbind''
   8.106    in
   8.107      thy
     9.1 --- a/src/Pure/Tools/nbe.ML	Fri Mar 30 16:19:02 2007 +0200
     9.2 +++ b/src/Pure/Tools/nbe.ML	Fri Mar 30 16:19:03 2007 +0200
     9.3 @@ -121,7 +121,9 @@
     9.4  
     9.5  fun ensure_funs thy funcgr t =
     9.6    let
     9.7 -    val consts = CodegenConsts.consts_of thy t;
     9.8 +    fun consts_of thy t =
     9.9 +      fold_aterms (fn Const c => cons (CodegenConsts.const_of_cexpr thy c) | _ => I) t []
    9.10 +    val consts = consts_of thy t;
    9.11      val nbe_tab = NBE_Data.get thy;
    9.12    in
    9.13      CodegenFuncgr.deps funcgr consts
    10.1 --- a/src/Pure/Tools/nbe_codegen.ML	Fri Mar 30 16:19:02 2007 +0200
    10.2 +++ b/src/Pure/Tools/nbe_codegen.ML	Fri Mar 30 16:19:03 2007 +0200
    10.3 @@ -150,7 +150,8 @@
    10.4    let
    10.5      fun to_term bounds (C s) tcount =
    10.6            let
    10.7 -            val (c, ty) = (CodegenConsts.typ_of_inst thy o the o CodegenNames.const_rev thy) s;
    10.8 +            val SOME (const as (c, _)) = CodegenNames.const_rev thy s;
    10.9 +            val ty = CodegenData.default_typ thy const;
   10.10              val ty' = map_type_tvar (fn ((s,i),S) => TypeInfer.param (tcount + i) (s,S)) ty;
   10.11              val tcount' = tcount + maxidx_of_typ ty + 1;
   10.12            in (Const (c, ty'), tcount') end
    11.1 --- a/src/Pure/Tools/nbe_eval.ML	Fri Mar 30 16:19:02 2007 +0200
    11.2 +++ b/src/Pure/Tools/nbe_eval.ML	Fri Mar 30 16:19:03 2007 +0200
    11.3 @@ -112,7 +112,8 @@
    11.4  
    11.5  (* ------------------ evaluation with greetings to Tarski ------------------ *)
    11.6  
    11.7 -fun prep_term thy (Const c) = Const (CodegenNames.const thy (CodegenConsts.norm_of_typ thy c), dummyT)
    11.8 +fun prep_term thy (Const c) = Const (CodegenNames.const thy
    11.9 +      (CodegenConsts.const_of_cexpr thy c), dummyT)
   11.10    | prep_term thy (Free v_ty) = Free v_ty
   11.11    | prep_term thy (s $ t) = prep_term thy s $ prep_term thy t
   11.12    | prep_term thy (Abs (raw_v, ty, raw_t)) =