src/Pure/name_space.ML
changeset 3786 d5655489867c
parent 3769 931c336b0707
child 3803 3e581526ae5e
equal deleted inserted replaced
3785:0830d11b8916 3786:d5655489867c
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     4 
     5 Hierarchically structured name spaces.
     5 Hierarchically structured name spaces.
     6 
     6 
     7 More general than ML-like nested structures, but slightly more ad-hoc.
     7 More general than ML-like nested structures, but also slightly more
     8 Does not support absolute addressing.  Unknown short (FIXME?) names
     8 ad-hoc.  Does not support absolute addressing.  Unknown names are
     9 are implicitely considered to be declared outermost.
     9 implicitely considered to be declared outermost.
       
    10 
       
    11 TODO:
       
    12   - absolute paths?
    10 *)
    13 *)
    11 
    14 
    12 signature NAME_SPACE =
    15 signature NAME_SPACE =
    13 sig
    16 sig
    14   val separator: string		(*single char!*)
    17   val separator: string		(*single char!*)
    15   val unpack: string -> string list
    18   val unpack: string -> string list
    16   val pack: string list -> string
    19   val pack: string list -> string
       
    20   val base: string -> string
    17   val qualified: string -> bool
    21   val qualified: string -> bool
    18   type T
    22   type T
    19   val dest: T -> string list
    23   val dest: T -> string list
    20   val empty: T
    24   val empty: T
    21   val extend: string list -> string list * T -> T
    25   val extend: string list * T -> T
    22   val merge: T * T -> T
    26   val merge: T * T -> T
    23   val lookup: T -> string -> string
    27   val lookup: T -> string -> string
    24   val prune: T -> string -> string
    28   val prune: T -> string -> string
    25 end;
    29 end;
    26 
    30 
    42       | (cs, _ :: cs') => implode cs :: expl cs');
    46       | (cs, _ :: cs') => implode cs :: expl cs');
    43   in expl chars end;
    47   in expl chars end;
    44 
    48 
    45 val unpack = unpack_aux o explode;
    49 val unpack = unpack_aux o explode;
    46 val pack = space_implode separator;
    50 val pack = space_implode separator;
       
    51 
       
    52 val base = last_elem o unpack;
    47 
    53 
    48 fun qualified name =
    54 fun qualified name =
    49   let val chs = explode name in
    55   let val chs = explode name in
    50     exists (equal separator) chs andalso (length (unpack_aux chs) > 1)
    56     exists (equal separator) chs andalso (length (unpack_aux chs) > 1)
    51   end;
    57   end;
    87 
    93 
    88 (* empty, extend, merge operations *)
    94 (* empty, extend, merge operations *)
    89 
    95 
    90 val empty = make [];
    96 val empty = make [];
    91 
    97 
    92 fun extend path (entries, space) =
    98 fun extend (entries, space) =
    93   make (map (fn e => path @ unpack e) (rev entries) @ entries_of space);
    99   make (map unpack (rev entries) @ entries_of space);
    94 
   100 
    95 fun merge (space1, space2) =
   101 fun merge (space1, space2) =
    96   make (merge_lists (entries_of space1) (entries_of space2));
   102   make (merge_lists (entries_of space1) (entries_of space2));
    97 
   103 
    98 
   104 
    99 (* lookup / prune names *)
   105 (* lookup / prune names *)
   100 
   106 
   101 (* FIXME improve handling of undeclared qualified names (?) *)
       
   102 fun lookup space name =
   107 fun lookup space name =
   103   if_none (Symtab.lookup (tab_of space, name)) name;
   108   if_none (Symtab.lookup (tab_of space, name)) name;
   104 
   109 
   105 fun prune space name =
   110 fun prune space name =
   106   let
   111   if not (qualified name) then name
   107     fun try [] = name
   112   else
   108       | try (nm :: nms) =
   113     let
   109           if lookup space nm = name then nm
   114       fun try [] = name
   110           else try nms;
   115         | try (nm :: nms) =
   111   in try (map pack (suffixes1 (unpack name))) end;
   116             if lookup space nm = name then nm
       
   117             else try nms;
       
   118     in try (map pack (suffixes1 (unpack name))) end;
   112 
   119 
   113 
   120 
   114 end;
   121 end;