src/Pure/General/name_space.ML
author wenzelm
Wed May 18 11:30:59 2005 +0200 (2005-05-18)
changeset 16002 e0557c452138
parent 15624 484178635bd8
child 16137 00e9ca1e7261
permissions -rw-r--r--
tuned;
     1 (*  Title:      Pure/General/name_space.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Hierarchically structured name spaces.
     6 
     7 More general than ML-like nested structures, but also slightly more
     8 ad-hoc.  Does not support absolute addressing.  Unknown names are
     9 implicitely considered to be declared outermost.
    10 *)
    11 
    12 signature NAME_SPACE =
    13 sig
    14   val separator: string                 (*single char*)
    15   val hidden: string -> string
    16   val append: string -> string -> string
    17   val unpack: string -> string list
    18   val pack: string list -> string
    19   val base: string -> string
    20   val map_base: (string -> string) -> string -> string
    21   val is_qualified: string -> bool
    22   val accesses: string -> string list
    23   val accesses': string -> string list
    24   type T
    25   val empty: T
    26   val extend: T * string list -> T
    27   val extend': (string -> string list) -> T * string list -> T
    28   val merge: T * T -> T
    29   val hide: bool -> T * string list -> T
    30   val intern: T -> string -> string
    31   val extern: T -> string -> string
    32   val long_names: bool ref
    33   val short_names: bool ref
    34   val unique_names: bool ref
    35   val cond_extern: T -> string -> string
    36   val cond_extern_table: T -> 'a Symtab.table -> (string * 'a) list
    37   val dest: T -> (string * string list) list
    38 end;
    39 
    40 structure NameSpace: NAME_SPACE =
    41 struct
    42 
    43 (** long identifiers **)
    44 
    45 val separator = ".";
    46 fun hidden name = "??." ^ name;
    47 fun is_hidden name = (case explode name of "?" :: "?" :: "." :: _ => true | _ => false);
    48 
    49 fun append name1 name2 = name1 ^ separator ^ name2;
    50 
    51 val unpack = space_explode separator;
    52 val pack = space_implode separator;
    53 
    54 val base = List.last o unpack;
    55 
    56 fun map_base f name =
    57   let val uname = unpack name
    58   in pack (map_nth_elem (length uname - 1) f uname) end;
    59 
    60 fun is_qualified name = length (unpack name) > 1;
    61 
    62 fun accesses name =
    63   let
    64     val uname = unpack name;
    65     val (q, b) = split_last uname;
    66     val sfxs = Library.suffixes1 uname;
    67     val pfxs = map (fn x => x @ [b]) (Library.prefixes1 q);
    68   in map pack (sfxs @ pfxs) end;
    69 
    70 val accesses' = map pack o Library.suffixes1 o unpack;
    71 
    72 
    73 
    74 (** name spaces **)
    75 
    76 (* basic operations *)
    77 
    78 fun map_space f xname tab =
    79   Symtab.update ((xname, f (if_none (Symtab.lookup (tab, xname)) ([], []))), tab);
    80 
    81 fun change f xname (name, tab) =
    82   map_space (fn (names, names') => (f names name, names')) xname tab;
    83 
    84 fun change' f xname (name', tab) =
    85   map_space (fn (names, names') => (names, f names' name')) xname tab;
    86 
    87 fun del names nm = if nm mem_string names then Library.gen_rem (op =) (names, nm) else names;
    88 fun add names nm = nm :: del names nm;
    89 
    90 
    91 (* datatype T *)
    92 
    93 datatype T =
    94   NameSpace of (string list * string list) Symtab.table;
    95 
    96 val empty = NameSpace Symtab.empty;
    97 
    98 
    99 (* extend *)            (*later entries preferred*)
   100 
   101 fun gen_extend_aux acc (name, tab) =
   102   if is_hidden name then
   103     error ("Attempt to declare hidden name " ^ quote name)
   104   else Library.foldl (fn (tb, xname) => change add xname (name, tb)) (tab, acc name);
   105 
   106 fun extend' acc (NameSpace tab, names) =
   107   NameSpace (foldr (gen_extend_aux acc) tab names);
   108 fun extend (NameSpace tab, names) =
   109   NameSpace (foldr (gen_extend_aux accesses) tab names);
   110 
   111 
   112 (* merge *)             (*1st preferred over 2nd*)
   113 
   114 fun merge_aux (tab, (xname, (names1, names1'))) =
   115   map_space (fn (names2, names2') =>
   116     (merge_lists' names2 names1, merge_lists' names2' names1')) xname tab;
   117 
   118 fun merge (NameSpace tab1, NameSpace tab2) =
   119   NameSpace (Symtab.foldl merge_aux (tab2, tab1));
   120 
   121 
   122 (* hide *)
   123 
   124 fun hide_aux fully (name, tab) =
   125   if not (is_qualified name) then
   126     error ("Attempt to hide global name " ^ quote name)
   127   else if is_hidden name then
   128     error ("Attempt to hide hidden name " ^ quote name)
   129   else (change' add name (name,
   130     Library.foldl (fn (tb, xname) => change del xname (name, tb))
   131       (tab, if fully then accesses name else [base name])));
   132 
   133 fun hide fully (NameSpace tab, names) = NameSpace (foldr (hide_aux fully) tab names);
   134 
   135 
   136 (* intern / extern names *)
   137 
   138 fun lookup (NameSpace tab) xname =
   139   (case Symtab.lookup (tab, xname) of
   140     NONE => (xname, true)
   141   | SOME ([name], _) => (name, true)
   142   | SOME (name :: _, _) => (name, false)
   143   | SOME ([], []) => (xname, true)
   144   | SOME ([], name' :: _) => (hidden name', true));
   145 
   146 fun intern spc xname = #1 (lookup spc xname);
   147 
   148 fun unique_extern mkunique space name =
   149   let
   150     fun try [] = hidden name
   151       | try (nm :: nms) =
   152           let val (full_nm, uniq) = lookup space nm
   153           in if full_nm = name andalso (uniq orelse (not mkunique)) then nm else try nms end
   154   in try (accesses' name) end;
   155 
   156 (*output unique names by default*)
   157 val unique_names = ref true;
   158 
   159 (*prune names on output by default*)
   160 val long_names = ref false;
   161 
   162 (*output only base name*)
   163 val short_names = ref false;
   164 
   165 fun extern space name = unique_extern (!unique_names) space name; 
   166 
   167 fun cond_extern space =
   168   if ! long_names then I
   169   else if ! short_names then base else extern space;
   170 
   171 fun cond_extern_table space tab =
   172   Library.sort_wrt #1 (map (apfst (cond_extern space)) (Symtab.dest tab));
   173 
   174 
   175 (* dest *)
   176 
   177 fun dest_entry (xname, ([], _)) = NONE
   178   | dest_entry (xname, (name :: _, _)) = SOME (name, xname);
   179 
   180 fun dest (NameSpace tab) =
   181   map (apsnd (sort (int_ord o pairself size)))
   182     (Symtab.dest (Symtab.make_multi (List.mapPartial dest_entry (Symtab.dest tab))));
   183 
   184 
   185 end;
   186 
   187 
   188 val long_names = NameSpace.long_names;