src/Pure/General/name_space.ML
author haftmann
Fri Oct 28 16:35:40 2005 +0200 (2005-10-28)
changeset 18011 685d95c793ff
parent 17756 d4a35f82fbb4
child 18939 18e2a2676d80
permissions -rw-r--r--
cleaned up nth, nth_update, nth_map and nth_string functions
     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 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 hide: bool -> string -> T -> T
    41   val merge: T * T -> T
    42   type naming
    43   val path_of: naming -> string
    44   val full: naming -> bstring -> string
    45   val declare: naming -> string -> T -> T
    46   val default_naming: naming
    47   val add_path: string -> naming -> naming
    48   val qualified_names: naming -> naming
    49   val no_base_names: naming -> naming
    50   val custom_accesses: (string list -> string list list) -> naming -> naming
    51   val set_policy: (string -> bstring -> string) * (string list -> string list list) ->
    52     naming -> naming
    53   type 'a table (*= T * 'a Symtab.table*)
    54   val empty_table: 'a table
    55   val extend_table: naming -> 'a table * (bstring * 'a) list -> 'a table
    56   val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table
    57   val dest_table: 'a table -> (string * 'a) list
    58   val extern_table: 'a table -> (xstring * 'a) list
    59 end;
    60 
    61 structure NameSpace: NAME_SPACE =
    62 struct
    63 
    64 (** long identifiers **)
    65 
    66 fun hidden name = "??." ^ name;
    67 val is_hidden = String.isPrefix "??."
    68 
    69 val separator = ".";
    70 val is_qualified = exists_string (equal separator);
    71 
    72 val pack = space_implode separator;
    73 val unpack = space_explode separator;
    74 
    75 fun append name1 "" = name1
    76   | append "" name2 = name2
    77   | append name1 name2 = name1 ^ separator ^ name2;
    78 
    79 fun qualified path name =
    80   if path = "" orelse name = "" then name
    81   else path ^ separator ^ name;
    82 
    83 fun base "" = ""
    84   | base name = List.last (unpack name);
    85 
    86 fun drop_base "" = ""
    87   | drop_base name = pack (#1 (split_last (unpack name)));
    88 
    89 fun map_base _ "" = ""
    90   | map_base f name =
    91       let val names = unpack name
    92       in pack (nth_map (length names - 1) f names) end;
    93 
    94 fun suffixes_prefixes xs =
    95   let
    96     val (qs, b) = split_last xs;
    97     val sfxs = Library.suffixes1 xs;
    98     val pfxs = map (fn x => x @ [b]) (Library.prefixes1 qs);
    99   in sfxs @ pfxs end;
   100 
   101 val accesses = map pack o suffixes_prefixes o unpack;
   102 val accesses' = map pack o Library.suffixes1 o unpack;
   103 
   104 
   105 
   106 (** name spaces **)
   107 
   108 (* datatype T *)
   109 
   110 datatype T =
   111   NameSpace of (string list * string list) Symtab.table;
   112 
   113 val empty = NameSpace Symtab.empty;
   114 
   115 fun lookup (NameSpace tab) xname =
   116   (case Symtab.lookup tab xname of
   117     NONE => (xname, true)
   118   | SOME ([], []) => (xname, true)
   119   | SOME ([name], _) => (name, true)
   120   | SOME (name :: _, _) => (name, false)
   121   | SOME ([], name' :: _) => (hidden name', true));
   122 
   123 fun valid_accesses (NameSpace tab) name = Symtab.fold (fn (xname, (names, _)) =>
   124   if not (null names) andalso hd names = name then cons xname else I) tab [];
   125 
   126 
   127 (* intern and extern *)
   128 
   129 fun intern space xname = #1 (lookup space xname);
   130 
   131 val long_names = ref false;
   132 val short_names = ref false;
   133 val unique_names = ref true;
   134 
   135 fun extern space name =
   136   let
   137     fun valid unique xname =
   138       let val (name', uniq) = lookup space xname
   139       in name = name' andalso (uniq orelse (not unique)) end;
   140 
   141     fun ex [] = if valid false name then name else hidden name
   142       | ex (nm :: nms) = if valid (! unique_names) nm then nm else ex nms;
   143   in
   144     if ! long_names then name
   145     else if ! short_names then base name
   146     else ex (accesses' name)
   147   end;
   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) = Symtab.fold (fn (xname, (names1, names1')) =>
   181   xname |> map_space (fn (names2, names2') =>
   182     (merge_lists' names2 names1, merge_lists' names2' names1'))) tab1 space2;
   183 
   184 
   185 
   186 (** naming contexts **)
   187 
   188 (* datatype naming *)
   189 
   190 datatype naming = Naming of
   191   string * ((string -> string -> string) * (string list -> string list list));
   192 
   193 fun path_of (Naming (path, _)) = path;
   194 
   195 
   196 (* declarations *)
   197 
   198 fun full (Naming (path, (qualify, _))) = qualify path;
   199 
   200 fun declare (Naming (_, (_, accs))) name space =
   201   if is_hidden name then
   202     error ("Attempt to declare hidden name " ^ quote name)
   203   else
   204     let val names = unpack name in
   205       conditional (null names orelse exists (equal "") names) (fn () =>
   206         error ("Bad name declaration " ^ quote name));
   207       fold (add_name name) (map pack (accs names)) space
   208     end;
   209 
   210 
   211 (* manipulate namings *)
   212 
   213 fun reject_qualified name =
   214   if is_qualified name then
   215     error ("Attempt to declare qualified name " ^ quote name)
   216   else name;
   217 
   218 val default_naming =
   219   Naming ("", (fn path => qualified path o reject_qualified, suffixes_prefixes));
   220 
   221 fun add_path elems (Naming (path, policy)) =
   222   if elems = "//" then Naming ("", (qualified, #2 policy))
   223   else if elems = "/" then Naming ("", policy)
   224   else if elems = ".." then Naming (drop_base path, policy)
   225   else Naming (append path elems, policy);
   226 
   227 fun qualified_names (Naming (path, (_, accs))) = Naming (path, (qualified, accs));
   228 
   229 fun no_base_names (Naming (path, (qualify, accs))) =
   230   Naming (path, (qualify, filter_out (fn [_] => true | _ => false) o accs));
   231 
   232 fun custom_accesses accs (Naming (path, (qualify, _))) = Naming (path, (qualify, accs));
   233 fun set_policy policy (Naming (path, _)) = Naming (path, policy);
   234 
   235 
   236 
   237 (** name spaces coupled with symbol tables **)
   238 
   239 type 'a table = T * 'a Symtab.table;
   240 
   241 val empty_table = (empty, Symtab.empty);
   242 
   243 fun extend_table naming ((space, tab), bentries) =
   244   let val entries = map (apfst (full naming)) bentries
   245   in (fold (declare naming o #1) entries space, Symtab.extend (tab, entries)) end;
   246 
   247 fun merge_tables eq ((space1, tab1), (space2, tab2)) =
   248   (merge (space1, space2), (Symtab.merge eq (tab1, tab2)));
   249 
   250 fun ext_table (space, tab) =
   251   Symtab.fold (fn (name, x) => cons ((name, extern space name), x)) tab []
   252   |> Library.sort_wrt (#2 o #1);
   253 
   254 fun dest_table tab = map (apfst #1) (ext_table tab);
   255 fun extern_table tab = map (apfst #2) (ext_table tab);
   256 
   257 end;
   258 
   259 structure BasicNameSpace: BASIC_NAME_SPACE = NameSpace;
   260 open BasicNameSpace;