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 append: string -> string -> string |
|
16 val unpack: string -> string list |
|
17 val pack: string list -> string |
|
18 val base: string -> string |
|
19 val qualified: string -> bool |
|
20 val accesses: string -> string list |
|
21 type T |
|
22 val empty: T |
|
23 val extend: T * string list -> T |
|
24 val merge: T * T -> T |
|
25 val intern: T -> string -> string |
|
26 val extern: T -> string -> string |
|
27 val dest: T -> (string * string list) list |
|
28 end; |
|
29 |
|
30 structure NameSpace: NAME_SPACE = |
|
31 struct |
|
32 |
|
33 |
|
34 (** utils **) |
|
35 |
|
36 fun prefixes1 [] = [] |
|
37 | prefixes1 (x :: xs) = map (cons x) ([] :: prefixes1 xs); |
|
38 |
|
39 fun suffixes1 xs = map rev (prefixes1 (rev xs)); |
|
40 |
|
41 |
|
42 |
|
43 (** long identifiers **) |
|
44 |
|
45 val separator = "."; |
|
46 |
|
47 fun append name1 name2 = name1 ^ separator ^ name2; |
|
48 |
|
49 val unpack = space_explode separator; |
|
50 val pack = space_implode separator; |
|
51 |
|
52 val base = last_elem o unpack; |
|
53 fun qualified name = length (unpack name) > 1; |
|
54 |
|
55 fun accesses name = |
|
56 let |
|
57 val uname = unpack name; |
|
58 val (q, b) = split_last uname; |
|
59 val sfxs = suffixes1 uname; |
|
60 val pfxs = map (fn x => x @ [b]) (prefixes1 q); |
|
61 in map pack (sfxs @ pfxs) end; |
|
62 |
|
63 |
|
64 |
|
65 (** name spaces **) |
|
66 |
|
67 (* datatype T *) |
|
68 |
|
69 datatype T = |
|
70 NameSpace of string Symtab.table; |
|
71 |
|
72 val empty = NameSpace Symtab.empty; |
|
73 |
|
74 |
|
75 (* extend, merge operations *) |
|
76 |
|
77 fun add (tab, entry) = Symtab.update (entry, tab); |
|
78 |
|
79 fun extend (NameSpace tab, names) = |
|
80 NameSpace (foldl add (tab, flat (map (fn name => map (rpair name) (accesses name)) names))); |
|
81 |
|
82 fun merge (NameSpace tab1, NameSpace tab2) = (*2nd overrides 1st*) |
|
83 NameSpace (foldl add (tab1, Symtab.dest tab2)); |
|
84 |
|
85 |
|
86 (* intern / extern names *) |
|
87 |
|
88 fun intern (NameSpace tab) name = |
|
89 if_none (Symtab.lookup (tab, name)) name; |
|
90 |
|
91 fun extern space name = |
|
92 let |
|
93 fun try [] = "??" ^ separator ^ name (*hidden name*) |
|
94 | try (nm :: nms) = |
|
95 if intern space nm = name then nm |
|
96 else try nms; |
|
97 in try (map pack (suffixes1 (unpack name))) end; |
|
98 |
|
99 |
|
100 (* dest *) |
|
101 |
|
102 fun dest (NameSpace tab) = |
|
103 map (apsnd (sort (int_ord o pairself size))) |
|
104 (Symtab.dest (Symtab.make_multi (map swap (Symtab.dest tab)))); |
|
105 |
|
106 |
|
107 end; |
|