optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil";
this gains one cardinality in the AA tree examples in the Nitpick manual
1 (* Title: HOL/Tools/Nitpick/nitpick_scope.ML
2 Author: Jasmin Blanchette, TU Muenchen
3 Copyright 2008, 2009, 2010
5 Scope enumerator for Nitpick.
8 signature NITPICK_SCOPE =
10 type styp = Nitpick_Util.styp
11 type hol_context = Nitpick_HOL.hol_context
28 constrs: constr_spec list}
31 hol_ctxt: hol_context,
32 card_assigns: (typ * int) list,
35 datatypes: dtype_spec list,
36 ofs: int Typtab.table}
38 val datatype_spec : dtype_spec list -> typ -> dtype_spec option
39 val constr_spec : dtype_spec list -> styp -> constr_spec
40 val is_complete_type : dtype_spec list -> typ -> bool
41 val is_concrete_type : dtype_spec list -> typ -> bool
42 val is_exact_type : dtype_spec list -> typ -> bool
43 val offset_of_type : int Typtab.table -> typ -> int
44 val spec_of_type : scope -> typ -> int * int
45 val pretties_for_scope : scope -> bool -> Pretty.T list
46 val multiline_string_for_scope : scope -> string
47 val scopes_equivalent : scope -> scope -> bool
48 val scope_less_eq : scope -> scope -> bool
50 hol_context -> int -> (typ option * int list) list
51 -> (styp option * int list) list -> (styp option * int list) list
52 -> int list -> int list -> typ list -> typ list -> typ list
56 structure Nitpick_Scope : NITPICK_SCOPE =
77 constrs: constr_spec list}
80 hol_ctxt: hol_context,
81 card_assigns: (typ * int) list,
84 datatypes: dtype_spec list,
85 ofs: int Typtab.table}
87 datatype row_kind = Card of typ | Max of styp
89 type row = row_kind * int list
92 (* dtype_spec list -> typ -> dtype_spec option *)
93 fun datatype_spec (dtypes : dtype_spec list) T =
94 List.find (curry (op =) T o #typ) dtypes
96 (* dtype_spec list -> styp -> constr_spec *)
97 fun constr_spec [] x = raise TERM ("Nitpick_Scope.constr_spec", [Const x])
98 | constr_spec ({constrs, ...} :: dtypes : dtype_spec list) (x as (s, T)) =
99 case List.find (curry (op =) (s, body_type T) o (apsnd body_type o #const))
102 | NONE => constr_spec dtypes x
104 (* dtype_spec list -> typ -> bool *)
105 fun is_complete_type dtypes (Type ("fun", [T1, T2])) =
106 is_concrete_type dtypes T1 andalso is_complete_type dtypes T2
107 | is_complete_type dtypes (Type ("*", Ts)) =
108 forall (is_complete_type dtypes) Ts
109 | is_complete_type dtypes T =
110 not (is_integer_type T) andalso not (is_bit_type T) andalso
111 #complete (the (datatype_spec dtypes T))
112 handle Option.Option => true
113 and is_concrete_type dtypes (Type ("fun", [T1, T2])) =
114 is_complete_type dtypes T1 andalso is_concrete_type dtypes T2
115 | is_concrete_type dtypes (Type ("*", Ts)) =
116 forall (is_concrete_type dtypes) Ts
117 | is_concrete_type dtypes T =
118 #concrete (the (datatype_spec dtypes T)) handle Option.Option => true
119 fun is_exact_type dtypes = is_complete_type dtypes andf is_concrete_type dtypes
121 (* int Typtab.table -> typ -> int *)
122 fun offset_of_type ofs T =
123 case Typtab.lookup ofs T of
125 | NONE => Typtab.lookup ofs dummyT |> the_default 0
127 (* scope -> typ -> int * int *)
128 fun spec_of_type ({card_assigns, ofs, ...} : scope) T =
129 (card_of_type card_assigns T
130 handle TYPE ("Nitpick_HOL.card_of_type", _, _) => ~1, offset_of_type ofs T)
132 (* (string -> string) -> scope
133 -> string list * string list * string list * string list * string list *)
134 fun quintuple_for_scope quote ({hol_ctxt as {thy, ctxt, ...}, card_assigns,
135 bits, bisim_depth, datatypes, ...} : scope) =
137 val boring_Ts = [@{typ unsigned_bit}, @{typ signed_bit}, @{typ \<xi>},
138 @{typ bisim_iterator}]
139 val (iter_assigns, card_assigns) =
140 card_assigns |> filter_out (member (op =) boring_Ts o fst)
141 |> List.partition (is_fp_iterator_type o fst)
142 val (secondary_card_assigns, primary_card_assigns) =
143 card_assigns |> List.partition ((is_integer_type orf is_datatype thy)
146 map (fn (T, k) => quote (string_for_type ctxt T) ^ " = " ^
150 (fn {const, explicit_max, ...} =>
151 if explicit_max < 0 then
154 SOME (Syntax.string_of_term ctxt (Const const) ^ " = " ^
155 string_of_int explicit_max))
156 o #constrs) datatypes
159 quote (Syntax.string_of_term ctxt
160 (Const (const_for_iterator_type T))) ^ " = " ^
161 string_of_int (k - 1)) iter_assigns
163 (if bits = 0 then [] else ["bits = " ^ string_of_int bits]) @
164 (if bisim_depth < 0 andalso forall (not o #co) datatypes then []
165 else ["bisim_depth = " ^ string_of_int bisim_depth])
168 (fn () => (cards primary_card_assigns, cards secondary_card_assigns,
169 maxes (), iters (), miscs ())) ()
172 (* scope -> bool -> Pretty.T list *)
173 fun pretties_for_scope scope verbose =
175 val (primary_cards, secondary_cards, maxes, iters, bisim_depths) =
176 quintuple_for_scope maybe_quote scope
177 val ss = map (prefix "card ") primary_cards @
179 map (prefix "card ") secondary_cards @
180 map (prefix "max ") maxes @
181 map (prefix "iter ") iters @
187 else serial_commas "and" ss |> map Pretty.str |> Pretty.breaks
190 (* scope -> string *)
191 fun multiline_string_for_scope scope =
193 val (primary_cards, secondary_cards, maxes, iters, bisim_depths) =
194 quintuple_for_scope I scope
195 val cards = primary_cards @ secondary_cards
197 case (if null cards then [] else ["card: " ^ commas cards]) @
198 (if null maxes then [] else ["max: " ^ commas maxes]) @
199 (if null iters then [] else ["iter: " ^ commas iters]) @
202 | lines => space_implode "\n" lines
205 (* scope -> scope -> bool *)
206 fun scopes_equivalent (s1 : scope) (s2 : scope) =
207 #datatypes s1 = #datatypes s2 andalso #card_assigns s1 = #card_assigns s2
208 fun scope_less_eq (s1 : scope) (s2 : scope) =
209 (s1, s2) |> pairself (map snd o #card_assigns) |> op ~~ |> forall (op <=)
212 fun rank_of_row (_, ks) = length ks
214 fun rank_of_block block = fold Integer.max (map rank_of_row block) 1
215 (* int -> typ * int list -> typ * int list *)
216 fun project_row column (y, ks) = (y, [nth ks (Int.min (column, length ks - 1))])
217 (* int -> block -> block *)
218 fun project_block (column, block) = map (project_row column) block
220 (* (''a * ''a -> bool) -> (''a option * int list) list -> ''a -> int list *)
221 fun lookup_ints_assign eq assigns key =
222 case triple_lookup eq assigns key of
224 | NONE => raise ARG ("Nitpick_Scope.lookup_ints_assign", "")
225 (* theory -> (typ option * int list) list -> typ -> int list *)
226 fun lookup_type_ints_assign thy assigns T =
227 map (curry Int.max 1) (lookup_ints_assign (type_match thy) assigns T)
228 handle ARG ("Nitpick_Scope.lookup_ints_assign", _) =>
229 raise TYPE ("Nitpick_Scope.lookup_type_ints_assign", [T], [])
230 (* theory -> (styp option * int list) list -> styp -> int list *)
231 fun lookup_const_ints_assign thy assigns x =
232 lookup_ints_assign (const_match thy) assigns x
233 handle ARG ("Nitpick_Scope.lookup_ints_assign", _) =>
234 raise TERM ("Nitpick_Scope.lookup_const_ints_assign", [Const x])
236 (* theory -> (styp option * int list) list -> styp -> row option *)
237 fun row_for_constr thy maxes_assigns constr =
238 SOME (Max constr, lookup_const_ints_assign thy maxes_assigns constr)
239 handle TERM ("lookup_const_ints_assign", _) => NONE
241 val max_bits = 31 (* Kodkod limit *)
243 (* hol_context -> (typ option * int list) list -> (styp option * int list) list
244 -> (styp option * int list) list -> int list -> int list -> typ -> block *)
245 fun block_for_type (hol_ctxt as {thy, ...}) cards_assigns maxes_assigns
246 iters_assigns bitss bisim_depths T =
247 if T = @{typ unsigned_bit} then
248 [(Card T, map (Integer.min max_bits o Integer.max 1) bitss)]
249 else if T = @{typ signed_bit} then
250 [(Card T, map (Integer.add 1 o Integer.min max_bits o Integer.max 1) bitss)]
251 else if T = @{typ "unsigned_bit word"} then
252 [(Card T, lookup_type_ints_assign thy cards_assigns nat_T)]
253 else if T = @{typ "signed_bit word"} then
254 [(Card T, lookup_type_ints_assign thy cards_assigns int_T)]
255 else if T = @{typ bisim_iterator} then
256 [(Card T, map (Integer.add 1 o Integer.max 0) bisim_depths)]
257 else if is_fp_iterator_type T then
258 [(Card T, map (Integer.add 1 o Integer.max 0)
259 (lookup_const_ints_assign thy iters_assigns
260 (const_for_iterator_type T)))]
262 (Card T, lookup_type_ints_assign thy cards_assigns T) ::
263 (case datatype_constrs hol_ctxt T of
265 | constrs => map_filter (row_for_constr thy maxes_assigns) constrs)
267 (* hol_context -> (typ option * int list) list -> (styp option * int list) list
268 -> (styp option * int list) list -> int list -> int list -> typ list
269 -> typ list -> block list *)
270 fun blocks_for_types hol_ctxt cards_assigns maxes_assigns iters_assigns bitss
271 bisim_depths mono_Ts nonmono_Ts =
274 val block_for = block_for_type hol_ctxt cards_assigns maxes_assigns
275 iters_assigns bitss bisim_depths
276 val mono_block = maps block_for mono_Ts
277 val nonmono_blocks = map block_for nonmono_Ts
278 in mono_block :: nonmono_blocks end
280 val sync_threshold = 5
282 (* int list -> int list list *)
283 fun all_combinations_ordered_smartly ks =
285 (* int list -> int *)
286 fun cost_with_monos [] = 0
287 | cost_with_monos (k :: ks) =
288 if k < sync_threshold andalso forall (curry (op =) k) ks then
291 k * (k + 1) div 2 + Integer.sum ks
292 fun cost_without_monos [] = 0
293 | cost_without_monos [k] = k
294 | cost_without_monos (_ :: k :: ks) =
295 if k < sync_threshold andalso forall (curry (op =) k) ks then
298 Integer.sum (k :: ks)
300 ks |> all_combinations
301 |> map (`(if fst (hd ks) > 1 then cost_with_monos
302 else cost_without_monos))
303 |> sort (int_ord o pairself fst) |> map snd
307 fun is_self_recursive_constr_type T =
308 exists (exists_subtype (curry (op =) (body_type T))) (binder_types T)
310 (* (styp * int) list -> styp -> int *)
311 fun constr_max maxes x = the_default ~1 (AList.lookup (op =) maxes x)
313 type scope_desc = (typ * int) list * (styp * int) list
315 (* hol_context -> scope_desc -> typ * int -> bool *)
316 fun is_surely_inconsistent_card_assign hol_ctxt (card_assigns, max_assigns)
318 case datatype_constrs hol_ctxt T of
323 map (Integer.prod o map (bounded_card_of_type k ~1 card_assigns)
324 o binder_types o snd) xs
325 val maxes = map (constr_max max_assigns) xs
326 (* int -> int -> int *)
327 fun effective_max card ~1 = card
328 | effective_max card max = Int.min (card, max)
329 val max = map2 effective_max dom_cards maxes |> Integer.sum
331 (* hol_context -> (typ * int) list -> (typ * int) list -> (styp * int) list
333 fun is_surely_inconsistent_scope_description hol_ctxt seen rest max_assigns =
334 exists (is_surely_inconsistent_card_assign hol_ctxt
335 (seen @ rest, max_assigns)) seen
337 (* hol_context -> scope_desc -> (typ * int) list option *)
338 fun repair_card_assigns hol_ctxt (card_assigns, max_assigns) =
340 (* (typ * int) list -> (typ * int) list -> (typ * int) list option *)
341 fun aux seen [] = SOME seen
342 | aux seen ((T, 0) :: _) = NONE
343 | aux seen ((T, k) :: rest) =
344 (if is_surely_inconsistent_scope_description hol_ctxt ((T, k) :: seen)
345 rest max_assigns then
348 case aux ((T, k) :: seen) rest of
349 SOME assigns => SOME assigns
350 | NONE => raise SAME ())
351 handle SAME () => aux seen ((T, k - 1) :: rest)
352 in aux [] (rev card_assigns) end
354 (* theory -> (typ * int) list -> typ * int -> typ * int *)
355 fun repair_iterator_assign thy assigns (T as Type (s, Ts), k) =
356 (T, if T = @{typ bisim_iterator} then
358 val co_cards = map snd (filter (is_codatatype thy o fst) assigns)
359 in Int.min (k, Integer.sum co_cards) end
360 else if is_fp_iterator_type T then
363 | _ => bounded_card_of_type k ~1 assigns (foldr1 HOLogic.mk_prodT Ts)
366 | repair_iterator_assign _ _ assign = assign
368 (* row -> scope_desc -> scope_desc *)
369 fun add_row_to_scope_descriptor (kind, ks) (card_assigns, max_assigns) =
371 Card T => ((T, the_single ks) :: card_assigns, max_assigns)
372 | Max x => (card_assigns, (x, the_single ks) :: max_assigns)
373 (* block -> scope_desc *)
374 fun scope_descriptor_from_block block =
375 fold_rev add_row_to_scope_descriptor block ([], [])
376 (* hol_context -> block list -> int list -> scope_desc option *)
377 fun scope_descriptor_from_combination (hol_ctxt as {thy, ...}) blocks columns =
379 val (card_assigns, max_assigns) =
380 maps project_block (columns ~~ blocks) |> scope_descriptor_from_block
381 val card_assigns = repair_card_assigns hol_ctxt (card_assigns, max_assigns)
384 SOME (map (repair_iterator_assign thy card_assigns) card_assigns,
387 handle Option.Option => NONE
389 (* theory -> (typ * int) list -> dtype_spec list -> int Typtab.table *)
390 fun offset_table_for_card_assigns thy assigns dtypes =
392 (* int -> (int * int) list -> (typ * int) list -> int Typtab.table
393 -> int Typtab.table *)
394 fun aux next _ [] = Typtab.update_new (dummyT, next)
395 | aux next reusable ((T, k) :: assigns) =
396 if k = 1 orelse is_integer_type T orelse is_bit_type T then
397 aux next reusable assigns
398 else if length (these (Option.map #constrs (datatype_spec dtypes T)))
400 Typtab.update_new (T, next) #> aux (next + k) reusable assigns
402 case AList.lookup (op =) reusable k of
403 SOME j0 => Typtab.update_new (T, j0) #> aux next reusable assigns
404 | NONE => Typtab.update_new (T, next)
405 #> aux (next + k) ((k, next) :: reusable) assigns
406 in aux 0 [] assigns Typtab.empty end
408 (* int -> (typ * int) list -> typ -> int *)
409 fun domain_card max card_assigns =
410 Integer.prod o map (bounded_card_of_type max max card_assigns) o binder_types
412 (* scope_desc -> bool -> int -> (int -> int) -> int -> int -> bool * styp
413 -> constr_spec list -> constr_spec list *)
414 fun add_constr_spec (card_assigns, max_assigns) co card sum_dom_cards
415 num_self_recs num_non_self_recs (self_rec, x as (s, T))
418 val max = constr_max max_assigns x
420 fun bound k = Int.min (card, (max >= 0 ? curry Int.min max) k)
422 fun next_delta () = if null constrs then 0 else #epsilon (hd constrs)
423 val {delta, epsilon, exclusive, total} =
425 let val delta = next_delta () in
426 {delta = delta, epsilon = delta, exclusive = true, total = false}
428 else if not co andalso num_self_recs > 0 then
429 (if num_self_recs = 1 andalso num_non_self_recs = 1 then
432 [{delta = 0, epsilon = 1, exclusive = true, ...}] =>
433 {delta = 1, epsilon = card, exclusive = true, total = false}
436 if domain_card 2 card_assigns T = 1 then
437 {delta = 0, epsilon = 1, exclusive = true, total = true}
443 {delta = 0, epsilon = card, exclusive = false, total = false}
444 else if card = sum_dom_cards (card + 1) then
445 let val delta = next_delta () in
446 {delta = delta, epsilon = delta + domain_card card card_assigns T,
447 exclusive = true, total = true}
450 {delta = 0, epsilon = card,
451 exclusive = (num_self_recs + num_non_self_recs = 1), total = false}
453 {const = x, delta = delta, epsilon = epsilon, exclusive = exclusive,
454 explicit_max = max, total = total} :: constrs
457 (* hol_context -> (typ * int) list -> typ -> bool *)
458 fun has_exact_card hol_ctxt card_assigns T =
459 let val card = card_of_type card_assigns T in
460 card = bounded_exact_card_of_type hol_ctxt (card + 1) 0 card_assigns T
463 (* hol_context -> typ list -> scope_desc -> typ * int -> dtype_spec *)
464 fun datatype_spec_from_scope_descriptor (hol_ctxt as {thy, ...}) deep_dataTs
465 (desc as (card_assigns, _)) (T, card) =
467 val deep = member (op =) deep_dataTs T
468 val co = is_codatatype thy T
469 val xs = boxed_datatype_constrs hol_ctxt T
470 val self_recs = map (is_self_recursive_constr_type o snd) xs
471 val (num_self_recs, num_non_self_recs) =
472 List.partition I self_recs |> pairself length
473 val complete = has_exact_card hol_ctxt card_assigns T
474 val concrete = xs |> maps (binder_types o snd) |> maps binder_types
475 |> forall (has_exact_card hol_ctxt card_assigns)
477 fun sum_dom_cards max =
478 map (domain_card max card_assigns o snd) xs |> Integer.sum
480 fold_rev (add_constr_spec desc co card sum_dom_cards num_self_recs
482 (sort (bool_ord o swap o pairself fst) (self_recs ~~ xs)) []
484 {typ = T, card = card, co = co, complete = complete, concrete = concrete,
485 deep = deep, constrs = constrs}
489 fun min_bits_for_nat_value n = if n <= 0 then 0 else IntInf.log2 n + 1
490 (* scope_desc -> int *)
491 fun min_bits_for_max_assigns (_, []) = 0
492 | min_bits_for_max_assigns (card_assigns, max_assigns) =
493 min_bits_for_nat_value (fold Integer.max
494 (map snd card_assigns @ map snd max_assigns) 0)
496 (* hol_context -> int -> typ list -> scope_desc -> scope *)
497 fun scope_from_descriptor (hol_ctxt as {thy, ...}) sym_break deep_dataTs
498 (desc as (card_assigns, _)) =
501 map (datatype_spec_from_scope_descriptor hol_ctxt deep_dataTs desc)
502 (filter (is_datatype thy o fst) card_assigns)
503 val bits = card_of_type card_assigns @{typ signed_bit} - 1
504 handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
505 card_of_type card_assigns @{typ unsigned_bit}
506 handle TYPE ("Nitpick_HOL.card_of_type", _, _) => 0
507 val bisim_depth = card_of_type card_assigns @{typ bisim_iterator} - 1
509 {hol_ctxt = hol_ctxt, card_assigns = card_assigns, datatypes = datatypes,
510 bits = bits, bisim_depth = bisim_depth,
511 ofs = if sym_break <= 0 then Typtab.empty
512 else offset_table_for_card_assigns thy card_assigns datatypes}
515 (* theory -> typ list -> (typ option * int list) list
516 -> (typ option * int list) list *)
517 fun repair_cards_assigns_wrt_boxing _ _ [] = []
518 | repair_cards_assigns_wrt_boxing thy Ts ((SOME T, ks) :: cards_assigns) =
519 (if is_fun_type T orelse is_pair_type T then
520 Ts |> filter (curry (type_match thy o swap) T o unbit_and_unbox_type)
521 |> map (rpair ks o SOME)
523 [(SOME T, ks)]) @ repair_cards_assigns_wrt_boxing thy Ts cards_assigns
524 | repair_cards_assigns_wrt_boxing thy Ts ((NONE, ks) :: cards_assigns) =
525 (NONE, ks) :: repair_cards_assigns_wrt_boxing thy Ts cards_assigns
527 val max_scopes = 4096
528 val distinct_threshold = 512
530 (* hol_context -> int -> (typ option * int list) list
531 -> (styp option * int list) list -> (styp option * int list) list -> int list
532 -> typ list -> typ list -> typ list -> int * scope list *)
533 fun all_scopes (hol_ctxt as {thy, ...}) sym_break cards_assigns maxes_assigns
534 iters_assigns bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs =
536 val cards_assigns = repair_cards_assigns_wrt_boxing thy mono_Ts
538 val blocks = blocks_for_types hol_ctxt cards_assigns maxes_assigns
539 iters_assigns bitss bisim_depths mono_Ts
541 val ranks = map rank_of_block blocks
542 val all = all_combinations_ordered_smartly (map (rpair 0) ranks)
543 val head = take max_scopes all
544 val descs = map_filter (scope_descriptor_from_combination hol_ctxt blocks)
547 (length all - length head,
548 descs |> length descs <= distinct_threshold ? distinct (op =)
549 |> map (scope_from_descriptor hol_ctxt sym_break deep_dataTs))