{-# 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)

------------------------------------------------------------------------
-- 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 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

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

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

-- TODO: get rid of this when we implement `cardinality`
-- in `HasSpec`
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

  -- NOTE: this function over-approximates and returns a liberal spec.
  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