{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeApplications #-}

module Constrained.Examples.Tree where

import Constrained.API
import Constrained.Spec.Tree (BinTree (..))
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 ->
      -- TODO: if there was a `binTreeRoot` function on trees
      -- this wouldn't need to be quadratic as we would
      -- only check agains the head of the left and right
      -- subtrees, not _every element_
      [ 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
  ]