# HG changeset patch # User haftmann # Date 1197282255 -3600 # Node ID 34860182b250bbf9b12839b59bbd502fbb5c120d # Parent ad9e3594f3f3637000700d07c6bce7c833e9de0c moved instance parameter management from class.ML to axclass.ML diff -r ad9e3594f3f3 -r 34860182b250 src/HOL/Tools/datatype_codegen.ML --- 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 diff -r ad9e3594f3f3 -r 34860182b250 src/Pure/Isar/class.ML --- 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; diff -r ad9e3594f3f3 -r 34860182b250 src/Pure/Isar/code.ML --- 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*) diff -r ad9e3594f3f3 -r 34860182b250 src/Pure/Isar/code_unit.ML --- 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 diff -r ad9e3594f3f3 -r 34860182b250 src/Pure/Isar/theory_target.ML --- 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 diff -r ad9e3594f3f3 -r 34860182b250 src/Pure/axclass.ML --- 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 **) diff -r ad9e3594f3f3 -r 34860182b250 src/Tools/code/code_funcgr.ML --- 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; diff -r ad9e3594f3f3 -r 34860182b250 src/Tools/code/code_name.ML --- 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)); diff -r ad9e3594f3f3 -r 34860182b250 src/Tools/code/code_package.ML --- 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; diff -r ad9e3594f3f3 -r 34860182b250 src/Tools/code/code_thingol.ML --- 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