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