src/HOL/Tools/Nitpick/nitpick_scope.ML
changeset 35190 ce653cc27a94
parent 35179 4b198af5beb5
child 35220 2bcdae5f4fdb
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Wed Feb 17 14:11:41 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Wed Feb 17 20:46:50 2010 +0100
     1.3 @@ -30,6 +30,7 @@
     1.4  
     1.5    type scope = {
     1.6      hol_ctxt: hol_context,
     1.7 +    binarize: bool,
     1.8      card_assigns: (typ * int) list,
     1.9      bits: int,
    1.10      bisim_depth: int,
    1.11 @@ -48,7 +49,7 @@
    1.12    val scopes_equivalent : scope -> scope -> bool
    1.13    val scope_less_eq : scope -> scope -> bool
    1.14    val all_scopes :
    1.15 -    hol_context -> int -> (typ option * int list) list
    1.16 +    hol_context -> bool -> int -> (typ option * int list) list
    1.17      -> (styp option * int list) list -> (styp option * int list) list
    1.18      -> int list -> int list -> typ list -> typ list -> typ list
    1.19      -> int * scope list
    1.20 @@ -80,6 +81,7 @@
    1.21  
    1.22  type scope = {
    1.23    hol_ctxt: hol_context,
    1.24 +  binarize: bool,
    1.25    card_assigns: (typ * int) list,
    1.26    bits: int,
    1.27    bisim_depth: int,
    1.28 @@ -242,9 +244,10 @@
    1.29  
    1.30  val max_bits = 31 (* Kodkod limit *)
    1.31  
    1.32 -(* hol_context -> (typ option * int list) list -> (styp option * int list) list
    1.33 -   -> (styp option * int list) list -> int list -> int list -> typ -> block *)
    1.34 -fun block_for_type (hol_ctxt as {thy, ...}) cards_assigns maxes_assigns
    1.35 +(* hol_context -> bool -> (typ option * int list) list
    1.36 +   -> (styp option * int list) list -> (styp option * int list) list -> int list
    1.37 +   -> int list -> typ -> block *)
    1.38 +fun block_for_type (hol_ctxt as {thy, ...}) binarize cards_assigns maxes_assigns
    1.39                     iters_assigns bitss bisim_depths T =
    1.40    if T = @{typ unsigned_bit} then
    1.41      [(Card T, map (Integer.min max_bits o Integer.max 1) bitss)]
    1.42 @@ -262,18 +265,18 @@
    1.43                                              (const_for_iterator_type T)))]
    1.44    else
    1.45      (Card T, lookup_type_ints_assign thy cards_assigns T) ::
    1.46 -    (case datatype_constrs hol_ctxt T of
    1.47 +    (case binarized_and_boxed_datatype_constrs hol_ctxt binarize T of
    1.48         [_] => []
    1.49       | constrs => map_filter (row_for_constr thy maxes_assigns) constrs)
    1.50  
    1.51 -(* hol_context -> (typ option * int list) list -> (styp option * int list) list
    1.52 -   -> (styp option * int list) list -> int list -> int list -> typ list
    1.53 -   -> typ list -> block list *)
    1.54 -fun blocks_for_types hol_ctxt cards_assigns maxes_assigns iters_assigns bitss
    1.55 -                     bisim_depths mono_Ts nonmono_Ts =
    1.56 +(* hol_context -> bool -> (typ option * int list) list
    1.57 +   -> (styp option * int list) list -> (styp option * int list) list -> int list
    1.58 +   -> int list -> typ list -> typ list -> block list *)
    1.59 +fun blocks_for_types hol_ctxt binarize cards_assigns maxes_assigns iters_assigns
    1.60 +                     bitss bisim_depths mono_Ts nonmono_Ts =
    1.61    let
    1.62      (* typ -> block *)
    1.63 -    val block_for = block_for_type hol_ctxt cards_assigns maxes_assigns
    1.64 +    val block_for = block_for_type hol_ctxt binarize cards_assigns maxes_assigns
    1.65                                     iters_assigns bitss bisim_depths
    1.66      val mono_block = maps block_for mono_Ts
    1.67      val nonmono_blocks = map block_for nonmono_Ts
    1.68 @@ -314,10 +317,10 @@
    1.69  
    1.70  type scope_desc = (typ * int) list * (styp * int) list
    1.71  
    1.72 -(* hol_context -> scope_desc -> typ * int -> bool *)
    1.73 -fun is_surely_inconsistent_card_assign hol_ctxt (card_assigns, max_assigns)
    1.74 -                                       (T, k) =
    1.75 -  case datatype_constrs hol_ctxt T of
    1.76 +(* hol_context -> bool -> scope_desc -> typ * int -> bool *)
    1.77 +fun is_surely_inconsistent_card_assign hol_ctxt binarize
    1.78 +                                       (card_assigns, max_assigns) (T, k) =
    1.79 +  case binarized_and_boxed_datatype_constrs hol_ctxt binarize T of
    1.80      [] => false
    1.81    | xs =>
    1.82      let
    1.83 @@ -330,21 +333,22 @@
    1.84          | effective_max card max = Int.min (card, max)
    1.85        val max = map2 effective_max dom_cards maxes |> Integer.sum
    1.86      in max < k end
    1.87 -(* hol_context -> (typ * int) list -> (typ * int) list -> (styp * int) list
    1.88 -   -> bool *)
    1.89 -fun is_surely_inconsistent_scope_description hol_ctxt seen rest max_assigns =
    1.90 -  exists (is_surely_inconsistent_card_assign hol_ctxt
    1.91 +(* hol_context -> bool -> (typ * int) list -> (typ * int) list
    1.92 +   -> (styp * int) list -> bool *)
    1.93 +fun is_surely_inconsistent_scope_description hol_ctxt binarize seen rest
    1.94 +                                             max_assigns =
    1.95 +  exists (is_surely_inconsistent_card_assign hol_ctxt binarize
    1.96                                               (seen @ rest, max_assigns)) seen
    1.97  
    1.98 -(* hol_context -> scope_desc -> (typ * int) list option *)
    1.99 -fun repair_card_assigns hol_ctxt (card_assigns, max_assigns) =
   1.100 +(* hol_context -> bool -> scope_desc -> (typ * int) list option *)
   1.101 +fun repair_card_assigns hol_ctxt binarize (card_assigns, max_assigns) =
   1.102    let
   1.103      (* (typ * int) list -> (typ * int) list -> (typ * int) list option *)
   1.104      fun aux seen [] = SOME seen
   1.105        | aux seen ((T, 0) :: _) = NONE
   1.106        | aux seen ((T, k) :: rest) =
   1.107 -        (if is_surely_inconsistent_scope_description hol_ctxt ((T, k) :: seen)
   1.108 -                                                     rest max_assigns then
   1.109 +        (if is_surely_inconsistent_scope_description hol_ctxt binarize
   1.110 +                ((T, k) :: seen) rest max_assigns then
   1.111             raise SAME ()
   1.112           else
   1.113             case aux ((T, k) :: seen) rest of
   1.114 @@ -375,13 +379,14 @@
   1.115  (* block -> scope_desc *)
   1.116  fun scope_descriptor_from_block block =
   1.117    fold_rev add_row_to_scope_descriptor block ([], [])
   1.118 -(* hol_context -> block list -> int list -> scope_desc option *)
   1.119 -fun scope_descriptor_from_combination (hol_ctxt as {thy, ...}) blocks columns =
   1.120 +(* hol_context -> bool -> block list -> int list -> scope_desc option *)
   1.121 +fun scope_descriptor_from_combination (hol_ctxt as {thy, ...}) binarize blocks
   1.122 +                                      columns =
   1.123    let
   1.124      val (card_assigns, max_assigns) =
   1.125        maps project_block (columns ~~ blocks) |> scope_descriptor_from_block
   1.126 -    val card_assigns = repair_card_assigns hol_ctxt (card_assigns, max_assigns)
   1.127 -                       |> the
   1.128 +    val card_assigns =
   1.129 +      repair_card_assigns hol_ctxt binarize (card_assigns, max_assigns) |> the
   1.130    in
   1.131      SOME (map (repair_iterator_assign thy card_assigns) card_assigns,
   1.132            max_assigns)
   1.133 @@ -462,14 +467,14 @@
   1.134      card = bounded_exact_card_of_type hol_ctxt (card + 1) 0 card_assigns T
   1.135    end
   1.136  
   1.137 -(* hol_context -> typ list -> scope_desc -> typ * int -> dtype_spec *)
   1.138 -fun datatype_spec_from_scope_descriptor (hol_ctxt as {thy, ...}) deep_dataTs
   1.139 -                                        (desc as (card_assigns, _)) (T, card) =
   1.140 +(* hol_context -> bool -> typ list -> scope_desc -> typ * int -> dtype_spec *)
   1.141 +fun datatype_spec_from_scope_descriptor (hol_ctxt as {thy, ...}) binarize
   1.142 +        deep_dataTs (desc as (card_assigns, _)) (T, card) =
   1.143    let
   1.144      val deep = member (op =) deep_dataTs T
   1.145      val co = is_codatatype thy T
   1.146      val standard = is_standard_datatype hol_ctxt T
   1.147 -    val xs = boxed_datatype_constrs hol_ctxt T
   1.148 +    val xs = binarized_and_boxed_datatype_constrs hol_ctxt binarize T
   1.149      val self_recs = map (is_self_recursive_constr_type o snd) xs
   1.150      val (num_self_recs, num_non_self_recs) =
   1.151        List.partition I self_recs |> pairself length
   1.152 @@ -496,21 +501,21 @@
   1.153      min_bits_for_nat_value (fold Integer.max
   1.154          (map snd card_assigns @ map snd max_assigns) 0)
   1.155  
   1.156 -(* hol_context -> int -> typ list -> scope_desc -> scope *)
   1.157 -fun scope_from_descriptor (hol_ctxt as {thy, ...}) sym_break deep_dataTs
   1.158 -                          (desc as (card_assigns, _)) =
   1.159 +(* hol_context -> bool -> int -> typ list -> scope_desc -> scope *)
   1.160 +fun scope_from_descriptor (hol_ctxt as {thy, ...}) binarize sym_break
   1.161 +                          deep_dataTs (desc as (card_assigns, _)) =
   1.162    let
   1.163      val datatypes =
   1.164 -      map (datatype_spec_from_scope_descriptor hol_ctxt deep_dataTs desc)
   1.165 -          (filter (is_datatype thy o fst) card_assigns)
   1.166 +      map (datatype_spec_from_scope_descriptor hol_ctxt binarize deep_dataTs
   1.167 +               desc) (filter (is_datatype thy o fst) card_assigns)
   1.168      val bits = card_of_type card_assigns @{typ signed_bit} - 1
   1.169                 handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
   1.170                        card_of_type card_assigns @{typ unsigned_bit}
   1.171                        handle TYPE ("Nitpick_HOL.card_of_type", _, _) => 0
   1.172      val bisim_depth = card_of_type card_assigns @{typ bisim_iterator} - 1
   1.173    in
   1.174 -    {hol_ctxt = hol_ctxt, card_assigns = card_assigns, datatypes = datatypes,
   1.175 -     bits = bits, bisim_depth = bisim_depth,
   1.176 +    {hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns,
   1.177 +     datatypes = datatypes, bits = bits, bisim_depth = bisim_depth,
   1.178       ofs = if sym_break <= 0 then Typtab.empty
   1.179             else offset_table_for_card_assigns thy card_assigns datatypes}
   1.180    end
   1.181 @@ -520,7 +525,7 @@
   1.182  fun repair_cards_assigns_wrt_boxing _ _ [] = []
   1.183    | repair_cards_assigns_wrt_boxing thy Ts ((SOME T, ks) :: cards_assigns) =
   1.184      (if is_fun_type T orelse is_pair_type T then
   1.185 -       Ts |> filter (curry (type_match thy o swap) T o unbit_and_unbox_type)
   1.186 +       Ts |> filter (curry (type_match thy o swap) T o unarize_and_unbox_type)
   1.187            |> map (rpair ks o SOME)
   1.188       else
   1.189         [(SOME T, ks)]) @ repair_cards_assigns_wrt_boxing thy Ts cards_assigns
   1.190 @@ -530,26 +535,29 @@
   1.191  val max_scopes = 4096
   1.192  val distinct_threshold = 512
   1.193  
   1.194 -(* hol_context -> int -> (typ option * int list) list
   1.195 +(* hol_context -> bool -> int -> (typ option * int list) list
   1.196     -> (styp option * int list) list -> (styp option * int list) list -> int list
   1.197     -> typ list -> typ list -> typ list -> int * scope list *)
   1.198 -fun all_scopes (hol_ctxt as {thy, ...}) sym_break cards_assigns maxes_assigns
   1.199 -               iters_assigns bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs =
   1.200 +fun all_scopes (hol_ctxt as {thy, ...}) binarize sym_break cards_assigns
   1.201 +               maxes_assigns iters_assigns bitss bisim_depths mono_Ts nonmono_Ts
   1.202 +               deep_dataTs =
   1.203    let
   1.204      val cards_assigns = repair_cards_assigns_wrt_boxing thy mono_Ts
   1.205                                                          cards_assigns
   1.206 -    val blocks = blocks_for_types hol_ctxt cards_assigns maxes_assigns
   1.207 +    val blocks = blocks_for_types hol_ctxt binarize cards_assigns maxes_assigns
   1.208                                    iters_assigns bitss bisim_depths mono_Ts
   1.209                                    nonmono_Ts
   1.210      val ranks = map rank_of_block blocks
   1.211      val all = all_combinations_ordered_smartly (map (rpair 0) ranks)
   1.212      val head = take max_scopes all
   1.213 -    val descs = map_filter (scope_descriptor_from_combination hol_ctxt blocks)
   1.214 -                           head
   1.215 +    val descs =
   1.216 +      map_filter (scope_descriptor_from_combination hol_ctxt binarize blocks)
   1.217 +                 head
   1.218    in
   1.219      (length all - length head,
   1.220       descs |> length descs <= distinct_threshold ? distinct (op =)
   1.221 -           |> map (scope_from_descriptor hol_ctxt sym_break deep_dataTs))
   1.222 +           |> map (scope_from_descriptor hol_ctxt binarize sym_break
   1.223 +                                         deep_dataTs))
   1.224    end
   1.225  
   1.226  end;