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