# HG changeset patch # User wenzelm # Date 1565014303 -7200 # Node ID 1b8858f4c393681dd747037cb32d31ea041685b8 # Parent b32d571f1190299ea6eb1f772f5ca8417744e999 clarified modules: more direct data implementation; diff -r b32d571f1190 -r 1b8858f4c393 src/Pure/axclass.ML --- a/src/Pure/axclass.ML Mon Aug 05 11:20:56 2019 +0200 +++ b/src/Pure/axclass.ML Mon Aug 05 16:11:43 2019 +0200 @@ -9,6 +9,7 @@ sig type info = {def: thm, intro: thm, axioms: thm list, params: (string * typ) list} val get_info: theory -> class -> info + val get_arity_thyname: theory -> string * class -> string option val class_of_param: theory -> string -> class option val instance_name: string * class -> string val param_of_inst: theory -> string * string -> string @@ -67,59 +68,67 @@ datatype data = Data of {axclasses: info Symtab.table, + arity_thynames: string Symreltab.table, params: param list, - (*arity theorems with theory name*) 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 make_data (axclasses, params, inst_params) = - Data {axclasses = axclasses, params = params, inst_params = inst_params}; +fun make_data (axclasses, arity_thynames, params, inst_params) = + Data {axclasses = axclasses, arity_thynames = arity_thynames, + params = params, inst_params = inst_params}; structure Data = Theory_Data' ( type T = data; - val empty = make_data (Symtab.empty, [], (Symtab.empty, Symtab.empty)); + val empty = make_data (Symtab.empty, Symreltab.empty, [], (Symtab.empty, Symtab.empty)); val extend = I; fun merge old_thys - (Data {axclasses = axclasses1, params = params1, inst_params = inst_params1}, - Data {axclasses = axclasses2, params = params2, inst_params = inst_params2}) = + (Data {axclasses = axclasses1, arity_thynames = arity_thynames1, + params = params1, inst_params = inst_params1}, + Data {axclasses = axclasses2, arity_thynames = arity_thynames2, + params = params2, inst_params = inst_params2}) = let val old_ctxt = Syntax.init_pretty_global (fst old_thys); val axclasses' = Symtab.merge (K true) (axclasses1, axclasses2); + val arity_thynames' = Symreltab.merge (K true) (arity_thynames1, arity_thynames2); val params' = if null params1 then params2 else fold_rev (fn p => if member (op =) params1 p then I else add_param old_ctxt p) params2 params1; - val inst_params' = (Symtab.join (K (Symtab.merge (K true))) (#1 inst_params1, #1 inst_params2), Symtab.merge (K true) (#2 inst_params1, #2 inst_params2)); - in make_data (axclasses', params', inst_params') end; + in make_data (axclasses', arity_thynames', params', inst_params') end; ); fun map_data f = - Data.map (fn Data {axclasses, params, inst_params} => - make_data (f (axclasses, params, inst_params))); + Data.map (fn Data {axclasses, arity_thynames, params, inst_params} => + make_data (f (axclasses, arity_thynames, params, inst_params))); fun map_axclasses f = - map_data (fn (axclasses, params, inst_params) => - (f axclasses, params, inst_params)); + map_data (fn (axclasses, arity_thynames, params, inst_params) => + (f axclasses, arity_thynames, params, inst_params)); + +fun map_arity_thynames f = + map_data (fn (axclasses, arity_thynames, params, inst_params) => + (axclasses, f arity_thynames, params, inst_params)); fun map_params f = - map_data (fn (axclasses, params, inst_params) => - (axclasses, f params, inst_params)); + map_data (fn (axclasses, arity_thynames, params, inst_params) => + (axclasses, arity_thynames, f params, inst_params)); fun map_inst_params f = - map_data (fn (axclasses, params, inst_params) => - (axclasses, params, f inst_params)); + map_data (fn (axclasses, arity_thynames, params, inst_params) => + (axclasses, arity_thynames, params, f inst_params)); val rep_data = Data.get #> (fn Data args => args); val axclasses_of = #axclasses o rep_data; +val arity_thynames_of = #arity_thynames o rep_data; val params_of = #params o rep_data; val inst_params_of = #inst_params o rep_data; @@ -142,6 +151,18 @@ fun class_of_param thy = AList.lookup (op =) (params_of thy); +(* theory name of first type instantiation *) + +fun get_arity_thyname thy (t, c) = + get_first (fn c' => Symreltab.lookup (arity_thynames_of thy) (t, c')) + (c :: Sign.super_classes thy c); + +fun put_arity_thyname ar thy = + if is_some (get_arity_thyname thy ar) then thy + else map_arity_thynames (Symreltab.update (ar, Context.theory_name thy)) thy; + + + (* maintain instance parameters *) fun get_inst_param thy (c, tyco) = @@ -290,6 +311,7 @@ thy |> Global_Theory.store_thm (binding, th) |-> Thm.add_arity + |> put_arity_thyname (t, c) |> fold (#2 oo declare_overloaded) missing_params end; diff -r b32d571f1190 -r 1b8858f4c393 src/Pure/thm.ML --- a/src/Pure/thm.ML Mon Aug 05 11:20:56 2019 +0200 +++ b/src/Pure/thm.ML Mon Aug 05 16:11:43 2019 +0200 @@ -167,7 +167,6 @@ val bicompose: Proof.context option -> {flatten: bool, match: bool, incremented: bool} -> bool * thm * int -> int -> thm -> thm Seq.seq val biresolution: Proof.context option -> bool -> (bool * thm) list -> int -> thm -> thm Seq.seq - val thynames_of_arity: theory -> string * class -> string list val add_classrel: thm -> theory -> theory val add_arity: thm -> theory -> theory end; @@ -875,7 +874,7 @@ datatype classes = Classes of {classrels: thm Symreltab.table, - arities: (thm * string * serial) Aritytab.table}; + arities: thm Aritytab.table}; fun make_classes (classrels, arities) = Classes {classrels = classrels, arities = arities}; @@ -928,7 +927,7 @@ fun the_arity thy (a, Ss, c) = (case Aritytab.lookup (get_arities thy) (a, Ss, c) of - SOME (thm, _, _) => transfer thy thm + SOME thm => transfer thy thm | NONE => error ("Unproven type arity " ^ Syntax.string_of_arity (Proof_Context.init_global thy) (a, Ss, [c]))); @@ -2210,12 +2209,7 @@ (* type arities *) -fun thynames_of_arity thy (a, c) = - (get_arities thy, []) |-> Aritytab.fold - (fn ((a', _, c'), (_, name, ser)) => (a = a' andalso c = c') ? cons (name, ser)) - |> sort (int_ord o apply2 #2) |> map #1; - -fun insert_arity_completions thy ((t, Ss, c), (th, thy_name, ser)) (finished, arities) = +fun insert_arity_completions thy ((t, Ss, c), th) (finished, arities) = let val completions = Sign.super_classes thy c |> map_filter (fn c1 => @@ -2227,7 +2221,7 @@ |> standard_tvars |> close_derivation |> trim_context; - in SOME ((t, Ss, c1), (th1, thy_name, ser)) end); + in SOME ((t, Ss, c1), th1) end); val finished' = finished andalso null completions; val arities' = fold Aritytab.update completions arities; in (finished', arities') end; @@ -2268,7 +2262,7 @@ val th = strip_shyps (transfer thy raw_th); val prop = plain_prop_of th; val (t, Ss, c) = Logic.dest_arity prop; - val ar = ((t, Ss, c), (th |> unconstrainT |> trim_context, Context.theory_name thy, serial ())); + val ar = ((t, Ss, c), (th |> unconstrainT |> trim_context)); in thy |> Sign.primitive_arity (t, Ss, [c]) diff -r b32d571f1190 -r 1b8858f4c393 src/Tools/Code/code_symbol.ML --- a/src/Tools/Code/code_symbol.ML Mon Aug 05 11:20:56 2019 +0200 +++ b/src/Tools/Code/code_symbol.ML Mon Aug 05 16:11:43 2019 +0200 @@ -99,9 +99,9 @@ local fun thyname_of_type thy = #theory_name o Name_Space.the_entry (Sign.type_space thy); fun thyname_of_class thy = #theory_name o Name_Space.the_entry (Sign.class_space thy); - fun thyname_of_instance thy inst = case Thm.thynames_of_arity thy inst - of [] => error ("No such instance: " ^ quote (fst inst ^ " :: " ^ snd inst)) - | thyname :: _ => thyname; + fun thyname_of_instance thy inst = case Axclass.get_arity_thyname thy inst + of NONE => error ("No such instance: " ^ quote (fst inst ^ " :: " ^ snd inst)) + | SOME thyname => thyname; fun thyname_of_const thy c = case Axclass.class_of_param thy c of SOME class => thyname_of_class thy class | NONE => (case Code.get_type_of_constr_or_abstr thy c