src/Pure/General/name_space.ML
author haftmann
Tue Oct 20 16:13:01 2009 +0200 (2009-10-20)
changeset 33037 b22e44496dc2
parent 32738 15bb09ca0378
child 33038 8f9594c31de4
permissions -rw-r--r--
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
     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 BASIC_NAME_SPACE =
    11 sig
    12   val long_names: bool Unsynchronized.ref
    13   val short_names: bool Unsynchronized.ref
    14   val unique_names: bool Unsynchronized.ref
    15 end;
    16 
    17 signature NAME_SPACE =
    18 sig
    19   include BASIC_NAME_SPACE
    20   val hidden: string -> string
    21   val is_hidden: string -> bool
    22   type T
    23   val empty: T
    24   val intern: T -> xstring -> string
    25   val extern: T -> string -> xstring
    26   val extern_flags: {long_names: bool, short_names: bool, unique_names: bool} ->
    27     T -> string -> xstring
    28   val hide: bool -> string -> T -> T
    29   val merge: T * T -> T
    30   type naming
    31   val default_naming: naming
    32   val declare: naming -> binding -> T -> string * T
    33   val full_name: naming -> binding -> string
    34   val external_names: naming -> string -> string list
    35   val add_path: string -> naming -> naming
    36   val root_path: naming -> naming
    37   val parent_path: naming -> naming
    38   val mandatory_path: string -> naming -> naming
    39   type 'a table = T * 'a Symtab.table
    40   val define: naming -> binding * 'a -> 'a table -> string * 'a table (*exception Symtab.DUP*)
    41   val empty_table: 'a table
    42   val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table (*exception Symtab.DUP*)
    43   val join_tables: (string -> 'a * 'a -> 'a) (*exception Symtab.DUP/Symtab.SAME*) ->
    44     'a table * 'a table -> 'a table (*exception Symtab.DUP*)
    45   val dest_table: 'a table -> (string * 'a) list
    46   val extern_table: 'a table -> (xstring * 'a) list
    47 end;
    48 
    49 structure NameSpace: NAME_SPACE =
    50 struct
    51 
    52 
    53 (** name spaces **)
    54 
    55 (* hidden entries *)
    56 
    57 fun hidden name = "??." ^ name;
    58 val is_hidden = String.isPrefix "??.";
    59 
    60 
    61 (* datatype T *)
    62 
    63 datatype T =
    64   NameSpace of
    65     (string list * string list) Symtab.table *   (*internals, hidden internals*)
    66     xstring list Symtab.table;                   (*externals*)
    67 
    68 val empty = NameSpace (Symtab.empty, Symtab.empty);
    69 
    70 fun lookup (NameSpace (tab, _)) xname =
    71   (case Symtab.lookup tab xname of
    72     NONE => (xname, true)
    73   | SOME ([], []) => (xname, true)
    74   | SOME ([name], _) => (name, true)
    75   | SOME (name :: _, _) => (name, false)
    76   | SOME ([], name' :: _) => (hidden name', true));
    77 
    78 fun get_accesses (NameSpace (_, xtab)) name =
    79   (case Symtab.lookup xtab name of
    80     NONE => [name]
    81   | SOME xnames => xnames);
    82 
    83 fun put_accesses name xnames (NameSpace (tab, xtab)) =
    84   NameSpace (tab, Symtab.update (name, xnames) xtab);
    85 
    86 fun valid_accesses (NameSpace (tab, _)) name = Symtab.fold (fn (xname, (names, _)) =>
    87   if not (null names) andalso hd names = name then cons xname else I) tab [];
    88 
    89 
    90 (* intern and extern *)
    91 
    92 fun intern space xname = #1 (lookup space xname);
    93 
    94 fun extern_flags {long_names, short_names, unique_names} space name =
    95   let
    96     fun valid require_unique xname =
    97       let val (name', is_unique) = lookup space xname
    98       in name = name' andalso (not require_unique orelse is_unique) end;
    99 
   100     fun ext [] = if valid false name then name else hidden name
   101       | ext (nm :: nms) = if valid unique_names nm then nm else ext nms;
   102   in
   103     if long_names then name
   104     else if short_names then Long_Name.base_name name
   105     else ext (get_accesses space name)
   106   end;
   107 
   108 val long_names = Unsynchronized.ref false;
   109 val short_names = Unsynchronized.ref false;
   110 val unique_names = Unsynchronized.ref true;
   111 
   112 fun extern space name =
   113   extern_flags
   114    {long_names = ! long_names,
   115     short_names = ! short_names,
   116     unique_names = ! unique_names} space name;
   117 
   118 
   119 (* basic operations *)
   120 
   121 local
   122 
   123 fun map_space f xname (NameSpace (tab, xtab)) =
   124   NameSpace (Symtab.map_default (xname, ([], [])) f tab, xtab);
   125 
   126 in
   127 
   128 val del_name = map_space o apfst o remove (op =);
   129 fun del_name_extra name = map_space (apfst (fn [] => [] | x :: xs => x :: remove (op =) name xs));
   130 val add_name = map_space o apfst o update (op =);
   131 val add_name' = map_space o apsnd o update (op =);
   132 
   133 end;
   134 
   135 
   136 (* hide *)
   137 
   138 fun hide fully name space =
   139   if not (Long_Name.is_qualified name) then
   140     error ("Attempt to hide global name " ^ quote name)
   141   else if is_hidden name then
   142     error ("Attempt to hide hidden name " ^ quote name)
   143   else
   144     let val names = valid_accesses space name in
   145       space
   146       |> add_name' name name
   147       |> fold (del_name name)
   148         (if fully then names else gen_inter (op =) (names, [Long_Name.base_name name]))
   149       |> fold (del_name_extra name) (get_accesses space name)
   150     end;
   151 
   152 
   153 (* merge *)
   154 
   155 fun merge (NameSpace (tab1, xtab1), NameSpace (tab2, xtab2)) =
   156   let
   157     val tab' = (tab1, tab2) |> Symtab.join
   158       (K (fn ((names1, names1'), (names2, names2')) =>
   159         if pointer_eq (names1, names2) andalso pointer_eq (names1', names2') then raise Symtab.SAME
   160         else (Library.merge (op =) (names1, names2), Library.merge (op =) (names1', names2'))));
   161     val xtab' = (xtab1, xtab2) |> Symtab.join
   162       (K (fn xnames =>
   163         if pointer_eq xnames then raise Symtab.SAME
   164         else (Library.merge (op =) xnames)));
   165   in NameSpace (tab', xtab') end;
   166 
   167 
   168 
   169 (** naming contexts **)
   170 
   171 (* datatype naming *)
   172 
   173 datatype naming = Naming of (string * bool) list;
   174 fun map_naming f (Naming path) = Naming (f path);
   175 
   176 val default_naming = Naming [];
   177 
   178 fun add_path elems = map_naming (fn path => path @ [(elems, false)]);
   179 val root_path = map_naming (fn _ => []);
   180 val parent_path = map_naming (perhaps (try (#1 o split_last)));
   181 fun mandatory_path elems = map_naming (fn path => path @ [(elems, true)]);
   182 
   183 
   184 (* full name *)
   185 
   186 fun err_bad binding = error ("Bad name binding " ^ quote (Binding.str_of binding));
   187 
   188 fun name_spec (Naming path) binding =
   189   let
   190     val (prefix, name) = Binding.dest binding;
   191     val _ = Long_Name.is_qualified name andalso err_bad binding;
   192 
   193     val spec1 = maps (fn (a, b) => map (rpair b) (Long_Name.explode a)) (path @ prefix);
   194     val spec2 = if name = "" then [] else [(name, true)];
   195     val spec = spec1 @ spec2;
   196     val _ =
   197       exists (fn (a, _) => a = "" orelse a = "??" orelse exists_string (fn s => s = "\"") a) spec
   198       andalso err_bad binding;
   199   in if null spec2 then [] else spec end;
   200 
   201 fun full naming = name_spec naming #> map fst;
   202 fun full_name naming = full naming #> Long_Name.implode;
   203 
   204 
   205 (* accesses *)
   206 
   207 fun mandatory xs = map_filter (fn (x, true) => SOME x | _ => NONE) xs;
   208 
   209 fun mandatory_prefixes xs = mandatory xs :: mandatory_prefixes1 xs
   210 and mandatory_prefixes1 [] = []
   211   | mandatory_prefixes1 ((x, true) :: xs) = map (cons x) (mandatory_prefixes1 xs)
   212   | mandatory_prefixes1 ((x, false) :: xs) = map (cons x) (mandatory_prefixes xs);
   213 
   214 fun mandatory_suffixes xs = map rev (mandatory_prefixes (rev xs));
   215 
   216 fun accesses naming binding =
   217   let
   218     val spec = name_spec naming binding;
   219     val sfxs = mandatory_suffixes spec;
   220     val pfxs = mandatory_prefixes spec;
   221   in pairself (map Long_Name.implode) (sfxs @ pfxs, sfxs) end;
   222 
   223 fun external_names naming = #2 o accesses naming o Binding.qualified_name;
   224 
   225 
   226 (* declaration *)
   227 
   228 fun declare naming binding space =
   229   let
   230     val names = full naming binding;
   231     val name = Long_Name.implode names;
   232     val _ = name = "" andalso err_bad binding;
   233     val (accs, accs') = accesses naming binding;
   234     val space' = space |> fold (add_name name) accs |> put_accesses name accs';
   235   in (name, space') end;
   236 
   237 
   238 
   239 (** name spaces coupled with symbol tables **)
   240 
   241 type 'a table = T * 'a Symtab.table;
   242 
   243 fun define naming (binding, x) (space, tab) =
   244   let val (name, space') = declare naming binding space
   245   in (name, (space', Symtab.update_new (name, x) tab)) end;
   246 
   247 val empty_table = (empty, Symtab.empty);
   248 
   249 fun merge_tables eq ((space1, tab1), (space2, tab2)) =
   250   (merge (space1, space2), Symtab.merge eq (tab1, tab2));
   251 
   252 fun join_tables f ((space1, tab1), (space2, tab2)) =
   253   (merge (space1, space2), Symtab.join f (tab1, tab2));
   254 
   255 fun ext_table (space, tab) =
   256   Symtab.fold (fn (name, x) => cons ((name, extern space name), x)) tab []
   257   |> Library.sort_wrt (#2 o #1);
   258 
   259 fun dest_table tab = map (apfst #1) (ext_table tab);
   260 fun extern_table tab = map (apfst #2) (ext_table tab);
   261 
   262 end;
   263 
   264 structure Basic_Name_Space: BASIC_NAME_SPACE = NameSpace;
   265 open Basic_Name_Space;
   266