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

module Constrained.Examples.Tree where

import Data.Tree

import Constrained

allZeroTree :: Specification BaseFn (BinTree Int)
allZeroTree :: Specification BaseFn (BinTree Int)
allZeroTree = forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term BaseFn (BinTree Int)
t ->
  [ forall (fn :: [*] -> * -> *) t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn t,
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsPred p fn,
 IsProd (SimpleRep a), HasSpec fn a) =>
Term fn t
-> FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> Pred fn
forAll' Term BaseFn (BinTree Int)
t forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (BinTree Int)
_ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
a Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (BinTree Int)
_ -> Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
a forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
0
  , forall (fn :: [*] -> * -> *) t.
HasGenHint fn t =>
Hint t -> Term fn t -> Pred fn
genHint Integer
10 Term BaseFn (BinTree Int)
t
  ]

isBST :: Specification BaseFn (BinTree Int)
isBST :: Specification BaseFn (BinTree Int)
isBST = forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term BaseFn (BinTree Int)
t ->
  [ forall (fn :: [*] -> * -> *) t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn t,
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsPred p fn,
 IsProd (SimpleRep a), HasSpec fn a) =>
Term fn t
-> FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> Pred fn
forAll' Term BaseFn (BinTree Int)
t forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (BinTree Int)
left Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
a Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (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_
      [ forall (fn :: [*] -> * -> *) t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn t,
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsPred p fn,
 IsProd (SimpleRep a), HasSpec fn a) =>
Term fn t
-> FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> Pred fn
forAll' Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (BinTree Int)
left forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (BinTree Int)
_ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
l Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (BinTree Int)
_ -> Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
l forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
a
      , forall (fn :: [*] -> * -> *) t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn t,
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsPred p fn,
 IsProd (SimpleRep a), HasSpec fn a) =>
Term fn t
-> FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> Pred fn
forAll' Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (BinTree Int)
right forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (BinTree Int)
_ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
h Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (BinTree Int)
_ -> Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
a forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
h
      ]
  , forall (fn :: [*] -> * -> *) t.
HasGenHint fn t =>
Hint t -> Term fn t -> Pred fn
genHint Integer
10 Term BaseFn (BinTree Int)
t
  ]

noChildrenSameTree :: Specification BaseFn (BinTree Int)
noChildrenSameTree :: Specification BaseFn (BinTree Int)
noChildrenSameTree = forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term BaseFn (BinTree Int)
t ->
  [ forall (fn :: [*] -> * -> *) t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn t,
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsPred p fn,
 IsProd (SimpleRep a), HasSpec fn a) =>
Term fn t
-> FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> Pred fn
forAll' Term BaseFn (BinTree Int)
t forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (BinTree Int)
left Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
a Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (BinTree Int)
right ->
      [ forall (fn :: [*] -> * -> *) t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn t,
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsPred p fn,
 IsProd (SimpleRep a), HasSpec fn a) =>
Term fn t
-> FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> Pred fn
forAll' Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (BinTree Int)
left forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (BinTree Int)
_ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
l Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (BinTree Int)
_ -> Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
l forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
/=. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
a
      , forall (fn :: [*] -> * -> *) t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn t,
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsPred p fn,
 IsProd (SimpleRep a), HasSpec fn a) =>
Term fn t
-> FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> Pred fn
forAll' Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (BinTree Int)
right forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (BinTree Int)
_ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
r Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (BinTree Int)
_ -> Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
r forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
/=. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
a
      ]
  , forall (fn :: [*] -> * -> *) t.
HasGenHint fn t =>
Hint t -> Term fn t -> Pred fn
genHint Integer
8 Term BaseFn (BinTree Int)
t
  ]

type RoseFn = Fix (OneofL (TreeFn : BaseFns))

isAllZeroTree :: Specification RoseFn (Tree Int)
isAllZeroTree :: Specification RoseFn (Tree Int)
isAllZeroTree = forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term RoseFn (Tree Int)
t ->
  [ forall (fn :: [*] -> * -> *) t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn t,
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsPred p fn,
 IsProd (SimpleRep a), HasSpec fn a) =>
Term fn t
-> FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> Pred fn
forAll' Term RoseFn (Tree Int)
t forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  Int
a Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  [Tree Int]
cs ->
      [ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  Int
a forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  Int
0
      , forall a (fn :: [*] -> * -> *).
HasSpec fn [a] =>
Term fn [a] -> Term fn Integer
length_ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  [Tree Int]
cs forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  Integer
4
      ]
  , forall (fn :: [*] -> * -> *) t.
HasGenHint fn t =>
Hint t -> Term fn t -> Pred fn
genHint (forall a. a -> Maybe a
Just Integer
2, Integer
30) Term RoseFn (Tree Int)
t
  ]

noSameChildrenTree :: Specification RoseFn (Tree Int)
noSameChildrenTree :: Specification RoseFn (Tree Int)
noSameChildrenTree = forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term RoseFn (Tree Int)
t ->
  [ forall (fn :: [*] -> * -> *) t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn t,
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsPred p fn,
 IsProd (SimpleRep a), HasSpec fn a) =>
Term fn t
-> FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> Pred fn
forAll' Term RoseFn (Tree Int)
t forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  Int
a Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  [Tree Int]
cs ->
      [ forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  Int
a forall a (fn :: [*] -> * -> *).
HasSpec fn a =>
Term fn a -> Term fn [a] -> Term fn Bool
`elem_` forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit [Int
1 .. Int
8]
      , forall t a (fn :: [*] -> * -> *) p.
(Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) =>
Term fn t -> (Term fn a -> p) -> Pred fn
forAll Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  [Tree Int]
cs forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  (Tree Int)
t' ->
          forall (fn :: [*] -> * -> *) t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn t,
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsPred p fn,
 IsProd (SimpleRep a), HasSpec fn a) =>
Term fn t
-> FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> Pred fn
forAll' Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  (Tree Int)
t' forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  Int
b Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  [Tree Int]
_ ->
            Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  Int
b forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
/=. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  Int
a
      ]
  , forall (fn :: [*] -> * -> *) t.
HasGenHint fn t =>
Hint t -> Term fn t -> Pred fn
genHint (forall a. a -> Maybe a
Just Integer
2, Integer
30) Term RoseFn (Tree Int)
t
  ]

successiveChildren :: Specification RoseFn (Tree Int)
successiveChildren :: Specification RoseFn (Tree Int)
successiveChildren = forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term RoseFn (Tree Int)
t ->
  [ forall (fn :: [*] -> * -> *) t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn t,
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsPred p fn,
 IsProd (SimpleRep a), HasSpec fn a) =>
Term fn t
-> FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> Pred fn
forAll' Term RoseFn (Tree Int)
t forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  Int
a Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  [Tree Int]
cs ->
      [ forall t a (fn :: [*] -> * -> *) p.
(Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) =>
Term fn t -> (Term fn a -> p) -> Pred fn
forAll Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  [Tree Int]
cs forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  (Tree Int)
t' ->
          forall (fn :: [*] -> * -> *) a.
(Member (TreeFn fn) fn, HasSpec fn a) =>
Term fn (Tree a) -> Term fn a
rootLabel_ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  (Tree Int)
t' forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  Int
a forall a. Num a => a -> a -> a
+ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  Int
1
      ]
  , forall (fn :: [*] -> * -> *) t.
HasGenHint fn t =>
Hint t -> Term fn t -> Pred fn
genHint (forall a. a -> Maybe a
Just Integer
2, Integer
10) Term RoseFn (Tree Int)
t
  ]

successiveChildren8 :: Specification RoseFn (Tree Int)
successiveChildren8 :: Specification RoseFn (Tree Int)
successiveChildren8 = forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term RoseFn (Tree Int)
t ->
  [ Term RoseFn (Tree Int)
t forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
`satisfies` Specification RoseFn (Tree Int)
successiveChildren
  , forall (fn :: [*] -> * -> *) t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn t,
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsPred p fn,
 IsProd (SimpleRep a), HasSpec fn a) =>
Term fn t
-> FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> Pred fn
forAll' Term RoseFn (Tree Int)
t forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  Int
a Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  [Tree Int]
_ -> Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  Int
a forall a (fn :: [*] -> * -> *).
HasSpec fn a =>
Term fn a -> Term fn [a] -> Term fn Bool
`elem_` forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit [Int
1 .. Int
5]
  ]

roseTreeList :: Specification RoseFn [Tree Int]
roseTreeList :: Specification RoseFn [Tree Int]
roseTreeList = forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term RoseFn [Tree Int]
ts ->
  [ forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *).
HasSpec fn [a] =>
Term fn [a] -> Term fn Integer
length_ Term RoseFn [Tree Int]
ts forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  Integer
10
  , forall t a (fn :: [*] -> * -> *) p.
(Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) =>
Term fn t -> (Term fn a -> p) -> Pred fn
forAll Term RoseFn [Tree Int]
ts forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  (Tree Int)
t ->
      [ forall t a (fn :: [*] -> * -> *) p.
(Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) =>
Term fn t -> (Term fn a -> p) -> Pred fn
forAll Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  (Tree Int)
t forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  (Int, [Tree Int])
_ -> Bool
False
      ]
  ]

roseTreePairs :: Specification RoseFn (Tree ([Int], [Int]))
roseTreePairs :: Specification RoseFn (Tree ([Int], [Int]))
roseTreePairs = forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term RoseFn (Tree ([Int], [Int]))
t ->
  [ forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
(Member (TreeFn fn) fn, HasSpec fn a) =>
Term fn (Tree a) -> Term fn a
rootLabel_ Term RoseFn (Tree ([Int], [Int]))
t forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit ([Int
1 .. Int
10], [Int
1 .. Int
10])
  , forall (fn :: [*] -> * -> *) t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn t,
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsPred p fn,
 IsProd (SimpleRep a), HasSpec fn a) =>
Term fn t
-> FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> Pred fn
forAll' Term RoseFn (Tree ([Int], [Int]))
t forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  ([Int], [Int])
p Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  [Tree ([Int], [Int])]
ts ->
      forall t a (fn :: [*] -> * -> *) p.
(Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) =>
Term fn t -> (Term fn a -> p) -> Pred fn
forAll Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  [Tree ([Int], [Int])]
ts forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  (Tree ([Int], [Int]))
t' ->
        forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn (a, b) -> Term fn a
fst_ (forall (fn :: [*] -> * -> *) a.
(Member (TreeFn fn) fn, HasSpec fn a) =>
Term fn (Tree a) -> Term fn a
rootLabel_ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  (Tree ([Int], [Int]))
t') forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn (a, b) -> Term fn b
snd_ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  ([Int], [Int])
p
  , forall (fn :: [*] -> * -> *) t.
HasGenHint fn t =>
Hint t -> Term fn t -> Pred fn
genHint (forall a. Maybe a
Nothing, Integer
10) Term RoseFn (Tree ([Int], [Int]))
t
  ]

roseTreeMaybe :: Specification RoseFn (Tree (Maybe (Int, Int)))
roseTreeMaybe :: Specification RoseFn (Tree (Maybe (Int, Int)))
roseTreeMaybe = forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term RoseFn (Tree (Maybe (Int, Int)))
t ->
  [ forall (fn :: [*] -> * -> *) t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn t,
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsPred p fn,
 IsProd (SimpleRep a), HasSpec fn a) =>
Term fn t
-> FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> Pred fn
forAll' Term RoseFn (Tree (Maybe (Int, Int)))
t forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  (Maybe (Int, Int))
mp Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  [Tree (Maybe (Int, Int))]
ts ->
      forall t a (fn :: [*] -> * -> *) p.
(Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) =>
Term fn t -> (Term fn a -> p) -> Pred fn
forAll Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  [Tree (Maybe (Int, Int))]
ts forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  (Tree (Maybe (Int, Int)))
t' ->
        forall (fn :: [*] -> * -> *) a p.
(BaseUniverse fn, HasSpec fn a, IsNormalType a, IsPred p fn) =>
Term fn (Maybe a) -> (Term fn a -> p) -> Pred fn
onJust Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  (Maybe (Int, Int))
mp forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  (Int, Int)
p ->
          forall (fn :: [*] -> * -> *) a p.
(BaseUniverse fn, HasSpec fn a, IsNormalType a, IsPred p fn) =>
Term fn (Maybe a) -> (Term fn a -> p) -> Pred fn
onJust (forall (fn :: [*] -> * -> *) a.
(Member (TreeFn fn) fn, HasSpec fn a) =>
Term fn (Tree a) -> Term fn a
rootLabel_ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  (Tree (Maybe (Int, Int)))
t') forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  (Int, Int)
p' ->
            forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn (a, b) -> Term fn a
fst_ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  (Int, Int)
p' forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn (a, b) -> Term fn b
snd_ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  (Int, Int)
p
  , forall (fn :: [*] -> * -> *) t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn t,
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsPred p fn,
 IsProd (SimpleRep a), HasSpec fn a) =>
Term fn t
-> FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> Pred fn
forAll' Term RoseFn (Tree (Maybe (Int, Int)))
t forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  (Maybe (Int, Int))
mp Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  [Tree (Maybe (Int, Int))]
_ -> forall (fn :: [*] -> * -> *) a.
(BaseUniverse fn, HasSpec fn a, IsNormalType a) =>
Term fn (Maybe a) -> Pred fn
isJust Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  (Maybe (Int, Int))
mp
  , forall (fn :: [*] -> * -> *) t.
HasGenHint fn t =>
Hint t -> Term fn t -> Pred fn
genHint (forall a. Maybe a
Nothing, Integer
10) Term RoseFn (Tree (Maybe (Int, Int)))
t
  ]

badTreeInteraction :: Specification RoseFn (Tree (Either Int Int))
badTreeInteraction :: Specification RoseFn (Tree (Either Int Int))
badTreeInteraction = forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term RoseFn (Tree (Either Int Int))
t ->
  [ forall (fn :: [*] -> * -> *) t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn t,
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsPred p fn,
 IsProd (SimpleRep a), HasSpec fn a) =>
Term fn t
-> FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> Pred fn
forAll' Term RoseFn (Tree (Either Int Int))
t forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  (Either Int Int)
n Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  [Tree (Either Int Int)]
ts' ->
      [ forall (c :: Symbol) a (fn :: [*] -> * -> *).
(IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a),
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a,
 HasSpec fn a, HasSpec fn (SimpleRep a),
 SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a,
 All (HasSpec fn) (Cases (SOP (TheSop a))),
 HasSpec fn (ProdOver (ConstrOf c (TheSop a)))) =>
Term fn a -> Pred fn
isCon @"Right" Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  (Either Int Int)
n
      , forall t a (fn :: [*] -> * -> *) p.
(Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) =>
Term fn t -> (Term fn a -> p) -> Pred fn
forAll Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  [Tree (Either Int Int)]
ts' forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  (Tree (Either Int Int))
_ -> Bool
True
      ]
  , forall (fn :: [*] -> * -> *) t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn t,
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsPred p fn,
 IsProd (SimpleRep a), HasSpec fn a) =>
Term fn t
-> FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> Pred fn
forAll' Term RoseFn (Tree (Either Int Int))
t forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  (Either Int Int)
n Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  [Tree (Either Int Int)]
ts' ->
      forall t a (fn :: [*] -> * -> *) p.
(Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) =>
Term fn t -> (Term fn a -> p) -> Pred fn
forAll Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  [Tree (Either Int Int)]
ts' forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  (Tree (Either Int Int))
t' ->
        [ forall (fn :: [*] -> * -> *) t.
HasGenHint fn t =>
Hint t -> Term fn t -> Pred fn
genHint (forall a. a -> Maybe a
Just Integer
4, Integer
10) Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  (Tree (Either Int Int))
t'
        , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
(Member (TreeFn fn) fn, HasSpec fn a) =>
Term fn (Tree a) -> Term fn a
rootLabel_ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  (Tree (Either Int Int))
t' forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))
        (Oneof
           (Oneof FunFn (Oneof SetFn OrdFn))
           (Oneof (Oneof PairFn ListFn) (Oneof TreeFn MapFn)))))
  (Either Int Int)
n
        ]
  , forall (fn :: [*] -> * -> *) t.
HasGenHint fn t =>
Hint t -> Term fn t -> Pred fn
genHint (forall a. a -> Maybe a
Just Integer
4, Integer
10) Term RoseFn (Tree (Either Int Int))
t
  ]