--- a/src/HOL/Tools/datatype_codegen.ML Mon Dec 10 11:24:14 2007 +0100
+++ b/src/HOL/Tools/datatype_codegen.ML Mon Dec 10 11:24:15 2007 +0100
@@ -342,7 +342,7 @@
|> MetaSimplifier.rewrite_rule [(Thm.symmetric o Thm.assume) asm]
|> Thm.implies_intr asm
|> Thm.generalize ([], params) 0
- |> Class.unoverload thy
+ |> AxClass.unoverload thy
|> Thm.varifyT
end;
@@ -426,7 +426,7 @@
fun add_eq_thms dtco thy =
let
val thy_ref = Theory.check_thy thy;
- val const = Class.param_of_inst thy ("op =", dtco);
+ val const = AxClass.param_of_inst thy ("op =", dtco);
val get_thms = (fn () => get_eq' (Theory.deref thy_ref) dtco |> rev);
in
Code.add_funcl (const, Susp.delay get_thms) thy
--- a/src/Pure/Isar/class.ML Mon Dec 10 11:24:14 2007 +0100
+++ b/src/Pure/Isar/class.ML Mon Dec 10 11:24:15 2007 +0100
@@ -36,20 +36,9 @@
val instantiation_instance: (local_theory -> local_theory) -> local_theory -> Proof.state
val prove_instantiation_instance: (Proof.context -> tactic) -> local_theory -> local_theory
val conclude_instantiation: local_theory -> local_theory
-
- val overloaded_const: string * typ -> theory -> term * theory
- val overloaded_def: string -> string * term -> theory -> thm * theory
val instantiation_param: Proof.context -> string -> string option
val confirm_declaration: string -> local_theory -> local_theory
- val unoverload: theory -> thm -> thm
- val overload: theory -> thm -> thm
- val unoverload_conv: theory -> conv
- val overload_conv: theory -> conv
- val unoverload_const: theory -> string * typ -> string
- val param_of_inst: theory -> string * string -> string
- val inst_of_param: theory -> string -> (string * string) option
-
(*old axclass layer*)
val axclass_cmd: bstring * xstring list
-> ((bstring * Attrib.src list) * string list) list
@@ -152,96 +141,6 @@
end; (*local*)
-(** basic overloading **)
-
-(* bookkeeping *)
-
-structure InstData = TheoryDataFun
-(
- type T = (string * thm) Symtab.table Symtab.table * (string * string) Symtab.table;
- (*constant name ~> type constructor ~> (constant name, equation),
- constant name ~> (constant name, type constructor)*)
- val empty = (Symtab.empty, Symtab.empty);
- val copy = I;
- val extend = I;
- fun merge _ ((taba1, tabb1), (taba2, tabb2)) =
- (Symtab.join (K (Symtab.merge (K true))) (taba1, taba2),
- Symtab.merge (K true) (tabb1, tabb2));
-);
-
-val inst_tyco = Option.map fst o try (dest_Type o the_single) oo Sign.const_typargs;
-
-fun inst thy (c, tyco) =
- (the o Symtab.lookup ((the o Symtab.lookup (fst (InstData.get thy))) c)) tyco;
-
-val param_of_inst = fst oo inst;
-
-fun inst_thms thy = (Symtab.fold (Symtab.fold (cons o snd o snd) o snd) o fst)
- (InstData.get thy) [];
-
-val inst_of_param = Symtab.lookup o snd o InstData.get;
-
-fun add_inst (c, tyco) inst = (InstData.map o apfst
- o Symtab.map_default (c, Symtab.empty)) (Symtab.update_new (tyco, inst))
- #> (InstData.map o apsnd) (Symtab.update_new (fst inst, (c, tyco)));
-
-fun unoverload thy = MetaSimplifier.simplify true (inst_thms thy);
-fun overload thy = MetaSimplifier.simplify true (map Thm.symmetric (inst_thms thy));
-
-fun unoverload_conv thy = MetaSimplifier.rewrite true (inst_thms thy);
-fun overload_conv thy = MetaSimplifier.rewrite true (map Thm.symmetric (inst_thms thy));
-
-fun unoverload_const thy (c_ty as (c, _)) =
- case AxClass.class_of_param thy c
- of SOME class => (case inst_tyco thy c_ty
- of SOME tyco => try (param_of_inst thy) (c, tyco) |> the_default c
- | NONE => c)
- | NONE => c;
-
-
-(* declaration and definition of instances of overloaded constants *)
-
-fun primitive_note kind (name, thm) =
- PureThy.note_thmss_i kind [((name, []), [([thm], [])])]
- #>> (fn [(_, [thm])] => thm);
-
-fun overloaded_const (c, ty) thy =
- let
- val SOME class = AxClass.class_of_param thy c;
- val SOME tyco = inst_tyco thy (c, ty);
- val name_inst = AxClass.instance_name (tyco, class) ^ "_inst";
- val c' = NameSpace.base c ^ "_" ^ NameSpace.base tyco;
- val ty' = Type.strip_sorts ty;
- in
- thy
- |> Sign.sticky_prefix name_inst
- |> Sign.no_base_names
- |> Sign.declare_const [] (c', ty', NoSyn)
- |-> (fn const' as Const (c'', _) => Thm.add_def false true
- (Thm.def_name c', Logic.mk_equals (Const (c, ty'), const'))
- #>> Thm.varifyT
- #-> (fn thm => add_inst (c, tyco) (c'', thm)
- #> primitive_note Thm.internalK (c', thm)
- #> snd
- #> Sign.restore_naming thy
- #> pair (Const (c, ty))))
- end;
-
-fun overloaded_def name (c, t) thy =
- let
- val ty = Term.fastype_of t;
- val SOME tyco = inst_tyco thy (c, ty);
- val (c', eq) = inst thy (c, tyco);
- val prop = Logic.mk_equals (Const (c', ty), t);
- val name' = Thm.def_name_optional
- (NameSpace.base c ^ "_" ^ NameSpace.base tyco) name;
- in
- thy
- |> Thm.add_def false false (name', prop)
- |>> (fn thm => Drule.transitive_thm OF [eq, thm])
- end;
-
-
(** class data **)
datatype class_data = ClassData of {
@@ -859,7 +758,8 @@
(* syntax *)
-fun subst_param thy params = map_aterms (fn t as Const (c, ty) => (case inst_tyco thy (c, ty)
+fun subst_param thy params = map_aterms (fn t as Const (c, ty) =>
+ (case AxClass.inst_tyco_of thy (c, ty)
of SOME tyco => (case AList.lookup (op =) params (c, tyco)
of SOME v_ty => Free v_ty
| NONE => t)
@@ -878,7 +778,7 @@
val tsig = ProofContext.tsig_of lthy;
val thy = ProofContext.theory_of lthy;
- fun check_improve (Const (c, ty)) = (case inst_tyco thy (c, ty)
+ fun check_improve (Const (c, ty)) = (case AxClass.inst_tyco_of thy (c, ty)
of SOME tyco => (case AList.lookup (op =) params (c, tyco)
of SOME (_, ty') => perhaps (try (Type.typ_match tsig (ty, ty')))
| NONE => I)
@@ -925,8 +825,8 @@
fun type_name "*" = "prod"
| type_name "+" = "sum"
| type_name s = sanatize_name (NameSpace.base s); (*FIXME*)
- fun get_param tyco (param, (c, ty)) = if can (inst thy) (c, tyco)
- then NONE else SOME ((unoverload_const thy (c, ty), tyco),
+ fun get_param tyco (param, (c, ty)) = if can (AxClass.param_of_inst thy) (c, tyco)
+ then NONE else SOME ((AxClass.unoverload_const thy (c, ty), tyco),
(param ^ "_" ^ type_name tyco, map_atyps (K (Type (tyco, vs))) ty));
val params = map_product get_param tycos (these_params thy sort) |> map_filter I;
in
@@ -965,40 +865,10 @@
val { arities, params } = the_instantiation lthy;
val (tycos, sorts, sort) = arities;
val thy = ProofContext.theory_of lthy;
- (*val _ = map (fn (tyco, sorts, sort) =>
- if Sign.of_sort thy
+ val _ = map (fn tyco => if Sign.of_sort thy
(Type (tyco, map TFree (Name.names Name.context Name.aT sorts)), sort)
then () else error ("Missing instance proof for type " ^ quote (Sign.extern_type thy tyco)))
- arities; FIXME activate when old instance command is gone*)
- val params_of = maps (these o try (#params o AxClass.get_info thy))
- o Sign.complete_sort thy;
- val missing_params = tycos
- |> maps (fn tyco => params_of sort |> map (rpair tyco))
- |> filter_out (can (inst thy) o apfst fst);
- fun declare_missing ((c, ty0), tyco) thy =
- (*fun declare_missing ((c, tyco), (_, ty)) thy =*)
- let
- val SOME class = AxClass.class_of_param thy c;
- val name_inst = AxClass.instance_name (tyco, class) ^ "_inst";
- val c' = NameSpace.base c ^ "_" ^ NameSpace.base tyco;
- val vs = Name.names Name.context Name.aT (replicate (Sign.arity_number thy tyco) []);
- val ty = map_atyps (fn _ => Type (tyco, map TFree vs)) ty0;
- in
- thy
- |> Sign.sticky_prefix name_inst
- |> Sign.no_base_names
- |> Sign.declare_const [] (c', ty, NoSyn)
- |-> (fn const' as Const (c'', _) => Thm.add_def false true
- (Thm.def_name c', Logic.mk_equals (const', Const (c, ty)))
- #>> Thm.varifyT
- #-> (fn thm => add_inst (c, tyco) (c'', Thm.symmetric thm)
- #> primitive_note Thm.internalK (c', thm)
- #> snd
- #> Sign.restore_naming thy))
- end;
- in
- lthy
- |> LocalTheory.theory (fold declare_missing missing_params)
- end;
+ tycos;
+ in lthy end;
end;
--- a/src/Pure/Isar/code.ML Mon Dec 10 11:24:14 2007 +0100
+++ b/src/Pure/Isar/code.ML Mon Dec 10 11:24:15 2007 +0100
@@ -518,7 +518,7 @@
cons (Thm.ctyp_of thy (TVar (x_i, sort)), Thm.ctyp_of thy ty)) env [];
in map (Thm.instantiate (instT, [])) thms' end;
-fun const_of_func thy = Class.unoverload_const thy o CodeUnit.head_func;
+fun const_of_func thy = AxClass.unoverload_const thy o CodeUnit.head_func;
fun certify_const thy const thms =
let
@@ -547,7 +547,7 @@
val vs = Name.invents Name.context "" (Sign.arity_number thy tyco);
val classparams = (map fst o these o try (#params o AxClass.get_info thy)) class;
val funcs = classparams
- |> map_filter (fn c => try (Class.param_of_inst thy) (c, tyco))
+ |> map_filter (fn c => try (AxClass.param_of_inst thy) (c, tyco))
|> map (Symtab.lookup ((the_funcs o the_exec) thy))
|> (map o Option.map) (Susp.force o fst o snd)
|> maps these
@@ -665,7 +665,7 @@
^ CodeUnit.string_of_typ thy ty_decl)
end;
fun check_typ (c, thm) =
- case Class.inst_of_param thy c
+ case AxClass.inst_of_param thy c
of SOME (c, tyco) => check_typ_classparam tyco (c, thm)
| NONE => check_typ_fun (c, thm);
in check_typ (const_of_func thy thm, thm) end;
@@ -782,7 +782,7 @@
fun add_datatype raw_cs thy =
let
- val cs = map (fn c_ty as (_, ty) => (Class.unoverload_const thy c_ty, ty)) raw_cs;
+ val cs = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) raw_cs;
val (tyco, vs_cos) = CodeUnit.constrset_of_consts thy cs;
val cs' = map fst (snd vs_cos);
val purge_cs = case Symtab.lookup ((the_dtyps o the_exec) thy) tyco
@@ -909,7 +909,7 @@
|> fold (fn (_, (_, f)) => apply_inline_proc thy f) ((#inline_procs o the_thmproc o the_exec) thy)
(*FIXME - must check: rewrite rule, defining equation, proper constant |> map (snd o check_func false thy) *)
|> common_typ_funcs
- |> map (Class.unoverload thy);
+ |> map (AxClass.unoverload thy);
fun preprocess_conv ct =
let
@@ -919,7 +919,7 @@
|> MetaSimplifier.rewrite false ((#inlines o the_thmproc o the_exec) thy)
|> fold (fn (_, (_, f)) => rhs_conv (apply_inline_proc_cterm thy f))
((#inline_procs o the_thmproc o the_exec) thy)
- |> rhs_conv (Class.unoverload_conv thy)
+ |> rhs_conv (AxClass.unoverload_conv thy)
end;
fun preprocess_term thy = term_of_conv thy preprocess_conv;
@@ -929,7 +929,7 @@
val thy = Thm.theory_of_cterm ct;
in
ct
- |> Class.overload_conv thy
+ |> AxClass.overload_conv thy
|> rhs_conv (MetaSimplifier.rewrite false ((#posts o the_thmproc o the_exec) thy))
end;
@@ -937,7 +937,7 @@
end; (*local*)
-fun default_typ_proto thy c = case Class.inst_of_param thy c
+fun default_typ_proto thy c = case AxClass.inst_of_param thy c
of SOME (c, tyco) => classparam_weakest_typ thy ((the o AxClass.class_of_param thy) c)
(c, tyco) |> SOME
| NONE => (case AxClass.class_of_param thy c
@@ -968,7 +968,7 @@
fun default_typ thy c = case default_typ_proto thy c
of SOME ty => ty
| NONE => (case get_funcs thy c
- of thm :: _ => snd (CodeUnit.head_func (Class.unoverload thy thm))
+ of thm :: _ => snd (CodeUnit.head_func (AxClass.unoverload thy thm))
| [] => Sign.the_const_type thy c);
end; (*local*)
--- a/src/Pure/Isar/code_unit.ML Mon Dec 10 11:24:14 2007 +0100
+++ b/src/Pure/Isar/code_unit.ML Mon Dec 10 11:24:15 2007 +0100
@@ -60,7 +60,7 @@
fun try_thm f thm = SOME (f thm) handle BAD_THM _ => NONE;
fun string_of_typ thy = setmp show_sorts true (Sign.string_of_typ thy);
-fun string_of_const thy c = case Class.inst_of_param thy c
+fun string_of_const thy c = case AxClass.inst_of_param thy c
of SOME (c, tyco) => Sign.extern_const thy c ^ " " ^ enclose "[" "]" (Sign.extern_type thy tyco)
| NONE => Sign.extern_const thy c;
@@ -76,7 +76,7 @@
| NONE => error ("Not a constant: " ^ Sign.string_of_term thy t)
end;
-fun read_const thy = Class.unoverload_const thy o read_bare_const thy;
+fun read_const thy = AxClass.unoverload_const thy o read_bare_const thy;
local
--- a/src/Pure/Isar/theory_target.ML Mon Dec 10 11:24:14 2007 +0100
+++ b/src/Pure/Isar/theory_target.ML Mon Dec 10 11:24:15 2007 +0100
@@ -203,7 +203,7 @@
fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
val declare_const = case Class.instantiation_param lthy c
of SOME c' => if mx3 <> NoSyn then syntax_error c'
- else LocalTheory.theory_result (Class.overloaded_const (c', U))
+ else LocalTheory.theory_result (AxClass.declare_overloaded (c', U))
##> Class.confirm_declaration c
| NONE => (case Overloading.operation lthy c
of SOME (c', _) => if mx3 <> NoSyn then syntax_error c'
@@ -276,7 +276,7 @@
(fn name => fn (Const (c, _), rhs) => Overloading.define checked name (c, rhs))
| NONE => if is_none (Class.instantiation_param lthy c)
then (fn name => fn eq => Thm.add_def false false (name, Logic.mk_equals eq))
- else (fn name => fn (Const (c, _), rhs) => Class.overloaded_def name (c, rhs));
+ else (fn name => fn (Const (c, _), rhs) => AxClass.define_overloaded name (c, rhs));
val (global_def, lthy3) = lthy2
|> LocalTheory.theory_result (define_const name' (lhs', rhs'));
val def = LocalDefs.trans_terms lthy3
--- a/src/Pure/axclass.ML Mon Dec 10 11:24:14 2007 +0100
+++ b/src/Pure/axclass.ML Mon Dec 10 11:24:15 2007 +0100
@@ -27,6 +27,16 @@
val axiomatize_arity: arity -> theory -> theory
val axiomatize_arity_cmd: xstring * string list * string -> theory -> theory
val instance_name: string * class -> string
+ val declare_overloaded: string * typ -> theory -> term * theory
+ val define_overloaded: string -> string * term -> theory -> thm * theory
+ val inst_tyco_of: theory -> string * typ -> string option
+ val unoverload: theory -> thm -> thm
+ val overload: theory -> thm -> thm
+ val unoverload_conv: theory -> conv
+ val overload_conv: theory -> conv
+ val unoverload_const: theory -> string * typ -> string
+ val param_of_inst: theory -> string * string -> string
+ val inst_of_param: theory -> string -> (string * string) option
type cache
val of_sort: theory -> typ * sort -> cache -> thm list * cache (*exception Sorts.CLASS_ERROR*)
val cache: cache
@@ -88,23 +98,36 @@
Symtab.join (K (merge (eq_fst op =))) (arities1, arities2));
+(* instance parameters *)
+
+type inst_params =
+ (string * thm) Symtab.table Symtab.table
+ (*constant name ~> type constructor ~> (constant name, equation)*)
+ * (string * string) Symtab.table; (*constant name ~> (constant name, type constructor)*)
+
+fun merge_inst_params ((const_param1, param_const1), (const_param2, param_const2)) =
+ (Symtab.join (K (Symtab.merge (K true))) (const_param1, const_param2),
+ Symtab.merge (K true) (param_const1, param_const2));
+
+
(* setup data *)
structure AxClassData = TheoryDataFun
(
- type T = axclasses * instances;
- val empty = ((Symtab.empty, []), ([], Symtab.empty));
+ type T = axclasses * (instances * inst_params);
+ val empty = ((Symtab.empty, []), (([], Symtab.empty), (Symtab.empty, Symtab.empty)));
val copy = I;
val extend = I;
- fun merge pp ((axclasses1, instances1), (axclasses2, instances2)) =
- (merge_axclasses pp (axclasses1, axclasses2), (merge_instances (instances1, instances2)));
+ fun merge pp ((axclasses1, (instances1, inst_params1)), (axclasses2, (instances2, inst_params2))) =
+ (merge_axclasses pp (axclasses1, axclasses2),
+ (merge_instances (instances1, instances2), merge_inst_params (inst_params1, inst_params2)));
);
(* maintain axclasses *)
val get_axclasses = #1 o AxClassData.get;
-fun map_axclasses f = AxClassData.map (apfst f);
+val map_axclasses = AxClassData.map o apfst;
val lookup_def = Symtab.lookup o #1 o get_axclasses;
@@ -135,8 +158,8 @@
fun instance_name (a, c) = NameSpace.base c ^ "_" ^ NameSpace.base a;
-val get_instances = #2 o AxClassData.get;
-fun map_instances f = AxClassData.map (apsnd f);
+val get_instances = #1 o #2 o AxClassData.get;
+val map_instances = AxClassData.map o apsnd o apfst;
fun the_classrel thy (c1, c2) =
@@ -159,6 +182,39 @@
(classrel, arities |> Symtab.insert_list (eq_fst op =) (t, ((c, Ss), th))));
+(* maintain instance parameters *)
+
+val get_inst_params = #2 o #2 o AxClassData.get;
+val map_inst_params = AxClassData.map o apsnd o apsnd;
+
+fun get_inst_param thy (c, tyco) =
+ (the o Symtab.lookup ((the o Symtab.lookup (fst (get_inst_params thy))) c)) tyco;
+
+fun add_inst_param (c, tyco) inst = (map_inst_params o apfst
+ o Symtab.map_default (c, Symtab.empty)) (Symtab.update_new (tyco, inst))
+ #> (map_inst_params o apsnd) (Symtab.update_new (fst inst, (c, tyco)));
+
+val inst_of_param = Symtab.lookup o snd o get_inst_params;
+val param_of_inst = fst oo get_inst_param;
+
+fun inst_thms thy = (Symtab.fold (Symtab.fold (cons o snd o snd) o snd) o fst)
+ (get_inst_params thy) [];
+
+val inst_tyco_of = Option.map fst o try (dest_Type o the_single) oo Sign.const_typargs;
+
+fun unoverload thy = MetaSimplifier.simplify true (inst_thms thy);
+fun overload thy = MetaSimplifier.simplify true (map Thm.symmetric (inst_thms thy));
+
+fun unoverload_conv thy = MetaSimplifier.rewrite true (inst_thms thy);
+fun overload_conv thy = MetaSimplifier.rewrite true (map Thm.symmetric (inst_thms thy));
+
+fun unoverload_const thy (c_ty as (c, _)) =
+ case class_of_param thy c
+ of SOME class => (case inst_tyco_of thy c_ty
+ of SOME tyco => try (param_of_inst thy) (c, tyco) |> the_default c
+ | NONE => c)
+ | NONE => c;
+
(** instances **)
@@ -200,10 +256,35 @@
val prop = Thm.plain_prop_of (Thm.transfer thy th);
val (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
val _ = map (Sign.certify_sort thy) Ss = Ss orelse err ();
+ (*FIXME turn this into a mere check as soon as "attach" has disappeared*)
+ val missing_params = Sign.complete_sort thy [c]
+ |> maps (these o Option.map (fn AxClass { params, ... } => params) o lookup_def thy)
+ |> filter_out (fn (p, _) => can (get_inst_param thy) (p, t));
+ fun declare_missing (p, T0) thy =
+ let
+ val name_inst = instance_name (t, c) ^ "_inst";
+ val p' = NameSpace.base p ^ "_" ^ NameSpace.base t;
+ val vs = Name.names Name.context Name.aT (replicate (Sign.arity_number thy t) []);
+ val T = map_atyps (fn _ => Type (t, map TFree vs)) T0;
+ in
+ thy
+ |> Sign.sticky_prefix name_inst
+ |> Sign.no_base_names
+ |> Sign.declare_const [] (p', T, NoSyn)
+ |-> (fn const' as Const (p'', _) => Thm.add_def false true
+ (Thm.def_name p', Logic.mk_equals (const', Const (p, T)))
+ #>> Thm.varifyT
+ #-> (fn thm => add_inst_param (p, t) (p'', Thm.symmetric thm)
+ #> PureThy.note Thm.internalK (p', thm)
+ #> snd
+ #> Sign.restore_naming thy))
+ end;
+
in
thy
|> Sign.primitive_arity (t, Ss, [c])
|> put_arity ((t, Ss, c), Drule.unconstrainTs th)
+ |> fold declare_missing missing_params
end;
@@ -240,6 +321,47 @@
end;
+(* instance parameters and overloaded definitions *)
+
+(* declaration and definition of instances of overloaded constants *)
+
+fun declare_overloaded (c, T) thy =
+ let
+ val SOME class = class_of_param thy c;
+ val SOME tyco = inst_tyco_of thy (c, T);
+ val name_inst = instance_name (tyco, class) ^ "_inst";
+ val c' = NameSpace.base c ^ "_" ^ NameSpace.base tyco;
+ val T' = Type.strip_sorts T;
+ in
+ thy
+ |> Sign.sticky_prefix name_inst
+ |> Sign.no_base_names
+ |> Sign.declare_const [] (c', T', NoSyn)
+ |-> (fn const' as Const (c'', _) => Thm.add_def false true
+ (Thm.def_name c', Logic.mk_equals (Const (c, T'), const'))
+ #>> Thm.varifyT
+ #-> (fn thm => add_inst_param (c, tyco) (c'', thm)
+ #> PureThy.note Thm.internalK (c', thm)
+ #> snd
+ #> Sign.restore_naming thy
+ #> pair (Const (c, T))))
+ end;
+
+fun define_overloaded name (c, t) thy =
+ let
+ val T = Term.fastype_of t;
+ val SOME tyco = inst_tyco_of thy (c, T);
+ val (c', eq) = get_inst_param thy (c, tyco);
+ val prop = Logic.mk_equals (Const (c', T), t);
+ val name' = Thm.def_name_optional
+ (NameSpace.base c ^ "_" ^ NameSpace.base tyco) name;
+ in
+ thy
+ |> Thm.add_def false false (name', prop)
+ |>> (fn thm => Drule.transitive_thm OF [eq, thm])
+ end;
+
+
(** class definitions **)
--- a/src/Tools/code/code_funcgr.ML Mon Dec 10 11:24:14 2007 +0100
+++ b/src/Tools/code/code_funcgr.ML Mon Dec 10 11:24:15 2007 +0100
@@ -157,7 +157,7 @@
val thy_classes = (#classes o Sorts.rep_algebra o Sign.classes_of) thy;
fun all_classparams tyco class =
these (try (#params o AxClass.get_info thy) class)
- |> map (fn (c, _) => Class.param_of_inst thy (c, tyco))
+ |> map (fn (c, _) => AxClass.param_of_inst thy (c, tyco))
in
Symtab.empty
|> fold (fn (tyco, class) =>
@@ -211,7 +211,7 @@
|> resort_funcss thy algebra funcgr
|> filter_out (can (Graph.get_node funcgr) o fst);
fun typ_func c [] = Code.default_typ thy c
- | typ_func c (thms as thm :: _) = case Class.inst_of_param thy c
+ | typ_func c (thms as thm :: _) = case AxClass.inst_of_param thy c
of SOME (c', tyco) =>
let
val (_, ty) = CodeUnit.head_func thm;
--- a/src/Tools/code/code_name.ML Mon Dec 10 11:24:14 2007 +0100
+++ b/src/Tools/code/code_name.ML Mon Dec 10 11:24:15 2007 +0100
@@ -216,7 +216,7 @@
of SOME dtco => SOME (thyname_of_tyco thy dtco)
| NONE => (case AxClass.class_of_param thy c
of SOME class => SOME (thyname_of_class thy class)
- | NONE => (case Class.inst_of_param thy c
+ | NONE => (case AxClass.inst_of_param thy c
of SOME (c, tyco) => SOME (thyname_of_instance thy
((the o AxClass.class_of_param thy) c, tyco))
| NONE => NONE));
--- a/src/Tools/code/code_package.ML Mon Dec 10 11:24:14 2007 +0100
+++ b/src/Tools/code/code_package.ML Mon Dec 10 11:24:15 2007 +0100
@@ -33,7 +33,7 @@
in
gr
|> Graph.subgraph (member (op =) select)
- |> Graph.map_nodes ((apsnd o map) (Class.overload thy))
+ |> Graph.map_nodes ((apsnd o map) (AxClass.overload thy))
end;
fun code_thms thy =
@@ -162,7 +162,7 @@
| SOME thm => let
val t = (ObjectLogic.drop_judgment thy o Thm.prop_of) thm;
val cs = fold_aterms (fn Const (c, ty) =>
- cons (Class.unoverload_const thy (c, ty)) | _ => I) t [];
+ cons (AxClass.unoverload_const thy (c, ty)) | _ => I) t [];
in if exists (member (op =) sel_cs) cs
andalso forall (member (op =) all_cs) cs
then SOME (thmref, thm) else NONE end;
--- a/src/Tools/code/code_thingol.ML Mon Dec 10 11:24:14 2007 +0100
+++ b/src/Tools/code/code_thingol.ML Mon Dec 10 11:24:15 2007 +0100
@@ -461,7 +461,7 @@
fun exprgen_classparam_inst (c, ty) =
let
val c_inst = Const (c, map_type_tfree (K arity_typ') ty);
- val thm = Class.unoverload_conv thy (Thm.cterm_of thy c_inst);
+ val thm = AxClass.unoverload_conv thy (Thm.cterm_of thy c_inst);
val c_ty = (apsnd Logic.unvarifyT o dest_Const o snd
o Logic.dest_equals o Thm.prop_of) thm;
in