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