# HG changeset patch # User wenzelm # Date 1683408020 -7200 # Node ID a12c48fbf10f0b570368ab39b7a3c125d76a8ec3 # Parent 14d133cff0735afbe0af8f5a75b7936dd79b9f2a back to more elementary concept of aliases as adhoc change of accesses, but now with "suppress" information (see also 31ea5c1f874d); diff -r 14d133cff073 -r a12c48fbf10f src/Pure/General/name_space.ML --- a/src/Pure/General/name_space.ML Sat May 06 14:49:54 2023 +0200 +++ b/src/Pure/General/name_space.ML Sat May 06 23:20:20 2023 +0200 @@ -14,7 +14,7 @@ val kind_of: T -> string val markup: T -> string -> Markup.T val markup_def: T -> string -> Markup.T - val decl_names: T -> string list + val get_names: T -> string list val the_entry: T -> string -> {concealed: bool, suppress: bool list, @@ -63,7 +63,7 @@ val full_name: naming -> binding -> string val base_name: binding -> string val hide: bool -> string -> T -> T - val alias: naming -> bool -> binding -> string -> T -> T + val alias: naming -> binding -> string -> T -> T val naming_of: Context.generic -> naming val map_naming: (naming -> naming) -> Context.generic -> Context.generic val declared: T -> string -> bool @@ -80,7 +80,7 @@ val lookup_key: 'a table -> string -> (string * 'a) option val get: 'a table -> string -> 'a val define: Context.generic -> bool -> binding * 'a -> 'a table -> string * 'a table - val alias_table: naming -> bool -> binding -> string -> 'a table -> 'a table + val alias_table: naming -> binding -> string -> 'a table -> 'a table val hide_table: bool -> string -> 'a table -> 'a table val del_table: string -> 'a table -> 'a table val map_table_entry: string -> ('a -> 'a) -> 'a table -> 'a table @@ -106,7 +106,7 @@ (* datatype entry *) -type decl = +type entry = {concealed: bool, suppress: bool list, group: serial, @@ -114,19 +114,8 @@ pos: Position.T, serial: serial}; -type alias = - {suppress: bool list, - pos: Position.T, - serial: serial}; - -datatype entry = Decl of decl | Alias of alias; - -val entry_suppress = fn Decl {suppress, ...} => suppress | Alias {suppress, ...} => suppress; -val entry_pos = fn Decl {pos, ...} => pos | Alias {pos, ...} => pos; -val entry_serial = fn Decl {serial, ...} => serial | Alias {serial, ...} => serial; - -fun markup_entry def kind (name, entry) = - Position.make_entity_markup def (entry_serial entry) kind (name, entry_pos entry); +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 (markup_entry {def = false} kind (name, entry)) name); @@ -135,11 +124,11 @@ 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) entries = +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) (entry_pos entry) end; + in err_dup_entry kind (name, old_entry) (name, entry) (#pos entry) end; (* internal names *) @@ -193,7 +182,7 @@ internals: internals, internals_hidden: internals, entries: entry Change_Table.T, - aliases: string list Symtab.table}; + aliases: (bool list * string) list Symtab.table}; fun make_name_space (kind, internals, internals_hidden, entries, aliases) = Name_Space {kind = kind, internals = internals, internals_hidden = internals_hidden, @@ -231,30 +220,33 @@ 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 member (op =) (lookup_aliases space c) a; + c = a orelse exists (fn (_, b) => b = a) (lookup_aliases space c); fun get_aliases space name = - lookup_aliases space name @ [name]; + lookup_aliases space name @ [suppress_entry space name]; fun is_valid_access space name xname = (case lookup_internals space xname of name' :: _ => name = name' | _ => false); -fun get_accesses {intern, aliases, valid} space name = +fun valid_accesses {intern, aliases} space name = let - fun accesses a = - let - val suppress = - (case lookup_entries space a of - SOME entry => entry_suppress entry - | NONE => []) - in - make_accesses {intern = intern} NONE suppress a - |> valid ? filter (is_valid_access space a) - end; - in if aliases then maps accesses (get_aliases space name) else accesses name end; + fun accesses (suppress, a) = + make_accesses {intern = intern} NONE suppress a + |> filter (is_valid_access space a); + in + if aliases then maps accesses (get_aliases space name) + else accesses (suppress_entry space name) + end; + fun gen_markup def space name = (case lookup_entries space name of @@ -264,7 +256,7 @@ val markup = gen_markup {def = false}; val markup_def = gen_markup {def = true}; -fun undefined (space as Name_Space {kind, entries, ...}) bad = +fun undefined_entry (space as Name_Space {kind, entries, ...}) bad = let val (prfx, sfx) = (case Long_Name.dest_hidden bad of @@ -275,13 +267,13 @@ | NONE => ("Undefined", quote bad)); in prfx ^ " " ^ plain_words kind ^ ": " ^ sfx end; -fun decl_names (Name_Space {entries, ...}) = - Change_Table.fold (fn (name, Decl _) => cons name | _ => I) entries []; - fun the_entry space name = (case lookup_entries space name of - SOME (Decl decl) => decl - | _ => error (undefined space name)); + SOME entry => entry + | _ => error (undefined_entry space name)); + +fun get_names (Name_Space {entries, ...}) = + Change_Table.fold (cons o #1) entries []; fun theory_name {long} space name = #theory_long_name (the_entry space name) @@ -328,15 +320,15 @@ else NONE end; - fun extern_name name = - get_first (extern_chunks names_unique name) - (get_accesses {intern = false, aliases = false, valid = false} space name); + 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 + (case get_first (uncurry extern_name) aliases of SOME xname => xname | NONE => - (case get_first (fn a => extern_chunks false a (Long_Name.make_chunks a)) aliases of + (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 @@ -413,7 +405,7 @@ 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 entry_serial (entry1, entry2)) then raise Change_Table.SAME + 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; @@ -537,9 +529,9 @@ let val _ = the_entry space name; val accesses = - get_accesses {intern = true, aliases = true, valid = true} space name + valid_accesses {intern = true, aliases = true} space name |> not fully ? inter Long_Name.eq_chunks [Long_Name.base_chunks name]; - val accesses' = get_accesses {intern = false, aliases = false, valid = true} space name; + val accesses' = valid_accesses {intern = false, aliases = false} space name; val internals' = internals |> fold (del_internals name) accesses |> fold (del_internals' name) accesses'; @@ -550,30 +542,16 @@ (* alias *) -fun alias naming strict binding name space = - let - val _ = the_entry space name; - val {restriction, suppress, full_name = alias_name, ...} = name_spec naming binding; - val alias_accesses = make_accesses {intern = true} restriction suppress alias_name; - val _ = alias_name = "" andalso error (Binding.bad binding); - val new_entry = is_none (lookup_entries space alias_name); - val decl_entry = can (the_entry space) alias_name; - in - space |> map_name_space (fn (kind, internals, internals_hidden, entries, aliases) => - let - val internals' = internals |> fold (add_internals name) alias_accesses; - val entries' = - if name <> alias_name andalso (new_entry orelse strict) then - entries |> update_entry strict kind (alias_name, - Alias { - suppress = suppress, - pos = #2 (Position.default (Binding.pos_of binding)), - serial = serial ()}) - else entries; - val aliases' = aliases - |> (not decl_entry) ? Symtab.update_list (op =) (name, alias_name); - in (kind, internals', internals_hidden, entries', aliases') end) - end; +fun alias naming binding name space = + space |> map_name_space (fn (kind, internals, internals_hidden, entries, aliases) => + let + val _ = the_entry space name; + 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); @@ -613,14 +591,13 @@ val accesses = make_accesses {intern = true} restriction suppress name; val (proper_pos, pos) = Position.default (Binding.pos_of binding); - val entry = - Decl { - concealed = #concealed name_spec, - suppress = suppress, - group = group, - theory_long_name = theory_long_name, - pos = pos, - serial = serial ()}; + 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, internals_hidden, entries, aliases) => let @@ -656,7 +633,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; @@ -674,7 +651,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 @@ -685,8 +662,8 @@ (* derived table operations *) -fun alias_table naming strict binding name (Table (space, tab)) = - Table (alias naming strict binding name space, tab); +fun alias_table naming binding name (Table (space, tab)) = + Table (alias naming binding name space, tab); fun hide_table fully name (Table (space, tab)) = Table (hide fully name space, tab); diff -r 14d133cff073 -r a12c48fbf10f src/Pure/Isar/entity.ML --- a/src/Pure/Isar/entity.ML Sat May 06 14:49:54 2023 +0200 +++ b/src/Pure/Isar/entity.ML Sat May 06 23:20:20 2023 +0200 @@ -39,7 +39,7 @@ let val naming = Name_Space.naming_of context; val binding' = Morphism.binding phi binding; - val data' = Name_Space.alias_table naming true binding' name (get_data context); + val data' = Name_Space.alias_table naming binding' name (get_data context); in put_data data' context end); fun transfer {get_data, put_data} ctxt = diff -r 14d133cff073 -r a12c48fbf10f src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Sat May 06 14:49:54 2023 +0200 +++ b/src/Pure/Isar/proof_context.ML Sat May 06 23:20:20 2023 +0200 @@ -1076,7 +1076,7 @@ end; -fun alias_fact b c ctxt = map_facts (Facts.alias (naming_of ctxt) false b c) ctxt; +fun alias_fact b c ctxt = map_facts (Facts.alias (naming_of ctxt) b c) ctxt; diff -r 14d133cff073 -r a12c48fbf10f src/Pure/Thy/export_theory.ML --- a/src/Pure/Thy/export_theory.ML Sat May 06 14:49:54 2023 +0200 +++ b/src/Pure/Thy/export_theory.ML Sat May 06 23:20:20 2023 +0200 @@ -463,7 +463,7 @@ let val space = get_space thy; val export_name = "other/" ^ Name_Space.kind_of space; - val decls = Name_Space.decl_names space |> map (rpair ()); + val decls = Name_Space.get_names space |> map (rpair ()); in export_entities export_name get_space decls (fn _ => fn () => SOME (K [])) end; val other_spaces = other_name_spaces thy; diff -r 14d133cff073 -r a12c48fbf10f src/Pure/consts.ML --- a/src/Pure/consts.ML Sat May 06 14:49:54 2023 +0200 +++ b/src/Pure/consts.ML Sat May 06 23:20:20 2023 +0200 @@ -140,7 +140,7 @@ fun space_of (Consts {decls, ...}) = Name_Space.space_of_table decls; fun alias naming binding name = map_consts (fn (decls, constraints, rev_abbrevs) => - ((Name_Space.alias_table naming true binding name decls), constraints, rev_abbrevs)); + ((Name_Space.alias_table naming binding name decls), constraints, rev_abbrevs)); val is_concealed = Name_Space.is_concealed o space_of; diff -r 14d133cff073 -r a12c48fbf10f src/Pure/facts.ML --- a/src/Pure/facts.ML Sat May 06 14:49:54 2023 +0200 +++ b/src/Pure/facts.ML Sat May 06 23:20:20 2023 +0200 @@ -24,7 +24,7 @@ type T val empty: T val space_of: T -> Name_Space.T - val alias: Name_Space.naming -> bool -> binding -> string -> T -> T + val alias: Name_Space.naming -> binding -> string -> T -> T val is_concealed: T -> string -> bool val check: Context.generic -> T -> xstring * Position.T -> string val intern: T -> xstring -> string @@ -155,8 +155,8 @@ val space_of = Name_Space.space_of_table o facts_of; -fun alias naming strict binding name (Facts {facts, props}) = - make_facts (Name_Space.alias_table naming strict binding name facts) props; +fun alias naming binding name (Facts {facts, props}) = + make_facts (Name_Space.alias_table naming binding name facts) props; val is_concealed = Name_Space.is_concealed o space_of; diff -r 14d133cff073 -r a12c48fbf10f src/Pure/global_theory.ML --- a/src/Pure/global_theory.ML Sat May 06 14:49:54 2023 +0200 +++ b/src/Pure/global_theory.ML Sat May 06 23:20:20 2023 +0200 @@ -79,7 +79,7 @@ val defined_fact = Facts.defined o facts_of; fun alias_fact binding name thy = - map_facts (Facts.alias (Sign.naming_of thy) true binding name) thy; + map_facts (Facts.alias (Sign.naming_of thy) binding name) thy; fun hide_fact fully name = map_facts (Facts.hide fully name); diff -r 14d133cff073 -r a12c48fbf10f src/Pure/type.ML --- a/src/Pure/type.ML Sat May 06 14:49:54 2023 +0200 +++ b/src/Pure/type.ML Sat May 06 23:20:20 2023 +0200 @@ -245,7 +245,7 @@ val type_space = Name_Space.space_of_table o #types o rep_tsig; fun type_alias naming binding name = map_tsig (fn (classes, default, types) => - (classes, default, (Name_Space.alias_table naming true binding name types))); + (classes, default, (Name_Space.alias_table naming binding name types))); fun undecl_type c = "Undeclared type constructor: " ^ quote c; diff -r 14d133cff073 -r a12c48fbf10f src/Pure/variable.ML --- a/src/Pure/variable.ML Sat May 06 14:49:54 2023 +0200 +++ b/src/Pure/variable.ML Sat May 06 23:20:20 2023 +0200 @@ -433,7 +433,7 @@ ctxt |> map_fixes (Name_Space.define context true (Binding.make (x', pos), (x, proper)) #> snd #> - x <> "" ? Name_Space.alias_table Name_Space.global_naming false (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;