# HG changeset patch
# User wenzelm
# Date 1683294972 -7200
# Node ID 31ea5c1f874d18cf7cee277b08faa98d5bd65539
# Parent  f68df517e8c4350b67e7c31fb70dbef6cfb29c7b
more explicit entries for aliases, with proper checks in "strict" mode (e.g. for logical entities);

diff -r f68df517e8c4 -r 31ea5c1f874d src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Fri May 05 12:34:23 2023 +0200
+++ b/src/Pure/General/name_space.ML	Fri May 05 15:56:12 2023 +0200
@@ -9,20 +9,19 @@
 
 signature NAME_SPACE =
 sig
-  type entry =
+  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 decl_names: T -> string list
+  val the_entry: T -> string ->
    {concealed: bool,
     suppress: bool list,
     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 theory_name: {long: bool} -> T -> string -> string
   val entry_ord: T -> string ord
   val is_concealed: T -> string -> bool
@@ -64,7 +63,7 @@
   val full_name: naming -> binding -> string
   val base_name: binding -> string
   val hide: bool -> string -> T -> T
-  val alias: naming -> binding -> string -> T -> T
+  val alias: naming -> bool -> binding -> string -> T -> T
   val naming_of: Context.generic -> naming
   val map_naming: (naming -> naming) -> Context.generic -> Context.generic
   val declared: T -> string -> bool
@@ -81,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 -> binding -> string -> 'a table -> 'a table
+  val alias_table: naming -> bool -> 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
@@ -107,7 +106,7 @@
 
 (* datatype entry *)
 
-type entry =
+type decl =
  {concealed: bool,
   suppress: bool list,
   group: serial,
@@ -115,19 +114,34 @@
   pos: Position.T,
   serial: serial};
 
-fun eq_entry_serial (entry1: entry, entry2: entry) : bool =
-  #serial entry1 = #serial entry2;
+type alias =
+  {decl: string,
+   suppress: bool list,
+   pos: Position.T,
+   serial: serial};
 
-fun entry_markup def kind (name, {pos, serial, ...}: entry) =
-  Position.make_entity_markup def serial kind (name, pos);
+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 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) 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;
+
 
 (* internal names *)
 
@@ -231,7 +245,7 @@
       let
         val suppress =
           (case lookup_entries space a of
-            SOME {suppress, ...} => suppress
+            SOME entry => entry_suppress entry
           | NONE => [])
       in
         make_accesses {intern = intern} NONE suppress a
@@ -242,7 +256,7 @@
 fun gen_markup def space name =
   (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};
@@ -258,13 +272,13 @@
       | NONE => ("Undefined", quote bad));
   in prfx ^ " " ^ plain_words kind ^ ": " ^ sfx end;
 
-fun get_names (Name_Space {entries, ...}) =
-  Change_Table.fold (cons o #1) entries [];
+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
-    NONE => error (undefined space name)
-  | SOME entry => entry);
+    SOME (Decl decl) => decl
+  | _ => error (undefined space name));
 
 fun theory_name {long} space name =
   #theory_long_name (the_entry space name)
@@ -392,8 +406,8 @@
         then raise Long_Name.Chunks.SAME
         else (Library.merge (op =) (names1, names2), Library.merge (op =) (names1', names2'))));
     val entries' = (entries1, entries2) |> Change_Table.join (fn name => fn (entry1, entry2) =>
-      if eq_entry_serial (entry1, entry2) then raise Change_Table.SAME
-      else err_dup kind' (name, entry1) (name, entry2) Position.none);
+      if op = (apply2 entry_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', entries', aliases') end;
 
@@ -528,16 +542,31 @@
 
 (* alias *)
 
-fun alias naming binding name space =
-  space |> map_name_space (fn (kind, internals, entries, aliases) =>
-    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 internals' = internals |> fold (add_name name) alias_accesses;
-      val aliases' = aliases |> Symtab.update_list (op =) (name, alias_name);
-    in (kind, internals', entries, aliases') end);
+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, entries, aliases) =>
+      let
+        val internals' = internals |> fold (add_name name) alias_accesses;
+        val entries' =
+          if name <> alias_name andalso (new_entry orelse strict) then
+            entries |> update_entry strict kind (alias_name,
+              Alias {
+                decl = name,
+                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', entries', aliases') end)
+  end;
 
 
 
@@ -578,24 +607,22 @@
 
     val (proper_pos, pos) = Position.default (Binding.pos_of binding);
     val entry =
-     {concealed = #concealed name_spec,
-      suppress = suppress,
-      group = group,
-      theory_long_name = theory_long_name,
-      pos = pos,
-      serial = serial ()};
+      Decl {
+        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, entries, aliases) =>
         let
           val internals' = internals |> fold (add_name name) accesses;
-          val entries' =
-            (if strict then Change_Table.update_new else Change_Table.update) (name, entry) entries
-            handle Change_Table.DUP dup =>
-              err_dup kind (dup, the (lookup_entries space dup)) (name, entry) (#pos entry);
+          val entries' = entries |> update_entry strict kind (name, entry);
         in (kind, internals', 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;
 
@@ -651,8 +678,8 @@
 
 (* derived table operations *)
 
-fun alias_table naming binding name (Table (space, tab)) =
-  Table (alias naming binding name space, tab);
+fun alias_table naming strict binding name (Table (space, tab)) =
+  Table (alias naming strict binding name space, tab);
 
 fun hide_table fully name (Table (space, tab)) =
   Table (hide fully name space, tab);
diff -r f68df517e8c4 -r 31ea5c1f874d src/Pure/Isar/entity.ML
--- a/src/Pure/Isar/entity.ML	Fri May 05 12:34:23 2023 +0200
+++ b/src/Pure/Isar/entity.ML	Fri May 05 15:56:12 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 binding' name (get_data context);
+      val data' = Name_Space.alias_table naming true binding' name (get_data context);
     in put_data data' context end);
 
 fun transfer {get_data, put_data} ctxt =
diff -r f68df517e8c4 -r 31ea5c1f874d src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Fri May 05 12:34:23 2023 +0200
+++ b/src/Pure/Isar/proof_context.ML	Fri May 05 15:56:12 2023 +0200
@@ -1076,7 +1076,7 @@
 
 end;
 
-fun alias_fact b c ctxt = map_facts (Facts.alias (naming_of ctxt) b c) ctxt;
+fun alias_fact b c ctxt = map_facts (Facts.alias (naming_of ctxt) false b c) ctxt;
 
 
 
diff -r f68df517e8c4 -r 31ea5c1f874d src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Fri May 05 12:34:23 2023 +0200
+++ b/src/Pure/Thy/export_theory.ML	Fri May 05 15:56:12 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.get_names space |> map (rpair ());
+        val decls = Name_Space.decl_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 f68df517e8c4 -r 31ea5c1f874d src/Pure/consts.ML
--- a/src/Pure/consts.ML	Fri May 05 12:34:23 2023 +0200
+++ b/src/Pure/consts.ML	Fri May 05 15:56:12 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 binding name decls), constraints, rev_abbrevs));
+  ((Name_Space.alias_table naming true binding name decls), constraints, rev_abbrevs));
 
 val is_concealed = Name_Space.is_concealed o space_of;
 
diff -r f68df517e8c4 -r 31ea5c1f874d src/Pure/facts.ML
--- a/src/Pure/facts.ML	Fri May 05 12:34:23 2023 +0200
+++ b/src/Pure/facts.ML	Fri May 05 15:56:12 2023 +0200
@@ -24,7 +24,7 @@
   type T
   val empty: T
   val space_of: T -> Name_Space.T
-  val alias: Name_Space.naming -> binding -> string -> T -> T
+  val alias: Name_Space.naming -> bool -> 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 binding name (Facts {facts, props}) =
-  make_facts (Name_Space.alias_table naming binding name facts) props;
+fun alias naming strict binding name (Facts {facts, props}) =
+  make_facts (Name_Space.alias_table naming strict binding name facts) props;
 
 val is_concealed = Name_Space.is_concealed o space_of;
 
diff -r f68df517e8c4 -r 31ea5c1f874d src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Fri May 05 12:34:23 2023 +0200
+++ b/src/Pure/global_theory.ML	Fri May 05 15:56:12 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) binding name) thy;
+  map_facts (Facts.alias (Sign.naming_of thy) true binding name) thy;
 
 fun hide_fact fully name = map_facts (Facts.hide fully name);
 
diff -r f68df517e8c4 -r 31ea5c1f874d src/Pure/type.ML
--- a/src/Pure/type.ML	Fri May 05 12:34:23 2023 +0200
+++ b/src/Pure/type.ML	Fri May 05 15:56:12 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 binding name types)));
+  (classes, default, (Name_Space.alias_table naming true binding name types)));
 
 
 fun undecl_type c = "Undeclared type constructor: " ^ quote c;
diff -r f68df517e8c4 -r 31ea5c1f874d src/Pure/variable.ML
--- a/src/Pure/variable.ML	Fri May 05 12:34:23 2023 +0200
+++ b/src/Pure/variable.ML	Fri May 05 15:56:12 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 (Binding.make (x, pos)) x')
+          x <> "" ? Name_Space.alias_table Name_Space.global_naming false (Binding.make (x, pos)) x')
       |> declare_fixed x
       |> declare_constraints (Syntax.free x')
   end;