|
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; |