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