src/Pure/General/name_space.ML
author wenzelm
Wed, 10 Jun 1998 11:51:58 +0200
changeset 5012 086b055c4d73
child 5175 2dbef0104bcf
permissions -rw-r--r--
moved name_space.ML to General/name_space.ML;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/name_space.ML
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
     4
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
     5
Hierarchically structured name spaces.
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
     6
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
     7
More general than ML-like nested structures, but also slightly more
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
     8
ad-hoc.  Does not support absolute addressing.  Unknown names are
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
     9
implicitely considered to be declared outermost.
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    10
*)
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    11
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    12
signature NAME_SPACE =
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    13
sig
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    14
  val separator: string                 (*single char!*)
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    15
  val append: string -> string -> string
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    16
  val unpack: string -> string list
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    17
  val pack: string list -> string
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    18
  val base: string -> string
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    19
  val qualified: string -> bool
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    20
  val accesses: string -> string list
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    21
  type T
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    22
  val empty: T
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    23
  val extend: T * string list -> T
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    24
  val merge: T * T -> T
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    25
  val intern: T -> string -> string
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    26
  val extern: T -> string -> string
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    27
  val dest: T -> (string * string list) list
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    28
end;
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    29
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    30
structure NameSpace: NAME_SPACE =
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    31
struct
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    32
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    33
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    34
(** utils **)
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    35
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    36
fun prefixes1 [] = []
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    37
  | prefixes1 (x :: xs) = map (cons x) ([] :: prefixes1 xs);
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    38
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    39
fun suffixes1 xs = map rev (prefixes1 (rev xs));
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    40
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    41
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    42
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    43
(** long identifiers **)
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    44
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    45
val separator = ".";
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    46
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    47
fun append name1 name2 = name1 ^ separator ^ name2;
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    48
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    49
val unpack = space_explode separator;
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    50
val pack = space_implode separator;
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    51
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    52
val base = last_elem o unpack;
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    53
fun qualified name = length (unpack name) > 1;
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    54
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    55
fun accesses name =
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    56
  let
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    57
    val uname = unpack name;
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    58
    val (q, b) = split_last uname;
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    59
    val sfxs = suffixes1 uname;
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    60
    val pfxs = map (fn x => x @ [b]) (prefixes1 q);
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    61
  in map pack (sfxs @ pfxs) end;
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    62
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    63
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    64
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    65
(** name spaces **)
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    66
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    67
(* datatype T *)
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    68
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    69
datatype T =
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    70
  NameSpace of string Symtab.table;
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    71
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    72
val empty = NameSpace Symtab.empty;
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    73
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    74
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    75
(* extend, merge operations *)
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    76
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    77
fun add (tab, entry) = Symtab.update (entry, tab);
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    78
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    79
fun extend (NameSpace tab, names) =
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    80
  NameSpace (foldl add (tab, flat (map (fn name => map (rpair name) (accesses name)) names)));
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    81
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    82
fun merge (NameSpace tab1, NameSpace tab2) =    (*2nd overrides 1st*)
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    83
  NameSpace (foldl add (tab1, Symtab.dest tab2));
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    84
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    85
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    86
(* intern / extern names *)
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    87
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    88
fun intern (NameSpace tab) name =
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    89
  if_none (Symtab.lookup (tab, name)) name;
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    90
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    91
fun extern space name =
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    92
  let
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    93
    fun try [] = "??" ^ separator ^ name      (*hidden name*)
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    94
      | try (nm :: nms) =
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    95
          if intern space nm = name then nm
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    96
          else try nms;
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    97
  in try (map pack (suffixes1 (unpack name))) end;
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    98
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    99
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   100
(* dest *)
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   101
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   102
fun dest (NameSpace tab) =
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   103
  map (apsnd (sort (int_ord o pairself size)))
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   104
    (Symtab.dest (Symtab.make_multi (map swap (Symtab.dest tab))));
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   105
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   106
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   107
end;