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