{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeApplications #-}
module Constrained.Examples.Tree where
import Constrained.API
import Constrained.Spec.Tree (BinTree (..), rootLabel_)
import Data.Tree
allZeroTree :: Specification (BinTree Int)
allZeroTree :: Specification (BinTree Int)
allZeroTree = (Term (BinTree Int) -> [Pred]) -> Specification (BinTree Int)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (BinTree Int) -> [Pred]) -> Specification (BinTree Int))
-> (Term (BinTree Int) -> [Pred]) -> Specification (BinTree Int)
forall a b. (a -> b) -> a -> b
$ \Term (BinTree Int)
t ->
[ Term (BinTree Int)
-> FunTy
(MapList Term (Args (SimpleRep (BinTree Int, Int, BinTree Int))))
(Term Bool)
-> Pred
forall t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec t,
HasSpec (SimpleRep a), HasSimpleRep a,
All HasSpec (Args (SimpleRep a)), IsPred p, IsProd (SimpleRep a),
IsProductType a, HasSpec a, GenericRequires a,
ProdAsListComputes a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (BinTree Int)
t (FunTy
(MapList Term (Args (SimpleRep (BinTree Int, Int, BinTree Int))))
(Term Bool)
-> Pred)
-> FunTy
(MapList Term (Args (SimpleRep (BinTree Int, Int, BinTree Int))))
(Term Bool)
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term (BinTree Int)
_ Term Int
a Term (BinTree Int)
_ -> Term Int
a Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
0
, Hint (BinTree Int) -> Term (BinTree Int) -> Pred
forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint Integer
Hint (BinTree Int)
10 Term (BinTree Int)
t
]
isBST :: Specification (BinTree Int)
isBST :: Specification (BinTree Int)
isBST = (Term (BinTree Int) -> [Pred]) -> Specification (BinTree Int)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (BinTree Int) -> [Pred]) -> Specification (BinTree Int))
-> (Term (BinTree Int) -> [Pred]) -> Specification (BinTree Int)
forall a b. (a -> b) -> a -> b
$ \Term (BinTree Int)
t ->
[ Term (BinTree Int)
-> FunTy
(MapList Term (Args (SimpleRep (BinTree Int, Int, BinTree Int))))
[Pred]
-> Pred
forall t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec t,
HasSpec (SimpleRep a), HasSimpleRep a,
All HasSpec (Args (SimpleRep a)), IsPred p, IsProd (SimpleRep a),
IsProductType a, HasSpec a, GenericRequires a,
ProdAsListComputes a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (BinTree Int)
t (FunTy
(MapList Term (Args (SimpleRep (BinTree Int, Int, BinTree Int))))
[Pred]
-> Pred)
-> FunTy
(MapList Term (Args (SimpleRep (BinTree Int, Int, BinTree Int))))
[Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term (BinTree Int)
left Term Int
a Term (BinTree Int)
right ->
[ Term (BinTree Int)
-> FunTy
(MapList Term (Args (SimpleRep (BinTree Int, Int, BinTree Int))))
(Term Bool)
-> Pred
forall t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec t,
HasSpec (SimpleRep a), HasSimpleRep a,
All HasSpec (Args (SimpleRep a)), IsPred p, IsProd (SimpleRep a),
IsProductType a, HasSpec a, GenericRequires a,
ProdAsListComputes a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (BinTree Int)
left (FunTy
(MapList Term (Args (SimpleRep (BinTree Int, Int, BinTree Int))))
(Term Bool)
-> Pred)
-> FunTy
(MapList Term (Args (SimpleRep (BinTree Int, Int, BinTree Int))))
(Term Bool)
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term (BinTree Int)
_ Term Int
l Term (BinTree Int)
_ -> Term Int
l Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
a
, Term (BinTree Int)
-> FunTy
(MapList Term (Args (SimpleRep (BinTree Int, Int, BinTree Int))))
(Term Bool)
-> Pred
forall t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec t,
HasSpec (SimpleRep a), HasSimpleRep a,
All HasSpec (Args (SimpleRep a)), IsPred p, IsProd (SimpleRep a),
IsProductType a, HasSpec a, GenericRequires a,
ProdAsListComputes a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (BinTree Int)
right (FunTy
(MapList Term (Args (SimpleRep (BinTree Int, Int, BinTree Int))))
(Term Bool)
-> Pred)
-> FunTy
(MapList Term (Args (SimpleRep (BinTree Int, Int, BinTree Int))))
(Term Bool)
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term (BinTree Int)
_ Term Int
h Term (BinTree Int)
_ -> Term Int
a Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
h
]
, Hint (BinTree Int) -> Term (BinTree Int) -> Pred
forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint Integer
Hint (BinTree Int)
10 Term (BinTree Int)
t
]
noChildrenSameTree :: Specification (BinTree Int)
noChildrenSameTree :: Specification (BinTree Int)
noChildrenSameTree = (Term (BinTree Int) -> [Pred]) -> Specification (BinTree Int)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (BinTree Int) -> [Pred]) -> Specification (BinTree Int))
-> (Term (BinTree Int) -> [Pred]) -> Specification (BinTree Int)
forall a b. (a -> b) -> a -> b
$ \Term (BinTree Int)
t ->
[ Term (BinTree Int)
-> FunTy
(MapList Term (Args (SimpleRep (BinTree Int, Int, BinTree Int))))
[Pred]
-> Pred
forall t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec t,
HasSpec (SimpleRep a), HasSimpleRep a,
All HasSpec (Args (SimpleRep a)), IsPred p, IsProd (SimpleRep a),
IsProductType a, HasSpec a, GenericRequires a,
ProdAsListComputes a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (BinTree Int)
t (FunTy
(MapList Term (Args (SimpleRep (BinTree Int, Int, BinTree Int))))
[Pred]
-> Pred)
-> FunTy
(MapList Term (Args (SimpleRep (BinTree Int, Int, BinTree Int))))
[Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term (BinTree Int)
left Term Int
a Term (BinTree Int)
right ->
[ Term (BinTree Int)
-> FunTy
(MapList Term (Args (SimpleRep (BinTree Int, Int, BinTree Int))))
(Term Bool)
-> Pred
forall t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec t,
HasSpec (SimpleRep a), HasSimpleRep a,
All HasSpec (Args (SimpleRep a)), IsPred p, IsProd (SimpleRep a),
IsProductType a, HasSpec a, GenericRequires a,
ProdAsListComputes a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (BinTree Int)
left (FunTy
(MapList Term (Args (SimpleRep (BinTree Int, Int, BinTree Int))))
(Term Bool)
-> Pred)
-> FunTy
(MapList Term (Args (SimpleRep (BinTree Int, Int, BinTree Int))))
(Term Bool)
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term (BinTree Int)
_ Term Int
l Term (BinTree Int)
_ -> Term Int
l Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
/=. Term Int
a
, Term (BinTree Int)
-> FunTy
(MapList Term (Args (SimpleRep (BinTree Int, Int, BinTree Int))))
(Term Bool)
-> Pred
forall t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec t,
HasSpec (SimpleRep a), HasSimpleRep a,
All HasSpec (Args (SimpleRep a)), IsPred p, IsProd (SimpleRep a),
IsProductType a, HasSpec a, GenericRequires a,
ProdAsListComputes a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (BinTree Int)
right (FunTy
(MapList Term (Args (SimpleRep (BinTree Int, Int, BinTree Int))))
(Term Bool)
-> Pred)
-> FunTy
(MapList Term (Args (SimpleRep (BinTree Int, Int, BinTree Int))))
(Term Bool)
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term (BinTree Int)
_ Term Int
r Term (BinTree Int)
_ -> Term Int
r Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
/=. Term Int
a
]
, Hint (BinTree Int) -> Term (BinTree Int) -> Pred
forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint Integer
Hint (BinTree Int)
8 Term (BinTree Int)
t
]
isAllZeroTree :: Specification (Tree Int)
isAllZeroTree :: Specification (Tree Int)
isAllZeroTree = (Term (Tree Int) -> [Pred]) -> Specification (Tree Int)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Tree Int) -> [Pred]) -> Specification (Tree Int))
-> (Term (Tree Int) -> [Pred]) -> Specification (Tree Int)
forall a b. (a -> b) -> a -> b
$ \Term (Tree Int)
t ->
[ Term (Tree Int)
-> FunTy
(MapList Term (Args (SimpleRep (Int, [Tree Int])))) [Term Bool]
-> Pred
forall t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec t,
HasSpec (SimpleRep a), HasSimpleRep a,
All HasSpec (Args (SimpleRep a)), IsPred p, IsProd (SimpleRep a),
IsProductType a, HasSpec a, GenericRequires a,
ProdAsListComputes a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (Tree Int)
t (FunTy
(MapList Term (Args (SimpleRep (Int, [Tree Int])))) [Term Bool]
-> Pred)
-> FunTy
(MapList Term (Args (SimpleRep (Int, [Tree Int])))) [Term Bool]
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term Int
a Term [Tree Int]
cs ->
[ Term Int
a Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
0
, Term [Tree Int] -> Term Integer
forall a. HasSpec a => Term [a] -> Term Integer
length_ Term [Tree Int]
cs Term Integer -> Term Integer -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Integer
4
]
, Hint (Tree Int) -> Term (Tree Int) -> Pred
forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
2, Integer
30) Term (Tree Int)
t
]
noSameChildrenTree :: Specification (Tree Int)
noSameChildrenTree :: Specification (Tree Int)
noSameChildrenTree = (Term (Tree Int) -> [Pred]) -> Specification (Tree Int)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Tree Int) -> [Pred]) -> Specification (Tree Int))
-> (Term (Tree Int) -> [Pred]) -> Specification (Tree Int)
forall a b. (a -> b) -> a -> b
$ \Term (Tree Int)
t ->
[ Term (Tree Int)
-> FunTy (MapList Term (Args (SimpleRep (Int, [Tree Int])))) [Pred]
-> Pred
forall t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec t,
HasSpec (SimpleRep a), HasSimpleRep a,
All HasSpec (Args (SimpleRep a)), IsPred p, IsProd (SimpleRep a),
IsProductType a, HasSpec a, GenericRequires a,
ProdAsListComputes a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (Tree Int)
t (FunTy (MapList Term (Args (SimpleRep (Int, [Tree Int])))) [Pred]
-> Pred)
-> FunTy (MapList Term (Args (SimpleRep (Int, [Tree Int])))) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term Int
a Term [Tree Int]
cs ->
[ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Int
a Term Int -> Term [Int] -> Term Bool
forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
`elem_` [Int] -> Term [Int]
forall a. HasSpec a => a -> Term a
lit [Int
1 .. Int
8]
, Term [Tree Int] -> (Term (Tree Int) -> Pred) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [Tree Int]
cs ((Term (Tree Int) -> Pred) -> Pred)
-> (Term (Tree Int) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term (Tree Int)
t' ->
Term (Tree Int)
-> FunTy
(MapList Term (Args (SimpleRep (Int, [Tree Int])))) (Term Bool)
-> Pred
forall t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec t,
HasSpec (SimpleRep a), HasSimpleRep a,
All HasSpec (Args (SimpleRep a)), IsPred p, IsProd (SimpleRep a),
IsProductType a, HasSpec a, GenericRequires a,
ProdAsListComputes a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (Tree Int)
t' (FunTy
(MapList Term (Args (SimpleRep (Int, [Tree Int])))) (Term Bool)
-> Pred)
-> FunTy
(MapList Term (Args (SimpleRep (Int, [Tree Int])))) (Term Bool)
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term Int
b Term [Tree Int]
_ ->
Term Int
b Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
/=. Term Int
a
]
, Hint (Tree Int) -> Term (Tree Int) -> Pred
forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
2, Integer
30) Term (Tree Int)
t
]
successiveChildren :: Specification (Tree Int)
successiveChildren :: Specification (Tree Int)
successiveChildren = (Term (Tree Int) -> [Pred]) -> Specification (Tree Int)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Tree Int) -> [Pred]) -> Specification (Tree Int))
-> (Term (Tree Int) -> [Pred]) -> Specification (Tree Int)
forall a b. (a -> b) -> a -> b
$ \Term (Tree Int)
t ->
[ Term (Tree Int)
-> FunTy (MapList Term (Args (SimpleRep (Int, [Tree Int])))) [Pred]
-> Pred
forall t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec t,
HasSpec (SimpleRep a), HasSimpleRep a,
All HasSpec (Args (SimpleRep a)), IsPred p, IsProd (SimpleRep a),
IsProductType a, HasSpec a, GenericRequires a,
ProdAsListComputes a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (Tree Int)
t (FunTy (MapList Term (Args (SimpleRep (Int, [Tree Int])))) [Pred]
-> Pred)
-> FunTy (MapList Term (Args (SimpleRep (Int, [Tree Int])))) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term Int
a Term [Tree Int]
cs ->
[ Term [Tree Int] -> (Term (Tree Int) -> Term Bool) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [Tree Int]
cs ((Term (Tree Int) -> Term Bool) -> Pred)
-> (Term (Tree Int) -> Term Bool) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term (Tree Int)
t' ->
Term (Tree Int) -> Term Int
forall a. HasSpec a => Term (Tree a) -> Term a
rootLabel_ Term (Tree Int)
t' Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
a Term Int -> Term Int -> Term Int
forall a. Num a => a -> a -> a
+ Term Int
1
]
, Hint (Tree Int) -> Term (Tree Int) -> Pred
forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
2, Integer
10) Term (Tree Int)
t
]
successiveChildren8 :: Specification (Tree Int)
successiveChildren8 :: Specification (Tree Int)
successiveChildren8 = (Term (Tree Int) -> [Pred]) -> Specification (Tree Int)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Tree Int) -> [Pred]) -> Specification (Tree Int))
-> (Term (Tree Int) -> [Pred]) -> Specification (Tree Int)
forall a b. (a -> b) -> a -> b
$ \Term (Tree Int)
t ->
[ Term (Tree Int)
t Term (Tree Int) -> Specification (Tree Int) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification (Tree Int)
successiveChildren
, Term (Tree Int)
-> FunTy
(MapList Term (Args (SimpleRep (Int, [Tree Int])))) (Term Bool)
-> Pred
forall t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec t,
HasSpec (SimpleRep a), HasSimpleRep a,
All HasSpec (Args (SimpleRep a)), IsPred p, IsProd (SimpleRep a),
IsProductType a, HasSpec a, GenericRequires a,
ProdAsListComputes a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (Tree Int)
t (FunTy
(MapList Term (Args (SimpleRep (Int, [Tree Int])))) (Term Bool)
-> Pred)
-> FunTy
(MapList Term (Args (SimpleRep (Int, [Tree Int])))) (Term Bool)
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term Int
a Term [Tree Int]
_ -> Term Int
a Term Int -> Term [Int] -> Term Bool
forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
`elem_` [Int] -> Term [Int]
forall a. HasSpec a => a -> Term a
lit [Int
1 .. Int
5]
]
roseTreeList :: Specification [Tree Int]
roseTreeList :: Specification [Tree Int]
roseTreeList = (Term [Tree Int] -> [Pred]) -> Specification [Tree Int]
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term [Tree Int] -> [Pred]) -> Specification [Tree Int])
-> (Term [Tree Int] -> [Pred]) -> Specification [Tree Int]
forall a b. (a -> b) -> a -> b
$ \Term [Tree Int]
ts ->
[ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term [Tree Int] -> Term Integer
forall a. HasSpec a => Term [a] -> Term Integer
length_ Term [Tree Int]
ts Term Integer -> Term Integer -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Integer
10
, Term [Tree Int] -> (Term (Tree Int) -> [Pred]) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [Tree Int]
ts ((Term (Tree Int) -> [Pred]) -> Pred)
-> (Term (Tree Int) -> [Pred]) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term (Tree Int)
t ->
[ Term (Tree Int) -> (Term (Int, [Tree Int]) -> Bool) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Tree Int)
t ((Term (Int, [Tree Int]) -> Bool) -> Pred)
-> (Term (Int, [Tree Int]) -> Bool) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term (Int, [Tree Int])
_ -> Bool
False
]
]
roseTreePairs :: Specification (Tree ([Int], [Int]))
roseTreePairs :: Specification (Tree ([Int], [Int]))
roseTreePairs = (Term (Tree ([Int], [Int])) -> [Pred])
-> Specification (Tree ([Int], [Int]))
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Tree ([Int], [Int])) -> [Pred])
-> Specification (Tree ([Int], [Int])))
-> (Term (Tree ([Int], [Int])) -> [Pred])
-> Specification (Tree ([Int], [Int]))
forall a b. (a -> b) -> a -> b
$ \Term (Tree ([Int], [Int]))
t ->
[ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Tree ([Int], [Int])) -> Term ([Int], [Int])
forall a. HasSpec a => Term (Tree a) -> Term a
rootLabel_ Term (Tree ([Int], [Int]))
t Term ([Int], [Int]) -> Term ([Int], [Int]) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. ([Int], [Int]) -> Term ([Int], [Int])
forall a. HasSpec a => a -> Term a
lit ([Int
1 .. Int
10], [Int
1 .. Int
10])
, Term (Tree ([Int], [Int]))
-> FunTy
(MapList
Term (Args (SimpleRep (([Int], [Int]), [Tree ([Int], [Int])]))))
Pred
-> Pred
forall t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec t,
HasSpec (SimpleRep a), HasSimpleRep a,
All HasSpec (Args (SimpleRep a)), IsPred p, IsProd (SimpleRep a),
IsProductType a, HasSpec a, GenericRequires a,
ProdAsListComputes a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (Tree ([Int], [Int]))
t (FunTy
(MapList
Term (Args (SimpleRep (([Int], [Int]), [Tree ([Int], [Int])]))))
Pred
-> Pred)
-> FunTy
(MapList
Term (Args (SimpleRep (([Int], [Int]), [Tree ([Int], [Int])]))))
Pred
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term ([Int], [Int])
p Term [Tree ([Int], [Int])]
ts ->
Term [Tree ([Int], [Int])]
-> (Term (Tree ([Int], [Int])) -> Term Bool) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [Tree ([Int], [Int])]
ts ((Term (Tree ([Int], [Int])) -> Term Bool) -> Pred)
-> (Term (Tree ([Int], [Int])) -> Term Bool) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term (Tree ([Int], [Int]))
t' ->
Term ([Int], [Int]) -> Term [Int]
forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term x
fst_ (Term (Tree ([Int], [Int])) -> Term ([Int], [Int])
forall a. HasSpec a => Term (Tree a) -> Term a
rootLabel_ Term (Tree ([Int], [Int]))
t') Term [Int] -> Term [Int] -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term ([Int], [Int]) -> Term [Int]
forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term y
snd_ Term ([Int], [Int])
p
, Hint (Tree ([Int], [Int])) -> Term (Tree ([Int], [Int])) -> Pred
forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint (Maybe Integer
forall a. Maybe a
Nothing, Integer
10) Term (Tree ([Int], [Int]))
t
]
roseTreeMaybe :: Specification (Tree (Maybe (Int, Int)))
roseTreeMaybe :: Specification (Tree (Maybe (Int, Int)))
roseTreeMaybe = (Term (Tree (Maybe (Int, Int))) -> [Pred])
-> Specification (Tree (Maybe (Int, Int)))
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Tree (Maybe (Int, Int))) -> [Pred])
-> Specification (Tree (Maybe (Int, Int))))
-> (Term (Tree (Maybe (Int, Int))) -> [Pred])
-> Specification (Tree (Maybe (Int, Int)))
forall a b. (a -> b) -> a -> b
$ \Term (Tree (Maybe (Int, Int)))
t ->
[ Term (Tree (Maybe (Int, Int)))
-> FunTy
(MapList
Term
(Args (SimpleRep (Maybe (Int, Int), [Tree (Maybe (Int, Int))]))))
Pred
-> Pred
forall t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec t,
HasSpec (SimpleRep a), HasSimpleRep a,
All HasSpec (Args (SimpleRep a)), IsPred p, IsProd (SimpleRep a),
IsProductType a, HasSpec a, GenericRequires a,
ProdAsListComputes a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (Tree (Maybe (Int, Int)))
t (FunTy
(MapList
Term
(Args (SimpleRep (Maybe (Int, Int), [Tree (Maybe (Int, Int))]))))
Pred
-> Pred)
-> FunTy
(MapList
Term
(Args (SimpleRep (Maybe (Int, Int), [Tree (Maybe (Int, Int))]))))
Pred
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term (Maybe (Int, Int))
mp Term [Tree (Maybe (Int, Int))]
ts ->
Term [Tree (Maybe (Int, Int))]
-> (Term (Tree (Maybe (Int, Int))) -> Pred) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [Tree (Maybe (Int, Int))]
ts ((Term (Tree (Maybe (Int, Int))) -> Pred) -> Pred)
-> (Term (Tree (Maybe (Int, Int))) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term (Tree (Maybe (Int, Int)))
t' ->
Term (Maybe (Int, Int)) -> (Term (Int, Int) -> Pred) -> Pred
forall a p.
(HasSpec a, IsNormalType a, IsPred p) =>
Term (Maybe a) -> (Term a -> p) -> Pred
onJust Term (Maybe (Int, Int))
mp ((Term (Int, Int) -> Pred) -> Pred)
-> (Term (Int, Int) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term (Int, Int)
p ->
Term (Maybe (Int, Int)) -> (Term (Int, Int) -> Term Bool) -> Pred
forall a p.
(HasSpec a, IsNormalType a, IsPred p) =>
Term (Maybe a) -> (Term a -> p) -> Pred
onJust (Term (Tree (Maybe (Int, Int))) -> Term (Maybe (Int, Int))
forall a. HasSpec a => Term (Tree a) -> Term a
rootLabel_ Term (Tree (Maybe (Int, Int)))
t') ((Term (Int, Int) -> Term Bool) -> Pred)
-> (Term (Int, Int) -> Term Bool) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term (Int, Int)
p' ->
Term (Int, Int) -> Term Int
forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term x
fst_ Term (Int, Int)
p' Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term (Int, Int) -> Term Int
forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term y
snd_ Term (Int, Int)
p
, Term (Tree (Maybe (Int, Int)))
-> FunTy
(MapList
Term
(Args (SimpleRep (Maybe (Int, Int), [Tree (Maybe (Int, Int))]))))
Pred
-> Pred
forall t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec t,
HasSpec (SimpleRep a), HasSimpleRep a,
All HasSpec (Args (SimpleRep a)), IsPred p, IsProd (SimpleRep a),
IsProductType a, HasSpec a, GenericRequires a,
ProdAsListComputes a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (Tree (Maybe (Int, Int)))
t (FunTy
(MapList
Term
(Args (SimpleRep (Maybe (Int, Int), [Tree (Maybe (Int, Int))]))))
Pred
-> Pred)
-> FunTy
(MapList
Term
(Args (SimpleRep (Maybe (Int, Int), [Tree (Maybe (Int, Int))]))))
Pred
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term (Maybe (Int, Int))
mp Term [Tree (Maybe (Int, Int))]
_ -> Term (Maybe (Int, Int)) -> Pred
forall a. (HasSpec a, IsNormalType a) => Term (Maybe a) -> Pred
isJust Term (Maybe (Int, Int))
mp
, Hint (Tree (Maybe (Int, Int)))
-> Term (Tree (Maybe (Int, Int))) -> Pred
forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint (Maybe Integer
forall a. Maybe a
Nothing, Integer
10) Term (Tree (Maybe (Int, Int)))
t
]
badTreeInteraction :: Specification (Tree (Either Int Int))
badTreeInteraction :: Specification (Tree (Either Int Int))
badTreeInteraction = (Term (Tree (Either Int Int)) -> [Pred])
-> Specification (Tree (Either Int Int))
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Tree (Either Int Int)) -> [Pred])
-> Specification (Tree (Either Int Int)))
-> (Term (Tree (Either Int Int)) -> [Pred])
-> Specification (Tree (Either Int Int))
forall a b. (a -> b) -> a -> b
$ \Term (Tree (Either Int Int))
t ->
[ Term (Tree (Either Int Int))
-> FunTy
(MapList
Term (Args (SimpleRep (Either Int Int, [Tree (Either Int Int)]))))
[Pred]
-> Pred
forall t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec t,
HasSpec (SimpleRep a), HasSimpleRep a,
All HasSpec (Args (SimpleRep a)), IsPred p, IsProd (SimpleRep a),
IsProductType a, HasSpec a, GenericRequires a,
ProdAsListComputes a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (Tree (Either Int Int))
t (FunTy
(MapList
Term (Args (SimpleRep (Either Int Int, [Tree (Either Int Int)]))))
[Pred]
-> Pred)
-> FunTy
(MapList
Term (Args (SimpleRep (Either Int Int, [Tree (Either Int Int)]))))
[Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term (Either Int Int)
n Term [Tree (Either Int Int)]
ts' ->
[ forall (c :: Symbol) a.
(IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a),
SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a,
All HasSpec (Cases (SOP (TheSop a))),
HasSpec (ProdOver (ConstrOf c (TheSop a))), GenericRequires a) =>
Term a -> Pred
isCon @"Right" Term (Either Int Int)
n
, Term [Tree (Either Int Int)]
-> (Term (Tree (Either Int Int)) -> Bool) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [Tree (Either Int Int)]
ts' ((Term (Tree (Either Int Int)) -> Bool) -> Pred)
-> (Term (Tree (Either Int Int)) -> Bool) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term (Tree (Either Int Int))
_ -> Bool
True
]
, Term (Tree (Either Int Int))
-> FunTy
(MapList
Term (Args (SimpleRep (Either Int Int, [Tree (Either Int Int)]))))
Pred
-> Pred
forall t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec t,
HasSpec (SimpleRep a), HasSimpleRep a,
All HasSpec (Args (SimpleRep a)), IsPred p, IsProd (SimpleRep a),
IsProductType a, HasSpec a, GenericRequires a,
ProdAsListComputes a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (Tree (Either Int Int))
t (FunTy
(MapList
Term (Args (SimpleRep (Either Int Int, [Tree (Either Int Int)]))))
Pred
-> Pred)
-> FunTy
(MapList
Term (Args (SimpleRep (Either Int Int, [Tree (Either Int Int)]))))
Pred
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term (Either Int Int)
n Term [Tree (Either Int Int)]
ts' ->
Term [Tree (Either Int Int)]
-> (Term (Tree (Either Int Int)) -> [Pred]) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [Tree (Either Int Int)]
ts' ((Term (Tree (Either Int Int)) -> [Pred]) -> Pred)
-> (Term (Tree (Either Int Int)) -> [Pred]) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term (Tree (Either Int Int))
t' ->
[ Hint (Tree (Either Int Int))
-> Term (Tree (Either Int Int)) -> Pred
forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
4, Integer
10) Term (Tree (Either Int Int))
t'
, Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Tree (Either Int Int)) -> Term (Either Int Int)
forall a. HasSpec a => Term (Tree a) -> Term a
rootLabel_ Term (Tree (Either Int Int))
t' Term (Either Int Int) -> Term (Either Int Int) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term (Either Int Int)
n
]
, Hint (Tree (Either Int Int))
-> Term (Tree (Either Int Int)) -> Pred
forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
4, Integer
10) Term (Tree (Either Int Int))
t
]