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