{-# 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 _ ListCtx Value as (HOLE a) _ (MemberSpec []) = forall a (fn :: [*] -> * -> *). OrdSet a -> Specification fn a MemberSpec [] 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)