src/HOL/Nitpick_Examples/minipick.ML
author wenzelm
Wed Nov 26 20:05:34 2014 +0100 (2014-11-26)
changeset 59058 a78612c67ec0
parent 55208 11dd3d1da83b
child 59970 e9f73d87d904
permissions -rw-r--r--
renamed "pairself" to "apply2", in accordance to @{apply 2};
blanchet@45035
     1
(*  Title:      HOL/Nitpick_Examples/minipick.ML
blanchet@45035
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@45035
     3
    Copyright   2009-2010
blanchet@45035
     4
blanchet@45035
     5
Finite model generation for HOL formulas using Kodkod, minimalistic version.
blanchet@45035
     6
*)
blanchet@45035
     7
blanchet@45035
     8
signature MINIPICK =
blanchet@45035
     9
sig
blanchet@45062
    10
  val minipick : Proof.context -> int -> term -> string
blanchet@45062
    11
  val minipick_expect : Proof.context -> string -> int -> term -> unit
blanchet@45035
    12
end;
blanchet@45035
    13
blanchet@45035
    14
structure Minipick : MINIPICK =
blanchet@45035
    15
struct
blanchet@45035
    16
blanchet@45035
    17
open Kodkod
blanchet@45035
    18
open Nitpick_Util
blanchet@45035
    19
open Nitpick_HOL
blanchet@45035
    20
open Nitpick_Peephole
blanchet@45035
    21
open Nitpick_Kodkod
blanchet@45035
    22
blanchet@45062
    23
datatype rep =
blanchet@45062
    24
  S_Rep |
blanchet@45062
    25
  R_Rep of bool
blanchet@45035
    26
blanchet@45062
    27
fun check_type ctxt raw_infinite (Type (@{type_name fun}, Ts)) =
blanchet@45062
    28
    List.app (check_type ctxt raw_infinite) Ts
blanchet@45062
    29
  | check_type ctxt raw_infinite (Type (@{type_name prod}, Ts)) =
blanchet@45062
    30
    List.app (check_type ctxt raw_infinite) Ts
blanchet@45062
    31
  | check_type _ _ @{typ bool} = ()
blanchet@45062
    32
  | check_type _ _ (TFree (_, @{sort "{}"})) = ()
blanchet@45062
    33
  | check_type _ _ (TFree (_, @{sort HOL.type})) = ()
blanchet@45062
    34
  | check_type ctxt raw_infinite T =
blanchet@46092
    35
    if raw_infinite T then
blanchet@46092
    36
      ()
blanchet@46092
    37
    else
blanchet@46092
    38
      error ("Not supported: Type " ^ quote (Syntax.string_of_typ ctxt T) ^ ".")
blanchet@45035
    39
blanchet@45035
    40
fun atom_schema_of S_Rep card (Type (@{type_name fun}, [T1, T2])) =
blanchet@45035
    41
    replicate_list (card T1) (atom_schema_of S_Rep card T2)
blanchet@45062
    42
  | atom_schema_of (R_Rep true) card
blanchet@45062
    43
                   (Type (@{type_name fun}, [T1, @{typ bool}])) =
blanchet@45035
    44
    atom_schema_of S_Rep card T1
blanchet@45062
    45
  | atom_schema_of (rep as R_Rep _) card (Type (@{type_name fun}, [T1, T2])) =
blanchet@45062
    46
    atom_schema_of S_Rep card T1 @ atom_schema_of rep card T2
blanchet@45035
    47
  | atom_schema_of _ card (Type (@{type_name prod}, Ts)) =
blanchet@45035
    48
    maps (atom_schema_of S_Rep card) Ts
blanchet@45035
    49
  | atom_schema_of _ card T = [card T]
blanchet@45035
    50
val arity_of = length ooo atom_schema_of
blanchet@45062
    51
val atom_seqs_of = map (AtomSeq o rpair 0) ooo atom_schema_of
blanchet@45062
    52
val atom_seq_product_of = foldl1 Product ooo atom_seqs_of
blanchet@45035
    53
blanchet@45035
    54
fun index_for_bound_var _ [_] 0 = 0
blanchet@45035
    55
  | index_for_bound_var card (_ :: Ts) 0 =
blanchet@45035
    56
    index_for_bound_var card Ts 0 + arity_of S_Rep card (hd Ts)
blanchet@45035
    57
  | index_for_bound_var card Ts n = index_for_bound_var card (tl Ts) (n - 1)
blanchet@45035
    58
fun vars_for_bound_var card R Ts j =
blanchet@45035
    59
  map (curry Var 1) (index_seq (index_for_bound_var card Ts j)
blanchet@45035
    60
                               (arity_of R card (nth Ts j)))
blanchet@45035
    61
val rel_expr_for_bound_var = foldl1 Product oooo vars_for_bound_var
blanchet@45035
    62
fun decls_for R card Ts T =
blanchet@45035
    63
  map2 (curry DeclOne o pair 1)
blanchet@45035
    64
       (index_seq (index_for_bound_var card (T :: Ts) 0)
blanchet@45035
    65
                  (arity_of R card (nth (T :: Ts) 0)))
blanchet@45062
    66
       (atom_seqs_of R card T)
blanchet@45035
    67
blanchet@45035
    68
val atom_product = foldl1 Product o map Atom
blanchet@45035
    69
blanchet@45062
    70
val false_atom_num = 0
blanchet@45062
    71
val true_atom_num = 1
blanchet@45062
    72
val false_atom = Atom false_atom_num
blanchet@45062
    73
val true_atom = Atom true_atom_num
blanchet@45035
    74
blanchet@45062
    75
fun kodkod_formula_from_term ctxt total card complete concrete frees =
blanchet@45035
    76
  let
blanchet@45062
    77
    fun F_from_S_rep (SOME false) r = Not (RelEq (r, false_atom))
blanchet@45062
    78
      | F_from_S_rep _ r = RelEq (r, true_atom)
blanchet@45062
    79
    fun S_rep_from_F NONE f = RelIf (f, true_atom, false_atom)
blanchet@45062
    80
      | S_rep_from_F (SOME true) f = RelIf (f, true_atom, None)
blanchet@45062
    81
      | S_rep_from_F (SOME false) f = RelIf (Not f, false_atom, None)
blanchet@45062
    82
    fun R_rep_from_S_rep (Type (@{type_name fun}, [T1, T2])) r =
blanchet@45062
    83
        if total andalso T2 = bool_T then
blanchet@45062
    84
          let
blanchet@45062
    85
            val jss = atom_schema_of S_Rep card T1 |> map (rpair 0)
blanchet@45062
    86
                      |> all_combinations
blanchet@45062
    87
          in
blanchet@45062
    88
            map2 (fn i => fn js =>
blanchet@45062
    89
(*
blanchet@45062
    90
                     RelIf (F_from_S_rep NONE (Project (r, [Num i])),
blanchet@45062
    91
                            atom_product js, empty_n_ary_rel (length js))
blanchet@45062
    92
*)
blanchet@45062
    93
                     Join (Project (r, [Num i]),
blanchet@45062
    94
                           atom_product (false_atom_num :: js))
blanchet@45062
    95
                 ) (index_seq 0 (length jss)) jss
blanchet@45062
    96
            |> foldl1 Union
blanchet@45062
    97
          end
blanchet@45062
    98
        else
blanchet@45062
    99
          let
blanchet@45062
   100
            val jss = atom_schema_of S_Rep card T1 |> map (rpair 0)
blanchet@45062
   101
                      |> all_combinations
blanchet@45062
   102
            val arity2 = arity_of S_Rep card T2
blanchet@45062
   103
          in
blanchet@45062
   104
            map2 (fn i => fn js =>
blanchet@45062
   105
                     Product (atom_product js,
blanchet@45062
   106
                              Project (r, num_seq (i * arity2) arity2)
blanchet@45062
   107
                              |> R_rep_from_S_rep T2))
blanchet@45062
   108
                 (index_seq 0 (length jss)) jss
blanchet@45062
   109
            |> foldl1 Union
blanchet@45062
   110
          end
blanchet@45035
   111
      | R_rep_from_S_rep _ r = r
blanchet@45035
   112
    fun S_rep_from_R_rep Ts (T as Type (@{type_name fun}, _)) r =
blanchet@45035
   113
        Comprehension (decls_for S_Rep card Ts T,
blanchet@45035
   114
            RelEq (R_rep_from_S_rep T
blanchet@45035
   115
                       (rel_expr_for_bound_var card S_Rep (T :: Ts) 0), r))
blanchet@45035
   116
      | S_rep_from_R_rep _ _ r = r
blanchet@45062
   117
    fun partial_eq pos Ts (Type (@{type_name fun}, [T1, T2])) t1 t2 =
blanchet@45062
   118
        HOLogic.mk_all ("x", T1,
blanchet@45062
   119
                        HOLogic.eq_const T2 $ (incr_boundvars 1 t1 $ Bound 0)
blanchet@45062
   120
                        $ (incr_boundvars 1 t2 $ Bound 0))
blanchet@45062
   121
        |> to_F (SOME pos) Ts
blanchet@45062
   122
      | partial_eq pos Ts T t1 t2 =
blanchet@45062
   123
        if pos andalso not (concrete T) then
blanchet@45062
   124
          False
blanchet@45062
   125
        else
wenzelm@59058
   126
          (t1, t2) |> apply2 (to_R_rep Ts)
blanchet@45062
   127
                   |> (if pos then Some o Intersect else Lone o Union)
blanchet@45062
   128
    and to_F pos Ts t =
blanchet@45035
   129
      (case t of
blanchet@45062
   130
         @{const Not} $ t1 => Not (to_F (Option.map not pos) Ts t1)
blanchet@45035
   131
       | @{const False} => False
blanchet@45035
   132
       | @{const True} => True
blanchet@45035
   133
       | Const (@{const_name All}, _) $ Abs (_, T, t') =>
blanchet@45062
   134
         if pos = SOME true andalso not (complete T) then False
blanchet@45062
   135
         else All (decls_for S_Rep card Ts T, to_F pos (T :: Ts) t')
blanchet@45035
   136
       | (t0 as Const (@{const_name All}, _)) $ t1 =>
blanchet@45062
   137
         to_F pos Ts (t0 $ eta_expand Ts t1 1)
blanchet@45035
   138
       | Const (@{const_name Ex}, _) $ Abs (_, T, t') =>
blanchet@45062
   139
         if pos = SOME false andalso not (complete T) then True
blanchet@45062
   140
         else Exist (decls_for S_Rep card Ts T, to_F pos (T :: Ts) t')
blanchet@45035
   141
       | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
blanchet@45062
   142
         to_F pos Ts (t0 $ eta_expand Ts t1 1)
blanchet@45062
   143
       | Const (@{const_name HOL.eq}, Type (_, [T, _])) $ t1 $ t2 =>
blanchet@45062
   144
         (case pos of
blanchet@45062
   145
            NONE => RelEq (to_R_rep Ts t1, to_R_rep Ts t2)
blanchet@45062
   146
          | SOME pos => partial_eq pos Ts T t1 t2)
blanchet@45035
   147
       | Const (@{const_name ord_class.less_eq},
blanchet@45035
   148
                Type (@{type_name fun},
blanchet@45062
   149
                      [Type (@{type_name fun}, [T', @{typ bool}]), _]))
blanchet@45035
   150
         $ t1 $ t2 =>
blanchet@45062
   151
         (case pos of
blanchet@45062
   152
            NONE => Subset (to_R_rep Ts t1, to_R_rep Ts t2)
blanchet@45062
   153
          | SOME true =>
blanchet@45062
   154
            Subset (Difference (atom_seq_product_of S_Rep card T',
blanchet@45062
   155
                                Join (to_R_rep Ts t1, false_atom)),
blanchet@45062
   156
                    Join (to_R_rep Ts t2, true_atom))
blanchet@45062
   157
          | SOME false =>
blanchet@45062
   158
            Subset (Join (to_R_rep Ts t1, true_atom),
blanchet@45062
   159
                    Difference (atom_seq_product_of S_Rep card T',
blanchet@45062
   160
                                Join (to_R_rep Ts t2, false_atom))))
blanchet@45062
   161
       | @{const HOL.conj} $ t1 $ t2 => And (to_F pos Ts t1, to_F pos Ts t2)
blanchet@45062
   162
       | @{const HOL.disj} $ t1 $ t2 => Or (to_F pos Ts t1, to_F pos Ts t2)
blanchet@45062
   163
       | @{const HOL.implies} $ t1 $ t2 =>
blanchet@45062
   164
         Implies (to_F (Option.map not pos) Ts t1, to_F pos Ts t2)
blanchet@46092
   165
       | Const (@{const_name Set.member}, _) $ t1 $ t2 => to_F pos Ts (t2 $ t1)
blanchet@45062
   166
       | t1 $ t2 =>
blanchet@45062
   167
         (case pos of
blanchet@45062
   168
            NONE => Subset (to_S_rep Ts t2, to_R_rep Ts t1)
blanchet@45062
   169
          | SOME pos =>
blanchet@45062
   170
            let
blanchet@45062
   171
              val kt1 = to_R_rep Ts t1
blanchet@45062
   172
              val kt2 = to_S_rep Ts t2
blanchet@45062
   173
              val kT = atom_seq_product_of S_Rep card (fastype_of1 (Ts, t2))
blanchet@45062
   174
            in
blanchet@45062
   175
              if pos then
blanchet@45062
   176
                Not (Subset (kt2, Difference (kT, Join (kt1, true_atom))))
blanchet@45062
   177
              else
blanchet@45062
   178
                Subset (kt2, Difference (kT, Join (kt1, false_atom)))
blanchet@45062
   179
            end)
blanchet@45062
   180
       | _ => raise SAME ())
blanchet@45062
   181
      handle SAME () => F_from_S_rep pos (to_R_rep Ts t)
blanchet@45035
   182
    and to_S_rep Ts t =
blanchet@45035
   183
      case t of
blanchet@45035
   184
        Const (@{const_name Pair}, _) $ t1 $ t2 =>
blanchet@45035
   185
        Product (to_S_rep Ts t1, to_S_rep Ts t2)
blanchet@45035
   186
      | Const (@{const_name Pair}, _) $ _ => to_S_rep Ts (eta_expand Ts t 1)
blanchet@45035
   187
      | Const (@{const_name Pair}, _) => to_S_rep Ts (eta_expand Ts t 2)
blanchet@45035
   188
      | Const (@{const_name fst}, _) $ t1 =>
blanchet@45035
   189
        let val fst_arity = arity_of S_Rep card (fastype_of1 (Ts, t)) in
blanchet@45035
   190
          Project (to_S_rep Ts t1, num_seq 0 fst_arity)
blanchet@45035
   191
        end
blanchet@45035
   192
      | Const (@{const_name fst}, _) => to_S_rep Ts (eta_expand Ts t 1)
blanchet@45035
   193
      | Const (@{const_name snd}, _) $ t1 =>
blanchet@45035
   194
        let
blanchet@45035
   195
          val pair_arity = arity_of S_Rep card (fastype_of1 (Ts, t1))
blanchet@45035
   196
          val snd_arity = arity_of S_Rep card (fastype_of1 (Ts, t))
blanchet@45035
   197
          val fst_arity = pair_arity - snd_arity
blanchet@45035
   198
        in Project (to_S_rep Ts t1, num_seq fst_arity snd_arity) end
blanchet@45035
   199
      | Const (@{const_name snd}, _) => to_S_rep Ts (eta_expand Ts t 1)
blanchet@45035
   200
      | Bound j => rel_expr_for_bound_var card S_Rep Ts j
blanchet@45035
   201
      | _ => S_rep_from_R_rep Ts (fastype_of1 (Ts, t)) (to_R_rep Ts t)
blanchet@45062
   202
    and partial_set_op swap1 swap2 op1 op2 Ts t1 t2 =
blanchet@45062
   203
      let
blanchet@45062
   204
        val kt1 = to_R_rep Ts t1
blanchet@45062
   205
        val kt2 = to_R_rep Ts t2
blanchet@45062
   206
        val (a11, a21) = (false_atom, true_atom) |> swap1 ? swap
blanchet@45062
   207
        val (a12, a22) = (false_atom, true_atom) |> swap2 ? swap
blanchet@45062
   208
      in
blanchet@45062
   209
        Union (Product (op1 (Join (kt1, a11), Join (kt2, a12)), true_atom),
blanchet@45062
   210
               Product (op2 (Join (kt1, a21), Join (kt2, a22)), false_atom))
blanchet@45062
   211
      end
blanchet@45035
   212
    and to_R_rep Ts t =
blanchet@45035
   213
      (case t of
blanchet@45035
   214
         @{const Not} => to_R_rep Ts (eta_expand Ts t 1)
blanchet@45035
   215
       | Const (@{const_name All}, _) => to_R_rep Ts (eta_expand Ts t 1)
blanchet@45035
   216
       | Const (@{const_name Ex}, _) => to_R_rep Ts (eta_expand Ts t 1)
blanchet@45035
   217
       | Const (@{const_name HOL.eq}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
blanchet@45035
   218
       | Const (@{const_name HOL.eq}, _) => to_R_rep Ts (eta_expand Ts t 2)
blanchet@45035
   219
       | Const (@{const_name ord_class.less_eq},
blanchet@45035
   220
                Type (@{type_name fun},
blanchet@45035
   221
                      [Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ =>
blanchet@45035
   222
         to_R_rep Ts (eta_expand Ts t 1)
blanchet@45035
   223
       | Const (@{const_name ord_class.less_eq}, _) =>
blanchet@45035
   224
         to_R_rep Ts (eta_expand Ts t 2)
blanchet@45035
   225
       | @{const HOL.conj} $ _ => to_R_rep Ts (eta_expand Ts t 1)
blanchet@45035
   226
       | @{const HOL.conj} => to_R_rep Ts (eta_expand Ts t 2)
blanchet@45035
   227
       | @{const HOL.disj} $ _ => to_R_rep Ts (eta_expand Ts t 1)
blanchet@45035
   228
       | @{const HOL.disj} => to_R_rep Ts (eta_expand Ts t 2)
blanchet@45035
   229
       | @{const HOL.implies} $ _ => to_R_rep Ts (eta_expand Ts t 1)
blanchet@45035
   230
       | @{const HOL.implies} => to_R_rep Ts (eta_expand Ts t 2)
blanchet@46092
   231
       | Const (@{const_name Set.member}, _) $ _ =>
blanchet@46092
   232
         to_R_rep Ts (eta_expand Ts t 1)
blanchet@46092
   233
       | Const (@{const_name Set.member}, _) => to_R_rep Ts (eta_expand Ts t 2)
blanchet@46092
   234
       | Const (@{const_name Collect}, _) $ t' => to_R_rep Ts t'
blanchet@46092
   235
       | Const (@{const_name Collect}, _) => to_R_rep Ts (eta_expand Ts t 1)
blanchet@45035
   236
       | Const (@{const_name bot_class.bot},
blanchet@45062
   237
                T as Type (@{type_name fun}, [T', @{typ bool}])) =>
blanchet@45062
   238
         if total then empty_n_ary_rel (arity_of (R_Rep total) card T)
blanchet@45062
   239
         else Product (atom_seq_product_of (R_Rep total) card T', false_atom)
blanchet@45062
   240
       | Const (@{const_name top_class.top},
blanchet@45062
   241
                T as Type (@{type_name fun}, [T', @{typ bool}])) =>
blanchet@45062
   242
         if total then atom_seq_product_of (R_Rep total) card T
blanchet@45062
   243
         else Product (atom_seq_product_of (R_Rep total) card T', true_atom)
blanchet@45062
   244
       | Const (@{const_name insert}, Type (_, [T, _])) $ t1 $ t2 =>
blanchet@45062
   245
         if total then
blanchet@45062
   246
           Union (to_S_rep Ts t1, to_R_rep Ts t2)
blanchet@45062
   247
         else
blanchet@45062
   248
           let
blanchet@45062
   249
             val kt1 = to_S_rep Ts t1
blanchet@45062
   250
             val kt2 = to_R_rep Ts t2
blanchet@45062
   251
           in
blanchet@45062
   252
             RelIf (Some kt1,
blanchet@45062
   253
                    if arity_of S_Rep card T = 1 then
blanchet@45062
   254
                      Override (kt2, Product (kt1, true_atom))
blanchet@45062
   255
                    else
blanchet@45062
   256
                      Union (Difference (kt2, Product (kt1, false_atom)),
blanchet@45062
   257
                             Product (kt1, true_atom)),
blanchet@45062
   258
                    Difference (kt2, Product (atom_seq_product_of S_Rep card T,
blanchet@45062
   259
                                              false_atom)))
blanchet@45062
   260
           end
blanchet@45035
   261
       | Const (@{const_name insert}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
blanchet@45035
   262
       | Const (@{const_name insert}, _) => to_R_rep Ts (eta_expand Ts t 2)
blanchet@45062
   263
       | Const (@{const_name trancl},
blanchet@45062
   264
                Type (_, [Type (_, [Type (_, [T', _]), _]), _])) $ t1 =>
blanchet@45062
   265
         if arity_of S_Rep card T' = 1 then
blanchet@45062
   266
           if total then
blanchet@45062
   267
             Closure (to_R_rep Ts t1)
blanchet@45062
   268
           else
blanchet@45062
   269
             let
blanchet@45062
   270
               val kt1 = to_R_rep Ts t1
blanchet@45062
   271
               val true_core_kt = Closure (Join (kt1, true_atom))
blanchet@45062
   272
               val kTx =
blanchet@45062
   273
                 atom_seq_product_of S_Rep card (HOLogic.mk_prodT (`I T'))
blanchet@45062
   274
               val false_mantle_kt =
blanchet@45062
   275
                 Difference (kTx,
blanchet@45062
   276
                     Closure (Difference (kTx, Join (kt1, false_atom))))
blanchet@45062
   277
             in
blanchet@45062
   278
               Union (Product (Difference (false_mantle_kt, true_core_kt),
blanchet@45062
   279
                               false_atom),
blanchet@45062
   280
                      Product (true_core_kt, true_atom))
blanchet@45062
   281
             end
blanchet@45035
   282
         else
blanchet@46092
   283
           error "Not supported: Transitive closure for function or pair type."
blanchet@45035
   284
       | Const (@{const_name trancl}, _) => to_R_rep Ts (eta_expand Ts t 1)
blanchet@45035
   285
       | Const (@{const_name inf_class.inf},
blanchet@45035
   286
                Type (@{type_name fun},
blanchet@45035
   287
                      [Type (@{type_name fun}, [_, @{typ bool}]), _]))
blanchet@45035
   288
         $ t1 $ t2 =>
blanchet@45062
   289
         if total then Intersect (to_R_rep Ts t1, to_R_rep Ts t2)
blanchet@45062
   290
         else partial_set_op true true Intersect Union Ts t1 t2
blanchet@45035
   291
       | Const (@{const_name inf_class.inf}, _) $ _ =>
blanchet@45035
   292
         to_R_rep Ts (eta_expand Ts t 1)
blanchet@45035
   293
       | Const (@{const_name inf_class.inf}, _) =>
blanchet@45035
   294
         to_R_rep Ts (eta_expand Ts t 2)
blanchet@45035
   295
       | Const (@{const_name sup_class.sup},
blanchet@45035
   296
                Type (@{type_name fun},
blanchet@45035
   297
                      [Type (@{type_name fun}, [_, @{typ bool}]), _]))
blanchet@45035
   298
         $ t1 $ t2 =>
blanchet@45062
   299
         if total then Union (to_R_rep Ts t1, to_R_rep Ts t2)
blanchet@45062
   300
         else partial_set_op true true Union Intersect Ts t1 t2
blanchet@45035
   301
       | Const (@{const_name sup_class.sup}, _) $ _ =>
blanchet@45035
   302
         to_R_rep Ts (eta_expand Ts t 1)
blanchet@45035
   303
       | Const (@{const_name sup_class.sup}, _) =>
blanchet@45035
   304
         to_R_rep Ts (eta_expand Ts t 2)
blanchet@45035
   305
       | Const (@{const_name minus_class.minus},
blanchet@45035
   306
                Type (@{type_name fun},
blanchet@45035
   307
                      [Type (@{type_name fun}, [_, @{typ bool}]), _]))
blanchet@45035
   308
         $ t1 $ t2 =>
blanchet@45062
   309
         if total then Difference (to_R_rep Ts t1, to_R_rep Ts t2)
blanchet@45062
   310
         else partial_set_op true false Intersect Union Ts t1 t2
blanchet@45035
   311
       | Const (@{const_name minus_class.minus},
blanchet@45035
   312
                Type (@{type_name fun},
blanchet@45035
   313
                      [Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ =>
blanchet@45035
   314
         to_R_rep Ts (eta_expand Ts t 1)
blanchet@45035
   315
       | Const (@{const_name minus_class.minus},
blanchet@45035
   316
                Type (@{type_name fun},
blanchet@45035
   317
                      [Type (@{type_name fun}, [_, @{typ bool}]), _])) =>
blanchet@45035
   318
         to_R_rep Ts (eta_expand Ts t 2)
blanchet@45062
   319
       | Const (@{const_name Pair}, _) $ _ $ _ => to_S_rep Ts t
blanchet@45062
   320
       | Const (@{const_name Pair}, _) $ _ => to_S_rep Ts t
blanchet@45062
   321
       | Const (@{const_name Pair}, _) => to_S_rep Ts t
blanchet@45035
   322
       | Const (@{const_name fst}, _) $ _ => raise SAME ()
blanchet@45035
   323
       | Const (@{const_name fst}, _) => raise SAME ()
blanchet@45035
   324
       | Const (@{const_name snd}, _) $ _ => raise SAME ()
blanchet@45035
   325
       | Const (@{const_name snd}, _) => raise SAME ()
blanchet@45062
   326
       | @{const False} => false_atom
blanchet@45062
   327
       | @{const True} => true_atom
blanchet@45035
   328
       | Free (x as (_, T)) =>
blanchet@45062
   329
         Rel (arity_of (R_Rep total) card T, find_index (curry (op =) x) frees)
blanchet@46092
   330
       | Term.Var _ => error "Not supported: Schematic variables."
blanchet@45035
   331
       | Bound _ => raise SAME ()
blanchet@45035
   332
       | Abs (_, T, t') =>
blanchet@45062
   333
         (case (total, fastype_of1 (T :: Ts, t')) of
blanchet@45062
   334
            (true, @{typ bool}) =>
blanchet@45062
   335
            Comprehension (decls_for S_Rep card Ts T, to_F NONE (T :: Ts) t')
blanchet@45062
   336
          | (_, T') =>
blanchet@45062
   337
            Comprehension (decls_for S_Rep card Ts T @
blanchet@45062
   338
                           decls_for (R_Rep total) card (T :: Ts) T',
blanchet@45062
   339
                           Subset (rel_expr_for_bound_var card (R_Rep total)
blanchet@45062
   340
                                                          (T' :: T :: Ts) 0,
blanchet@45062
   341
                                   to_R_rep (T :: Ts) t')))
blanchet@45035
   342
       | t1 $ t2 =>
blanchet@45035
   343
         (case fastype_of1 (Ts, t) of
blanchet@45062
   344
            @{typ bool} =>
blanchet@45062
   345
            if total then
blanchet@45062
   346
              S_rep_from_F NONE (to_F NONE Ts t)
blanchet@45062
   347
            else
blanchet@45062
   348
              RelIf (to_F (SOME true) Ts t, true_atom,
blanchet@45062
   349
                     RelIf (Not (to_F (SOME false) Ts t), false_atom,
blanchet@45062
   350
                     None))
blanchet@45035
   351
          | T =>
blanchet@45035
   352
            let val T2 = fastype_of1 (Ts, t2) in
blanchet@45035
   353
              case arity_of S_Rep card T2 of
blanchet@45035
   354
                1 => Join (to_S_rep Ts t2, to_R_rep Ts t1)
blanchet@45035
   355
              | arity2 =>
blanchet@45062
   356
                let val res_arity = arity_of (R_Rep total) card T in
blanchet@45035
   357
                  Project (Intersect
blanchet@45035
   358
                      (Product (to_S_rep Ts t2,
blanchet@45062
   359
                                atom_seq_product_of (R_Rep total) card T),
blanchet@45035
   360
                       to_R_rep Ts t1),
blanchet@45035
   361
                      num_seq arity2 res_arity)
blanchet@45035
   362
                end
blanchet@45035
   363
            end)
blanchet@46092
   364
       | _ => error ("Not supported: Term " ^
blanchet@46092
   365
                     quote (Syntax.string_of_term ctxt t) ^ "."))
blanchet@45035
   366
      handle SAME () => R_rep_from_S_rep (fastype_of1 (Ts, t)) (to_S_rep Ts t)
blanchet@45062
   367
  in to_F (if total then NONE else SOME true) [] end
blanchet@45035
   368
blanchet@45062
   369
fun bound_for_free total card i (s, T) =
blanchet@45062
   370
  let val js = atom_schema_of (R_Rep total) card T in
blanchet@45035
   371
    ([((length js, i), s)],
blanchet@45062
   372
     [TupleSet [], atom_schema_of (R_Rep total) card T |> map (rpair 0)
blanchet@45035
   373
                   |> tuple_set_from_atom_schema])
blanchet@45035
   374
  end
blanchet@45035
   375
blanchet@45062
   376
fun declarative_axiom_for_rel_expr total card Ts
blanchet@45062
   377
                                   (Type (@{type_name fun}, [T1, T2])) r =
blanchet@45062
   378
    if total andalso body_type T2 = bool_T then
blanchet@45035
   379
      True
blanchet@45035
   380
    else
blanchet@45035
   381
      All (decls_for S_Rep card Ts T1,
blanchet@45062
   382
           declarative_axiom_for_rel_expr total card (T1 :: Ts) T2
blanchet@45035
   383
               (List.foldl Join r (vars_for_bound_var card S_Rep (T1 :: Ts) 0)))
blanchet@45062
   384
  | declarative_axiom_for_rel_expr total _ _ _ r =
blanchet@45062
   385
    (if total then One else Lone) r
blanchet@45062
   386
fun declarative_axiom_for_free total card i (_, T) =
blanchet@45062
   387
  declarative_axiom_for_rel_expr total card [] T
blanchet@45062
   388
      (Rel (arity_of (R_Rep total) card T, i))
blanchet@45035
   389
blanchet@46092
   390
(* Hack to make the old code work as is with sets. *)
blanchet@46092
   391
fun unsetify_type (Type (@{type_name set}, [T])) = unsetify_type T --> bool_T
blanchet@46092
   392
  | unsetify_type (Type (s, Ts)) = Type (s, map unsetify_type Ts)
blanchet@46092
   393
  | unsetify_type T = T
blanchet@46092
   394
blanchet@45062
   395
fun kodkod_problem_from_term ctxt total raw_card raw_infinite t =
blanchet@45035
   396
  let
wenzelm@45128
   397
    val thy = Proof_Context.theory_of ctxt
blanchet@45035
   398
    fun card (Type (@{type_name fun}, [T1, T2])) =
blanchet@45035
   399
        reasonable_power (card T2) (card T1)
blanchet@45035
   400
      | card (Type (@{type_name prod}, [T1, T2])) = card T1 * card T2
blanchet@45035
   401
      | card @{typ bool} = 2
blanchet@45035
   402
      | card T = Int.max (1, raw_card T)
blanchet@45062
   403
    fun complete (Type (@{type_name fun}, [T1, T2])) =
blanchet@45062
   404
        concrete T1 andalso complete T2
blanchet@45062
   405
      | complete (Type (@{type_name prod}, Ts)) = forall complete Ts
blanchet@45062
   406
      | complete T = not (raw_infinite T)
blanchet@45062
   407
    and concrete (Type (@{type_name fun}, [T1, T2])) =
blanchet@45062
   408
        complete T1 andalso concrete T2
blanchet@45062
   409
      | concrete (Type (@{type_name prod}, Ts)) = forall concrete Ts
blanchet@45062
   410
      | concrete _ = true
blanchet@46092
   411
    val neg_t =
blanchet@46092
   412
      @{const Not} $ Object_Logic.atomize_term thy t
blanchet@46092
   413
      |> map_types unsetify_type
blanchet@45062
   414
    val _ = fold_types (K o check_type ctxt raw_infinite) neg_t ()
blanchet@45035
   415
    val frees = Term.add_frees neg_t []
blanchet@45062
   416
    val bounds =
blanchet@45062
   417
      map2 (bound_for_free total card) (index_seq 0 (length frees)) frees
blanchet@45035
   418
    val declarative_axioms =
blanchet@45062
   419
      map2 (declarative_axiom_for_free total card)
blanchet@45062
   420
           (index_seq 0 (length frees)) frees
blanchet@45062
   421
    val formula =
blanchet@45062
   422
      neg_t |> kodkod_formula_from_term ctxt total card complete concrete frees 
blanchet@45062
   423
            |> fold_rev (curry And) declarative_axioms
blanchet@45035
   424
    val univ_card = univ_card 0 0 0 bounds formula
blanchet@45035
   425
  in
blanchet@45035
   426
    {comment = "", settings = [], univ_card = univ_card, tuple_assigns = [],
blanchet@45035
   427
     bounds = bounds, int_bounds = [], expr_assigns = [], formula = formula}
blanchet@45035
   428
  end
blanchet@45035
   429
blanchet@45035
   430
fun solve_any_kodkod_problem thy problems =
blanchet@45035
   431
  let
blanchet@55199
   432
    val {debug, overlord, timeout, ...} = Nitpick_Commands.default_params thy []
blanchet@45035
   433
    val max_threads = 1
blanchet@45035
   434
    val max_solutions = 1
blanchet@45035
   435
  in
blanchet@54845
   436
    case solve_any_problem debug overlord timeout max_threads max_solutions
blanchet@45035
   437
                           problems of
blanchet@49026
   438
      JavaNotFound => "unknown"
blanchet@45035
   439
    | JavaTooOld => "unknown"
blanchet@45035
   440
    | KodkodiNotInstalled => "unknown"
blanchet@50487
   441
    | KodkodiTooOld => "unknown"
blanchet@45035
   442
    | Normal ([], _, _) => "none"
blanchet@45035
   443
    | Normal _ => "genuine"
blanchet@45035
   444
    | TimedOut _ => "unknown"
blanchet@45035
   445
    | Error (s, _) => error ("Kodkod error: " ^ s)
blanchet@45035
   446
  end
blanchet@45035
   447
blanchet@45062
   448
val default_raw_infinite = member (op =) [@{typ nat}, @{typ int}]
blanchet@45062
   449
blanchet@45062
   450
fun minipick ctxt n t =
blanchet@45062
   451
  let
wenzelm@45128
   452
    val thy = Proof_Context.theory_of ctxt
blanchet@55199
   453
    val {total_consts, ...} = Nitpick_Commands.default_params thy []
blanchet@45062
   454
    val totals =
blanchet@45062
   455
      total_consts |> Option.map single |> the_default [true, false]
blanchet@45062
   456
    fun problem_for (total, k) =
blanchet@45062
   457
      kodkod_problem_from_term ctxt total (K k) default_raw_infinite t
blanchet@45062
   458
  in
blanchet@55208
   459
    (totals, 1 upto n)
blanchet@45062
   460
    |-> map_product pair
blanchet@45062
   461
    |> map problem_for
blanchet@45062
   462
    |> solve_any_kodkod_problem (Proof_Context.theory_of ctxt)
blanchet@45062
   463
  end
blanchet@45062
   464
blanchet@45062
   465
fun minipick_expect ctxt expect n t =
blanchet@45062
   466
  if getenv "KODKODI" <> "" then
blanchet@45062
   467
    if minipick ctxt n t = expect then ()
blanchet@45062
   468
    else error ("\"minipick_expect\" expected " ^ quote expect)
blanchet@45062
   469
  else
blanchet@45062
   470
    ()
blanchet@45062
   471
blanchet@45035
   472
end;