# HG changeset patch # User wenzelm # Date 1565113666 -7200 # Node ID 98b6da301e139fe742e014e314de17dcce65b89c # Parent 2353966954011ff5d30a2b3d1a894f8aac81000c backed out changeset 1b8858f4c393: odd problems e.g. in CAVA_LTL_Modelchecker; diff -r 235396695401 -r 98b6da301e13 src/Pure/axclass.ML --- a/src/Pure/axclass.ML Tue Aug 06 19:07:12 2019 +0200 +++ b/src/Pure/axclass.ML Tue Aug 06 19:47:46 2019 +0200 @@ -9,7 +9,6 @@ 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 @@ -68,67 +67,59 @@ 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, arity_thynames, params, inst_params) = - Data {axclasses = axclasses, arity_thynames = arity_thynames, - params = params, inst_params = inst_params}; +fun make_data (axclasses, params, inst_params) = + Data {axclasses = axclasses, params = params, inst_params = inst_params}; structure Data = Theory_Data' ( type T = data; - val empty = make_data (Symtab.empty, Symreltab.empty, [], (Symtab.empty, Symtab.empty)); + val empty = make_data (Symtab.empty, [], (Symtab.empty, Symtab.empty)); val extend = I; fun merge old_thys - (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}) = + (Data {axclasses = axclasses1, params = params1, inst_params = inst_params1}, + Data {axclasses = axclasses2, 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', arity_thynames', params', inst_params') end; + in make_data (axclasses', params', inst_params') end; ); fun map_data f = - Data.map (fn Data {axclasses, arity_thynames, params, inst_params} => - make_data (f (axclasses, arity_thynames, params, inst_params))); + Data.map (fn Data {axclasses, params, inst_params} => + make_data (f (axclasses, params, inst_params))); fun map_axclasses f = - 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)); + map_data (fn (axclasses, params, inst_params) => + (f axclasses, params, inst_params)); fun map_params f = - map_data (fn (axclasses, arity_thynames, params, inst_params) => - (axclasses, arity_thynames, f params, inst_params)); + map_data (fn (axclasses, params, inst_params) => + (axclasses, f params, inst_params)); fun map_inst_params f = - map_data (fn (axclasses, arity_thynames, params, inst_params) => - (axclasses, arity_thynames, params, f inst_params)); + map_data (fn (axclasses, params, inst_params) => + (axclasses, 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; @@ -151,18 +142,6 @@ 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) = @@ -311,7 +290,6 @@ 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 235396695401 -r 98b6da301e13 src/Pure/thm.ML --- a/src/Pure/thm.ML Tue Aug 06 19:07:12 2019 +0200 +++ b/src/Pure/thm.ML Tue Aug 06 19:47:46 2019 +0200 @@ -167,6 +167,7 @@ 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; @@ -874,7 +875,7 @@ datatype classes = Classes of {classrels: thm Symreltab.table, - arities: thm Aritytab.table}; + arities: (thm * string * serial) Aritytab.table}; fun make_classes (classrels, arities) = Classes {classrels = classrels, arities = arities}; @@ -927,7 +928,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,7 +2211,12 @@ (* type arities *) -fun insert_arity_completions thy ((t, Ss, c), th) (finished, 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) = let val completions = Sign.super_classes thy c |> map_filter (fn c1 => @@ -2222,7 +2228,7 @@ |> standard_tvars |> close_derivation |> trim_context; - in SOME ((t, Ss, c1), th1) end); + in SOME ((t, Ss, c1), (th1, thy_name, ser)) end); val finished' = finished andalso null completions; val arities' = fold Aritytab.update completions arities; in (finished', arities') end; @@ -2263,7 +2269,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)); + val ar = ((t, Ss, c), (th |> unconstrainT |> trim_context, Context.theory_name thy, serial ())); in thy |> Sign.primitive_arity (t, Ss, [c]) diff -r 235396695401 -r 98b6da301e13 src/Tools/Code/code_symbol.ML --- a/src/Tools/Code/code_symbol.ML Tue Aug 06 19:07:12 2019 +0200 +++ b/src/Tools/Code/code_symbol.ML Tue Aug 06 19:47:46 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 Axclass.get_arity_thyname thy inst - of NONE => error ("No such instance: " ^ quote (fst inst ^ " :: " ^ snd inst)) - | SOME thyname => thyname; + 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_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