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