equal
deleted
inserted
replaced
47 val pretties_for_scope : scope -> bool -> Pretty.T list |
47 val pretties_for_scope : scope -> bool -> Pretty.T list |
48 val multiline_string_for_scope : scope -> string |
48 val multiline_string_for_scope : scope -> string |
49 val scopes_equivalent : scope * scope -> bool |
49 val scopes_equivalent : scope * scope -> bool |
50 val scope_less_eq : scope -> scope -> bool |
50 val scope_less_eq : scope -> scope -> bool |
51 val all_scopes : |
51 val all_scopes : |
52 hol_context -> bool -> int -> (typ option * int list) list |
52 hol_context -> bool -> (typ option * int list) list |
53 -> (styp option * int list) list -> (styp option * int list) list |
53 -> (styp option * int list) list -> (styp option * int list) list |
54 -> int list -> int list -> typ list -> typ list -> typ list -> typ list |
54 -> int list -> int list -> typ list -> typ list -> typ list -> typ list |
55 -> int * scope list |
55 -> int * scope list |
56 end; |
56 end; |
57 |
57 |
456 in |
456 in |
457 {typ = T, card = card, co = co, standard = standard, complete = complete, |
457 {typ = T, card = card, co = co, standard = standard, complete = complete, |
458 concrete = concrete, deep = deep, constrs = constrs} |
458 concrete = concrete, deep = deep, constrs = constrs} |
459 end |
459 end |
460 |
460 |
461 fun scope_from_descriptor (hol_ctxt as {thy, stds, ...}) binarize sym_break |
461 fun scope_from_descriptor (hol_ctxt as {thy, stds, ...}) binarize deep_dataTs |
462 deep_dataTs finitizable_dataTs |
462 finitizable_dataTs (desc as (card_assigns, _)) = |
463 (desc as (card_assigns, _)) = |
|
464 let |
463 let |
465 val datatypes = |
464 val datatypes = |
466 map (datatype_spec_from_scope_descriptor hol_ctxt binarize deep_dataTs |
465 map (datatype_spec_from_scope_descriptor hol_ctxt binarize deep_dataTs |
467 finitizable_dataTs desc) |
466 finitizable_dataTs desc) |
468 (filter (is_datatype thy stds o fst) card_assigns) |
467 (filter (is_datatype thy stds o fst) card_assigns) |
472 handle TYPE ("Nitpick_HOL.card_of_type", _, _) => 0 |
471 handle TYPE ("Nitpick_HOL.card_of_type", _, _) => 0 |
473 val bisim_depth = card_of_type card_assigns @{typ bisim_iterator} - 1 |
472 val bisim_depth = card_of_type card_assigns @{typ bisim_iterator} - 1 |
474 in |
473 in |
475 {hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns, |
474 {hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns, |
476 datatypes = datatypes, bits = bits, bisim_depth = bisim_depth, |
475 datatypes = datatypes, bits = bits, bisim_depth = bisim_depth, |
477 ofs = if sym_break <= 0 then Typtab.empty |
476 ofs = offset_table_for_card_assigns card_assigns datatypes} |
478 else offset_table_for_card_assigns card_assigns datatypes} |
|
479 end |
477 end |
480 |
478 |
481 fun repair_cards_assigns_wrt_boxing_etc _ _ [] = [] |
479 fun repair_cards_assigns_wrt_boxing_etc _ _ [] = [] |
482 | repair_cards_assigns_wrt_boxing_etc thy Ts ((SOME T, ks) :: cards_assigns) = |
480 | repair_cards_assigns_wrt_boxing_etc thy Ts ((SOME T, ks) :: cards_assigns) = |
483 (if is_fun_type T orelse is_pair_type T then |
481 (if is_fun_type T orelse is_pair_type T then |
489 (NONE, ks) :: repair_cards_assigns_wrt_boxing_etc thy Ts cards_assigns |
487 (NONE, ks) :: repair_cards_assigns_wrt_boxing_etc thy Ts cards_assigns |
490 |
488 |
491 val max_scopes = 4096 |
489 val max_scopes = 4096 |
492 val distinct_threshold = 512 |
490 val distinct_threshold = 512 |
493 |
491 |
494 fun all_scopes (hol_ctxt as {thy, ...}) binarize sym_break cards_assigns |
492 fun all_scopes (hol_ctxt as {thy, ...}) binarize cards_assigns maxes_assigns |
495 maxes_assigns iters_assigns bitss bisim_depths mono_Ts nonmono_Ts |
493 iters_assigns bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs |
496 deep_dataTs finitizable_dataTs = |
494 finitizable_dataTs = |
497 let |
495 let |
498 val cards_assigns = repair_cards_assigns_wrt_boxing_etc thy mono_Ts |
496 val cards_assigns = repair_cards_assigns_wrt_boxing_etc thy mono_Ts |
499 cards_assigns |
497 cards_assigns |
500 val blocks = blocks_for_types hol_ctxt binarize cards_assigns maxes_assigns |
498 val blocks = blocks_for_types hol_ctxt binarize cards_assigns maxes_assigns |
501 iters_assigns bitss bisim_depths mono_Ts |
499 iters_assigns bitss bisim_depths mono_Ts |
507 map_filter (scope_descriptor_from_combination hol_ctxt binarize blocks) |
505 map_filter (scope_descriptor_from_combination hol_ctxt binarize blocks) |
508 head |
506 head |
509 in |
507 in |
510 (length all - length head, |
508 (length all - length head, |
511 descs |> length descs <= distinct_threshold ? distinct (op =) |
509 descs |> length descs <= distinct_threshold ? distinct (op =) |
512 |> map (scope_from_descriptor hol_ctxt binarize sym_break |
510 |> map (scope_from_descriptor hol_ctxt binarize deep_dataTs |
513 deep_dataTs finitizable_dataTs)) |
511 finitizable_dataTs)) |
514 end |
512 end |
515 |
513 |
516 end; |
514 end; |