{-# 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.AbstractSyntax
import Constrained.Base (
  Forallable (..),
  HOLE (..),
  HasGenHint (..),
  HasSpec (..),
  Logic (..),
  Specification,
  Term,
  appTerm,
  constrained,
  errorLikeMessage,
  explainSpec,
  isErrorLike,
  typeSpec,
  pattern TypeSpec,
  pattern Unary,
 )
import Constrained.Conformance (
  conformsToSpec,
  satisfies,
 )
import Constrained.Core (
  unionWithMaybe,
 )
import Constrained.FunctionSymbol
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 (Eq (BinTree a)
Eq (BinTree a) =>
(BinTree a -> BinTree a -> Ordering)
-> (BinTree a -> BinTree a -> Bool)
-> (BinTree a -> BinTree a -> Bool)
-> (BinTree a -> BinTree a -> Bool)
-> (BinTree a -> BinTree a -> Bool)
-> (BinTree a -> BinTree a -> BinTree a)
-> (BinTree a -> BinTree a -> BinTree a)
-> Ord (BinTree a)
BinTree a -> BinTree a -> Bool
BinTree a -> BinTree a -> Ordering
BinTree a -> BinTree a -> BinTree a
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
$ccompare :: forall a. Ord a => BinTree a -> BinTree a -> Ordering
compare :: BinTree a -> BinTree a -> Ordering
$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
>= :: BinTree a -> BinTree a -> Bool
$cmax :: forall a. Ord a => BinTree a -> BinTree a -> BinTree a
max :: BinTree a -> BinTree a -> BinTree a
$cmin :: forall a. Ord a => BinTree a -> BinTree a -> BinTree a
min :: BinTree a -> BinTree a -> BinTree a
Ord, BinTree a -> BinTree a -> Bool
(BinTree a -> BinTree a -> Bool)
-> (BinTree a -> BinTree a -> Bool) -> Eq (BinTree a)
forall a. Eq a => BinTree a -> BinTree a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
/= :: BinTree a -> BinTree a -> Bool
Eq, Int -> BinTree a -> ShowS
[BinTree a] -> ShowS
BinTree a -> String
(Int -> BinTree a -> ShowS)
-> (BinTree a -> String)
-> ([BinTree a] -> ShowS)
-> Show (BinTree a)
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
$cshowsPrec :: forall a. Show a => Int -> BinTree a -> ShowS
showsPrec :: Int -> BinTree a -> ShowS
$cshow :: forall a. Show a => BinTree a -> String
show :: BinTree a -> String
$cshowList :: forall a. Show a => [BinTree a] -> ShowS
showList :: [BinTree a] -> ShowS
Show, (forall x. BinTree a -> Rep (BinTree a) x)
-> (forall x. Rep (BinTree a) x -> BinTree a)
-> Generic (BinTree a)
forall x. Rep (BinTree a) x -> BinTree a
forall x. BinTree a -> Rep (BinTree a) x
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
$cfrom :: forall a x. BinTree a -> Rep (BinTree a) x
from :: forall x. BinTree a -> Rep (BinTree a) x
$cto :: forall a x. Rep (BinTree a) x -> BinTree a
to :: forall x. Rep (BinTree a) x -> BinTree a
Generic)

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

data BinTreeSpec a = BinTreeSpec (Maybe Integer) (Specification (BinTree a, a, BinTree a))
  deriving (Int -> BinTreeSpec a -> ShowS
[BinTreeSpec a] -> ShowS
BinTreeSpec a -> String
(Int -> BinTreeSpec a -> ShowS)
-> (BinTreeSpec a -> String)
-> ([BinTreeSpec a] -> ShowS)
-> Show (BinTreeSpec a)
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
$cshowsPrec :: forall a. HasSpec a => Int -> BinTreeSpec a -> ShowS
showsPrec :: Int -> BinTreeSpec a -> ShowS
$cshow :: forall a. HasSpec a => BinTreeSpec a -> String
show :: BinTreeSpec a -> String
$cshowList :: forall a. HasSpec a => [BinTreeSpec a] -> ShowS
showList :: [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 = TypeSpec (BinTree a) -> Specification (BinTree a)
BinTreeSpec a -> Specification (BinTree a)
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (BinTreeSpec a -> Specification (BinTree a))
-> (Specification (BinTree a, a, BinTree a) -> BinTreeSpec a)
-> Specification (BinTree a, a, BinTree a)
-> Specification (BinTree a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Integer
-> Specification (BinTree a, a, BinTree a) -> BinTreeSpec a
forall a.
Maybe Integer
-> Specification (BinTree a, a, BinTree a) -> BinTreeSpec a
BinTreeSpec Maybe Integer
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) (BinTree a, a, BinTree a)
-> [(BinTree a, a, BinTree a)] -> [(BinTree a, a, BinTree a)]
forall a. a -> [a] -> [a]
: BinTree a -> [(BinTree a, a, BinTree a)]
forall t e. Forallable t e => t -> [e]
forAllToList BinTree a
left [(BinTree a, a, BinTree a)]
-> [(BinTree a, a, BinTree a)] -> [(BinTree a, a, BinTree a)]
forall a. [a] -> [a] -> [a]
++ BinTree a -> [(BinTree a, a, BinTree 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 = Maybe Integer
-> Specification (BinTree a, a, BinTree a) -> BinTreeSpec a
forall a.
Maybe Integer
-> Specification (BinTree a, a, BinTree a) -> BinTreeSpec a
BinTreeSpec Maybe Integer
forall a. Maybe a
Nothing Specification (BinTree a, a, BinTree a)
forall deps a. SpecificationD deps 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') =
    TypeSpec (BinTree a) -> Specification (BinTree a)
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (TypeSpec (BinTree a) -> Specification (BinTree a))
-> TypeSpec (BinTree a) -> Specification (BinTree a)
forall a b. (a -> b) -> a -> b
$ Maybe Integer
-> Specification (BinTree a, a, BinTree a) -> BinTreeSpec a
forall a.
Maybe Integer
-> Specification (BinTree a, a, BinTree a) -> BinTreeSpec a
BinTreeSpec ((Integer -> Integer -> Integer)
-> Maybe Integer -> Maybe Integer -> Maybe Integer
forall a. (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a
unionWithMaybe Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min Maybe Integer
sz Maybe Integer
sz') (Specification (BinTree a, a, BinTree a)
s Specification (BinTree a, a, BinTree a)
-> Specification (BinTree a, a, BinTree a)
-> Specification (BinTree a, a, BinTree a)
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) =
    [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and
      [ (BinTree a
left, a
a, BinTree a
right) (BinTree a, a, BinTree a)
-> Specification (BinTree a, a, BinTree a) -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification (BinTree a, a, BinTree a)
es
      , BinTree a
left BinTree a -> TypeSpec (BinTree a) -> Bool
forall a. (HasSpec a, HasCallStack) => a -> TypeSpec a -> Bool
`conformsTo` TypeSpec (BinTree a)
s
      , BinTree a
right BinTree a -> TypeSpec (BinTree a) -> Bool
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 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
0 = BinTree a -> GenT m (BinTree a)
forall a. a -> GenT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure BinTree a
forall a. BinTree a
BinTip
    | Bool
otherwise = do
        let sz :: Integer
sz = Integer -> (Integer -> Integer) -> Maybe Integer -> Integer
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Integer
20 Integer -> Integer
forall a. a -> a
id Maybe Integer
msz
            sz' :: Integer
sz' = Integer
sz Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
2
        [GenT GE (BinTree a)] -> GenT m (BinTree a)
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) (Specification (BinTree a, a, BinTree a)
 -> GenT GE (BinTree a, a, BinTree a))
-> Specification (BinTree a, a, BinTree a)
-> GenT GE (BinTree a, a, BinTree a)
forall a b. (a -> b) -> a -> b
$
                (Term (BinTree a, a, BinTree a) -> [Pred])
-> Specification (BinTree a, a, BinTree a)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (BinTree a, a, BinTree a) -> [Pred])
 -> Specification (BinTree a, a, BinTree a))
-> (Term (BinTree a, a, BinTree a) -> [Pred])
-> Specification (BinTree a, a, BinTree a)
forall a b. (a -> b) -> a -> b
$ \Term (BinTree a, a, BinTree a)
ctx ->
                  [ Term (BinTree a, a, BinTree a)
-> FunTy
     (MapList Term (ProductAsList (BinTree a, a, BinTree a))) [Pred]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (BinTree a, a, BinTree a)
ctx (FunTy
   (MapList Term (ProductAsList (BinTree a, a, BinTree a))) [Pred]
 -> Pred)
-> FunTy
     (MapList Term (ProductAsList (BinTree a, a, BinTree a))) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term (BinTree a)
left TermD Deps a
_ Term (BinTree a)
right ->
                      [ Term (BinTree a)
-> (Term (BinTree a, a, BinTree a) -> Pred) -> Pred
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (BinTree a)
left (Term (BinTree a, a, BinTree a)
-> Specification (BinTree a, a, BinTree a) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification (BinTree a, a, BinTree a)
s)
                      , Hint (BinTree a) -> Term (BinTree a) -> Pred
forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint Integer
Hint (BinTree a)
sz' Term (BinTree a)
left
                      , Term (BinTree a)
-> (Term (BinTree a, a, BinTree a) -> Pred) -> Pred
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (BinTree a)
right (Term (BinTree a, a, BinTree a)
-> Specification (BinTree a, a, BinTree a) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification (BinTree a, a, BinTree a)
s)
                      , Hint (BinTree a) -> Term (BinTree a) -> Pred
forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint Integer
Hint (BinTree a)
sz' Term (BinTree a)
right
                      ]
                  , Term (BinTree a, a, BinTree a)
ctx Term (BinTree a, a, BinTree a)
-> Specification (BinTree a, a, BinTree a) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification (BinTree a, a, BinTree a)
s
                  ]
              BinTree a -> GenT GE (BinTree a)
forall a. a -> GenT GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BinTree a -> GenT GE (BinTree a))
-> BinTree a -> GenT GE (BinTree a)
forall a b. (a -> b) -> a -> b
$ BinTree a -> a -> BinTree a -> BinTree a
forall a. BinTree a -> a -> BinTree a -> BinTree a
BinNode BinTree a
left a
a BinTree a
right
          , BinTree a -> GenT GE (BinTree a)
forall a. a -> GenT GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure BinTree a
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) =
    BinTree a
forall a. BinTree a
BinTip
      BinTree a -> [BinTree a] -> [BinTree a]
forall a. a -> [a] -> [a]
: BinTree a
left
      BinTree a -> [BinTree a] -> [BinTree a]
forall a. a -> [a] -> [a]
: BinTree a
right
      BinTree a -> [BinTree a] -> [BinTree a]
forall a. a -> [a] -> [a]
: (BinTree a -> a -> BinTree a -> BinTree a
forall a. BinTree a -> a -> BinTree a -> BinTree a
BinNode BinTree a
left a
a (BinTree a -> BinTree a) -> [BinTree a] -> [BinTree a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeSpec (BinTree a) -> BinTree a -> [BinTree a]
forall a. HasSpec a => TypeSpec a -> a -> [a]
shrinkWithTypeSpec TypeSpec (BinTree a)
s BinTree a
right)
      [BinTree a] -> [BinTree a] -> [BinTree a]
forall a. [a] -> [a] -> [a]
++ ((\BinTree a
l -> BinTree a -> a -> BinTree a -> BinTree a
forall a. BinTree a -> a -> BinTree a -> BinTree a
BinNode BinTree a
l a
a BinTree a
right) (BinTree a -> BinTree a) -> [BinTree a] -> [BinTree a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeSpec (BinTree a) -> BinTree a -> [BinTree a]
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)
_ = Specification Integer
forall deps a. SpecificationD deps 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) =
    (Term (BinTree a)
-> (Term (BinTree a, a, BinTree a) -> Pred) -> Pred
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (BinTree a)
t ((Term (BinTree a, a, BinTree a) -> Pred) -> Pred)
-> (Term (BinTree a, a, BinTree a) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term (BinTree a, a, BinTree a)
n -> Term (BinTree a, a, BinTree a)
n Term (BinTree a, a, BinTree a)
-> Specification (BinTree a, a, BinTree a) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification (BinTree a, a, BinTree a)
s)
      Pred -> Pred -> Pred
forall a. Semigroup a => a -> a -> a
<> Pred -> (Integer -> Pred) -> Maybe Integer -> Pred
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Pred
forall deps. PredD deps
TruePred ((Integer -> Term (BinTree a) -> Pred)
-> Term (BinTree a) -> Integer -> Pred
forall a b c. (a -> b -> c) -> b -> a -> c
flip Integer -> Term (BinTree a) -> Pred
Hint (BinTree a) -> Term (BinTree a) -> Pred
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 = TypeSpec (BinTree a) -> Specification (BinTree a)
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (TypeSpec (BinTree a) -> Specification (BinTree a))
-> TypeSpec (BinTree a) -> Specification (BinTree a)
forall a b. (a -> b) -> a -> b
$ Maybe Integer
-> Specification (BinTree a, a, BinTree a) -> BinTreeSpec a
forall a.
Maybe Integer
-> Specification (BinTree a, a, BinTree a) -> BinTreeSpec a
BinTreeSpec (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
Hint (BinTree a)
h) Specification (BinTree a, a, BinTree a)
forall deps a. SpecificationD deps 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 = TreeSpec a -> Specification (Tree a)
forall a. HasSpec (Tree a) => TreeSpec a -> Specification (Tree a)
guardRoseSpec (TreeSpec a -> Specification (Tree a))
-> (Specification (a, [Tree a]) -> TreeSpec a)
-> Specification (a, [Tree a])
-> Specification (Tree a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Integer
-> Maybe Integer
-> Specification a
-> Specification (a, [Tree a])
-> TreeSpec a
forall a.
Maybe Integer
-> Maybe Integer
-> Specification a
-> Specification (a, [Tree a])
-> TreeSpec a
TreeSpec Maybe Integer
forall a. Maybe a
Nothing Maybe Integer
forall a. Maybe a
Nothing Specification a
forall deps a. SpecificationD deps a
TrueSpec
  forAllToList :: Tree a -> [(a, [Tree a])]
forAllToList (Node a
a [Tree a]
children) = (a
a, [Tree a]
children) (a, [Tree a]) -> [(a, [Tree a])] -> [(a, [Tree a])]
forall a. a -> [a] -> [a]
: (Tree a -> [(a, [Tree a])]) -> [Tree a] -> [(a, [Tree a])]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Tree a -> [(a, [Tree a])]
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)
  | Specification a -> Bool
forall a. Specification a -> Bool
isErrorLike Specification a
rs = NonEmpty String -> SpecificationD Deps (Tree a)
forall deps a. NonEmpty String -> SpecificationD deps a
ErrorSpec (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"guardRoseSpec: rootSpec is error")
  | Specification (a, [Tree a]) -> Bool
forall a. Specification a -> Bool
isErrorLike Specification (a, [Tree a])
s = NonEmpty String -> SpecificationD Deps (Tree a)
forall deps a. NonEmpty String -> SpecificationD deps a
ErrorSpec (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"guardRoseSpec: ctxSpec is error")
  | Bool
otherwise = TypeSpec (Tree a) -> [Tree a] -> SpecificationD Deps (Tree a)
forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
TypeSpec TypeSpec (Tree a)
TreeSpec a
spec []

instance HasSpec a => HasSpec (Tree a) where
  type TypeSpec (Tree a) = TreeSpec a

  emptySpec :: TypeSpec (Tree a)
emptySpec = Maybe Integer
-> Maybe Integer
-> Specification a
-> Specification (a, [Tree a])
-> TreeSpec a
forall a.
Maybe Integer
-> Maybe Integer
-> Specification a
-> Specification (a, [Tree a])
-> TreeSpec a
TreeSpec Maybe Integer
forall a. Maybe a
Nothing Maybe Integer
forall a. Maybe a
Nothing Specification a
forall deps a. SpecificationD deps a
TrueSpec Specification (a, [Tree a])
forall deps a. SpecificationD deps 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')
    | Specification (a, [Tree a]) -> Bool
forall a. Specification a -> Bool
isErrorLike Specification (a, [Tree a])
alteredspec = NonEmpty String -> Specification (Tree a)
forall deps a. NonEmpty String -> SpecificationD deps a
ErrorSpec (Specification (a, [Tree a]) -> NonEmpty String
forall a. Specification a -> NonEmpty String
errorLikeMessage Specification (a, [Tree a])
alteredspec)
    | Bool
otherwise =
        TreeSpec a -> Specification (Tree a)
forall a. HasSpec (Tree a) => TreeSpec a -> Specification (Tree a)
guardRoseSpec (TreeSpec a -> Specification (Tree a))
-> TreeSpec a -> Specification (Tree a)
forall a b. (a -> b) -> a -> b
$
          Maybe Integer
-> Maybe Integer
-> Specification a
-> Specification (a, [Tree a])
-> TreeSpec a
forall a.
Maybe Integer
-> Maybe Integer
-> Specification a
-> Specification (a, [Tree a])
-> TreeSpec a
TreeSpec
            ((Integer -> Integer -> Integer)
-> Maybe Integer -> Maybe Integer -> Maybe Integer
forall a. (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a
unionWithMaybe Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Maybe Integer
mal Maybe Integer
mal')
            ((Integer -> Integer -> Integer)
-> Maybe Integer -> Maybe Integer -> Maybe Integer
forall a. (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a
unionWithMaybe Integer -> Integer -> Integer
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 = (TypeSpec (a, [Tree a]) -> Specification (a, [Tree a])
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (Specification a -> Specification [Tree a] -> PairSpec a [Tree a]
forall a b. Specification a -> Specification b -> PairSpec a b
Cartesian Specification a
rs'' Specification [Tree a]
forall deps a. SpecificationD deps a
TrueSpec) Specification (a, [Tree a])
-> Specification (a, [Tree a]) -> Specification (a, [Tree a])
forall a. Semigroup a => a -> a -> a
<> Specification (a, [Tree a])
s'')
      rs'' :: Specification a
rs'' = Specification a
rs Specification a -> Specification a -> Specification a
forall a. Semigroup a => a -> a -> a
<> Specification a
rs'
      s'' :: Specification (a, [Tree a])
s'' = Specification (a, [Tree a])
s Specification (a, [Tree a])
-> Specification (a, [Tree a]) -> Specification (a, [Tree a])
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) =
    [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and
      [ (a
a, [Tree a]
children) (a, [Tree a]) -> Specification (a, [Tree a]) -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification (a, [Tree a])
s
      , (Tree a -> Bool) -> [Tree a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\(Node a
a' [Tree a]
children') -> (a
a', [Tree a]
children') (a, [Tree a]) -> Specification (a, [Tree a]) -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification (a, [Tree a])
s) [Tree a]
children
      , a
a a -> Specification a -> Bool
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 = Integer -> (Integer -> Integer) -> Maybe Integer -> Integer
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Integer
20 Integer -> Integer
forall a. a -> a
id Maybe Integer
msz
        sz' :: Integer
sz' = Integer -> (Integer -> Integer) -> Maybe Integer -> Integer
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Integer
sz Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
4) (Integer
sz Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div`) Maybe Integer
mal
        childrenSpec :: Specification [Tree a]
childrenSpec =
          TypeSpec [Tree a] -> Specification [Tree a]
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (TypeSpec [Tree a] -> Specification [Tree a])
-> TypeSpec [Tree a] -> Specification [Tree a]
forall a b. (a -> b) -> a -> b
$
            Maybe Integer
-> [Tree a]
-> Specification Integer
-> Specification (Tree a)
-> FoldSpec (Tree a)
-> ListSpec (Tree a)
forall a.
Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
ListSpec
              (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
sz')
              []
              Specification Integer
forall deps a. SpecificationD deps a
TrueSpec
              (TypeSpec (Tree a) -> Specification (Tree a)
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (TypeSpec (Tree a) -> Specification (Tree a))
-> TypeSpec (Tree a) -> Specification (Tree a)
forall a b. (a -> b) -> a -> b
$ Maybe Integer
-> Maybe Integer
-> Specification a
-> Specification (a, [Tree a])
-> TreeSpec a
forall a.
Maybe Integer
-> Maybe Integer
-> Specification a
-> Specification (a, [Tree a])
-> TreeSpec a
TreeSpec Maybe Integer
mal (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
sz') Specification a
forall deps a. SpecificationD deps a
TrueSpec Specification (a, [Tree a])
s)
              FoldSpec (Tree a)
forall a. FoldSpec a
NoFold
        innerSpec :: Specification (a, [Tree a])
innerSpec = Specification (a, [Tree a])
s Specification (a, [Tree a])
-> Specification (a, [Tree a]) -> Specification (a, [Tree a])
forall a. Semigroup a => a -> a -> a
<> TypeSpec (a, [Tree a]) -> Specification (a, [Tree a])
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (Specification a -> Specification [Tree a] -> PairSpec a [Tree a]
forall a b. Specification a -> Specification b -> PairSpec a b
Cartesian Specification a
rs Specification [Tree a]
childrenSpec)
    ((a, [Tree a]) -> Tree a)
-> GenT m (a, [Tree a]) -> GenT m (Tree a)
forall a b. (a -> b) -> GenT m a -> GenT m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> [Tree a] -> Tree a) -> (a, [Tree a]) -> Tree a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry a -> [Tree a] -> Tree a
forall a. a -> [Tree a] -> Tree a
Node) (GenT m (a, [Tree a]) -> GenT m (Tree a))
-> GenT m (a, [Tree a]) -> GenT m (Tree a)
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) =
    [a -> [Tree a] -> Tree a
forall a. a -> [Tree a] -> Tree a
Node a
a [] | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Tree a] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Tree a]
ts]
      [Tree a] -> [Tree a] -> [Tree a]
forall a. [a] -> [a] -> [a]
++ [Tree a]
ts
      [Tree a] -> [Tree a] -> [Tree a]
forall a. [a] -> [a] -> [a]
++ [a -> [Tree a] -> Tree a
forall a. a -> [Tree a] -> Tree a
Node a
a' [Tree a]
ts | a
a' <- Specification a -> a -> [a]
forall a. HasSpec a => Specification a -> a -> [a]
shrinkWithSpec Specification a
rs a
a]
      [Tree a] -> [Tree a] -> [Tree a]
forall a. [a] -> [a] -> [a]
++ [a -> [Tree a] -> Tree a
forall a. a -> [Tree a] -> Tree a
Node a
a [Tree a
t] | Tree a
t <- [Tree a]
ts]
      [Tree a] -> [Tree a] -> [Tree a]
forall a. [a] -> [a] -> [a]
++ [ a -> [Tree a] -> Tree a
forall a. a -> [Tree a] -> Tree a
Node a
a [Tree a]
ts'
         | [Tree a]
ts' <- (Tree a -> [Tree a]) -> [Tree a] -> [[Tree a]]
forall a. (a -> [a]) -> [a] -> [[a]]
shrinkList (TypeSpec (Tree a) -> Tree a -> [Tree a]
forall a. HasSpec a => TypeSpec a -> a -> [a]
shrinkWithTypeSpec (Maybe Integer
-> Maybe Integer
-> Specification a
-> Specification (a, [Tree a])
-> TreeSpec a
forall a.
Maybe Integer
-> Maybe Integer
-> Specification a
-> Specification (a, [Tree a])
-> TreeSpec a
TreeSpec Maybe Integer
forall a. Maybe a
Nothing Maybe Integer
forall a. Maybe a
Nothing Specification a
forall deps a. SpecificationD deps a
TrueSpec Specification (a, [Tree a])
ctxSpec)) [Tree a]
ts
         ]

  cardinalTypeSpec :: TypeSpec (Tree a) -> Specification Integer
cardinalTypeSpec TypeSpec (Tree a)
_ = Specification Integer
forall deps a. SpecificationD deps 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) =
    (Term (Tree a) -> (Term (a, [Tree a]) -> Pred) -> Pred
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Tree a)
t ((Term (a, [Tree a]) -> Pred) -> Pred)
-> (Term (a, [Tree a]) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term (a, [Tree a])
n -> Term (a, [Tree a])
n Term (a, [Tree a]) -> Specification (a, [Tree a]) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification (a, [Tree a])
s)
      Pred -> Pred -> Pred
forall a. Semigroup a => a -> a -> a
<> Term (Tree a) -> Term a
forall a. HasSpec a => Term (Tree a) -> Term a
rootLabel_ Term (Tree a)
t
        Term a -> Specification a -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification a
rs
      Pred -> Pred -> Pred
forall a. Semigroup a => a -> a -> a
<> Pred -> (Integer -> Pred) -> Maybe Integer -> Pred
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Pred
forall deps. PredD deps
TruePred (\Integer
sz -> Hint (Tree a) -> Term (Tree a) -> Pred
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) = TypeSpec (Tree a) -> Specification (Tree a)
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (TypeSpec (Tree a) -> Specification (Tree a))
-> TypeSpec (Tree a) -> Specification (Tree a)
forall a b. (a -> b) -> a -> b
$ Maybe Integer
-> Maybe Integer
-> Specification a
-> Specification (a, [Tree a])
-> TreeSpec a
forall a.
Maybe Integer
-> Maybe Integer
-> Specification a
-> Specification (a, [Tree a])
-> TreeSpec a
TreeSpec Maybe Integer
avgLen (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
sz) Specification a
forall deps a. SpecificationD deps a
TrueSpec Specification (a, [Tree a])
forall deps a. SpecificationD deps 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

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 SpecificationD Deps b
s) = [String] -> Specification a -> Specification a
forall a. [String] -> Specification a -> Specification a
explainSpec [String]
es (Specification a -> Specification a)
-> Specification a -> Specification a
forall a b. (a -> b) -> a -> b
$ TreeW as b
-> ListCtx Value as (HOLE a)
-> SpecificationD Deps b
-> Specification a
forall (as :: [*]) b a.
(AppRequires TreeW as b, HasSpec a) =>
TreeW as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
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 SpecificationD Deps b
s
  propagate TreeW as b
_ ListCtx Value as (HOLE a)
_ SpecificationD Deps b
TrueSpec = Specification a
forall deps a. SpecificationD deps a
TrueSpec
  propagate TreeW as b
_ ListCtx Value as (HOLE a)
_ (ErrorSpec NonEmpty String
msgs) = NonEmpty String -> Specification a
forall deps a. NonEmpty String -> SpecificationD deps a
ErrorSpec NonEmpty String
msgs
  propagate TreeW as b
RootLabelW (Unary HOLE a (Tree b)
HOLE) (SuspendedSpec Var b
v Pred
ps) = (Term a -> Pred) -> Specification a
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term a -> Pred) -> Specification a)
-> (Term a -> Pred) -> Specification a
forall a b. (a -> b) -> a -> b
$ \Term a
v' -> TermD Deps b -> BinderD Deps b -> Pred
forall deps a. TermD deps a -> BinderD deps a -> PredD deps
Let (TreeW '[Tree b] b -> List Term '[Tree b] -> TermD Deps b
forall deps (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequiresD deps t dom a =>
t dom a -> List (TermD deps) dom -> TermD deps a
App TreeW '[Tree b] b
forall a. HasSpec a => TreeW '[Tree a] a
RootLabelW (Term a
TermD Deps (Tree b)
v' TermD Deps (Tree b) -> List Term '[] -> List Term '[Tree b]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List Term '[]
forall {k} (f :: k -> *). List f '[]
Nil)) (Var b
v Var b -> Pred -> BinderD Deps b
forall deps a.
(HasSpecD deps a, Show a) =>
Var a -> PredD deps -> BinderD deps a
:-> Pred
ps)
  propagate TreeW as b
RootLabelW (Unary HOLE a (Tree b)
HOLE) SpecificationD Deps b
spec = TypeSpec a -> Specification a
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (TypeSpec a -> Specification a) -> TypeSpec a -> Specification a
forall a b. (a -> b) -> a -> b
$ Maybe Integer
-> Maybe Integer
-> SpecificationD Deps b
-> Specification (b, [Tree b])
-> TreeSpec b
forall a.
Maybe Integer
-> Maybe Integer
-> Specification a
-> Specification (a, [Tree a])
-> TreeSpec a
TreeSpec Maybe Integer
forall a. Maybe a
Nothing Maybe Integer
forall a. Maybe a
Nothing SpecificationD Deps b
spec Specification (b, [Tree b])
forall deps a. SpecificationD deps 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_ = TreeW '[Tree a] a -> FunTy (MapList Term '[Tree a]) (TermD Deps a)
forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm TreeW '[Tree a] a
forall a. HasSpec a => TreeW '[Tree a] a
RootLabelW