{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}

module Constrained.Spec.Tree (BinTree (..), TreeFn, rootLabel_, TreeSpec (..)) where

import Data.Kind
import Data.Tree
import GHC.Generics
import Test.QuickCheck (shrinkList)

import Constrained.Base
import Constrained.Core
import Constrained.GenT
import Constrained.List
import Constrained.Spec.Generics
import Constrained.Spec.Pairs
import Constrained.Univ

------------------------------------------------------------------------
-- The types
------------------------------------------------------------------------

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)

------------------------------------------------------------------------
-- HasSpec for BinTree
------------------------------------------------------------------------

data BinTreeSpec fn a = BinTreeSpec (Maybe Integer) (Specification fn (BinTree a, a, BinTree a))
  deriving (Int -> BinTreeSpec fn a -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Int -> BinTreeSpec fn a -> ShowS
forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
[BinTreeSpec fn a] -> ShowS
forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
BinTreeSpec fn a -> String
showList :: [BinTreeSpec fn a] -> ShowS
$cshowList :: forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
[BinTreeSpec fn a] -> ShowS
show :: BinTreeSpec fn a -> String
$cshow :: forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
BinTreeSpec fn a -> String
showsPrec :: Int -> BinTreeSpec fn a -> ShowS
$cshowsPrec :: forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Int -> BinTreeSpec fn a -> ShowS
Show)

instance Forallable (BinTree a) (BinTree a, a, BinTree a) where
  fromForAllSpec :: forall (fn :: [*] -> * -> *).
(HasSpec fn (BinTree a), HasSpec fn (BinTree a, a, BinTree a),
 BaseUniverse fn) =>
Specification fn (BinTree a, a, BinTree a)
-> Specification fn (BinTree a)
fromForAllSpec = forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> Specification fn a
typeSpec forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (fn :: [*] -> * -> *) a.
Maybe Integer
-> Specification fn (BinTree a, a, BinTree a) -> BinTreeSpec fn 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 fn a => HasSpec fn (BinTree a) where
  type TypeSpec fn (BinTree a) = BinTreeSpec fn a

  emptySpec :: TypeSpec fn (BinTree a)
emptySpec = forall (fn :: [*] -> * -> *) a.
Maybe Integer
-> Specification fn (BinTree a, a, BinTree a) -> BinTreeSpec fn a
BinTreeSpec forall a. Maybe a
Nothing forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec

  combineSpec :: TypeSpec fn (BinTree a)
-> TypeSpec fn (BinTree a) -> Specification fn (BinTree a)
combineSpec (BinTreeSpec Maybe Integer
sz Specification fn (BinTree a, a, BinTree a)
s) (BinTreeSpec Maybe Integer
sz' Specification fn (BinTree a, a, BinTree a)
s') =
    forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> Specification fn a
typeSpec forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
Maybe Integer
-> Specification fn (BinTree a, a, BinTree a) -> BinTreeSpec fn 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 fn (BinTree a, a, BinTree a)
s forall a. Semigroup a => a -> a -> a
<> Specification fn (BinTree a, a, BinTree a)
s')

  conformsTo :: HasCallStack => BinTree a -> TypeSpec fn (BinTree a) -> Bool
conformsTo BinTree a
BinTip TypeSpec fn (BinTree a)
_ = Bool
True
  conformsTo (BinNode BinTree a
left a
a BinTree a
right) s :: TypeSpec fn (BinTree a)
s@(BinTreeSpec Maybe Integer
_ Specification fn (BinTree a, a, BinTree a)
es) =
    forall (t :: * -> *). Foldable t => t Bool -> Bool
and
      [ (BinTree a
left, a
a, BinTree a
right) forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
a -> Specification fn a -> Bool
`conformsToSpec` Specification fn (BinTree a, a, BinTree a)
es
      , BinTree a
left forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, HasCallStack) =>
a -> TypeSpec fn a -> Bool
`conformsTo` TypeSpec fn (BinTree a)
s
      , BinTree a
right forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, HasCallStack) =>
a -> TypeSpec fn a -> Bool
`conformsTo` TypeSpec fn (BinTree a)
s
      ]

  genFromTypeSpec :: forall (m :: * -> *).
(HasCallStack, MonadGenError m) =>
TypeSpec fn (BinTree a) -> GenT m (BinTree a)
genFromTypeSpec (BinTreeSpec Maybe Integer
msz Specification fn (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 (m :: * -> *) a. MonadGenError m => [GenT GE a] -> GenT m a
oneofT
          [ do
              (BinTree a
left, a
a, BinTree a
right) <- forall (fn :: [*] -> * -> *) a (m :: * -> *).
(HasCallStack, HasSpec fn a, MonadGenError m) =>
Specification fn a -> GenT m a
genFromSpecT @fn @(BinTree a, a, BinTree a) forall a b. (a -> b) -> a -> b
$
                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 fn (BinTree a, a, BinTree a)
ctx ->
                  [ forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (BinTree a, a, BinTree a)
ctx forall a b. (a -> b) -> a -> b
$ \Term fn (BinTree a)
left Term fn a
_ Term fn (BinTree a)
right ->
                      [ 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 fn (BinTree a)
left (forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
`satisfies` Specification fn (BinTree a, a, BinTree a)
s)
                      , forall (fn :: [*] -> * -> *) t.
HasGenHint fn t =>
Hint t -> Term fn t -> Pred fn
genHint Integer
sz' Term fn (BinTree a)
left
                      , 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 fn (BinTree a)
right (forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
`satisfies` Specification fn (BinTree a, a, BinTree a)
s)
                      , forall (fn :: [*] -> * -> *) t.
HasGenHint fn t =>
Hint t -> Term fn t -> Pred fn
genHint Integer
sz' Term fn (BinTree a)
right
                      ]
                  , Term fn (BinTree a, a, BinTree a)
ctx forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
`satisfies` Specification fn (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 fn (BinTree a) -> BinTree a -> [BinTree a]
shrinkWithTypeSpec TypeSpec fn (BinTree a)
_ BinTree a
BinTip = []
  shrinkWithTypeSpec TypeSpec fn (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 (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> a -> [a]
shrinkWithTypeSpec TypeSpec fn (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 (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> a -> [a]
shrinkWithTypeSpec TypeSpec fn (BinTree a)
s BinTree a
left)

  cardinalTypeSpec :: TypeSpec fn (BinTree a) -> Specification fn Integer
cardinalTypeSpec TypeSpec fn (BinTree a)
_ = forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec

  toPreds :: Term fn (BinTree a) -> TypeSpec fn (BinTree a) -> Pred fn
toPreds Term fn (BinTree a)
t (BinTreeSpec Maybe Integer
msz Specification fn (BinTree a, a, BinTree a)
s) =
    (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 fn (BinTree a)
t forall a b. (a -> b) -> a -> b
$ \Term fn (BinTree a, a, BinTree a)
n -> Term fn (BinTree a, a, BinTree a)
n forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
`satisfies` Specification fn (BinTree a, a, BinTree a)
s)
      forall a. Semigroup a => a -> a -> a
<> forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall (fn :: [*] -> * -> *). Pred fn
TruePred (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (fn :: [*] -> * -> *) t.
HasGenHint fn t =>
Hint t -> Term fn t -> Pred fn
genHint Term fn (BinTree a)
t) Maybe Integer
msz

instance HasSpec fn a => HasGenHint fn (BinTree a) where
  type Hint (BinTree a) = Integer
  giveHint :: Hint (BinTree a) -> Specification fn (BinTree a)
giveHint Hint (BinTree a)
h = forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> Specification fn a
typeSpec forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
Maybe Integer
-> Specification fn (BinTree a, a, BinTree a) -> BinTreeSpec fn a
BinTreeSpec (forall a. a -> Maybe a
Just Hint (BinTree a)
h) forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec

------------------------------------------------------------------------
-- HasSpec for Tree
------------------------------------------------------------------------

data TreeSpec fn a = TreeSpec
  { forall (fn :: [*] -> * -> *) a. TreeSpec fn a -> Maybe Integer
roseTreeAvgLength :: Maybe Integer
  , forall (fn :: [*] -> * -> *) a. TreeSpec fn a -> Maybe Integer
roseTreeMaxSize :: Maybe Integer
  , forall (fn :: [*] -> * -> *) a. TreeSpec fn a -> Specification fn a
roseTreeRootSpec :: Specification fn a
  , forall (fn :: [*] -> * -> *) a.
TreeSpec fn a -> Specification fn (a, [Tree a])
roseTreeCtxSpec :: Specification fn (a, [Tree a])
  }

deriving instance (HasSpec fn a, Member (TreeFn fn) fn) => Show (TreeSpec fn a)

instance Forallable (Tree a) (a, [Tree a]) where
  fromForAllSpec :: forall (fn :: [*] -> * -> *).
(HasSpec fn (Tree a), HasSpec fn (a, [Tree a]), BaseUniverse fn) =>
Specification fn (a, [Tree a]) -> Specification fn (Tree a)
fromForAllSpec = forall (fn :: [*] -> * -> *) a.
HasSpec fn (Tree a) =>
TreeSpec fn a -> Specification fn (Tree a)
guardRoseSpec forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (fn :: [*] -> * -> *) a.
Maybe Integer
-> Maybe Integer
-> Specification fn a
-> Specification fn (a, [Tree a])
-> TreeSpec fn a
TreeSpec forall a. Maybe a
Nothing forall a. Maybe a
Nothing forall (fn :: [*] -> * -> *) a. Specification fn 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

-- TODO: get rid of this when we implement `cardinality`
-- in `HasSpec`
guardRoseSpec :: HasSpec fn (Tree a) => TreeSpec fn a -> Specification fn (Tree a)
guardRoseSpec :: forall (fn :: [*] -> * -> *) a.
HasSpec fn (Tree a) =>
TreeSpec fn a -> Specification fn (Tree a)
guardRoseSpec spec :: TreeSpec fn a
spec@(TreeSpec Maybe Integer
_ Maybe Integer
_ Specification fn a
rs Specification fn (a, [Tree a])
s)
  | forall (fn :: [*] -> * -> *) a. Specification fn a -> Bool
isErrorLike Specification fn a
rs = forall (fn :: [*] -> * -> *) a.
NonEmpty String -> Specification fn a
ErrorSpec (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"guardRoseSpec: rootSpec is error")
  | forall (fn :: [*] -> * -> *) a. Specification fn a -> Bool
isErrorLike Specification fn (a, [Tree a])
s = forall (fn :: [*] -> * -> *) a.
NonEmpty String -> Specification fn a
ErrorSpec (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"guardRoseSpec: ctxSpec is error")
  | Bool
otherwise = forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> OrdSet a -> Specification fn a
TypeSpec TreeSpec fn a
spec []

instance (HasSpec fn a, Member (TreeFn fn) fn) => HasSpec fn (Tree a) where
  type TypeSpec fn (Tree a) = TreeSpec fn a

  emptySpec :: TypeSpec fn (Tree a)
emptySpec = forall (fn :: [*] -> * -> *) a.
Maybe Integer
-> Maybe Integer
-> Specification fn a
-> Specification fn (a, [Tree a])
-> TreeSpec fn a
TreeSpec forall a. Maybe a
Nothing forall a. Maybe a
Nothing forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec

  combineSpec :: TypeSpec fn (Tree a)
-> TypeSpec fn (Tree a) -> Specification fn (Tree a)
combineSpec (TreeSpec Maybe Integer
mal Maybe Integer
sz Specification fn a
rs Specification fn (a, [Tree a])
s) (TreeSpec Maybe Integer
mal' Maybe Integer
sz' Specification fn a
rs' Specification fn (a, [Tree a])
s')
    | forall (fn :: [*] -> * -> *) a. Specification fn a -> Bool
isErrorLike Specification fn (a, [Tree a])
alteredspec = forall (fn :: [*] -> * -> *) a.
NonEmpty String -> Specification fn a
ErrorSpec (forall (fn :: [*] -> * -> *) a.
Specification fn a -> NonEmpty String
errorLikeMessage Specification fn (a, [Tree a])
alteredspec)
    | Bool
otherwise =
        forall (fn :: [*] -> * -> *) a.
HasSpec fn (Tree a) =>
TreeSpec fn a -> Specification fn (Tree a)
guardRoseSpec forall a b. (a -> b) -> a -> b
$
          forall (fn :: [*] -> * -> *) a.
Maybe Integer
-> Maybe Integer
-> Specification fn a
-> Specification fn (a, [Tree a])
-> TreeSpec fn 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 fn a
rs''
            Specification fn (a, [Tree a])
s''
    where
      alteredspec :: Specification fn (a, [Tree a])
alteredspec = (forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> Specification fn a
typeSpec (forall (fn :: [*] -> * -> *) a b.
Specification fn a -> Specification fn b -> PairSpec fn a b
Cartesian Specification fn a
rs'' forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec) forall a. Semigroup a => a -> a -> a
<> Specification fn (a, [Tree a])
s'')
      rs'' :: Specification fn a
rs'' = Specification fn a
rs forall a. Semigroup a => a -> a -> a
<> Specification fn a
rs'
      s'' :: Specification fn (a, [Tree a])
s'' = Specification fn (a, [Tree a])
s forall a. Semigroup a => a -> a -> a
<> Specification fn (a, [Tree a])
s'

  conformsTo :: HasCallStack => Tree a -> TypeSpec fn (Tree a) -> Bool
conformsTo (Node a
a [Tree a]
children) (TreeSpec Maybe Integer
_ Maybe Integer
_ Specification fn a
rs Specification fn (a, [Tree a])
s) =
    forall (t :: * -> *). Foldable t => t Bool -> Bool
and
      [ (a
a, [Tree a]
children) forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
a -> Specification fn a -> Bool
`conformsToSpec` Specification fn (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 (fn :: [*] -> * -> *) a.
HasSpec fn a =>
a -> Specification fn a -> Bool
`conformsToSpec` Specification fn (a, [Tree a])
s) [Tree a]
children
      , a
a forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
a -> Specification fn a -> Bool
`conformsToSpec` Specification fn a
rs
      ]

  genFromTypeSpec :: forall (m :: * -> *).
(HasCallStack, MonadGenError m) =>
TypeSpec fn (Tree a) -> GenT m (Tree a)
genFromTypeSpec (TreeSpec Maybe Integer
mal Maybe Integer
msz Specification fn a
rs Specification fn (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 fn [Tree a]
childrenSpec =
          forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> Specification fn a
typeSpec forall a b. (a -> b) -> a -> b
$
            forall (fn :: [*] -> * -> *) a.
Maybe Integer
-> [a]
-> Specification fn Integer
-> Specification fn a
-> FoldSpec fn a
-> ListSpec fn a
ListSpec
              (forall a. a -> Maybe a
Just Integer
sz')
              []
              forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec
              (forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> Specification fn a
typeSpec forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
Maybe Integer
-> Maybe Integer
-> Specification fn a
-> Specification fn (a, [Tree a])
-> TreeSpec fn a
TreeSpec Maybe Integer
mal (forall a. a -> Maybe a
Just Integer
sz') forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec Specification fn (a, [Tree a])
s)
              forall (fn :: [*] -> * -> *) a. FoldSpec fn a
NoFold
        innerSpec :: Specification fn (a, [Tree a])
innerSpec = Specification fn (a, [Tree a])
s forall a. Semigroup a => a -> a -> a
<> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> Specification fn a
typeSpec (forall (fn :: [*] -> * -> *) a b.
Specification fn a -> Specification fn b -> PairSpec fn a b
Cartesian Specification fn a
rs Specification fn [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 (fn :: [*] -> * -> *) a (m :: * -> *).
(HasCallStack, HasSpec fn a, MonadGenError m) =>
Specification fn a -> GenT m a
genFromSpecT @fn @(a, [Tree a]) Specification fn (a, [Tree a])
innerSpec

  shrinkWithTypeSpec :: TypeSpec fn (Tree a) -> Tree a -> [Tree a]
shrinkWithTypeSpec (TreeSpec Maybe Integer
_ Maybe Integer
_ Specification fn a
rs Specification fn (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 (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn a -> a -> [a]
shrinkWithSpec Specification fn 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 (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> a -> [a]
shrinkWithTypeSpec (forall (fn :: [*] -> * -> *) a.
Maybe Integer
-> Maybe Integer
-> Specification fn a
-> Specification fn (a, [Tree a])
-> TreeSpec fn a
TreeSpec forall a. Maybe a
Nothing forall a. Maybe a
Nothing forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec Specification fn (a, [Tree a])
ctxSpec)) [Tree a]
ts
         ]

  cardinalTypeSpec :: TypeSpec fn (Tree a) -> Specification fn Integer
cardinalTypeSpec TypeSpec fn (Tree a)
_ = forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec

  toPreds :: Term fn (Tree a) -> TypeSpec fn (Tree a) -> Pred fn
toPreds Term fn (Tree a)
t (TreeSpec Maybe Integer
mal Maybe Integer
msz Specification fn a
rs Specification fn (a, [Tree a])
s) =
    (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 fn (Tree a)
t forall a b. (a -> b) -> a -> b
$ \Term fn (a, [Tree a])
n -> Term fn (a, [Tree a])
n forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
`satisfies` Specification fn (a, [Tree a])
s)
      forall a. Semigroup a => a -> a -> a
<> forall (fn :: [*] -> * -> *) a.
(Member (TreeFn fn) fn, HasSpec fn a) =>
Term fn (Tree a) -> Term fn a
rootLabel_ Term fn (Tree a)
t forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
`satisfies` Specification fn a
rs
      forall a. Semigroup a => a -> a -> a
<> forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall (fn :: [*] -> * -> *). Pred fn
TruePred (\Integer
sz -> forall (fn :: [*] -> * -> *) t.
HasGenHint fn t =>
Hint t -> Term fn t -> Pred fn
genHint (Maybe Integer
mal, Integer
sz) Term fn (Tree a)
t) Maybe Integer
msz

instance (Member (TreeFn fn) fn, HasSpec fn a) => HasGenHint fn (Tree a) where
  type Hint (Tree a) = (Maybe Integer, Integer)
  giveHint :: Hint (Tree a) -> Specification fn (Tree a)
giveHint (Maybe Integer
avgLen, Integer
sz) = forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> Specification fn a
typeSpec forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
Maybe Integer
-> Maybe Integer
-> Specification fn a
-> Specification fn (a, [Tree a])
-> TreeSpec fn a
TreeSpec Maybe Integer
avgLen (forall a. a -> Maybe a
Just Integer
sz) forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec

data TreeFn (fn :: [Type] -> Type -> Type) args res where
  RootLabel :: TreeFn fn '[Tree a] a

deriving instance Eq (TreeFn fn args res)
deriving instance Show (TreeFn fn args res)

instance FunctionLike (TreeFn fn) where
  sem :: forall (as :: [*]) b. TreeFn fn as b -> FunTy as b
sem TreeFn fn as b
RootLabel = \(Node b
a [Tree b]
_) -> b
a

instance (Member (TreeFn fn) fn, BaseUniverse fn) => Functions (TreeFn fn) fn where
  propagateSpecFun :: forall (as :: [*]) a b.
(TypeList as, Typeable as, HasSpec fn a, HasSpec fn b,
 All (HasSpec fn) as) =>
TreeFn fn as b
-> ListCtx Value as (HOLE a)
-> Specification fn b
-> Specification fn a
propagateSpecFun TreeFn fn as b
_ ListCtx Value as (HOLE a)
_ Specification fn b
TrueSpec = forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec
  propagateSpecFun TreeFn fn as b
_ ListCtx Value as (HOLE a)
_ (ErrorSpec NonEmpty String
err) = forall (fn :: [*] -> * -> *) a.
NonEmpty String -> Specification fn a
ErrorSpec NonEmpty String
err
  propagateSpecFun TreeFn fn as b
fn ListCtx Value as (HOLE a)
ctx Specification fn b
spec = case TreeFn fn as b
fn of
    TreeFn fn as b
_
      | SuspendedSpec Var b
v Pred fn
ps <- Specification fn b
spec
      , ListCtx List Value as
pre HOLE a a
HOLE List Value as'
suf <- ListCtx Value as (HOLE a)
ctx ->
          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 fn a
v' ->
            let args :: List (Term fn) (Append as (a : as'))
args = forall {a} (f :: a -> *) (as :: [a]) (bs :: [a]).
List f as -> List f bs -> List f (Append as bs)
appendList (forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList (\(Value a
a) -> forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
Lit a
a) List Value as
pre) (Term fn a
v' forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList (\(Value a
a) -> forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
Lit a
a) List Value as'
suf)
             in forall (fn :: [*] -> * -> *) a. Term fn a -> Binder fn a -> Pred fn
Let (forall (as :: [*]) (fn :: [*] -> * -> *) a.
(Typeable as, TypeList as, All (HasSpec fn) as, HasSpec fn a,
 BaseUniverse fn) =>
fn as a -> List (Term fn) as -> Term fn a
App (forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b.
Member fn fnU =>
fn as b -> fnU as b
injectFn TreeFn fn as b
fn) List (Term fn) (Append as (a : as'))
args) (Var b
v forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Var a -> Pred fn -> Binder fn a
:-> Pred fn
ps)
    TreeFn fn as b
RootLabel ->
      -- No TypeAbstractions in ghc-8.10
      case TreeFn fn as b
fn of
        (TreeFn fn '[Tree b] b
_ :: TreeFn fn '[Tree a] a)
          | NilCtx HOLE a (Tree b)
HOLE <- ListCtx Value as (HOLE a)
ctx -> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> Specification fn a
typeSpec forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
Maybe Integer
-> Maybe Integer
-> Specification fn a
-> Specification fn (a, [Tree a])
-> TreeSpec fn a
TreeSpec forall a. Maybe a
Nothing forall a. Maybe a
Nothing Specification fn b
spec forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec

  -- NOTE: this function over-approximates and returns a liberal spec.
  mapTypeSpec :: forall a b.
(HasSpec fn a, HasSpec fn b) =>
TreeFn fn '[a] b -> TypeSpec fn a -> Specification fn b
mapTypeSpec TreeFn fn '[a] b
f TypeSpec fn a
ts = case TreeFn fn '[a] b
f of
    TreeFn fn '[a] b
RootLabel ->
      -- No TypeAbstractions in ghc-8.10
      case TreeFn fn '[a] b
f of
        (TreeFn fn '[Tree b] b
_ :: TreeFn fn '[Tree a] a)
          | TreeSpec Maybe Integer
_ Maybe Integer
_ Specification fn b
rs Specification fn (b, [Tree b])
_ <- TypeSpec fn a
ts -> Specification fn b
rs

rootLabel_ ::
  forall fn a.
  (Member (TreeFn fn) fn, HasSpec fn a) =>
  Term fn (Tree a) ->
  Term fn a
rootLabel_ :: forall (fn :: [*] -> * -> *) a.
(Member (TreeFn fn) fn, HasSpec fn a) =>
Term fn (Tree a) -> Term fn a
rootLabel_ = forall (fn :: [*] -> * -> *) b (as :: [*]).
(HasSpec fn b, Typeable as, TypeList as, All (HasSpec fn) as) =>
fn as b -> FunTy (MapList (Term fn) as) (Term fn b)
app (forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b.
Member fn fnU =>
fn as b -> fnU as b
injectFn forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a. TreeFn fn '[Tree a] a
RootLabel @fn)