src/HOL/Nitpick_Examples/minipick.ML
changeset 45062 9598cada31b3
parent 45035 60d2c03d5c70
child 45128 5af3a3203a76
     1.1 --- a/src/HOL/Nitpick_Examples/minipick.ML	Fri Sep 23 14:08:50 2011 +0200
     1.2 +++ b/src/HOL/Nitpick_Examples/minipick.ML	Fri Sep 23 14:25:53 2011 +0200
     1.3 @@ -7,21 +7,8 @@
     1.4  
     1.5  signature MINIPICK =
     1.6  sig
     1.7 -  datatype rep = S_Rep | R_Rep
     1.8 -  type styp = Nitpick_Util.styp
     1.9 -
    1.10 -  val vars_for_bound_var :
    1.11 -    (typ -> int) -> rep -> typ list -> int -> Kodkod.rel_expr list
    1.12 -  val rel_expr_for_bound_var :
    1.13 -    (typ -> int) -> rep -> typ list -> int -> Kodkod.rel_expr
    1.14 -  val decls_for : rep -> (typ -> int) -> typ list -> typ -> Kodkod.decl list
    1.15 -  val false_atom : Kodkod.rel_expr
    1.16 -  val true_atom : Kodkod.rel_expr
    1.17 -  val formula_from_atom : Kodkod.rel_expr -> Kodkod.formula
    1.18 -  val atom_from_formula : Kodkod.formula -> Kodkod.rel_expr
    1.19 -  val kodkod_problem_from_term :
    1.20 -    Proof.context -> (typ -> int) -> term -> Kodkod.problem
    1.21 -  val solve_any_kodkod_problem : theory -> Kodkod.problem list -> string
    1.22 +  val minipick : Proof.context -> int -> term -> string
    1.23 +  val minipick_expect : Proof.context -> string -> int -> term -> unit
    1.24  end;
    1.25  
    1.26  structure Minipick : MINIPICK =
    1.27 @@ -33,28 +20,34 @@
    1.28  open Nitpick_Peephole
    1.29  open Nitpick_Kodkod
    1.30  
    1.31 -datatype rep = S_Rep | R_Rep
    1.32 +datatype rep =
    1.33 +  S_Rep |
    1.34 +  R_Rep of bool
    1.35  
    1.36 -fun check_type ctxt (Type (@{type_name fun}, Ts)) =
    1.37 -    List.app (check_type ctxt) Ts
    1.38 -  | check_type ctxt (Type (@{type_name prod}, Ts)) =
    1.39 -    List.app (check_type ctxt) Ts
    1.40 -  | check_type _ @{typ bool} = ()
    1.41 -  | check_type _ (TFree (_, @{sort "{}"})) = ()
    1.42 -  | check_type _ (TFree (_, @{sort HOL.type})) = ()
    1.43 -  | check_type ctxt T =
    1.44 -    raise NOT_SUPPORTED ("type " ^ quote (Syntax.string_of_typ ctxt T))
    1.45 +fun check_type ctxt raw_infinite (Type (@{type_name fun}, Ts)) =
    1.46 +    List.app (check_type ctxt raw_infinite) Ts
    1.47 +  | check_type ctxt raw_infinite (Type (@{type_name prod}, Ts)) =
    1.48 +    List.app (check_type ctxt raw_infinite) Ts
    1.49 +  | check_type _ _ @{typ bool} = ()
    1.50 +  | check_type _ _ (TFree (_, @{sort "{}"})) = ()
    1.51 +  | check_type _ _ (TFree (_, @{sort HOL.type})) = ()
    1.52 +  | check_type ctxt raw_infinite T =
    1.53 +    if raw_infinite T then ()
    1.54 +    else raise NOT_SUPPORTED ("type " ^ quote (Syntax.string_of_typ ctxt T))
    1.55  
    1.56  fun atom_schema_of S_Rep card (Type (@{type_name fun}, [T1, T2])) =
    1.57      replicate_list (card T1) (atom_schema_of S_Rep card T2)
    1.58 -  | atom_schema_of R_Rep card (Type (@{type_name fun}, [T1, @{typ bool}])) =
    1.59 +  | atom_schema_of (R_Rep true) card
    1.60 +                   (Type (@{type_name fun}, [T1, @{typ bool}])) =
    1.61      atom_schema_of S_Rep card T1
    1.62 -  | atom_schema_of R_Rep card (Type (@{type_name fun}, [T1, T2])) =
    1.63 -    atom_schema_of S_Rep card T1 @ atom_schema_of R_Rep card T2
    1.64 +  | atom_schema_of (rep as R_Rep _) card (Type (@{type_name fun}, [T1, T2])) =
    1.65 +    atom_schema_of S_Rep card T1 @ atom_schema_of rep card T2
    1.66    | atom_schema_of _ card (Type (@{type_name prod}, Ts)) =
    1.67      maps (atom_schema_of S_Rep card) Ts
    1.68    | atom_schema_of _ card T = [card T]
    1.69  val arity_of = length ooo atom_schema_of
    1.70 +val atom_seqs_of = map (AtomSeq o rpair 0) ooo atom_schema_of
    1.71 +val atom_seq_product_of = foldl1 Product ooo atom_seqs_of
    1.72  
    1.73  fun index_for_bound_var _ [_] 0 = 0
    1.74    | index_for_bound_var card (_ :: Ts) 0 =
    1.75 @@ -68,78 +61,121 @@
    1.76    map2 (curry DeclOne o pair 1)
    1.77         (index_seq (index_for_bound_var card (T :: Ts) 0)
    1.78                    (arity_of R card (nth (T :: Ts) 0)))
    1.79 -       (map (AtomSeq o rpair 0) (atom_schema_of R card T))
    1.80 +       (atom_seqs_of R card T)
    1.81  
    1.82  val atom_product = foldl1 Product o map Atom
    1.83  
    1.84 -val false_atom = Atom 0
    1.85 -val true_atom = Atom 1
    1.86 +val false_atom_num = 0
    1.87 +val true_atom_num = 1
    1.88 +val false_atom = Atom false_atom_num
    1.89 +val true_atom = Atom true_atom_num
    1.90  
    1.91 -fun formula_from_atom r = RelEq (r, true_atom)
    1.92 -fun atom_from_formula f = RelIf (f, true_atom, false_atom)
    1.93 -
    1.94 -fun kodkod_formula_from_term ctxt card frees =
    1.95 +fun kodkod_formula_from_term ctxt total card complete concrete frees =
    1.96    let
    1.97 -    fun R_rep_from_S_rep (Type (@{type_name fun}, [T1, @{typ bool}])) r =
    1.98 -        let
    1.99 -          val jss = atom_schema_of S_Rep card T1 |> map (rpair 0)
   1.100 -                    |> all_combinations
   1.101 -        in
   1.102 -          map2 (fn i => fn js =>
   1.103 -                   RelIf (formula_from_atom (Project (r, [Num i])),
   1.104 -                          atom_product js, empty_n_ary_rel (length js)))
   1.105 -               (index_seq 0 (length jss)) jss
   1.106 -          |> foldl1 Union
   1.107 -        end
   1.108 -      | R_rep_from_S_rep (Type (@{type_name fun}, [T1, T2])) r =
   1.109 -        let
   1.110 -          val jss = atom_schema_of S_Rep card T1 |> map (rpair 0)
   1.111 -                    |> all_combinations
   1.112 -          val arity2 = arity_of S_Rep card T2
   1.113 -        in
   1.114 -          map2 (fn i => fn js =>
   1.115 -                   Product (atom_product js,
   1.116 -                            Project (r, num_seq (i * arity2) arity2)
   1.117 -                            |> R_rep_from_S_rep T2))
   1.118 -               (index_seq 0 (length jss)) jss
   1.119 -          |> foldl1 Union
   1.120 -        end
   1.121 +    fun F_from_S_rep (SOME false) r = Not (RelEq (r, false_atom))
   1.122 +      | F_from_S_rep _ r = RelEq (r, true_atom)
   1.123 +    fun S_rep_from_F NONE f = RelIf (f, true_atom, false_atom)
   1.124 +      | S_rep_from_F (SOME true) f = RelIf (f, true_atom, None)
   1.125 +      | S_rep_from_F (SOME false) f = RelIf (Not f, false_atom, None)
   1.126 +    fun R_rep_from_S_rep (Type (@{type_name fun}, [T1, T2])) r =
   1.127 +        if total andalso T2 = bool_T then
   1.128 +          let
   1.129 +            val jss = atom_schema_of S_Rep card T1 |> map (rpair 0)
   1.130 +                      |> all_combinations
   1.131 +          in
   1.132 +            map2 (fn i => fn js =>
   1.133 +(*
   1.134 +                     RelIf (F_from_S_rep NONE (Project (r, [Num i])),
   1.135 +                            atom_product js, empty_n_ary_rel (length js))
   1.136 +*)
   1.137 +                     Join (Project (r, [Num i]),
   1.138 +                           atom_product (false_atom_num :: js))
   1.139 +                 ) (index_seq 0 (length jss)) jss
   1.140 +            |> foldl1 Union
   1.141 +          end
   1.142 +        else
   1.143 +          let
   1.144 +            val jss = atom_schema_of S_Rep card T1 |> map (rpair 0)
   1.145 +                      |> all_combinations
   1.146 +            val arity2 = arity_of S_Rep card T2
   1.147 +          in
   1.148 +            map2 (fn i => fn js =>
   1.149 +                     Product (atom_product js,
   1.150 +                              Project (r, num_seq (i * arity2) arity2)
   1.151 +                              |> R_rep_from_S_rep T2))
   1.152 +                 (index_seq 0 (length jss)) jss
   1.153 +            |> foldl1 Union
   1.154 +          end
   1.155        | R_rep_from_S_rep _ r = r
   1.156      fun S_rep_from_R_rep Ts (T as Type (@{type_name fun}, _)) r =
   1.157          Comprehension (decls_for S_Rep card Ts T,
   1.158              RelEq (R_rep_from_S_rep T
   1.159                         (rel_expr_for_bound_var card S_Rep (T :: Ts) 0), r))
   1.160        | S_rep_from_R_rep _ _ r = r
   1.161 -    fun to_F Ts t =
   1.162 +    fun partial_eq pos Ts (Type (@{type_name fun}, [T1, T2])) t1 t2 =
   1.163 +        HOLogic.mk_all ("x", T1,
   1.164 +                        HOLogic.eq_const T2 $ (incr_boundvars 1 t1 $ Bound 0)
   1.165 +                        $ (incr_boundvars 1 t2 $ Bound 0))
   1.166 +        |> to_F (SOME pos) Ts
   1.167 +      | partial_eq pos Ts T t1 t2 =
   1.168 +        if pos andalso not (concrete T) then
   1.169 +          False
   1.170 +        else
   1.171 +          (t1, t2) |> pairself (to_R_rep Ts)
   1.172 +                   |> (if pos then Some o Intersect else Lone o Union)
   1.173 +    and to_F pos Ts t =
   1.174        (case t of
   1.175 -         @{const Not} $ t1 => Not (to_F Ts t1)
   1.176 +         @{const Not} $ t1 => Not (to_F (Option.map not pos) Ts t1)
   1.177         | @{const False} => False
   1.178         | @{const True} => True
   1.179         | Const (@{const_name All}, _) $ Abs (_, T, t') =>
   1.180 -         All (decls_for S_Rep card Ts T, to_F (T :: Ts) t')
   1.181 +         if pos = SOME true andalso not (complete T) then False
   1.182 +         else All (decls_for S_Rep card Ts T, to_F pos (T :: Ts) t')
   1.183         | (t0 as Const (@{const_name All}, _)) $ t1 =>
   1.184 -         to_F Ts (t0 $ eta_expand Ts t1 1)
   1.185 +         to_F pos Ts (t0 $ eta_expand Ts t1 1)
   1.186         | Const (@{const_name Ex}, _) $ Abs (_, T, t') =>
   1.187 -         Exist (decls_for S_Rep card Ts T, to_F (T :: Ts) t')
   1.188 +         if pos = SOME false andalso not (complete T) then True
   1.189 +         else Exist (decls_for S_Rep card Ts T, to_F pos (T :: Ts) t')
   1.190         | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
   1.191 -         to_F Ts (t0 $ eta_expand Ts t1 1)
   1.192 -       | Const (@{const_name HOL.eq}, _) $ t1 $ t2 =>
   1.193 -         RelEq (to_R_rep Ts t1, to_R_rep Ts t2)
   1.194 +         to_F pos Ts (t0 $ eta_expand Ts t1 1)
   1.195 +       | Const (@{const_name HOL.eq}, Type (_, [T, _])) $ t1 $ t2 =>
   1.196 +         (case pos of
   1.197 +            NONE => RelEq (to_R_rep Ts t1, to_R_rep Ts t2)
   1.198 +          | SOME pos => partial_eq pos Ts T t1 t2)
   1.199         | Const (@{const_name ord_class.less_eq},
   1.200                  Type (@{type_name fun},
   1.201 -                      [Type (@{type_name fun}, [_, @{typ bool}]), _]))
   1.202 +                      [Type (@{type_name fun}, [T', @{typ bool}]), _]))
   1.203           $ t1 $ t2 =>
   1.204 -         Subset (to_R_rep Ts t1, to_R_rep Ts t2)
   1.205 -       | @{const HOL.conj} $ t1 $ t2 => And (to_F Ts t1, to_F Ts t2)
   1.206 -       | @{const HOL.disj} $ t1 $ t2 => Or (to_F Ts t1, to_F Ts t2)
   1.207 -       | @{const HOL.implies} $ t1 $ t2 => Implies (to_F Ts t1, to_F Ts t2)
   1.208 -       | t1 $ t2 => Subset (to_S_rep Ts t2, to_R_rep Ts t1)
   1.209 -       | Free _ => raise SAME ()
   1.210 -       | Term.Var _ => raise SAME ()
   1.211 -       | Bound _ => raise SAME ()
   1.212 -       | Const (s, _) => raise NOT_SUPPORTED ("constant " ^ quote s)
   1.213 -       | _ => raise TERM ("Minipick.kodkod_formula_from_term.to_F", [t]))
   1.214 -      handle SAME () => formula_from_atom (to_R_rep Ts t)
   1.215 +         (case pos of
   1.216 +            NONE => Subset (to_R_rep Ts t1, to_R_rep Ts t2)
   1.217 +          | SOME true =>
   1.218 +            Subset (Difference (atom_seq_product_of S_Rep card T',
   1.219 +                                Join (to_R_rep Ts t1, false_atom)),
   1.220 +                    Join (to_R_rep Ts t2, true_atom))
   1.221 +          | SOME false =>
   1.222 +            Subset (Join (to_R_rep Ts t1, true_atom),
   1.223 +                    Difference (atom_seq_product_of S_Rep card T',
   1.224 +                                Join (to_R_rep Ts t2, false_atom))))
   1.225 +       | @{const HOL.conj} $ t1 $ t2 => And (to_F pos Ts t1, to_F pos Ts t2)
   1.226 +       | @{const HOL.disj} $ t1 $ t2 => Or (to_F pos Ts t1, to_F pos Ts t2)
   1.227 +       | @{const HOL.implies} $ t1 $ t2 =>
   1.228 +         Implies (to_F (Option.map not pos) Ts t1, to_F pos Ts t2)
   1.229 +       | t1 $ t2 =>
   1.230 +         (case pos of
   1.231 +            NONE => Subset (to_S_rep Ts t2, to_R_rep Ts t1)
   1.232 +          | SOME pos =>
   1.233 +            let
   1.234 +              val kt1 = to_R_rep Ts t1
   1.235 +              val kt2 = to_S_rep Ts t2
   1.236 +              val kT = atom_seq_product_of S_Rep card (fastype_of1 (Ts, t2))
   1.237 +            in
   1.238 +              if pos then
   1.239 +                Not (Subset (kt2, Difference (kT, Join (kt1, true_atom))))
   1.240 +              else
   1.241 +                Subset (kt2, Difference (kT, Join (kt1, false_atom)))
   1.242 +            end)
   1.243 +       | _ => raise SAME ())
   1.244 +      handle SAME () => F_from_S_rep pos (to_R_rep Ts t)
   1.245      and to_S_rep Ts t =
   1.246        case t of
   1.247          Const (@{const_name Pair}, _) $ t1 $ t2 =>
   1.248 @@ -160,6 +196,16 @@
   1.249        | Const (@{const_name snd}, _) => to_S_rep Ts (eta_expand Ts t 1)
   1.250        | Bound j => rel_expr_for_bound_var card S_Rep Ts j
   1.251        | _ => S_rep_from_R_rep Ts (fastype_of1 (Ts, t)) (to_R_rep Ts t)
   1.252 +    and partial_set_op swap1 swap2 op1 op2 Ts t1 t2 =
   1.253 +      let
   1.254 +        val kt1 = to_R_rep Ts t1
   1.255 +        val kt2 = to_R_rep Ts t2
   1.256 +        val (a11, a21) = (false_atom, true_atom) |> swap1 ? swap
   1.257 +        val (a12, a22) = (false_atom, true_atom) |> swap2 ? swap
   1.258 +      in
   1.259 +        Union (Product (op1 (Join (kt1, a11), Join (kt2, a12)), true_atom),
   1.260 +               Product (op2 (Join (kt1, a21), Join (kt2, a22)), false_atom))
   1.261 +      end
   1.262      and to_R_rep Ts t =
   1.263        (case t of
   1.264           @{const Not} => to_R_rep Ts (eta_expand Ts t 1)
   1.265 @@ -180,15 +226,51 @@
   1.266         | @{const HOL.implies} $ _ => to_R_rep Ts (eta_expand Ts t 1)
   1.267         | @{const HOL.implies} => to_R_rep Ts (eta_expand Ts t 2)
   1.268         | Const (@{const_name bot_class.bot},
   1.269 -                T as Type (@{type_name fun}, [_, @{typ bool}])) =>
   1.270 -         empty_n_ary_rel (arity_of R_Rep card T)
   1.271 -       | Const (@{const_name insert}, _) $ t1 $ t2 =>
   1.272 -         Union (to_S_rep Ts t1, to_R_rep Ts t2)
   1.273 +                T as Type (@{type_name fun}, [T', @{typ bool}])) =>
   1.274 +         if total then empty_n_ary_rel (arity_of (R_Rep total) card T)
   1.275 +         else Product (atom_seq_product_of (R_Rep total) card T', false_atom)
   1.276 +       | Const (@{const_name top_class.top},
   1.277 +                T as Type (@{type_name fun}, [T', @{typ bool}])) =>
   1.278 +         if total then atom_seq_product_of (R_Rep total) card T
   1.279 +         else Product (atom_seq_product_of (R_Rep total) card T', true_atom)
   1.280 +       | Const (@{const_name insert}, Type (_, [T, _])) $ t1 $ t2 =>
   1.281 +         if total then
   1.282 +           Union (to_S_rep Ts t1, to_R_rep Ts t2)
   1.283 +         else
   1.284 +           let
   1.285 +             val kt1 = to_S_rep Ts t1
   1.286 +             val kt2 = to_R_rep Ts t2
   1.287 +           in
   1.288 +             RelIf (Some kt1,
   1.289 +                    if arity_of S_Rep card T = 1 then
   1.290 +                      Override (kt2, Product (kt1, true_atom))
   1.291 +                    else
   1.292 +                      Union (Difference (kt2, Product (kt1, false_atom)),
   1.293 +                             Product (kt1, true_atom)),
   1.294 +                    Difference (kt2, Product (atom_seq_product_of S_Rep card T,
   1.295 +                                              false_atom)))
   1.296 +           end
   1.297         | Const (@{const_name insert}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
   1.298         | Const (@{const_name insert}, _) => to_R_rep Ts (eta_expand Ts t 2)
   1.299 -       | Const (@{const_name trancl}, _) $ t1 =>
   1.300 -         if arity_of R_Rep card (fastype_of1 (Ts, t1)) = 2 then
   1.301 -           Closure (to_R_rep Ts t1)
   1.302 +       | Const (@{const_name trancl},
   1.303 +                Type (_, [Type (_, [Type (_, [T', _]), _]), _])) $ t1 =>
   1.304 +         if arity_of S_Rep card T' = 1 then
   1.305 +           if total then
   1.306 +             Closure (to_R_rep Ts t1)
   1.307 +           else
   1.308 +             let
   1.309 +               val kt1 = to_R_rep Ts t1
   1.310 +               val true_core_kt = Closure (Join (kt1, true_atom))
   1.311 +               val kTx =
   1.312 +                 atom_seq_product_of S_Rep card (HOLogic.mk_prodT (`I T'))
   1.313 +               val false_mantle_kt =
   1.314 +                 Difference (kTx,
   1.315 +                     Closure (Difference (kTx, Join (kt1, false_atom))))
   1.316 +             in
   1.317 +               Union (Product (Difference (false_mantle_kt, true_core_kt),
   1.318 +                               false_atom),
   1.319 +                      Product (true_core_kt, true_atom))
   1.320 +             end
   1.321           else
   1.322             raise NOT_SUPPORTED "transitive closure for function or pair type"
   1.323         | Const (@{const_name trancl}, _) => to_R_rep Ts (eta_expand Ts t 1)
   1.324 @@ -196,7 +278,8 @@
   1.325                  Type (@{type_name fun},
   1.326                        [Type (@{type_name fun}, [_, @{typ bool}]), _]))
   1.327           $ t1 $ t2 =>
   1.328 -         Intersect (to_R_rep Ts t1, to_R_rep Ts t2)
   1.329 +         if total then Intersect (to_R_rep Ts t1, to_R_rep Ts t2)
   1.330 +         else partial_set_op true true Intersect Union Ts t1 t2
   1.331         | Const (@{const_name inf_class.inf}, _) $ _ =>
   1.332           to_R_rep Ts (eta_expand Ts t 1)
   1.333         | Const (@{const_name inf_class.inf}, _) =>
   1.334 @@ -205,7 +288,8 @@
   1.335                  Type (@{type_name fun},
   1.336                        [Type (@{type_name fun}, [_, @{typ bool}]), _]))
   1.337           $ t1 $ t2 =>
   1.338 -         Union (to_R_rep Ts t1, to_R_rep Ts t2)
   1.339 +         if total then Union (to_R_rep Ts t1, to_R_rep Ts t2)
   1.340 +         else partial_set_op true true Union Intersect Ts t1 t2
   1.341         | Const (@{const_name sup_class.sup}, _) $ _ =>
   1.342           to_R_rep Ts (eta_expand Ts t 1)
   1.343         | Const (@{const_name sup_class.sup}, _) =>
   1.344 @@ -214,7 +298,8 @@
   1.345                  Type (@{type_name fun},
   1.346                        [Type (@{type_name fun}, [_, @{typ bool}]), _]))
   1.347           $ t1 $ t2 =>
   1.348 -         Difference (to_R_rep Ts t1, to_R_rep Ts t2)
   1.349 +         if total then Difference (to_R_rep Ts t1, to_R_rep Ts t2)
   1.350 +         else partial_set_op true false Intersect Union Ts t1 t2
   1.351         | Const (@{const_name minus_class.minus},
   1.352                  Type (@{type_name fun},
   1.353                        [Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ =>
   1.354 @@ -223,40 +308,47 @@
   1.355                  Type (@{type_name fun},
   1.356                        [Type (@{type_name fun}, [_, @{typ bool}]), _])) =>
   1.357           to_R_rep Ts (eta_expand Ts t 2)
   1.358 -       | Const (@{const_name Pair}, _) $ _ $ _ => raise SAME ()
   1.359 -       | Const (@{const_name Pair}, _) $ _ => raise SAME ()
   1.360 -       | Const (@{const_name Pair}, _) => raise SAME ()
   1.361 +       | Const (@{const_name Pair}, _) $ _ $ _ => to_S_rep Ts t
   1.362 +       | Const (@{const_name Pair}, _) $ _ => to_S_rep Ts t
   1.363 +       | Const (@{const_name Pair}, _) => to_S_rep Ts t
   1.364         | Const (@{const_name fst}, _) $ _ => raise SAME ()
   1.365         | Const (@{const_name fst}, _) => raise SAME ()
   1.366         | Const (@{const_name snd}, _) $ _ => raise SAME ()
   1.367         | Const (@{const_name snd}, _) => raise SAME ()
   1.368 -       | Const (_, @{typ bool}) => atom_from_formula (to_F Ts t)
   1.369 +       | @{const False} => false_atom
   1.370 +       | @{const True} => true_atom
   1.371         | Free (x as (_, T)) =>
   1.372 -         Rel (arity_of R_Rep card T, find_index (curry (op =) x) frees)
   1.373 +         Rel (arity_of (R_Rep total) card T, find_index (curry (op =) x) frees)
   1.374         | Term.Var _ => raise NOT_SUPPORTED "schematic variables"
   1.375         | Bound _ => raise SAME ()
   1.376         | Abs (_, T, t') =>
   1.377 -         (case fastype_of1 (T :: Ts, t') of
   1.378 -            @{typ bool} => Comprehension (decls_for S_Rep card Ts T,
   1.379 -                                          to_F (T :: Ts) t')
   1.380 -          | T' => Comprehension (decls_for S_Rep card Ts T @
   1.381 -                                 decls_for R_Rep card (T :: Ts) T',
   1.382 -                                 Subset (rel_expr_for_bound_var card R_Rep
   1.383 -                                                              (T' :: T :: Ts) 0,
   1.384 -                                         to_R_rep (T :: Ts) t')))
   1.385 +         (case (total, fastype_of1 (T :: Ts, t')) of
   1.386 +            (true, @{typ bool}) =>
   1.387 +            Comprehension (decls_for S_Rep card Ts T, to_F NONE (T :: Ts) t')
   1.388 +          | (_, T') =>
   1.389 +            Comprehension (decls_for S_Rep card Ts T @
   1.390 +                           decls_for (R_Rep total) card (T :: Ts) T',
   1.391 +                           Subset (rel_expr_for_bound_var card (R_Rep total)
   1.392 +                                                          (T' :: T :: Ts) 0,
   1.393 +                                   to_R_rep (T :: Ts) t')))
   1.394         | t1 $ t2 =>
   1.395           (case fastype_of1 (Ts, t) of
   1.396 -            @{typ bool} => atom_from_formula (to_F Ts t)
   1.397 +            @{typ bool} =>
   1.398 +            if total then
   1.399 +              S_rep_from_F NONE (to_F NONE Ts t)
   1.400 +            else
   1.401 +              RelIf (to_F (SOME true) Ts t, true_atom,
   1.402 +                     RelIf (Not (to_F (SOME false) Ts t), false_atom,
   1.403 +                     None))
   1.404            | T =>
   1.405              let val T2 = fastype_of1 (Ts, t2) in
   1.406                case arity_of S_Rep card T2 of
   1.407                  1 => Join (to_S_rep Ts t2, to_R_rep Ts t1)
   1.408                | arity2 =>
   1.409 -                let val res_arity = arity_of R_Rep card T in
   1.410 +                let val res_arity = arity_of (R_Rep total) card T in
   1.411                    Project (Intersect
   1.412                        (Product (to_S_rep Ts t2,
   1.413 -                                atom_schema_of R_Rep card T
   1.414 -                                |> map (AtomSeq o rpair 0) |> foldl1 Product),
   1.415 +                                atom_seq_product_of (R_Rep total) card T),
   1.416                         to_R_rep Ts t1),
   1.417                        num_seq arity2 res_arity)
   1.418                  end
   1.419 @@ -264,28 +356,30 @@
   1.420         | _ => raise NOT_SUPPORTED ("term " ^
   1.421                                     quote (Syntax.string_of_term ctxt t)))
   1.422        handle SAME () => R_rep_from_S_rep (fastype_of1 (Ts, t)) (to_S_rep Ts t)
   1.423 -  in to_F [] end
   1.424 +  in to_F (if total then NONE else SOME true) [] end
   1.425  
   1.426 -fun bound_for_free card i (s, T) =
   1.427 -  let val js = atom_schema_of R_Rep card T in
   1.428 +fun bound_for_free total card i (s, T) =
   1.429 +  let val js = atom_schema_of (R_Rep total) card T in
   1.430      ([((length js, i), s)],
   1.431 -     [TupleSet [], atom_schema_of R_Rep card T |> map (rpair 0)
   1.432 +     [TupleSet [], atom_schema_of (R_Rep total) card T |> map (rpair 0)
   1.433                     |> tuple_set_from_atom_schema])
   1.434    end
   1.435  
   1.436 -fun declarative_axiom_for_rel_expr card Ts (Type (@{type_name fun}, [T1, T2]))
   1.437 -                                   r =
   1.438 -    if body_type T2 = bool_T then
   1.439 +fun declarative_axiom_for_rel_expr total card Ts
   1.440 +                                   (Type (@{type_name fun}, [T1, T2])) r =
   1.441 +    if total andalso body_type T2 = bool_T then
   1.442        True
   1.443      else
   1.444        All (decls_for S_Rep card Ts T1,
   1.445 -           declarative_axiom_for_rel_expr card (T1 :: Ts) T2
   1.446 +           declarative_axiom_for_rel_expr total card (T1 :: Ts) T2
   1.447                 (List.foldl Join r (vars_for_bound_var card S_Rep (T1 :: Ts) 0)))
   1.448 -  | declarative_axiom_for_rel_expr _ _ _ r = One r
   1.449 -fun declarative_axiom_for_free card i (_, T) =
   1.450 -  declarative_axiom_for_rel_expr card [] T (Rel (arity_of R_Rep card T, i))
   1.451 +  | declarative_axiom_for_rel_expr total _ _ _ r =
   1.452 +    (if total then One else Lone) r
   1.453 +fun declarative_axiom_for_free total card i (_, T) =
   1.454 +  declarative_axiom_for_rel_expr total card [] T
   1.455 +      (Rel (arity_of (R_Rep total) card T, i))
   1.456  
   1.457 -fun kodkod_problem_from_term ctxt raw_card t =
   1.458 +fun kodkod_problem_from_term ctxt total raw_card raw_infinite t =
   1.459    let
   1.460      val thy = ProofContext.theory_of ctxt
   1.461      fun card (Type (@{type_name fun}, [T1, T2])) =
   1.462 @@ -293,14 +387,25 @@
   1.463        | card (Type (@{type_name prod}, [T1, T2])) = card T1 * card T2
   1.464        | card @{typ bool} = 2
   1.465        | card T = Int.max (1, raw_card T)
   1.466 +    fun complete (Type (@{type_name fun}, [T1, T2])) =
   1.467 +        concrete T1 andalso complete T2
   1.468 +      | complete (Type (@{type_name prod}, Ts)) = forall complete Ts
   1.469 +      | complete T = not (raw_infinite T)
   1.470 +    and concrete (Type (@{type_name fun}, [T1, T2])) =
   1.471 +        complete T1 andalso concrete T2
   1.472 +      | concrete (Type (@{type_name prod}, Ts)) = forall concrete Ts
   1.473 +      | concrete _ = true
   1.474      val neg_t = @{const Not} $ Object_Logic.atomize_term thy t
   1.475 -    val _ = fold_types (K o check_type ctxt) neg_t ()
   1.476 +    val _ = fold_types (K o check_type ctxt raw_infinite) neg_t ()
   1.477      val frees = Term.add_frees neg_t []
   1.478 -    val bounds = map2 (bound_for_free card) (index_seq 0 (length frees)) frees
   1.479 +    val bounds =
   1.480 +      map2 (bound_for_free total card) (index_seq 0 (length frees)) frees
   1.481      val declarative_axioms =
   1.482 -      map2 (declarative_axiom_for_free card) (index_seq 0 (length frees)) frees
   1.483 -    val formula = kodkod_formula_from_term ctxt card frees neg_t
   1.484 -                  |> fold_rev (curry And) declarative_axioms
   1.485 +      map2 (declarative_axiom_for_free total card)
   1.486 +           (index_seq 0 (length frees)) frees
   1.487 +    val formula =
   1.488 +      neg_t |> kodkod_formula_from_term ctxt total card complete concrete frees 
   1.489 +            |> fold_rev (curry And) declarative_axioms
   1.490      val univ_card = univ_card 0 0 0 bounds formula
   1.491    in
   1.492      {comment = "", settings = [], univ_card = univ_card, tuple_assigns = [],
   1.493 @@ -324,4 +429,28 @@
   1.494      | Error (s, _) => error ("Kodkod error: " ^ s)
   1.495    end
   1.496  
   1.497 +val default_raw_infinite = member (op =) [@{typ nat}, @{typ int}]
   1.498 +
   1.499 +fun minipick ctxt n t =
   1.500 +  let
   1.501 +    val thy = ProofContext.theory_of ctxt
   1.502 +    val {total_consts, ...} = Nitpick_Isar.default_params thy []
   1.503 +    val totals =
   1.504 +      total_consts |> Option.map single |> the_default [true, false]
   1.505 +    fun problem_for (total, k) =
   1.506 +      kodkod_problem_from_term ctxt total (K k) default_raw_infinite t
   1.507 +  in
   1.508 +    (totals, 1 upto n)
   1.509 +    |-> map_product pair
   1.510 +    |> map problem_for
   1.511 +    |> solve_any_kodkod_problem (Proof_Context.theory_of ctxt)
   1.512 +  end
   1.513 +
   1.514 +fun minipick_expect ctxt expect n t =
   1.515 +  if getenv "KODKODI" <> "" then
   1.516 +    if minipick ctxt n t = expect then ()
   1.517 +    else error ("\"minipick_expect\" expected " ^ quote expect)
   1.518 +  else
   1.519 +    ()
   1.520 +
   1.521  end;