{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Constrained.Spec.Tree (BinTree (..), TreeW (..), rootLabel_, TreeSpec (..)) where
import Constrained.Base (
Binder (..),
Forallable (..),
HOLE (..),
HasGenHint (..),
HasSpec (..),
Logic (..),
Pred (..),
Semantics (..),
Specification (..),
Syntax (..),
Term (..),
appTerm,
constrained,
errorLikeMessage,
explainSpec,
isErrorLike,
typeSpec,
pattern Unary,
)
import Constrained.Conformance (
conformsToSpec,
satisfies,
)
import Constrained.Core (
unionWithMaybe,
)
import Constrained.GenT (
oneofT,
)
import Constrained.List (
List (..),
)
import Constrained.Spec.SumProd (
match,
)
import Constrained.Syntax (
forAll,
genHint,
)
import Constrained.TheKnot (
FoldSpec (..),
ListSpec (..),
PairSpec (..),
genFromSpecT,
shrinkWithSpec,
)
import Data.Kind
import Data.Tree
import GHC.Generics
import Test.QuickCheck (shrinkList)
data BinTree a
= BinTip
| BinNode (BinTree a) a (BinTree a)
deriving (BinTree a -> BinTree a -> Bool
BinTree a -> BinTree a -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {a}. Ord a => Eq (BinTree a)
forall a. Ord a => BinTree a -> BinTree a -> Bool
forall a. Ord a => BinTree a -> BinTree a -> Ordering
forall a. Ord a => BinTree a -> BinTree a -> BinTree a
min :: BinTree a -> BinTree a -> BinTree a
$cmin :: forall a. Ord a => BinTree a -> BinTree a -> BinTree a
max :: BinTree a -> BinTree a -> BinTree a
$cmax :: forall a. Ord a => BinTree a -> BinTree a -> BinTree a
>= :: BinTree a -> BinTree a -> Bool
$c>= :: forall a. Ord a => BinTree a -> BinTree a -> Bool
> :: BinTree a -> BinTree a -> Bool
$c> :: forall a. Ord a => BinTree a -> BinTree a -> Bool
<= :: BinTree a -> BinTree a -> Bool
$c<= :: forall a. Ord a => BinTree a -> BinTree a -> Bool
< :: BinTree a -> BinTree a -> Bool
$c< :: forall a. Ord a => BinTree a -> BinTree a -> Bool
compare :: BinTree a -> BinTree a -> Ordering
$ccompare :: forall a. Ord a => BinTree a -> BinTree a -> Ordering
Ord, BinTree a -> BinTree a -> Bool
forall a. Eq a => BinTree a -> BinTree a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: BinTree a -> BinTree a -> Bool
$c/= :: forall a. Eq a => BinTree a -> BinTree a -> Bool
== :: BinTree a -> BinTree a -> Bool
$c== :: forall a. Eq a => BinTree a -> BinTree a -> Bool
Eq, Int -> BinTree a -> ShowS
forall a. Show a => Int -> BinTree a -> ShowS
forall a. Show a => [BinTree a] -> ShowS
forall a. Show a => BinTree a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [BinTree a] -> ShowS
$cshowList :: forall a. Show a => [BinTree a] -> ShowS
show :: BinTree a -> String
$cshow :: forall a. Show a => BinTree a -> String
showsPrec :: Int -> BinTree a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> BinTree a -> ShowS
Show, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (BinTree a) x -> BinTree a
forall a x. BinTree a -> Rep (BinTree a) x
$cto :: forall a x. Rep (BinTree a) x -> BinTree a
$cfrom :: forall a x. BinTree a -> Rep (BinTree a) x
Generic)
data BinTreeSpec a = BinTreeSpec (Maybe Integer) (Specification (BinTree a, a, BinTree a))
deriving (Int -> BinTreeSpec a -> ShowS
forall a. HasSpec a => Int -> BinTreeSpec a -> ShowS
forall a. HasSpec a => [BinTreeSpec a] -> ShowS
forall a. HasSpec a => BinTreeSpec a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [BinTreeSpec a] -> ShowS
$cshowList :: forall a. HasSpec a => [BinTreeSpec a] -> ShowS
show :: BinTreeSpec a -> String
$cshow :: forall a. HasSpec a => BinTreeSpec a -> String
showsPrec :: Int -> BinTreeSpec a -> ShowS
$cshowsPrec :: forall a. HasSpec a => Int -> BinTreeSpec a -> ShowS
Show)
instance Forallable (BinTree a) (BinTree a, a, BinTree a) where
fromForAllSpec :: (HasSpec (BinTree a), HasSpec (BinTree a, a, BinTree a)) =>
Specification (BinTree a, a, BinTree a)
-> Specification (BinTree a)
fromForAllSpec = forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
Maybe Integer
-> Specification (BinTree a, a, BinTree a) -> BinTreeSpec a
BinTreeSpec forall a. Maybe a
Nothing
forAllToList :: BinTree a -> [(BinTree a, a, BinTree a)]
forAllToList BinTree a
BinTip = []
forAllToList (BinNode BinTree a
left a
a BinTree a
right) = (BinTree a
left, a
a, BinTree a
right) forall a. a -> [a] -> [a]
: forall t e. Forallable t e => t -> [e]
forAllToList BinTree a
left forall a. [a] -> [a] -> [a]
++ forall t e. Forallable t e => t -> [e]
forAllToList BinTree a
right
instance HasSpec a => HasSpec (BinTree a) where
type TypeSpec (BinTree a) = BinTreeSpec a
emptySpec :: TypeSpec (BinTree a)
emptySpec = forall a.
Maybe Integer
-> Specification (BinTree a, a, BinTree a) -> BinTreeSpec a
BinTreeSpec forall a. Maybe a
Nothing forall a. Specification a
TrueSpec
combineSpec :: TypeSpec (BinTree a)
-> TypeSpec (BinTree a) -> Specification (BinTree a)
combineSpec (BinTreeSpec Maybe Integer
sz Specification (BinTree a, a, BinTree a)
s) (BinTreeSpec Maybe Integer
sz' Specification (BinTree a, a, BinTree a)
s') =
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec forall a b. (a -> b) -> a -> b
$ forall a.
Maybe Integer
-> Specification (BinTree a, a, BinTree a) -> BinTreeSpec a
BinTreeSpec (forall a. (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a
unionWithMaybe forall a. Ord a => a -> a -> a
min Maybe Integer
sz Maybe Integer
sz') (Specification (BinTree a, a, BinTree a)
s forall a. Semigroup a => a -> a -> a
<> Specification (BinTree a, a, BinTree a)
s')
conformsTo :: HasCallStack => BinTree a -> TypeSpec (BinTree a) -> Bool
conformsTo BinTree a
BinTip TypeSpec (BinTree a)
_ = Bool
True
conformsTo (BinNode BinTree a
left a
a BinTree a
right) s :: TypeSpec (BinTree a)
s@(BinTreeSpec Maybe Integer
_ Specification (BinTree a, a, BinTree a)
es) =
forall (t :: * -> *). Foldable t => t Bool -> Bool
and
[ (BinTree a
left, a
a, BinTree a
right) forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification (BinTree a, a, BinTree a)
es
, BinTree a
left forall a. (HasSpec a, HasCallStack) => a -> TypeSpec a -> Bool
`conformsTo` TypeSpec (BinTree a)
s
, BinTree a
right forall a. (HasSpec a, HasCallStack) => a -> TypeSpec a -> Bool
`conformsTo` TypeSpec (BinTree a)
s
]
genFromTypeSpec :: forall (m :: * -> *).
(HasCallStack, MonadGenError m) =>
TypeSpec (BinTree a) -> GenT m (BinTree a)
genFromTypeSpec (BinTreeSpec Maybe Integer
msz Specification (BinTree a, a, BinTree a)
s)
| Just Integer
sz <- Maybe Integer
msz, Integer
sz forall a. Ord a => a -> a -> Bool
<= Integer
0 = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. BinTree a
BinTip
| Bool
otherwise = do
let sz :: Integer
sz = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Integer
20 forall a. a -> a
id Maybe Integer
msz
sz' :: Integer
sz' = Integer
sz forall a. Integral a => a -> a -> a
`div` Integer
2
forall a (m :: * -> *).
(Typeable a, MonadGenError m) =>
[GenT GE a] -> GenT m a
oneofT
[ do
(BinTree a
left, a
a, BinTree a
right) <- forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecT @(BinTree a, a, BinTree a) forall a b. (a -> b) -> a -> b
$
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (BinTree a, a, BinTree a)
ctx ->
[ forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (BinTree a, a, BinTree a)
ctx forall a b. (a -> b) -> a -> b
$ \Term (BinTree a)
left Term a
_ Term (BinTree a)
right ->
[ forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (BinTree a)
left (forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification (BinTree a, a, BinTree a)
s)
, forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint Integer
sz' Term (BinTree a)
left
, forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (BinTree a)
right (forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification (BinTree a, a, BinTree a)
s)
, forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint Integer
sz' Term (BinTree a)
right
]
, Term (BinTree a, a, BinTree a)
ctx forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification (BinTree a, a, BinTree a)
s
]
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. BinTree a -> a -> BinTree a -> BinTree a
BinNode BinTree a
left a
a BinTree a
right
, forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. BinTree a
BinTip
]
shrinkWithTypeSpec :: TypeSpec (BinTree a) -> BinTree a -> [BinTree a]
shrinkWithTypeSpec TypeSpec (BinTree a)
_ BinTree a
BinTip = []
shrinkWithTypeSpec TypeSpec (BinTree a)
s (BinNode BinTree a
left a
a BinTree a
right) =
forall a. BinTree a
BinTip
forall a. a -> [a] -> [a]
: BinTree a
left
forall a. a -> [a] -> [a]
: BinTree a
right
forall a. a -> [a] -> [a]
: (forall a. BinTree a -> a -> BinTree a -> BinTree a
BinNode BinTree a
left a
a forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. HasSpec a => TypeSpec a -> a -> [a]
shrinkWithTypeSpec TypeSpec (BinTree a)
s BinTree a
right)
forall a. [a] -> [a] -> [a]
++ ((\BinTree a
l -> forall a. BinTree a -> a -> BinTree a -> BinTree a
BinNode BinTree a
l a
a BinTree a
right) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. HasSpec a => TypeSpec a -> a -> [a]
shrinkWithTypeSpec TypeSpec (BinTree a)
s BinTree a
left)
cardinalTypeSpec :: TypeSpec (BinTree a) -> Specification Integer
cardinalTypeSpec TypeSpec (BinTree a)
_ = forall a. Specification a
TrueSpec
toPreds :: Term (BinTree a) -> TypeSpec (BinTree a) -> Pred
toPreds Term (BinTree a)
t (BinTreeSpec Maybe Integer
msz Specification (BinTree a, a, BinTree a)
s) =
(forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (BinTree a)
t forall a b. (a -> b) -> a -> b
$ \Term (BinTree a, a, BinTree a)
n -> Term (BinTree a, a, BinTree a)
n forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification (BinTree a, a, BinTree a)
s)
forall a. Semigroup a => a -> a -> a
<> forall b a. b -> (a -> b) -> Maybe a -> b
maybe Pred
TruePred (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint Term (BinTree a)
t) Maybe Integer
msz
instance HasSpec a => HasGenHint (BinTree a) where
type Hint (BinTree a) = Integer
giveHint :: Hint (BinTree a) -> Specification (BinTree a)
giveHint Hint (BinTree a)
h = forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec forall a b. (a -> b) -> a -> b
$ forall a.
Maybe Integer
-> Specification (BinTree a, a, BinTree a) -> BinTreeSpec a
BinTreeSpec (forall a. a -> Maybe a
Just Hint (BinTree a)
h) forall a. Specification a
TrueSpec
data TreeSpec a = TreeSpec
{ forall a. TreeSpec a -> Maybe Integer
roseTreeAvgLength :: Maybe Integer
, forall a. TreeSpec a -> Maybe Integer
roseTreeMaxSize :: Maybe Integer
, forall a. TreeSpec a -> Specification a
roseTreeRootSpec :: Specification a
, forall a. TreeSpec a -> Specification (a, [Tree a])
roseTreeCtxSpec :: Specification (a, [Tree a])
}
deriving instance HasSpec a => Show (TreeSpec a)
instance Forallable (Tree a) (a, [Tree a]) where
fromForAllSpec :: (HasSpec (Tree a), HasSpec (a, [Tree a])) =>
Specification (a, [Tree a]) -> Specification (Tree a)
fromForAllSpec = forall a. HasSpec (Tree a) => TreeSpec a -> Specification (Tree a)
guardRoseSpec forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
Maybe Integer
-> Maybe Integer
-> Specification a
-> Specification (a, [Tree a])
-> TreeSpec a
TreeSpec forall a. Maybe a
Nothing forall a. Maybe a
Nothing forall a. Specification a
TrueSpec
forAllToList :: Tree a -> [(a, [Tree a])]
forAllToList (Node a
a [Tree a]
children) = (a
a, [Tree a]
children) forall a. a -> [a] -> [a]
: forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall t e. Forallable t e => t -> [e]
forAllToList [Tree a]
children
guardRoseSpec :: HasSpec (Tree a) => TreeSpec a -> Specification (Tree a)
guardRoseSpec :: forall a. HasSpec (Tree a) => TreeSpec a -> Specification (Tree a)
guardRoseSpec spec :: TreeSpec a
spec@(TreeSpec Maybe Integer
_ Maybe Integer
_ Specification a
rs Specification (a, [Tree a])
s)
| forall a. Specification a -> Bool
isErrorLike Specification a
rs = forall a. NonEmpty String -> Specification a
ErrorSpec (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"guardRoseSpec: rootSpec is error")
| forall a. Specification a -> Bool
isErrorLike Specification (a, [Tree a])
s = forall a. NonEmpty String -> Specification a
ErrorSpec (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"guardRoseSpec: ctxSpec is error")
| Bool
otherwise = forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
TypeSpec TreeSpec a
spec []
instance HasSpec a => HasSpec (Tree a) where
type TypeSpec (Tree a) = TreeSpec a
emptySpec :: TypeSpec (Tree a)
emptySpec = forall a.
Maybe Integer
-> Maybe Integer
-> Specification a
-> Specification (a, [Tree a])
-> TreeSpec a
TreeSpec forall a. Maybe a
Nothing forall a. Maybe a
Nothing forall a. Specification a
TrueSpec forall a. Specification a
TrueSpec
combineSpec :: TypeSpec (Tree a) -> TypeSpec (Tree a) -> Specification (Tree a)
combineSpec (TreeSpec Maybe Integer
mal Maybe Integer
sz Specification a
rs Specification (a, [Tree a])
s) (TreeSpec Maybe Integer
mal' Maybe Integer
sz' Specification a
rs' Specification (a, [Tree a])
s')
| forall a. Specification a -> Bool
isErrorLike Specification (a, [Tree a])
alteredspec = forall a. NonEmpty String -> Specification a
ErrorSpec (forall a. Specification a -> NonEmpty String
errorLikeMessage Specification (a, [Tree a])
alteredspec)
| Bool
otherwise =
forall a. HasSpec (Tree a) => TreeSpec a -> Specification (Tree a)
guardRoseSpec forall a b. (a -> b) -> a -> b
$
forall a.
Maybe Integer
-> Maybe Integer
-> Specification a
-> Specification (a, [Tree a])
-> TreeSpec a
TreeSpec
(forall a. (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a
unionWithMaybe forall a. Ord a => a -> a -> a
max Maybe Integer
mal Maybe Integer
mal')
(forall a. (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a
unionWithMaybe forall a. Ord a => a -> a -> a
min Maybe Integer
sz Maybe Integer
sz')
Specification a
rs''
Specification (a, [Tree a])
s''
where
alteredspec :: Specification (a, [Tree a])
alteredspec = (forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (forall a b. Specification a -> Specification b -> PairSpec a b
Cartesian Specification a
rs'' forall a. Specification a
TrueSpec) forall a. Semigroup a => a -> a -> a
<> Specification (a, [Tree a])
s'')
rs'' :: Specification a
rs'' = Specification a
rs forall a. Semigroup a => a -> a -> a
<> Specification a
rs'
s'' :: Specification (a, [Tree a])
s'' = Specification (a, [Tree a])
s forall a. Semigroup a => a -> a -> a
<> Specification (a, [Tree a])
s'
conformsTo :: HasCallStack => Tree a -> TypeSpec (Tree a) -> Bool
conformsTo (Node a
a [Tree a]
children) (TreeSpec Maybe Integer
_ Maybe Integer
_ Specification a
rs Specification (a, [Tree a])
s) =
forall (t :: * -> *). Foldable t => t Bool -> Bool
and
[ (a
a, [Tree a]
children) forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification (a, [Tree a])
s
, forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\(Node a
a' [Tree a]
children') -> (a
a', [Tree a]
children') forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification (a, [Tree a])
s) [Tree a]
children
, a
a forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
rs
]
genFromTypeSpec :: forall (m :: * -> *).
(HasCallStack, MonadGenError m) =>
TypeSpec (Tree a) -> GenT m (Tree a)
genFromTypeSpec (TreeSpec Maybe Integer
mal Maybe Integer
msz Specification a
rs Specification (a, [Tree a])
s) = do
let sz :: Integer
sz = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Integer
20 forall a. a -> a
id Maybe Integer
msz
sz' :: Integer
sz' = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Integer
sz forall a. Integral a => a -> a -> a
`div` Integer
4) (Integer
sz forall a. Integral a => a -> a -> a
`div`) Maybe Integer
mal
childrenSpec :: Specification [Tree a]
childrenSpec =
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec forall a b. (a -> b) -> a -> b
$
forall a.
Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
ListSpec
(forall a. a -> Maybe a
Just Integer
sz')
[]
forall a. Specification a
TrueSpec
(forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec forall a b. (a -> b) -> a -> b
$ forall a.
Maybe Integer
-> Maybe Integer
-> Specification a
-> Specification (a, [Tree a])
-> TreeSpec a
TreeSpec Maybe Integer
mal (forall a. a -> Maybe a
Just Integer
sz') forall a. Specification a
TrueSpec Specification (a, [Tree a])
s)
forall a. FoldSpec a
NoFold
innerSpec :: Specification (a, [Tree a])
innerSpec = Specification (a, [Tree a])
s forall a. Semigroup a => a -> a -> a
<> forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (forall a b. Specification a -> Specification b -> PairSpec a b
Cartesian Specification a
rs Specification [Tree a]
childrenSpec)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a. a -> [Tree a] -> Tree a
Node) forall a b. (a -> b) -> a -> b
$
forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecT @(a, [Tree a]) Specification (a, [Tree a])
innerSpec
shrinkWithTypeSpec :: TypeSpec (Tree a) -> Tree a -> [Tree a]
shrinkWithTypeSpec (TreeSpec Maybe Integer
_ Maybe Integer
_ Specification a
rs Specification (a, [Tree a])
ctxSpec) (Node a
a [Tree a]
ts) =
[forall a. a -> [Tree a] -> Tree a
Node a
a [] | Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Tree a]
ts]
forall a. [a] -> [a] -> [a]
++ [Tree a]
ts
forall a. [a] -> [a] -> [a]
++ [forall a. a -> [Tree a] -> Tree a
Node a
a' [Tree a]
ts | a
a' <- forall a. HasSpec a => Specification a -> a -> [a]
shrinkWithSpec Specification a
rs a
a]
forall a. [a] -> [a] -> [a]
++ [forall a. a -> [Tree a] -> Tree a
Node a
a [Tree a
t] | Tree a
t <- [Tree a]
ts]
forall a. [a] -> [a] -> [a]
++ [ forall a. a -> [Tree a] -> Tree a
Node a
a [Tree a]
ts'
| [Tree a]
ts' <- forall a. (a -> [a]) -> [a] -> [[a]]
shrinkList (forall a. HasSpec a => TypeSpec a -> a -> [a]
shrinkWithTypeSpec (forall a.
Maybe Integer
-> Maybe Integer
-> Specification a
-> Specification (a, [Tree a])
-> TreeSpec a
TreeSpec forall a. Maybe a
Nothing forall a. Maybe a
Nothing forall a. Specification a
TrueSpec Specification (a, [Tree a])
ctxSpec)) [Tree a]
ts
]
cardinalTypeSpec :: TypeSpec (Tree a) -> Specification Integer
cardinalTypeSpec TypeSpec (Tree a)
_ = forall a. Specification a
TrueSpec
toPreds :: Term (Tree a) -> TypeSpec (Tree a) -> Pred
toPreds Term (Tree a)
t (TreeSpec Maybe Integer
mal Maybe Integer
msz Specification a
rs Specification (a, [Tree a])
s) =
(forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Tree a)
t forall a b. (a -> b) -> a -> b
$ \Term (a, [Tree a])
n -> Term (a, [Tree a])
n forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification (a, [Tree a])
s)
forall a. Semigroup a => a -> a -> a
<> forall a. HasSpec a => Term (Tree a) -> Term a
rootLabel_ Term (Tree a)
t
forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification a
rs
forall a. Semigroup a => a -> a -> a
<> forall b a. b -> (a -> b) -> Maybe a -> b
maybe Pred
TruePred (\Integer
sz -> forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint (Maybe Integer
mal, Integer
sz) Term (Tree a)
t) Maybe Integer
msz
instance HasSpec a => HasGenHint (Tree a) where
type Hint (Tree a) = (Maybe Integer, Integer)
giveHint :: Hint (Tree a) -> Specification (Tree a)
giveHint (Maybe Integer
avgLen, Integer
sz) = forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec forall a b. (a -> b) -> a -> b
$ forall a.
Maybe Integer
-> Maybe Integer
-> Specification a
-> Specification (a, [Tree a])
-> TreeSpec a
TreeSpec Maybe Integer
avgLen (forall a. a -> Maybe a
Just Integer
sz) forall a. Specification a
TrueSpec forall a. Specification a
TrueSpec
data TreeW (dom :: [Type]) (rng :: Type) where
RootLabelW :: HasSpec a => TreeW '[Tree a] a
deriving instance Eq (TreeW d r)
deriving instance Show (TreeW d r)
instance Semantics TreeW where
semantics :: forall (d :: [*]) r. TreeW d r -> FunTy d r
semantics TreeW d r
RootLabelW = \(Node r
a [Tree r]
_) -> r
a
instance Syntax TreeW where
inFix :: forall (dom :: [*]) rng. TreeW dom rng -> Bool
inFix TreeW dom rng
_ = Bool
False
instance Logic TreeW where
propagate :: forall (as :: [*]) b a.
(AppRequires TreeW as b, HasSpec a) =>
TreeW as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
propagate TreeW as b
f ListCtx Value as (HOLE a)
ctxt (ExplainSpec [String]
es Specification b
s) = forall a. [String] -> Specification a -> Specification a
explainSpec [String]
es forall a b. (a -> b) -> a -> b
$ forall (t :: [*] -> * -> *) (as :: [*]) b a.
(Logic t, AppRequires t as b, HasSpec a) =>
t as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
propagate TreeW as b
f ListCtx Value as (HOLE a)
ctxt Specification b
s
propagate TreeW as b
_ ListCtx Value as (HOLE a)
_ Specification b
TrueSpec = forall a. Specification a
TrueSpec
propagate TreeW as b
_ ListCtx Value as (HOLE a)
_ (ErrorSpec NonEmpty String
msgs) = forall a. NonEmpty String -> Specification a
ErrorSpec NonEmpty String
msgs
propagate TreeW as b
RootLabelW (Unary HOLE a (Tree b)
HOLE) (SuspendedSpec Var b
v Pred
ps) = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term a
v' -> forall a. Term a -> Binder a -> Pred
Let (forall (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequires t dom a =>
t dom a -> List Term dom -> Term a
App forall a. HasSpec a => TreeW '[Tree a] a
RootLabelW (Term a
v' forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall {k} (f :: k -> *). List f '[]
Nil)) (Var b
v forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred
ps)
propagate TreeW as b
RootLabelW (Unary HOLE a (Tree b)
HOLE) Specification b
spec = forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec forall a b. (a -> b) -> a -> b
$ forall a.
Maybe Integer
-> Maybe Integer
-> Specification a
-> Specification (a, [Tree a])
-> TreeSpec a
TreeSpec forall a. Maybe a
Nothing forall a. Maybe a
Nothing Specification b
spec forall a. Specification a
TrueSpec
mapTypeSpec :: forall a b.
(HasSpec a, HasSpec b) =>
TreeW '[a] b -> TypeSpec a -> Specification b
mapTypeSpec TreeW '[a] b
RootLabelW (TreeSpec Maybe Integer
_ Maybe Integer
_ Specification b
rs Specification (b, [Tree b])
_) = Specification b
rs
rootLabel_ ::
forall a.
HasSpec a =>
Term (Tree a) ->
Term a
rootLabel_ :: forall a. HasSpec a => Term (Tree a) -> Term a
rootLabel_ = forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm forall a. HasSpec a => TreeW '[Tree a] a
RootLabelW