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