src/Pure/General/name_space.ML
author haftmann
Thu May 24 08:37:37 2007 +0200 (2007-05-24)
changeset 23086 12320f6e2523
parent 22057 d7c91b2f5a9e
child 23668 8b5a2a79a6e3
permissions -rw-r--r--
tuned Pure/General/name_space.ML
     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 implode: string list -> string
    26   val explode: 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 -> (bstring * 'a) list -> 'a table -> '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 implode_name = space_implode separator;
    74 val explode_name = 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 (explode_name name);
    86 
    87 fun qualifier "" = ""
    88   | qualifier name = implode_name (#1 (split_last (explode_name name)));
    89 
    90 fun map_base _ "" = ""
    91   | map_base f name =
    92       let val names = explode_name name
    93       in implode_name (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 implode_name o suffixes_prefixes o explode_name;
   121 val accesses' = map implode_name o Library.suffixes1 o explode_name;
   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   NameSpace (Symtab.map_default (xname, (([], []), stamp ()))
   173     (fn (entry, _) => (f entry, stamp ())) tab);
   174 
   175 fun del (name: string) = remove (op =) name;
   176 fun add name names = name :: del name names;
   177 
   178 val del_name = map_space o apfst o del;
   179 val add_name = map_space o apfst o add;
   180 val add_name' = map_space o apsnd o add;
   181 
   182 
   183 (* hide *)
   184 
   185 fun hide fully name space =
   186   if not (is_qualified name) then
   187     error ("Attempt to hide global name " ^ quote name)
   188   else if is_hidden name then
   189     error ("Attempt to hide hidden name " ^ quote name)
   190   else
   191     let val names = valid_accesses space name in
   192       space
   193       |> add_name' name name
   194       |> fold (del_name name) (if fully then names else names inter_string [base name])
   195     end;
   196 
   197 
   198 (* merge *)
   199 
   200 fun merge (NameSpace tab1, NameSpace tab2) =
   201   NameSpace ((tab1, tab2) |> Symtab.join
   202     (K (fn (((names1, names1'), stamp1), ((names2, names2'), stamp2)) =>
   203       if stamp1 = stamp2 then raise Symtab.SAME
   204       else
   205         ((Library.merge (op =) (names2, names1),
   206           Library.merge (op =) (names2', names1')), stamp ()))));
   207 
   208 
   209 
   210 (** naming contexts **)
   211 
   212 (* datatype naming *)
   213 
   214 datatype naming = Naming of
   215   string * ((string -> string -> string) * (string list -> string list list));
   216 
   217 fun path_of (Naming (path, _)) = path;
   218 
   219 
   220 (* declarations *)
   221 
   222 fun full (Naming (path, (qualify, _))) = qualify path;
   223 
   224 fun declare (Naming (_, (_, accs))) name space =
   225   if is_hidden name then
   226     error ("Attempt to declare hidden name " ^ quote name)
   227   else
   228     let
   229       val names = explode_name name;
   230       val _ = (null names orelse exists (fn s => s = "") names) andalso
   231         error ("Bad name declaration " ^ quote name);
   232     in fold (add_name name) (map implode_name (accs names)) space end;
   233 
   234 
   235 (* manipulate namings *)
   236 
   237 fun reject_qualified name =
   238   if is_qualified name then
   239     error ("Attempt to declare qualified name " ^ quote name)
   240   else name;
   241 
   242 val default_naming =
   243   Naming ("", (fn path => qualified path o reject_qualified, suffixes_prefixes));
   244 
   245 fun add_path elems (Naming (path, policy)) =
   246   if elems = "//" then Naming ("", (qualified, #2 policy))
   247   else if elems = "/" then Naming ("", policy)
   248   else if elems = ".." then Naming (qualifier path, policy)
   249   else Naming (append path elems, policy);
   250 
   251 fun no_base_names (Naming (path, (qualify, accs))) =
   252   Naming (path, (qualify, filter_out (fn [_] => true | _ => false) o accs));
   253 
   254 fun qualified_names (Naming (path, (_, accs))) = Naming (path, (qualified, accs));
   255 
   256 fun sticky_prefix prfx (Naming (path, (qualify, _))) =
   257   Naming (append path prfx,
   258     (qualify, suffixes_prefixes_split (length (explode_name path)) (length (explode_name prfx))));
   259 
   260 fun set_policy policy (Naming (path, _)) = Naming (path, policy);
   261 
   262 
   263 
   264 (** name spaces coupled with symbol tables **)
   265 
   266 type 'a table = T * 'a Symtab.table;
   267 
   268 val empty_table = (empty, Symtab.empty);
   269 
   270 fun extend_table naming bentries (space, tab) =
   271   let val entries = map (apfst (full naming)) bentries
   272   in (fold (declare naming o #1) entries space, Symtab.extend (tab, entries)) end;
   273 
   274 fun merge_tables eq ((space1, tab1), (space2, tab2)) =
   275   (merge (space1, space2), Symtab.merge eq (tab1, tab2));
   276 
   277 fun ext_table (space, tab) =
   278   Symtab.fold (fn (name, x) => cons ((name, extern space name), x)) tab []
   279   |> Library.sort_wrt (#2 o #1);
   280 
   281 fun dest_table tab = map (apfst #1) (ext_table tab);
   282 fun extern_table tab = map (apfst #2) (ext_table tab);
   283 
   284 
   285 (*final declarations of this structure!*)
   286 val implode = implode_name;
   287 val explode = explode_name;
   288 
   289 end;
   290 
   291 structure BasicNameSpace: BASIC_NAME_SPACE = NameSpace;
   292 open BasicNameSpace;