# HG changeset patch # User blanchet # Date 1316780753 -7200 # Node ID 9598cada31b351ceb57e16dd68acffd8bb763904 # Parent 39519609abe0c35e6beab7fed768a2bcf0e1d96b first step towards extending Minipick with more translations diff -r 39519609abe0 -r 9598cada31b3 src/HOL/Nitpick_Examples/Mini_Nits.thy --- 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 "\x. x = x"} *} ML {* none 1 @{prop "\x. x = y"} *} ML {* genuine 2 @{prop "\x. x = y"} *} -ML {* none 1 @{prop "\x. x = y"} *} ML {* none 2 @{prop "\x. x = y"} *} ML {* none 2 @{prop "\x\'a \ 'a. x = x"} *} ML {* none 2 @{prop "\x\'a \ 'a. x = y"} *} @@ -74,6 +67,9 @@ ML {* genuine 2 @{prop "{a} = {a, b}"} *} ML {* genuine 1 @{prop "{a} \ {a, b}"} *} ML {* none 5 @{prop "{}\<^sup>+ = {}"} *} +ML {* none 5 @{prop "UNIV\<^sup>+ = UNIV"} *} +ML {* none 5 @{prop "(UNIV\'a \ 'b \ bool) - {} = UNIV"} *} +ML {* none 5 @{prop "{} - (UNIV\'a \ 'b \ 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 \ c \ {(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) \ b"} *} +ML {* genuine 2 @{prop "f ((x, z), y) = (x, z)"} *} +ML {* none 2 @{prop "(ALL x. f x = fst x) \ 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 "\f. \a b. f (a, b) = (a, b)"} *} ML {* none 3 @{prop "f = (\a b. (b, a)) \ f x y = (y, x)"} *} ML {* genuine 2 @{prop "f = (\a b. (b, a)) \ f x y = (x, y)"} *} +ML {* none 5 @{prop "f = (\x. f x)"} *} +ML {* none 5 @{prop "f = (\x. f x\'a \ bool)"} *} +ML {* none 5 @{prop "f = (\x y. f x y)"} *} +ML {* none 5 @{prop "f = (\x y. f x y\'a \ bool)"} *} end diff -r 39519609abe0 -r 9598cada31b3 src/HOL/Nitpick_Examples/minipick.ML --- 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;