src/Pure/General/name_space.ML
author wenzelm
Fri Nov 25 18:37:14 2011 +0100 (2011-11-25 ago)
changeset 45633 2cb7e34f6096
parent 45412 7797f5351ec4
child 45666 d83797ef0d2d
permissions -rw-r--r--
retain stderr and include it in syslog, which is buffered and thus increases the chance that users see remains from crashes etc.;
     1 (*  Title:      Pure/General/name_space.ML
     2     Author:     Markus Wenzel, TU Muenchen
     3 
     4 Generic name spaces with declared and hidden entries.  Unknown names
     5 are considered global; no support for absolute addressing.
     6 *)
     7 
     8 type xstring = string;    (*external names*)
     9 
    10 signature NAME_SPACE =
    11 sig
    12   val hidden: string -> string
    13   val is_hidden: string -> bool
    14   type T
    15   val empty: string -> T
    16   val kind_of: T -> string
    17   val the_entry: T -> string ->
    18     {concealed: bool, group: serial option, theory_name: string, pos: Position.T, id: serial}
    19   val entry_ord: T -> string * string -> order
    20   val markup: T -> string -> Markup.T
    21   val is_concealed: T -> string -> bool
    22   val intern: T -> xstring -> string
    23   val names_long_default: bool Unsynchronized.ref
    24   val names_long_raw: Config.raw
    25   val names_long: bool Config.T
    26   val names_short_default: bool Unsynchronized.ref
    27   val names_short_raw: Config.raw
    28   val names_short: bool Config.T
    29   val names_unique_default: bool Unsynchronized.ref
    30   val names_unique_raw: Config.raw
    31   val names_unique: bool Config.T
    32   val extern: Proof.context -> T -> string -> xstring
    33   val hide: bool -> string -> T -> T
    34   val merge: T * T -> T
    35   type naming
    36   val default_naming: naming
    37   val conceal: naming -> naming
    38   val get_group: naming -> serial option
    39   val set_group: serial option -> naming -> naming
    40   val set_theory_name: string -> naming -> naming
    41   val new_group: naming -> naming
    42   val reset_group: naming -> naming
    43   val add_path: string -> naming -> naming
    44   val root_path: naming -> naming
    45   val parent_path: naming -> naming
    46   val mandatory_path: string -> naming -> naming
    47   val qualified_path: bool -> binding -> naming -> naming
    48   val transform_binding: naming -> binding -> binding
    49   val full_name: naming -> binding -> string
    50   val declare: Proof.context -> bool -> naming -> binding -> T -> string * T
    51   val alias: naming -> binding -> string -> T -> T
    52   type 'a table = T * 'a Symtab.table
    53   val check: Proof.context -> 'a table -> xstring * Position.T -> string * 'a
    54   val get: 'a table -> string -> 'a
    55   val define: Proof.context -> bool -> naming -> binding * 'a -> 'a table -> string * 'a table
    56   val empty_table: string -> 'a table
    57   val merge_tables: 'a table * 'a table -> 'a table
    58   val join_tables: (string -> 'a * 'a -> 'a) (*Symtab.SAME*) ->
    59     'a table * 'a table -> 'a table
    60   val dest_table: Proof.context -> 'a table -> (string * 'a) list
    61   val extern_table: Proof.context -> 'a table -> (xstring * 'a) list
    62 end;
    63 
    64 structure Name_Space: NAME_SPACE =
    65 struct
    66 
    67 
    68 (** name spaces **)
    69 
    70 (* hidden entries *)
    71 
    72 fun hidden name = "??." ^ name;
    73 val is_hidden = String.isPrefix "??.";
    74 
    75 
    76 (* datatype entry *)
    77 
    78 type entry =
    79  {concealed: bool,
    80   group: serial option,
    81   theory_name: string,
    82   pos: Position.T,
    83   id: serial};
    84 
    85 fun entry_markup def kind (name, {pos, id, ...}: entry) =
    86   Markup.properties (Position.entity_properties_of def id pos) (Markup.entity kind name);
    87 
    88 fun print_entry def kind (name, entry) =
    89   quote (Markup.markup (entry_markup def kind (name, entry)) name);
    90 
    91 fun err_dup kind entry1 entry2 =
    92   error ("Duplicate " ^ kind ^ " declaration " ^
    93     print_entry true kind entry1 ^ " vs. " ^ print_entry true kind entry2);
    94 
    95 fun undefined kind name = "Undefined " ^ kind ^ ": " ^ quote name;
    96 
    97 
    98 (* datatype T *)
    99 
   100 datatype T =
   101   Name_Space of
   102    {kind: string,
   103     internals: (string list * string list) Symtab.table,  (*visible, hidden*)
   104     entries: (xstring list * entry) Symtab.table};        (*externals, entry*)
   105 
   106 fun make_name_space (kind, internals, entries) =
   107   Name_Space {kind = kind, internals = internals, entries = entries};
   108 
   109 fun map_name_space f (Name_Space {kind = kind, internals = internals, entries = entries}) =
   110   make_name_space (f (kind, internals, entries));
   111 
   112 fun map_internals f xname = map_name_space (fn (kind, internals, entries) =>
   113   (kind, Symtab.map_default (xname, ([], [])) f internals, entries));
   114 
   115 
   116 fun empty kind = make_name_space (kind, Symtab.empty, Symtab.empty);
   117 
   118 fun kind_of (Name_Space {kind, ...}) = kind;
   119 
   120 fun the_entry (Name_Space {kind, entries, ...}) name =
   121   (case Symtab.lookup entries name of
   122     NONE => error ("Unknown " ^ kind ^ " " ^ quote name)
   123   | SOME (_, entry) => entry);
   124 
   125 fun entry_ord space = int_ord o pairself (#id o the_entry space);
   126 
   127 fun markup (Name_Space {kind, entries, ...}) name =
   128   (case Symtab.lookup entries name of
   129     NONE => Markup.hilite
   130   | SOME (_, entry) => entry_markup false kind (name, entry));
   131 
   132 fun is_concealed space name = #concealed (the_entry space name);
   133 
   134 
   135 (* name accesses *)
   136 
   137 fun lookup (Name_Space {internals, ...}) xname =
   138   (case Symtab.lookup internals xname of
   139     NONE => (xname, true)
   140   | SOME ([], []) => (xname, true)
   141   | SOME ([name], _) => (name, true)
   142   | SOME (name :: _, _) => (name, false)
   143   | SOME ([], name' :: _) => (hidden name', true));
   144 
   145 fun get_accesses (Name_Space {entries, ...}) name =
   146   (case Symtab.lookup entries name of
   147     NONE => [name]
   148   | SOME (externals, _) => externals);
   149 
   150 fun valid_accesses (Name_Space {internals, ...}) name =
   151   Symtab.fold (fn (xname, (names, _)) =>
   152     if not (null names) andalso hd names = name then cons xname else I) internals [];
   153 
   154 
   155 (* intern and extern *)
   156 
   157 fun intern space xname = #1 (lookup space xname);
   158 
   159 
   160 val names_long_default = Unsynchronized.ref false;
   161 val names_long_raw = Config.declare "names_long" (fn _ => Config.Bool (! names_long_default));
   162 val names_long = Config.bool names_long_raw;
   163 
   164 val names_short_default = Unsynchronized.ref false;
   165 val names_short_raw = Config.declare "names_short" (fn _ => Config.Bool (! names_short_default));
   166 val names_short = Config.bool names_short_raw;
   167 
   168 val names_unique_default = Unsynchronized.ref true;
   169 val names_unique_raw = Config.declare "names_unique" (fn _ => Config.Bool (! names_unique_default));
   170 val names_unique = Config.bool names_unique_raw;
   171 
   172 fun extern ctxt space name =
   173   let
   174     val names_long = Config.get ctxt names_long;
   175     val names_short = Config.get ctxt names_short;
   176     val names_unique = Config.get ctxt names_unique;
   177 
   178     fun valid require_unique xname =
   179       let val (name', is_unique) = lookup space xname
   180       in name = name' andalso (not require_unique orelse is_unique) end;
   181 
   182     fun ext [] = if valid false name then name else hidden name
   183       | ext (nm :: nms) = if valid names_unique nm then nm else ext nms;
   184   in
   185     if names_long then name
   186     else if names_short then Long_Name.base_name name
   187     else ext (get_accesses space name)
   188   end;
   189 
   190 
   191 (* modify internals *)
   192 
   193 val del_name = map_internals o apfst o remove (op =);
   194 fun del_name_extra name =
   195   map_internals (apfst (fn [] => [] | x :: xs => x :: remove (op =) name xs));
   196 val add_name = map_internals o apfst o update (op =);
   197 val add_name' = map_internals o apsnd o update (op =);
   198 
   199 
   200 (* hide *)
   201 
   202 fun hide fully name space =
   203   if not (Long_Name.is_qualified name) then
   204     error ("Attempt to hide global name " ^ quote name)
   205   else if is_hidden name then
   206     error ("Attempt to hide hidden name " ^ quote name)
   207   else
   208     let val names = valid_accesses space name in
   209       space
   210       |> add_name' name name
   211       |> fold (del_name name)
   212         (if fully then names else inter (op =) [Long_Name.base_name name] names)
   213       |> fold (del_name_extra name) (get_accesses space name)
   214     end;
   215 
   216 
   217 (* merge *)
   218 
   219 fun merge
   220   (Name_Space {kind = kind1, internals = internals1, entries = entries1},
   221     Name_Space {kind = kind2, internals = internals2, entries = entries2}) =
   222   let
   223     val kind' =
   224       if kind1 = kind2 then kind1
   225       else error ("Attempt to merge different kinds of name spaces " ^
   226         quote kind1 ^ " vs. " ^ quote kind2);
   227     val internals' = (internals1, internals2) |> Symtab.join
   228       (K (fn ((names1, names1'), (names2, names2')) =>
   229         if pointer_eq (names1, names2) andalso pointer_eq (names1', names2')
   230         then raise Symtab.SAME
   231         else (Library.merge (op =) (names1, names2), Library.merge (op =) (names1', names2'))));
   232     val entries' = (entries1, entries2) |> Symtab.join
   233       (fn name => fn ((_, entry1), (_, entry2)) =>
   234         if #id entry1 = #id entry2 then raise Symtab.SAME
   235         else err_dup kind' (name, entry1) (name, entry2));
   236   in make_name_space (kind', internals', entries') end;
   237 
   238 
   239 
   240 (** naming contexts **)
   241 
   242 (* datatype naming *)
   243 
   244 datatype naming = Naming of
   245  {conceal: bool,
   246   group: serial option,
   247   theory_name: string,
   248   path: (string * bool) list};
   249 
   250 fun make_naming (conceal, group, theory_name, path) =
   251   Naming {conceal = conceal, group = group, theory_name = theory_name, path = path};
   252 
   253 fun map_naming f (Naming {conceal, group, theory_name, path}) =
   254   make_naming (f (conceal, group, theory_name, path));
   255 
   256 fun map_path f = map_naming (fn (conceal, group, theory_name, path) =>
   257   (conceal, group, theory_name, f path));
   258 
   259 
   260 val default_naming = make_naming (false, NONE, "", []);
   261 
   262 val conceal = map_naming (fn (_, group, theory_name, path) =>
   263   (true, group, theory_name, path));
   264 
   265 fun set_theory_name theory_name = map_naming (fn (conceal, group, _, path) =>
   266   (conceal, group, theory_name, path));
   267 
   268 
   269 fun get_group (Naming {group, ...}) = group;
   270 
   271 fun set_group group = map_naming (fn (conceal, _, theory_name, path) =>
   272   (conceal, group, theory_name, path));
   273 
   274 fun new_group naming = set_group (SOME (serial ())) naming;
   275 val reset_group = set_group NONE;
   276 
   277 fun add_path elems = map_path (fn path => path @ [(elems, false)]);
   278 val root_path = map_path (fn _ => []);
   279 val parent_path = map_path (perhaps (try (#1 o split_last)));
   280 fun mandatory_path elems = map_path (fn path => path @ [(elems, true)]);
   281 
   282 fun qualified_path mandatory binding = map_path (fn path =>
   283   path @ #2 (Binding.dest (Binding.qualified mandatory "" binding)));
   284 
   285 
   286 (* full name *)
   287 
   288 fun err_bad binding = error (Binding.bad binding);
   289 
   290 fun transform_binding (Naming {conceal = true, ...}) = Binding.conceal
   291   | transform_binding _ = I;
   292 
   293 fun name_spec (naming as Naming {path, ...}) raw_binding =
   294   let
   295     val binding = transform_binding naming raw_binding;
   296     val (concealed, prefix, name) = Binding.dest binding;
   297     val _ = Long_Name.is_qualified name andalso err_bad binding;
   298 
   299     val spec1 = maps (fn (a, b) => map (rpair b) (Long_Name.explode a)) (path @ prefix);
   300     val spec2 = if name = "" then [] else [(name, true)];
   301     val spec = spec1 @ spec2;
   302     val _ =
   303       exists (fn (a, _) => a = "" orelse a = "??" orelse exists_string (fn s => s = "\"") a) spec
   304       andalso err_bad binding;
   305   in (concealed, if null spec2 then [] else spec) end;
   306 
   307 fun full_name naming =
   308   name_spec naming #> #2 #> map #1 #> Long_Name.implode;
   309 
   310 
   311 (* accesses *)
   312 
   313 fun mandatory xs = map_filter (fn (x, true) => SOME x | _ => NONE) xs;
   314 
   315 fun mandatory_prefixes xs = mandatory xs :: mandatory_prefixes1 xs
   316 and mandatory_prefixes1 [] = []
   317   | mandatory_prefixes1 ((x, true) :: xs) = map (cons x) (mandatory_prefixes1 xs)
   318   | mandatory_prefixes1 ((x, false) :: xs) = map (cons x) (mandatory_prefixes xs);
   319 
   320 fun mandatory_suffixes xs = map rev (mandatory_prefixes (rev xs));
   321 
   322 fun accesses naming binding =
   323   let
   324     val spec = #2 (name_spec naming binding);
   325     val sfxs = mandatory_suffixes spec;
   326     val pfxs = mandatory_prefixes spec;
   327   in pairself (map Long_Name.implode) (sfxs @ pfxs, sfxs) end;
   328 
   329 
   330 (* declaration *)
   331 
   332 fun new_entry strict (name, (externals, entry)) =
   333   map_name_space (fn (kind, internals, entries) =>
   334     let
   335       val entries' =
   336         (if strict then Symtab.update_new else Symtab.update) (name, (externals, entry)) entries
   337           handle Symtab.DUP dup =>
   338             err_dup kind (dup, #2 (the (Symtab.lookup entries dup))) (name, entry);
   339     in (kind, internals, entries') end);
   340 
   341 fun declare ctxt strict naming binding space =
   342   let
   343     val Naming {group, theory_name, ...} = naming;
   344     val (concealed, spec) = name_spec naming binding;
   345     val (accs, accs') = accesses naming binding;
   346 
   347     val name = Long_Name.implode (map fst spec);
   348     val _ = name = "" andalso err_bad binding;
   349 
   350     val pos = Position.default (Binding.pos_of binding);
   351     val entry =
   352      {concealed = concealed,
   353       group = group,
   354       theory_name = theory_name,
   355       pos = pos,
   356       id = serial ()};
   357     val space' = space
   358       |> fold (add_name name) accs
   359       |> new_entry strict (name, (accs', entry));
   360     val _ = Context_Position.report ctxt pos (entry_markup true (kind_of space) (name, entry));
   361   in (name, space') end;
   362 
   363 
   364 (* alias *)
   365 
   366 fun alias naming binding name space =
   367   let
   368     val (accs, accs') = accesses naming binding;
   369     val space' = space
   370       |> fold (add_name name) accs
   371       |> map_name_space (fn (kind, internals, entries) =>
   372         let
   373           val _ = Symtab.defined entries name orelse error (undefined kind name);
   374           val entries' = entries
   375             |> Symtab.map_entry name (fn (externals, entry) =>
   376               (Library.merge (op =) (externals, accs'), entry))
   377         in (kind, internals, entries') end);
   378   in space' end;
   379 
   380 
   381 
   382 (** name space coupled with symbol table **)
   383 
   384 type 'a table = T * 'a Symtab.table;
   385 
   386 fun check ctxt (space, tab) (xname, pos) =
   387   let val name = intern space xname in
   388     (case Symtab.lookup tab name of
   389       SOME x => (Context_Position.report ctxt pos (markup space name); (name, x))
   390     | NONE => error (undefined (kind_of space) name ^ Position.str_of pos))
   391   end;
   392 
   393 fun get (space, tab) name =
   394   (case Symtab.lookup tab name of
   395     SOME x => x
   396   | NONE => error (undefined (kind_of space) name));
   397 
   398 fun define ctxt strict naming (binding, x) (space, tab) =
   399   let val (name, space') = declare ctxt strict naming binding space
   400   in (name, (space', Symtab.update (name, x) tab)) end;
   401 
   402 fun empty_table kind = (empty kind, Symtab.empty);
   403 
   404 fun merge_tables ((space1, tab1), (space2, tab2)) =
   405   (merge (space1, space2), Symtab.merge (K true) (tab1, tab2));
   406 
   407 fun join_tables f ((space1, tab1), (space2, tab2)) =
   408   (merge (space1, space2), Symtab.join f (tab1, tab2));
   409 
   410 fun ext_table ctxt (space, tab) =
   411   Symtab.fold (fn (name, x) => cons ((name, extern ctxt space name), x)) tab []
   412   |> Library.sort_wrt (#2 o #1);
   413 
   414 fun dest_table ctxt tab = map (apfst #1) (ext_table ctxt tab);
   415 fun extern_table ctxt tab = map (apfst #2) (ext_table ctxt tab);
   416 
   417 end;
   418