src/Pure/name_space.ML
author nipkow
Fri Nov 28 07:35:10 1997 +0100 (1997-11-28)
changeset 4318 9b672ea2dfe7
parent 4101 e8ad51c88be9
child 4490 14cd07c16e02
permissions -rw-r--r--
Fixed the definition of `termord': is now antisymmetric.
     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 declared: T -> string -> bool
    25   val intern: T -> string -> string
    26   val extern: T -> string -> string
    27 end;
    28 
    29 structure NameSpace: NAME_SPACE =
    30 struct
    31 
    32 
    33 (** long identifiers **)
    34 
    35 val separator = ".";
    36 
    37 val unpack = space_explode separator;
    38 val pack = space_implode separator;
    39 
    40 val base = last_elem o unpack;
    41 fun qualified name = length (unpack name) > 1;
    42 
    43 
    44 
    45 (** name spaces **)
    46 
    47 (* utils *)
    48 
    49 fun prefixes1 [] = []
    50   | prefixes1 (x :: xs) = map (cons x) ([] :: prefixes1 xs);
    51 
    52 fun suffixes1 xs = map rev (prefixes1 (rev xs));
    53 
    54 
    55 (* datatype T *)
    56 
    57 datatype T =
    58   NameSpace of string list list * string Symtab.table;
    59 
    60 fun entries_of (NameSpace (entries, _)) = entries;
    61 fun tab_of (NameSpace (_, tab)) = tab;
    62 
    63 fun make entries =
    64   let
    65     fun accesses [] = []
    66       | accesses entry =
    67           let
    68             val p = pack entry;
    69             val (q, b) = split_last entry;
    70             val sfxs = suffixes1 entry;
    71             val pfxs = map (fn x => x @ [b]) (prefixes1 q);
    72           in
    73             map (rpair p o pack) (sfxs @ pfxs)
    74           end;
    75     val mapping = filter_out (op =) (distinct_fst_string (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 fun declared space name = unpack name mem (entries_of space);
    95 
    96 
    97 (* intern / extern names *)
    98 
    99 fun intern space name =
   100   if_none (Symtab.lookup (tab_of space, name)) name;
   101 
   102 fun extern space name =
   103   let
   104     fun try [] = "??" ^ separator ^ name      (*hidden name*)
   105       | try (nm :: nms) =
   106           if intern space nm = name then nm
   107           else try nms;
   108   in try (map pack (suffixes1 (unpack name))) end;
   109 
   110 
   111 end;