33192
|
1 |
(* Title: HOL/Nitpick/Tools/nitpick_rep.ML
|
|
2 |
Author: Jasmin Blanchette, TU Muenchen
|
|
3 |
Copyright 2008, 2009
|
|
4 |
|
|
5 |
Kodkod representations of Nitpick terms.
|
|
6 |
*)
|
|
7 |
|
|
8 |
signature NITPICK_REP =
|
|
9 |
sig
|
|
10 |
type polarity = NitpickUtil.polarity
|
|
11 |
type scope = NitpickScope.scope
|
|
12 |
|
|
13 |
datatype rep =
|
|
14 |
Any |
|
|
15 |
Formula of polarity |
|
|
16 |
Unit |
|
|
17 |
Atom of int * int |
|
|
18 |
Struct of rep list |
|
|
19 |
Vect of int * rep |
|
|
20 |
Func of rep * rep |
|
|
21 |
Opt of rep
|
|
22 |
|
|
23 |
exception REP of string * rep list
|
|
24 |
|
|
25 |
val string_for_polarity : polarity -> string
|
|
26 |
val string_for_rep : rep -> string
|
|
27 |
val is_Func : rep -> bool
|
|
28 |
val is_Opt : rep -> bool
|
|
29 |
val is_opt_rep : rep -> bool
|
|
30 |
val flip_rep_polarity : rep -> rep
|
|
31 |
val card_of_rep : rep -> int
|
|
32 |
val arity_of_rep : rep -> int
|
|
33 |
val min_univ_card_of_rep : rep -> int
|
|
34 |
val is_one_rep : rep -> bool
|
|
35 |
val is_lone_rep : rep -> bool
|
|
36 |
val dest_Func : rep -> rep * rep
|
|
37 |
val smart_range_rep : int Typtab.table -> typ -> (unit -> int) -> rep -> rep
|
|
38 |
val binder_reps : rep -> rep list
|
|
39 |
val body_rep : rep -> rep
|
|
40 |
val one_rep : int Typtab.table -> typ -> rep -> rep
|
|
41 |
val optable_rep : int Typtab.table -> typ -> rep -> rep
|
|
42 |
val opt_rep : int Typtab.table -> typ -> rep -> rep
|
|
43 |
val unopt_rep : rep -> rep
|
|
44 |
val min_rep : rep -> rep -> rep
|
|
45 |
val min_reps : rep list -> rep list -> rep list
|
|
46 |
val card_of_domain_from_rep : int -> rep -> int
|
|
47 |
val rep_to_binary_rel_rep : int Typtab.table -> typ -> rep -> rep
|
|
48 |
val best_one_rep_for_type : scope -> typ -> rep
|
|
49 |
val best_opt_set_rep_for_type : scope -> typ -> rep
|
|
50 |
val best_non_opt_set_rep_for_type : scope -> typ -> rep
|
|
51 |
val best_set_rep_for_type : scope -> typ -> rep
|
|
52 |
val best_non_opt_symmetric_reps_for_fun_type : scope -> typ -> rep * rep
|
|
53 |
val atom_schema_of_rep : rep -> (int * int) list
|
|
54 |
val atom_schema_of_reps : rep list -> (int * int) list
|
|
55 |
val type_schema_of_rep : typ -> rep -> typ list
|
|
56 |
val type_schema_of_reps : typ list -> rep list -> typ list
|
|
57 |
val all_combinations_for_rep : rep -> int list list
|
|
58 |
val all_combinations_for_reps : rep list -> int list list
|
|
59 |
end;
|
|
60 |
|
|
61 |
structure NitpickRep : NITPICK_REP =
|
|
62 |
struct
|
|
63 |
|
|
64 |
open NitpickUtil
|
|
65 |
open NitpickHOL
|
|
66 |
open NitpickScope
|
|
67 |
|
|
68 |
datatype rep =
|
|
69 |
Any |
|
|
70 |
Formula of polarity |
|
|
71 |
Unit |
|
|
72 |
Atom of int * int |
|
|
73 |
Struct of rep list |
|
|
74 |
Vect of int * rep |
|
|
75 |
Func of rep * rep |
|
|
76 |
Opt of rep
|
|
77 |
|
|
78 |
exception REP of string * rep list
|
|
79 |
|
|
80 |
(* polarity -> string *)
|
|
81 |
fun string_for_polarity Pos = "+"
|
|
82 |
| string_for_polarity Neg = "-"
|
|
83 |
| string_for_polarity Neut = "="
|
|
84 |
|
|
85 |
(* rep -> string *)
|
|
86 |
fun atomic_string_for_rep rep =
|
|
87 |
let val s = string_for_rep rep in
|
|
88 |
if String.isPrefix "[" s orelse not (is_substring_of " " s) then s
|
|
89 |
else "(" ^ s ^ ")"
|
|
90 |
end
|
|
91 |
(* rep -> string *)
|
|
92 |
and string_for_rep Any = "X"
|
|
93 |
| string_for_rep (Formula polar) = "F" ^ string_for_polarity polar
|
|
94 |
| string_for_rep Unit = "U"
|
|
95 |
| string_for_rep (Atom (k, j0)) =
|
|
96 |
"A" ^ string_of_int k ^ (if j0 = 0 then "" else "@" ^ string_of_int j0)
|
|
97 |
| string_for_rep (Struct rs) = "[" ^ commas (map string_for_rep rs) ^ "]"
|
|
98 |
| string_for_rep (Vect (k, R)) =
|
|
99 |
string_of_int k ^ " x " ^ atomic_string_for_rep R
|
|
100 |
| string_for_rep (Func (R1, R2)) =
|
|
101 |
atomic_string_for_rep R1 ^ " => " ^ string_for_rep R2
|
|
102 |
| string_for_rep (Opt R) = atomic_string_for_rep R ^ "?"
|
|
103 |
|
|
104 |
(* rep -> bool *)
|
|
105 |
fun is_Func (Func _) = true
|
|
106 |
| is_Func _ = false
|
|
107 |
fun is_Opt (Opt _) = true
|
|
108 |
| is_Opt _ = false
|
|
109 |
fun is_opt_rep (Func (_, R2)) = is_opt_rep R2
|
|
110 |
| is_opt_rep (Opt _) = true
|
|
111 |
| is_opt_rep _ = false
|
|
112 |
|
|
113 |
(* rep -> int *)
|
|
114 |
fun card_of_rep Any = raise REP ("NitpickRep.card_of_rep", [Any])
|
|
115 |
| card_of_rep (Formula _) = 2
|
|
116 |
| card_of_rep Unit = 1
|
|
117 |
| card_of_rep (Atom (k, _)) = k
|
|
118 |
| card_of_rep (Struct rs) = Integer.prod (map card_of_rep rs)
|
|
119 |
| card_of_rep (Vect (k, R)) = reasonable_power (card_of_rep R) k
|
|
120 |
| card_of_rep (Func (R1, R2)) =
|
|
121 |
reasonable_power (card_of_rep R2) (card_of_rep R1)
|
|
122 |
| card_of_rep (Opt R) = card_of_rep R
|
|
123 |
fun arity_of_rep Any = raise REP ("NitpickRep.arity_of_rep", [Any])
|
|
124 |
| arity_of_rep (Formula _) = 0
|
|
125 |
| arity_of_rep Unit = 0
|
|
126 |
| arity_of_rep (Atom _) = 1
|
|
127 |
| arity_of_rep (Struct Rs) = Integer.sum (map arity_of_rep Rs)
|
|
128 |
| arity_of_rep (Vect (k, R)) = k * arity_of_rep R
|
|
129 |
| arity_of_rep (Func (R1, R2)) = arity_of_rep R1 + arity_of_rep R2
|
|
130 |
| arity_of_rep (Opt R) = arity_of_rep R
|
|
131 |
fun min_univ_card_of_rep Any =
|
|
132 |
raise REP ("NitpickRep.min_univ_card_of_rep", [Any])
|
|
133 |
| min_univ_card_of_rep (Formula _) = 0
|
|
134 |
| min_univ_card_of_rep Unit = 0
|
|
135 |
| min_univ_card_of_rep (Atom (k, j0)) = k + j0 + 1
|
|
136 |
| min_univ_card_of_rep (Struct Rs) =
|
|
137 |
fold Integer.max (map min_univ_card_of_rep Rs) 0
|
|
138 |
| min_univ_card_of_rep (Vect (_, R)) = min_univ_card_of_rep R
|
|
139 |
| min_univ_card_of_rep (Func (R1, R2)) =
|
|
140 |
Int.max (min_univ_card_of_rep R1, min_univ_card_of_rep R2)
|
|
141 |
| min_univ_card_of_rep (Opt R) = min_univ_card_of_rep R
|
|
142 |
|
|
143 |
(* rep -> bool *)
|
|
144 |
fun is_one_rep Unit = true
|
|
145 |
| is_one_rep (Atom _) = true
|
|
146 |
| is_one_rep (Struct _) = true
|
|
147 |
| is_one_rep (Vect _) = true
|
|
148 |
| is_one_rep _ = false
|
|
149 |
fun is_lone_rep (Opt R) = is_one_rep R
|
|
150 |
| is_lone_rep R = is_one_rep R
|
|
151 |
|
|
152 |
(* rep -> rep * rep *)
|
|
153 |
fun dest_Func (Func z) = z
|
|
154 |
| dest_Func R = raise REP ("NitpickRep.dest_Func", [R])
|
|
155 |
(* int Typtab.table -> typ -> (unit -> int) -> rep -> rep *)
|
|
156 |
fun smart_range_rep _ _ _ Unit = Unit
|
|
157 |
| smart_range_rep _ _ _ (Vect (_, R)) = R
|
|
158 |
| smart_range_rep _ _ _ (Func (_, R2)) = R2
|
|
159 |
| smart_range_rep ofs T ran_card (Opt R) =
|
|
160 |
Opt (smart_range_rep ofs T ran_card R)
|
|
161 |
| smart_range_rep ofs (Type ("fun", [_, T2])) _ (Atom (1, _)) =
|
|
162 |
Atom (1, offset_of_type ofs T2)
|
|
163 |
| smart_range_rep ofs (Type ("fun", [_, T2])) ran_card (Atom _) =
|
|
164 |
Atom (ran_card (), offset_of_type ofs T2)
|
|
165 |
| smart_range_rep _ _ _ R = raise REP ("NitpickRep.smart_range_rep", [R])
|
|
166 |
|
|
167 |
(* rep -> rep list *)
|
|
168 |
fun binder_reps (Func (R1, R2)) = R1 :: binder_reps R2
|
|
169 |
| binder_reps R = []
|
|
170 |
(* rep -> rep *)
|
|
171 |
fun body_rep (Func (_, R2)) = body_rep R2
|
|
172 |
| body_rep R = R
|
|
173 |
|
|
174 |
(* rep -> rep *)
|
|
175 |
fun flip_rep_polarity (Formula polar) = Formula (flip_polarity polar)
|
|
176 |
| flip_rep_polarity (Func (R1, R2)) = Func (R1, flip_rep_polarity R2)
|
|
177 |
| flip_rep_polarity R = R
|
|
178 |
|
|
179 |
(* int Typtab.table -> rep -> rep *)
|
|
180 |
fun one_rep _ _ Any = raise REP ("NitpickRep.one_rep", [Any])
|
|
181 |
| one_rep _ _ (Atom x) = Atom x
|
|
182 |
| one_rep _ _ (Struct Rs) = Struct Rs
|
|
183 |
| one_rep _ _ (Vect z) = Vect z
|
|
184 |
| one_rep ofs T (Opt R) = one_rep ofs T R
|
|
185 |
| one_rep ofs T R = Atom (card_of_rep R, offset_of_type ofs T)
|
|
186 |
fun optable_rep ofs (Type ("fun", [_, T2])) (Func (R1, R2)) =
|
|
187 |
Func (R1, optable_rep ofs T2 R2)
|
|
188 |
| optable_rep ofs T R = one_rep ofs T R
|
|
189 |
fun opt_rep ofs (Type ("fun", [_, T2])) (Func (R1, R2)) =
|
|
190 |
Func (R1, opt_rep ofs T2 R2)
|
|
191 |
| opt_rep ofs T R = Opt (optable_rep ofs T R)
|
|
192 |
(* rep -> rep *)
|
|
193 |
fun unopt_rep (Func (R1, R2)) = Func (R1, unopt_rep R2)
|
|
194 |
| unopt_rep (Opt R) = R
|
|
195 |
| unopt_rep R = R
|
|
196 |
|
|
197 |
(* polarity -> polarity -> polarity *)
|
|
198 |
fun min_polarity polar1 polar2 =
|
|
199 |
if polar1 = polar2 then
|
|
200 |
polar1
|
|
201 |
else if polar1 = Neut then
|
|
202 |
polar2
|
|
203 |
else if polar2 = Neut then
|
|
204 |
polar1
|
|
205 |
else
|
|
206 |
raise ARG ("NitpickRep.min_polarity",
|
|
207 |
commas (map (quote o string_for_polarity) [polar1, polar2]))
|
|
208 |
|
|
209 |
(* It's important that Func is before Vect, because if the range is Opt we
|
|
210 |
could lose information by converting a Func to a Vect. *)
|
|
211 |
(* rep -> rep -> rep *)
|
|
212 |
fun min_rep (Opt R1) (Opt R2) = Opt (min_rep R1 R2)
|
|
213 |
| min_rep (Opt R) _ = Opt R
|
|
214 |
| min_rep _ (Opt R) = Opt R
|
|
215 |
| min_rep (Formula polar1) (Formula polar2) =
|
|
216 |
Formula (min_polarity polar1 polar2)
|
|
217 |
| min_rep (Formula polar) _ = Formula polar
|
|
218 |
| min_rep _ (Formula polar) = Formula polar
|
|
219 |
| min_rep Unit _ = Unit
|
|
220 |
| min_rep _ Unit = Unit
|
|
221 |
| min_rep (Atom x) _ = Atom x
|
|
222 |
| min_rep _ (Atom x) = Atom x
|
|
223 |
| min_rep (Struct Rs1) (Struct Rs2) = Struct (min_reps Rs1 Rs2)
|
|
224 |
| min_rep (Struct Rs) _ = Struct Rs
|
|
225 |
| min_rep _ (Struct Rs) = Struct Rs
|
|
226 |
| min_rep (R1 as Func (R11, R12)) (R2 as Func (R21, R22)) =
|
|
227 |
(case pairself is_opt_rep (R12, R22) of
|
|
228 |
(true, false) => R1
|
|
229 |
| (false, true) => R2
|
|
230 |
| _ => if R11 = R21 then Func (R11, min_rep R12 R22)
|
|
231 |
else if min_rep R11 R21 = R11 then R1
|
|
232 |
else R2)
|
|
233 |
| min_rep (Func z) _ = Func z
|
|
234 |
| min_rep _ (Func z) = Func z
|
|
235 |
| min_rep (Vect (k1, R1)) (Vect (k2, R2)) =
|
|
236 |
if k1 < k2 then Vect (k1, R1)
|
|
237 |
else if k1 > k2 then Vect (k2, R2)
|
|
238 |
else Vect (k1, min_rep R1 R2)
|
|
239 |
| min_rep R1 R2 = raise REP ("NitpickRep.min_rep", [R1, R2])
|
|
240 |
(* rep list -> rep list -> rep list *)
|
|
241 |
and min_reps [] _ = []
|
|
242 |
| min_reps _ [] = []
|
|
243 |
| min_reps (R1 :: Rs1) (R2 :: Rs2) =
|
|
244 |
if R1 = R2 then R1 :: min_reps Rs1 Rs2
|
|
245 |
else if min_rep R1 R2 = R1 then R1 :: Rs1
|
|
246 |
else R2 :: Rs2
|
|
247 |
|
|
248 |
(* int -> rep -> int *)
|
|
249 |
fun card_of_domain_from_rep ran_card R =
|
|
250 |
case R of
|
|
251 |
Unit => 1
|
|
252 |
| Atom (k, _) => exact_log ran_card k
|
|
253 |
| Vect (k, _) => k
|
|
254 |
| Func (R1, _) => card_of_rep R1
|
|
255 |
| Opt R => card_of_domain_from_rep ran_card R
|
|
256 |
| _ => raise REP ("NitpickRep.card_of_domain_from_rep", [R])
|
|
257 |
|
|
258 |
(* int Typtab.table -> typ -> rep -> rep *)
|
|
259 |
fun rep_to_binary_rel_rep ofs T R =
|
|
260 |
let
|
|
261 |
val k = exact_root 2 (card_of_domain_from_rep 2 R)
|
|
262 |
val j0 = offset_of_type ofs (fst (HOLogic.dest_prodT (domain_type T)))
|
|
263 |
in Func (Struct [Atom (k, j0), Atom (k, j0)], Formula Neut) end
|
|
264 |
|
|
265 |
(* scope -> typ -> rep *)
|
|
266 |
fun best_one_rep_for_type (scope as {card_assigns, ...} : scope)
|
|
267 |
(Type ("fun", [T1, T2])) =
|
|
268 |
(case best_one_rep_for_type scope T2 of
|
|
269 |
Unit => Unit
|
|
270 |
| R2 => Vect (card_of_type card_assigns T1, R2))
|
|
271 |
| best_one_rep_for_type scope (Type ("*", [T1, T2])) =
|
|
272 |
(case (best_one_rep_for_type scope T1, best_one_rep_for_type scope T2) of
|
|
273 |
(Unit, Unit) => Unit
|
|
274 |
| (R1, R2) => Struct [R1, R2])
|
|
275 |
| best_one_rep_for_type (scope as {card_assigns, datatypes, ofs, ...}) T =
|
|
276 |
(case card_of_type card_assigns T of
|
|
277 |
1 => if is_some (datatype_spec datatypes T)
|
|
278 |
orelse is_fp_iterator_type T then
|
|
279 |
Atom (1, offset_of_type ofs T)
|
|
280 |
else
|
|
281 |
Unit
|
|
282 |
| k => Atom (k, offset_of_type ofs T))
|
|
283 |
|
|
284 |
(* Datatypes are never represented by Unit, because it would confuse
|
|
285 |
"nfa_transitions_for_ctor". *)
|
|
286 |
(* scope -> typ -> rep *)
|
|
287 |
fun best_opt_set_rep_for_type scope (Type ("fun", [T1, T2])) =
|
|
288 |
Func (best_one_rep_for_type scope T1, best_opt_set_rep_for_type scope T2)
|
|
289 |
| best_opt_set_rep_for_type (scope as {ofs, ...}) T =
|
|
290 |
opt_rep ofs T (best_one_rep_for_type scope T)
|
|
291 |
fun best_non_opt_set_rep_for_type (scope as {ofs, ...})
|
|
292 |
(Type ("fun", [T1, T2])) =
|
|
293 |
(case (best_one_rep_for_type scope T1,
|
|
294 |
best_non_opt_set_rep_for_type scope T2) of
|
|
295 |
(_, Unit) => Unit
|
|
296 |
| (Unit, Atom (2, _)) =>
|
|
297 |
Func (Atom (1, offset_of_type ofs T1), Formula Neut)
|
|
298 |
| (R1, Atom (2, _)) => Func (R1, Formula Neut)
|
|
299 |
| z => Func z)
|
|
300 |
| best_non_opt_set_rep_for_type scope T = best_one_rep_for_type scope T
|
|
301 |
fun best_set_rep_for_type (scope as {datatypes, ...}) T =
|
|
302 |
(if is_precise_type datatypes T then best_non_opt_set_rep_for_type
|
|
303 |
else best_opt_set_rep_for_type) scope T
|
|
304 |
fun best_non_opt_symmetric_reps_for_fun_type (scope as {ofs, ...})
|
|
305 |
(Type ("fun", [T1, T2])) =
|
|
306 |
(optable_rep ofs T1 (best_one_rep_for_type scope T1),
|
|
307 |
optable_rep ofs T2 (best_one_rep_for_type scope T2))
|
|
308 |
| best_non_opt_symmetric_reps_for_fun_type _ T =
|
|
309 |
raise TYPE ("NitpickRep.best_non_opt_symmetric_reps_for_fun_type", [T], [])
|
|
310 |
|
|
311 |
(* rep -> (int * int) list *)
|
|
312 |
fun atom_schema_of_rep Any = raise REP ("NitpickRep.atom_schema_of_rep", [Any])
|
|
313 |
| atom_schema_of_rep (Formula _) = []
|
|
314 |
| atom_schema_of_rep Unit = []
|
|
315 |
| atom_schema_of_rep (Atom x) = [x]
|
|
316 |
| atom_schema_of_rep (Struct Rs) = atom_schema_of_reps Rs
|
|
317 |
| atom_schema_of_rep (Vect (k, R)) = replicate_list k (atom_schema_of_rep R)
|
|
318 |
| atom_schema_of_rep (Func (R1, R2)) =
|
|
319 |
atom_schema_of_rep R1 @ atom_schema_of_rep R2
|
|
320 |
| atom_schema_of_rep (Opt R) = atom_schema_of_rep R
|
|
321 |
(* rep list -> (int * int) list *)
|
|
322 |
and atom_schema_of_reps Rs = maps atom_schema_of_rep Rs
|
|
323 |
|
|
324 |
(* typ -> rep -> typ list *)
|
|
325 |
fun type_schema_of_rep _ (Formula _) = []
|
|
326 |
| type_schema_of_rep _ Unit = []
|
|
327 |
| type_schema_of_rep T (Atom _) = [T]
|
|
328 |
| type_schema_of_rep (Type ("*", [T1, T2])) (Struct [R1, R2]) =
|
|
329 |
type_schema_of_reps [T1, T2] [R1, R2]
|
|
330 |
| type_schema_of_rep (Type ("fun", [_, T2])) (Vect (k, R)) =
|
|
331 |
replicate_list k (type_schema_of_rep T2 R)
|
|
332 |
| type_schema_of_rep (Type ("fun", [T1, T2])) (Func (R1, R2)) =
|
|
333 |
type_schema_of_rep T1 R1 @ type_schema_of_rep T2 R2
|
|
334 |
| type_schema_of_rep T (Opt R) = type_schema_of_rep T R
|
|
335 |
| type_schema_of_rep T R = raise REP ("NitpickRep.type_schema_of_rep", [R])
|
|
336 |
(* typ list -> rep list -> typ list *)
|
|
337 |
and type_schema_of_reps Ts Rs = flat (map2 type_schema_of_rep Ts Rs)
|
|
338 |
|
|
339 |
(* rep -> int list list *)
|
|
340 |
val all_combinations_for_rep = all_combinations o atom_schema_of_rep
|
|
341 |
(* rep list -> int list list *)
|
|
342 |
val all_combinations_for_reps = all_combinations o atom_schema_of_reps
|
|
343 |
|
|
344 |
end;
|