202 fun project_row column (y, ks) = (y, [nth ks (Int.min (column, length ks - 1))]) |
208 fun project_row column (y, ks) = (y, [nth ks (Int.min (column, length ks - 1))]) |
203 (* int -> block -> block *) |
209 (* int -> block -> block *) |
204 fun project_block (column, block) = map (project_row column) block |
210 fun project_block (column, block) = map (project_row column) block |
205 |
211 |
206 (* (''a * ''a -> bool) -> (''a option * int list) list -> ''a -> int list *) |
212 (* (''a * ''a -> bool) -> (''a option * int list) list -> ''a -> int list *) |
207 fun lookup_ints_assign eq asgns key = |
213 fun lookup_ints_assign eq assigns key = |
208 case triple_lookup eq asgns key of |
214 case triple_lookup eq assigns key of |
209 SOME ks => ks |
215 SOME ks => ks |
210 | NONE => raise ARG ("Nitpick_Scope.lookup_ints_assign", "") |
216 | NONE => raise ARG ("Nitpick_Scope.lookup_ints_assign", "") |
211 (* theory -> (typ option * int list) list -> typ -> int list *) |
217 (* theory -> (typ option * int list) list -> typ -> int list *) |
212 fun lookup_type_ints_assign thy asgns T = |
218 fun lookup_type_ints_assign thy assigns T = |
213 map (curry Int.max 1) (lookup_ints_assign (type_match thy) asgns T) |
219 map (curry Int.max 1) (lookup_ints_assign (type_match thy) assigns T) |
214 handle ARG ("Nitpick_Scope.lookup_ints_assign", _) => |
220 handle ARG ("Nitpick_Scope.lookup_ints_assign", _) => |
215 raise TYPE ("Nitpick_Scope.lookup_type_ints_assign", [T], []) |
221 raise TYPE ("Nitpick_Scope.lookup_type_ints_assign", [T], []) |
216 (* theory -> (styp option * int list) list -> styp -> int list *) |
222 (* theory -> (styp option * int list) list -> styp -> int list *) |
217 fun lookup_const_ints_assign thy asgns x = |
223 fun lookup_const_ints_assign thy assigns x = |
218 lookup_ints_assign (const_match thy) asgns x |
224 lookup_ints_assign (const_match thy) assigns x |
219 handle ARG ("Nitpick_Scope.lookup_ints_assign", _) => |
225 handle ARG ("Nitpick_Scope.lookup_ints_assign", _) => |
220 raise TERM ("Nitpick_Scope.lookup_const_ints_assign", [Const x]) |
226 raise TERM ("Nitpick_Scope.lookup_const_ints_assign", [Const x]) |
221 |
227 |
222 (* theory -> (styp option * int list) list -> styp -> row option *) |
228 (* theory -> (styp option * int list) list -> styp -> row option *) |
223 fun row_for_constr thy maxes_asgns constr = |
229 fun row_for_constr thy maxes_assigns constr = |
224 SOME (Max constr, lookup_const_ints_assign thy maxes_asgns constr) |
230 SOME (Max constr, lookup_const_ints_assign thy maxes_assigns constr) |
225 handle TERM ("lookup_const_ints_assign", _) => NONE |
231 handle TERM ("lookup_const_ints_assign", _) => NONE |
226 |
232 |
227 (* extended_context -> (typ option * int list) list |
233 (* extended_context -> (typ option * int list) list |
228 -> (styp option * int list) list -> (styp option * int list) list -> int list |
234 -> (styp option * int list) list -> (styp option * int list) list -> int list |
229 -> typ -> block *) |
235 -> typ -> block *) |
230 fun block_for_type (ext_ctxt as {thy, ...}) cards_asgns maxes_asgns iters_asgns |
236 fun block_for_type (ext_ctxt as {thy, ...}) cards_assigns maxes_assigns |
231 bisim_depths T = |
237 iters_assigns bisim_depths T = |
232 if T = @{typ bisim_iterator} then |
238 if T = @{typ bisim_iterator} then |
233 [(Card T, map (fn k => Int.max (0, k) + 1) bisim_depths)] |
239 [(Card T, map (fn k => Int.max (0, k) + 1) bisim_depths)] |
234 else if is_fp_iterator_type T then |
240 else if is_fp_iterator_type T then |
235 [(Card T, map (fn k => Int.max (0, k) + 1) |
241 [(Card T, map (fn k => Int.max (0, k) + 1) |
236 (lookup_const_ints_assign thy iters_asgns |
242 (lookup_const_ints_assign thy iters_assigns |
237 (const_for_iterator_type T)))] |
243 (const_for_iterator_type T)))] |
238 else |
244 else |
239 (Card T, lookup_type_ints_assign thy cards_asgns T) :: |
245 (Card T, lookup_type_ints_assign thy cards_assigns T) :: |
240 (case datatype_constrs ext_ctxt T of |
246 (case datatype_constrs ext_ctxt T of |
241 [_] => [] |
247 [_] => [] |
242 | constrs => map_filter (row_for_constr thy maxes_asgns) constrs) |
248 | constrs => map_filter (row_for_constr thy maxes_assigns) constrs) |
243 |
249 |
244 (* extended_context -> (typ option * int list) list |
250 (* extended_context -> (typ option * int list) list |
245 -> (styp option * int list) list -> (styp option * int list) list -> int list |
251 -> (styp option * int list) list -> (styp option * int list) list -> int list |
246 -> typ list -> typ list -> block list *) |
252 -> typ list -> typ list -> block list *) |
247 fun blocks_for_types ext_ctxt cards_asgns maxes_asgns iters_asgns bisim_depths |
253 fun blocks_for_types ext_ctxt cards_assigns maxes_assigns iters_assigns |
248 mono_Ts nonmono_Ts = |
254 bisim_depths mono_Ts nonmono_Ts = |
249 let |
255 let |
250 (* typ -> block *) |
256 (* typ -> block *) |
251 val block_for = block_for_type ext_ctxt cards_asgns maxes_asgns iters_asgns |
257 val block_for = block_for_type ext_ctxt cards_assigns maxes_assigns |
252 bisim_depths |
258 iters_assigns bisim_depths |
253 val mono_block = maps block_for mono_Ts |
259 val mono_block = maps block_for mono_Ts |
254 val nonmono_blocks = map block_for nonmono_Ts |
260 val nonmono_blocks = map block_for nonmono_Ts |
255 in mono_block :: nonmono_blocks end |
261 in mono_block :: nonmono_blocks end |
256 |
262 |
257 val sync_threshold = 5 |
263 val sync_threshold = 5 |
288 fun constr_max maxes x = the_default ~1 (AList.lookup (op =) maxes x) |
294 fun constr_max maxes x = the_default ~1 (AList.lookup (op =) maxes x) |
289 |
295 |
290 type scope_desc = (typ * int) list * (styp * int) list |
296 type scope_desc = (typ * int) list * (styp * int) list |
291 |
297 |
292 (* extended_context -> scope_desc -> typ * int -> bool *) |
298 (* extended_context -> scope_desc -> typ * int -> bool *) |
293 fun is_surely_inconsistent_card_assign ext_ctxt (card_asgns, max_asgns) (T, k) = |
299 fun is_surely_inconsistent_card_assign ext_ctxt (card_assigns, max_assigns) |
|
300 (T, k) = |
294 case datatype_constrs ext_ctxt T of |
301 case datatype_constrs ext_ctxt T of |
295 [] => false |
302 [] => false |
296 | xs => |
303 | xs => |
297 let |
304 let |
298 val precise_cards = |
305 val exact_cards = |
299 map (Integer.prod |
306 map (Integer.prod |
300 o map (bounded_precise_card_of_type ext_ctxt k 0 card_asgns) |
307 o map (bounded_exact_card_of_type ext_ctxt k 0 card_assigns) |
301 o binder_types o snd) xs |
308 o binder_types o snd) xs |
302 val maxes = map (constr_max max_asgns) xs |
309 val maxes = map (constr_max max_assigns) xs |
303 (* int -> int -> int *) |
310 (* int -> int -> int *) |
304 fun effective_max 0 ~1 = k |
311 fun effective_max 0 ~1 = k |
305 | effective_max 0 max = max |
312 | effective_max 0 max = max |
306 | effective_max card ~1 = card |
313 | effective_max card ~1 = card |
307 | effective_max card max = Int.min (card, max) |
314 | effective_max card max = Int.min (card, max) |
308 val max = map2 effective_max precise_cards maxes |> Integer.sum |
315 val max = map2 effective_max exact_cards maxes |> Integer.sum |
309 (* unit -> int *) |
316 (* unit -> int *) |
310 fun doms_card () = |
317 fun doms_card () = |
311 xs |> map (Integer.prod o map (bounded_card_of_type k ~1 card_asgns) |
318 xs |> map (Integer.prod o map (bounded_card_of_type k ~1 card_assigns) |
312 o binder_types o snd) |
319 o binder_types o snd) |
313 |> Integer.sum |
320 |> Integer.sum |
314 in |
321 in |
315 max < k |
322 max < k |
316 orelse (forall (not_equal 0) precise_cards andalso doms_card () < k) |
323 orelse (forall (not_equal 0) exact_cards andalso doms_card () < k) |
317 end |
324 end |
318 handle TYPE ("Nitpick_HOL.card_of_type", _, _) => false |
325 handle TYPE ("Nitpick_HOL.card_of_type", _, _) => false |
319 |
326 |
320 (* extended_context -> scope_desc -> bool *) |
327 (* extended_context -> scope_desc -> bool *) |
321 fun is_surely_inconsistent_scope_description ext_ctxt |
328 fun is_surely_inconsistent_scope_description ext_ctxt |
322 (desc as (card_asgns, _)) = |
329 (desc as (card_assigns, _)) = |
323 exists (is_surely_inconsistent_card_assign ext_ctxt desc) card_asgns |
330 exists (is_surely_inconsistent_card_assign ext_ctxt desc) card_assigns |
324 |
331 |
325 (* extended_context -> scope_desc -> (typ * int) list option *) |
332 (* extended_context -> scope_desc -> (typ * int) list option *) |
326 fun repair_card_assigns ext_ctxt (card_asgns, max_asgns) = |
333 fun repair_card_assigns ext_ctxt (card_assigns, max_assigns) = |
327 let |
334 let |
328 (* (typ * int) list -> (typ * int) list -> (typ * int) list option *) |
335 (* (typ * int) list -> (typ * int) list -> (typ * int) list option *) |
329 fun aux seen [] = SOME seen |
336 fun aux seen [] = SOME seen |
330 | aux seen ((T, 0) :: _) = NONE |
337 | aux seen ((T, 0) :: _) = NONE |
331 | aux seen ((T, k) :: asgns) = |
338 | aux seen ((T, k) :: assigns) = |
332 (if is_surely_inconsistent_scope_description ext_ctxt |
339 (if is_surely_inconsistent_scope_description ext_ctxt |
333 ((T, k) :: seen, max_asgns) then |
340 ((T, k) :: seen, max_assigns) then |
334 raise SAME () |
341 raise SAME () |
335 else |
342 else |
336 case aux ((T, k) :: seen) asgns of |
343 case aux ((T, k) :: seen) assigns of |
337 SOME asgns => SOME asgns |
344 SOME assigns => SOME assigns |
338 | NONE => raise SAME ()) |
345 | NONE => raise SAME ()) |
339 handle SAME () => aux seen ((T, k - 1) :: asgns) |
346 handle SAME () => aux seen ((T, k - 1) :: assigns) |
340 in aux [] (rev card_asgns) end |
347 in aux [] (rev card_assigns) end |
341 |
348 |
342 (* theory -> (typ * int) list -> typ * int -> typ * int *) |
349 (* theory -> (typ * int) list -> typ * int -> typ * int *) |
343 fun repair_iterator_assign thy asgns (T as Type (s, Ts), k) = |
350 fun repair_iterator_assign thy assigns (T as Type (s, Ts), k) = |
344 (T, if T = @{typ bisim_iterator} then |
351 (T, if T = @{typ bisim_iterator} then |
345 let val co_cards = map snd (filter (is_codatatype thy o fst) asgns) in |
352 let |
346 Int.min (k, Integer.sum co_cards) |
353 val co_cards = map snd (filter (is_codatatype thy o fst) assigns) |
347 end |
354 in Int.min (k, Integer.sum co_cards) end |
348 else if is_fp_iterator_type T then |
355 else if is_fp_iterator_type T then |
349 case Ts of |
356 case Ts of |
350 [] => 1 |
357 [] => 1 |
351 | _ => bounded_card_of_type k ~1 asgns (foldr1 HOLogic.mk_prodT Ts) |
358 | _ => bounded_card_of_type k ~1 assigns (foldr1 HOLogic.mk_prodT Ts) |
352 else |
359 else |
353 k) |
360 k) |
354 | repair_iterator_assign _ _ asgn = asgn |
361 | repair_iterator_assign _ _ assign = assign |
355 |
362 |
356 (* row -> scope_desc -> scope_desc *) |
363 (* row -> scope_desc -> scope_desc *) |
357 fun add_row_to_scope_descriptor (kind, ks) (card_asgns, max_asgns) = |
364 fun add_row_to_scope_descriptor (kind, ks) (card_assigns, max_assigns) = |
358 case kind of |
365 case kind of |
359 Card T => ((T, the_single ks) :: card_asgns, max_asgns) |
366 Card T => ((T, the_single ks) :: card_assigns, max_assigns) |
360 | Max x => (card_asgns, (x, the_single ks) :: max_asgns) |
367 | Max x => (card_assigns, (x, the_single ks) :: max_assigns) |
361 (* block -> scope_desc *) |
368 (* block -> scope_desc *) |
362 fun scope_descriptor_from_block block = |
369 fun scope_descriptor_from_block block = |
363 fold_rev add_row_to_scope_descriptor block ([], []) |
370 fold_rev add_row_to_scope_descriptor block ([], []) |
364 (* extended_context -> block list -> int list -> scope_desc option *) |
371 (* extended_context -> block list -> int list -> scope_desc option *) |
365 fun scope_descriptor_from_combination (ext_ctxt as {thy, ...}) blocks columns = |
372 fun scope_descriptor_from_combination (ext_ctxt as {thy, ...}) blocks columns = |
366 let |
373 let |
367 val (card_asgns, max_asgns) = |
374 val (card_assigns, max_assigns) = |
368 maps project_block (columns ~~ blocks) |> scope_descriptor_from_block |
375 maps project_block (columns ~~ blocks) |> scope_descriptor_from_block |
369 val card_asgns = repair_card_assigns ext_ctxt (card_asgns, max_asgns) |> the |
376 val card_assigns = repair_card_assigns ext_ctxt (card_assigns, max_assigns) |
370 in |
377 |> the |
371 SOME (map (repair_iterator_assign thy card_asgns) card_asgns, max_asgns) |
378 in |
|
379 SOME (map (repair_iterator_assign thy card_assigns) card_assigns, |
|
380 max_assigns) |
372 end |
381 end |
373 handle Option.Option => NONE |
382 handle Option.Option => NONE |
374 |
383 |
375 (* theory -> (typ * int) list -> dtype_spec list -> int Typtab.table *) |
384 (* theory -> (typ * int) list -> dtype_spec list -> int Typtab.table *) |
376 fun offset_table_for_card_assigns thy asgns dtypes = |
385 fun offset_table_for_card_assigns thy assigns dtypes = |
377 let |
386 let |
378 (* int -> (int * int) list -> (typ * int) list -> int Typtab.table |
387 (* int -> (int * int) list -> (typ * int) list -> int Typtab.table |
379 -> int Typtab.table *) |
388 -> int Typtab.table *) |
380 fun aux next _ [] = Typtab.update_new (dummyT, next) |
389 fun aux next _ [] = Typtab.update_new (dummyT, next) |
381 | aux next reusable ((T, k) :: asgns) = |
390 | aux next reusable ((T, k) :: assigns) = |
382 if k = 1 orelse is_integer_type T then |
391 if k = 1 orelse is_integer_type T then |
383 aux next reusable asgns |
392 aux next reusable assigns |
384 else if length (these (Option.map #constrs (datatype_spec dtypes T))) |
393 else if length (these (Option.map #constrs (datatype_spec dtypes T))) |
385 > 1 then |
394 > 1 then |
386 Typtab.update_new (T, next) #> aux (next + k) reusable asgns |
395 Typtab.update_new (T, next) #> aux (next + k) reusable assigns |
387 else |
396 else |
388 case AList.lookup (op =) reusable k of |
397 case AList.lookup (op =) reusable k of |
389 SOME j0 => Typtab.update_new (T, j0) #> aux next reusable asgns |
398 SOME j0 => Typtab.update_new (T, j0) #> aux next reusable assigns |
390 | NONE => Typtab.update_new (T, next) |
399 | NONE => Typtab.update_new (T, next) |
391 #> aux (next + k) ((k, next) :: reusable) asgns |
400 #> aux (next + k) ((k, next) :: reusable) assigns |
392 in aux 0 [] asgns Typtab.empty end |
401 in aux 0 [] assigns Typtab.empty end |
393 |
402 |
394 (* int -> (typ * int) list -> typ -> int *) |
403 (* int -> (typ * int) list -> typ -> int *) |
395 fun domain_card max card_asgns = |
404 fun domain_card max card_assigns = |
396 Integer.prod o map (bounded_card_of_type max max card_asgns) o binder_types |
405 Integer.prod o map (bounded_card_of_type max max card_assigns) o binder_types |
397 |
406 |
398 (* scope_desc -> bool -> int -> (int -> int) -> int -> int -> bool * styp |
407 (* scope_desc -> bool -> int -> (int -> int) -> int -> int -> bool * styp |
399 -> constr_spec list -> constr_spec list *) |
408 -> constr_spec list -> constr_spec list *) |
400 fun add_constr_spec (card_asgns, max_asgns) co card sum_dom_cards num_self_recs |
409 fun add_constr_spec (card_assigns, max_assigns) co card sum_dom_cards |
401 num_non_self_recs (self_rec, x as (s, T)) constrs = |
410 num_self_recs num_non_self_recs (self_rec, x as (s, T)) |
402 let |
411 constrs = |
403 val max = constr_max max_asgns x |
412 let |
|
413 val max = constr_max max_assigns x |
404 (* int -> int *) |
414 (* int -> int *) |
405 fun bound k = Int.min (card, (max >= 0 ? curry Int.min max) k) |
415 fun bound k = Int.min (card, (max >= 0 ? curry Int.min max) k) |
406 (* unit -> int *) |
416 (* unit -> int *) |
407 fun next_delta () = if null constrs then 0 else #epsilon (hd constrs) |
417 fun next_delta () = if null constrs then 0 else #epsilon (hd constrs) |
408 val {delta, epsilon, exclusive, total} = |
418 val {delta, epsilon, exclusive, total} = |
410 let val delta = next_delta () in |
420 let val delta = next_delta () in |
411 {delta = delta, epsilon = delta, exclusive = true, total = false} |
421 {delta = delta, epsilon = delta, exclusive = true, total = false} |
412 end |
422 end |
413 else if not co andalso num_self_recs > 0 then |
423 else if not co andalso num_self_recs > 0 then |
414 if not self_rec andalso num_non_self_recs = 1 |
424 if not self_rec andalso num_non_self_recs = 1 |
415 andalso domain_card 2 card_asgns T = 1 then |
425 andalso domain_card 2 card_assigns T = 1 then |
416 {delta = 0, epsilon = 1, exclusive = (s = @{const_name Nil}), |
426 {delta = 0, epsilon = 1, exclusive = (s = @{const_name Nil}), |
417 total = true} |
427 total = true} |
418 else if s = @{const_name Cons} then |
428 else if s = @{const_name Cons} then |
419 {delta = 1, epsilon = card, exclusive = true, total = false} |
429 {delta = 1, epsilon = card, exclusive = true, total = false} |
420 else |
430 else |
421 {delta = 0, epsilon = card, exclusive = false, total = false} |
431 {delta = 0, epsilon = card, exclusive = false, total = false} |
422 else if card = sum_dom_cards (card + 1) then |
432 else if card = sum_dom_cards (card + 1) then |
423 let val delta = next_delta () in |
433 let val delta = next_delta () in |
424 {delta = delta, epsilon = delta + domain_card card card_asgns T, |
434 {delta = delta, epsilon = delta + domain_card card card_assigns T, |
425 exclusive = true, total = true} |
435 exclusive = true, total = true} |
426 end |
436 end |
427 else |
437 else |
428 {delta = 0, epsilon = card, |
438 {delta = 0, epsilon = card, |
429 exclusive = (num_self_recs + num_non_self_recs = 1), total = false} |
439 exclusive = (num_self_recs + num_non_self_recs = 1), total = false} |
430 in |
440 in |
431 {const = x, delta = delta, epsilon = epsilon, exclusive = exclusive, |
441 {const = x, delta = delta, epsilon = epsilon, exclusive = exclusive, |
432 explicit_max = max, total = total} :: constrs |
442 explicit_max = max, total = total} :: constrs |
433 end |
443 end |
434 |
444 |
|
445 (* extended_context -> (typ * int) list -> typ -> bool *) |
|
446 fun has_exact_card ext_ctxt card_assigns T = |
|
447 let val card = card_of_type card_assigns T in |
|
448 card = bounded_exact_card_of_type ext_ctxt (card + 1) 0 card_assigns T |
|
449 end |
|
450 |
435 (* extended_context -> typ list -> scope_desc -> typ * int -> dtype_spec *) |
451 (* extended_context -> typ list -> scope_desc -> typ * int -> dtype_spec *) |
436 fun datatype_spec_from_scope_descriptor (ext_ctxt as {thy, ...}) shallow_dataTs |
452 fun datatype_spec_from_scope_descriptor (ext_ctxt as {thy, ...}) shallow_dataTs |
437 (desc as (card_asgns, _)) (T, card) = |
453 (desc as (card_assigns, _)) (T, card) = |
438 let |
454 let |
439 val shallow = member (op =) shallow_dataTs T |
455 val shallow = member (op =) shallow_dataTs T |
440 val co = is_codatatype thy T |
456 val co = is_codatatype thy T |
441 val xs = boxed_datatype_constrs ext_ctxt T |
457 val xs = boxed_datatype_constrs ext_ctxt T |
442 val self_recs = map (is_self_recursive_constr_type o snd) xs |
458 val self_recs = map (is_self_recursive_constr_type o snd) xs |
443 val (num_self_recs, num_non_self_recs) = |
459 val (num_self_recs, num_non_self_recs) = |
444 List.partition (curry (op =) true) self_recs |> pairself length |
460 List.partition I self_recs |> pairself length |
445 val precise = (card = bounded_precise_card_of_type ext_ctxt (card + 1) 0 |
461 val complete = has_exact_card ext_ctxt card_assigns T |
446 card_asgns T) |
462 val concrete = xs |> maps (binder_types o snd) |> maps binder_types |
|
463 |> forall (has_exact_card ext_ctxt card_assigns) |
447 (* int -> int *) |
464 (* int -> int *) |
448 fun sum_dom_cards max = |
465 fun sum_dom_cards max = |
449 map (domain_card max card_asgns o snd) xs |> Integer.sum |
466 map (domain_card max card_assigns o snd) xs |> Integer.sum |
450 val constrs = |
467 val constrs = |
451 fold_rev (add_constr_spec desc co card sum_dom_cards num_self_recs |
468 fold_rev (add_constr_spec desc co card sum_dom_cards num_self_recs |
452 num_non_self_recs) (self_recs ~~ xs) [] |
469 num_non_self_recs) (self_recs ~~ xs) [] |
453 in |
470 in |
454 {typ = T, card = card, co = co, precise = precise, shallow = shallow, |
471 {typ = T, card = card, co = co, complete = complete, concrete = concrete, |
455 constrs = constrs} |
472 shallow = shallow, constrs = constrs} |
456 end |
473 end |
457 |
474 |
458 (* extended_context -> int -> typ list -> scope_desc -> scope *) |
475 (* extended_context -> int -> typ list -> scope_desc -> scope *) |
459 fun scope_from_descriptor (ext_ctxt as {thy, ...}) sym_break shallow_dataTs |
476 fun scope_from_descriptor (ext_ctxt as {thy, ...}) sym_break shallow_dataTs |
460 (desc as (card_asgns, _)) = |
477 (desc as (card_assigns, _)) = |
461 let |
478 let |
462 val datatypes = |
479 val datatypes = |
463 map (datatype_spec_from_scope_descriptor ext_ctxt shallow_dataTs desc) |
480 map (datatype_spec_from_scope_descriptor ext_ctxt shallow_dataTs desc) |
464 (filter (is_datatype thy o fst) card_asgns) |
481 (filter (is_datatype thy o fst) card_assigns) |
465 val bisim_depth = card_of_type card_asgns @{typ bisim_iterator} - 1 |
482 val bisim_depth = card_of_type card_assigns @{typ bisim_iterator} - 1 |
466 in |
483 in |
467 {ext_ctxt = ext_ctxt, card_assigns = card_asgns, datatypes = datatypes, |
484 {ext_ctxt = ext_ctxt, card_assigns = card_assigns, datatypes = datatypes, |
468 bisim_depth = bisim_depth, |
485 bisim_depth = bisim_depth, |
469 ofs = if sym_break <= 0 then Typtab.empty |
486 ofs = if sym_break <= 0 then Typtab.empty |
470 else offset_table_for_card_assigns thy card_asgns datatypes} |
487 else offset_table_for_card_assigns thy card_assigns datatypes} |
471 end |
488 end |
472 |
489 |
473 (* theory -> typ list -> (typ option * int list) list |
490 (* theory -> typ list -> (typ option * int list) list |
474 -> (typ option * int list) list *) |
491 -> (typ option * int list) list *) |
475 fun fix_cards_assigns_wrt_boxing _ _ [] = [] |
492 fun fix_cards_assigns_wrt_boxing _ _ [] = [] |
476 | fix_cards_assigns_wrt_boxing thy Ts ((SOME T, ks) :: cards_asgns) = |
493 | fix_cards_assigns_wrt_boxing thy Ts ((SOME T, ks) :: cards_assigns) = |
477 (if is_fun_type T orelse is_pair_type T then |
494 (if is_fun_type T orelse is_pair_type T then |
478 Ts |> filter (curry (type_match thy o swap) T o unbox_type) |
495 Ts |> filter (curry (type_match thy o swap) T o unbox_type) |
479 |> map (rpair ks o SOME) |
496 |> map (rpair ks o SOME) |
480 else |
497 else |
481 [(SOME T, ks)]) @ fix_cards_assigns_wrt_boxing thy Ts cards_asgns |
498 [(SOME T, ks)]) @ fix_cards_assigns_wrt_boxing thy Ts cards_assigns |
482 | fix_cards_assigns_wrt_boxing thy Ts ((NONE, ks) :: cards_asgns) = |
499 | fix_cards_assigns_wrt_boxing thy Ts ((NONE, ks) :: cards_assigns) = |
483 (NONE, ks) :: fix_cards_assigns_wrt_boxing thy Ts cards_asgns |
500 (NONE, ks) :: fix_cards_assigns_wrt_boxing thy Ts cards_assigns |
484 |
501 |
485 val max_scopes = 4096 |
502 val max_scopes = 4096 |
486 val distinct_threshold = 512 |
503 val distinct_threshold = 512 |
487 |
504 |
488 (* extended_context -> int -> (typ option * int list) list |
505 (* extended_context -> int -> (typ option * int list) list |
489 -> (styp option * int list) list -> (styp option * int list) list -> int list |
506 -> (styp option * int list) list -> (styp option * int list) list -> int list |
490 -> typ list -> typ list -> typ list -> int * scope list *) |
507 -> typ list -> typ list -> typ list -> int * scope list *) |
491 fun all_scopes (ext_ctxt as {thy, ...}) sym_break cards_asgns maxes_asgns |
508 fun all_scopes (ext_ctxt as {thy, ...}) sym_break cards_assigns maxes_assigns |
492 iters_asgns bisim_depths mono_Ts nonmono_Ts shallow_dataTs = |
509 iters_assigns bisim_depths mono_Ts nonmono_Ts shallow_dataTs = |
493 let |
510 let |
494 val cards_asgns = fix_cards_assigns_wrt_boxing thy mono_Ts cards_asgns |
511 val cards_assigns = fix_cards_assigns_wrt_boxing thy mono_Ts cards_assigns |
495 val blocks = blocks_for_types ext_ctxt cards_asgns maxes_asgns iters_asgns |
512 val blocks = blocks_for_types ext_ctxt cards_assigns maxes_assigns |
496 bisim_depths mono_Ts nonmono_Ts |
513 iters_assigns bisim_depths mono_Ts nonmono_Ts |
497 val ranks = map rank_of_block blocks |
514 val ranks = map rank_of_block blocks |
498 val all = all_combinations_ordered_smartly (map (rpair 0) ranks) |
515 val all = all_combinations_ordered_smartly (map (rpair 0) ranks) |
499 val head = take max_scopes all |
516 val head = take max_scopes all |
500 val descs = map_filter (scope_descriptor_from_combination ext_ctxt blocks) |
517 val descs = map_filter (scope_descriptor_from_combination ext_ctxt blocks) |
501 head |
518 head |