{-# LANGUAGE BangPatterns           #-}
{-# LANGUAGE CPP                    #-}
{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE DeriveDataTypeable     #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs                  #-}
{-# LANGUAGE RankNTypes             #-}
{-# LANGUAGE Safe                   #-}
{-# LANGUAGE ScopedTypeVariables    #-}
{-# LANGUAGE StandaloneDeriving     #-}
{-# LANGUAGE TypeFamilies           #-}
-- | Depth indexed perfect binary tree.
module Data.RAVec.Tree (
    Tree (..),

    -- * Construction
    singleton,

    -- * Conversions
    toList,
    reverse,

    -- * Indexing
    (!),
    tabulate,
    leftmost,
    rightmost,

    -- * Folds
    foldMap,
    foldMap1,
    ifoldMap,
    ifoldMap1,
    foldr,
    ifoldr,
    foldr1Map,
    ifoldr1Map,
    foldl,
    ifoldl,

    -- * Special folds
    length,
    null,
    sum,
    product,

    -- * Mapping
    map,
    imap,
    traverse,
    itraverse,
#ifdef MIN_VERSION_semigroupoids
    traverse1,
    itraverse1,
#endif
    itraverse_,

    -- * Zipping
    zipWith,
    izipWith,
    repeat,

    -- * Universe
    universe,

    -- * QuickCheck
    liftArbitrary,
    liftShrink,
    ) where

import Prelude
       (Bool (..), Eq (..), Functor (..), Int, Num, Ord (..), Show, id, seq,
       uncurry, ($), (*), (+), (.))

import Control.Applicative (Applicative (..), (<$>))
import Control.DeepSeq     (NFData (..))
import Control.Monad       (void)
import Data.Hashable       (Hashable (..))
import Data.Monoid         (Monoid (..))
import Data.Nat            (Nat (..))
import Data.Semigroup      (Semigroup (..))
import Data.Typeable       (Typeable)
import Data.Wrd            (Wrd (..))

import qualified Data.Type.Nat as N

-- instances
import qualified Data.Foldable    as I (Foldable (..))
import qualified Data.Traversable as I (Traversable (..))
import qualified Test.QuickCheck  as QC

import qualified Data.Functor.WithIndex     as WI (FunctorWithIndex (..))
import qualified Data.Foldable.WithIndex    as WI (FoldableWithIndex (..))
import qualified Data.Traversable.WithIndex as WI (TraversableWithIndex (..))

#ifdef MIN_VERSION_distributive
import qualified Data.Distributive as I (Distributive (..))

#ifdef MIN_VERSION_adjunctions
import qualified Data.Functor.Rep as I (Representable (..))
#endif
#endif

#ifdef MIN_VERSION_semigroupoids
import Data.Functor.Apply (Apply (..))

import qualified Data.Semigroup.Foldable    as I (Foldable1 (..))
import qualified Data.Semigroup.Traversable as I (Traversable1 (..))
#endif

-- $setup
-- >>> :set -XScopedTypeVariables
-- >>> import Data.Proxy (Proxy (..))
-- >>> import Prelude (Char, not, uncurry, flip, ($), Bool (..))
-- >>> import Data.Wrd (Wrd (..))
-- >>> import qualified Data.Type.Nat as N

-------------------------------------------------------------------------------
-- Data
-------------------------------------------------------------------------------

-- | Perfectly balanced binary tree of depth @n@, with @2 ^ n@ elements.
data Tree (n :: Nat) a where
    Leaf :: a -> Tree 'Z a
    Node :: Tree n a -> Tree n a -> Tree ('S n) a
  deriving (Typeable)

-------------------------------------------------------------------------------
-- Helpers
-------------------------------------------------------------------------------

goLeft :: (Wrd ('S n) -> a) -> Wrd n -> a
goLeft :: (Wrd ('S n) -> a) -> Wrd n -> a
goLeft Wrd ('S n) -> a
f Wrd n
xs = Wrd ('S n) -> a
f (Wrd n -> Wrd ('S n)
forall (n1 :: Nat). Wrd n1 -> Wrd ('S n1)
W0 Wrd n
xs)

goRight :: (Wrd ('S n) -> a) -> Wrd n -> a
goRight :: (Wrd ('S n) -> a) -> Wrd n -> a
goRight Wrd ('S n) -> a
f Wrd n
xs = Wrd ('S n) -> a
f (Wrd n -> Wrd ('S n)
forall (n1 :: Nat). Wrd n1 -> Wrd ('S n1)
W1 Wrd n
xs)

-------------------------------------------------------------------------------
-- Instances
-------------------------------------------------------------------------------

deriving instance Eq a => Eq (Tree n a)
deriving instance Ord a => Ord (Tree n a)
deriving instance Show a => Show (Tree n a)

instance Functor (Tree n) where
    fmap :: (a -> b) -> Tree n a -> Tree n b
fmap = (a -> b) -> Tree n a -> Tree n b
forall a b (n :: Nat). (a -> b) -> Tree n a -> Tree n b
map

instance I.Foldable (Tree n) where
    foldMap :: (a -> m) -> Tree n a -> m
foldMap = (a -> m) -> Tree n a -> m
forall m a (n :: Nat). Monoid m => (a -> m) -> Tree n a -> m
foldMap
    foldr :: (a -> b -> b) -> b -> Tree n a -> b
foldr   = (a -> b -> b) -> b -> Tree n a -> b
forall a b (n :: Nat). (a -> b -> b) -> b -> Tree n a -> b
foldr
    foldl :: (b -> a -> b) -> b -> Tree n a -> b
foldl   = (b -> a -> b) -> b -> Tree n a -> b
forall b a (n :: Nat). (b -> a -> b) -> b -> Tree n a -> b
foldl
#if MIN_VERSION_base(4,8,0)
    null :: Tree n a -> Bool
null   = Tree n a -> Bool
forall (n :: Nat) a. Tree n a -> Bool
null
    toList :: Tree n a -> [a]
toList = Tree n a -> [a]
forall (n :: Nat) a. Tree n a -> [a]
toList
    length :: Tree n a -> Int
length = Tree n a -> Int
forall (n :: Nat) a. Tree n a -> Int
length
#endif

instance I.Traversable (Tree n) where
    traverse :: (a -> f b) -> Tree n a -> f (Tree n b)
traverse = (a -> f b) -> Tree n a -> f (Tree n b)
forall (f :: * -> *) a b (n :: Nat).
Applicative f =>
(a -> f b) -> Tree n a -> f (Tree n b)
traverse

-- | @since 0.2
instance WI.FunctorWithIndex (Wrd n) (Tree n) where
    imap :: (Wrd n -> a -> b) -> Tree n a -> Tree n b
imap = (Wrd n -> a -> b) -> Tree n a -> Tree n b
forall (n :: Nat) a b. (Wrd n -> a -> b) -> Tree n a -> Tree n b
imap

-- | @since 0.2
instance WI.FoldableWithIndex (Wrd n) (Tree n) where
    ifoldMap :: (Wrd n -> a -> m) -> Tree n a -> m
ifoldMap = (Wrd n -> a -> m) -> Tree n a -> m
forall m (n :: Nat) a.
Monoid m =>
(Wrd n -> a -> m) -> Tree n a -> m
ifoldMap
    ifoldr :: (Wrd n -> a -> b -> b) -> b -> Tree n a -> b
ifoldr   = (Wrd n -> a -> b -> b) -> b -> Tree n a -> b
forall (n :: Nat) a b. (Wrd n -> a -> b -> b) -> b -> Tree n a -> b
ifoldr

-- | @since 0.2
instance WI.TraversableWithIndex (Wrd n) (Tree n) where
    itraverse :: (Wrd n -> a -> f b) -> Tree n a -> f (Tree n b)
itraverse = (Wrd n -> a -> f b) -> Tree n a -> f (Tree n b)
forall (f :: * -> *) (n :: Nat) a b.
Applicative f =>
(Wrd n -> a -> f b) -> Tree n a -> f (Tree n b)
itraverse

#ifdef MIN_VERSION_semigroupoids
instance I.Foldable1 (Tree n) where
    foldMap1 :: (a -> m) -> Tree n a -> m
foldMap1 = (a -> m) -> Tree n a -> m
forall s a (n :: Nat). Semigroup s => (a -> s) -> Tree n a -> s
foldMap1

instance I.Traversable1 (Tree n) where
    traverse1 :: (a -> f b) -> Tree n a -> f (Tree n b)
traverse1 = (a -> f b) -> Tree n a -> f (Tree n b)
forall (f :: * -> *) a b (n :: Nat).
Apply f =>
(a -> f b) -> Tree n a -> f (Tree n b)
traverse1
#endif

instance NFData a => NFData (Tree n a) where
    rnf :: Tree n a -> ()
rnf (Leaf a
x)   = a -> ()
forall a. NFData a => a -> ()
rnf a
x
    rnf (Node Tree n a
x Tree n a
y) = Tree n a -> ()
forall a. NFData a => a -> ()
rnf Tree n a
x () -> () -> ()
`seq` Tree n a -> ()
forall a. NFData a => a -> ()
rnf Tree n a
y

instance Hashable a => Hashable (Tree n a) where
    hashWithSalt :: Int -> Tree n a -> Int
hashWithSalt Int
salt (Leaf a
x) = Int
salt
        Int -> a -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` a
x
    hashWithSalt Int
salt (Node Tree n a
x Tree n a
y) = Int
salt
        Int -> Tree n a -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Tree n a
x
        Int -> Tree n a -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Tree n a
y

instance N.SNatI n => Applicative (Tree n) where
    pure :: a -> Tree n a
pure = a -> Tree n a
forall (n :: Nat) a. SNatI n => a -> Tree n a
repeat
    <*> :: Tree n (a -> b) -> Tree n a -> Tree n b
(<*>) = ((a -> b) -> a -> b) -> Tree n (a -> b) -> Tree n a -> Tree n b
forall a b c (n :: Nat).
(a -> b -> c) -> Tree n a -> Tree n b -> Tree n c
zipWith (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
($)
    Tree n a
x <* :: Tree n a -> Tree n b -> Tree n a
<* Tree n b
_ = Tree n a
x
    Tree n a
_ *> :: Tree n a -> Tree n b -> Tree n b
*> Tree n b
x = Tree n b
x
#if MIN_VERSION_base(4,10,0)
    liftA2 :: (a -> b -> c) -> Tree n a -> Tree n b -> Tree n c
liftA2 = (a -> b -> c) -> Tree n a -> Tree n b -> Tree n c
forall a b c (n :: Nat).
(a -> b -> c) -> Tree n a -> Tree n b -> Tree n c
zipWith
#endif

-- TODO: Monad

#ifdef MIN_VERSION_distributive
instance N.SNatI n => I.Distributive (Tree n) where
    distribute :: f (Tree n a) -> Tree n (f a)
distribute f (Tree n a)
f = (Wrd n -> f a) -> Tree n (f a)
forall (n :: Nat) a. SNatI n => (Wrd n -> a) -> Tree n a
tabulate (\Wrd n
k -> (Tree n a -> a) -> f (Tree n a) -> f a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Tree n a -> Wrd n -> a
forall (n :: Nat) a. Tree n a -> Wrd n -> a
! Wrd n
k) f (Tree n a)
f)

#ifdef MIN_VERSION_adjunctions
instance N.SNatI n => I.Representable (Tree n) where
    type Rep (Tree n) = Wrd n

    tabulate :: (Rep (Tree n) -> a) -> Tree n a
tabulate = (Rep (Tree n) -> a) -> Tree n a
forall (n :: Nat) a. SNatI n => (Wrd n -> a) -> Tree n a
tabulate
    index :: Tree n a -> Rep (Tree n) -> a
index    = (!)
#endif
#endif

instance Semigroup a => Semigroup (Tree n a) where
    Leaf a
x   <> :: Tree n a -> Tree n a -> Tree n a
<> Leaf a
y   = a -> Tree 'Z a
forall a. a -> Tree 'Z a
Leaf (a
x a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
y)
    Node Tree n a
x Tree n a
y <> Node Tree n a
u Tree n a
v = Tree n a -> Tree n a -> Tree ('S n) a
forall (n :: Nat) a. Tree n a -> Tree n a -> Tree ('S n) a
Node (Tree n a
x Tree n a -> Tree n a -> Tree n a
forall a. Semigroup a => a -> a -> a
<> Tree n a
Tree n a
u) (Tree n a
y Tree n a -> Tree n a -> Tree n a
forall a. Semigroup a => a -> a -> a
<> Tree n a
Tree n a
v)

#ifdef MIN_VERSION_semigroupoids
instance Apply (Tree n) where
    <.> :: Tree n (a -> b) -> Tree n a -> Tree n b
(<.>)  = ((a -> b) -> a -> b) -> Tree n (a -> b) -> Tree n a -> Tree n b
forall a b c (n :: Nat).
(a -> b -> c) -> Tree n a -> Tree n b -> Tree n c
zipWith (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
($)
    Tree n a
_ .> :: Tree n a -> Tree n b -> Tree n b
.> Tree n b
x = Tree n b
x
    Tree n a
x <. :: Tree n a -> Tree n b -> Tree n a
<. Tree n b
_ = Tree n a
x
    liftF2 :: (a -> b -> c) -> Tree n a -> Tree n b -> Tree n c
liftF2 = (a -> b -> c) -> Tree n a -> Tree n b -> Tree n c
forall a b c (n :: Nat).
(a -> b -> c) -> Tree n a -> Tree n b -> Tree n c
zipWith
#endif

-------------------------------------------------------------------------------
-- Construction
-------------------------------------------------------------------------------

-- | 'Tree' of zero depth, with single element.
--
-- >>> singleton True
-- Leaf True
singleton :: a -> Tree 'Z a
singleton :: a -> Tree 'Z a
singleton = a -> Tree 'Z a
forall a. a -> Tree 'Z a
Leaf

-------------------------------------------------------------------------------
-- Conversions
-------------------------------------------------------------------------------

-- | Convert 'Tree' to list.
--
-- >>> toList $ Node (Node (Leaf 'a') (Leaf 'b')) (Node (Leaf 'c') (Leaf 'd'))
-- "abcd"
toList :: Tree n a -> [a]
toList :: Tree n a -> [a]
toList Tree n a
t = Tree n a -> [a] -> [a]
forall (n :: Nat) a. Tree n a -> [a] -> [a]
go Tree n a
t [] where
    go :: Tree n a -> [a] -> [a]
    go :: Tree n a -> [a] -> [a]
go (Leaf a
x) = (a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
:)
    go (Node Tree n a
x Tree n a
y) = Tree n a -> [a] -> [a]
forall (n :: Nat) a. Tree n a -> [a] -> [a]
go Tree n a
x ([a] -> [a]) -> ([a] -> [a]) -> [a] -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tree n a -> [a] -> [a]
forall (n :: Nat) a. Tree n a -> [a] -> [a]
go Tree n a
y

-------------------------------------------------------------------------------
-- Indexing
-------------------------------------------------------------------------------

-- | Indexing.
(!) :: Tree n a -> Wrd n -> a
(!) (Leaf a
x)   Wrd n
WE      = a
x
(!) (Node Tree n a
x Tree n a
_) (W0 Wrd n1
is) = Tree n a
x Tree n a -> Wrd n -> a
forall (n :: Nat) a. Tree n a -> Wrd n -> a
! Wrd n
Wrd n1
is
(!) (Node Tree n a
_ Tree n a
y) (W1 Wrd n1
is) = Tree n a
y Tree n a -> Wrd n -> a
forall (n :: Nat) a. Tree n a -> Wrd n -> a
! Wrd n
Wrd n1
is

tabulate :: forall n a. N.SNatI n => (Wrd n -> a) -> Tree n a
tabulate :: (Wrd n -> a) -> Tree n a
tabulate Wrd n -> a
f = case SNat n
forall (n :: Nat). SNatI n => SNat n
N.snat :: N.SNat n of
    SNat n
N.SZ -> a -> Tree 'Z a
forall a. a -> Tree 'Z a
Leaf (Wrd n -> a
f Wrd n
Wrd 'Z
WE)
    SNat n
N.SS -> Tree n1 a -> Tree n1 a -> Tree ('S n1) a
forall (n :: Nat) a. Tree n a -> Tree n a -> Tree ('S n) a
Node ((Wrd n1 -> a) -> Tree n1 a
forall (n :: Nat) a. SNatI n => (Wrd n -> a) -> Tree n a
tabulate ((Wrd ('S n1) -> a) -> Wrd n1 -> a
forall (n :: Nat) a. (Wrd ('S n) -> a) -> Wrd n -> a
goLeft Wrd n -> a
Wrd ('S n1) -> a
f)) ((Wrd n1 -> a) -> Tree n1 a
forall (n :: Nat) a. SNatI n => (Wrd n -> a) -> Tree n a
tabulate ((Wrd ('S n1) -> a) -> Wrd n1 -> a
forall (n :: Nat) a. (Wrd ('S n) -> a) -> Wrd n -> a
goRight Wrd n -> a
Wrd ('S n1) -> a
f))

leftmost :: Tree n a -> a
leftmost :: Tree n a -> a
leftmost (Leaf a
a)   = a
a
leftmost (Node Tree n a
x Tree n a
_) = Tree n a -> a
forall (n :: Nat) a. Tree n a -> a
leftmost Tree n a
x

rightmost :: Tree n a -> a
rightmost :: Tree n a -> a
rightmost (Leaf a
a)   = a
a
rightmost (Node Tree n a
_ Tree n a
y) = Tree n a -> a
forall (n :: Nat) a. Tree n a -> a
rightmost Tree n a
y

-------------------------------------------------------------------------------
-- Reverse
-------------------------------------------------------------------------------

-- | Reverse 'Tree'.
--
-- >>> let t = Node (Node (Leaf 'a') (Leaf 'b')) (Node (Leaf 'c') (Leaf 'd'))
-- >>> reverse t
-- Node (Node (Leaf 'd') (Leaf 'c')) (Node (Leaf 'b') (Leaf 'a'))
--
-- @since 0.1.1
reverse :: Tree n a -> Tree n a
reverse :: Tree n a -> Tree n a
reverse t :: Tree n a
t@(Leaf a
_) = Tree n a
t
reverse (Node Tree n a
x Tree n a
y) = Tree n a -> Tree n a -> Tree ('S n) a
forall (n :: Nat) a. Tree n a -> Tree n a -> Tree ('S n) a
Node (Tree n a -> Tree n a
forall (n :: Nat) a. Tree n a -> Tree n a
reverse Tree n a
y) (Tree n a -> Tree n a
forall (n :: Nat) a. Tree n a -> Tree n a
reverse Tree n a
x)

-------------------------------------------------------------------------------
-- Folds
-------------------------------------------------------------------------------

foldMap :: Monoid m => (a -> m) -> Tree n a -> m
foldMap :: (a -> m) -> Tree n a -> m
foldMap a -> m
f (Leaf a
x)   = a -> m
f a
x
foldMap a -> m
f (Node Tree n a
x Tree n a
y) = m -> m -> m
forall a. Monoid a => a -> a -> a
mappend ((a -> m) -> Tree n a -> m
forall m a (n :: Nat). Monoid m => (a -> m) -> Tree n a -> m
foldMap a -> m
f Tree n a
x) ((a -> m) -> Tree n a -> m
forall m a (n :: Nat). Monoid m => (a -> m) -> Tree n a -> m
foldMap a -> m
f Tree n a
y)

ifoldMap :: Monoid m => (Wrd n -> a -> m) -> Tree n a -> m
ifoldMap :: (Wrd n -> a -> m) -> Tree n a -> m
ifoldMap Wrd n -> a -> m
f (Leaf a
x)   = Wrd n -> a -> m
f Wrd n
Wrd 'Z
WE a
x
ifoldMap Wrd n -> a -> m
f (Node Tree n a
x Tree n a
y) = m -> m -> m
forall a. Monoid a => a -> a -> a
mappend ((Wrd n -> a -> m) -> Tree n a -> m
forall m (n :: Nat) a.
Monoid m =>
(Wrd n -> a -> m) -> Tree n a -> m
ifoldMap ((Wrd ('S n) -> a -> m) -> Wrd n -> a -> m
forall (n :: Nat) a. (Wrd ('S n) -> a) -> Wrd n -> a
goLeft Wrd n -> a -> m
Wrd ('S n) -> a -> m
f) Tree n a
x) ((Wrd n -> a -> m) -> Tree n a -> m
forall m (n :: Nat) a.
Monoid m =>
(Wrd n -> a -> m) -> Tree n a -> m
ifoldMap ((Wrd ('S n) -> a -> m) -> Wrd n -> a -> m
forall (n :: Nat) a. (Wrd ('S n) -> a) -> Wrd n -> a
goRight Wrd n -> a -> m
Wrd ('S n) -> a -> m
f) Tree n a
y)

foldMap1 :: Semigroup s => (a -> s) -> Tree n a -> s
foldMap1 :: (a -> s) -> Tree n a -> s
foldMap1 a -> s
f (Leaf a
x)   = a -> s
f a
x
foldMap1 a -> s
f (Node Tree n a
x Tree n a
y) = (a -> s) -> Tree n a -> s
forall s a (n :: Nat). Semigroup s => (a -> s) -> Tree n a -> s
foldMap1 a -> s
f Tree n a
x s -> s -> s
forall a. Semigroup a => a -> a -> a
<> (a -> s) -> Tree n a -> s
forall s a (n :: Nat). Semigroup s => (a -> s) -> Tree n a -> s
foldMap1 a -> s
f Tree n a
y

ifoldMap1 :: Semigroup s => (Wrd n -> a -> s) -> Tree n a -> s
ifoldMap1 :: (Wrd n -> a -> s) -> Tree n a -> s
ifoldMap1 Wrd n -> a -> s
f (Leaf a
x)   = Wrd n -> a -> s
f Wrd n
Wrd 'Z
WE a
x
ifoldMap1 Wrd n -> a -> s
f (Node Tree n a
x Tree n a
y) = (Wrd n -> a -> s) -> Tree n a -> s
forall s (n :: Nat) a.
Semigroup s =>
(Wrd n -> a -> s) -> Tree n a -> s
ifoldMap1 ((Wrd ('S n) -> a -> s) -> Wrd n -> a -> s
forall (n :: Nat) a. (Wrd ('S n) -> a) -> Wrd n -> a
goLeft Wrd n -> a -> s
Wrd ('S n) -> a -> s
f) Tree n a
x s -> s -> s
forall a. Semigroup a => a -> a -> a
<> (Wrd n -> a -> s) -> Tree n a -> s
forall s (n :: Nat) a.
Semigroup s =>
(Wrd n -> a -> s) -> Tree n a -> s
ifoldMap1 ((Wrd ('S n) -> a -> s) -> Wrd n -> a -> s
forall (n :: Nat) a. (Wrd ('S n) -> a) -> Wrd n -> a
goRight Wrd n -> a -> s
Wrd ('S n) -> a -> s
f) Tree n a
y

-- | >>> foldr (:) [] $ Node (Leaf True) (Leaf False)
-- [True,False]
foldr :: (a -> b -> b) -> b -> Tree n a -> b
foldr :: (a -> b -> b) -> b -> Tree n a -> b
foldr a -> b -> b
f b
z (Leaf a
x)   = a -> b -> b
f a
x b
z
foldr a -> b -> b
f b
z (Node Tree n a
x Tree n a
y) = (a -> b -> b) -> b -> Tree n a -> b
forall a b (n :: Nat). (a -> b -> b) -> b -> Tree n a -> b
foldr a -> b -> b
f ((a -> b -> b) -> b -> Tree n a -> b
forall a b (n :: Nat). (a -> b -> b) -> b -> Tree n a -> b
foldr a -> b -> b
f b
z Tree n a
y) Tree n a
x

ifoldr :: (Wrd n -> a -> b -> b) -> b -> Tree n a -> b
ifoldr :: (Wrd n -> a -> b -> b) -> b -> Tree n a -> b
ifoldr Wrd n -> a -> b -> b
f b
z (Leaf a
x)   = Wrd n -> a -> b -> b
f Wrd n
Wrd 'Z
WE a
x b
z
ifoldr Wrd n -> a -> b -> b
f b
z (Node Tree n a
x Tree n a
y) = (Wrd n -> a -> b -> b) -> b -> Tree n a -> b
forall (n :: Nat) a b. (Wrd n -> a -> b -> b) -> b -> Tree n a -> b
ifoldr ((Wrd ('S n) -> a -> b -> b) -> Wrd n -> a -> b -> b
forall (n :: Nat) a. (Wrd ('S n) -> a) -> Wrd n -> a
goLeft Wrd n -> a -> b -> b
Wrd ('S n) -> a -> b -> b
f) ((Wrd n -> a -> b -> b) -> b -> Tree n a -> b
forall (n :: Nat) a b. (Wrd n -> a -> b -> b) -> b -> Tree n a -> b
ifoldr ((Wrd ('S n) -> a -> b -> b) -> Wrd n -> a -> b -> b
forall (n :: Nat) a. (Wrd ('S n) -> a) -> Wrd n -> a
goRight Wrd n -> a -> b -> b
Wrd ('S n) -> a -> b -> b
f) b
z Tree n a
y) Tree n a
x

foldr1Map :: (a -> b -> b) -> (a -> b) -> Tree n a -> b
foldr1Map :: (a -> b -> b) -> (a -> b) -> Tree n a -> b
foldr1Map a -> b -> b
_ a -> b
z (Leaf a
x)   = a -> b
z a
x
foldr1Map a -> b -> b
f a -> b
z (Node Tree n a
x Tree n a
y) = (a -> b -> b) -> b -> Tree n a -> b
forall a b (n :: Nat). (a -> b -> b) -> b -> Tree n a -> b
foldr a -> b -> b
f ((a -> b -> b) -> (a -> b) -> Tree n a -> b
forall a b (n :: Nat). (a -> b -> b) -> (a -> b) -> Tree n a -> b
foldr1Map a -> b -> b
f a -> b
z Tree n a
y) Tree n a
x

ifoldr1Map :: (Wrd n -> a -> b -> b) -> (Wrd n -> a -> b) -> Tree n a -> b
ifoldr1Map :: (Wrd n -> a -> b -> b) -> (Wrd n -> a -> b) -> Tree n a -> b
ifoldr1Map Wrd n -> a -> b -> b
_ Wrd n -> a -> b
z (Leaf a
x) = Wrd n -> a -> b
z Wrd n
Wrd 'Z
WE a
x
ifoldr1Map Wrd n -> a -> b -> b
f Wrd n -> a -> b
z (Node Tree n a
x Tree n a
y) = (Wrd n -> a -> b -> b) -> b -> Tree n a -> b
forall (n :: Nat) a b. (Wrd n -> a -> b -> b) -> b -> Tree n a -> b
ifoldr ((Wrd ('S n) -> a -> b -> b) -> Wrd n -> a -> b -> b
forall (n :: Nat) a. (Wrd ('S n) -> a) -> Wrd n -> a
goLeft Wrd n -> a -> b -> b
Wrd ('S n) -> a -> b -> b
f) ((Wrd n -> a -> b -> b) -> (Wrd n -> a -> b) -> Tree n a -> b
forall (n :: Nat) a b.
(Wrd n -> a -> b -> b) -> (Wrd n -> a -> b) -> Tree n a -> b
ifoldr1Map ((Wrd ('S n) -> a -> b -> b) -> Wrd n -> a -> b -> b
forall (n :: Nat) a. (Wrd ('S n) -> a) -> Wrd n -> a
goRight Wrd n -> a -> b -> b
Wrd ('S n) -> a -> b -> b
f) ((Wrd ('S n) -> a -> b) -> Wrd n -> a -> b
forall (n :: Nat) a. (Wrd ('S n) -> a) -> Wrd n -> a
goRight Wrd n -> a -> b
Wrd ('S n) -> a -> b
z) Tree n a
y) Tree n a
x

-- | >>> foldl (flip (:)) [] $ Node (Leaf True) (Leaf False)
-- [False,True]
foldl :: (b -> a -> b) -> b -> Tree n a -> b
foldl :: (b -> a -> b) -> b -> Tree n a -> b
foldl b -> a -> b
f b
z (Leaf a
x) = b -> a -> b
f b
z a
x
foldl b -> a -> b
f b
z (Node Tree n a
x Tree n a
y) = (b -> a -> b) -> b -> Tree n a -> b
forall b a (n :: Nat). (b -> a -> b) -> b -> Tree n a -> b
foldl b -> a -> b
f ((b -> a -> b) -> b -> Tree n a -> b
forall b a (n :: Nat). (b -> a -> b) -> b -> Tree n a -> b
foldl b -> a -> b
f b
z Tree n a
x) Tree n a
y

ifoldl :: (Wrd n -> b -> a -> b) -> b -> Tree n a -> b
ifoldl :: (Wrd n -> b -> a -> b) -> b -> Tree n a -> b
ifoldl Wrd n -> b -> a -> b
f b
z (Leaf a
x)   = Wrd n -> b -> a -> b
f Wrd n
Wrd 'Z
WE b
z a
x
ifoldl Wrd n -> b -> a -> b
f b
z (Node Tree n a
x Tree n a
y) = (Wrd n -> b -> a -> b) -> b -> Tree n a -> b
forall (n :: Nat) b a. (Wrd n -> b -> a -> b) -> b -> Tree n a -> b
ifoldl ((Wrd ('S n) -> b -> a -> b) -> Wrd n -> b -> a -> b
forall (n :: Nat) a. (Wrd ('S n) -> a) -> Wrd n -> a
goLeft Wrd n -> b -> a -> b
Wrd ('S n) -> b -> a -> b
f) ((Wrd n -> b -> a -> b) -> b -> Tree n a -> b
forall (n :: Nat) b a. (Wrd n -> b -> a -> b) -> b -> Tree n a -> b
ifoldl ((Wrd ('S n) -> b -> a -> b) -> Wrd n -> b -> a -> b
forall (n :: Nat) a. (Wrd ('S n) -> a) -> Wrd n -> a
goRight Wrd n -> b -> a -> b
Wrd ('S n) -> b -> a -> b
f) b
z Tree n a
x) Tree n a
y

-------------------------------------------------------------------------------
-- Special folds
-------------------------------------------------------------------------------

-- | @since 0.1.1
null :: Tree n a -> Bool
null :: Tree n a -> Bool
null Tree n a
_ = Bool
False

-- | >>> length (universe :: Tree N.Nat3 (Wrd N.Nat3))
-- 8
--
length :: Tree n a -> Int
length :: Tree n a -> Int
length = Int -> Tree n a -> Int
forall (n :: Nat) a. Int -> Tree n a -> Int
go Int
1 where
    go :: Int -> Tree n a -> Int
    go :: Int -> Tree n a -> Int
go !Int
acc (Leaf a
_)   = Int
acc
    go  Int
acc (Node Tree n a
x Tree n a
_) = Int -> Tree n a -> Int
forall (n :: Nat) a. Int -> Tree n a -> Int
go (Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
acc) Tree n a
x

-- | Non-strict 'sum'.
--
-- @since 0.1.1
sum :: Num a => Tree n a -> a
sum :: Tree n a -> a
sum (Leaf a
a)   = a
a
sum (Node Tree n a
x Tree n a
y) = Tree n a -> a
forall a (n :: Nat). Num a => Tree n a -> a
sum Tree n a
x a -> a -> a
forall a. Num a => a -> a -> a
+ Tree n a -> a
forall a (n :: Nat). Num a => Tree n a -> a
sum Tree n a
y

-- | Non-strict 'product'.
--
-- @since 0.1.1
product :: Num a => Tree n a -> a
product :: Tree n a -> a
product (Leaf a
a)   = a
a
product (Node Tree n a
x Tree n a
y) = Tree n a -> a
forall a (n :: Nat). Num a => Tree n a -> a
product Tree n a
x a -> a -> a
forall a. Num a => a -> a -> a
* Tree n a -> a
forall a (n :: Nat). Num a => Tree n a -> a
product Tree n a
y

-------------------------------------------------------------------------------
-- Mapping
-------------------------------------------------------------------------------

-- | >>> map not $ Node (Leaf True) (Leaf False)
-- Node (Leaf False) (Leaf True)
map :: (a -> b) -> Tree n a -> Tree n b
map :: (a -> b) -> Tree n a -> Tree n b
map a -> b
f (Leaf a
x)   = b -> Tree 'Z b
forall a. a -> Tree 'Z a
Leaf (a -> b
f a
x)
map a -> b
f (Node Tree n a
x Tree n a
y) = Tree n b -> Tree n b -> Tree ('S n) b
forall (n :: Nat) a. Tree n a -> Tree n a -> Tree ('S n) a
Node ((a -> b) -> Tree n a -> Tree n b
forall a b (n :: Nat). (a -> b) -> Tree n a -> Tree n b
map a -> b
f Tree n a
x) ((a -> b) -> Tree n a -> Tree n b
forall a b (n :: Nat). (a -> b) -> Tree n a -> Tree n b
map a -> b
f Tree n a
y)

-- | >>> imap (,) $ Node (Leaf True) (Leaf False)
-- Node (Leaf (0b0,True)) (Leaf (0b1,False))
imap :: (Wrd n -> a -> b) -> Tree n a -> Tree n b
imap :: (Wrd n -> a -> b) -> Tree n a -> Tree n b
imap Wrd n -> a -> b
f (Leaf a
x) = b -> Tree 'Z b
forall a. a -> Tree 'Z a
Leaf (Wrd n -> a -> b
f Wrd n
Wrd 'Z
WE a
x)
imap Wrd n -> a -> b
f (Node Tree n a
x Tree n a
y) = Tree n b -> Tree n b -> Tree ('S n) b
forall (n :: Nat) a. Tree n a -> Tree n a -> Tree ('S n) a
Node ((Wrd n -> a -> b) -> Tree n a -> Tree n b
forall (n :: Nat) a b. (Wrd n -> a -> b) -> Tree n a -> Tree n b
imap ((Wrd ('S n) -> a -> b) -> Wrd n -> a -> b
forall (n :: Nat) a. (Wrd ('S n) -> a) -> Wrd n -> a
goLeft Wrd n -> a -> b
Wrd ('S n) -> a -> b
f) Tree n a
x) ((Wrd n -> a -> b) -> Tree n a -> Tree n b
forall (n :: Nat) a b. (Wrd n -> a -> b) -> Tree n a -> Tree n b
imap ((Wrd ('S n) -> a -> b) -> Wrd n -> a -> b
forall (n :: Nat) a. (Wrd ('S n) -> a) -> Wrd n -> a
goRight Wrd n -> a -> b
Wrd ('S n) -> a -> b
f) Tree n a
y)

traverse :: Applicative f => (a -> f b) -> Tree n a -> f (Tree n b)
traverse :: (a -> f b) -> Tree n a -> f (Tree n b)
traverse a -> f b
f (Leaf a
x)   = b -> Tree 'Z b
forall a. a -> Tree 'Z a
Leaf (b -> Tree 'Z b) -> f b -> f (Tree 'Z b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f b
f a
x
traverse a -> f b
f (Node Tree n a
x Tree n a
y) = Tree n b -> Tree n b -> Tree ('S n) b
forall (n :: Nat) a. Tree n a -> Tree n a -> Tree ('S n) a
Node (Tree n b -> Tree n b -> Tree ('S n) b)
-> f (Tree n b) -> f (Tree n b -> Tree ('S n) b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> f b) -> Tree n a -> f (Tree n b)
forall (f :: * -> *) a b (n :: Nat).
Applicative f =>
(a -> f b) -> Tree n a -> f (Tree n b)
traverse a -> f b
f Tree n a
x f (Tree n b -> Tree ('S n) b) -> f (Tree n b) -> f (Tree ('S n) b)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (a -> f b) -> Tree n a -> f (Tree n b)
forall (f :: * -> *) a b (n :: Nat).
Applicative f =>
(a -> f b) -> Tree n a -> f (Tree n b)
traverse a -> f b
f Tree n a
y

itraverse :: Applicative f => (Wrd n -> a -> f b) -> Tree n a -> f (Tree n b)
itraverse :: (Wrd n -> a -> f b) -> Tree n a -> f (Tree n b)
itraverse Wrd n -> a -> f b
f (Leaf a
x)   = b -> Tree 'Z b
forall a. a -> Tree 'Z a
Leaf (b -> Tree 'Z b) -> f b -> f (Tree 'Z b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Wrd n -> a -> f b
f Wrd n
Wrd 'Z
WE a
x
itraverse Wrd n -> a -> f b
f (Node Tree n a
x Tree n a
y) = Tree n b -> Tree n b -> Tree ('S n) b
forall (n :: Nat) a. Tree n a -> Tree n a -> Tree ('S n) a
Node (Tree n b -> Tree n b -> Tree ('S n) b)
-> f (Tree n b) -> f (Tree n b -> Tree ('S n) b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Wrd n -> a -> f b) -> Tree n a -> f (Tree n b)
forall (f :: * -> *) (n :: Nat) a b.
Applicative f =>
(Wrd n -> a -> f b) -> Tree n a -> f (Tree n b)
itraverse ((Wrd ('S n) -> a -> f b) -> Wrd n -> a -> f b
forall (n :: Nat) a. (Wrd ('S n) -> a) -> Wrd n -> a
goLeft Wrd n -> a -> f b
Wrd ('S n) -> a -> f b
f) Tree n a
x f (Tree n b -> Tree ('S n) b) -> f (Tree n b) -> f (Tree ('S n) b)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Wrd n -> a -> f b) -> Tree n a -> f (Tree n b)
forall (f :: * -> *) (n :: Nat) a b.
Applicative f =>
(Wrd n -> a -> f b) -> Tree n a -> f (Tree n b)
itraverse ((Wrd ('S n) -> a -> f b) -> Wrd n -> a -> f b
forall (n :: Nat) a. (Wrd ('S n) -> a) -> Wrd n -> a
goRight Wrd n -> a -> f b
Wrd ('S n) -> a -> f b
f) Tree n a
y

#ifdef MIN_VERSION_semigroupoids
traverse1 :: Apply f => (a -> f b) -> Tree n a -> f (Tree n b)
traverse1 :: (a -> f b) -> Tree n a -> f (Tree n b)
traverse1 a -> f b
f (Leaf a
x)   = b -> Tree 'Z b
forall a. a -> Tree 'Z a
Leaf (b -> Tree 'Z b) -> f b -> f (Tree 'Z b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f b
f a
x
traverse1 a -> f b
f (Node Tree n a
x Tree n a
y) = Tree n b -> Tree n b -> Tree ('S n) b
forall (n :: Nat) a. Tree n a -> Tree n a -> Tree ('S n) a
Node (Tree n b -> Tree n b -> Tree ('S n) b)
-> f (Tree n b) -> f (Tree n b -> Tree ('S n) b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> f b) -> Tree n a -> f (Tree n b)
forall (f :: * -> *) a b (n :: Nat).
Apply f =>
(a -> f b) -> Tree n a -> f (Tree n b)
traverse1 a -> f b
f Tree n a
x f (Tree n b -> Tree ('S n) b) -> f (Tree n b) -> f (Tree ('S n) b)
forall (f :: * -> *) a b. Apply f => f (a -> b) -> f a -> f b
<.> (a -> f b) -> Tree n a -> f (Tree n b)
forall (f :: * -> *) a b (n :: Nat).
Apply f =>
(a -> f b) -> Tree n a -> f (Tree n b)
traverse1 a -> f b
f Tree n a
y

itraverse1 :: Apply f => (Wrd n -> a -> f b) -> Tree n a -> f (Tree n b)
itraverse1 :: (Wrd n -> a -> f b) -> Tree n a -> f (Tree n b)
itraverse1 Wrd n -> a -> f b
f (Leaf a
x)   = b -> Tree 'Z b
forall a. a -> Tree 'Z a
Leaf (b -> Tree 'Z b) -> f b -> f (Tree 'Z b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Wrd n -> a -> f b
f Wrd n
Wrd 'Z
WE a
x
itraverse1 Wrd n -> a -> f b
f (Node Tree n a
x Tree n a
y) = Tree n b -> Tree n b -> Tree ('S n) b
forall (n :: Nat) a. Tree n a -> Tree n a -> Tree ('S n) a
Node (Tree n b -> Tree n b -> Tree ('S n) b)
-> f (Tree n b) -> f (Tree n b -> Tree ('S n) b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Wrd n -> a -> f b) -> Tree n a -> f (Tree n b)
forall (f :: * -> *) (n :: Nat) a b.
Apply f =>
(Wrd n -> a -> f b) -> Tree n a -> f (Tree n b)
itraverse1 ((Wrd ('S n) -> a -> f b) -> Wrd n -> a -> f b
forall (n :: Nat) a. (Wrd ('S n) -> a) -> Wrd n -> a
goLeft Wrd n -> a -> f b
Wrd ('S n) -> a -> f b
f) Tree n a
x f (Tree n b -> Tree ('S n) b) -> f (Tree n b) -> f (Tree ('S n) b)
forall (f :: * -> *) a b. Apply f => f (a -> b) -> f a -> f b
<.> (Wrd n -> a -> f b) -> Tree n a -> f (Tree n b)
forall (f :: * -> *) (n :: Nat) a b.
Apply f =>
(Wrd n -> a -> f b) -> Tree n a -> f (Tree n b)
itraverse1 ((Wrd ('S n) -> a -> f b) -> Wrd n -> a -> f b
forall (n :: Nat) a. (Wrd ('S n) -> a) -> Wrd n -> a
goRight Wrd n -> a -> f b
Wrd ('S n) -> a -> f b
f) Tree n a
y
#endif

-- |
-- @since 0.1.1
itraverse_ :: forall n f a b. Applicative f => (Wrd n -> a -> f b) -> Tree n a -> f ()
itraverse_ :: (Wrd n -> a -> f b) -> Tree n a -> f ()
itraverse_ Wrd n -> a -> f b
f (Leaf a
x)   = f b -> f ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Wrd n -> a -> f b
f Wrd n
Wrd 'Z
WE a
x)
itraverse_ Wrd n -> a -> f b
f (Node Tree n a
x Tree n a
y) = (Wrd n -> a -> f b) -> Tree n a -> f ()
forall (n :: Nat) (f :: * -> *) a b.
Applicative f =>
(Wrd n -> a -> f b) -> Tree n a -> f ()
itraverse_ (Wrd n -> a -> f b
f (Wrd n -> a -> f b) -> (Wrd n -> Wrd n) -> Wrd n -> a -> f b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrd n -> Wrd n
forall (n1 :: Nat). Wrd n1 -> Wrd ('S n1)
W0) Tree n a
x f () -> f () -> f ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Wrd n -> a -> f b) -> Tree n a -> f ()
forall (n :: Nat) (f :: * -> *) a b.
Applicative f =>
(Wrd n -> a -> f b) -> Tree n a -> f ()
itraverse_ (Wrd n -> a -> f b
f (Wrd n -> a -> f b) -> (Wrd n -> Wrd n) -> Wrd n -> a -> f b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrd n -> Wrd n
forall (n1 :: Nat). Wrd n1 -> Wrd ('S n1)
W1) Tree n a
y

-------------------------------------------------------------------------------
-- Zipping
-------------------------------------------------------------------------------

-- | Zip two 'Vec's with a function.
zipWith ::  (a -> b -> c) -> Tree n a -> Tree n b -> Tree n c
zipWith :: (a -> b -> c) -> Tree n a -> Tree n b -> Tree n c
zipWith a -> b -> c
f (Leaf a
x)   (Leaf b
y)   = c -> Tree 'Z c
forall a. a -> Tree 'Z a
Leaf (a -> b -> c
f a
x b
y)
zipWith a -> b -> c
f (Node Tree n a
x Tree n a
y) (Node Tree n b
u Tree n b
v) = Tree n c -> Tree n c -> Tree ('S n) c
forall (n :: Nat) a. Tree n a -> Tree n a -> Tree ('S n) a
Node ((a -> b -> c) -> Tree n a -> Tree n b -> Tree n c
forall a b c (n :: Nat).
(a -> b -> c) -> Tree n a -> Tree n b -> Tree n c
zipWith a -> b -> c
f Tree n a
x Tree n b
Tree n b
u) ((a -> b -> c) -> Tree n a -> Tree n b -> Tree n c
forall a b c (n :: Nat).
(a -> b -> c) -> Tree n a -> Tree n b -> Tree n c
zipWith a -> b -> c
f Tree n a
y Tree n b
Tree n b
v)

-- | Zip two 'Tree's. with a function that also takes the elements' indices.
izipWith :: (Wrd n -> a -> b -> c) -> Tree n a -> Tree n b -> Tree n c
izipWith :: (Wrd n -> a -> b -> c) -> Tree n a -> Tree n b -> Tree n c
izipWith Wrd n -> a -> b -> c
f (Leaf a
x)   (Leaf b
y)   = c -> Tree 'Z c
forall a. a -> Tree 'Z a
Leaf (Wrd n -> a -> b -> c
f Wrd n
Wrd 'Z
WE a
x b
y)
izipWith Wrd n -> a -> b -> c
f (Node Tree n a
x Tree n a
y) (Node Tree n b
u Tree n b
v) = Tree n c -> Tree n c -> Tree ('S n) c
forall (n :: Nat) a. Tree n a -> Tree n a -> Tree ('S n) a
Node ((Wrd n -> a -> b -> c) -> Tree n a -> Tree n b -> Tree n c
forall (n :: Nat) a b c.
(Wrd n -> a -> b -> c) -> Tree n a -> Tree n b -> Tree n c
izipWith ((Wrd ('S n) -> a -> b -> c) -> Wrd n -> a -> b -> c
forall (n :: Nat) a. (Wrd ('S n) -> a) -> Wrd n -> a
goLeft Wrd n -> a -> b -> c
Wrd ('S n) -> a -> b -> c
f) Tree n a
x Tree n b
Tree n b
u) ((Wrd n -> a -> b -> c) -> Tree n a -> Tree n b -> Tree n c
forall (n :: Nat) a b c.
(Wrd n -> a -> b -> c) -> Tree n a -> Tree n b -> Tree n c
izipWith ((Wrd ('S n) -> a -> b -> c) -> Wrd n -> a -> b -> c
forall (n :: Nat) a. (Wrd ('S n) -> a) -> Wrd n -> a
goRight Wrd n -> a -> b -> c
Wrd ('S n) -> a -> b -> c
f) Tree n a
y Tree n b
Tree n b
v)

-- | Repeat a value.
--
-- >>> repeat 'x' :: Tree N.Nat2 Char
-- Node (Node (Leaf 'x') (Leaf 'x')) (Node (Leaf 'x') (Leaf 'x'))
--
repeat :: N.SNatI n => a -> Tree n a
repeat :: a -> Tree n a
repeat a
x = Tree 'Z a
-> (forall (m :: Nat). SNatI m => Tree m a -> Tree ('S m) a)
-> Tree n a
forall (n :: Nat) (f :: Nat -> * -> *) a.
SNatI n =>
f 'Z a
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a) -> f n a
N.induction1 (a -> Tree 'Z a
forall a. a -> Tree 'Z a
Leaf a
x) (\Tree m a
t -> Tree m a -> Tree m a -> Tree ('S m) a
forall (n :: Nat) a. Tree n a -> Tree n a -> Tree ('S n) a
Node Tree m a
t Tree m a
t)

-------------------------------------------------------------------------------
-- Universe
-------------------------------------------------------------------------------

-- | Get all @'Vec' n 'Bool'@ indices in @'Tree' n@.
--
-- >>> universe :: Tree N.Nat2 (Wrd N.Nat2)
-- Node (Node (Leaf 0b00) (Leaf 0b01)) (Node (Leaf 0b10) (Leaf 0b11))
--
universe :: N.SNatI n => Tree n (Wrd n)
universe :: Tree n (Wrd n)
universe = (Wrd n -> Wrd n) -> Tree n (Wrd n)
forall (n :: Nat) a. SNatI n => (Wrd n -> a) -> Tree n a
tabulate Wrd n -> Wrd n
forall a. a -> a
id

-------------------------------------------------------------------------------
-- QuickCheck
-------------------------------------------------------------------------------

instance N.SNatI n => QC.Arbitrary1 (Tree n) where
    liftArbitrary :: Gen a -> Gen (Tree n a)
liftArbitrary = Gen a -> Gen (Tree n a)
forall (n :: Nat) a. SNatI n => Gen a -> Gen (Tree n a)
liftArbitrary
    liftShrink :: (a -> [a]) -> Tree n a -> [Tree n a]
liftShrink    = (a -> [a]) -> Tree n a -> [Tree n a]
forall (n :: Nat) a. (a -> [a]) -> Tree n a -> [Tree n a]
liftShrink

liftArbitrary :: forall n a. N.SNatI n => QC.Gen a -> QC.Gen (Tree n a)
liftArbitrary :: Gen a -> Gen (Tree n a)
liftArbitrary Gen a
arb = Arb n a -> Gen (Tree n a)
forall (n :: Nat) a. Arb n a -> Gen (Tree n a)
getArb (Arb n a -> Gen (Tree n a)) -> Arb n a -> Gen (Tree n a)
forall a b. (a -> b) -> a -> b
$ Arb 'Z a
-> (forall (m :: Nat). SNatI m => Arb m a -> Arb ('S m) a)
-> Arb n a
forall (n :: Nat) (f :: Nat -> * -> *) a.
SNatI n =>
f 'Z a
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a) -> f n a
N.induction1 (Gen (Tree 'Z a) -> Arb 'Z a
forall (n :: Nat) a. Gen (Tree n a) -> Arb n a
Arb ((a -> Tree 'Z a) -> Gen a -> Gen (Tree 'Z a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Tree 'Z a
forall a. a -> Tree 'Z a
Leaf Gen a
arb)) forall (m :: Nat). SNatI m => Arb m a -> Arb ('S m) a
forall (m :: Nat). Arb m a -> Arb ('S m) a
step where
    step :: Arb m a -> Arb ('S m) a
    step :: Arb m a -> Arb ('S m) a
step (Arb Gen (Tree m a)
rec) = Gen (Tree ('S m) a) -> Arb ('S m) a
forall (n :: Nat) a. Gen (Tree n a) -> Arb n a
Arb (Gen (Tree ('S m) a) -> Arb ('S m) a)
-> Gen (Tree ('S m) a) -> Arb ('S m) a
forall a b. (a -> b) -> a -> b
$ Tree m a -> Tree m a -> Tree ('S m) a
forall (n :: Nat) a. Tree n a -> Tree n a -> Tree ('S n) a
Node (Tree m a -> Tree m a -> Tree ('S m) a)
-> Gen (Tree m a) -> Gen (Tree m a -> Tree ('S m) a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (Tree m a)
rec Gen (Tree m a -> Tree ('S m) a)
-> Gen (Tree m a) -> Gen (Tree ('S m) a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen (Tree m a)
rec

newtype Arb n a = Arb { Arb n a -> Gen (Tree n a)
getArb :: QC.Gen (Tree n a) }

liftShrink :: forall n a. (a -> [a]) -> Tree n a -> [Tree n a]
liftShrink :: (a -> [a]) -> Tree n a -> [Tree n a]
liftShrink a -> [a]
shr (Leaf a
x)   = a -> Tree 'Z a
forall a. a -> Tree 'Z a
Leaf (a -> Tree 'Z a) -> [a] -> [Tree 'Z a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> [a]
shr a
x
liftShrink a -> [a]
shr (Node Tree n a
l Tree n a
r) = (Tree n a -> Tree n a -> Tree ('S n) a)
-> (Tree n a, Tree n a) -> Tree ('S n) a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Tree n a -> Tree n a -> Tree ('S n) a
forall (n :: Nat) a. Tree n a -> Tree n a -> Tree ('S n) a
Node ((Tree n a, Tree n a) -> Tree ('S n) a)
-> [(Tree n a, Tree n a)] -> [Tree ('S n) a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Tree n a -> [Tree n a])
-> (Tree n a -> [Tree n a])
-> (Tree n a, Tree n a)
-> [(Tree n a, Tree n a)]
forall (f :: * -> * -> *) a b.
Arbitrary2 f =>
(a -> [a]) -> (b -> [b]) -> f a b -> [f a b]
QC.liftShrink2 Tree n a -> [Tree n a]
rec Tree n a -> [Tree n a]
rec (Tree n a
l, Tree n a
r) where
    rec :: Tree n a -> [Tree n a]
rec = (a -> [a]) -> Tree n a -> [Tree n a]
forall (n :: Nat) a. (a -> [a]) -> Tree n a -> [Tree n a]
liftShrink a -> [a]
shr

instance (N.SNatI n, QC.Arbitrary a) => QC.Arbitrary (Tree n a) where
    arbitrary :: Gen (Tree n a)
arbitrary = Gen (Tree n a)
forall (f :: * -> *) a. (Arbitrary1 f, Arbitrary a) => Gen (f a)
QC.arbitrary1
    shrink :: Tree n a -> [Tree n a]
shrink    = Tree n a -> [Tree n a]
forall (f :: * -> *) a. (Arbitrary1 f, Arbitrary a) => f a -> [f a]
QC.shrink1

instance QC.CoArbitrary a => QC.CoArbitrary (Tree n a) where
    coarbitrary :: Tree n a -> Gen b -> Gen b
coarbitrary (Leaf a
x)   = Int -> Gen b -> Gen b
forall n a. Integral n => n -> Gen a -> Gen a
QC.variant (Int
0 :: Int) (Gen b -> Gen b) -> (Gen b -> Gen b) -> Gen b -> Gen b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Gen b -> Gen b
forall a b. CoArbitrary a => a -> Gen b -> Gen b
QC.coarbitrary a
x
    coarbitrary (Node Tree n a
l Tree n a
r) = Int -> Gen b -> Gen b
forall n a. Integral n => n -> Gen a -> Gen a
QC.variant (Int
1 :: Int) (Gen b -> Gen b) -> (Gen b -> Gen b) -> Gen b -> Gen b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Tree n a, Tree n a) -> Gen b -> Gen b
forall a b. CoArbitrary a => a -> Gen b -> Gen b
QC.coarbitrary (Tree n a
l, Tree n a
r)

instance (N.SNatI n, QC.Function a) => QC.Function (Tree n a) where
    function :: (Tree n a -> b) -> Tree n a :-> b
function = case SNat n
forall (n :: Nat). SNatI n => SNat n
N.snat :: N.SNat n of
        SNat n
N.SZ -> (Tree 'Z a -> a)
-> (a -> Tree 'Z a) -> (Tree 'Z a -> b) -> Tree 'Z a :-> b
forall b a c.
Function b =>
(a -> b) -> (b -> a) -> (a -> c) -> a :-> c
QC.functionMap (\(Leaf a
x) -> a
x)         a -> Tree 'Z a
forall a. a -> Tree 'Z a
Leaf
        SNat n
N.SS -> (Tree ('S n1) a -> (Tree n1 a, Tree n1 a))
-> ((Tree n1 a, Tree n1 a) -> Tree ('S n1) a)
-> (Tree ('S n1) a -> b)
-> Tree ('S n1) a :-> b
forall b a c.
Function b =>
(a -> b) -> (b -> a) -> (a -> c) -> a :-> c
QC.functionMap (\(Node Tree n a
l Tree n a
r ) -> (Tree n a
l, Tree n a
r)) ((Tree n1 a -> Tree n1 a -> Tree ('S n1) a)
-> (Tree n1 a, Tree n1 a) -> Tree ('S n1) a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Tree n1 a -> Tree n1 a -> Tree ('S n1) a
forall (n :: Nat) a. Tree n a -> Tree n a -> Tree ('S n) a
Node)