maintain explicit name space kind;
authorwenzelm
Sat Oct 24 20:54:08 2009 +0200 (2009-10-24 ago)
changeset 33096db3c18fd9708
parent 33095 bbd52d2f8696
child 33097 9d501e11084a
maintain explicit name space kind;
export Name_Space.the_entry;
tuned messages;
src/Pure/General/name_space.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/method.ML
src/Pure/consts.ML
src/Pure/facts.ML
src/Pure/simplifier.ML
src/Pure/theory.ML
src/Pure/thm.ML
src/Pure/type.ML
     1.1 --- a/src/Pure/General/name_space.ML	Sat Oct 24 19:47:37 2009 +0200
     1.2 +++ b/src/Pure/General/name_space.ML	Sat Oct 24 20:54:08 2009 +0200
     1.3 @@ -20,7 +20,9 @@
     1.4    val hidden: string -> string
     1.5    val is_hidden: string -> bool
     1.6    type T
     1.7 -  val empty: T
     1.8 +  val empty: string -> T
     1.9 +  val kind_of: T -> string
    1.10 +  val the_entry: T -> string -> {is_system: bool, pos: Position.T, id: serial}
    1.11    val intern: T -> xstring -> string
    1.12    val extern: T -> string -> xstring
    1.13    val extern_flags: {long_names: bool, short_names: bool, unique_names: bool} ->
    1.14 @@ -38,7 +40,7 @@
    1.15    val mandatory_path: string -> naming -> naming
    1.16    type 'a table = T * 'a Symtab.table
    1.17    val define: bool -> naming -> binding * 'a -> 'a table -> string * 'a table
    1.18 -  val empty_table: 'a table
    1.19 +  val empty_table: string -> 'a table
    1.20    val merge_tables: 'a table * 'a table -> 'a table
    1.21    val join_tables:
    1.22      (string -> 'a * 'a -> 'a) (*Symtab.SAME*) -> 'a table * 'a table -> 'a table
    1.23 @@ -66,41 +68,63 @@
    1.24    pos: Position.T,
    1.25    id: serial};
    1.26  
    1.27 -fun make_entry (externals, is_system, pos, id) : entry =
    1.28 -  {externals = externals, is_system = is_system, pos = pos, id = id};
    1.29 -
    1.30  fun str_of_entry def (name, {pos, id, ...}: entry) =
    1.31    let
    1.32      val occurrence = (if def then Markup.defN else Markup.refN, string_of_int id);
    1.33      val props = occurrence :: Position.properties_of pos;
    1.34    in Markup.markup (Markup.properties props (Markup.entity name)) name end;
    1.35  
    1.36 +fun err_dup kind entry1 entry2 =
    1.37 +  error ("Duplicate " ^ kind ^ " declaration " ^
    1.38 +    quote (str_of_entry true entry1) ^ " vs. " ^ quote (str_of_entry true entry2));
    1.39 +
    1.40  
    1.41  (* datatype T *)
    1.42  
    1.43  datatype T =
    1.44    Name_Space of
    1.45 -    (string list * string list) Symtab.table *   (*internals, hidden internals*)
    1.46 -    entry Symtab.table;
    1.47 +   {kind: string,
    1.48 +    internals: (string list * string list) Symtab.table,  (*visible, hidden*)
    1.49 +    entries: entry Symtab.table};
    1.50 +
    1.51 +fun make_name_space (kind, internals, entries) =
    1.52 +  Name_Space {kind = kind, internals = internals, entries = entries};
    1.53 +
    1.54 +fun map_name_space f (Name_Space {kind = kind, internals = internals, entries = entries}) =
    1.55 +  make_name_space (f (kind, internals, entries));
    1.56 +
    1.57 +fun map_internals f xname = map_name_space (fn (kind, internals, entries) =>
    1.58 +  (kind, Symtab.map_default (xname, ([], [])) f internals, entries));
    1.59 +
    1.60  
    1.61 -val empty = Name_Space (Symtab.empty, Symtab.empty);
    1.62 +fun empty kind = make_name_space (kind, Symtab.empty, Symtab.empty);
    1.63 +
    1.64 +fun kind_of (Name_Space {kind, ...}) = kind;
    1.65  
    1.66 -fun lookup (Name_Space (tab, _)) xname =
    1.67 -  (case Symtab.lookup tab xname of
    1.68 +fun the_entry (Name_Space {kind, entries, ...}) name =
    1.69 +  (case Symtab.lookup entries name of
    1.70 +    NONE => error ("Unknown " ^ kind ^ " " ^ quote name)
    1.71 +  | SOME {is_system, pos, id, ...} => {is_system = is_system, pos = pos, id = id});
    1.72 +
    1.73 +
    1.74 +(* name accesses *)
    1.75 +
    1.76 +fun lookup (Name_Space {internals, ...}) xname =
    1.77 +  (case Symtab.lookup internals xname of
    1.78      NONE => (xname, true)
    1.79    | SOME ([], []) => (xname, true)
    1.80    | SOME ([name], _) => (name, true)
    1.81    | SOME (name :: _, _) => (name, false)
    1.82    | SOME ([], name' :: _) => (hidden name', true));
    1.83  
    1.84 -fun get_accesses (Name_Space (_, entries)) name =
    1.85 +fun get_accesses (Name_Space {entries, ...}) name =
    1.86    (case Symtab.lookup entries name of
    1.87      NONE => [name]
    1.88    | SOME {externals, ...} => externals);
    1.89  
    1.90 -fun valid_accesses (Name_Space (tab, _)) name =
    1.91 +fun valid_accesses (Name_Space {internals, ...}) name =
    1.92    Symtab.fold (fn (xname, (names, _)) =>
    1.93 -    if not (null names) andalso hd names = name then cons xname else I) tab [];
    1.94 +    if not (null names) andalso hd names = name then cons xname else I) internals [];
    1.95  
    1.96  
    1.97  (* intern and extern *)
    1.98 @@ -132,21 +156,13 @@
    1.99      unique_names = ! unique_names} space name;
   1.100  
   1.101  
   1.102 -(* basic operations *)
   1.103 -
   1.104 -local
   1.105 -
   1.106 -fun map_space f xname (Name_Space (tab, entries)) =
   1.107 -  Name_Space (Symtab.map_default (xname, ([], [])) f tab, entries);
   1.108 +(* modify internals *)
   1.109  
   1.110 -in
   1.111 -
   1.112 -val del_name = map_space o apfst o remove (op =);
   1.113 -fun del_name_extra name = map_space (apfst (fn [] => [] | x :: xs => x :: remove (op =) name xs));
   1.114 -val add_name = map_space o apfst o update (op =);
   1.115 -val add_name' = map_space o apsnd o update (op =);
   1.116 -
   1.117 -end;
   1.118 +val del_name = map_internals o apfst o remove (op =);
   1.119 +fun del_name_extra name =
   1.120 +  map_internals (apfst (fn [] => [] | x :: xs => x :: remove (op =) name xs));
   1.121 +val add_name = map_internals o apfst o update (op =);
   1.122 +val add_name' = map_internals o apsnd o update (op =);
   1.123  
   1.124  
   1.125  (* hide *)
   1.126 @@ -168,9 +184,15 @@
   1.127  
   1.128  (* merge *)
   1.129  
   1.130 -fun merge (Name_Space (tab1, entries1), Name_Space (tab2, entries2)) =
   1.131 +fun merge
   1.132 +  (Name_Space {kind = kind1, internals = internals1, entries = entries1},
   1.133 +    Name_Space {kind = kind2, internals = internals2, entries = entries2}) =
   1.134    let
   1.135 -    val tab' = (tab1, tab2) |> Symtab.join
   1.136 +    val kind' =
   1.137 +      if kind1 = kind2 then kind1
   1.138 +      else error ("Attempt to merge different kinds of name spaces " ^
   1.139 +        quote kind1 ^ " vs. " ^ quote kind2);
   1.140 +    val internals' = (internals1, internals2) |> Symtab.join
   1.141        (K (fn ((names1, names1'), (names2, names2')) =>
   1.142          if pointer_eq (names1, names2) andalso pointer_eq (names1', names2')
   1.143          then raise Symtab.SAME
   1.144 @@ -178,11 +200,8 @@
   1.145      val entries' = (entries1, entries2) |> Symtab.join
   1.146        (fn name => fn (entry1, entry2) =>
   1.147          if #id entry1 = #id entry2 then raise Symtab.SAME
   1.148 -        else
   1.149 -          error ("Duplicate declaration " ^
   1.150 -            quote (str_of_entry true (name, entry1)) ^ " vs. " ^
   1.151 -            quote (str_of_entry true (name, entry2))));
   1.152 -  in Name_Space (tab', entries') end;
   1.153 +        else err_dup kind' (name, entry1) (name, entry2));
   1.154 +  in make_name_space (kind', internals', entries') end;
   1.155  
   1.156  
   1.157  
   1.158 @@ -245,13 +264,14 @@
   1.159  
   1.160  (* declaration *)
   1.161  
   1.162 -fun new_entry strict entry (Name_Space (tab, entries)) =
   1.163 -  let
   1.164 -    val entries' =
   1.165 -      (if strict then Symtab.update_new else Symtab.update) entry entries
   1.166 -        handle Symtab.DUP _ =>
   1.167 -          error ("Duplicate declaration " ^ quote (str_of_entry true entry));
   1.168 -  in Name_Space (tab, entries') end;
   1.169 +fun new_entry strict entry =
   1.170 +  map_name_space (fn (kind, internals, entries) =>
   1.171 +    let
   1.172 +      val entries' =
   1.173 +        (if strict then Symtab.update_new else Symtab.update) entry entries
   1.174 +          handle Symtab.DUP dup =>
   1.175 +            err_dup kind (dup, the (Symtab.lookup entries dup)) entry;
   1.176 +    in (kind, internals, entries') end);
   1.177  
   1.178  fun declare strict naming binding space =
   1.179    let
   1.180 @@ -259,12 +279,12 @@
   1.181      val name = Long_Name.implode names;
   1.182      val _ = name = "" andalso err_bad binding;
   1.183      val (accs, accs') = accesses naming binding;
   1.184 -
   1.185 -    val is_system = false;  (* FIXME *)
   1.186 -    val entry = make_entry (accs', is_system, Binding.pos_of binding, serial ());
   1.187 -    val space' = space
   1.188 -      |> fold (add_name name) accs
   1.189 -      |> new_entry strict (name, entry);
   1.190 +    val entry =
   1.191 +     {externals = accs',
   1.192 +      is_system = false,
   1.193 +      pos = Binding.pos_of binding,
   1.194 +      id = serial ()};
   1.195 +    val space' = space |> fold (add_name name) accs |> new_entry strict (name, entry);
   1.196    in (name, space') end;
   1.197  
   1.198  
   1.199 @@ -277,7 +297,7 @@
   1.200    let val (name, space') = declare strict naming binding space
   1.201    in (name, (space', Symtab.update (name, x) tab)) end;
   1.202  
   1.203 -val empty_table = (empty, Symtab.empty);
   1.204 +fun empty_table kind = (empty kind, Symtab.empty);
   1.205  
   1.206  fun merge_tables ((space1, tab1), (space2, tab2)) =
   1.207    (merge (space1, space2), Symtab.merge (K true) (tab1, tab2));
     2.1 --- a/src/Pure/Isar/attrib.ML	Sat Oct 24 19:47:37 2009 +0200
     2.2 +++ b/src/Pure/Isar/attrib.ML	Sat Oct 24 20:54:08 2009 +0200
     2.3 @@ -68,7 +68,7 @@
     2.4  structure Attributes = TheoryDataFun
     2.5  (
     2.6    type T = ((src -> attribute) * string) Name_Space.table;
     2.7 -  val empty = Name_Space.empty_table;
     2.8 +  val empty = Name_Space.empty_table "attribute";
     2.9    val copy = I;
    2.10    val extend = I;
    2.11    fun merge _ tables : T = Name_Space.merge_tables tables;
     3.1 --- a/src/Pure/Isar/locale.ML	Sat Oct 24 19:47:37 2009 +0200
     3.2 +++ b/src/Pure/Isar/locale.ML	Sat Oct 24 20:54:08 2009 +0200
     3.3 @@ -125,7 +125,7 @@
     3.4  structure Locales = TheoryDataFun
     3.5  (
     3.6    type T = locale Name_Space.table;
     3.7 -  val empty = Name_Space.empty_table;
     3.8 +  val empty = Name_Space.empty_table "locale";
     3.9    val copy = I;
    3.10    val extend = I;
    3.11    fun merge _ = Name_Space.join_tables (K merge_locale);
     4.1 --- a/src/Pure/Isar/method.ML	Sat Oct 24 19:47:37 2009 +0200
     4.2 +++ b/src/Pure/Isar/method.ML	Sat Oct 24 20:54:08 2009 +0200
     4.3 @@ -323,7 +323,7 @@
     4.4  structure Methods = TheoryDataFun
     4.5  (
     4.6    type T = ((src -> Proof.context -> method) * string) Name_Space.table;
     4.7 -  val empty = Name_Space.empty_table;
     4.8 +  val empty = Name_Space.empty_table "method";
     4.9    val copy = I;
    4.10    val extend = I;
    4.11    fun merge _ tables : T = Name_Space.merge_tables tables;
     5.1 --- a/src/Pure/consts.ML	Sat Oct 24 19:47:37 2009 +0200
     5.2 +++ b/src/Pure/consts.ML	Sat Oct 24 20:54:08 2009 +0200
     5.3 @@ -29,7 +29,7 @@
     5.4    val certify: Pretty.pp -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
     5.5    val typargs: T -> string * typ -> typ list
     5.6    val instance: T -> string * typ list -> typ
     5.7 -  val declare: bool -> Name_Space.naming -> Properties.T -> (binding * typ) -> T -> T
     5.8 +  val declare: bool -> Name_Space.naming -> Properties.T -> binding * typ -> T -> T
     5.9    val constrain: string * typ option -> T -> T
    5.10    val abbreviate: Pretty.pp -> Type.tsig -> Name_Space.naming -> string -> Properties.T ->
    5.11      binding * term -> T -> (term * term) * T
    5.12 @@ -307,7 +307,7 @@
    5.13  
    5.14  (* empty and merge *)
    5.15  
    5.16 -val empty = make_consts (Name_Space.empty_table, Symtab.empty, Symtab.empty);
    5.17 +val empty = make_consts (Name_Space.empty_table "constant", Symtab.empty, Symtab.empty);
    5.18  
    5.19  fun merge
    5.20     (Consts {decls = decls1, constraints = constraints1, rev_abbrevs = rev_abbrevs1},
     6.1 --- a/src/Pure/facts.ML	Sat Oct 24 19:47:37 2009 +0200
     6.2 +++ b/src/Pure/facts.ML	Sat Oct 24 20:54:08 2009 +0200
     6.3 @@ -126,7 +126,7 @@
     6.4    props: thm Net.net};
     6.5  
     6.6  fun make_facts facts props = Facts {facts = facts, props = props};
     6.7 -val empty = make_facts Name_Space.empty_table Net.empty;
     6.8 +val empty = make_facts (Name_Space.empty_table "fact") Net.empty;
     6.9  
    6.10  
    6.11  (* named facts *)
     7.1 --- a/src/Pure/simplifier.ML	Sat Oct 24 19:47:37 2009 +0200
     7.2 +++ b/src/Pure/simplifier.ML	Sat Oct 24 20:54:08 2009 +0200
     7.3 @@ -148,7 +148,7 @@
     7.4  structure Simprocs = GenericDataFun
     7.5  (
     7.6    type T = simproc Name_Space.table;
     7.7 -  val empty = Name_Space.empty_table;
     7.8 +  val empty = Name_Space.empty_table "simproc";
     7.9    val extend = I;
    7.10    fun merge _ simprocs = Name_Space.merge_tables simprocs;
    7.11  );
     8.1 --- a/src/Pure/theory.ML	Sat Oct 24 19:47:37 2009 +0200
     8.2 +++ b/src/Pure/theory.ML	Sat Oct 24 20:54:08 2009 +0200
     8.3 @@ -89,18 +89,18 @@
     8.4  structure ThyData = TheoryDataFun
     8.5  (
     8.6    type T = thy;
     8.7 -  val empty = make_thy (Name_Space.empty_table, Defs.empty, ([], []));
     8.8 +  val empty_axioms = Name_Space.empty_table "axiom";
     8.9 +  val empty = make_thy (empty_axioms, Defs.empty, ([], []));
    8.10    val copy = I;
    8.11  
    8.12 -  fun extend (Thy {axioms = _, defs, wrappers}) =
    8.13 -    make_thy (Name_Space.empty_table, defs, wrappers);
    8.14 +  fun extend (Thy {axioms = _, defs, wrappers}) = make_thy (empty_axioms, defs, wrappers);
    8.15  
    8.16    fun merge pp (thy1, thy2) =
    8.17      let
    8.18        val Thy {axioms = _, defs = defs1, wrappers = (bgs1, ens1)} = thy1;
    8.19        val Thy {axioms = _, defs = defs2, wrappers = (bgs2, ens2)} = thy2;
    8.20  
    8.21 -      val axioms' = Name_Space.empty_table;
    8.22 +      val axioms' = empty_axioms;
    8.23        val defs' = Defs.merge pp (defs1, defs2);
    8.24        val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2);
    8.25        val ens' = Library.merge (eq_snd op =) (ens1, ens2);
     9.1 --- a/src/Pure/thm.ML	Sat Oct 24 19:47:37 2009 +0200
     9.2 +++ b/src/Pure/thm.ML	Sat Oct 24 20:54:08 2009 +0200
     9.3 @@ -1727,7 +1727,7 @@
     9.4  structure Oracles = TheoryDataFun
     9.5  (
     9.6    type T = unit Name_Space.table;
     9.7 -  val empty = Name_Space.empty_table;
     9.8 +  val empty = Name_Space.empty_table "oracle";
     9.9    val copy = I;
    9.10    val extend = I;
    9.11    fun merge _ oracles : T = Name_Space.merge_tables oracles;
    10.1 --- a/src/Pure/type.ML	Sat Oct 24 19:47:37 2009 +0200
    10.2 +++ b/src/Pure/type.ML	Sat Oct 24 20:54:08 2009 +0200
    10.3 @@ -120,7 +120,7 @@
    10.4    build_tsig (f (classes, default, types));
    10.5  
    10.6  val empty_tsig =
    10.7 -  build_tsig ((Name_Space.empty, Sorts.empty_algebra), [], Name_Space.empty_table);
    10.8 +  build_tsig ((Name_Space.empty "class", Sorts.empty_algebra), [], Name_Space.empty_table "type");
    10.9  
   10.10  
   10.11  (* classes and sorts *)