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