# HG changeset patch # User wenzelm # Date 1683492683 -7200 # Node ID e30a56be9c7bdfb154ad74760aa2a2617c5ed07f # Parent ffdad62bc2354c0df68169b5fb502a766068c4ba# Parent c1b8fdd6588ac232110e61559a4e7b09236fe309 merged diff -r ffdad62bc235 -r e30a56be9c7b NEWS --- a/NEWS Sun May 07 14:52:53 2023 +0100 +++ b/NEWS Sun May 07 22:51:23 2023 +0200 @@ -7,6 +7,17 @@ New in this Isabelle version ---------------------------- +*** General *** + +* The special "of_class" introduction rule for 'class' definitions has +been renamed from "class.NAME.of_class.intro" to "NAME.intro_of_class" +(where NAME is the name specification of the class). E.g. see the HOL +library: + + class.preorder.of_class.intro ~> preorder.intro_of_class + class.order.of_class.intro ~> order.intro_of_class + + *** Document preparation *** * Various well-known LaTeX styles are included as Isabelle components, diff -r ffdad62bc235 -r e30a56be9c7b src/HOL/Library/Lexord.thy --- a/src/HOL/Library/Lexord.thy Sun May 07 14:52:53 2023 +0100 +++ b/src/HOL/Library/Lexord.thy Sun May 07 22:51:23 2023 +0200 @@ -153,7 +153,7 @@ and less_list = lex.lex_less .. instance - by (rule class.preorder.of_class.intro, rule preordering_preorderI, fact lex.preordering) + by (rule preorder.intro_of_class, rule preordering_preorderI, fact lex.preordering) end @@ -171,7 +171,7 @@ qed instance list :: (order) order - by (rule class.order.of_class.intro, rule ordering_orderI, fact lex.ordering) + by (rule order.intro_of_class, rule ordering_orderI, fact lex.ordering) export_code \(\) :: _ list \ _ list \ bool\ \(<) :: _ list \ _ list \ bool\ in Haskell diff -r ffdad62bc235 -r e30a56be9c7b src/HOL/Library/Poly_Mapping.thy --- a/src/HOL/Library/Poly_Mapping.thy Sun May 07 14:52:53 2023 +0100 +++ b/src/HOL/Library/Poly_Mapping.thy Sun May 07 22:51:23 2023 +0200 @@ -910,7 +910,7 @@ is "\f g. less_fun f g \ f = g" . -instance proof (rule class.Orderings.linorder.of_class.intro) +instance proof (rule linorder.intro_of_class) show "class.linorder (less_eq :: (_ \\<^sub>0 _) \ _) less" proof (rule linorder_strictI, rule order_strictI) fix f g h :: "'a \\<^sub>0 'b" diff -r ffdad62bc235 -r e30a56be9c7b src/Pure/General/binding.ML --- a/src/Pure/General/binding.ML Sun May 07 14:52:53 2023 +0100 +++ b/src/Pure/General/binding.ML Sun May 07 22:51:23 2023 +0200 @@ -42,8 +42,9 @@ val print: binding -> string val bad: binding -> string val check: binding -> unit - val name_spec: scope list -> (string * bool) list -> binding -> - {restriction: bool option, concealed: bool, spec: (string * bool) list, full_name: string} + type name_spec = + {restriction: bool option, concealed: bool, suppress: bool list, full_name: string} + val name_spec: scope list -> (string * bool) list -> binding -> name_spec end; structure Binding: BINDING = @@ -194,7 +195,10 @@ val bad_specs = ["", "??", "__"]; -fun name_spec scopes path binding = +type name_spec = + {restriction: bool option, concealed: bool, suppress: bool list, full_name: string}; + +fun name_spec scopes path binding : name_spec = let val Binding {restricted, concealed, prefix, qualifier, name, ...} = binding; val _ = Long_Name.is_qualified name andalso error (bad binding); @@ -213,8 +217,11 @@ andalso error (bad binding); val spec' = if null spec2 then [] else spec; + val suppress = map (not o #2) spec'; val full_name = Long_Name.implode (map #1 spec'); - in {restriction = restriction, concealed = concealed, spec = spec', full_name = full_name} end; + in + {restriction = restriction, concealed = concealed, suppress = suppress, full_name = full_name} + end; end; diff -r ffdad62bc235 -r e30a56be9c7b src/Pure/General/change_table.ML --- a/src/Pure/General/change_table.ML Sun May 07 14:52:53 2023 +0100 +++ b/src/Pure/General/change_table.ML Sun May 07 22:51:23 2023 +0200 @@ -30,6 +30,11 @@ val map_entry: key -> ('a -> 'a) -> 'a T -> 'a T val map_default: key * 'a -> ('a -> 'a) -> 'a T -> 'a T val delete_safe: key -> 'a T -> 'a T + val lookup_list: 'a list T -> Table.key -> 'a list + val insert_list: ('a * 'a -> bool) -> key * 'a -> 'a list T -> 'a list T + val remove_list: ('b * 'a -> bool) -> key * 'b -> 'a list T -> 'a list T + val update_list: ('a * 'a -> bool) -> key * 'a -> 'a list T -> 'a list T + val merge_list: ('a * 'a -> bool) -> 'a list T * 'a list T -> 'a list T end; functor Change_Table(Key: KEY): CHANGE_TABLE = @@ -135,6 +140,9 @@ fun merge eq = join (fn key => fn xy => if eq xy then raise Table.SAME else raise Table.DUP key); +fun merge_list eq = + join (fn _ => fn xy => if eq_list eq xy then raise Table.SAME else Library.merge eq xy); + (* derived operations *) @@ -153,7 +161,11 @@ fun map_default (key, x) f = change_table key (Table.map_default (key, x) f); fun delete_safe key = change_table key (Table.delete_safe key); +fun lookup_list arg = Table.lookup_list (table_of arg); +fun insert_list eq (key, x) = change_table key (Table.insert_list eq (key, x)); +fun remove_list eq (key, x) = change_table key (Table.remove_list eq (key, x)); +fun update_list eq (key, x) = change_table key (Table.update_list eq (key, x)); + end; structure Change_Table = Change_Table(type key = string val ord = fast_string_ord); - diff -r ffdad62bc235 -r e30a56be9c7b src/Pure/General/long_name.ML --- a/src/Pure/General/long_name.ML Sun May 07 14:52:53 2023 +0100 +++ b/src/Pure/General/long_name.ML Sun May 07 22:51:23 2023 +0200 @@ -25,12 +25,13 @@ val count_chunks: chunks -> int val size_chunks: chunks -> int val empty_chunks: chunks + val is_empty_chunks: chunks -> bool val base_chunks: string -> chunks val suppress_chunks: int -> bool list -> string -> chunks val make_chunks: string -> chunks val explode_chunks: chunks -> string list val implode_chunks: chunks -> string - val compare_chunks: chunks * chunks -> order + val compare_chunks: chunks ord val eq_chunks: chunks * chunks -> bool structure Chunks: CHANGE_TABLE end; @@ -107,18 +108,26 @@ fun range_length r = r mod range_limit; fun range_string s r = String.substring (s, range_index r, range_length r); +val range_empty = 0; +val ranges_empty: int vector = Vector.fromList []; + in -abstype chunks = Chunks of {ranges: int list (*reverse*), string: string} +abstype chunks = Chunks of {range0: int, ranges: int list (*reverse*), string: string} with -fun count_chunks (Chunks {ranges, ...}) = length ranges; +val empty_chunks = Chunks {range0 = range_empty, ranges = [], string = ""}; + +fun is_empty_chunks (Chunks {range0, ranges, ...}) = + range0 = range_empty andalso null ranges; -fun size_chunks (Chunks {ranges, ...}) = - if null ranges then 0 - else fold (fn r => fn n => n + range_length r + 1) ranges ~1; +fun count_chunks (chunks as Chunks {ranges, ...}) = + if is_empty_chunks chunks then 0 + else length ranges + 1; -val empty_chunks = Chunks {ranges = [], string = ""}; +fun size_chunks (chunks as Chunks {range0, ranges, ...}) = + if is_empty_chunks chunks then 0 + else fold (fn r => fn n => n + range_length r + 1) ranges (range_length range0); fun base_chunks name = let @@ -126,7 +135,7 @@ val j = i + 1; in if i < 0 then empty_chunks - else Chunks {ranges = [range name j (size name - j)], string = name} + else Chunks {range0 = range name j (size name - j), ranges = [], string = name} end; fun suppress_chunks suppress1 suppress2 string = @@ -158,25 +167,30 @@ if not string_end then suppr_chunks suppr1' suppr2' i' j' rs' else if not (suppr1' = 0 andalso null suppr2') then failure string ("cannot suppress chunks beyond " ^ string_of_int (length rs')) - else if null rs' then empty_chunks - else Chunks {ranges = rs', string = string} + else + (case rs' of + [] => empty_chunks + | r0 :: rest => Chunks {range0 = r0, ranges = rest, string = string}) end; in suppr_chunks suppress1 suppress2 0 0 [] end; val make_chunks = suppress_chunks 0 []; -fun explode_chunks (Chunks {ranges, string}) = - fold (cons o range_string string) ranges []; +fun explode_chunks (chunks as Chunks {range0, ranges, string}) = + if is_empty_chunks chunks then [] + else fold (cons o range_string string) ranges [range_string string range0]; -fun implode_chunks (chunks as Chunks {ranges, string}) = +fun implode_chunks (chunks as Chunks {range0, ranges, string}) = if size_chunks chunks = size string then string - else if length ranges = 1 then range_string string (nth ranges 0) + else if null ranges then range_string string range0 else implode (explode_chunks chunks); val compare_chunks = pointer_eq_ord (fn (chunks1, chunks2) => let - val Chunks {ranges = ranges1, string = string1} = chunks1; - val Chunks {ranges = ranges2, string = string2} = chunks2; + val Chunks {range0 = range01, ranges = ranges1, string = string1} = chunks1; + val Chunks {range0 = range02, ranges = ranges2, string = string2} = chunks2; + val count1 = count_chunks chunks1; + val count2 = count_chunks chunks2; val range_length_ord = int_ord o apply2 range_length; fun range_substring_ord arg = @@ -192,9 +206,20 @@ else EQUAL; in (case int_ord (m, n) of EQUAL => substring_ord 0 | ord => ord) end; in - (case list_ord range_length_ord (ranges1, ranges2) of - EQUAL => dict_ord range_substring_ord (ranges1, ranges2) - | ord => ord) + if count1 = 0 andalso count2 = 0 then EQUAL + else + (case int_ord (count1, count2) of + EQUAL => + (case range_length_ord (range01, range02) of + EQUAL => + (case dict_ord range_length_ord (ranges1, ranges2) of + EQUAL => + (case range_substring_ord (range01, range02) of + EQUAL => dict_ord range_substring_ord (ranges1, ranges2) + | ord => ord) + | ord => ord) + | ord => ord) + | ord => ord) end); val eq_chunks = is_equal o compare_chunks; diff -r ffdad62bc235 -r e30a56be9c7b src/Pure/General/name_space.ML --- a/src/Pure/General/name_space.ML Sun May 07 14:52:53 2023 +0100 +++ b/src/Pure/General/name_space.ML Sun May 07 22:51:23 2023 +0200 @@ -1,28 +1,27 @@ (* Title: Pure/General/name_space.ML - Author: Markus Wenzel, TU Muenchen + Author: Makarius -Generic name spaces with declared and hidden entries; no support for -absolute addressing. +Generic name spaces with authentic declarations, hidden names and aliases. *) -type xstring = string; (*external names*) +type xstring = string; (*external names with partial qualification*) signature NAME_SPACE = sig - type entry = - {concealed: bool, - group: serial, - theory_long_name: string, - pos: Position.T, - serial: serial} type T val empty: string -> T val kind_of: T -> string val markup: T -> string -> Markup.T val markup_def: T -> string -> Markup.T val get_names: T -> string list - val the_entry: T -> string -> entry - val the_entry_theory_name: T -> string -> string + val the_entry: T -> string -> + {concealed: bool, + suppress: bool list, + group: serial, + theory_long_name: string, + pos: Position.T, + serial: serial} + val theory_name: {long: bool} -> T -> string -> string val entry_ord: T -> string ord val is_concealed: T -> string -> bool val intern: T -> xstring -> string @@ -108,103 +107,160 @@ type entry = {concealed: bool, + suppress: bool list, group: serial, theory_long_name: string, pos: Position.T, serial: serial}; -fun entry_markup def kind (name, {pos, serial, ...}: entry) = - Position.make_entity_markup def serial kind (name, pos); +fun markup_entry def kind (name, entry: entry) = + Position.make_entity_markup def (#serial entry) kind (name, #pos entry); fun print_entry_ref kind (name, entry) = - quote (Markup.markup (entry_markup {def = false} kind (name, entry)) name); + quote (Markup.markup (markup_entry {def = false} kind (name, entry)) name); -fun err_dup kind entry1 entry2 pos = +fun err_dup_entry kind entry1 entry2 pos = error ("Duplicate " ^ plain_words kind ^ " declaration " ^ print_entry_ref kind entry1 ^ " vs. " ^ print_entry_ref kind entry2 ^ Position.here pos); +fun update_entry strict kind (name, entry: entry) entries = + (if strict then Change_Table.update_new else Change_Table.update) (name, entry) entries + handle Change_Table.DUP _ => + let val old_entry = the (Change_Table.lookup entries name) + in err_dup_entry kind (name, old_entry) (name, entry) (#pos entry) end; + (* internal names *) -type internal = string list * string list; (*visible, hidden*) -type internals = internal Long_Name.Chunks.T; (*xname -> internal*) +type internals = string list Long_Name.Chunks.T; (*external name -> internal names*) -fun map_internals f xname : internals -> internals = - Long_Name.Chunks.map_default (xname, ([], [])) f; +val merge_internals : internals * internals -> internals = Long_Name.Chunks.merge_list (op =); -val del_name = map_internals o apfst o remove (op =); -fun del_name_extra name = - map_internals (apfst (fn [] => [] | x :: xs => x :: remove (op =) name xs)); -val add_name = map_internals o apfst o update (op =); -fun hide_name name = map_internals (apsnd (update (op =) name)) (Long_Name.make_chunks name); +fun add_internals name xname : internals -> internals = + Long_Name.Chunks.update_list (op =) (xname, name); + +fun del_internals name xname : internals -> internals = + Long_Name.Chunks.remove_list (op =) (xname, name); + +fun del_internals' name xname : internals -> internals = + Long_Name.Chunks.map_default (xname, []) (fn [] => [] | x :: xs => x :: remove (op =) name xs); -(* external accesses *) +(* accesses *) + +local + +fun suppress_prefixes1 [] = [] + | suppress_prefixes1 (s :: ss) = + map (cons false) (if s then suppress_prefixes ss else suppress_prefixes1 ss) +and suppress_prefixes ss = ss :: suppress_prefixes1 ss; + +fun suppress_suffixes ss = map rev (suppress_prefixes (rev ss)); -type external = - {accesses: Long_Name.chunks list, - accesses': Long_Name.chunks list, - entry: entry}; +fun make_chunks full_name m s = + let val chunks = Long_Name.suppress_chunks 0 s full_name + in if Long_Name.count_chunks chunks > m then SOME chunks else NONE end; + +in -type externals = external Change_Table.T; (*name -> external*) +fun make_accesses {intern} restriction (suppress, full_name) = + if restriction = SOME true then [] + else + ((if intern then suppress_prefixes suppress else []) @ suppress_suffixes suppress) + |> map_filter (make_chunks full_name (if is_some restriction then 1 else 0)) + |> distinct Long_Name.eq_chunks; + +end; (* datatype T *) -datatype T = Name_Space of {kind: string, internals: internals, externals: externals}; +datatype T = + Name_Space of + {kind: string, + internals: internals, + internals_hidden: internals, + entries: entry Change_Table.T, + aliases: (bool list * string) list Symtab.table}; -fun make_name_space (kind, internals, externals) = - Name_Space {kind = kind, internals = internals, externals = externals}; +fun make_name_space (kind, internals, internals_hidden, entries, aliases) = + Name_Space {kind = kind, internals = internals, internals_hidden = internals_hidden, + entries = entries, aliases = aliases}; -fun map_name_space f (Name_Space {kind = kind, internals = internals, externals = externals}) = - make_name_space (f (kind, internals, externals)); +fun map_name_space f (Name_Space {kind, internals, internals_hidden, entries, aliases}) = + make_name_space (f (kind, internals, internals_hidden, entries, aliases)); -fun change_base_space begin = map_name_space (fn (kind, internals, externals) => - (kind, - Long_Name.Chunks.change_base begin internals, - Change_Table.change_base begin externals)); +fun change_base_space begin = + map_name_space (fn (kind, internals, internals_hidden, entries, aliases) => + (kind, + Long_Name.Chunks.change_base begin internals, + Long_Name.Chunks.change_base begin internals_hidden, + Change_Table.change_base begin entries, + aliases)); -val change_ignore_space = map_name_space (fn (kind, internals, externals) => - (kind, - Long_Name.Chunks.change_ignore internals, - Change_Table.change_ignore externals)); +val change_ignore_space = + map_name_space (fn (kind, internals, internals_hidden, entries, aliases) => + (kind, + Long_Name.Chunks.change_ignore internals, + Long_Name.Chunks.change_ignore internals_hidden, + Change_Table.change_ignore entries, + aliases)); -fun empty kind = make_name_space (kind, Long_Name.Chunks.empty, Change_Table.empty); +fun empty kind = + make_name_space + (kind, Long_Name.Chunks.empty, Long_Name.Chunks.empty, Change_Table.empty, Symtab.empty); fun kind_of (Name_Space {kind, ...}) = kind; -fun lookup_internals (Name_Space {internals, ...}) = Long_Name.Chunks.lookup internals; -fun lookup_externals (Name_Space {externals, ...}) = Change_Table.lookup externals; +fun lookup_internals (Name_Space {internals, ...}) = + Long_Name.Chunks.lookup_list internals; +fun lookup_internals_hidden (Name_Space {internals_hidden, ...}) = + Long_Name.Chunks.lookup_list internals_hidden; +fun lookup_entries (Name_Space {entries, ...}) = Change_Table.lookup entries; +fun lookup_aliases (Name_Space {aliases, ...}) = Symtab.lookup_list aliases; + + +fun suppress_entry space name = + (case lookup_entries space name of + SOME {suppress, ...} => (suppress, name) + | NONE => ([], name)); + +fun is_alias space c a = + c = a orelse exists (fn (_, b) => b = a) (lookup_aliases space c); + +fun get_aliases space name = + lookup_aliases space name @ [suppress_entry space name]; fun gen_markup def space name = - (case lookup_externals space name of + (case lookup_entries space name of NONE => Markup.intensify - | SOME {entry, ...} => entry_markup def (kind_of space) (name, entry)); + | SOME entry => markup_entry def (kind_of space) (name, entry)); val markup = gen_markup {def = false}; val markup_def = gen_markup {def = true}; -fun undefined (space as Name_Space {kind, externals, ...}) bad = +fun undefined_entry (space as Name_Space {kind, entries, ...}) bad = let val (prfx, sfx) = (case Long_Name.dest_hidden bad of SOME name => - if Change_Table.defined externals name + if Change_Table.defined entries name then ("Inaccessible", Markup.markup (markup space name) (quote name)) else ("Undefined", quote name) | NONE => ("Undefined", quote bad)); in prfx ^ " " ^ plain_words kind ^ ": " ^ sfx end; -fun get_names (Name_Space {externals, ...}) = - Change_Table.fold (cons o #1) externals []; +fun the_entry space name = + (case lookup_entries space name of + SOME entry => entry + | _ => error (undefined_entry space name)); -fun the_entry space name = - (case lookup_externals space name of - NONE => error (undefined space name) - | SOME {entry, ...} => entry); +fun get_names (Name_Space {entries, ...}) = + Change_Table.fold (cons o #1) entries []; -fun the_entry_theory_name space name = - Long_Name.base_name (#theory_long_name (the_entry space name)); +fun theory_name {long} space name = + #theory_long_name (the_entry space name) + |> not long ? Long_Name.base_name; fun entry_ord space = int_ord o apply2 (#serial o the_entry space); @@ -215,18 +271,17 @@ (* intern *) fun intern_chunks space xname = - (case the_default ([], []) (lookup_internals space xname) of - ([name], _) => (name, true) - | (name :: _, _) => (name, false) - | ([], []) => (Long_Name.hidden (Long_Name.implode_chunks xname), true) - | ([], name' :: _) => (Long_Name.hidden name', true)); + (case lookup_internals space xname of + name :: rest => {name = name, full_name = name, unique = null rest} + | [] => + (case lookup_internals_hidden space xname of + name' :: _ => {name = Long_Name.hidden name', full_name = "", unique = true} + | [] => + {name = Long_Name.hidden (Long_Name.implode_chunks xname), + full_name = "", + unique = true})); -fun intern space = #1 o intern_chunks space o Long_Name.make_chunks; - -fun is_valid_access space name xname = - (case lookup_internals space xname of - SOME (name' :: _, _) => name = name' - | _ => false); +fun intern space = #name o intern_chunks space o Long_Name.make_chunks; (* extern *) @@ -241,23 +296,28 @@ val names_short = Config.get ctxt names_short; val names_unique = Config.get ctxt names_unique; - fun valid require_unique xname = - let val (name', is_unique) = intern_chunks space xname - in name = name' andalso (not require_unique orelse is_unique) end; + fun extern_chunks require_unique a chunks = + let val {full_name = c, unique, ...} = intern_chunks space chunks in + if (not require_unique orelse unique) andalso is_alias space c a + then SOME (Long_Name.implode_chunks chunks) + else NONE + end; - fun extern [] = - if valid false (Long_Name.make_chunks name) then name - else Long_Name.hidden name - | extern (a :: bs) = - if valid names_unique a then Long_Name.implode_chunks a - else extern bs; + fun extern_name (suppress, a) = + get_first (extern_chunks names_unique a) + (make_accesses {intern = false} NONE (suppress, a)); + + fun extern_names aliases = + (case get_first extern_name aliases of + SOME xname => xname + | NONE => + (case get_first (fn (_, a) => extern_chunks false a (Long_Name.make_chunks a)) aliases of + SOME xname => xname + | NONE => Long_Name.hidden name)); in if names_long then name else if names_short then Long_Name.base_name name - else - (case lookup_externals space name of - NONE => extern [] - | SOME {accesses', ...} => extern accesses') + else extern_names (get_aliases space name) end; fun extern_ord ctxt space = string_ord o apply2 (extern ctxt space); @@ -306,7 +366,7 @@ else I; in Long_Name.Chunks.fold - (fn (xname', (name :: _, _)) => complete (Long_Name.implode_chunks xname') name | _ => I) + (fn (xname', name :: _) => complete (Long_Name.implode_chunks xname') name | _ => I) internals [] |> sort_distinct result_ord |> map #2 @@ -316,23 +376,22 @@ (* merge *) fun merge - (Name_Space {kind = kind1, internals = internals1, externals = externals1}, - Name_Space {kind = kind2, internals = internals2, externals = externals2}) = + (Name_Space {kind = kind1, internals = internals1, internals_hidden = internals_hidden1, + entries = entries1, aliases = aliases1}, + Name_Space {kind = kind2, internals = internals2, internals_hidden = internals_hidden2, + entries = entries2, aliases = aliases2}) = let val kind' = if kind1 = kind2 then kind1 else error ("Attempt to merge different kinds of name spaces " ^ quote kind1 ^ " vs. " ^ quote kind2); - val internals' = (internals1, internals2) |> Long_Name.Chunks.join - (K (fn ((names1, names1'), (names2, names2')) => - if pointer_eq (names1, names2) andalso pointer_eq (names1', names2') - then raise Long_Name.Chunks.SAME - else (Library.merge (op =) (names1, names2), Library.merge (op =) (names1', names2')))); - val externals' = (externals1, externals2) |> Change_Table.join - (fn name => fn ({entry = entry1, ...}, {entry = entry2, ...}) => - if #serial entry1 = #serial entry2 then raise Change_Table.SAME - else err_dup kind' (name, entry1) (name, entry2) Position.none); - in make_name_space (kind', internals', externals') end; + val internals' = merge_internals (internals1, internals2); + val internals_hidden' = merge_internals (internals_hidden1, internals_hidden2); + val entries' = (entries1, entries2) |> Change_Table.join (fn name => fn (entry1, entry2) => + if op = (apply2 #serial (entry1, entry2)) then raise Change_Table.SAME + else err_dup_entry kind' (name, entry1) (name, entry2) Position.none); + val aliases' = Symtab.merge_list (op =) (aliases1, aliases2); + in make_name_space (kind', internals', internals_hidden', entries', aliases') end; @@ -446,72 +505,37 @@ val base_name = Long_Name.base_name o full_name global_naming; -(* accesses *) - -local - -fun mandatory xs = fold_rev (fn (x, b) => b ? cons x) xs []; - -fun mandatory_prefixes xs = mandatory xs :: mandatory_prefixes1 xs -and mandatory_prefixes1 [] = [] - | mandatory_prefixes1 ((x, true) :: xs) = map (cons x) (mandatory_prefixes1 xs) - | mandatory_prefixes1 ((x, false) :: xs) = map (cons x) (mandatory_prefixes xs); - -fun mandatory_suffixes xs = map rev (mandatory_prefixes (rev xs)); - -in - -fun make_accesses naming binding = - let - val args as {restriction, spec, ...} = name_spec naming binding; - val accesses = - if restriction = SOME true then ([], []) - else - let - val restrict = is_some restriction ? filter (fn [_] => false | _ => true); - val sfxs = restrict (mandatory_suffixes spec); - val pfxs = restrict (mandatory_prefixes spec); - in apply2 (map Long_Name.implode o distinct op =) (sfxs @ pfxs, sfxs) end; - in (apply2 (map Long_Name.make_chunks) accesses (* FIXME suppress_chunks *), args) end; - -end; - - (* hide *) fun hide fully name space = - space |> map_name_space (fn (kind, internals, externals) => + space |> map_name_space (fn (kind, internals, internals_hidden, entries, aliases) => let val _ = the_entry space name; - val (accesses, accesses') = - (case lookup_externals space name of - NONE => ([], []) - | SOME {accesses, accesses', ...} => (accesses, accesses')); - val xnames = filter (is_valid_access space name) accesses; - val xnames' = - if fully then xnames - else inter Long_Name.eq_chunks [Long_Name.base_chunks name] xnames; + val hide_names = get_aliases space name; + val accesses = + maps (make_accesses {intern = true} NONE) hide_names + |> not fully ? inter Long_Name.eq_chunks [Long_Name.base_chunks name]; + val accesses' = maps (make_accesses {intern = false} NONE) hide_names; val internals' = internals - |> hide_name name - |> fold (del_name name) xnames' - |> fold (del_name_extra name) accesses'; - in (kind, internals', externals) end); + |> fold (del_internals name) accesses + |> fold (del_internals' name) accesses'; + val internals_hidden' = internals_hidden + |> add_internals name (Long_Name.make_chunks name); + in (kind, internals', internals_hidden', entries, aliases) end); (* alias *) fun alias naming binding name space = - space |> map_name_space (fn (kind, internals, externals) => + space |> map_name_space (fn (kind, internals, internals_hidden, entries, aliases) => let val _ = the_entry space name; - val (more_accs, more_accs') = #1 (make_accesses naming binding); - val internals' = internals |> fold (add_name name) more_accs; - val externals' = externals - |> Change_Table.map_entry name (fn {accesses, accesses', entry} => - {accesses = fold_rev (update Long_Name.eq_chunks) more_accs accesses, - accesses' = fold_rev (update Long_Name.eq_chunks) more_accs' accesses', - entry = entry}); - in (kind, internals', externals') end); + val {restriction, suppress, full_name = alias_name, ...} = name_spec naming binding; + val _ = alias_name = "" andalso error (Binding.bad binding); + val alias_accesses = make_accesses {intern = true} restriction (suppress, alias_name); + val internals' = internals |> fold (add_internals name) alias_accesses; + val aliases' = aliases |> Symtab.update_list (op =) (name, (suppress, alias_name)); + in (kind, internals', internals_hidden, entries, aliases') end); @@ -540,36 +564,33 @@ (* declaration *) -fun declared (Name_Space {externals, ...}) = Change_Table.defined externals; +fun declared (Name_Space {entries, ...}) = Change_Table.defined entries; fun declare context strict binding space = let val naming = naming_of context; val Naming {group, theory_long_name, ...} = naming; - val ((accesses, accesses'), {concealed, full_name = name, ...}) = make_accesses naming binding; + val name_spec as {restriction, suppress, full_name = name, ...} = name_spec naming binding; val _ = name = "" andalso error (Binding.bad binding); + val accesses = make_accesses {intern = true} restriction (suppress, name); val (proper_pos, pos) = Position.default (Binding.pos_of binding); - val entry = - {concealed = concealed, + val entry: entry = + {concealed = #concealed name_spec, + suppress = suppress, group = group, theory_long_name = theory_long_name, pos = pos, serial = serial ()}; val space' = - space |> map_name_space (fn (kind, internals, externals) => + space |> map_name_space (fn (kind, internals, internals_hidden, entries, aliases) => let - val internals' = internals |> fold (add_name name) accesses; - val externals' = - (if strict then Change_Table.update_new else Change_Table.update) - (name, {accesses = accesses, accesses' = accesses', entry = entry}) externals - handle Change_Table.DUP dup => - err_dup kind (dup, #entry (the (lookup_externals space dup))) - (name, entry) (#pos entry); - in (kind, internals', externals') end); + val internals' = internals |> fold (add_internals name) accesses; + val entries' = entries |> update_entry strict kind (name, entry); + in (kind, internals', internals_hidden, entries', aliases) end); val _ = if proper_pos andalso Context_Position.is_reported_generic context pos then - Position.report pos (entry_markup {def = true} (kind_of space) (name, entry)) + Position.report pos (markup_entry {def = true} (kind_of space) (name, entry)) else (); in (name, space') end; @@ -596,7 +617,7 @@ |> map (fn pos => (pos, markup space name)); in ((name, reports), x) end | NONE => - error (undefined space name ^ Position.here_list ps ^ + error (undefined_entry space name ^ Position.here_list ps ^ Completion.markup_report (map (fn pos => completion context space (K true) (xname, pos)) ps))) end; @@ -614,7 +635,7 @@ fun get table name = (case lookup_key table name of SOME (_, x) => x - | NONE => error (undefined (space_of_table table) name)); + | NONE => error (undefined_entry (space_of_table table) name)); fun define context strict (binding, x) (Table (space, tab)) = let diff -r ffdad62bc235 -r e30a56be9c7b src/Pure/General/table.ML --- a/src/Pure/General/table.ML Sun May 07 14:52:53 2023 +0100 +++ b/src/Pure/General/table.ML Sun May 07 22:51:23 2023 +0200 @@ -56,8 +56,8 @@ val lookup_list: 'a list table -> key -> 'a list val cons_list: key * 'a -> 'a list table -> 'a list table val insert_list: ('a * 'a -> bool) -> key * 'a -> 'a list table -> 'a list table + val update_list: ('a * 'a -> bool) -> key * 'a -> 'a list table -> 'a list table val remove_list: ('b * 'a -> bool) -> key * 'b -> 'a list table -> 'a list table - val update_list: ('a * 'a -> bool) -> key * 'a -> 'a list table -> 'a list table val make_list: (key * 'a) list -> 'a list table val dest_list: 'a list table -> (key * 'a) list val merge_list: ('a * 'a -> bool) -> 'a list table * 'a list table -> 'a list table @@ -621,20 +621,27 @@ fun cons_list (key, x) tab = modify key (fn NONE => [x] | SOME xs => x :: xs) tab; -fun insert_list eq (key, x) = - modify key (fn NONE => [x] | SOME xs => if Library.member eq xs x then raise SAME else x :: xs); +fun modify_list key f = + modify key (fn arg => + let + val xs = the_default [] arg; + val ys = f xs; + in if pointer_eq (xs, ys) then raise SAME else ys end); + +fun insert_list eq (key, x) = modify_list key (Library.insert eq x); +fun update_list eq (key, x) = modify_list key (Library.update eq x); fun remove_list eq (key, x) tab = - map_entry key (fn xs => (case Library.remove eq x xs of [] => raise UNDEF key | ys => ys)) tab + map_entry key (fn xs => + (case Library.remove eq x xs of + [] => raise UNDEF key + | ys => if pointer_eq (xs, ys) then raise SAME else ys)) tab handle UNDEF _ => delete key tab; -fun update_list eq (key, x) = - modify key (fn NONE => [x] | SOME [] => [x] | SOME (xs as y :: _) => - if eq (x, y) then raise SAME else Library.update eq x xs); - fun make_list args = build (fold_rev cons_list args); fun dest_list tab = maps (fn (key, xs) => map (pair key) xs) (dest tab); -fun merge_list eq = join (fn _ => Library.merge eq); +fun merge_list eq = + join (fn _ => fn xy => if eq_list eq xy then raise SAME else Library.merge eq xy); (* set operations *) diff -r ffdad62bc235 -r e30a56be9c7b src/Pure/Isar/class_declaration.ML --- a/src/Pure/Isar/class_declaration.ML Sun May 07 14:52:53 2023 +0100 +++ b/src/Pure/Isar/class_declaration.ML Sun May 07 22:51:23 2023 +0200 @@ -322,13 +322,13 @@ fun gen_class prep_class_spec b raw_includes raw_supclasses raw_elems thy = let val class = Sign.full_name thy b; - val prefix = Binding.qualify true "class"; val ctxt = Proof_Context.init_global thy; val (((sups, supparam_names), (supsort, base_sort, supexpr)), (includes, elems, global_syntax)) = prep_class_spec ctxt raw_supclasses raw_includes raw_elems; + val of_class_binding = Binding.qualify_name true b "intro_of_class"; in thy - |> Expression.add_locale b (prefix b) includes supexpr elems + |> Expression.add_locale b (Binding.qualify true "class" b) includes supexpr elems |> snd |> Local_Theory.exit_global |> adjungate_axclass b class base_sort sups supsort supparam_names global_syntax |-> (fn (param_map, params, assm_axiom) => @@ -339,7 +339,7 @@ mixin = Option.map (rpair true) eq_morph, export = export_morph}) #> Class.register class sups params base_sort base_morph export_morph some_axiom some_assm_intro of_class - #> Global_Theory.store_thm (prefix (Binding.qualified_name (class ^ ".of_class.intro")), of_class))) + #> Global_Theory.store_thm (of_class_binding, of_class))) |> snd |> Named_Target.init includes class |> pair class diff -r ffdad62bc235 -r e30a56be9c7b src/Pure/Isar/entity.ML diff -r ffdad62bc235 -r e30a56be9c7b src/Pure/Isar/proof_context.ML diff -r ffdad62bc235 -r e30a56be9c7b src/Pure/Thy/export_theory.ML diff -r ffdad62bc235 -r e30a56be9c7b src/Pure/consts.ML diff -r ffdad62bc235 -r e30a56be9c7b src/Pure/facts.ML diff -r ffdad62bc235 -r e30a56be9c7b src/Pure/global_theory.ML diff -r ffdad62bc235 -r e30a56be9c7b src/Pure/library.ML --- a/src/Pure/library.ML Sun May 07 14:52:53 2023 +0100 +++ b/src/Pure/library.ML Sun May 07 22:51:23 2023 +0200 @@ -198,7 +198,7 @@ val is_greater_equal: order -> bool val rev_order: order -> order val make_ord: ('a * 'a -> bool) -> 'a ord - val pointer_eq_ord: ('a * 'a -> order) -> 'a * 'a -> order + val pointer_eq_ord: 'a ord -> 'a ord val bool_ord: bool ord val int_ord: int ord val string_ord: string ord @@ -371,12 +371,21 @@ (* basic list functions *) -fun eq_list eq (list1, list2) = - pointer_eq (list1, list2) orelse - let - fun eq_lst (x :: xs, y :: ys) = eq (x, y) andalso eq_lst (xs, ys) - | eq_lst _ = true; - in length list1 = length list2 andalso eq_lst (list1, list2) end; +fun eq_list eq lists = + let + fun eq_len args = + pointer_eq args orelse + (case args of + (_ :: xs, _ :: ys) => eq_len (xs, ys) + | ([], []) => true + | _ => false); + fun eq_lst args = + pointer_eq args orelse + (case args of + (x :: xs, y :: ys) => eq (x, y) andalso eq_lst (xs, ys) + | ([], []) => true + | _ => false); + in eq_len lists andalso eq_lst lists end; fun maps f [] = [] | maps f (x :: xs) = f x @ maps f xs; @@ -607,9 +616,8 @@ else ([], (xs, ys)); fun prefixes1 [] = [] - | prefixes1 (x :: xs) = map (cons x) ([] :: prefixes1 xs); - -fun prefixes xs = [] :: prefixes1 xs; + | prefixes1 (x :: xs) = map (cons x) (prefixes xs) +and prefixes xs = [] :: prefixes1 xs; fun suffixes1 xs = map rev (prefixes1 (rev xs)); fun suffixes xs = [] :: suffixes1 xs; @@ -828,7 +836,13 @@ fun insert eq x xs = if member eq xs x then xs else x :: xs; fun remove eq x xs = if member eq xs x then filter_out (fn y => eq (x, y)) xs else xs; -fun update eq x xs = cons x (remove eq x xs); + +fun update eq x list = + (case list of + [] => [x] + | y :: rest => + if member eq rest x then x :: remove eq x list + else if eq (x, y) then list else x :: list); fun inter eq xs = filter (member eq xs); @@ -955,15 +969,17 @@ | dict_ord _ ([], _ :: _) = LESS | dict_ord _ (_ :: _, []) = GREATER; -(*lexicographic product of lists*) -fun length_ord (xs, ys) = int_ord (length xs, length ys); -fun list_ord elem_ord = length_ord ||| dict_ord elem_ord; +fun length_ord args = + (case args of + (_ :: xs, _ :: ys) => length_ord (xs, ys) + | ([], []) => EQUAL + | ([], _ :: _) => LESS + | (_ :: _, []) => GREATER); -fun vector_ord ord = - pointer_eq_ord (int_ord o apply2 Vector.length ||| Vector.collate ord); - -fun array_ord ord = - pointer_eq_ord (int_ord o apply2 Array.length ||| Array.collate ord); +(*lexicographic product of lists, vectors, arrays*) +fun list_ord elem_ord = length_ord ||| dict_ord elem_ord; +fun vector_ord ord = pointer_eq_ord (int_ord o apply2 Vector.length ||| Vector.collate ord); +fun array_ord ord = pointer_eq_ord (int_ord o apply2 Array.length ||| Array.collate ord); (* sorting *) diff -r ffdad62bc235 -r e30a56be9c7b src/Pure/thm.ML --- a/src/Pure/thm.ML Sun May 07 14:52:53 2023 +0100 +++ b/src/Pure/thm.ML Sun May 07 22:51:23 2023 +0200 @@ -400,7 +400,6 @@ in val union_constraints = Ord_List.union constraint_ord; -val unions_constraints = Ord_List.unions constraint_ord; fun insert_constraints thy (T, S) = let @@ -481,7 +480,6 @@ val union_hyps = Ord_List.union Term_Ord.fast_term_ord; -val unions_hyps = Ord_List.unions Term_Ord.fast_term_ord; val insert_hyps = Ord_List.insert Term_Ord.fast_term_ord; val remove_hyps = Ord_List.remove Term_Ord.fast_term_ord; @@ -503,7 +501,6 @@ val maxidx_of = #maxidx o rep_thm; fun maxidx_thm th i = Int.max (maxidx_of th, i); -val constraints_of = #constraints o rep_thm; val shyps_of = #shyps o rep_thm; val hyps_of = #hyps o rep_thm; val prop_of = #prop o rep_thm; diff -r ffdad62bc235 -r e30a56be9c7b src/Pure/type.ML diff -r ffdad62bc235 -r e30a56be9c7b src/Pure/variable.ML --- a/src/Pure/variable.ML Sun May 07 14:52:53 2023 +0100 +++ b/src/Pure/variable.ML Sun May 07 22:51:23 2023 +0200 @@ -433,7 +433,7 @@ ctxt |> map_fixes (Name_Space.define context true (Binding.make (x', pos), (x, proper)) #> snd #> - Name_Space.alias_table Name_Space.global_naming (Binding.make (x, pos)) x') + x <> "" ? Name_Space.alias_table Name_Space.global_naming (Binding.make (x, pos)) x') |> declare_fixed x |> declare_constraints (Syntax.free x') end; diff -r ffdad62bc235 -r e30a56be9c7b src/Tools/Code/code_symbol.ML --- a/src/Tools/Code/code_symbol.ML Sun May 07 14:52:53 2023 +0100 +++ b/src/Tools/Code/code_symbol.ML Sun May 07 22:51:23 2023 +0200 @@ -97,8 +97,9 @@ end; local - val thyname_of_type = Name_Space.the_entry_theory_name o Sign.type_space; - val thyname_of_class = Name_Space.the_entry_theory_name o Sign.class_space; + val thyname_of = Name_Space.theory_name {long = false}; + val thyname_of_type = thyname_of o Sign.type_space; + val thyname_of_class = thyname_of o Sign.class_space; fun thyname_of_instance thy inst = case Thm.theory_names_of_arity {long = false} thy inst of [] => error ("No such instance: " ^ quote (fst inst ^ " :: " ^ snd inst)) | thyname :: _ => thyname; @@ -106,7 +107,7 @@ of SOME class => thyname_of_class thy class | NONE => (case Code.get_type_of_constr_or_abstr thy c of SOME (tyco, _) => thyname_of_type thy tyco - | NONE => Name_Space.the_entry_theory_name (Sign.const_space thy) c); + | NONE => thyname_of (Sign.const_space thy) c); fun prefix thy (Constant "") = "Code" | prefix thy (Constant c) = thyname_of_const thy c | prefix thy (Type_Constructor tyco) = thyname_of_type thy tyco