src/Pure/General/name_space.ML
author wenzelm
Sun Jun 05 11:31:25 2005 +0200 (2005-06-05)
changeset 16262 bd1b38f57fc7
parent 16137 00e9ca1e7261
child 16341 e573e5167eda
permissions -rw-r--r--
no warning for non-identifiers;
     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 as 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 drop_base: string -> string
    31   val map_base: (string -> string) -> string -> string
    32   val suffixes_prefixes: 'a list -> 'a list list
    33   val accesses: string -> string list
    34   val accesses': string -> string list
    35   type T
    36   val empty: T
    37   val valid_accesses: T -> string -> xstring list
    38   val intern: T -> xstring -> string
    39   val extern: T -> string -> xstring
    40   val extern_table: T -> 'a Symtab.table -> (xstring * 'a) list
    41   val hide: bool -> string -> T -> T
    42   val merge: T * T -> T
    43   val dest: T -> (string * xstring list) list
    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 qualified_names: naming -> naming
    51   val no_base_names: naming -> naming
    52   val custom_accesses: (string list -> string list list) -> naming -> naming
    53   val set_policy: (string -> bstring -> string) * (string list -> string list list) ->
    54     naming -> naming
    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 (equal separator);
    67 
    68 val pack = space_implode separator;
    69 val unpack = 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 (unpack name);
    81 
    82 fun drop_base "" = ""
    83   | drop_base name = pack (#1 (split_last (unpack name)));
    84 
    85 fun map_base _ "" = ""
    86   | map_base f name =
    87       let val names = unpack name
    88       in pack (map_nth_elem (length names - 1) f names) end;
    89 
    90 fun suffixes_prefixes xs =
    91   let
    92     val (qs, b) = split_last xs;
    93     val sfxs = Library.suffixes1 xs;
    94     val pfxs = map (fn x => x @ [b]) (Library.prefixes1 qs);
    95   in sfxs @ pfxs end;
    96 
    97 val accesses = map pack o suffixes_prefixes o unpack;
    98 val accesses' = map pack o Library.suffixes1 o unpack;
    99 
   100 
   101 
   102 (** name spaces **)
   103 
   104 (* datatype T *)
   105 
   106 datatype T =
   107   NameSpace of (string list * string list) Symtab.table;
   108 
   109 val empty = NameSpace Symtab.empty;
   110 
   111 fun lookup (NameSpace tab) xname =
   112   (case Symtab.lookup (tab, xname) of
   113     NONE => (xname, true)
   114   | SOME ([], []) => (xname, true)
   115   | SOME ([name], _) => (name, true)
   116   | SOME (name :: _, _) => (name, false)
   117   | SOME ([], name' :: _) => (hidden name', true));
   118 
   119 fun valid_accesses (NameSpace tab) name =
   120   ([], tab) |> Symtab.foldl (fn (accs, (xname, (names, _))) =>
   121     if null names orelse hd names <> name then accs else xname :: accs);
   122 
   123 
   124 (* intern and extern *)
   125 
   126 fun intern space xname = #1 (lookup space xname);
   127 
   128 val long_names = ref false;
   129 val short_names = ref false;
   130 val unique_names = ref true;
   131 
   132 fun extern space name =
   133   let
   134     fun valid unique xname =
   135       let val (name', uniq) = lookup space xname
   136       in name = name' andalso (uniq orelse (not unique)) end;
   137 
   138     fun ex [] = if valid false name then name else hidden name
   139       | ex (nm :: nms) = if valid (! unique_names) nm then nm else ex nms;
   140   in
   141     if ! long_names then name
   142     else if ! short_names then base name
   143     else ex (accesses' name)
   144   end;
   145 
   146 fun extern_table space tab =
   147   Library.sort_wrt #1 (map (apfst (extern space)) (Symtab.dest tab));
   148 
   149 
   150 (* basic operations *)
   151 
   152 fun map_space f xname (NameSpace tab) =
   153   NameSpace (Symtab.update ((xname, f (if_none (Symtab.lookup (tab, xname)) ([], []))), tab));
   154 
   155 fun del (name: string) = remove (op =) name;
   156 fun add name names = name :: del name names;
   157 
   158 val del_name = map_space o apfst o del;
   159 val add_name = map_space o apfst o add;
   160 val add_name' = map_space o apsnd o add;
   161 
   162 
   163 (* hide *)
   164 
   165 fun hide fully name space =
   166   if not (is_qualified name) then
   167     error ("Attempt to hide global name " ^ quote name)
   168   else if is_hidden name then
   169     error ("Attempt to hide hidden name " ^ quote name)
   170   else
   171     let val names = valid_accesses space name in
   172       space
   173       |> add_name' name name
   174       |> fold (del_name name) (if fully then names else names inter_string [base name])
   175     end;
   176 
   177 
   178 (* merge *)
   179 
   180 fun merge (NameSpace tab1, space2) = (space2, tab1) |> Symtab.foldl
   181   (fn (space, (xname, (names1, names1'))) =>
   182     map_space (fn (names2, names2') =>
   183       (merge_lists' names2 names1, merge_lists' names2' names1')) xname space);
   184 
   185 
   186 (* dest *)
   187 
   188 fun dest_entry (xname, ([], _)) = NONE
   189   | dest_entry (xname, (name :: _, _)) = SOME (name, xname);
   190 
   191 fun dest (NameSpace tab) =
   192   map (apsnd (sort (int_ord o pairself size)))
   193     (Symtab.dest (Symtab.make_multi (List.mapPartial dest_entry (Symtab.dest tab))));
   194 
   195 
   196 
   197 (** naming contexts **)
   198 
   199 (* datatype naming *)
   200 
   201 datatype naming = Naming of
   202   string * ((string -> string -> string) * (string list -> string list list));
   203 
   204 fun path_of (Naming (path, _)) = path;
   205 
   206 
   207 (* declarations *)
   208 
   209 fun full (Naming (path, (qualify, _))) = qualify path;
   210 
   211 fun declare (Naming (_, (_, accs))) name space =
   212   if is_hidden name then
   213     error ("Attempt to declare hidden name " ^ quote name)
   214   else
   215     let val names = unpack name in
   216       conditional (null names orelse exists (equal "") names) (fn () =>
   217         error ("Bad name declaration " ^ quote name));
   218       fold (add_name name) (map pack (accs names)) space
   219     end;
   220 
   221 
   222 (* manipulate namings *)
   223 
   224 fun reject_qualified name =
   225   if is_qualified name then
   226     error ("Attempt to declare qualified name " ^ quote name)
   227   else name;
   228 
   229 val default_naming =
   230   Naming ("", (fn path => qualified path o reject_qualified, suffixes_prefixes));
   231 
   232 fun add_path elems (Naming (path, policy)) =
   233   if elems = "//" then Naming ("", (qualified, #2 policy))
   234   else if elems = "/" then Naming ("", policy)
   235   else if elems = ".." then Naming (drop_base path, policy)
   236   else Naming (append path elems, policy);
   237 
   238 fun qualified_names (Naming (path, (_, accs))) = Naming (path, (qualified, accs));
   239 
   240 fun no_base_names (Naming (path, (qualify, accs))) =
   241   Naming (path, (qualify, filter_out (fn [_] => true | _ => false) o accs));
   242 
   243 fun custom_accesses accs (Naming (path, (qualify, _))) = Naming (path, (qualify, accs));
   244 fun set_policy policy (Naming (path, _)) = Naming (path, policy);
   245 
   246 
   247 end;
   248 
   249 structure BasicNameSpace: BASIC_NAME_SPACE = NameSpace;
   250 open BasicNameSpace;