src/Pure/name_space.ML
author wenzelm
Fri Oct 10 15:51:14 1997 +0200 (1997-10-10)
changeset 3833 370e845c391f
parent 3803 3e581526ae5e
child 3876 e6f918979f2d
permissions -rw-r--r--
tuned;
more accesses to long name;
     1 (*  Title:      Pure/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 unpack: string -> string list
    16   val pack: string list -> string
    17   val base: string -> string
    18   val qualified: string -> bool
    19   type T
    20   val dest: T -> string list
    21   val empty: T
    22   val extend: string list * T -> T
    23   val merge: T * T -> T
    24   val lookup: T -> string -> string
    25   val prune: T -> string -> string
    26 end;
    27 
    28 structure NameSpace(*: NAME_SPACE FIXME *) =
    29 struct
    30 
    31 
    32 (** long identifiers **)
    33 
    34 val separator = ".";
    35 
    36 val unpack = space_explode separator;
    37 val pack = space_implode separator;
    38 
    39 val base = last_elem o unpack;
    40 fun qualified name = length (unpack name) > 1;
    41 
    42 
    43 
    44 (** name spaces **)
    45 
    46 (* utils *)
    47 
    48 fun prefixes1 [] = []
    49   | prefixes1 (x :: xs) = map (cons x) ([] :: prefixes1 xs);
    50 
    51 fun suffixes1 xs = map rev (prefixes1 (rev xs));
    52 
    53 
    54 (* datatype T *)
    55 
    56 datatype T =
    57   NameSpace of string list list * string Symtab.table;
    58 
    59 fun entries_of (NameSpace (entries, _)) = entries;
    60 fun tab_of (NameSpace (_, tab)) = tab;
    61 
    62 fun make entries =
    63   let
    64     fun accesses [] = []		(* FIXME !? *)
    65       | accesses entry =
    66           let
    67             val p = pack entry;
    68             val (q, b) = split_last entry;
    69             val sfxs = suffixes1 entry;
    70             val pfxs = map (fn x => x @ [b]) (prefixes1 q);
    71           in
    72             map (rpair p o pack) (sfxs @ pfxs)
    73           end;
    74     val mapping = filter_out (op =)
    75       (gen_distinct eq_fst (flat (map accesses entries)));
    76   in
    77     NameSpace (entries, Symtab.make mapping)
    78   end;
    79 
    80 fun dest space = rev (map pack (entries_of space));
    81 
    82 
    83 
    84 (* empty, extend, merge operations *)
    85 
    86 val empty = make [];
    87 
    88 fun extend (entries, space) =
    89   make (map unpack (rev entries) @ entries_of space);
    90 
    91 fun merge (space1, space2) =    (*2nd overrides 1st*)
    92   make (merge_lists (entries_of space2) (entries_of space1));
    93 
    94 
    95 (* lookup / prune names *)
    96 
    97 fun lookup space name =
    98   if_none (Symtab.lookup (tab_of space, name)) name;
    99 
   100 fun prune space name =
   101   if not (qualified name) then name
   102   else
   103     let
   104       fun try [] = "??" ^ separator ^ name      (*hidden name*)
   105         | try (nm :: nms) =
   106             if lookup space nm = name then nm
   107             else try nms;
   108     in try (map pack (suffixes1 (unpack name))) end;
   109 
   110 
   111 end;