1 (* Title: HOL/Tools/Nitpick/nitpick_rep.ML
2 Author: Jasmin Blanchette, TU Muenchen
3 Copyright 2008, 2009, 2010
5 Kodkod representations of Nitpick terms.
8 signature NITPICK_REP =
10 type polarity = Nitpick_Util.polarity
11 type scope = Nitpick_Scope.scope
23 exception REP of string * rep list
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
61 structure Nitpick_Rep : NITPICK_REP =
78 exception REP of string * rep list
80 (* polarity -> string *)
81 fun string_for_polarity Pos = "+"
82 | string_for_polarity Neg = "-"
83 | string_for_polarity Neut = "="
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
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 ^ "?"
105 fun is_Func (Func _) = true
107 fun is_Opt (Opt _) = true
109 fun is_opt_rep (Func (_, R2)) = is_opt_rep R2
110 | is_opt_rep (Opt _) = true
111 | is_opt_rep _ = false
114 fun card_of_rep Any = raise REP ("Nitpick_Rep.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 ("Nitpick_Rep.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 ("Nitpick_Rep.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
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
152 (* rep -> rep * rep *)
153 fun dest_Func (Func z) = z
154 | dest_Func R = raise REP ("Nitpick_Rep.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 (@{type_name fun}, [_, T2])) _ (Atom (1, _)) =
162 Atom (1, offset_of_type ofs T2)
163 | smart_range_rep ofs (Type (@{type_name fun}, [_, T2])) ran_card (Atom _) =
164 Atom (ran_card (), offset_of_type ofs T2)
165 | smart_range_rep _ _ _ R = raise REP ("Nitpick_Rep.smart_range_rep", [R])
167 (* rep -> rep list *)
168 fun binder_reps (Func (R1, R2)) = R1 :: binder_reps R2
171 fun body_rep (Func (_, R2)) = body_rep R2
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
179 (* int Typtab.table -> rep -> rep *)
180 fun one_rep _ _ Any = raise REP ("Nitpick_Rep.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 (@{type_name 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 (@{type_name 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)
193 fun unopt_rep (Func (R1, R2)) = Func (R1, unopt_rep R2)
194 | unopt_rep (Opt R) = R
197 (* polarity -> polarity -> polarity *)
198 fun min_polarity polar1 polar2 =
199 if polar1 = polar2 then
201 else if polar1 = Neut then
203 else if polar2 = Neut then
206 raise ARG ("Nitpick_Rep.min_polarity",
207 commas (map (quote o string_for_polarity) [polar1, polar2]))
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
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
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 ("Nitpick_Rep.min_rep", [R1, R2])
240 (* rep list -> rep list -> rep list *)
241 and 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
248 (* int -> rep -> int *)
249 fun card_of_domain_from_rep ran_card R =
252 | Atom (k, _) => exact_log ran_card k
254 | Func (R1, _) => card_of_rep R1
255 | Opt R => card_of_domain_from_rep ran_card R
256 | _ => raise REP ("Nitpick_Rep.card_of_domain_from_rep", [R])
258 (* int Typtab.table -> typ -> rep -> rep *)
259 fun rep_to_binary_rel_rep ofs T R =
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
265 (* scope -> typ -> rep *)
266 fun best_one_rep_for_type (scope as {card_assigns, ...} : scope)
267 (Type (@{type_name fun}, [T1, T2])) =
268 (case best_one_rep_for_type scope T2 of
270 | R2 => Vect (card_of_type card_assigns T1, R2))
271 | best_one_rep_for_type scope (Type (@{type_name "*"}, [T1, T2])) =
272 (case (best_one_rep_for_type scope T1, best_one_rep_for_type scope T2) of
274 | (R1, R2) => Struct [R1, R2])
275 | best_one_rep_for_type {card_assigns, datatypes, ofs, ...} T =
276 (case card_of_type card_assigns T of
277 1 => if is_some (datatype_spec datatypes T) orelse
278 is_iterator_type T then
279 Atom (1, offset_of_type ofs T)
282 | k => Atom (k, offset_of_type ofs T))
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 (@{type_name 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 (@{type_name fun}, [T1, T2])) =
293 (case (best_one_rep_for_type scope T1,
294 best_non_opt_set_rep_for_type scope T2) of
296 | (Unit, Atom (2, _)) =>
297 Func (Atom (1, offset_of_type ofs T1), Formula Neut)
298 | (R1, Atom (2, _)) => Func (R1, Formula Neut)
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_exact_type datatypes true 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 (@{type_name 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 ("Nitpick_Rep.best_non_opt_symmetric_reps_for_fun_type", [T], [])
311 (* rep -> (int * int) list *)
312 fun atom_schema_of_rep Any = raise REP ("Nitpick_Rep.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
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 (@{type_name "*"}, [T1, T2])) (Struct [R1, R2]) =
329 type_schema_of_reps [T1, T2] [R1, R2]
330 | type_schema_of_rep (Type (@{type_name fun}, [_, T2])) (Vect (k, R)) =
331 replicate_list k (type_schema_of_rep T2 R)
332 | type_schema_of_rep (Type (@{type_name 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 _ R = raise REP ("Nitpick_Rep.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)
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