--- a/src/HOL/Nitpick_Examples/Mini_Nits.thy Fri Sep 23 14:08:50 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Mini_Nits.thy Fri Sep 23 14:25:53 2011 +0200
@@ -12,22 +12,16 @@
uses "minipick.ML"
begin
-ML {*
-exception FAIL
+nitpick_params [verbose, sat_solver = MiniSat_JNI, max_threads = 1]
-val has_kodkodi = (getenv "KODKODI" <> "")
+nitpick_params [total_consts = smart]
-fun minipick n t =
- map (fn k => Minipick.kodkod_problem_from_term @{context} (K k) t) (1 upto n)
- |> Minipick.solve_any_kodkod_problem @{theory}
-fun minipick_expect expect n t =
- if has_kodkodi then
- if minipick n t = expect then () else raise FAIL
- else
- ()
-val none = minipick_expect "none"
-val genuine = minipick_expect "genuine"
-val unknown = minipick_expect "unknown"
+ML {*
+val check = Minipick.minipick @{context}
+val expect = Minipick.minipick_expect @{context}
+val none = expect "none"
+val genuine = expect "genuine"
+val unknown = expect "unknown"
*}
ML {* genuine 1 @{prop "x = Not"} *}
@@ -43,7 +37,6 @@
ML {* none 5 @{prop "\<exists>x. x = x"} *}
ML {* none 1 @{prop "\<forall>x. x = y"} *}
ML {* genuine 2 @{prop "\<forall>x. x = y"} *}
-ML {* none 1 @{prop "\<exists>x. x = y"} *}
ML {* none 2 @{prop "\<exists>x. x = y"} *}
ML {* none 2 @{prop "\<forall>x\<Colon>'a \<times> 'a. x = x"} *}
ML {* none 2 @{prop "\<exists>x\<Colon>'a \<times> 'a. x = y"} *}
@@ -74,6 +67,9 @@
ML {* genuine 2 @{prop "{a} = {a, b}"} *}
ML {* genuine 1 @{prop "{a} \<noteq> {a, b}"} *}
ML {* none 5 @{prop "{}\<^sup>+ = {}"} *}
+ML {* none 5 @{prop "UNIV\<^sup>+ = UNIV"} *}
+ML {* none 5 @{prop "(UNIV\<Colon>'a \<times> 'b \<Rightarrow> bool) - {} = UNIV"} *}
+ML {* none 5 @{prop "{} - (UNIV\<Colon>'a \<times> 'b \<Rightarrow> bool) = {}"} *}
ML {* none 1 @{prop "{(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
ML {* genuine 2 @{prop "{(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
ML {* none 5 @{prop "a \<noteq> c \<Longrightarrow> {(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
@@ -93,6 +89,8 @@
ML {* none 1 @{prop "fst (a, b) = b"} *}
ML {* genuine 2 @{prop "fst (a, b) = b"} *}
ML {* genuine 2 @{prop "fst (a, b) \<noteq> b"} *}
+ML {* genuine 2 @{prop "f ((x, z), y) = (x, z)"} *}
+ML {* none 2 @{prop "(ALL x. f x = fst x) \<longrightarrow> f ((x, z), y) = (x, z)"} *}
ML {* none 5 @{prop "snd (a, b) = b"} *}
ML {* none 1 @{prop "snd (a, b) = a"} *}
ML {* genuine 2 @{prop "snd (a, b) = a"} *}
@@ -105,5 +103,9 @@
ML {* none 2 @{prop "\<exists>f. \<forall>a b. f (a, b) = (a, b)"} *}
ML {* none 3 @{prop "f = (\<lambda>a b. (b, a)) \<longrightarrow> f x y = (y, x)"} *}
ML {* genuine 2 @{prop "f = (\<lambda>a b. (b, a)) \<longrightarrow> f x y = (x, y)"} *}
+ML {* none 5 @{prop "f = (\<lambda>x. f x)"} *}
+ML {* none 5 @{prop "f = (\<lambda>x. f x\<Colon>'a \<Rightarrow> bool)"} *}
+ML {* none 5 @{prop "f = (\<lambda>x y. f x y)"} *}
+ML {* none 5 @{prop "f = (\<lambda>x y. f x y\<Colon>'a \<Rightarrow> bool)"} *}
end
--- a/src/HOL/Nitpick_Examples/minipick.ML Fri Sep 23 14:08:50 2011 +0200
+++ b/src/HOL/Nitpick_Examples/minipick.ML Fri Sep 23 14:25:53 2011 +0200
@@ -7,21 +7,8 @@
signature MINIPICK =
sig
- datatype rep = S_Rep | R_Rep
- type styp = Nitpick_Util.styp
-
- val vars_for_bound_var :
- (typ -> int) -> rep -> typ list -> int -> Kodkod.rel_expr list
- val rel_expr_for_bound_var :
- (typ -> int) -> rep -> typ list -> int -> Kodkod.rel_expr
- val decls_for : rep -> (typ -> int) -> typ list -> typ -> Kodkod.decl list
- val false_atom : Kodkod.rel_expr
- val true_atom : Kodkod.rel_expr
- val formula_from_atom : Kodkod.rel_expr -> Kodkod.formula
- val atom_from_formula : Kodkod.formula -> Kodkod.rel_expr
- val kodkod_problem_from_term :
- Proof.context -> (typ -> int) -> term -> Kodkod.problem
- val solve_any_kodkod_problem : theory -> Kodkod.problem list -> string
+ val minipick : Proof.context -> int -> term -> string
+ val minipick_expect : Proof.context -> string -> int -> term -> unit
end;
structure Minipick : MINIPICK =
@@ -33,28 +20,34 @@
open Nitpick_Peephole
open Nitpick_Kodkod
-datatype rep = S_Rep | R_Rep
+datatype rep =
+ S_Rep |
+ R_Rep of bool
-fun check_type ctxt (Type (@{type_name fun}, Ts)) =
- List.app (check_type ctxt) Ts
- | check_type ctxt (Type (@{type_name prod}, Ts)) =
- List.app (check_type ctxt) Ts
- | check_type _ @{typ bool} = ()
- | check_type _ (TFree (_, @{sort "{}"})) = ()
- | check_type _ (TFree (_, @{sort HOL.type})) = ()
- | check_type ctxt T =
- raise NOT_SUPPORTED ("type " ^ quote (Syntax.string_of_typ ctxt T))
+fun check_type ctxt raw_infinite (Type (@{type_name fun}, Ts)) =
+ List.app (check_type ctxt raw_infinite) Ts
+ | check_type ctxt raw_infinite (Type (@{type_name prod}, Ts)) =
+ List.app (check_type ctxt raw_infinite) Ts
+ | check_type _ _ @{typ bool} = ()
+ | check_type _ _ (TFree (_, @{sort "{}"})) = ()
+ | check_type _ _ (TFree (_, @{sort HOL.type})) = ()
+ | check_type ctxt raw_infinite T =
+ if raw_infinite T then ()
+ else raise NOT_SUPPORTED ("type " ^ quote (Syntax.string_of_typ ctxt T))
fun atom_schema_of S_Rep card (Type (@{type_name fun}, [T1, T2])) =
replicate_list (card T1) (atom_schema_of S_Rep card T2)
- | atom_schema_of R_Rep card (Type (@{type_name fun}, [T1, @{typ bool}])) =
+ | atom_schema_of (R_Rep true) card
+ (Type (@{type_name fun}, [T1, @{typ bool}])) =
atom_schema_of S_Rep card T1
- | atom_schema_of R_Rep card (Type (@{type_name fun}, [T1, T2])) =
- atom_schema_of S_Rep card T1 @ atom_schema_of R_Rep card T2
+ | atom_schema_of (rep as R_Rep _) card (Type (@{type_name fun}, [T1, T2])) =
+ atom_schema_of S_Rep card T1 @ atom_schema_of rep card T2
| atom_schema_of _ card (Type (@{type_name prod}, Ts)) =
maps (atom_schema_of S_Rep card) Ts
| atom_schema_of _ card T = [card T]
val arity_of = length ooo atom_schema_of
+val atom_seqs_of = map (AtomSeq o rpair 0) ooo atom_schema_of
+val atom_seq_product_of = foldl1 Product ooo atom_seqs_of
fun index_for_bound_var _ [_] 0 = 0
| index_for_bound_var card (_ :: Ts) 0 =
@@ -68,78 +61,121 @@
map2 (curry DeclOne o pair 1)
(index_seq (index_for_bound_var card (T :: Ts) 0)
(arity_of R card (nth (T :: Ts) 0)))
- (map (AtomSeq o rpair 0) (atom_schema_of R card T))
+ (atom_seqs_of R card T)
val atom_product = foldl1 Product o map Atom
-val false_atom = Atom 0
-val true_atom = Atom 1
+val false_atom_num = 0
+val true_atom_num = 1
+val false_atom = Atom false_atom_num
+val true_atom = Atom true_atom_num
-fun formula_from_atom r = RelEq (r, true_atom)
-fun atom_from_formula f = RelIf (f, true_atom, false_atom)
-
-fun kodkod_formula_from_term ctxt card frees =
+fun kodkod_formula_from_term ctxt total card complete concrete frees =
let
- fun R_rep_from_S_rep (Type (@{type_name fun}, [T1, @{typ bool}])) r =
- let
- val jss = atom_schema_of S_Rep card T1 |> map (rpair 0)
- |> all_combinations
- in
- map2 (fn i => fn js =>
- RelIf (formula_from_atom (Project (r, [Num i])),
- atom_product js, empty_n_ary_rel (length js)))
- (index_seq 0 (length jss)) jss
- |> foldl1 Union
- end
- | R_rep_from_S_rep (Type (@{type_name fun}, [T1, T2])) r =
- let
- val jss = atom_schema_of S_Rep card T1 |> map (rpair 0)
- |> all_combinations
- val arity2 = arity_of S_Rep card T2
- in
- map2 (fn i => fn js =>
- Product (atom_product js,
- Project (r, num_seq (i * arity2) arity2)
- |> R_rep_from_S_rep T2))
- (index_seq 0 (length jss)) jss
- |> foldl1 Union
- end
+ fun F_from_S_rep (SOME false) r = Not (RelEq (r, false_atom))
+ | F_from_S_rep _ r = RelEq (r, true_atom)
+ fun S_rep_from_F NONE f = RelIf (f, true_atom, false_atom)
+ | S_rep_from_F (SOME true) f = RelIf (f, true_atom, None)
+ | S_rep_from_F (SOME false) f = RelIf (Not f, false_atom, None)
+ fun R_rep_from_S_rep (Type (@{type_name fun}, [T1, T2])) r =
+ if total andalso T2 = bool_T then
+ let
+ val jss = atom_schema_of S_Rep card T1 |> map (rpair 0)
+ |> all_combinations
+ in
+ map2 (fn i => fn js =>
+(*
+ RelIf (F_from_S_rep NONE (Project (r, [Num i])),
+ atom_product js, empty_n_ary_rel (length js))
+*)
+ Join (Project (r, [Num i]),
+ atom_product (false_atom_num :: js))
+ ) (index_seq 0 (length jss)) jss
+ |> foldl1 Union
+ end
+ else
+ let
+ val jss = atom_schema_of S_Rep card T1 |> map (rpair 0)
+ |> all_combinations
+ val arity2 = arity_of S_Rep card T2
+ in
+ map2 (fn i => fn js =>
+ Product (atom_product js,
+ Project (r, num_seq (i * arity2) arity2)
+ |> R_rep_from_S_rep T2))
+ (index_seq 0 (length jss)) jss
+ |> foldl1 Union
+ end
| R_rep_from_S_rep _ r = r
fun S_rep_from_R_rep Ts (T as Type (@{type_name fun}, _)) r =
Comprehension (decls_for S_Rep card Ts T,
RelEq (R_rep_from_S_rep T
(rel_expr_for_bound_var card S_Rep (T :: Ts) 0), r))
| S_rep_from_R_rep _ _ r = r
- fun to_F Ts t =
+ fun partial_eq pos Ts (Type (@{type_name fun}, [T1, T2])) t1 t2 =
+ HOLogic.mk_all ("x", T1,
+ HOLogic.eq_const T2 $ (incr_boundvars 1 t1 $ Bound 0)
+ $ (incr_boundvars 1 t2 $ Bound 0))
+ |> to_F (SOME pos) Ts
+ | partial_eq pos Ts T t1 t2 =
+ if pos andalso not (concrete T) then
+ False
+ else
+ (t1, t2) |> pairself (to_R_rep Ts)
+ |> (if pos then Some o Intersect else Lone o Union)
+ and to_F pos Ts t =
(case t of
- @{const Not} $ t1 => Not (to_F Ts t1)
+ @{const Not} $ t1 => Not (to_F (Option.map not pos) Ts t1)
| @{const False} => False
| @{const True} => True
| Const (@{const_name All}, _) $ Abs (_, T, t') =>
- All (decls_for S_Rep card Ts T, to_F (T :: Ts) t')
+ if pos = SOME true andalso not (complete T) then False
+ else All (decls_for S_Rep card Ts T, to_F pos (T :: Ts) t')
| (t0 as Const (@{const_name All}, _)) $ t1 =>
- to_F Ts (t0 $ eta_expand Ts t1 1)
+ to_F pos Ts (t0 $ eta_expand Ts t1 1)
| Const (@{const_name Ex}, _) $ Abs (_, T, t') =>
- Exist (decls_for S_Rep card Ts T, to_F (T :: Ts) t')
+ if pos = SOME false andalso not (complete T) then True
+ else Exist (decls_for S_Rep card Ts T, to_F pos (T :: Ts) t')
| (t0 as Const (@{const_name Ex}, _)) $ t1 =>
- to_F Ts (t0 $ eta_expand Ts t1 1)
- | Const (@{const_name HOL.eq}, _) $ t1 $ t2 =>
- RelEq (to_R_rep Ts t1, to_R_rep Ts t2)
+ to_F pos Ts (t0 $ eta_expand Ts t1 1)
+ | Const (@{const_name HOL.eq}, Type (_, [T, _])) $ t1 $ t2 =>
+ (case pos of
+ NONE => RelEq (to_R_rep Ts t1, to_R_rep Ts t2)
+ | SOME pos => partial_eq pos Ts T t1 t2)
| Const (@{const_name ord_class.less_eq},
Type (@{type_name fun},
- [Type (@{type_name fun}, [_, @{typ bool}]), _]))
+ [Type (@{type_name fun}, [T', @{typ bool}]), _]))
$ t1 $ t2 =>
- Subset (to_R_rep Ts t1, to_R_rep Ts t2)
- | @{const HOL.conj} $ t1 $ t2 => And (to_F Ts t1, to_F Ts t2)
- | @{const HOL.disj} $ t1 $ t2 => Or (to_F Ts t1, to_F Ts t2)
- | @{const HOL.implies} $ t1 $ t2 => Implies (to_F Ts t1, to_F Ts t2)
- | t1 $ t2 => Subset (to_S_rep Ts t2, to_R_rep Ts t1)
- | Free _ => raise SAME ()
- | Term.Var _ => raise SAME ()
- | Bound _ => raise SAME ()
- | Const (s, _) => raise NOT_SUPPORTED ("constant " ^ quote s)
- | _ => raise TERM ("Minipick.kodkod_formula_from_term.to_F", [t]))
- handle SAME () => formula_from_atom (to_R_rep Ts t)
+ (case pos of
+ NONE => Subset (to_R_rep Ts t1, to_R_rep Ts t2)
+ | SOME true =>
+ Subset (Difference (atom_seq_product_of S_Rep card T',
+ Join (to_R_rep Ts t1, false_atom)),
+ Join (to_R_rep Ts t2, true_atom))
+ | SOME false =>
+ Subset (Join (to_R_rep Ts t1, true_atom),
+ Difference (atom_seq_product_of S_Rep card T',
+ Join (to_R_rep Ts t2, false_atom))))
+ | @{const HOL.conj} $ t1 $ t2 => And (to_F pos Ts t1, to_F pos Ts t2)
+ | @{const HOL.disj} $ t1 $ t2 => Or (to_F pos Ts t1, to_F pos Ts t2)
+ | @{const HOL.implies} $ t1 $ t2 =>
+ Implies (to_F (Option.map not pos) Ts t1, to_F pos Ts t2)
+ | t1 $ t2 =>
+ (case pos of
+ NONE => Subset (to_S_rep Ts t2, to_R_rep Ts t1)
+ | SOME pos =>
+ let
+ val kt1 = to_R_rep Ts t1
+ val kt2 = to_S_rep Ts t2
+ val kT = atom_seq_product_of S_Rep card (fastype_of1 (Ts, t2))
+ in
+ if pos then
+ Not (Subset (kt2, Difference (kT, Join (kt1, true_atom))))
+ else
+ Subset (kt2, Difference (kT, Join (kt1, false_atom)))
+ end)
+ | _ => raise SAME ())
+ handle SAME () => F_from_S_rep pos (to_R_rep Ts t)
and to_S_rep Ts t =
case t of
Const (@{const_name Pair}, _) $ t1 $ t2 =>
@@ -160,6 +196,16 @@
| Const (@{const_name snd}, _) => to_S_rep Ts (eta_expand Ts t 1)
| Bound j => rel_expr_for_bound_var card S_Rep Ts j
| _ => S_rep_from_R_rep Ts (fastype_of1 (Ts, t)) (to_R_rep Ts t)
+ and partial_set_op swap1 swap2 op1 op2 Ts t1 t2 =
+ let
+ val kt1 = to_R_rep Ts t1
+ val kt2 = to_R_rep Ts t2
+ val (a11, a21) = (false_atom, true_atom) |> swap1 ? swap
+ val (a12, a22) = (false_atom, true_atom) |> swap2 ? swap
+ in
+ Union (Product (op1 (Join (kt1, a11), Join (kt2, a12)), true_atom),
+ Product (op2 (Join (kt1, a21), Join (kt2, a22)), false_atom))
+ end
and to_R_rep Ts t =
(case t of
@{const Not} => to_R_rep Ts (eta_expand Ts t 1)
@@ -180,15 +226,51 @@
| @{const HOL.implies} $ _ => to_R_rep Ts (eta_expand Ts t 1)
| @{const HOL.implies} => to_R_rep Ts (eta_expand Ts t 2)
| Const (@{const_name bot_class.bot},
- T as Type (@{type_name fun}, [_, @{typ bool}])) =>
- empty_n_ary_rel (arity_of R_Rep card T)
- | Const (@{const_name insert}, _) $ t1 $ t2 =>
- Union (to_S_rep Ts t1, to_R_rep Ts t2)
+ T as Type (@{type_name fun}, [T', @{typ bool}])) =>
+ if total then empty_n_ary_rel (arity_of (R_Rep total) card T)
+ else Product (atom_seq_product_of (R_Rep total) card T', false_atom)
+ | Const (@{const_name top_class.top},
+ T as Type (@{type_name fun}, [T', @{typ bool}])) =>
+ if total then atom_seq_product_of (R_Rep total) card T
+ else Product (atom_seq_product_of (R_Rep total) card T', true_atom)
+ | Const (@{const_name insert}, Type (_, [T, _])) $ t1 $ t2 =>
+ if total then
+ Union (to_S_rep Ts t1, to_R_rep Ts t2)
+ else
+ let
+ val kt1 = to_S_rep Ts t1
+ val kt2 = to_R_rep Ts t2
+ in
+ RelIf (Some kt1,
+ if arity_of S_Rep card T = 1 then
+ Override (kt2, Product (kt1, true_atom))
+ else
+ Union (Difference (kt2, Product (kt1, false_atom)),
+ Product (kt1, true_atom)),
+ Difference (kt2, Product (atom_seq_product_of S_Rep card T,
+ false_atom)))
+ end
| Const (@{const_name insert}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
| Const (@{const_name insert}, _) => to_R_rep Ts (eta_expand Ts t 2)
- | Const (@{const_name trancl}, _) $ t1 =>
- if arity_of R_Rep card (fastype_of1 (Ts, t1)) = 2 then
- Closure (to_R_rep Ts t1)
+ | Const (@{const_name trancl},
+ Type (_, [Type (_, [Type (_, [T', _]), _]), _])) $ t1 =>
+ if arity_of S_Rep card T' = 1 then
+ if total then
+ Closure (to_R_rep Ts t1)
+ else
+ let
+ val kt1 = to_R_rep Ts t1
+ val true_core_kt = Closure (Join (kt1, true_atom))
+ val kTx =
+ atom_seq_product_of S_Rep card (HOLogic.mk_prodT (`I T'))
+ val false_mantle_kt =
+ Difference (kTx,
+ Closure (Difference (kTx, Join (kt1, false_atom))))
+ in
+ Union (Product (Difference (false_mantle_kt, true_core_kt),
+ false_atom),
+ Product (true_core_kt, true_atom))
+ end
else
raise NOT_SUPPORTED "transitive closure for function or pair type"
| Const (@{const_name trancl}, _) => to_R_rep Ts (eta_expand Ts t 1)
@@ -196,7 +278,8 @@
Type (@{type_name fun},
[Type (@{type_name fun}, [_, @{typ bool}]), _]))
$ t1 $ t2 =>
- Intersect (to_R_rep Ts t1, to_R_rep Ts t2)
+ if total then Intersect (to_R_rep Ts t1, to_R_rep Ts t2)
+ else partial_set_op true true Intersect Union Ts t1 t2
| Const (@{const_name inf_class.inf}, _) $ _ =>
to_R_rep Ts (eta_expand Ts t 1)
| Const (@{const_name inf_class.inf}, _) =>
@@ -205,7 +288,8 @@
Type (@{type_name fun},
[Type (@{type_name fun}, [_, @{typ bool}]), _]))
$ t1 $ t2 =>
- Union (to_R_rep Ts t1, to_R_rep Ts t2)
+ if total then Union (to_R_rep Ts t1, to_R_rep Ts t2)
+ else partial_set_op true true Union Intersect Ts t1 t2
| Const (@{const_name sup_class.sup}, _) $ _ =>
to_R_rep Ts (eta_expand Ts t 1)
| Const (@{const_name sup_class.sup}, _) =>
@@ -214,7 +298,8 @@
Type (@{type_name fun},
[Type (@{type_name fun}, [_, @{typ bool}]), _]))
$ t1 $ t2 =>
- Difference (to_R_rep Ts t1, to_R_rep Ts t2)
+ if total then Difference (to_R_rep Ts t1, to_R_rep Ts t2)
+ else partial_set_op true false Intersect Union Ts t1 t2
| Const (@{const_name minus_class.minus},
Type (@{type_name fun},
[Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ =>
@@ -223,40 +308,47 @@
Type (@{type_name fun},
[Type (@{type_name fun}, [_, @{typ bool}]), _])) =>
to_R_rep Ts (eta_expand Ts t 2)
- | Const (@{const_name Pair}, _) $ _ $ _ => raise SAME ()
- | Const (@{const_name Pair}, _) $ _ => raise SAME ()
- | Const (@{const_name Pair}, _) => raise SAME ()
+ | Const (@{const_name Pair}, _) $ _ $ _ => to_S_rep Ts t
+ | Const (@{const_name Pair}, _) $ _ => to_S_rep Ts t
+ | Const (@{const_name Pair}, _) => to_S_rep Ts t
| Const (@{const_name fst}, _) $ _ => raise SAME ()
| Const (@{const_name fst}, _) => raise SAME ()
| Const (@{const_name snd}, _) $ _ => raise SAME ()
| Const (@{const_name snd}, _) => raise SAME ()
- | Const (_, @{typ bool}) => atom_from_formula (to_F Ts t)
+ | @{const False} => false_atom
+ | @{const True} => true_atom
| Free (x as (_, T)) =>
- Rel (arity_of R_Rep card T, find_index (curry (op =) x) frees)
+ Rel (arity_of (R_Rep total) card T, find_index (curry (op =) x) frees)
| Term.Var _ => raise NOT_SUPPORTED "schematic variables"
| Bound _ => raise SAME ()
| Abs (_, T, t') =>
- (case fastype_of1 (T :: Ts, t') of
- @{typ bool} => Comprehension (decls_for S_Rep card Ts T,
- to_F (T :: Ts) t')
- | T' => Comprehension (decls_for S_Rep card Ts T @
- decls_for R_Rep card (T :: Ts) T',
- Subset (rel_expr_for_bound_var card R_Rep
- (T' :: T :: Ts) 0,
- to_R_rep (T :: Ts) t')))
+ (case (total, fastype_of1 (T :: Ts, t')) of
+ (true, @{typ bool}) =>
+ Comprehension (decls_for S_Rep card Ts T, to_F NONE (T :: Ts) t')
+ | (_, T') =>
+ Comprehension (decls_for S_Rep card Ts T @
+ decls_for (R_Rep total) card (T :: Ts) T',
+ Subset (rel_expr_for_bound_var card (R_Rep total)
+ (T' :: T :: Ts) 0,
+ to_R_rep (T :: Ts) t')))
| t1 $ t2 =>
(case fastype_of1 (Ts, t) of
- @{typ bool} => atom_from_formula (to_F Ts t)
+ @{typ bool} =>
+ if total then
+ S_rep_from_F NONE (to_F NONE Ts t)
+ else
+ RelIf (to_F (SOME true) Ts t, true_atom,
+ RelIf (Not (to_F (SOME false) Ts t), false_atom,
+ None))
| T =>
let val T2 = fastype_of1 (Ts, t2) in
case arity_of S_Rep card T2 of
1 => Join (to_S_rep Ts t2, to_R_rep Ts t1)
| arity2 =>
- let val res_arity = arity_of R_Rep card T in
+ let val res_arity = arity_of (R_Rep total) card T in
Project (Intersect
(Product (to_S_rep Ts t2,
- atom_schema_of R_Rep card T
- |> map (AtomSeq o rpair 0) |> foldl1 Product),
+ atom_seq_product_of (R_Rep total) card T),
to_R_rep Ts t1),
num_seq arity2 res_arity)
end
@@ -264,28 +356,30 @@
| _ => raise NOT_SUPPORTED ("term " ^
quote (Syntax.string_of_term ctxt t)))
handle SAME () => R_rep_from_S_rep (fastype_of1 (Ts, t)) (to_S_rep Ts t)
- in to_F [] end
+ in to_F (if total then NONE else SOME true) [] end
-fun bound_for_free card i (s, T) =
- let val js = atom_schema_of R_Rep card T in
+fun bound_for_free total card i (s, T) =
+ let val js = atom_schema_of (R_Rep total) card T in
([((length js, i), s)],
- [TupleSet [], atom_schema_of R_Rep card T |> map (rpair 0)
+ [TupleSet [], atom_schema_of (R_Rep total) card T |> map (rpair 0)
|> tuple_set_from_atom_schema])
end
-fun declarative_axiom_for_rel_expr card Ts (Type (@{type_name fun}, [T1, T2]))
- r =
- if body_type T2 = bool_T then
+fun declarative_axiom_for_rel_expr total card Ts
+ (Type (@{type_name fun}, [T1, T2])) r =
+ if total andalso body_type T2 = bool_T then
True
else
All (decls_for S_Rep card Ts T1,
- declarative_axiom_for_rel_expr card (T1 :: Ts) T2
+ declarative_axiom_for_rel_expr total card (T1 :: Ts) T2
(List.foldl Join r (vars_for_bound_var card S_Rep (T1 :: Ts) 0)))
- | declarative_axiom_for_rel_expr _ _ _ r = One r
-fun declarative_axiom_for_free card i (_, T) =
- declarative_axiom_for_rel_expr card [] T (Rel (arity_of R_Rep card T, i))
+ | declarative_axiom_for_rel_expr total _ _ _ r =
+ (if total then One else Lone) r
+fun declarative_axiom_for_free total card i (_, T) =
+ declarative_axiom_for_rel_expr total card [] T
+ (Rel (arity_of (R_Rep total) card T, i))
-fun kodkod_problem_from_term ctxt raw_card t =
+fun kodkod_problem_from_term ctxt total raw_card raw_infinite t =
let
val thy = ProofContext.theory_of ctxt
fun card (Type (@{type_name fun}, [T1, T2])) =
@@ -293,14 +387,25 @@
| card (Type (@{type_name prod}, [T1, T2])) = card T1 * card T2
| card @{typ bool} = 2
| card T = Int.max (1, raw_card T)
+ fun complete (Type (@{type_name fun}, [T1, T2])) =
+ concrete T1 andalso complete T2
+ | complete (Type (@{type_name prod}, Ts)) = forall complete Ts
+ | complete T = not (raw_infinite T)
+ and concrete (Type (@{type_name fun}, [T1, T2])) =
+ complete T1 andalso concrete T2
+ | concrete (Type (@{type_name prod}, Ts)) = forall concrete Ts
+ | concrete _ = true
val neg_t = @{const Not} $ Object_Logic.atomize_term thy t
- val _ = fold_types (K o check_type ctxt) neg_t ()
+ val _ = fold_types (K o check_type ctxt raw_infinite) neg_t ()
val frees = Term.add_frees neg_t []
- val bounds = map2 (bound_for_free card) (index_seq 0 (length frees)) frees
+ val bounds =
+ map2 (bound_for_free total card) (index_seq 0 (length frees)) frees
val declarative_axioms =
- map2 (declarative_axiom_for_free card) (index_seq 0 (length frees)) frees
- val formula = kodkod_formula_from_term ctxt card frees neg_t
- |> fold_rev (curry And) declarative_axioms
+ map2 (declarative_axiom_for_free total card)
+ (index_seq 0 (length frees)) frees
+ val formula =
+ neg_t |> kodkod_formula_from_term ctxt total card complete concrete frees
+ |> fold_rev (curry And) declarative_axioms
val univ_card = univ_card 0 0 0 bounds formula
in
{comment = "", settings = [], univ_card = univ_card, tuple_assigns = [],
@@ -324,4 +429,28 @@
| Error (s, _) => error ("Kodkod error: " ^ s)
end
+val default_raw_infinite = member (op =) [@{typ nat}, @{typ int}]
+
+fun minipick ctxt n t =
+ let
+ val thy = ProofContext.theory_of ctxt
+ val {total_consts, ...} = Nitpick_Isar.default_params thy []
+ val totals =
+ total_consts |> Option.map single |> the_default [true, false]
+ fun problem_for (total, k) =
+ kodkod_problem_from_term ctxt total (K k) default_raw_infinite t
+ in
+ (totals, 1 upto n)
+ |-> map_product pair
+ |> map problem_for
+ |> solve_any_kodkod_problem (Proof_Context.theory_of ctxt)
+ end
+
+fun minipick_expect ctxt expect n t =
+ if getenv "KODKODI" <> "" then
+ if minipick ctxt n t = expect then ()
+ else error ("\"minipick_expect\" expected " ^ quote expect)
+ else
+ ()
+
end;