src/Pure/General/name_space.ML
author haftmann
Mon Dec 01 12:17:01 2008 +0100 (2008-12-01)
changeset 28923 0a981c596372
parent 28860 b1d46059d502
child 28941 128459bd72d2
permissions -rw-r--r--
exported get_accesses (for diagnostic purpose)
     1 (*  Title:      Pure/General/name_space.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Generic name spaces with declared and hidden entries.  Unknown names
     6 are considered global; no support for absolute addressing.
     7 *)
     8 
     9 type bstring = string;    (*names to be bound*)
    10 type xstring = string;    (*external names*)
    11 
    12 signature BASIC_NAME_SPACE =
    13 sig
    14   val long_names: bool ref
    15   val short_names: bool ref
    16   val unique_names: bool ref
    17 end;
    18 
    19 signature NAME_BINDING =
    20 sig
    21   type binding
    22   val binding_pos: string * Position.T -> binding
    23   val binding: string -> binding
    24   val no_binding: binding
    25   val dest_binding: binding -> (string * bool) list * string
    26   val is_nothing: binding -> bool
    27   val pos_of: binding -> Position.T
    28   val map_binding: ((string * bool) list * string -> (string * bool) list * string)
    29     -> binding -> binding
    30 end
    31 
    32 signature NAME_SPACE =
    33 sig
    34   include BASIC_NAME_SPACE
    35   val hidden: string -> string
    36   val is_hidden: string -> bool
    37   val separator: string                 (*single char*)
    38   val is_qualified: string -> bool
    39   val implode: string list -> string
    40   val explode: string -> string list
    41   val append: string -> string -> string
    42   val qualified: string -> string -> string
    43   val base: string -> string
    44   val qualifier: string -> string
    45   val map_base: (string -> string) -> string -> string
    46   type T
    47   val empty: T
    48   val intern: T -> xstring -> string
    49   val extern: T -> string -> xstring
    50   val hide: bool -> string -> T -> T
    51   val get_accesses: T -> string -> xstring list
    52   val merge: T * T -> T
    53   type naming
    54   val path_of: naming -> string
    55   val external_names: naming -> string -> string list
    56   val full: naming -> bstring -> string
    57   val declare: naming -> string -> T -> T
    58   val default_naming: naming
    59   val add_path: string -> naming -> naming
    60   val no_base_names: naming -> naming
    61   val qualified_names: naming -> naming
    62   val sticky_prefix: string -> naming -> naming
    63   include NAME_BINDING
    64   val full_binding: naming -> binding -> string
    65   val declare_binding: naming -> binding -> T -> string * T
    66   type 'a table = T * 'a Symtab.table
    67   val empty_table: 'a table
    68   val table_declare: naming -> binding * 'a
    69     -> 'a table -> string * 'a table (*exception Symtab.DUP*)
    70   val table_declare_permissive: naming -> binding * 'a
    71     -> 'a table -> string * 'a table
    72   val extend_table: naming -> (bstring * 'a) list -> 'a table -> 'a table
    73   val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table
    74   val dest_table: 'a table -> (string * 'a) list
    75   val extern_table: 'a table -> (xstring * 'a) list
    76 end;
    77 
    78 structure NameSpace: NAME_SPACE =
    79 struct
    80 
    81 (** long identifiers **)
    82 
    83 fun hidden name = "??." ^ name;
    84 val is_hidden = String.isPrefix "??."
    85 
    86 val separator = ".";
    87 val is_qualified = exists_string (fn s => s = separator);
    88 
    89 val implode_name = space_implode separator;
    90 val explode_name = space_explode separator;
    91 
    92 fun append name1 "" = name1
    93   | append "" name2 = name2
    94   | append name1 name2 = name1 ^ separator ^ name2;
    95 
    96 fun qualified path name =
    97   if path = "" orelse name = "" then name
    98   else path ^ separator ^ name;
    99 
   100 fun base "" = ""
   101   | base name = List.last (explode_name name);
   102 
   103 fun qualifier "" = ""
   104   | qualifier name = implode_name (#1 (split_last (explode_name name)));
   105 
   106 fun map_base _ "" = ""
   107   | map_base f name =
   108       let val names = explode_name name
   109       in implode_name (nth_map (length names - 1) f names) end;
   110 
   111 
   112 (* standard accesses *)
   113 
   114 infixr 6 @@;
   115 fun ([] @@ yss) = []
   116   | ((xs :: xss) @@ yss) = map (fn ys => xs @ ys) yss @ (xss @@ yss);
   117 
   118 fun suffixes_prefixes list =
   119   let
   120     val (xs, ws) = chop (length list - 1) list;
   121     val sfxs = suffixes xs @@ [ws];
   122     val pfxs = prefixes1 xs @@ [ws];
   123   in (sfxs @ pfxs, sfxs) end;
   124 
   125 fun suffixes_prefixes_split i k list =
   126   let
   127     val (((xs, ys), zs), ws) = list |> chop i ||>> chop k ||>> chop (length list - (i + k + 1));
   128     val sfxs =
   129       [ys] @@ suffixes zs @@ [ws] @
   130       suffixes1 xs @@ [ys @ zs @ ws];
   131     val pfxs =
   132       prefixes1 xs @@ [ys @ ws] @
   133       [xs @ ys] @@ prefixes1 zs @@ [ws];
   134   in (sfxs @ pfxs, sfxs) end;
   135 
   136 
   137 
   138 (** name spaces **)
   139 
   140 (* datatype T *)
   141 
   142 datatype T =
   143   NameSpace of
   144     ((string list * string list) * stamp) Symtab.table *   (*internals, hidden internals*)
   145     (string list * stamp) Symtab.table;                    (*externals*)
   146 
   147 val empty = NameSpace (Symtab.empty, Symtab.empty);
   148 
   149 fun lookup (NameSpace (tab, _)) xname =
   150   (case Symtab.lookup tab xname of
   151     NONE => (xname, true)
   152   | SOME (([], []), _) => (xname, true)
   153   | SOME (([name], _), _) => (name, true)
   154   | SOME ((name :: _, _), _) => (name, false)
   155   | SOME (([], name' :: _), _) => (hidden name', true));
   156 
   157 fun get_accesses (NameSpace (_, tab)) name =
   158   (case Symtab.lookup tab name of
   159     NONE => [name]
   160   | SOME (xnames, _) => xnames);
   161 
   162 fun put_accesses name xnames (NameSpace (tab, xtab)) =
   163   NameSpace (tab, Symtab.update (name, (xnames, stamp ())) xtab);
   164 
   165 fun valid_accesses (NameSpace (tab, _)) name = Symtab.fold (fn (xname, ((names, _), _)) =>
   166   if not (null names) andalso hd names = name then cons xname else I) tab [];
   167 
   168 
   169 (* intern and extern *)
   170 
   171 fun intern space xname = #1 (lookup space xname);
   172 
   173 val long_names = ref false;
   174 val short_names = ref false;
   175 val unique_names = ref true;
   176 
   177 fun extern space name =
   178   let
   179     fun valid unique xname =
   180       let val (name', uniq) = lookup space xname
   181       in name = name' andalso (uniq orelse not unique) end;
   182 
   183     fun ext [] = if valid false name then name else hidden name
   184       | ext (nm :: nms) = if valid (! unique_names) nm then nm else ext nms;
   185   in
   186     if ! long_names then name
   187     else if ! short_names then base name
   188     else ext (get_accesses space name)
   189   end;
   190 
   191 
   192 (* basic operations *)
   193 
   194 local
   195 
   196 fun map_space f xname (NameSpace (tab, xtab)) =
   197   NameSpace (Symtab.map_default (xname, (([], []), stamp ()))
   198     (fn (entry, _) => (f entry, stamp ())) tab, xtab);
   199 
   200 in
   201 
   202 val del_name = map_space o apfst o remove (op =);
   203 fun del_name_extra name = map_space (apfst (fn [] => [] | x :: xs => x :: remove (op =) name xs));
   204 val add_name = map_space o apfst o update (op =);
   205 val add_name' = map_space o apsnd o update (op =);
   206 
   207 end;
   208 
   209 
   210 (* hide *)
   211 
   212 fun hide fully name space =
   213   if not (is_qualified name) then
   214     error ("Attempt to hide global name " ^ quote name)
   215   else if is_hidden name then
   216     error ("Attempt to hide hidden name " ^ quote name)
   217   else
   218     let val names = valid_accesses space name in
   219       space
   220       |> add_name' name name
   221       |> fold (del_name name) (if fully then names else names inter_string [base name])
   222       |> fold (del_name_extra name) (get_accesses space name)
   223     end;
   224 
   225 
   226 (* merge *)
   227 
   228 fun merge (NameSpace (tab1, xtab1), NameSpace (tab2, xtab2)) =
   229   let
   230     val tab' = (tab1, tab2) |> Symtab.join
   231       (K (fn (((names1, names1'), stamp1), ((names2, names2'), stamp2)) =>
   232         if stamp1 = stamp2 then raise Symtab.SAME
   233         else
   234           ((Library.merge (op =) (names1, names2),
   235             Library.merge (op =) (names1', names2')), stamp ())));
   236     val xtab' = (xtab1, xtab2) |> Symtab.join
   237       (K (fn ((xnames1, stamp1), (xnames2, stamp2)) =>
   238         if stamp1 = stamp2 then raise Symtab.SAME
   239         else (Library.merge (op =) (xnames1, xnames2), stamp ())));
   240   in NameSpace (tab', xtab') end;
   241 
   242 
   243 
   244 (** generic name bindings **)
   245 
   246 datatype binding = Binding of ((string * bool) list * string) * Position.T;
   247 
   248 fun binding_pos (name, pos) = Binding (([], name), pos);
   249 fun binding name = binding_pos (name, Position.none);
   250 val no_binding = binding "";
   251 
   252 fun pos_of (Binding (_, pos)) = pos;
   253 fun dest_binding (Binding (prefix_name, _)) = prefix_name;
   254 
   255 fun map_binding f (Binding (prefix_name, pos)) = Binding (f prefix_name, pos);
   256 
   257 fun is_nothing (Binding ((_, name), _)) = name = "";
   258 
   259 
   260 
   261 (** naming contexts **)
   262 
   263 (* datatype naming *)
   264 
   265 datatype naming = Naming of
   266   string *                                                 (*path*)
   267   ((string -> string -> string) *                          (*qualify*)
   268    (string list -> string list list * string list list));  (*accesses*)
   269 
   270 fun path_of (Naming (path, _)) = path;
   271 fun accesses (Naming (_, (_, accs))) = accs;
   272 
   273 fun external_names naming = map implode_name o #2 o accesses naming o explode_name;
   274 
   275 
   276 (* manipulate namings *)
   277 
   278 fun reject_qualified name =
   279   if is_qualified name then
   280     error ("Attempt to declare qualified name " ^ quote name)
   281   else name;
   282 
   283 val default_naming =
   284   Naming ("", (fn path => qualified path o reject_qualified, suffixes_prefixes));
   285 
   286 fun add_path elems (Naming (path, policy)) =
   287   if elems = "//" then Naming ("", (qualified, #2 policy))
   288   else if elems = "/" then Naming ("", policy)
   289   else if elems = ".." then Naming (qualifier path, policy)
   290   else Naming (append path elems, policy);
   291 
   292 fun no_base_names (Naming (path, (qualify, accs))) =
   293   Naming (path, (qualify, pairself (filter_out (fn [_] => true | _ => false)) o accs));
   294 
   295 fun qualified_names (Naming (path, (_, accs))) = Naming (path, (qualified, accs));
   296 
   297 fun sticky_prefix prfx (Naming (path, (qualify, _))) =
   298   Naming (append path prfx,
   299     (qualify, suffixes_prefixes_split (length (explode_name path)) (length (explode_name prfx))));
   300 
   301 val apply_prefix =
   302   let
   303     fun mk_prefix (prfx, true) = sticky_prefix prfx
   304       | mk_prefix (prfx, false) = add_path prfx;
   305   in fold mk_prefix end;
   306 
   307 
   308 (* declarations *)
   309 
   310 fun full (Naming (path, (qualify, _))) = qualify path;
   311 
   312 fun declare naming name space =
   313   if is_hidden name then
   314     error ("Attempt to declare hidden name " ^ quote name)
   315   else
   316     let
   317       val names = explode_name name;
   318       val _ = (null names orelse exists (fn s => s = "") names
   319           orelse exists_string (fn s => s = "\"") name) andalso
   320         error ("Bad name declaration " ^ quote name);
   321       val (accs, accs') = pairself (map implode_name) (accesses naming names);
   322     in space |> fold (add_name name) accs |> put_accesses name accs' end;
   323 
   324 fun declare_binding bnaming (Binding ((prefix, bname), _)) =
   325   let
   326     val naming = apply_prefix prefix bnaming;
   327     val name = full naming bname;
   328   in declare naming name #> pair name end;
   329 
   330 
   331 
   332 (** name spaces coupled with symbol tables **)
   333 
   334 type 'a table = T * 'a Symtab.table;
   335 
   336 val empty_table = (empty, Symtab.empty);
   337 
   338 fun gen_table_declare update naming (binding, x) (space, tab) =
   339   let
   340     val (name, space') = declare_binding naming binding space;
   341   in (name, (space', update (name, x) tab)) end;
   342 
   343 fun table_declare naming = gen_table_declare Symtab.update_new naming;
   344 fun table_declare_permissive naming = gen_table_declare Symtab.update naming;
   345 
   346 fun full_binding naming (Binding ((prefix, bname), _)) =
   347   full (apply_prefix prefix naming) bname;
   348 
   349 fun extend_table naming bentries (space, tab) =
   350   let val entries = map (apfst (full naming)) bentries
   351   in (fold (declare naming o #1) entries space, Symtab.extend (tab, entries)) end;
   352 
   353 fun merge_tables eq ((space1, tab1), (space2, tab2)) =
   354   (merge (space1, space2), Symtab.merge eq (tab1, tab2));
   355 
   356 fun ext_table (space, tab) =
   357   Symtab.fold (fn (name, x) => cons ((name, extern space name), x)) tab []
   358   |> Library.sort_wrt (#2 o #1);
   359 
   360 fun dest_table tab = map (apfst #1) (ext_table tab);
   361 fun extern_table tab = map (apfst #2) (ext_table tab);
   362 
   363 
   364 (*final declarations of this structure!*)
   365 val implode = implode_name;
   366 val explode = explode_name;
   367 
   368 end;
   369 
   370 structure BasicNameSpace: BASIC_NAME_SPACE = NameSpace;
   371 open BasicNameSpace;