src/Pure/General/name_space.ML
author wenzelm
Tue Mar 10 16:51:08 2009 +0100 (2009-03-10)
changeset 30412 7f5b0a020ccd
parent 30359 3f9b3ff851ca
child 30418 b5044aca0729
permissions -rw-r--r--
just one naming policy based on binding content -- eliminated odd "object-oriented" style;
uniform handling of regular vs. mandatory name prefixes -- add_path and sticky_prefix may be freely intermixed;
misc tuning and cleanup;
     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 ref
    13   val short_names: bool ref
    14   val unique_names: bool 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 no_base_names: naming -> naming
    37   val qualified_names: naming -> naming
    38   val sticky_prefix: string -> naming -> naming
    39   type 'a table = T * 'a Symtab.table
    40   val bind: 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 = ref false;
   109 val short_names = ref false;
   110 val unique_names = 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 names inter_string [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 names as ((names1, names1'), (names2, names2')) =>
   159         if pointer_eq names 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
   174  {path: (string * bool) list,
   175   no_base_names: bool,
   176   qualified_names: bool};
   177 
   178 fun make_naming (path, no_base_names, qualified_names) =
   179   Naming {path = path, no_base_names = no_base_names, qualified_names = qualified_names};
   180 
   181 fun map_naming f (Naming {path, no_base_names, qualified_names}) =
   182   make_naming (f (path, no_base_names, qualified_names));
   183 
   184 fun path_of (Naming {path, ...}) = path;
   185 
   186 
   187 (* configure naming *)
   188 
   189 val default_naming = make_naming ([], false, false);
   190 
   191 fun add_path elems = map_naming (fn (path, no_base_names, qualified_names) =>
   192   if elems = "//" then ([], no_base_names, true)
   193   else if elems = "/" then ([], no_base_names, qualified_names)
   194   else if elems = ".." then (perhaps (try (#1 o split_last)) path, no_base_names, qualified_names)
   195   else (path @ map (rpair false) (Long_Name.explode elems), no_base_names, qualified_names));
   196 
   197 fun sticky_prefix elems = map_naming (fn (path, no_base_names, qualified_names) =>
   198   (path @ map (rpair true) (Long_Name.explode elems), no_base_names, qualified_names));
   199 
   200 val no_base_names = map_naming (fn (path, _, qualified_names) => (path, true, qualified_names));
   201 val qualified_names = map_naming (fn (path, no_base_names, _) => (path, no_base_names, true));
   202 
   203 
   204 (* full name *)
   205 
   206 fun err_bad binding = error ("Bad name declaration " ^ quote (Binding.str_of binding));
   207 
   208 fun name_spec (Naming {path, qualified_names, ...}) binding =
   209   let
   210     val (prefix, name) = Binding.dest binding;
   211     val _ = not qualified_names andalso Long_Name.is_qualified name andalso err_bad binding;
   212 
   213     val spec1 = maps (fn (a, b) => map (rpair b) (Long_Name.explode a)) (path @ prefix);
   214     val spec2 =
   215       (case try split_last (Long_Name.explode name) of
   216         NONE => []
   217       | SOME (qual, base) => map (rpair false) qual @ [(base, true)]);
   218 
   219     val spec = spec1 @ spec2;
   220     val _ =
   221       exists (fn (a, _) => a = "" orelse a = "??" orelse exists_string (fn s => s = "\"") a) spec
   222       andalso err_bad binding;
   223   in if null spec2 then [] else spec end;
   224 
   225 fun full naming = name_spec naming #> map fst;
   226 fun full_name naming = full naming #> Long_Name.implode;
   227 
   228 
   229 (* accesses *)
   230 
   231 fun mandatory xs = map_filter (fn (x, true) => SOME x | _ => NONE) xs;
   232 
   233 fun mandatory_prefixes xs = mandatory xs :: mandatory_prefixes1 xs
   234 and mandatory_prefixes1 [] = []
   235   | mandatory_prefixes1 ((x, true) :: xs) = map (cons x) (mandatory_prefixes1 xs)
   236   | mandatory_prefixes1 ((x, false) :: xs) = map (cons x) (mandatory_prefixes xs);
   237 
   238 fun mandatory_suffixes1 xs = map rev (mandatory_prefixes1 (rev xs));
   239 fun mandatory_suffixes xs = map rev (mandatory_prefixes (rev xs));
   240 
   241 fun accesses (naming as Naming {no_base_names, ...}) binding =
   242   let
   243     val spec = name_spec naming binding;
   244     val sfxs = mandatory_suffixes spec;
   245     val pfxs = mandatory_prefixes spec;
   246   in
   247     (sfxs @ pfxs, sfxs)
   248     |> pairself (no_base_names ? filter (fn [_] => false | _ => true))
   249     |> pairself (map Long_Name.implode)
   250   end;
   251 
   252 fun external_names naming = #2 o accesses naming o Binding.qualified_name;
   253 
   254 
   255 (* declaration *)
   256 
   257 fun declare naming binding space =
   258   let
   259     val names = full naming binding;
   260     val name = Long_Name.implode names;
   261     val _ = name = "" andalso err_bad binding;
   262     val (accs, accs') = accesses naming binding;
   263     val space' = space |> fold (add_name name) accs |> put_accesses name accs';
   264   in (name, space') end;
   265 
   266 
   267 
   268 (** name spaces coupled with symbol tables **)
   269 
   270 type 'a table = T * 'a Symtab.table;
   271 
   272 fun bind naming (binding, x) (space, tab) =
   273   let val (name, space') = declare naming binding space
   274   in (name, (space', Symtab.update_new (name, x) tab)) end;
   275 
   276 val empty_table = (empty, Symtab.empty);
   277 
   278 fun merge_tables eq ((space1, tab1), (space2, tab2)) =
   279   (merge (space1, space2), Symtab.merge eq (tab1, tab2));
   280 
   281 fun join_tables f ((space1, tab1), (space2, tab2)) =
   282   (merge (space1, space2), Symtab.join f (tab1, tab2));
   283 
   284 fun ext_table (space, tab) =
   285   Symtab.fold (fn (name, x) => cons ((name, extern space name), x)) tab []
   286   |> Library.sort_wrt (#2 o #1);
   287 
   288 fun dest_table tab = map (apfst #1) (ext_table tab);
   289 fun extern_table tab = map (apfst #2) (ext_table tab);
   290 
   291 end;
   292 
   293 structure BasicNameSpace: BASIC_NAME_SPACE = NameSpace;
   294 open BasicNameSpace;
   295