isabelle: src/HOL/Nitpick_Examples/minipick.ML@1e9e68247ad1

     1 (*  Title:      HOL/Nitpick_Examples/minipick.ML

     2     Author:     Jasmin Blanchette, TU Muenchen

     3     Copyright   2009-2010

     5 Finite model generation for HOL formulas using Kodkod, minimalistic version.

     6 *)

     8 signature MINIPICK =

     9 sig

    10   val minipick : Proof.context -> int -> term -> string

    11   val minipick_expect : Proof.context -> string -> int -> term -> unit

    12 end;

    14 structure Minipick : MINIPICK =

    15 struct

    17 open Kodkod

    18 open Nitpick_Util

    19 open Nitpick_HOL

    20 open Nitpick_Peephole

    21 open Nitpick_Kodkod

    23 datatype rep =

    24   S_Rep |

    25   R_Rep of bool

    27 fun check_type ctxt raw_infinite (Type (@{type_name fun}, Ts)) =

    28     List.app (check_type ctxt raw_infinite) Ts

    29   | check_type ctxt raw_infinite (Type (@{type_name prod}, Ts)) =

    30     List.app (check_type ctxt raw_infinite) Ts

    31   | check_type _ _ @{typ bool} = ()

    32   | check_type _ _ (TFree (_, @{sort "{}"})) = ()

    33   | check_type _ _ (TFree (_, @{sort HOL.type})) = ()

    34   | check_type ctxt raw_infinite T =

    35     if raw_infinite T then

    36       ()

    37     else

    38       error ("Not supported: Type " ^ quote (Syntax.string_of_typ ctxt T) ^ ".")

    40 fun atom_schema_of S_Rep card (Type (@{type_name fun}, [T1, T2])) =

    41     replicate_list (card T1) (atom_schema_of S_Rep card T2)

    42   | atom_schema_of (R_Rep true) card

    43                    (Type (@{type_name fun}, [T1, @{typ bool}])) =

    44     atom_schema_of S_Rep card T1

    45   | atom_schema_of (rep as R_Rep _) card (Type (@{type_name fun}, [T1, T2])) =

    46     atom_schema_of S_Rep card T1 @ atom_schema_of rep card T2

    47   | atom_schema_of _ card (Type (@{type_name prod}, Ts)) =

    48     maps (atom_schema_of S_Rep card) Ts

    49   | atom_schema_of _ card T = [card T]

    50 val arity_of = length ooo atom_schema_of

    51 val atom_seqs_of = map (AtomSeq o rpair 0) ooo atom_schema_of

    52 val atom_seq_product_of = foldl1 Product ooo atom_seqs_of

    54 fun index_for_bound_var _ [_] 0 = 0

    55   | index_for_bound_var card (_ :: Ts) 0 =

    56     index_for_bound_var card Ts 0 + arity_of S_Rep card (hd Ts)

    57   | index_for_bound_var card Ts n = index_for_bound_var card (tl Ts) (n - 1)

    58 fun vars_for_bound_var card R Ts j =

    59   map (curry Var 1) (index_seq (index_for_bound_var card Ts j)

    60                                (arity_of R card (nth Ts j)))

    61 val rel_expr_for_bound_var = foldl1 Product oooo vars_for_bound_var

    62 fun decls_for R card Ts T =

    63   map2 (curry DeclOne o pair 1)

    64        (index_seq (index_for_bound_var card (T :: Ts) 0)

    65                   (arity_of R card (nth (T :: Ts) 0)))

    66        (atom_seqs_of R card T)

    68 val atom_product = foldl1 Product o map Atom

    70 val false_atom_num = 0

    71 val true_atom_num = 1

    72 val false_atom = Atom false_atom_num

    73 val true_atom = Atom true_atom_num

    75 fun kodkod_formula_from_term ctxt total card complete concrete frees =

    76   let

    77     fun F_from_S_rep (SOME false) r = Not (RelEq (r, false_atom))

    78       | F_from_S_rep _ r = RelEq (r, true_atom)

    79     fun S_rep_from_F NONE f = RelIf (f, true_atom, false_atom)

    80       | S_rep_from_F (SOME true) f = RelIf (f, true_atom, None)

    81       | S_rep_from_F (SOME false) f = RelIf (Not f, false_atom, None)

    82     fun R_rep_from_S_rep (Type (@{type_name fun}, [T1, T2])) r =

    83         if total andalso T2 = bool_T then

    84           let

    85             val jss = atom_schema_of S_Rep card T1 |> map (rpair 0)

    86                       |> all_combinations

    87           in

    88             map2 (fn i => fn js =>

    89 (*

    90                      RelIf (F_from_S_rep NONE (Project (r, [Num i])),

    91                             atom_product js, empty_n_ary_rel (length js))

    92 *)

    93                      Join (Project (r, [Num i]),

    94                            atom_product (false_atom_num :: js))

    95                  ) (index_seq 0 (length jss)) jss

    96             |> foldl1 Union

    97           end

    98         else

    99           let

   100             val jss = atom_schema_of S_Rep card T1 |> map (rpair 0)

   101                       |> all_combinations

   102             val arity2 = arity_of S_Rep card T2

   103           in

   104             map2 (fn i => fn js =>

   105                      Product (atom_product js,

   106                               Project (r, num_seq (i * arity2) arity2)

   107                               |> R_rep_from_S_rep T2))

   108                  (index_seq 0 (length jss)) jss

   109             |> foldl1 Union

   110           end

   111       | R_rep_from_S_rep _ r = r

   112     fun S_rep_from_R_rep Ts (T as Type (@{type_name fun}, _)) r =

   113         Comprehension (decls_for S_Rep card Ts T,

   114             RelEq (R_rep_from_S_rep T

   115                        (rel_expr_for_bound_var card S_Rep (T :: Ts) 0), r))

   116       | S_rep_from_R_rep _ _ r = r

   117     fun partial_eq pos Ts (Type (@{type_name fun}, [T1, T2])) t1 t2 =

   118         HOLogic.mk_all ("x", T1,

   119                         HOLogic.eq_const T2 $ (incr_boundvars 1 t1 $ Bound 0)

   120                         $ (incr_boundvars 1 t2 $ Bound 0))

   121         |> to_F (SOME pos) Ts

   122       | partial_eq pos Ts T t1 t2 =

   123         if pos andalso not (concrete T) then

   124           False

   125         else

   126           (t1, t2) |> pairself (to_R_rep Ts)

   127                    |> (if pos then Some o Intersect else Lone o Union)

   128     and to_F pos Ts t =

   129       (case t of

   130          @{const Not} $ t1 => Not (to_F (Option.map not pos) Ts t1)

   131        | @{const False} => False

   132        | @{const True} => True

   133        | Const (@{const_name All}, _) $ Abs (_, T, t') =>

   134          if pos = SOME true andalso not (complete T) then False

   135          else All (decls_for S_Rep card Ts T, to_F pos (T :: Ts) t')

   136        | (t0 as Const (@{const_name All}, _)) $ t1 =>

   137          to_F pos Ts (t0 $ eta_expand Ts t1 1)

   138        | Const (@{const_name Ex}, _) $ Abs (_, T, t') =>

   139          if pos = SOME false andalso not (complete T) then True

   140          else Exist (decls_for S_Rep card Ts T, to_F pos (T :: Ts) t')

   141        | (t0 as Const (@{const_name Ex}, _)) $ t1 =>

   142          to_F pos Ts (t0 $ eta_expand Ts t1 1)

   143        | Const (@{const_name HOL.eq}, Type (_, [T, _])) $ t1 $ t2 =>

   144          (case pos of

   145             NONE => RelEq (to_R_rep Ts t1, to_R_rep Ts t2)

   146           | SOME pos => partial_eq pos Ts T t1 t2)

   147        | Const (@{const_name ord_class.less_eq},

   148                 Type (@{type_name fun},

   149                       [Type (@{type_name fun}, [T', @{typ bool}]), _]))

   150          $ t1 $ t2 =>

   151          (case pos of

   152             NONE => Subset (to_R_rep Ts t1, to_R_rep Ts t2)

   153           | SOME true =>

   154             Subset (Difference (atom_seq_product_of S_Rep card T',

   155                                 Join (to_R_rep Ts t1, false_atom)),

   156                     Join (to_R_rep Ts t2, true_atom))

   157           | SOME false =>

   158             Subset (Join (to_R_rep Ts t1, true_atom),

   159                     Difference (atom_seq_product_of S_Rep card T',

   160                                 Join (to_R_rep Ts t2, false_atom))))

   161        | @{const HOL.conj} $ t1 $ t2 => And (to_F pos Ts t1, to_F pos Ts t2)

   162        | @{const HOL.disj} $ t1 $ t2 => Or (to_F pos Ts t1, to_F pos Ts t2)

   163        | @{const HOL.implies} $ t1 $ t2 =>

   164          Implies (to_F (Option.map not pos) Ts t1, to_F pos Ts t2)

   165        | Const (@{const_name Set.member}, _) $ t1 $ t2 => to_F pos Ts (t2 $ t1)

   166        | t1 $ t2 =>

   167          (case pos of

   168             NONE => Subset (to_S_rep Ts t2, to_R_rep Ts t1)

   169           | SOME pos =>

   170             let

   171               val kt1 = to_R_rep Ts t1

   172               val kt2 = to_S_rep Ts t2

   173               val kT = atom_seq_product_of S_Rep card (fastype_of1 (Ts, t2))

   174             in

   175               if pos then

   176                 Not (Subset (kt2, Difference (kT, Join (kt1, true_atom))))

   177               else

   178                 Subset (kt2, Difference (kT, Join (kt1, false_atom)))

   179             end)

   180        | _ => raise SAME ())

   181       handle SAME () => F_from_S_rep pos (to_R_rep Ts t)

   182     and to_S_rep Ts t =

   183       case t of

   184         Const (@{const_name Pair}, _) $ t1 $ t2 =>

   185         Product (to_S_rep Ts t1, to_S_rep Ts t2)

   186       | Const (@{const_name Pair}, _) $ _ => to_S_rep Ts (eta_expand Ts t 1)

   187       | Const (@{const_name Pair}, _) => to_S_rep Ts (eta_expand Ts t 2)

   188       | Const (@{const_name fst}, _) $ t1 =>

   189         let val fst_arity = arity_of S_Rep card (fastype_of1 (Ts, t)) in

   190           Project (to_S_rep Ts t1, num_seq 0 fst_arity)

   191         end

   192       | Const (@{const_name fst}, _) => to_S_rep Ts (eta_expand Ts t 1)

   193       | Const (@{const_name snd}, _) $ t1 =>

   194         let

   195           val pair_arity = arity_of S_Rep card (fastype_of1 (Ts, t1))

   196           val snd_arity = arity_of S_Rep card (fastype_of1 (Ts, t))

   197           val fst_arity = pair_arity - snd_arity

   198         in Project (to_S_rep Ts t1, num_seq fst_arity snd_arity) end

   199       | Const (@{const_name snd}, _) => to_S_rep Ts (eta_expand Ts t 1)

   200       | Bound j => rel_expr_for_bound_var card S_Rep Ts j

   201       | _ => S_rep_from_R_rep Ts (fastype_of1 (Ts, t)) (to_R_rep Ts t)

   202     and partial_set_op swap1 swap2 op1 op2 Ts t1 t2 =

   203       let

   204         val kt1 = to_R_rep Ts t1

   205         val kt2 = to_R_rep Ts t2

   206         val (a11, a21) = (false_atom, true_atom) |> swap1 ? swap

   207         val (a12, a22) = (false_atom, true_atom) |> swap2 ? swap

   208       in

   209         Union (Product (op1 (Join (kt1, a11), Join (kt2, a12)), true_atom),

   210                Product (op2 (Join (kt1, a21), Join (kt2, a22)), false_atom))

   211       end

   212     and to_R_rep Ts t =

   213       (case t of

   214          @{const Not} => to_R_rep Ts (eta_expand Ts t 1)

   215        | Const (@{const_name All}, _) => to_R_rep Ts (eta_expand Ts t 1)

   216        | Const (@{const_name Ex}, _) => to_R_rep Ts (eta_expand Ts t 1)

   217        | Const (@{const_name HOL.eq}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)

   218        | Const (@{const_name HOL.eq}, _) => to_R_rep Ts (eta_expand Ts t 2)

   219        | Const (@{const_name ord_class.less_eq},

   220                 Type (@{type_name fun},

   221                       [Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ =>

   222          to_R_rep Ts (eta_expand Ts t 1)

   223        | Const (@{const_name ord_class.less_eq}, _) =>

   224          to_R_rep Ts (eta_expand Ts t 2)

   225        | @{const HOL.conj} $ _ => to_R_rep Ts (eta_expand Ts t 1)

   226        | @{const HOL.conj} => to_R_rep Ts (eta_expand Ts t 2)

   227        | @{const HOL.disj} $ _ => to_R_rep Ts (eta_expand Ts t 1)

   228        | @{const HOL.disj} => to_R_rep Ts (eta_expand Ts t 2)

   229        | @{const HOL.implies} $ _ => to_R_rep Ts (eta_expand Ts t 1)

   230        | @{const HOL.implies} => to_R_rep Ts (eta_expand Ts t 2)

   231        | Const (@{const_name Set.member}, _) $ _ =>

   232          to_R_rep Ts (eta_expand Ts t 1)

   233        | Const (@{const_name Set.member}, _) => to_R_rep Ts (eta_expand Ts t 2)

   234        | Const (@{const_name Collect}, _) $ t' => to_R_rep Ts t'

   235        | Const (@{const_name Collect}, _) => to_R_rep Ts (eta_expand Ts t 1)

   236        | Const (@{const_name bot_class.bot},

   237                 T as Type (@{type_name fun}, [T', @{typ bool}])) =>

   238          if total then empty_n_ary_rel (arity_of (R_Rep total) card T)

   239          else Product (atom_seq_product_of (R_Rep total) card T', false_atom)

   240        | Const (@{const_name top_class.top},

   241                 T as Type (@{type_name fun}, [T', @{typ bool}])) =>

   242          if total then atom_seq_product_of (R_Rep total) card T

   243          else Product (atom_seq_product_of (R_Rep total) card T', true_atom)

   244        | Const (@{const_name insert}, Type (_, [T, _])) $ t1 $ t2 =>

   245          if total then

   246            Union (to_S_rep Ts t1, to_R_rep Ts t2)

   247          else

   248            let

   249              val kt1 = to_S_rep Ts t1

   250              val kt2 = to_R_rep Ts t2

   251            in

   252              RelIf (Some kt1,

   253                     if arity_of S_Rep card T = 1 then

   254                       Override (kt2, Product (kt1, true_atom))

   255                     else

   256                       Union (Difference (kt2, Product (kt1, false_atom)),

   257                              Product (kt1, true_atom)),

   258                     Difference (kt2, Product (atom_seq_product_of S_Rep card T,

   259                                               false_atom)))

   260            end

   261        | Const (@{const_name insert}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)

   262        | Const (@{const_name insert}, _) => to_R_rep Ts (eta_expand Ts t 2)

   263        | Const (@{const_name trancl},

   264                 Type (_, [Type (_, [Type (_, [T', _]), _]), _])) $ t1 =>

   265          if arity_of S_Rep card T' = 1 then

   266            if total then

   267              Closure (to_R_rep Ts t1)

   268            else

   269              let

   270                val kt1 = to_R_rep Ts t1

   271                val true_core_kt = Closure (Join (kt1, true_atom))

   272                val kTx =

   273                  atom_seq_product_of S_Rep card (HOLogic.mk_prodT (`I T'))

   274                val false_mantle_kt =

   275                  Difference (kTx,

   276                      Closure (Difference (kTx, Join (kt1, false_atom))))

   277              in

   278                Union (Product (Difference (false_mantle_kt, true_core_kt),

   279                                false_atom),

   280                       Product (true_core_kt, true_atom))

   281              end

   282          else

   283            error "Not supported: Transitive closure for function or pair type."

   284        | Const (@{const_name trancl}, _) => to_R_rep Ts (eta_expand Ts t 1)

   285        | Const (@{const_name inf_class.inf},

   286                 Type (@{type_name fun},

   287                       [Type (@{type_name fun}, [_, @{typ bool}]), _]))

   288          $ t1 $ t2 =>

   289          if total then Intersect (to_R_rep Ts t1, to_R_rep Ts t2)

   290          else partial_set_op true true Intersect Union Ts t1 t2

   291        | Const (@{const_name inf_class.inf}, _) $ _ =>

   292          to_R_rep Ts (eta_expand Ts t 1)

   293        | Const (@{const_name inf_class.inf}, _) =>

   294          to_R_rep Ts (eta_expand Ts t 2)

   295        | Const (@{const_name sup_class.sup},

   296                 Type (@{type_name fun},

   297                       [Type (@{type_name fun}, [_, @{typ bool}]), _]))

   298          $ t1 $ t2 =>

   299          if total then Union (to_R_rep Ts t1, to_R_rep Ts t2)

   300          else partial_set_op true true Union Intersect Ts t1 t2

   301        | Const (@{const_name sup_class.sup}, _) $ _ =>

   302          to_R_rep Ts (eta_expand Ts t 1)

   303        | Const (@{const_name sup_class.sup}, _) =>

   304          to_R_rep Ts (eta_expand Ts t 2)

   305        | Const (@{const_name minus_class.minus},

   306                 Type (@{type_name fun},

   307                       [Type (@{type_name fun}, [_, @{typ bool}]), _]))

   308          $ t1 $ t2 =>

   309          if total then Difference (to_R_rep Ts t1, to_R_rep Ts t2)

   310          else partial_set_op true false Intersect Union Ts t1 t2

   311        | Const (@{const_name minus_class.minus},

   312                 Type (@{type_name fun},

   313                       [Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ =>

   314          to_R_rep Ts (eta_expand Ts t 1)

   315        | Const (@{const_name minus_class.minus},

   316                 Type (@{type_name fun},

   317                       [Type (@{type_name fun}, [_, @{typ bool}]), _])) =>

   318          to_R_rep Ts (eta_expand Ts t 2)

   319        | Const (@{const_name Pair}, _) $ _ $ _ => to_S_rep Ts t

   320        | Const (@{const_name Pair}, _) $ _ => to_S_rep Ts t

   321        | Const (@{const_name Pair}, _) => to_S_rep Ts t

   322        | Const (@{const_name fst}, _) $ _ => raise SAME ()

   323        | Const (@{const_name fst}, _) => raise SAME ()

   324        | Const (@{const_name snd}, _) $ _ => raise SAME ()

   325        | Const (@{const_name snd}, _) => raise SAME ()

   326        | @{const False} => false_atom

   327        | @{const True} => true_atom

   328        | Free (x as (_, T)) =>

   329          Rel (arity_of (R_Rep total) card T, find_index (curry (op =) x) frees)

   330        | Term.Var _ => error "Not supported: Schematic variables."

   331        | Bound _ => raise SAME ()

   332        | Abs (_, T, t') =>

   333          (case (total, fastype_of1 (T :: Ts, t')) of

   334             (true, @{typ bool}) =>

   335             Comprehension (decls_for S_Rep card Ts T, to_F NONE (T :: Ts) t')

   336           | (_, T') =>

   337             Comprehension (decls_for S_Rep card Ts T @

   338                            decls_for (R_Rep total) card (T :: Ts) T',

   339                            Subset (rel_expr_for_bound_var card (R_Rep total)

   340                                                           (T' :: T :: Ts) 0,

   341                                    to_R_rep (T :: Ts) t')))

   342        | t1 $ t2 =>

   343          (case fastype_of1 (Ts, t) of

   344             @{typ bool} =>

   345             if total then

   346               S_rep_from_F NONE (to_F NONE Ts t)

   347             else

   348               RelIf (to_F (SOME true) Ts t, true_atom,

   349                      RelIf (Not (to_F (SOME false) Ts t), false_atom,

   350                      None))

   351           | T =>

   352             let val T2 = fastype_of1 (Ts, t2) in

   353               case arity_of S_Rep card T2 of

   354                 1 => Join (to_S_rep Ts t2, to_R_rep Ts t1)

   355               | arity2 =>

   356                 let val res_arity = arity_of (R_Rep total) card T in

   357                   Project (Intersect

   358                       (Product (to_S_rep Ts t2,

   359                                 atom_seq_product_of (R_Rep total) card T),

   360                        to_R_rep Ts t1),

   361                       num_seq arity2 res_arity)

   362                 end

   363             end)

   364        | _ => error ("Not supported: Term " ^

   365                      quote (Syntax.string_of_term ctxt t) ^ "."))

   366       handle SAME () => R_rep_from_S_rep (fastype_of1 (Ts, t)) (to_S_rep Ts t)

   367   in to_F (if total then NONE else SOME true) [] end

   369 fun bound_for_free total card i (s, T) =

   370   let val js = atom_schema_of (R_Rep total) card T in

   371     ([((length js, i), s)],

   372      [TupleSet [], atom_schema_of (R_Rep total) card T |> map (rpair 0)

   373                    |> tuple_set_from_atom_schema])

   374   end

   376 fun declarative_axiom_for_rel_expr total card Ts

   377                                    (Type (@{type_name fun}, [T1, T2])) r =

   378     if total andalso body_type T2 = bool_T then

   379       True

   380     else

   381       All (decls_for S_Rep card Ts T1,

   382            declarative_axiom_for_rel_expr total card (T1 :: Ts) T2

   383                (List.foldl Join r (vars_for_bound_var card S_Rep (T1 :: Ts) 0)))

   384   | declarative_axiom_for_rel_expr total _ _ _ r =

   385     (if total then One else Lone) r

   386 fun declarative_axiom_for_free total card i (_, T) =

   387   declarative_axiom_for_rel_expr total card [] T

   388       (Rel (arity_of (R_Rep total) card T, i))

   390 (* Hack to make the old code work as is with sets. *)

   391 fun unsetify_type (Type (@{type_name set}, [T])) = unsetify_type T --> bool_T

   392   | unsetify_type (Type (s, Ts)) = Type (s, map unsetify_type Ts)

   393   | unsetify_type T = T

   395 fun kodkod_problem_from_term ctxt total raw_card raw_infinite t =

   396   let

   397     val thy = Proof_Context.theory_of ctxt

   398     fun card (Type (@{type_name fun}, [T1, T2])) =

   399         reasonable_power (card T2) (card T1)

   400       | card (Type (@{type_name prod}, [T1, T2])) = card T1 * card T2

   401       | card @{typ bool} = 2

   402       | card T = Int.max (1, raw_card T)

   403     fun complete (Type (@{type_name fun}, [T1, T2])) =

   404         concrete T1 andalso complete T2

   405       | complete (Type (@{type_name prod}, Ts)) = forall complete Ts

   406       | complete T = not (raw_infinite T)

   407     and concrete (Type (@{type_name fun}, [T1, T2])) =

   408         complete T1 andalso concrete T2

   409       | concrete (Type (@{type_name prod}, Ts)) = forall concrete Ts

   410       | concrete _ = true

   411     val neg_t =

   412       @{const Not} $ Object_Logic.atomize_term thy t

   413       |> map_types unsetify_type

   414     val _ = fold_types (K o check_type ctxt raw_infinite) neg_t ()

   415     val frees = Term.add_frees neg_t []

   416     val bounds =

   417       map2 (bound_for_free total card) (index_seq 0 (length frees)) frees

   418     val declarative_axioms =

   419       map2 (declarative_axiom_for_free total card)

   420            (index_seq 0 (length frees)) frees

   421     val formula =

   422       neg_t |> kodkod_formula_from_term ctxt total card complete concrete frees

   423             |> fold_rev (curry And) declarative_axioms

   424     val univ_card = univ_card 0 0 0 bounds formula

   425   in

   426     {comment = "", settings = [], univ_card = univ_card, tuple_assigns = [],

   427      bounds = bounds, int_bounds = [], expr_assigns = [], formula = formula}

   428   end

   430 fun solve_any_kodkod_problem thy problems =

   431   let

   432     val {debug, overlord, ...} = Nitpick_Isar.default_params thy []

   433     val max_threads = 1

   434     val max_solutions = 1

   435   in

   436     case solve_any_problem debug overlord NONE max_threads max_solutions

   437                            problems of

   438       JavaNotFound => "unknown"

   439     | JavaTooOld => "unknown"

   440     | KodkodiNotInstalled => "unknown"

   441     | KodkodiTooOld => "unknown"

   442     | Normal ([], _, _) => "none"

   443     | Normal _ => "genuine"

   444     | TimedOut _ => "unknown"

   445     | Error (s, _) => error ("Kodkod error: " ^ s)

   446   end

   448 val default_raw_infinite = member (op =) [@{typ nat}, @{typ int}]

   450 fun minipick ctxt n t =

   451   let

   452     val thy = Proof_Context.theory_of ctxt

   453     val {total_consts, ...} = Nitpick_Isar.default_params thy []

   454     val totals =

   455       total_consts |> Option.map single |> the_default [true, false]

   456     fun problem_for (total, k) =

   457       kodkod_problem_from_term ctxt total (K k) default_raw_infinite t

   458   in

   459     (totals, 1 upto n)

   460     |-> map_product pair

   461     |> map problem_for

   462     |> solve_any_kodkod_problem (Proof_Context.theory_of ctxt)

   463   end

   465 fun minipick_expect ctxt expect n t =

   466   if getenv "KODKODI" <> "" then

   467     if minipick ctxt n t = expect then ()

   468     else error ("\"minipick_expect\" expected " ^ quote expect)

   469   else

   470     ()

   472 end;

author	hoelzl
	Fri Mar 22 10:41:43 2013 +0100 (2013-03-22)
changeset 51474	1e9e68247ad1
parent 50487	9486641e691b
child 54845	10df188349b3
permissions	-rw-r--r--