author | wenzelm |
Wed, 18 May 2005 11:30:59 +0200 | |
changeset 16002 | e0557c452138 |
parent 15624 | 484178635bd8 |
child 16137 | 00e9ca1e7261 |
permissions | -rw-r--r-- |
6118 | 1 |
(* Title: Pure/General/name_space.ML |
5012 | 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 |
|
12588 | 14 |
val separator: string (*single char*) |
9120 | 15 |
val hidden: string -> string |
5012 | 16 |
val append: string -> string -> string |
17 |
val unpack: string -> string list |
|
18 |
val pack: string list -> string |
|
19 |
val base: string -> string |
|
11829 | 20 |
val map_base: (string -> string) -> string -> string |
8728 | 21 |
val is_qualified: string -> bool |
5012 | 22 |
val accesses: string -> string list |
13332 | 23 |
val accesses': string -> string list |
5012 | 24 |
type T |
25 |
val empty: T |
|
26 |
val extend: T * string list -> T |
|
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15574
diff
changeset
|
27 |
val extend': (string -> string list) -> T * string list -> T |
5012 | 28 |
val merge: T * T -> T |
12588 | 29 |
val hide: bool -> T * string list -> T |
5012 | 30 |
val intern: T -> string -> string |
31 |
val extern: T -> string -> string |
|
5175 | 32 |
val long_names: bool ref |
14382 | 33 |
val short_names: bool ref |
15016 | 34 |
val unique_names: bool ref |
5175 | 35 |
val cond_extern: T -> string -> string |
6845 | 36 |
val cond_extern_table: T -> 'a Symtab.table -> (string * 'a) list |
5012 | 37 |
val dest: T -> (string * string list) list |
38 |
end; |
|
39 |
||
40 |
structure NameSpace: NAME_SPACE = |
|
41 |
struct |
|
42 |
||
43 |
(** long identifiers **) |
|
44 |
||
45 |
val separator = "."; |
|
8728 | 46 |
fun hidden name = "??." ^ name; |
47 |
fun is_hidden name = (case explode name of "?" :: "?" :: "." :: _ => true | _ => false); |
|
5012 | 48 |
|
49 |
fun append name1 name2 = name1 ^ separator ^ name2; |
|
50 |
||
51 |
val unpack = space_explode separator; |
|
52 |
val pack = space_implode separator; |
|
53 |
||
15570 | 54 |
val base = List.last o unpack; |
11829 | 55 |
|
56 |
fun map_base f name = |
|
57 |
let val uname = unpack name |
|
58 |
in pack (map_nth_elem (length uname - 1) f uname) end; |
|
59 |
||
8728 | 60 |
fun is_qualified name = length (unpack name) > 1; |
5012 | 61 |
|
62 |
fun accesses name = |
|
63 |
let |
|
64 |
val uname = unpack name; |
|
65 |
val (q, b) = split_last uname; |
|
12251 | 66 |
val sfxs = Library.suffixes1 uname; |
67 |
val pfxs = map (fn x => x @ [b]) (Library.prefixes1 q); |
|
5012 | 68 |
in map pack (sfxs @ pfxs) end; |
69 |
||
13332 | 70 |
val accesses' = map pack o Library.suffixes1 o unpack; |
71 |
||
5012 | 72 |
|
73 |
||
74 |
(** name spaces **) |
|
75 |
||
8728 | 76 |
(* basic operations *) |
77 |
||
78 |
fun map_space f xname tab = |
|
16002 | 79 |
Symtab.update ((xname, f (if_none (Symtab.lookup (tab, xname)) ([], []))), tab); |
8728 | 80 |
|
81 |
fun change f xname (name, tab) = |
|
82 |
map_space (fn (names, names') => (f names name, names')) xname tab; |
|
83 |
||
84 |
fun change' f xname (name', tab) = |
|
85 |
map_space (fn (names, names') => (names, f names' name')) xname tab; |
|
86 |
||
87 |
fun del names nm = if nm mem_string names then Library.gen_rem (op =) (names, nm) else names; |
|
88 |
fun add names nm = nm :: del names nm; |
|
89 |
||
90 |
||
5012 | 91 |
(* datatype T *) |
92 |
||
93 |
datatype T = |
|
8728 | 94 |
NameSpace of (string list * string list) Symtab.table; |
5012 | 95 |
|
96 |
val empty = NameSpace Symtab.empty; |
|
97 |
||
98 |
||
8728 | 99 |
(* extend *) (*later entries preferred*) |
100 |
||
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15574
diff
changeset
|
101 |
fun gen_extend_aux acc (name, tab) = |
8728 | 102 |
if is_hidden name then |
103 |
error ("Attempt to declare hidden name " ^ quote name) |
|
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15574
diff
changeset
|
104 |
else Library.foldl (fn (tb, xname) => change add xname (name, tb)) (tab, acc name); |
5012 | 105 |
|
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15574
diff
changeset
|
106 |
fun extend' acc (NameSpace tab, names) = |
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15574
diff
changeset
|
107 |
NameSpace (foldr (gen_extend_aux acc) tab names); |
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15574
diff
changeset
|
108 |
fun extend (NameSpace tab, names) = |
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15574
diff
changeset
|
109 |
NameSpace (foldr (gen_extend_aux accesses) tab names); |
8728 | 110 |
|
111 |
||
112 |
(* merge *) (*1st preferred over 2nd*) |
|
113 |
||
14198
8ea2645b8132
Modified merge_aux to prevent newer names from getting overwritten
berghofe
parents:
13332
diff
changeset
|
114 |
fun merge_aux (tab, (xname, (names1, names1'))) = |
8ea2645b8132
Modified merge_aux to prevent newer names from getting overwritten
berghofe
parents:
13332
diff
changeset
|
115 |
map_space (fn (names2, names2') => |
8ea2645b8132
Modified merge_aux to prevent newer names from getting overwritten
berghofe
parents:
13332
diff
changeset
|
116 |
(merge_lists' names2 names1, merge_lists' names2' names1')) xname tab; |
5012 | 117 |
|
8728 | 118 |
fun merge (NameSpace tab1, NameSpace tab2) = |
119 |
NameSpace (Symtab.foldl merge_aux (tab2, tab1)); |
|
120 |
||
121 |
||
122 |
(* hide *) |
|
5012 | 123 |
|
12588 | 124 |
fun hide_aux fully (name, tab) = |
8728 | 125 |
if not (is_qualified name) then |
126 |
error ("Attempt to hide global name " ^ quote name) |
|
127 |
else if is_hidden name then |
|
128 |
error ("Attempt to hide hidden name " ^ quote name) |
|
129 |
else (change' add name (name, |
|
15570 | 130 |
Library.foldl (fn (tb, xname) => change del xname (name, tb)) |
12588 | 131 |
(tab, if fully then accesses name else [base name]))); |
8728 | 132 |
|
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset
|
133 |
fun hide fully (NameSpace tab, names) = NameSpace (foldr (hide_aux fully) tab names); |
5012 | 134 |
|
135 |
||
136 |
(* intern / extern names *) |
|
137 |
||
8728 | 138 |
fun lookup (NameSpace tab) xname = |
139 |
(case Symtab.lookup (tab, xname) of |
|
15531 | 140 |
NONE => (xname, true) |
141 |
| SOME ([name], _) => (name, true) |
|
142 |
| SOME (name :: _, _) => (name, false) |
|
143 |
| SOME ([], []) => (xname, true) |
|
144 |
| SOME ([], name' :: _) => (hidden name', true)); |
|
8728 | 145 |
|
146 |
fun intern spc xname = #1 (lookup spc xname); |
|
5012 | 147 |
|
15016 | 148 |
fun unique_extern mkunique space name = |
5012 | 149 |
let |
8728 | 150 |
fun try [] = hidden name |
5012 | 151 |
| try (nm :: nms) = |
8728 | 152 |
let val (full_nm, uniq) = lookup space nm |
15016 | 153 |
in if full_nm = name andalso (uniq orelse (not mkunique)) then nm else try nms end |
13332 | 154 |
in try (accesses' name) end; |
5012 | 155 |
|
15016 | 156 |
(*output unique names by default*) |
157 |
val unique_names = ref true; |
|
158 |
||
5175 | 159 |
(*prune names on output by default*) |
160 |
val long_names = ref false; |
|
161 |
||
14382 | 162 |
(*output only base name*) |
163 |
val short_names = ref false; |
|
164 |
||
15016 | 165 |
fun extern space name = unique_extern (!unique_names) space name; |
166 |
||
14382 | 167 |
fun cond_extern space = |
168 |
if ! long_names then I |
|
169 |
else if ! short_names then base else extern space; |
|
5175 | 170 |
|
6845 | 171 |
fun cond_extern_table space tab = |
172 |
Library.sort_wrt #1 (map (apfst (cond_extern space)) (Symtab.dest tab)); |
|
173 |
||
5012 | 174 |
|
175 |
(* dest *) |
|
176 |
||
15531 | 177 |
fun dest_entry (xname, ([], _)) = NONE |
178 |
| dest_entry (xname, (name :: _, _)) = SOME (name, xname); |
|
8728 | 179 |
|
5012 | 180 |
fun dest (NameSpace tab) = |
181 |
map (apsnd (sort (int_ord o pairself size))) |
|
15570 | 182 |
(Symtab.dest (Symtab.make_multi (List.mapPartial dest_entry (Symtab.dest tab)))); |
5012 | 183 |
|
184 |
||
185 |
end; |
|
5175 | 186 |
|
187 |
||
188 |
val long_names = NameSpace.long_names; |