src/Pure/name_space.ML
changeset 3761 d99d93d46ca5
child 3769 931c336b0707
equal deleted inserted replaced
3760:77f71f650433 3761:d99d93d46ca5
       
     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 slightly more ad-hoc.
       
     8 Does not support absolute addressing.  Unknown short (FIXME?) names
       
     9 are implicitely considered to be declared outermost.
       
    10 *)
       
    11 
       
    12 signature NAME_SPACE =
       
    13 sig
       
    14   val unpack: string -> string list
       
    15   val pack: string list -> string
       
    16   val qualified: string -> bool
       
    17   type T
       
    18   val dest: T -> string list
       
    19   val empty: T
       
    20   val extend: string list -> string list * T -> T
       
    21   val merge: T * T -> T
       
    22   val lookup: T -> string -> string
       
    23   val prune: T -> string -> string
       
    24 end;
       
    25 
       
    26 structure NameSpace: NAME_SPACE =
       
    27 struct
       
    28 
       
    29 
       
    30 (** long identifiers **)
       
    31 
       
    32 val separator = "'";
       
    33 
       
    34 fun unpack_aux name =
       
    35   let
       
    36     (*handle trailing separators gracefully*)
       
    37     val (chars, seps) = take_suffix (equal separator) name;
       
    38     fun expl chs =
       
    39       (case take_prefix (not_equal separator) chs of
       
    40         (cs, []) => [implode (cs @ seps)]
       
    41       | (cs, _ :: cs') => implode cs :: expl cs');
       
    42   in expl chars end;
       
    43 
       
    44 val unpack = unpack_aux o explode;
       
    45 val pack = space_implode separator;
       
    46 
       
    47 fun qualified name =
       
    48   let val chs = explode name in
       
    49     exists (equal separator) chs andalso (length (unpack_aux chs) > 1)
       
    50   end;
       
    51 
       
    52 
       
    53 
       
    54 (** name spaces **)
       
    55 
       
    56 (* utils *)
       
    57 
       
    58 fun prefixes1 [] = []
       
    59   | prefixes1 (x :: xs) = map (cons x) ([] :: prefixes1 xs);
       
    60 
       
    61 fun suffixes1 xs = map rev (prefixes1 (rev xs));
       
    62 
       
    63 
       
    64 (* datatype T *)
       
    65 
       
    66 datatype T =
       
    67   NameSpace of string list list * string Symtab.table;
       
    68 
       
    69 fun entries_of (NameSpace (entries, _)) = entries;
       
    70 fun tab_of (NameSpace (_, tab)) = tab;
       
    71 
       
    72 fun make entries =
       
    73   let
       
    74     fun accesses entry =
       
    75       let val packed = pack entry in
       
    76         map (rpair packed o pack) (suffixes1 entry)
       
    77       end;
       
    78     val mapping = gen_distinct eq_fst (flat (map accesses entries));
       
    79   in
       
    80     NameSpace (entries, Symtab.make mapping)
       
    81   end;
       
    82 
       
    83 fun dest space = rev (map pack (entries_of space));
       
    84 
       
    85 
       
    86 
       
    87 (* empty, extend, merge operations *)
       
    88 
       
    89 val empty = make [];
       
    90 
       
    91 fun extend path (entries, space) =
       
    92   make (map (fn e => path @ unpack e) (rev entries) @ entries_of space);
       
    93 
       
    94 fun merge (space1, space2) =
       
    95   make (merge_lists (entries_of space1) (entries_of space2));
       
    96 
       
    97 
       
    98 (* lookup / prune names *)
       
    99 
       
   100 (* FIXME improve handling of undeclared qualified names (?) *)
       
   101 fun lookup space name =
       
   102   if_none (Symtab.lookup (tab_of space, name)) name;
       
   103 
       
   104 fun prune space name =
       
   105   let
       
   106     fun try [] = name
       
   107       | try (nm :: nms) =
       
   108           if lookup space nm = name then nm
       
   109           else try nms;
       
   110   in try (map pack (suffixes1 (unpack name))) end;
       
   111 
       
   112 
       
   113 end;