src/HOL/Tools/Nitpick/nitpick_scope.ML
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (24 months ago)
changeset 66695 91500c024c7f
parent 59058 a78612c67ec0
child 69593 3dda49e08b9d
permissions -rw-r--r--
tuned;
blanchet@33982
     1
(*  Title:      HOL/Tools/Nitpick/nitpick_scope.ML
blanchet@33192
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@34982
     3
    Copyright   2008, 2009, 2010
blanchet@33192
     4
blanchet@33192
     5
Scope enumerator for Nitpick.
blanchet@33192
     6
*)
blanchet@33192
     7
blanchet@33192
     8
signature NITPICK_SCOPE =
blanchet@33192
     9
sig
blanchet@35070
    10
  type hol_context = Nitpick_HOL.hol_context
blanchet@33192
    11
blanchet@36390
    12
  type constr_spec =
blanchet@55889
    13
    {const: string * typ,
blanchet@36390
    14
     delta: int,
blanchet@36390
    15
     epsilon: int,
blanchet@36390
    16
     exclusive: bool,
blanchet@36390
    17
     explicit_max: int,
blanchet@36390
    18
     total: bool}
blanchet@33192
    19
blanchet@55890
    20
  type data_type_spec =
blanchet@36390
    21
    {typ: typ,
blanchet@36390
    22
     card: int,
blanchet@36390
    23
     co: bool,
blanchet@38126
    24
     self_rec: bool,
blanchet@36390
    25
     complete: bool * bool,
blanchet@36390
    26
     concrete: bool * bool,
blanchet@36390
    27
     deep: bool,
blanchet@36390
    28
     constrs: constr_spec list}
blanchet@33192
    29
blanchet@36390
    30
  type scope =
blanchet@36390
    31
    {hol_ctxt: hol_context,
blanchet@36390
    32
     binarize: bool,
blanchet@36390
    33
     card_assigns: (typ * int) list,
blanchet@36390
    34
     bits: int,
blanchet@36390
    35
     bisim_depth: int,
blanchet@55890
    36
     data_types: data_type_spec list,
blanchet@36390
    37
     ofs: int Typtab.table}
blanchet@33192
    38
blanchet@55890
    39
  val is_asymmetric_non_data_type : typ -> bool
blanchet@55890
    40
  val data_type_spec : data_type_spec list -> typ -> data_type_spec option
blanchet@55890
    41
  val constr_spec : data_type_spec list -> string * typ -> constr_spec
blanchet@55890
    42
  val is_complete_type : data_type_spec list -> bool -> typ -> bool
blanchet@55890
    43
  val is_concrete_type : data_type_spec list -> bool -> typ -> bool
blanchet@55890
    44
  val is_exact_type : data_type_spec list -> bool -> typ -> bool
blanchet@33192
    45
  val offset_of_type : int Typtab.table -> typ -> int
blanchet@33192
    46
  val spec_of_type : scope -> typ -> int * int
blanchet@33192
    47
  val pretties_for_scope : scope -> bool -> Pretty.T list
blanchet@33192
    48
  val multiline_string_for_scope : scope -> string
blanchet@35814
    49
  val scopes_equivalent : scope * scope -> bool
blanchet@33192
    50
  val scope_less_eq : scope -> scope -> bool
blanchet@38126
    51
  val is_self_recursive_constr_type : typ -> bool
blanchet@33192
    52
  val all_scopes :
blanchet@55889
    53
    hol_context -> bool -> (typ option * int list) list ->
blanchet@55889
    54
    ((string * typ) option * int list) list ->
blanchet@55889
    55
    ((string * typ) option * int list) list -> int list -> int list ->
blanchet@55889
    56
    typ list -> typ list -> typ list -> typ list -> int * scope list
blanchet@33192
    57
end;
blanchet@33192
    58
blanchet@33232
    59
structure Nitpick_Scope : NITPICK_SCOPE =
blanchet@33192
    60
struct
blanchet@33192
    61
blanchet@33232
    62
open Nitpick_Util
blanchet@33232
    63
open Nitpick_HOL
blanchet@33192
    64
blanchet@36390
    65
type constr_spec =
blanchet@55889
    66
  {const: string * typ,
blanchet@36390
    67
   delta: int,
blanchet@36390
    68
   epsilon: int,
blanchet@36390
    69
   exclusive: bool,
blanchet@36390
    70
   explicit_max: int,
blanchet@36390
    71
   total: bool}
blanchet@33192
    72
blanchet@55890
    73
type data_type_spec =
blanchet@36390
    74
  {typ: typ,
blanchet@36390
    75
   card: int,
blanchet@36390
    76
   co: bool,
blanchet@38126
    77
   self_rec: bool,
blanchet@36390
    78
   complete: bool * bool,
blanchet@36390
    79
   concrete: bool * bool,
blanchet@36390
    80
   deep: bool,
blanchet@36390
    81
   constrs: constr_spec list}
blanchet@33192
    82
blanchet@36390
    83
type scope =
blanchet@36390
    84
  {hol_ctxt: hol_context,
blanchet@36390
    85
   binarize: bool,
blanchet@36390
    86
   card_assigns: (typ * int) list,
blanchet@36390
    87
   bits: int,
blanchet@36390
    88
   bisim_depth: int,
blanchet@55890
    89
   data_types: data_type_spec list,
blanchet@36390
    90
   ofs: int Typtab.table}
blanchet@33192
    91
blanchet@55889
    92
datatype row_kind = Card of typ | Max of string * typ
blanchet@33192
    93
blanchet@33192
    94
type row = row_kind * int list
blanchet@33192
    95
type block = row list
blanchet@33192
    96
blanchet@55890
    97
val is_asymmetric_non_data_type =
blanchet@38127
    98
  is_iterator_type orf is_integer_type orf is_bit_type
blanchet@38127
    99
blanchet@55890
   100
fun data_type_spec (dtypes : data_type_spec list) T =
blanchet@34121
   101
  List.find (curry (op =) T o #typ) dtypes
blanchet@33192
   102
blanchet@33232
   103
fun constr_spec [] x = raise TERM ("Nitpick_Scope.constr_spec", [Const x])
blanchet@55890
   104
  | constr_spec ({constrs, ...} :: dtypes : data_type_spec list) (x as (s, T)) =
blanchet@34121
   105
    case List.find (curry (op =) (s, body_type T) o (apsnd body_type o #const))
blanchet@33192
   106
                   constrs of
blanchet@33192
   107
      SOME c => c
blanchet@33192
   108
    | NONE => constr_spec dtypes x
blanchet@33192
   109
blanchet@35665
   110
fun is_complete_type dtypes facto (Type (@{type_name fun}, [T1, T2])) =
blanchet@35385
   111
    is_concrete_type dtypes facto T1 andalso is_complete_type dtypes facto T2
blanchet@38190
   112
  | is_complete_type dtypes facto (Type (@{type_name prod}, Ts)) =
blanchet@35385
   113
    forall (is_complete_type dtypes facto) Ts
blanchet@46083
   114
  | is_complete_type dtypes facto (Type (@{type_name set}, [T'])) =
blanchet@46083
   115
    is_concrete_type dtypes facto T'
blanchet@35385
   116
  | is_complete_type dtypes facto T =
blanchet@35220
   117
    not (is_integer_like_type T) andalso not (is_bit_type T) andalso
blanchet@55890
   118
    fun_from_pair (#complete (the (data_type_spec dtypes T))) facto
blanchet@33192
   119
    handle Option.Option => true
blanchet@35665
   120
and is_concrete_type dtypes facto (Type (@{type_name fun}, [T1, T2])) =
blanchet@35385
   121
    is_complete_type dtypes facto T1 andalso is_concrete_type dtypes facto T2
blanchet@38190
   122
  | is_concrete_type dtypes facto (Type (@{type_name prod}, Ts)) =
blanchet@35385
   123
    forall (is_concrete_type dtypes facto) Ts
blanchet@46083
   124
  | is_concrete_type dtypes facto (Type (@{type_name set}, [T'])) =
blanchet@46083
   125
    is_complete_type dtypes facto T'
blanchet@35385
   126
  | is_concrete_type dtypes facto T =
blanchet@55890
   127
    fun_from_pair (#concrete (the (data_type_spec dtypes T))) facto
blanchet@35385
   128
    handle Option.Option => true
blanchet@35665
   129
and is_exact_type dtypes facto =
blanchet@35385
   130
  is_complete_type dtypes facto andf is_concrete_type dtypes facto
blanchet@33192
   131
blanchet@33192
   132
fun offset_of_type ofs T =
blanchet@33192
   133
  case Typtab.lookup ofs T of
blanchet@33192
   134
    SOME j0 => j0
blanchet@33192
   135
  | NONE => Typtab.lookup ofs dummyT |> the_default 0
blanchet@33192
   136
blanchet@33192
   137
fun spec_of_type ({card_assigns, ofs, ...} : scope) T =
blanchet@33192
   138
  (card_of_type card_assigns T
blanchet@33232
   139
   handle TYPE ("Nitpick_HOL.card_of_type", _, _) => ~1, offset_of_type ofs T)
blanchet@33192
   140
blanchet@38188
   141
fun quintuple_for_scope code_type code_term code_string
blanchet@55888
   142
        ({hol_ctxt = {ctxt, ...}, card_assigns, bits, bisim_depth,
blanchet@55890
   143
         data_types, ...} : scope) =
blanchet@33192
   144
  let
blanchet@35075
   145
    val boring_Ts = [@{typ unsigned_bit}, @{typ signed_bit},
blanchet@34124
   146
                     @{typ bisim_iterator}]
blanchet@34123
   147
    val (iter_assigns, card_assigns) =
blanchet@34124
   148
      card_assigns |> filter_out (member (op =) boring_Ts o fst)
blanchet@33192
   149
                   |> List.partition (is_fp_iterator_type o fst)
blanchet@34124
   150
    val (secondary_card_assigns, primary_card_assigns) =
blanchet@37256
   151
      card_assigns
blanchet@55890
   152
      |> List.partition ((is_integer_type orf is_data_type ctxt) o fst)
blanchet@33192
   153
    val cards =
blanchet@38188
   154
      map (fn (T, k) =>
blanchet@38188
   155
              [code_type ctxt T, code_string (" = " ^ string_of_int k)])
blanchet@33192
   156
    fun maxes () =
blanchet@33192
   157
      maps (map_filter
blanchet@33192
   158
                (fn {const, explicit_max, ...} =>
blanchet@33192
   159
                    if explicit_max < 0 then
blanchet@33192
   160
                      NONE
blanchet@33192
   161
                    else
blanchet@38188
   162
                      SOME [code_term ctxt (Const const),
blanchet@38188
   163
                            code_string (" = " ^ string_of_int explicit_max)])
blanchet@55890
   164
                 o #constrs) data_types
blanchet@33192
   165
    fun iters () =
blanchet@33192
   166
      map (fn (T, k) =>
blanchet@38188
   167
              [code_term ctxt (Const (const_for_iterator_type T)),
blanchet@38188
   168
               code_string (" = " ^ string_of_int (k - 1))]) iter_assigns
blanchet@34124
   169
    fun miscs () =
blanchet@38188
   170
      (if bits = 0 then []
blanchet@38188
   171
       else [code_string ("bits = " ^ string_of_int bits)]) @
blanchet@55890
   172
      (if bisim_depth < 0 andalso forall (not o #co) data_types then []
blanchet@38188
   173
       else [code_string ("bisim_depth = " ^ signed_string_of_int bisim_depth)])
blanchet@33192
   174
  in
wenzelm@39118
   175
    (cards primary_card_assigns, cards secondary_card_assigns,
wenzelm@39118
   176
     maxes (), iters (), miscs ())
blanchet@33192
   177
  end
blanchet@33192
   178
blanchet@33192
   179
fun pretties_for_scope scope verbose =
blanchet@33192
   180
  let
blanchet@38188
   181
    fun standard_blocks s = map (Pretty.block o cons (Pretty.str (s ^ " ")))
blanchet@38188
   182
    val (primary_cards, secondary_cards, maxes, iters, miscs) =
wenzelm@58928
   183
      quintuple_for_scope
wenzelm@58928
   184
        (fn ctxt => pretty_maybe_quote (Thy_Header.get_keywords' ctxt) o pretty_for_type ctxt)
wenzelm@58928
   185
        (fn ctxt => pretty_maybe_quote (Thy_Header.get_keywords' ctxt) o Syntax.pretty_term ctxt)
wenzelm@58928
   186
        Pretty.str scope
blanchet@33192
   187
  in
blanchet@38188
   188
    standard_blocks "card" primary_cards @
blanchet@38188
   189
    (if verbose then
blanchet@38188
   190
       standard_blocks "card" secondary_cards @
blanchet@38188
   191
       standard_blocks "max" maxes @
blanchet@38188
   192
       standard_blocks "iter" iters @
blanchet@38188
   193
       miscs
blanchet@38188
   194
     else
blanchet@38188
   195
       [])
blanchet@38188
   196
    |> pretty_serial_commas "and"
blanchet@33192
   197
  end
blanchet@33192
   198
blanchet@33192
   199
fun multiline_string_for_scope scope =
blanchet@33192
   200
  let
blanchet@38188
   201
    val (primary_cards, secondary_cards, maxes, iters, miscs) =
blanchet@38188
   202
      quintuple_for_scope Syntax.string_of_typ Syntax.string_of_term I scope
blanchet@34124
   203
    val cards = primary_cards @ secondary_cards
blanchet@33192
   204
  in
blanchet@38188
   205
    case (if null cards then [] else ["card: " ^ commas (map implode cards)]) @
blanchet@38188
   206
         (if null maxes then [] else ["max: " ^ commas (map implode maxes)]) @
blanchet@38188
   207
         (if null iters then [] else ["iter: " ^ commas (map implode iters)]) @
blanchet@38188
   208
         miscs of
blanchet@33192
   209
      [] => "empty"
wenzelm@55628
   210
    | lines => cat_lines lines
blanchet@33192
   211
  end
blanchet@33192
   212
blanchet@35814
   213
fun scopes_equivalent (s1 : scope, s2 : scope) =
blanchet@55890
   214
  #data_types s1 = #data_types s2 andalso #card_assigns s1 = #card_assigns s2
blanchet@55889
   215
blanchet@33192
   216
fun scope_less_eq (s1 : scope) (s2 : scope) =
wenzelm@59058
   217
  (s1, s2) |> apply2 (map snd o #card_assigns) |> op ~~ |> forall (op <=)
blanchet@33192
   218
blanchet@33192
   219
fun rank_of_row (_, ks) = length ks
blanchet@55889
   220
blanchet@33192
   221
fun rank_of_block block = fold Integer.max (map rank_of_row block) 1
blanchet@55889
   222
blanchet@41991
   223
fun project_row _ (y, []) = (y, [1]) (* desperate measure *)
blanchet@41991
   224
  | project_row column (y, ks) = (y, [nth ks (Int.min (column, length ks - 1))])
blanchet@55889
   225
blanchet@33192
   226
fun project_block (column, block) = map (project_row column) block
blanchet@33192
   227
blanchet@34123
   228
fun lookup_ints_assign eq assigns key =
blanchet@34123
   229
  case triple_lookup eq assigns key of
blanchet@33192
   230
    SOME ks => ks
blanchet@33232
   231
  | NONE => raise ARG ("Nitpick_Scope.lookup_ints_assign", "")
blanchet@55889
   232
blanchet@34123
   233
fun lookup_type_ints_assign thy assigns T =
blanchet@36384
   234
  map (Integer.max 1) (lookup_ints_assign (type_match thy) assigns T)
blanchet@33232
   235
  handle ARG ("Nitpick_Scope.lookup_ints_assign", _) =>
blanchet@33232
   236
         raise TYPE ("Nitpick_Scope.lookup_type_ints_assign", [T], [])
blanchet@55889
   237
blanchet@34123
   238
fun lookup_const_ints_assign thy assigns x =
blanchet@34123
   239
  lookup_ints_assign (const_match thy) assigns x
blanchet@33232
   240
  handle ARG ("Nitpick_Scope.lookup_ints_assign", _) =>
blanchet@33232
   241
         raise TERM ("Nitpick_Scope.lookup_const_ints_assign", [Const x])
blanchet@33192
   242
blanchet@34123
   243
fun row_for_constr thy maxes_assigns constr =
blanchet@34123
   244
  SOME (Max constr, lookup_const_ints_assign thy maxes_assigns constr)
blanchet@33192
   245
  handle TERM ("lookup_const_ints_assign", _) => NONE
blanchet@33192
   246
blanchet@34124
   247
val max_bits = 31 (* Kodkod limit *)
blanchet@34124
   248
blanchet@35190
   249
fun block_for_type (hol_ctxt as {thy, ...}) binarize cards_assigns maxes_assigns
blanchet@34124
   250
                   iters_assigns bitss bisim_depths T =
blanchet@38240
   251
  case T of
blanchet@38240
   252
    @{typ unsigned_bit} =>
blanchet@34124
   253
    [(Card T, map (Integer.min max_bits o Integer.max 1) bitss)]
blanchet@38240
   254
  | @{typ signed_bit} =>
blanchet@34124
   255
    [(Card T, map (Integer.add 1 o Integer.min max_bits o Integer.max 1) bitss)]
blanchet@38240
   256
  | @{typ "unsigned_bit word"} =>
blanchet@34126
   257
    [(Card T, lookup_type_ints_assign thy cards_assigns nat_T)]
blanchet@38240
   258
  | @{typ "signed_bit word"} =>
blanchet@34126
   259
    [(Card T, lookup_type_ints_assign thy cards_assigns int_T)]
blanchet@38240
   260
  | @{typ bisim_iterator} =>
blanchet@34124
   261
    [(Card T, map (Integer.add 1 o Integer.max 0) bisim_depths)]
blanchet@38240
   262
  | _ =>
blanchet@38240
   263
    if is_fp_iterator_type T then
blanchet@38240
   264
      [(Card T, map (Integer.add 1 o Integer.max 0)
blanchet@38240
   265
                    (lookup_const_ints_assign thy iters_assigns
blanchet@38240
   266
                                              (const_for_iterator_type T)))]
blanchet@38240
   267
    else
blanchet@38240
   268
      (Card T, lookup_type_ints_assign thy cards_assigns T) ::
blanchet@55890
   269
      (case binarized_and_boxed_data_type_constrs hol_ctxt binarize T of
blanchet@38240
   270
         [_] => []
blanchet@38240
   271
       | constrs => map_filter (row_for_constr thy maxes_assigns) constrs)
blanchet@33192
   272
blanchet@35190
   273
fun blocks_for_types hol_ctxt binarize cards_assigns maxes_assigns iters_assigns
blanchet@35190
   274
                     bitss bisim_depths mono_Ts nonmono_Ts =
blanchet@33192
   275
  let
blanchet@35190
   276
    val block_for = block_for_type hol_ctxt binarize cards_assigns maxes_assigns
blanchet@34124
   277
                                   iters_assigns bitss bisim_depths
blanchet@33192
   278
    val mono_block = maps block_for mono_Ts
blanchet@33192
   279
    val nonmono_blocks = map block_for nonmono_Ts
blanchet@33192
   280
  in mono_block :: nonmono_blocks end
blanchet@33192
   281
blanchet@33192
   282
val sync_threshold = 5
blanchet@38186
   283
val linearity = 5
blanchet@33192
   284
blanchet@38186
   285
val all_combinations_ordered_smartly =
blanchet@33192
   286
  let
blanchet@38186
   287
    fun cost [] = 0
blanchet@38186
   288
      | cost [k] = k
blanchet@38186
   289
      | cost (k :: ks) =
blanchet@34121
   290
        if k < sync_threshold andalso forall (curry (op =) k) ks then
blanchet@33192
   291
          k - sync_threshold
blanchet@33192
   292
        else
blanchet@38187
   293
          k :: ks |> map (fn k => (k + linearity) * (k + linearity))
blanchet@38187
   294
                  |> Integer.sum
blanchet@33192
   295
  in
wenzelm@59058
   296
    all_combinations #> map (`cost) #> sort (int_ord o apply2 fst) #> map snd
blanchet@33192
   297
  end
blanchet@33192
   298
blanchet@33192
   299
fun is_self_recursive_constr_type T =
blanchet@34121
   300
  exists (exists_subtype (curry (op =) (body_type T))) (binder_types T)
blanchet@33192
   301
blanchet@33192
   302
fun constr_max maxes x = the_default ~1 (AList.lookup (op =) maxes x)
blanchet@33192
   303
blanchet@55889
   304
type scope_desc = (typ * int) list * ((string * typ) * int) list
blanchet@33192
   305
blanchet@35190
   306
fun is_surely_inconsistent_card_assign hol_ctxt binarize
blanchet@35190
   307
                                       (card_assigns, max_assigns) (T, k) =
blanchet@55890
   308
  case binarized_and_boxed_data_type_constrs hol_ctxt binarize T of
blanchet@33192
   309
    [] => false
blanchet@33192
   310
  | xs =>
blanchet@33192
   311
    let
blanchet@34126
   312
      val dom_cards =
blanchet@34126
   313
        map (Integer.prod o map (bounded_card_of_type k ~1 card_assigns)
blanchet@33192
   314
             o binder_types o snd) xs
blanchet@34123
   315
      val maxes = map (constr_max max_assigns) xs
blanchet@34126
   316
      fun effective_max card ~1 = card
blanchet@33192
   317
        | effective_max card max = Int.min (card, max)
blanchet@34126
   318
      val max = map2 effective_max dom_cards maxes |> Integer.sum
blanchet@34126
   319
    in max < k end
blanchet@55889
   320
blanchet@35190
   321
fun is_surely_inconsistent_scope_description hol_ctxt binarize seen rest
blanchet@35190
   322
                                             max_assigns =
blanchet@35190
   323
  exists (is_surely_inconsistent_card_assign hol_ctxt binarize
blanchet@34126
   324
                                             (seen @ rest, max_assigns)) seen
blanchet@33192
   325
blanchet@35190
   326
fun repair_card_assigns hol_ctxt binarize (card_assigns, max_assigns) =
blanchet@33192
   327
  let
blanchet@33192
   328
    fun aux seen [] = SOME seen
blanchet@35280
   329
      | aux _ ((_, 0) :: _) = NONE
blanchet@34126
   330
      | aux seen ((T, k) :: rest) =
blanchet@35190
   331
        (if is_surely_inconsistent_scope_description hol_ctxt binarize
blanchet@35190
   332
                ((T, k) :: seen) rest max_assigns then
blanchet@33192
   333
           raise SAME ()
blanchet@33192
   334
         else
blanchet@34126
   335
           case aux ((T, k) :: seen) rest of
blanchet@34123
   336
             SOME assigns => SOME assigns
blanchet@33192
   337
           | NONE => raise SAME ())
blanchet@34126
   338
        handle SAME () => aux seen ((T, k - 1) :: rest)
blanchet@34123
   339
  in aux [] (rev card_assigns) end
blanchet@33192
   340
blanchet@38240
   341
fun repair_iterator_assign ctxt assigns (T as Type (_, Ts), k) =
blanchet@33192
   342
    (T, if T = @{typ bisim_iterator} then
blanchet@34123
   343
          let
blanchet@38240
   344
            val co_cards = map snd (filter (is_codatatype ctxt o fst) assigns)
blanchet@34123
   345
          in Int.min (k, Integer.sum co_cards) end
blanchet@33192
   346
        else if is_fp_iterator_type T then
blanchet@33192
   347
          case Ts of
blanchet@33192
   348
            [] => 1
blanchet@34123
   349
          | _ => bounded_card_of_type k ~1 assigns (foldr1 HOLogic.mk_prodT Ts)
blanchet@33192
   350
        else
blanchet@33192
   351
          k)
blanchet@34123
   352
  | repair_iterator_assign _ _ assign = assign
blanchet@33192
   353
blanchet@34123
   354
fun add_row_to_scope_descriptor (kind, ks) (card_assigns, max_assigns) =
blanchet@33192
   355
  case kind of
blanchet@34123
   356
    Card T => ((T, the_single ks) :: card_assigns, max_assigns)
blanchet@34123
   357
  | Max x => (card_assigns, (x, the_single ks) :: max_assigns)
blanchet@55889
   358
blanchet@33192
   359
fun scope_descriptor_from_block block =
blanchet@33192
   360
  fold_rev add_row_to_scope_descriptor block ([], [])
blanchet@55889
   361
blanchet@38240
   362
fun scope_descriptor_from_combination (hol_ctxt as {ctxt, ...}) binarize blocks
blanchet@35190
   363
                                      columns =
blanchet@33192
   364
  let
blanchet@34123
   365
    val (card_assigns, max_assigns) =
blanchet@33192
   366
      maps project_block (columns ~~ blocks) |> scope_descriptor_from_block
blanchet@33192
   367
  in
blanchet@41991
   368
    (card_assigns, max_assigns)
blanchet@41991
   369
    |> repair_card_assigns hol_ctxt binarize
blanchet@41991
   370
    |> Option.map
blanchet@41991
   371
           (fn card_assigns =>
blanchet@41991
   372
               (map (repair_iterator_assign ctxt card_assigns) card_assigns,
blanchet@41991
   373
                max_assigns))
blanchet@33192
   374
  end
blanchet@33192
   375
blanchet@38124
   376
fun offset_table_for_card_assigns dtypes assigns =
blanchet@33192
   377
  let
blanchet@33192
   378
    fun aux next _ [] = Typtab.update_new (dummyT, next)
blanchet@34123
   379
      | aux next reusable ((T, k) :: assigns) =
blanchet@55890
   380
        if k = 1 orelse is_asymmetric_non_data_type T then
blanchet@34123
   381
          aux next reusable assigns
blanchet@55890
   382
        else if length (these (Option.map #constrs (data_type_spec dtypes T)))
blanchet@33192
   383
                > 1 then
blanchet@34123
   384
          Typtab.update_new (T, next) #> aux (next + k) reusable assigns
blanchet@33192
   385
        else
blanchet@33192
   386
          case AList.lookup (op =) reusable k of
blanchet@34123
   387
            SOME j0 => Typtab.update_new (T, j0) #> aux next reusable assigns
blanchet@33192
   388
          | NONE => Typtab.update_new (T, next)
blanchet@34123
   389
                    #> aux (next + k) ((k, next) :: reusable) assigns
blanchet@38124
   390
  in Typtab.empty |> aux 0 [] assigns end
blanchet@33192
   391
blanchet@34123
   392
fun domain_card max card_assigns =
blanchet@34123
   393
  Integer.prod o map (bounded_card_of_type max max card_assigns) o binder_types
blanchet@33192
   394
blanchet@38162
   395
fun add_constr_spec (card_assigns, max_assigns) acyclic card sum_dom_cards
blanchet@35280
   396
                    num_self_recs num_non_self_recs (self_rec, x as (_, T))
blanchet@34123
   397
                    constrs =
blanchet@33192
   398
  let
blanchet@34123
   399
    val max = constr_max max_assigns x
blanchet@33192
   400
    fun next_delta () = if null constrs then 0 else #epsilon (hd constrs)
blanchet@33192
   401
    val {delta, epsilon, exclusive, total} =
blanchet@33192
   402
      if max = 0 then
blanchet@33192
   403
        let val delta = next_delta () in
blanchet@33192
   404
          {delta = delta, epsilon = delta, exclusive = true, total = false}
blanchet@33192
   405
        end
blanchet@38162
   406
      else if num_self_recs > 0 then
blanchet@38193
   407
        (if num_non_self_recs = 1 then
blanchet@35072
   408
           if self_rec then
blanchet@38193
   409
             case List.last constrs of
blanchet@38193
   410
               {delta = 0, epsilon = 1, exclusive = true, ...} =>
blanchet@38193
   411
               {delta = 1, epsilon = card, exclusive = (num_self_recs = 1),
blanchet@38193
   412
                total = false}
blanchet@35072
   413
             | _ => raise SAME ()
blanchet@35072
   414
           else
blanchet@35072
   415
             if domain_card 2 card_assigns T = 1 then
blanchet@38162
   416
               {delta = 0, epsilon = 1, exclusive = acyclic, total = acyclic}
blanchet@35072
   417
             else
blanchet@35072
   418
               raise SAME ()
blanchet@35072
   419
         else
blanchet@35072
   420
           raise SAME ())
blanchet@35072
   421
        handle SAME () =>
blanchet@35072
   422
               {delta = 0, epsilon = card, exclusive = false, total = false}
blanchet@33192
   423
      else if card = sum_dom_cards (card + 1) then
blanchet@33192
   424
        let val delta = next_delta () in
blanchet@34123
   425
          {delta = delta, epsilon = delta + domain_card card card_assigns T,
blanchet@33192
   426
           exclusive = true, total = true}
blanchet@33192
   427
        end
blanchet@33192
   428
      else
blanchet@33192
   429
        {delta = 0, epsilon = card,
blanchet@33192
   430
         exclusive = (num_self_recs + num_non_self_recs = 1), total = false}
blanchet@33192
   431
  in
blanchet@33192
   432
    {const = x, delta = delta, epsilon = epsilon, exclusive = exclusive,
blanchet@33192
   433
     explicit_max = max, total = total} :: constrs
blanchet@33192
   434
  end
blanchet@33192
   435
blanchet@35385
   436
fun has_exact_card hol_ctxt facto finitizable_dataTs card_assigns T =
blanchet@34123
   437
  let val card = card_of_type card_assigns T in
blanchet@35385
   438
    card = bounded_exact_card_of_type hol_ctxt
blanchet@35385
   439
               (if facto then finitizable_dataTs else []) (card + 1) 0
blanchet@35385
   440
               card_assigns T
blanchet@34123
   441
  end
blanchet@34123
   442
blanchet@55890
   443
fun data_type_spec_from_scope_descriptor (hol_ctxt as {ctxt, ...})
blanchet@38240
   444
        binarize deep_dataTs finitizable_dataTs (desc as (card_assigns, _))
blanchet@38240
   445
        (T, card) =
blanchet@33192
   446
  let
blanchet@34982
   447
    val deep = member (op =) deep_dataTs T
blanchet@38240
   448
    val co = is_codatatype ctxt T
blanchet@55890
   449
    val xs = binarized_and_boxed_data_type_constrs hol_ctxt binarize T
blanchet@33192
   450
    val self_recs = map (is_self_recursive_constr_type o snd) xs
blanchet@33192
   451
    val (num_self_recs, num_non_self_recs) =
wenzelm@59058
   452
      List.partition I self_recs |> apply2 length
blanchet@38126
   453
    val self_rec = num_self_recs > 0
blanchet@35385
   454
    fun is_complete facto =
blanchet@35385
   455
      has_exact_card hol_ctxt facto finitizable_dataTs card_assigns T
blanchet@35385
   456
    fun is_concrete facto =
blanchet@35385
   457
      is_word_type T orelse
blanchet@47909
   458
      (* FIXME: looks wrong; other types than just functions might be
blanchet@45402
   459
         abstract. "is_complete" is also suspicious. *)
blanchet@35385
   460
      xs |> maps (binder_types o snd) |> maps binder_types
blanchet@35385
   461
         |> forall (has_exact_card hol_ctxt facto finitizable_dataTs
blanchet@35385
   462
                                   card_assigns)
blanchet@35385
   463
    val complete = pair_from_fun is_complete
blanchet@35385
   464
    val concrete = pair_from_fun is_concrete
blanchet@33192
   465
    fun sum_dom_cards max =
blanchet@34123
   466
      map (domain_card max card_assigns o snd) xs |> Integer.sum
blanchet@33192
   467
    val constrs =
blanchet@55888
   468
      fold_rev (add_constr_spec desc (not co) card sum_dom_cards num_self_recs
blanchet@55888
   469
                                num_non_self_recs)
wenzelm@59058
   470
               (sort (bool_ord o swap o apply2 fst) (self_recs ~~ xs)) []
blanchet@33558
   471
  in
blanchet@55888
   472
    {typ = T, card = card, co = co, self_rec = self_rec, complete = complete,
blanchet@55888
   473
     concrete = concrete, deep = deep, constrs = constrs}
blanchet@33558
   474
  end
blanchet@33192
   475
blanchet@55888
   476
fun scope_from_descriptor (hol_ctxt as {ctxt, ...}) binarize deep_dataTs
blanchet@36386
   477
                          finitizable_dataTs (desc as (card_assigns, _)) =
blanchet@33192
   478
  let
blanchet@55890
   479
    val data_types =
blanchet@55890
   480
      map (data_type_spec_from_scope_descriptor hol_ctxt binarize deep_dataTs
blanchet@55890
   481
                                                finitizable_dataTs desc)
blanchet@55890
   482
          (filter (is_data_type ctxt o fst) card_assigns)
blanchet@34124
   483
    val bits = card_of_type card_assigns @{typ signed_bit} - 1
blanchet@34124
   484
               handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
blanchet@34124
   485
                      card_of_type card_assigns @{typ unsigned_bit}
blanchet@34124
   486
                      handle TYPE ("Nitpick_HOL.card_of_type", _, _) => 0
blanchet@34123
   487
    val bisim_depth = card_of_type card_assigns @{typ bisim_iterator} - 1
blanchet@33192
   488
  in
blanchet@35190
   489
    {hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns,
blanchet@55890
   490
     data_types = data_types, bits = bits, bisim_depth = bisim_depth,
blanchet@55890
   491
     ofs = offset_table_for_card_assigns data_types card_assigns}
blanchet@33192
   492
  end
blanchet@33192
   493
blanchet@35665
   494
fun repair_cards_assigns_wrt_boxing_etc _ _ [] = []
blanchet@35665
   495
  | repair_cards_assigns_wrt_boxing_etc thy Ts ((SOME T, ks) :: cards_assigns) =
blanchet@33192
   496
    (if is_fun_type T orelse is_pair_type T then
blanchet@35665
   497
       Ts |> filter (curry (type_match thy o swap) T) |> map (rpair ks o SOME)
blanchet@33192
   498
     else
blanchet@35665
   499
       [(SOME T, ks)]) @
blanchet@35665
   500
       repair_cards_assigns_wrt_boxing_etc thy Ts cards_assigns
blanchet@35665
   501
  | repair_cards_assigns_wrt_boxing_etc thy Ts ((NONE, ks) :: cards_assigns) =
blanchet@35665
   502
    (NONE, ks) :: repair_cards_assigns_wrt_boxing_etc thy Ts cards_assigns
blanchet@33192
   503
blanchet@38180
   504
val max_scopes = 5000
blanchet@38180
   505
val distinct_threshold = 1000
blanchet@33192
   506
blanchet@36386
   507
fun all_scopes (hol_ctxt as {thy, ...}) binarize cards_assigns maxes_assigns
blanchet@36386
   508
               iters_assigns bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs
blanchet@36386
   509
               finitizable_dataTs =
blanchet@33192
   510
  let
blanchet@38240
   511
    val cards_assigns =
blanchet@38240
   512
      repair_cards_assigns_wrt_boxing_etc thy mono_Ts cards_assigns
blanchet@38240
   513
    val blocks =
blanchet@38240
   514
      blocks_for_types hol_ctxt binarize cards_assigns maxes_assigns
blanchet@38240
   515
                       iters_assigns bitss bisim_depths mono_Ts nonmono_Ts
blanchet@33192
   516
    val ranks = map rank_of_block blocks
blanchet@33580
   517
    val all = all_combinations_ordered_smartly (map (rpair 0) ranks)
haftmann@33957
   518
    val head = take max_scopes all
blanchet@35190
   519
    val descs =
blanchet@35190
   520
      map_filter (scope_descriptor_from_combination hol_ctxt binarize blocks)
blanchet@35190
   521
                 head
blanchet@33192
   522
  in
blanchet@33580
   523
    (length all - length head,
blanchet@33580
   524
     descs |> length descs <= distinct_threshold ? distinct (op =)
blanchet@36386
   525
           |> map (scope_from_descriptor hol_ctxt binarize deep_dataTs
blanchet@36386
   526
                                         finitizable_dataTs))
blanchet@33192
   527
  end
blanchet@33192
   528
blanchet@33192
   529
end;