{-# LANGUAGE CPP                    #-}
{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE DeriveDataTypeable     #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs                  #-}
{-# LANGUAGE RankNTypes             #-}
{-# LANGUAGE Safe                   #-}
{-# LANGUAGE ScopedTypeVariables    #-}
{-# LANGUAGE TypeFamilies           #-}
-- | Depth indexed perfect tree as data family.
module Data.RAVec.Tree.DF (
    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,

    -- * Ensure spine
    ensureSpine,
) where

import Prelude
       (Bool (..), Eq (..), Functor (..), Int, Num, Ord (..), Ordering (..),
       Show (..), ShowS, flip, id, seq, showChar, showParen, showString,
       uncurry, ($), (&&), (*), (+), (.))

import Control.Applicative (Applicative (..), liftA2, (<$>))
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.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.Foldable.WithIndex    as WI (FoldableWithIndex (..))
import qualified Data.Functor.WithIndex     as WI (FunctorWithIndex (..))
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, error, ($), Bool (..), id)
-- >>> import Data.Wrd (Wrd (..))
-- >>> import qualified Data.Type.Nat as N

-------------------------------------------------------------------------------
-- Types
-------------------------------------------------------------------------------

data family Tree (n :: Nat) a

newtype instance Tree 'Z     a = Leaf a
data instance    Tree ('S n) a = Node (Tree n a) (Tree n a)

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

instance (Eq a, N.SNatI n) => Eq (Tree n a) where
    == :: Tree n a -> Tree n a -> Bool
(==) = Equal n a -> Tree n a -> Tree n a -> Bool
forall (n :: Nat) a. Equal n a -> Tree n a -> Tree n a -> Bool
getEqual (Equal 'Z a
-> (forall (m :: Nat). SNatI m => Equal m a -> Equal ('S m) a)
-> Equal 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 Equal 'Z a
start Equal m a -> Equal ('S m) a
forall (m :: Nat). SNatI m => Equal m a -> Equal ('S m) a
forall (m :: Nat). Equal m a -> Equal ('S m) a
step) where
        start :: Equal 'Z a
        start :: Equal 'Z a
start = (Tree 'Z a -> Tree 'Z a -> Bool) -> Equal 'Z a
forall (n :: Nat) a. (Tree n a -> Tree n a -> Bool) -> Equal n a
Equal ((Tree 'Z a -> Tree 'Z a -> Bool) -> Equal 'Z a)
-> (Tree 'Z a -> Tree 'Z a -> Bool) -> Equal 'Z a
forall a b. (a -> b) -> a -> b
$ \(Leaf a
x) (Leaf a
y) -> a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y

        step :: Equal m a -> Equal ('S m) a
        step :: forall (m :: Nat). Equal m a -> Equal ('S m) a
step (Equal Tree m a -> Tree m a -> Bool
go) = (Tree ('S m) a -> Tree ('S m) a -> Bool) -> Equal ('S m) a
forall (n :: Nat) a. (Tree n a -> Tree n a -> Bool) -> Equal n a
Equal ((Tree ('S m) a -> Tree ('S m) a -> Bool) -> Equal ('S m) a)
-> (Tree ('S m) a -> Tree ('S m) a -> Bool) -> Equal ('S m) a
forall a b. (a -> b) -> a -> b
$ \(Node Tree m a
x1 Tree m a
y1) (Node Tree m a
x2 Tree m a
y2) ->
            Tree m a -> Tree m a -> Bool
go Tree m a
x1 Tree m a
x2 Bool -> Bool -> Bool
&& Tree m a -> Tree m a -> Bool
go Tree m a
y1 Tree m a
y2

newtype Equal n a = Equal { forall (n :: Nat) a. Equal n a -> Tree n a -> Tree n a -> Bool
getEqual :: Tree n a -> Tree n a -> Bool }

instance (Ord a, N.SNatI n) => Ord (Tree n a) where
    compare :: Tree n a -> Tree n a -> Ordering
compare = Compare n a -> Tree n a -> Tree n a -> Ordering
forall (n :: Nat) a.
Compare n a -> Tree n a -> Tree n a -> Ordering
getCompare (Compare 'Z a
-> (forall (m :: Nat). SNatI m => Compare m a -> Compare ('S m) a)
-> Compare 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 Compare 'Z a
start Compare m a -> Compare ('S m) a
forall (m :: Nat). SNatI m => Compare m a -> Compare ('S m) a
forall (m :: Nat). Compare m a -> Compare ('S m) a
step) where
        start :: Compare 'Z a
        start :: Compare 'Z a
start = (Tree 'Z a -> Tree 'Z a -> Ordering) -> Compare 'Z a
forall (n :: Nat) a.
(Tree n a -> Tree n a -> Ordering) -> Compare n a
Compare ((Tree 'Z a -> Tree 'Z a -> Ordering) -> Compare 'Z a)
-> (Tree 'Z a -> Tree 'Z a -> Ordering) -> Compare 'Z a
forall a b. (a -> b) -> a -> b
$ \(Leaf a
x) (Leaf a
y) -> a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
x a
y

        step :: Compare m a -> Compare ('S m) a
        step :: forall (m :: Nat). Compare m a -> Compare ('S m) a
step (Compare Tree m a -> Tree m a -> Ordering
go) = (Tree ('S m) a -> Tree ('S m) a -> Ordering) -> Compare ('S m) a
forall (n :: Nat) a.
(Tree n a -> Tree n a -> Ordering) -> Compare n a
Compare ((Tree ('S m) a -> Tree ('S m) a -> Ordering) -> Compare ('S m) a)
-> (Tree ('S m) a -> Tree ('S m) a -> Ordering) -> Compare ('S m) a
forall a b. (a -> b) -> a -> b
$ \(Node Tree m a
x1 Tree m a
y1) (Node Tree m a
x2 Tree m a
y2) ->
            Tree m a -> Tree m a -> Ordering
go Tree m a
x1 Tree m a
x2 Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> Tree m a -> Tree m a -> Ordering
go Tree m a
y1 Tree m a
y2

newtype Compare n a = Compare { forall (n :: Nat) a.
Compare n a -> Tree n a -> Tree n a -> Ordering
getCompare :: Tree n a -> Tree n a -> Ordering }

instance (Show a, N.SNatI n) => Show (Tree n a) where
    showsPrec :: Int -> Tree n a -> ShowS
showsPrec = ShowsPrec n a -> Int -> Tree n a -> ShowS
forall (n :: Nat) a. ShowsPrec n a -> Int -> Tree n a -> ShowS
getShowsPrec (ShowsPrec 'Z a
-> (forall (m :: Nat).
    SNatI m =>
    ShowsPrec m a -> ShowsPrec ('S m) a)
-> ShowsPrec 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 ShowsPrec 'Z a
start ShowsPrec m a -> ShowsPrec ('S m) a
forall (m :: Nat). SNatI m => ShowsPrec m a -> ShowsPrec ('S m) a
forall (m :: Nat). ShowsPrec m a -> ShowsPrec ('S m) a
step) where
        start :: ShowsPrec 'Z a
        start :: ShowsPrec 'Z a
start = (Int -> Tree 'Z a -> ShowS) -> ShowsPrec 'Z a
forall (n :: Nat) a. (Int -> Tree n a -> ShowS) -> ShowsPrec n a
ShowsPrec ((Int -> Tree 'Z a -> ShowS) -> ShowsPrec 'Z a)
-> (Int -> Tree 'Z a -> ShowS) -> ShowsPrec 'Z a
forall a b. (a -> b) -> a -> b
$ \Int
d (Leaf a
x) -> Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10)
            (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"Leaf "
            ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 a
x

        step :: ShowsPrec m a -> ShowsPrec ('S m) a
        step :: forall (m :: Nat). ShowsPrec m a -> ShowsPrec ('S m) a
step (ShowsPrec Int -> Tree m a -> ShowS
go) = (Int -> Tree ('S m) a -> ShowS) -> ShowsPrec ('S m) a
forall (n :: Nat) a. (Int -> Tree n a -> ShowS) -> ShowsPrec n a
ShowsPrec ((Int -> Tree ('S m) a -> ShowS) -> ShowsPrec ('S m) a)
-> (Int -> Tree ('S m) a -> ShowS) -> ShowsPrec ('S m) a
forall a b. (a -> b) -> a -> b
$ \Int
d (Node Tree m a
x Tree m a
y) -> Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10)
            (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"Node "
            ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Tree m a -> ShowS
go Int
11 Tree m a
x
            ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' '
            ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Tree m a -> ShowS
go Int
11 Tree m a
y

newtype ShowsPrec n a = ShowsPrec { forall (n :: Nat) a. ShowsPrec n a -> Int -> Tree n a -> ShowS
getShowsPrec :: Int -> Tree n a -> ShowS }

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

instance N.SNatI n => I.Foldable (Tree n) where
    foldMap :: forall m a. Monoid m => (a -> m) -> Tree n a -> m
foldMap = (a -> m) -> Tree n a -> m
forall a (n :: Nat) m.
(Monoid m, SNatI n) =>
(a -> m) -> Tree n a -> m
foldMap

    foldr :: forall a b. (a -> b -> b) -> b -> Tree n a -> b
foldr  = (a -> b -> b) -> b -> Tree n a -> b
forall a b (n :: Nat).
SNatI n =>
(a -> b -> b) -> b -> Tree n a -> b
foldr
    -- foldl' = foldl'

    null :: forall a. Tree n a -> Bool
null    = Tree n a -> Bool
forall (n :: Nat) a. Tree n a -> Bool
null
    length :: forall a. Tree n a -> Int
length  = Tree n a -> Int
forall (n :: Nat) a. SNatI n => Tree n a -> Int
length
    sum :: forall a. Num a => Tree n a -> a
sum     = Tree n a -> a
forall a (n :: Nat). (Num a, SNatI n) => Tree n a -> a
sum
    product :: forall a. Num a => Tree n a -> a
product = Tree n a -> a
forall a (n :: Nat). (Num a, SNatI n) => Tree n a -> a
product

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

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

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

-- | @since 0.2
instance N.SNatI n => WI.FunctorWithIndex (Wrd n) (Tree n) where
    imap :: forall a b. (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.
SNatI n =>
(Wrd n -> a -> b) -> Tree n a -> Tree n b
imap

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

-- | @since 0.2
instance N.SNatI n => WI.TraversableWithIndex (Wrd n) (Tree n) where
    itraverse :: forall (f :: * -> *) a b.
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)
forall (n :: Nat) (f :: * -> *) a b.
(Applicative f, SNatI n) =>
(Wrd n -> a -> f b) -> Tree n a -> f (Tree n b)
itraverse

instance (NFData a, N.SNatI n) => NFData (Tree n a) where
    rnf :: Tree n a -> ()
rnf = Rnf n a -> Tree n a -> ()
forall (n :: Nat) a. Rnf n a -> Tree n a -> ()
getRnf (Rnf 'Z a
-> (forall (m :: Nat). SNatI m => Rnf m a -> Rnf ('S m) a)
-> Rnf 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 Rnf 'Z a
z Rnf m a -> Rnf ('S m) a
forall (m :: Nat). SNatI m => Rnf m a -> Rnf ('S m) a
forall {n :: Nat} {a}. Rnf n a -> Rnf ('S n) a
s) where
        z :: Rnf 'Z a
z           = (Tree 'Z a -> ()) -> Rnf 'Z a
forall (n :: Nat) a. (Tree n a -> ()) -> Rnf n a
Rnf ((Tree 'Z a -> ()) -> Rnf 'Z a) -> (Tree 'Z a -> ()) -> Rnf 'Z a
forall a b. (a -> b) -> a -> b
$ \(Leaf a
x)   -> a -> ()
forall a. NFData a => a -> ()
rnf a
x
        s :: Rnf n a -> Rnf ('S n) a
s (Rnf Tree n a -> ()
rec) = (Tree ('S n) a -> ()) -> Rnf ('S n) a
forall (n :: Nat) a. (Tree n a -> ()) -> Rnf n a
Rnf ((Tree ('S n) a -> ()) -> Rnf ('S n) a)
-> (Tree ('S n) a -> ()) -> Rnf ('S n) a
forall a b. (a -> b) -> a -> b
$ \(Node Tree n a
x Tree n a
y) -> Tree n a -> ()
rec Tree n a
x () -> () -> ()
forall a b. a -> b -> b
`seq` Tree n a -> ()
rec Tree n a
y

newtype Rnf n a = Rnf { forall (n :: Nat) a. Rnf n a -> Tree n a -> ()
getRnf :: Tree n a -> () }

instance (Hashable a, N.SNatI n) => Hashable (Tree n a) where
    hashWithSalt :: Int -> Tree n a -> Int
hashWithSalt = HashWithSalt n a -> Int -> Tree n a -> Int
forall (n :: Nat) a. HashWithSalt n a -> Int -> Tree n a -> Int
getHashWithSalt (HashWithSalt 'Z a
-> (forall (m :: Nat).
    SNatI m =>
    HashWithSalt m a -> HashWithSalt ('S m) a)
-> HashWithSalt 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 HashWithSalt 'Z a
z HashWithSalt m a -> HashWithSalt ('S m) a
forall (m :: Nat).
SNatI m =>
HashWithSalt m a -> HashWithSalt ('S m) a
forall {n :: Nat} {a}. HashWithSalt n a -> HashWithSalt ('S n) a
s) where
        z :: HashWithSalt 'Z a
z = (Int -> Tree 'Z a -> Int) -> HashWithSalt 'Z a
forall (n :: Nat) a. (Int -> Tree n a -> Int) -> HashWithSalt n a
HashWithSalt ((Int -> Tree 'Z a -> Int) -> HashWithSalt 'Z a)
-> (Int -> Tree 'Z a -> Int) -> HashWithSalt 'Z a
forall a b. (a -> b) -> a -> b
$ \Int
salt (Leaf a
x) -> Int
salt Int -> a -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` a
x
        s :: HashWithSalt n a -> HashWithSalt ('S n) a
s (HashWithSalt Int -> Tree n a -> Int
rec) = (Int -> Tree ('S n) a -> Int) -> HashWithSalt ('S n) a
forall (n :: Nat) a. (Int -> Tree n a -> Int) -> HashWithSalt n a
HashWithSalt ((Int -> Tree ('S n) a -> Int) -> HashWithSalt ('S n) a)
-> (Int -> Tree ('S n) a -> Int) -> HashWithSalt ('S n) a
forall a b. (a -> b) -> a -> b
$ \Int
salt (Node Tree n a
x Tree n a
y) -> Int -> Tree n a -> Int
rec (Int -> Tree n a -> Int
rec Int
salt Tree n a
x) Tree n a
y

newtype HashWithSalt n a = HashWithSalt { forall (n :: Nat) a. HashWithSalt n a -> Int -> Tree n a -> Int
getHashWithSalt :: Int -> Tree n a -> Int }

instance N.SNatI n => Applicative (Tree n) where
    pure :: forall a. a -> Tree n a
pure = a -> Tree n a
forall (n :: Nat) x. SNatI n => x -> Tree n x
repeat
    <*> :: forall a b. 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).
SNatI n =>
(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
_ *> :: forall a b. Tree n a -> Tree n b -> Tree n b
*> Tree n b
x = Tree n b
x
    Tree n a
x <* :: forall a b. Tree n a -> Tree n b -> Tree n a
<* Tree n b
_ = Tree n a
x
    liftA2 :: forall a b c. (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).
SNatI n =>
(a -> b -> c) -> Tree n a -> Tree n b -> Tree n c
zipWith

-- TODO: Monad

#ifdef MIN_VERSION_distributive
instance N.SNatI n => I.Distributive (Tree n) where
    distribute :: forall (f :: * -> *) a. Functor f => 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 a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Tree n a -> Wrd n -> a
forall (n :: Nat) a. SNatI n => 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 :: forall a. (Rep (Tree n) -> a) -> Tree n a
tabulate = (Rep (Tree n) -> a) -> Tree n a
(Wrd n -> a) -> Tree n a
forall (n :: Nat) a. SNatI n => (Wrd n -> a) -> Tree n a
tabulate
    index :: forall a. Tree n a -> Rep (Tree n) -> a
index    = Tree n a -> Rep (Tree n) -> a
Tree n a -> Wrd n -> a
forall (n :: Nat) a. SNatI n => Tree n a -> Wrd n -> a
(!)
#endif
#endif

instance (Semigroup a, N.SNatI n) => Semigroup (Tree n a) where
    <> :: Tree n a -> Tree n a -> Tree n a
(<>) = (a -> a -> a) -> Tree n a -> Tree n a -> Tree n a
forall a b c (n :: Nat).
SNatI n =>
(a -> b -> c) -> Tree n a -> Tree n b -> Tree n c
zipWith a -> a -> a
forall a. Semigroup a => a -> a -> a
(<>)

instance (Monoid a, N.SNatI n) => Monoid (Tree n a) where
    mempty :: Tree n a
mempty = a -> Tree n a
forall a. a -> Tree n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
forall a. Monoid a => a
mempty
    mappend :: Tree n a -> Tree n a -> Tree n a
mappend = (a -> a -> a) -> Tree n a -> Tree n a -> Tree n a
forall a b c (n :: Nat).
SNatI n =>
(a -> b -> c) -> Tree n a -> Tree n b -> Tree n c
zipWith a -> a -> a
forall a. Monoid a => a -> a -> a
mappend

#ifdef MIN_VERSION_semigroupoids
instance N.SNatI n => Apply (Tree n) where
    <.> :: forall a b. 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).
SNatI n =>
(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
_ .> :: forall a b. Tree n a -> Tree n b -> Tree n b
.> Tree n b
x = Tree n b
x
    Tree n a
x <. :: forall a b. Tree n a -> Tree n b -> Tree n a
<. Tree n b
_ = Tree n a
x
    liftF2 :: forall a b c. (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).
SNatI n =>
(a -> b -> c) -> Tree n a -> Tree n b -> Tree n c
zipWith

-- TODO: Bind
#endif

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

-- | 'Tree' with exactly one element.
--
-- >>> singleton True
-- Leaf True
--
singleton :: a -> Tree 'Z a
singleton :: forall a. 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 'f') (Leaf 'o')) (Node (Leaf 'o') (Leaf 'd'))
-- "food"
toList :: forall n a. N.SNatI n => Tree n a -> [a]
toList :: forall (n :: Nat) a. SNatI n => Tree n a -> [a]
toList Tree n a
xs = ToList n a -> Tree n a -> [a] -> [a]
forall (n :: Nat) a. ToList n a -> Tree n a -> [a] -> [a]
getToList (ToList 'Z a
-> (forall (m :: Nat). SNatI m => ToList m a -> ToList ('S m) a)
-> ToList 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 ToList 'Z a
start ToList m a -> ToList ('S m) a
forall (m :: Nat). SNatI m => ToList m a -> ToList ('S m) a
forall (m :: Nat). ToList m a -> ToList ('S m) a
step) Tree n a
xs [] where
    start :: ToList 'Z a
    start :: ToList 'Z a
start = (Tree 'Z a -> [a] -> [a]) -> ToList 'Z a
forall (n :: Nat) a. (Tree n a -> [a] -> [a]) -> ToList n a
ToList (\(Leaf a
x) -> (a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
:))

    step :: ToList m a -> ToList ('S m) a
    step :: forall (m :: Nat). ToList m a -> ToList ('S m) a
step (ToList Tree m a -> [a] -> [a]
f) = (Tree ('S m) a -> [a] -> [a]) -> ToList ('S m) a
forall (n :: Nat) a. (Tree n a -> [a] -> [a]) -> ToList n a
ToList ((Tree ('S m) a -> [a] -> [a]) -> ToList ('S m) a)
-> (Tree ('S m) a -> [a] -> [a]) -> ToList ('S m) a
forall a b. (a -> b) -> a -> b
$ \(Node Tree m a
x Tree m a
y) -> Tree m a -> [a] -> [a]
f Tree m a
x ([a] -> [a]) -> ([a] -> [a]) -> [a] -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tree m a -> [a] -> [a]
f Tree m a
y

newtype ToList n a = ToList { forall (n :: Nat) a. ToList n a -> Tree n a -> [a] -> [a]
getToList :: Tree n a -> [a] -> [a] }

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

flipIndex :: N.SNatI n => Wrd n -> Tree n a -> a
flipIndex :: forall (n :: Nat) a. SNatI n => Wrd n -> Tree n a -> a
flipIndex = Index n a -> Wrd n -> Tree n a -> a
forall (n :: Nat) a. Index n a -> Wrd n -> Tree n a -> a
getIndex (Index 'Z a
-> (forall (m :: Nat). SNatI m => Index m a -> Index ('S m) a)
-> Index 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 Index 'Z a
forall a. Index 'Z a
start Index m a -> Index ('S m) a
forall (m :: Nat). SNatI m => Index m a -> Index ('S m) a
forall (m :: Nat) a. Index m a -> Index ('S m) a
step) where
    start :: Index 'Z a
    start :: forall a. Index 'Z a
start = (Wrd 'Z -> Tree 'Z a -> a) -> Index 'Z a
forall (n :: Nat) a. (Wrd n -> Tree n a -> a) -> Index n a
Index ((Wrd 'Z -> Tree 'Z a -> a) -> Index 'Z a)
-> (Wrd 'Z -> Tree 'Z a -> a) -> Index 'Z a
forall a b. (a -> b) -> a -> b
$ \Wrd 'Z
_ (Leaf a
x) -> a
x

    step :: Index m a-> Index ('N.S m) a
    step :: forall (m :: Nat) a. Index m a -> Index ('S m) a
step (Index Wrd m -> Tree m a -> a
go) = (Wrd ('S m) -> Tree ('S m) a -> a) -> Index ('S m) a
forall (n :: Nat) a. (Wrd n -> Tree n a -> a) -> Index n a
Index ((Wrd ('S m) -> Tree ('S m) a -> a) -> Index ('S m) a)
-> (Wrd ('S m) -> Tree ('S m) a -> a) -> Index ('S m) a
forall a b. (a -> b) -> a -> b
$ \Wrd ('S m)
i (Node Tree m a
x Tree m a
y) -> case Wrd ('S m)
i of
        W0 Wrd n1
j -> Wrd m -> Tree m a -> a
go Wrd m
Wrd n1
j Tree m a
x
        W1 Wrd n1
j -> Wrd m -> Tree m a -> a
go Wrd m
Wrd n1
j Tree m a
y

newtype Index n a = Index { forall (n :: Nat) a. Index n a -> Wrd n -> Tree n a -> a
getIndex :: Wrd n -> Tree n a -> a }

-- | Indexing.
--
-- >>> let t = Node (Node (Leaf 'a') (Leaf 'b')) (Node (Leaf 'c') (Leaf 'd'))
-- >>> t ! W1 (W0 WE)
-- 'c'
--
(!) :: N.SNatI n => Tree n a -> Wrd n -> a
! :: forall (n :: Nat) a. SNatI n => Tree n a -> Wrd n -> a
(!) = (Wrd n -> Tree n a -> a) -> Tree n a -> Wrd n -> a
forall a b c. (a -> b -> c) -> b -> a -> c
flip Wrd n -> Tree n a -> a
forall (n :: Nat) a. SNatI n => Wrd n -> Tree n a -> a
flipIndex

-- | Tabulating, inverse of '!'.
--
-- >>> tabulate id :: Tree N.Nat2 (Wrd N.Nat2)
-- Node (Node (Leaf 0b00) (Leaf 0b01)) (Node (Leaf 0b10) (Leaf 0b11))
tabulate :: N.SNatI n => (Wrd n -> a) -> Tree n a
tabulate :: forall (n :: Nat) a. SNatI n => (Wrd n -> a) -> Tree n a
tabulate = Tabulate n a -> (Wrd n -> a) -> Tree n a
forall (n :: Nat) a. Tabulate n a -> (Wrd n -> a) -> Tree n a
getTabulate (Tabulate 'Z a
-> (forall (m :: Nat).
    SNatI m =>
    Tabulate m a -> Tabulate ('S m) a)
-> Tabulate 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 Tabulate 'Z a
forall a. Tabulate 'Z a
start Tabulate m a -> Tabulate ('S m) a
forall (m :: Nat). SNatI m => Tabulate m a -> Tabulate ('S m) a
forall (m :: Nat) a. Tabulate m a -> Tabulate ('S m) a
step) where
    start :: Tabulate 'Z a
    start :: forall a. Tabulate 'Z a
start = ((Wrd 'Z -> a) -> Tree 'Z a) -> Tabulate 'Z a
forall (n :: Nat) a. ((Wrd n -> a) -> Tree n a) -> Tabulate n a
Tabulate (((Wrd 'Z -> a) -> Tree 'Z a) -> Tabulate 'Z a)
-> ((Wrd 'Z -> a) -> Tree 'Z a) -> Tabulate 'Z a
forall a b. (a -> b) -> a -> b
$ \Wrd 'Z -> a
f -> a -> Tree 'Z a
forall a. a -> Tree 'Z a
Leaf (Wrd 'Z -> a
f Wrd 'Z
WE)

    step :: Tabulate m a -> Tabulate ('S m) a
    step :: forall (m :: Nat) a. Tabulate m a -> Tabulate ('S m) a
step (Tabulate (Wrd m -> a) -> Tree m a
go) = ((Wrd ('S m) -> a) -> Tree ('S m) a) -> Tabulate ('S m) a
forall (n :: Nat) a. ((Wrd n -> a) -> Tree n a) -> Tabulate n a
Tabulate (((Wrd ('S m) -> a) -> Tree ('S m) a) -> Tabulate ('S m) a)
-> ((Wrd ('S m) -> a) -> Tree ('S m) a) -> Tabulate ('S m) a
forall a b. (a -> b) -> a -> b
$ \Wrd ('S m) -> a
f -> 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 ((Wrd m -> a) -> Tree m a
go (Wrd ('S m) -> a
f (Wrd ('S m) -> a) -> (Wrd m -> Wrd ('S m)) -> Wrd m -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrd m -> Wrd ('S m)
forall (n1 :: Nat). Wrd n1 -> Wrd ('S n1)
W0)) ((Wrd m -> a) -> Tree m a
go (Wrd ('S m) -> a
f (Wrd ('S m) -> a) -> (Wrd m -> Wrd ('S m)) -> Wrd m -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrd m -> Wrd ('S m)
forall (n1 :: Nat). Wrd n1 -> Wrd ('S n1)
W1))

newtype Tabulate n a = Tabulate { forall (n :: Nat) a. Tabulate n a -> (Wrd n -> a) -> Tree n a
getTabulate :: (Wrd n -> a) -> Tree n a }

leftmost :: N.SNatI n => Tree n a -> a
leftmost :: forall (n :: Nat) a. SNatI n => Tree n a -> a
leftmost = TheMost n a -> Tree n a -> a
forall (n :: Nat) a. TheMost n a -> Tree n a -> a
getTheMost (TheMost 'Z a
-> (forall (m :: Nat). SNatI m => TheMost m a -> TheMost ('S m) a)
-> TheMost 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 TheMost 'Z a
forall a. TheMost 'Z a
start TheMost m a -> TheMost ('S m) a
forall (m :: Nat). SNatI m => TheMost m a -> TheMost ('S m) a
forall (m :: Nat) a. TheMost m a -> TheMost ('S m) a
step) where
    start :: TheMost 'Z a
    start :: forall a. TheMost 'Z a
start = (Tree 'Z a -> a) -> TheMost 'Z a
forall (n :: Nat) a. (Tree n a -> a) -> TheMost n a
TheMost ((Tree 'Z a -> a) -> TheMost 'Z a)
-> (Tree 'Z a -> a) -> TheMost 'Z a
forall a b. (a -> b) -> a -> b
$ \(Leaf a
x) -> a
x

    step :: TheMost m a -> TheMost ('S m) a
    step :: forall (m :: Nat) a. TheMost m a -> TheMost ('S m) a
step (TheMost Tree m a -> a
go) = (Tree ('S m) a -> a) -> TheMost ('S m) a
forall (n :: Nat) a. (Tree n a -> a) -> TheMost n a
TheMost ((Tree ('S m) a -> a) -> TheMost ('S m) a)
-> (Tree ('S m) a -> a) -> TheMost ('S m) a
forall a b. (a -> b) -> a -> b
$ \(Node Tree m a
x Tree m a
_) -> Tree m a -> a
go Tree m a
x

rightmost :: N.SNatI n => Tree n a -> a
rightmost :: forall (n :: Nat) a. SNatI n => Tree n a -> a
rightmost = TheMost n a -> Tree n a -> a
forall (n :: Nat) a. TheMost n a -> Tree n a -> a
getTheMost (TheMost 'Z a
-> (forall (m :: Nat). SNatI m => TheMost m a -> TheMost ('S m) a)
-> TheMost 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 TheMost 'Z a
forall a. TheMost 'Z a
start TheMost m a -> TheMost ('S m) a
forall (m :: Nat). SNatI m => TheMost m a -> TheMost ('S m) a
forall (m :: Nat) a. TheMost m a -> TheMost ('S m) a
step) where
    start :: TheMost 'Z a
    start :: forall a. TheMost 'Z a
start = (Tree 'Z a -> a) -> TheMost 'Z a
forall (n :: Nat) a. (Tree n a -> a) -> TheMost n a
TheMost ((Tree 'Z a -> a) -> TheMost 'Z a)
-> (Tree 'Z a -> a) -> TheMost 'Z a
forall a b. (a -> b) -> a -> b
$ \(Leaf a
x) -> a
x

    step :: TheMost m a -> TheMost ('S m) a
    step :: forall (m :: Nat) a. TheMost m a -> TheMost ('S m) a
step (TheMost Tree m a -> a
go) = (Tree ('S m) a -> a) -> TheMost ('S m) a
forall (n :: Nat) a. (Tree n a -> a) -> TheMost n a
TheMost ((Tree ('S m) a -> a) -> TheMost ('S m) a)
-> (Tree ('S m) a -> a) -> TheMost ('S m) a
forall a b. (a -> b) -> a -> b
$ \(Node Tree m a
_ Tree m a
y) -> Tree m a -> a
go Tree m a
y

newtype TheMost n a = TheMost { forall (n :: Nat) a. TheMost n a -> Tree n a -> a
getTheMost :: Tree n a -> a }

-------------------------------------------------------------------------------
-- 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'))
--
reverse :: forall n a. N.SNatI n => Tree n a -> Tree n a
reverse :: forall (n :: Nat) a. SNatI n => Tree n a -> Tree n a
reverse = Reverse n a -> Tree n a -> Tree n a
forall (n :: Nat) a. Reverse n a -> Tree n a -> Tree n a
getReverse (Reverse 'Z a
-> (forall (m :: Nat). SNatI m => Reverse m a -> Reverse ('S m) a)
-> Reverse 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 Reverse 'Z a
start Reverse m a -> Reverse ('S m) a
forall (m :: Nat). SNatI m => Reverse m a -> Reverse ('S m) a
step) where
    start :: Reverse 'Z a
    start :: Reverse 'Z a
start = (Tree 'Z a -> Tree 'Z a) -> Reverse 'Z a
forall (n :: Nat) a. (Tree n a -> Tree n a) -> Reverse n a
Reverse Tree 'Z a -> Tree 'Z a
forall a. a -> a
id

    step :: N.SNatI m => Reverse m a -> Reverse ('S m) a
    step :: forall (m :: Nat). SNatI m => Reverse m a -> Reverse ('S m) a
step (Reverse Tree m a -> Tree m a
go) = (Tree ('S m) a -> Tree ('S m) a) -> Reverse ('S m) a
forall (n :: Nat) a. (Tree n a -> Tree n a) -> Reverse n a
Reverse ((Tree ('S m) a -> Tree ('S m) a) -> Reverse ('S m) a)
-> (Tree ('S m) a -> Tree ('S m) a) -> Reverse ('S m) a
forall a b. (a -> b) -> a -> b
$ \(Node Tree m a
x Tree m a
y) -> 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
go Tree m a
y) (Tree m a -> Tree m a
go Tree m a
x)

newtype Reverse n a = Reverse { forall (n :: Nat) a. Reverse n a -> Tree n a -> Tree n a
getReverse :: Tree n a -> Tree n a }

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

-- | >>> map not $ Node (Leaf True) (Leaf False)
-- Node (Leaf False) (Leaf True)
--
map :: forall a b n. N.SNatI n => (a -> b) -> Tree n a -> Tree n b
map :: forall a b (n :: Nat). SNatI n => (a -> b) -> Tree n a -> Tree n b
map a -> b
f = Map a n b -> Tree n a -> Tree n b
forall a (n :: Nat) b. Map a n b -> Tree n a -> Tree n b
getMap (Map a n b -> Tree n a -> Tree n b)
-> Map a n b -> Tree n a -> Tree n b
forall a b. (a -> b) -> a -> b
$ Map a 'Z b
-> (forall (m :: Nat). SNatI m => Map a m b -> Map a ('S m) b)
-> Map a n b
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 Map a 'Z b
start Map a m b -> Map a ('S m) b
forall (m :: Nat). SNatI m => Map a m b -> Map a ('S m) b
forall (m :: Nat). Map a m b -> Map a ('S m) b
step where
    start :: Map a 'Z b
    start :: Map a 'Z b
start = (Tree 'Z a -> Tree 'Z b) -> Map a 'Z b
forall a (n :: Nat) b. (Tree n a -> Tree n b) -> Map a n b
Map ((Tree 'Z a -> Tree 'Z b) -> Map a 'Z b)
-> (Tree 'Z a -> Tree 'Z b) -> Map a 'Z b
forall a b. (a -> b) -> a -> b
$ \(Leaf a
x) -> b -> Tree 'Z b
forall a. a -> Tree 'Z a
Leaf (a -> b
f a
x)

    step :: Map a m b -> Map a ('S m) b
    step :: forall (m :: Nat). Map a m b -> Map a ('S m) b
step (Map Tree m a -> Tree m b
go) = (Tree ('S m) a -> Tree ('S m) b) -> Map a ('S m) b
forall a (n :: Nat) b. (Tree n a -> Tree n b) -> Map a n b
Map ((Tree ('S m) a -> Tree ('S m) b) -> Map a ('S m) b)
-> (Tree ('S m) a -> Tree ('S m) b) -> Map a ('S m) b
forall a b. (a -> b) -> a -> b
$ \(Node Tree m a
x Tree m a
y) -> Tree m b -> Tree m b -> Tree ('S m) b
forall (n :: Nat) a. Tree n a -> Tree n a -> Tree ('S n) a
Node (Tree m a -> Tree m b
go Tree m a
x) (Tree m a -> Tree m b
go Tree m a
y)

newtype Map a n b = Map { forall a (n :: Nat) b. Map a n b -> Tree n a -> Tree n b
getMap :: Tree n a -> Tree n b }

-- |
-- >>> let t = Node (Node (Leaf 'a') (Leaf 'b')) (Node (Leaf 'c') (Leaf 'd'))
-- >>> imap (,) t
-- Node (Node (Leaf (0b00,'a')) (Leaf (0b01,'b'))) (Node (Leaf (0b10,'c')) (Leaf (0b11,'d')))
--
imap :: N.SNatI n => (Wrd n -> a -> b) -> Tree n a -> Tree n b
imap :: forall (n :: Nat) a b.
SNatI n =>
(Wrd n -> a -> b) -> Tree n a -> Tree n b
imap = IMap a n b -> (Wrd n -> a -> b) -> Tree n a -> Tree n b
forall a (n :: Nat) b.
IMap a n b -> (Wrd n -> a -> b) -> Tree n a -> Tree n b
getIMap (IMap a n b -> (Wrd n -> a -> b) -> Tree n a -> Tree n b)
-> IMap a n b -> (Wrd n -> a -> b) -> Tree n a -> Tree n b
forall a b. (a -> b) -> a -> b
$ IMap a 'Z b
-> (forall (m :: Nat). SNatI m => IMap a m b -> IMap a ('S m) b)
-> IMap a n b
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 IMap a 'Z b
forall a b. IMap a 'Z b
start IMap a m b -> IMap a ('S m) b
forall a (m :: Nat) b. IMap a m b -> IMap a ('S m) b
forall (m :: Nat). SNatI m => IMap a m b -> IMap a ('S m) b
step where
    start :: IMap a 'Z b
    start :: forall a b. IMap a 'Z b
start = ((Wrd 'Z -> a -> b) -> Tree 'Z a -> Tree 'Z b) -> IMap a 'Z b
forall a (n :: Nat) b.
((Wrd n -> a -> b) -> Tree n a -> Tree n b) -> IMap a n b
IMap (((Wrd 'Z -> a -> b) -> Tree 'Z a -> Tree 'Z b) -> IMap a 'Z b)
-> ((Wrd 'Z -> a -> b) -> Tree 'Z a -> Tree 'Z b) -> IMap a 'Z b
forall a b. (a -> b) -> a -> b
$ \Wrd 'Z -> a -> b
f (Leaf a
x) -> b -> Tree 'Z b
forall a. a -> Tree 'Z a
Leaf (Wrd 'Z -> a -> b
f Wrd 'Z
WE a
x)

    step :: IMap a m b -> IMap a ('S m) b
    step :: forall a (m :: Nat) b. IMap a m b -> IMap a ('S m) b
step (IMap (Wrd m -> a -> b) -> Tree m a -> Tree m b
go) = ((Wrd ('S m) -> a -> b) -> Tree ('S m) a -> Tree ('S m) b)
-> IMap a ('S m) b
forall a (n :: Nat) b.
((Wrd n -> a -> b) -> Tree n a -> Tree n b) -> IMap a n b
IMap (((Wrd ('S m) -> a -> b) -> Tree ('S m) a -> Tree ('S m) b)
 -> IMap a ('S m) b)
-> ((Wrd ('S m) -> a -> b) -> Tree ('S m) a -> Tree ('S m) b)
-> IMap a ('S m) b
forall a b. (a -> b) -> a -> b
$ \Wrd ('S m) -> a -> b
f (Node Tree m a
x Tree m a
y) ->
        Tree m b -> Tree m b -> Tree ('S m) b
forall (n :: Nat) a. Tree n a -> Tree n a -> Tree ('S n) a
Node ((Wrd m -> a -> b) -> Tree m a -> Tree m b
go (Wrd ('S m) -> a -> b
f (Wrd ('S m) -> a -> b) -> (Wrd m -> Wrd ('S m)) -> Wrd m -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrd m -> Wrd ('S m)
forall (n1 :: Nat). Wrd n1 -> Wrd ('S n1)
W0) Tree m a
x) ((Wrd m -> a -> b) -> Tree m a -> Tree m b
go (Wrd ('S m) -> a -> b
f (Wrd ('S m) -> a -> b) -> (Wrd m -> Wrd ('S m)) -> Wrd m -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrd m -> Wrd ('S m)
forall (n1 :: Nat). Wrd n1 -> Wrd ('S n1)
W1) Tree m a
y)

newtype IMap a n b = IMap { forall a (n :: Nat) b.
IMap a n b -> (Wrd n -> a -> b) -> Tree n a -> Tree n b
getIMap :: (Wrd n -> a -> b) -> Tree n a -> Tree n b }

-- | Apply an action to every element of a 'Tree', yielding a 'Tree' of results.
traverse :: forall n f a b. (Applicative f, N.SNatI n) => (a -> f b) -> Tree n a -> f (Tree n b)
traverse :: forall (n :: Nat) (f :: * -> *) a b.
(Applicative f, SNatI n) =>
(a -> f b) -> Tree n a -> f (Tree n b)
traverse a -> f b
f =  Traverse f a n b -> Tree n a -> f (Tree n b)
forall (f :: * -> *) a (n :: Nat) b.
Traverse f a n b -> Tree n a -> f (Tree n b)
getTraverse (Traverse f a n b -> Tree n a -> f (Tree n b))
-> Traverse f a n b -> Tree n a -> f (Tree n b)
forall a b. (a -> b) -> a -> b
$ Traverse f a 'Z b
-> (forall (m :: Nat).
    SNatI m =>
    Traverse f a m b -> Traverse f a ('S m) b)
-> Traverse f a n b
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 Traverse f a 'Z b
start Traverse f a m b -> Traverse f a ('S m) b
forall (m :: Nat).
SNatI m =>
Traverse f a m b -> Traverse f a ('S m) b
forall (m :: Nat). Traverse f a m b -> Traverse f a ('S m) b
step where
    start :: Traverse f a 'Z b
    start :: Traverse f a 'Z b
start = (Tree 'Z a -> f (Tree 'Z b)) -> Traverse f a 'Z b
forall (f :: * -> *) a (n :: Nat) b.
(Tree n a -> f (Tree n b)) -> Traverse f a n b
Traverse ((Tree 'Z a -> f (Tree 'Z b)) -> Traverse f a 'Z b)
-> (Tree 'Z a -> f (Tree 'Z b)) -> Traverse f a 'Z b
forall a b. (a -> b) -> a -> b
$ \(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

    step :: Traverse f a m b -> Traverse f a ('S m) b
    step :: forall (m :: Nat). Traverse f a m b -> Traverse f a ('S m) b
step (Traverse Tree m a -> f (Tree m b)
go) = (Tree ('S m) a -> f (Tree ('S m) b)) -> Traverse f a ('S m) b
forall (f :: * -> *) a (n :: Nat) b.
(Tree n a -> f (Tree n b)) -> Traverse f a n b
Traverse ((Tree ('S m) a -> f (Tree ('S m) b)) -> Traverse f a ('S m) b)
-> (Tree ('S m) a -> f (Tree ('S m) b)) -> Traverse f a ('S m) b
forall a b. (a -> b) -> a -> b
$ \(Node Tree m a
x Tree m a
y) -> (Tree m b -> Tree m b -> Tree ('S m) b)
-> f (Tree m b) -> f (Tree m b) -> f (Tree ('S m) b)
forall a b c. (a -> b -> c) -> f a -> f b -> f c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Tree m b -> Tree m b -> Tree ('S m) b
forall (n :: Nat) a. Tree n a -> Tree n a -> Tree ('S n) a
Node (Tree m a -> f (Tree m b)
go Tree m a
x) (Tree m a -> f (Tree m b)
go Tree m a
y)
{-# INLINE traverse #-}

newtype Traverse f a n b = Traverse { forall (f :: * -> *) a (n :: Nat) b.
Traverse f a n b -> Tree n a -> f (Tree n b)
getTraverse :: Tree n a -> f (Tree n b) }

-- | Apply an action to every element of a 'Tree' and its index, yielding a 'Tree' of results.
itraverse :: forall n f a b. (Applicative f, N.SNatI n) => (Wrd n -> a -> f b) -> Tree n a -> f (Tree n b)
itraverse :: forall (n :: Nat) (f :: * -> *) a b.
(Applicative f, SNatI n) =>
(Wrd n -> a -> f b) -> Tree n a -> f (Tree n b)
itraverse = ITraverse f a n b
-> (Wrd n -> a -> f b) -> Tree n a -> f (Tree n b)
forall (f :: * -> *) a (n :: Nat) b.
ITraverse f a n b
-> (Wrd n -> a -> f b) -> Tree n a -> f (Tree n b)
getITraverse (ITraverse f a n b
 -> (Wrd n -> a -> f b) -> Tree n a -> f (Tree n b))
-> ITraverse f a n b
-> (Wrd n -> a -> f b)
-> Tree n a
-> f (Tree n b)
forall a b. (a -> b) -> a -> b
$ ITraverse f a 'Z b
-> (forall (m :: Nat).
    SNatI m =>
    ITraverse f a m b -> ITraverse f a ('S m) b)
-> ITraverse f a n b
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 ITraverse f a 'Z b
start ITraverse f a m b -> ITraverse f a ('S m) b
forall (m :: Nat).
SNatI m =>
ITraverse f a m b -> ITraverse f a ('S m) b
forall (m :: Nat). ITraverse f a m b -> ITraverse f a ('S m) b
step where
    start :: ITraverse f a 'Z b
    start :: ITraverse f a 'Z b
start = ((Wrd 'Z -> a -> f b) -> Tree 'Z a -> f (Tree 'Z b))
-> ITraverse f a 'Z b
forall (f :: * -> *) a (n :: Nat) b.
((Wrd n -> a -> f b) -> Tree n a -> f (Tree n b))
-> ITraverse f a n b
ITraverse (((Wrd 'Z -> a -> f b) -> Tree 'Z a -> f (Tree 'Z b))
 -> ITraverse f a 'Z b)
-> ((Wrd 'Z -> a -> f b) -> Tree 'Z a -> f (Tree 'Z b))
-> ITraverse f a 'Z b
forall a b. (a -> b) -> a -> b
$ \Wrd 'Z -> 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 'Z -> a -> f b
f Wrd 'Z
WE a
x

    step :: ITraverse f a m b -> ITraverse f a ('S m) b
    step :: forall (m :: Nat). ITraverse f a m b -> ITraverse f a ('S m) b
step (ITraverse (Wrd m -> a -> f b) -> Tree m a -> f (Tree m b)
go) = ((Wrd ('S m) -> a -> f b) -> Tree ('S m) a -> f (Tree ('S m) b))
-> ITraverse f a ('S m) b
forall (f :: * -> *) a (n :: Nat) b.
((Wrd n -> a -> f b) -> Tree n a -> f (Tree n b))
-> ITraverse f a n b
ITraverse (((Wrd ('S m) -> a -> f b) -> Tree ('S m) a -> f (Tree ('S m) b))
 -> ITraverse f a ('S m) b)
-> ((Wrd ('S m) -> a -> f b) -> Tree ('S m) a -> f (Tree ('S m) b))
-> ITraverse f a ('S m) b
forall a b. (a -> b) -> a -> b
$ \Wrd ('S m) -> a -> f b
f (Node Tree m a
x Tree m a
y) -> (Tree m b -> Tree m b -> Tree ('S m) b)
-> f (Tree m b) -> f (Tree m b) -> f (Tree ('S m) b)
forall a b c. (a -> b -> c) -> f a -> f b -> f c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Tree m b -> Tree m b -> Tree ('S m) b
forall (n :: Nat) a. Tree n a -> Tree n a -> Tree ('S n) a
Node ((Wrd m -> a -> f b) -> Tree m a -> f (Tree m b)
go (Wrd ('S m) -> a -> f b
f (Wrd ('S m) -> a -> f b)
-> (Wrd m -> Wrd ('S m)) -> Wrd m -> a -> f b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrd m -> Wrd ('S m)
forall (n1 :: Nat). Wrd n1 -> Wrd ('S n1)
W0) Tree m a
x) ((Wrd m -> a -> f b) -> Tree m a -> f (Tree m b)
go (Wrd ('S m) -> a -> f b
f (Wrd ('S m) -> a -> f b)
-> (Wrd m -> Wrd ('S m)) -> Wrd m -> a -> f b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrd m -> Wrd ('S m)
forall (n1 :: Nat). Wrd n1 -> Wrd ('S n1)
W1) Tree m a
y)
{-# INLINE itraverse #-}

newtype ITraverse f a n b = ITraverse { forall (f :: * -> *) a (n :: Nat) b.
ITraverse f a n b
-> (Wrd n -> a -> f b) -> Tree n a -> f (Tree n b)
getITraverse :: (Wrd n -> a -> f b) -> Tree n a -> f (Tree n b) }

#ifdef MIN_VERSION_semigroupoids
-- | Apply an action to non-empty 'Tree', yielding a 'Tree' of results.
traverse1 :: forall n f a b. (Apply f, N.SNatI n) => (a -> f b) -> Tree n a -> f (Tree n b)
traverse1 :: forall (n :: Nat) (f :: * -> *) a b.
(Apply f, SNatI n) =>
(a -> f b) -> Tree n a -> f (Tree n b)
traverse1 a -> f b
f = Traverse f a n b -> Tree n a -> f (Tree n b)
forall (f :: * -> *) a (n :: Nat) b.
Traverse f a n b -> Tree n a -> f (Tree n b)
getTraverse (Traverse f a n b -> Tree n a -> f (Tree n b))
-> Traverse f a n b -> Tree n a -> f (Tree n b)
forall a b. (a -> b) -> a -> b
$ Traverse f a 'Z b
-> (forall (m :: Nat).
    SNatI m =>
    Traverse f a m b -> Traverse f a ('S m) b)
-> Traverse f a n b
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 Traverse f a 'Z b
start Traverse f a m b -> Traverse f a ('S m) b
forall (m :: Nat).
SNatI m =>
Traverse f a m b -> Traverse f a ('S m) b
forall (m :: Nat). Traverse f a m b -> Traverse f a ('S m) b
step where
    start :: Traverse f a 'Z b
    start :: Traverse f a 'Z b
start = (Tree 'Z a -> f (Tree 'Z b)) -> Traverse f a 'Z b
forall (f :: * -> *) a (n :: Nat) b.
(Tree n a -> f (Tree n b)) -> Traverse f a n b
Traverse ((Tree 'Z a -> f (Tree 'Z b)) -> Traverse f a 'Z b)
-> (Tree 'Z a -> f (Tree 'Z b)) -> Traverse f a 'Z b
forall a b. (a -> b) -> a -> b
$ \(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

    step :: Traverse f a m b -> Traverse f a ('S m) b
    step :: forall (m :: Nat). Traverse f a m b -> Traverse f a ('S m) b
step (Traverse Tree m a -> f (Tree m b)
go) = (Tree ('S m) a -> f (Tree ('S m) b)) -> Traverse f a ('S m) b
forall (f :: * -> *) a (n :: Nat) b.
(Tree n a -> f (Tree n b)) -> Traverse f a n b
Traverse ((Tree ('S m) a -> f (Tree ('S m) b)) -> Traverse f a ('S m) b)
-> (Tree ('S m) a -> f (Tree ('S m) b)) -> Traverse f a ('S m) b
forall a b. (a -> b) -> a -> b
$ \(Node Tree m a
x Tree m a
y) -> (Tree m b -> Tree m b -> Tree ('S m) b)
-> f (Tree m b) -> f (Tree m b) -> f (Tree ('S m) b)
forall a b c. (a -> b -> c) -> f a -> f b -> f c
forall (f :: * -> *) a b c.
Apply f =>
(a -> b -> c) -> f a -> f b -> f c
liftF2 Tree m b -> Tree m b -> Tree ('S m) b
forall (n :: Nat) a. Tree n a -> Tree n a -> Tree ('S n) a
Node (Tree m a -> f (Tree m b)
go Tree m a
x) (Tree m a -> f (Tree m b)
go Tree m a
y)
{-# INLINE traverse1 #-}

itraverse1 :: forall n f a b. (Apply f, N.SNatI n) => (Wrd n -> a -> f b) -> Tree n a -> f (Tree n b)
itraverse1 :: forall (n :: Nat) (f :: * -> *) a b.
(Apply f, SNatI n) =>
(Wrd n -> a -> f b) -> Tree n a -> f (Tree n b)
itraverse1 = ITraverse f a n b
-> (Wrd n -> a -> f b) -> Tree n a -> f (Tree n b)
forall (f :: * -> *) a (n :: Nat) b.
ITraverse f a n b
-> (Wrd n -> a -> f b) -> Tree n a -> f (Tree n b)
getITraverse (ITraverse f a n b
 -> (Wrd n -> a -> f b) -> Tree n a -> f (Tree n b))
-> ITraverse f a n b
-> (Wrd n -> a -> f b)
-> Tree n a
-> f (Tree n b)
forall a b. (a -> b) -> a -> b
$ ITraverse f a 'Z b
-> (forall (m :: Nat).
    SNatI m =>
    ITraverse f a m b -> ITraverse f a ('S m) b)
-> ITraverse f a n b
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 ITraverse f a 'Z b
start ITraverse f a m b -> ITraverse f a ('S m) b
forall (m :: Nat).
SNatI m =>
ITraverse f a m b -> ITraverse f a ('S m) b
forall (m :: Nat). ITraverse f a m b -> ITraverse f a ('S m) b
step where
    start :: ITraverse f a 'Z b
    start :: ITraverse f a 'Z b
start = ((Wrd 'Z -> a -> f b) -> Tree 'Z a -> f (Tree 'Z b))
-> ITraverse f a 'Z b
forall (f :: * -> *) a (n :: Nat) b.
((Wrd n -> a -> f b) -> Tree n a -> f (Tree n b))
-> ITraverse f a n b
ITraverse (((Wrd 'Z -> a -> f b) -> Tree 'Z a -> f (Tree 'Z b))
 -> ITraverse f a 'Z b)
-> ((Wrd 'Z -> a -> f b) -> Tree 'Z a -> f (Tree 'Z b))
-> ITraverse f a 'Z b
forall a b. (a -> b) -> a -> b
$ \Wrd 'Z -> 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 'Z -> a -> f b
f Wrd 'Z
WE a
x

    step :: ITraverse f a m b -> ITraverse f a ('S m) b
    step :: forall (m :: Nat). ITraverse f a m b -> ITraverse f a ('S m) b
step (ITraverse (Wrd m -> a -> f b) -> Tree m a -> f (Tree m b)
go) = ((Wrd ('S m) -> a -> f b) -> Tree ('S m) a -> f (Tree ('S m) b))
-> ITraverse f a ('S m) b
forall (f :: * -> *) a (n :: Nat) b.
((Wrd n -> a -> f b) -> Tree n a -> f (Tree n b))
-> ITraverse f a n b
ITraverse (((Wrd ('S m) -> a -> f b) -> Tree ('S m) a -> f (Tree ('S m) b))
 -> ITraverse f a ('S m) b)
-> ((Wrd ('S m) -> a -> f b) -> Tree ('S m) a -> f (Tree ('S m) b))
-> ITraverse f a ('S m) b
forall a b. (a -> b) -> a -> b
$ \Wrd ('S m) -> a -> f b
f (Node Tree m a
x Tree m a
y) -> (Tree m b -> Tree m b -> Tree ('S m) b)
-> f (Tree m b) -> f (Tree m b) -> f (Tree ('S m) b)
forall a b c. (a -> b -> c) -> f a -> f b -> f c
forall (f :: * -> *) a b c.
Apply f =>
(a -> b -> c) -> f a -> f b -> f c
liftF2 Tree m b -> Tree m b -> Tree ('S m) b
forall (n :: Nat) a. Tree n a -> Tree n a -> Tree ('S n) a
Node ((Wrd m -> a -> f b) -> Tree m a -> f (Tree m b)
go (Wrd ('S m) -> a -> f b
f (Wrd ('S m) -> a -> f b)
-> (Wrd m -> Wrd ('S m)) -> Wrd m -> a -> f b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrd m -> Wrd ('S m)
forall (n1 :: Nat). Wrd n1 -> Wrd ('S n1)
W0) Tree m a
x) ((Wrd m -> a -> f b) -> Tree m a -> f (Tree m b)
go (Wrd ('S m) -> a -> f b
f (Wrd ('S m) -> a -> f b)
-> (Wrd m -> Wrd ('S m)) -> Wrd m -> a -> f b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrd m -> Wrd ('S m)
forall (n1 :: Nat). Wrd n1 -> Wrd ('S n1)
W1) Tree m a
y)
{-# INLINE itraverse1 #-}
#endif

-- | Apply an action to every element of a 'Tree' and its index, ignoring the results.
itraverse_ :: forall n f a b. (Applicative f, N.SNatI n) => (Wrd n -> a -> f b) -> Tree n a -> f ()
itraverse_ :: forall (n :: Nat) (f :: * -> *) a b.
(Applicative f, SNatI n) =>
(Wrd n -> a -> f b) -> Tree n a -> f ()
itraverse_ = ITraverse_ f a n b -> (Wrd n -> a -> f b) -> Tree n a -> f ()
forall (f :: * -> *) a (n :: Nat) b.
ITraverse_ f a n b -> (Wrd n -> a -> f b) -> Tree n a -> f ()
getITraverse_ (ITraverse_ f a n b -> (Wrd n -> a -> f b) -> Tree n a -> f ())
-> ITraverse_ f a n b -> (Wrd n -> a -> f b) -> Tree n a -> f ()
forall a b. (a -> b) -> a -> b
$ ITraverse_ f a 'Z b
-> (forall (m :: Nat).
    SNatI m =>
    ITraverse_ f a m b -> ITraverse_ f a ('S m) b)
-> ITraverse_ f a n b
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 ITraverse_ f a 'Z b
start ITraverse_ f a m b -> ITraverse_ f a ('S m) b
forall (m :: Nat).
SNatI m =>
ITraverse_ f a m b -> ITraverse_ f a ('S m) b
forall (m :: Nat). ITraverse_ f a m b -> ITraverse_ f a ('S m) b
step where
    start :: ITraverse_ f a 'Z b
    start :: ITraverse_ f a 'Z b
start = ((Wrd 'Z -> a -> f b) -> Tree 'Z a -> f ()) -> ITraverse_ f a 'Z b
forall (f :: * -> *) a (n :: Nat) b.
((Wrd n -> a -> f b) -> Tree n a -> f ()) -> ITraverse_ f a n b
ITraverse_ (((Wrd 'Z -> a -> f b) -> Tree 'Z a -> f ())
 -> ITraverse_ f a 'Z b)
-> ((Wrd 'Z -> a -> f b) -> Tree 'Z a -> f ())
-> ITraverse_ f a 'Z b
forall a b. (a -> b) -> a -> b
$ \Wrd 'Z -> a -> f b
f (Leaf a
x) -> f b -> f ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Wrd 'Z -> a -> f b
f Wrd 'Z
WE a
x)

    step :: ITraverse_ f a m b -> ITraverse_ f a ('S m) b
    step :: forall (m :: Nat). ITraverse_ f a m b -> ITraverse_ f a ('S m) b
step (ITraverse_ (Wrd m -> a -> f b) -> Tree m a -> f ()
go) = ((Wrd ('S m) -> a -> f b) -> Tree ('S m) a -> f ())
-> ITraverse_ f a ('S m) b
forall (f :: * -> *) a (n :: Nat) b.
((Wrd n -> a -> f b) -> Tree n a -> f ()) -> ITraverse_ f a n b
ITraverse_ (((Wrd ('S m) -> a -> f b) -> Tree ('S m) a -> f ())
 -> ITraverse_ f a ('S m) b)
-> ((Wrd ('S m) -> a -> f b) -> Tree ('S m) a -> f ())
-> ITraverse_ f a ('S m) b
forall a b. (a -> b) -> a -> b
$ \Wrd ('S m) -> a -> f b
f (Node Tree m a
x Tree m a
y) -> (Wrd m -> a -> f b) -> Tree m a -> f ()
go (Wrd ('S m) -> a -> f b
f (Wrd ('S m) -> a -> f b)
-> (Wrd m -> Wrd ('S m)) -> Wrd m -> a -> f b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrd m -> Wrd ('S m)
forall (n1 :: Nat). Wrd n1 -> Wrd ('S n1)
W0) Tree m a
x f () -> f () -> f ()
forall a b. f a -> f b -> f b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Wrd m -> a -> f b) -> Tree m a -> f ()
go (Wrd ('S m) -> a -> f b
f (Wrd ('S m) -> a -> f b)
-> (Wrd m -> Wrd ('S m)) -> Wrd m -> a -> f b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrd m -> Wrd ('S m)
forall (n1 :: Nat). Wrd n1 -> Wrd ('S n1)
W1) Tree m a
y

newtype ITraverse_ f a n b = ITraverse_ { forall (f :: * -> *) a (n :: Nat) b.
ITraverse_ f a n b -> (Wrd n -> a -> f b) -> Tree n a -> f ()
getITraverse_ :: (Wrd n -> a -> f b) -> Tree n a -> f () }

-------------------------------------------------------------------------------
-- Folding
-------------------------------------------------------------------------------

-- | See 'I.Foldable'.
foldMap :: forall a n m. (Monoid m, N.SNatI n) => (a -> m) -> Tree n a -> m
foldMap :: forall a (n :: Nat) m.
(Monoid m, SNatI n) =>
(a -> m) -> Tree n a -> m
foldMap a -> m
f = Fold a n m -> Tree n a -> m
forall a (n :: Nat) b. Fold a n b -> Tree n a -> b
getFold (Fold a 'Z m
-> (forall (m :: Nat). SNatI m => Fold a m m -> Fold a ('S m) m)
-> Fold a n m
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 Fold a 'Z m
start Fold a m m -> Fold a ('S m) m
forall (m :: Nat). SNatI m => Fold a m m -> Fold a ('S m) m
forall (p :: Nat). Fold a p m -> Fold a ('S p) m
step) where
    start :: Fold a 'Z m
    start :: Fold a 'Z m
start = (Tree 'Z a -> m) -> Fold a 'Z m
forall a (n :: Nat) b. (Tree n a -> b) -> Fold a n b
Fold ((Tree 'Z a -> m) -> Fold a 'Z m)
-> (Tree 'Z a -> m) -> Fold a 'Z m
forall a b. (a -> b) -> a -> b
$ \(Leaf a
x) -> a -> m
f a
x

    step :: Fold a p m -> Fold a ('S p) m
    step :: forall (p :: Nat). Fold a p m -> Fold a ('S p) m
step (Fold Tree p a -> m
g) = (Tree ('S p) a -> m) -> Fold a ('S p) m
forall a (n :: Nat) b. (Tree n a -> b) -> Fold a n b
Fold ((Tree ('S p) a -> m) -> Fold a ('S p) m)
-> (Tree ('S p) a -> m) -> Fold a ('S p) m
forall a b. (a -> b) -> a -> b
$ \(Node Tree p a
x Tree p a
y) -> Tree p a -> m
g Tree p a
x m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` Tree p a -> m
g Tree p a
y

newtype Fold a n b = Fold  { forall a (n :: Nat) b. Fold a n b -> Tree n a -> b
getFold  :: Tree n a -> b }

-- | See 'I.Foldable1'.
foldMap1 :: forall s a n. (Semigroup s, N.SNatI n) => (a -> s) -> Tree n a -> s
foldMap1 :: forall s a (n :: Nat).
(Semigroup s, SNatI n) =>
(a -> s) -> Tree n a -> s
foldMap1 a -> s
f = Fold a n s -> Tree n a -> s
forall a (n :: Nat) b. Fold a n b -> Tree n a -> b
getFold (Fold a n s -> Tree n a -> s) -> Fold a n s -> Tree n a -> s
forall a b. (a -> b) -> a -> b
$ Fold a 'Z s
-> (forall (m :: Nat). SNatI m => Fold a m s -> Fold a ('S m) s)
-> Fold a n s
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 Fold a 'Z s
start Fold a m s -> Fold a ('S m) s
forall (m :: Nat). SNatI m => Fold a m s -> Fold a ('S m) s
forall (m :: Nat). Fold a m s -> Fold a ('S m) s
step where
    start :: Fold a 'Z s
    start :: Fold a 'Z s
start = (Tree 'Z a -> s) -> Fold a 'Z s
forall a (n :: Nat) b. (Tree n a -> b) -> Fold a n b
Fold ((Tree 'Z a -> s) -> Fold a 'Z s)
-> (Tree 'Z a -> s) -> Fold a 'Z s
forall a b. (a -> b) -> a -> b
$ \(Leaf a
x) -> a -> s
f a
x

    step :: Fold a m s -> Fold a ('S m) s
    step :: forall (m :: Nat). Fold a m s -> Fold a ('S m) s
step (Fold Tree m a -> s
g) = (Tree ('S m) a -> s) -> Fold a ('S m) s
forall a (n :: Nat) b. (Tree n a -> b) -> Fold a n b
Fold ((Tree ('S m) a -> s) -> Fold a ('S m) s)
-> (Tree ('S m) a -> s) -> Fold a ('S m) s
forall a b. (a -> b) -> a -> b
$ \(Node Tree m a
x Tree m a
y) -> Tree m a -> s
g Tree m a
x s -> s -> s
forall a. Semigroup a => a -> a -> a
<> Tree m a -> s
g Tree m a
y

-- | See 'I.FoldableWithIndex'.
ifoldMap :: forall a n m. (Monoid m, N.SNatI n) => (Wrd n -> a -> m) -> Tree n a -> m
ifoldMap :: forall a (n :: Nat) m.
(Monoid m, SNatI n) =>
(Wrd n -> a -> m) -> Tree n a -> m
ifoldMap = IFoldMap a n m -> (Wrd n -> a -> m) -> Tree n a -> m
forall a (n :: Nat) m.
IFoldMap a n m -> (Wrd n -> a -> m) -> Tree n a -> m
getIFoldMap (IFoldMap a n m -> (Wrd n -> a -> m) -> Tree n a -> m)
-> IFoldMap a n m -> (Wrd n -> a -> m) -> Tree n a -> m
forall a b. (a -> b) -> a -> b
$ IFoldMap a 'Z m
-> (forall (m :: Nat).
    SNatI m =>
    IFoldMap a m m -> IFoldMap a ('S m) m)
-> IFoldMap a n m
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 IFoldMap a 'Z m
start IFoldMap a m m -> IFoldMap a ('S m) m
forall (m :: Nat). SNatI m => IFoldMap a m m -> IFoldMap a ('S m) m
forall (p :: Nat). IFoldMap a p m -> IFoldMap a ('S p) m
step where
    start :: IFoldMap a 'Z m
    start :: IFoldMap a 'Z m
start = ((Wrd 'Z -> a -> m) -> Tree 'Z a -> m) -> IFoldMap a 'Z m
forall a (n :: Nat) m.
((Wrd n -> a -> m) -> Tree n a -> m) -> IFoldMap a n m
IFoldMap (((Wrd 'Z -> a -> m) -> Tree 'Z a -> m) -> IFoldMap a 'Z m)
-> ((Wrd 'Z -> a -> m) -> Tree 'Z a -> m) -> IFoldMap a 'Z m
forall a b. (a -> b) -> a -> b
$ \Wrd 'Z -> a -> m
f (Leaf a
x) -> Wrd 'Z -> a -> m
f Wrd 'Z
WE a
x

    step :: IFoldMap a p m -> IFoldMap a ('S p) m
    step :: forall (p :: Nat). IFoldMap a p m -> IFoldMap a ('S p) m
step (IFoldMap (Wrd p -> a -> m) -> Tree p a -> m
go) = ((Wrd ('S p) -> a -> m) -> Tree ('S p) a -> m)
-> IFoldMap a ('S p) m
forall a (n :: Nat) m.
((Wrd n -> a -> m) -> Tree n a -> m) -> IFoldMap a n m
IFoldMap (((Wrd ('S p) -> a -> m) -> Tree ('S p) a -> m)
 -> IFoldMap a ('S p) m)
-> ((Wrd ('S p) -> a -> m) -> Tree ('S p) a -> m)
-> IFoldMap a ('S p) m
forall a b. (a -> b) -> a -> b
$ \Wrd ('S p) -> a -> m
f (Node Tree p a
x Tree p a
y) -> (Wrd p -> a -> m) -> Tree p a -> m
go (Wrd ('S p) -> a -> m
f (Wrd ('S p) -> a -> m) -> (Wrd p -> Wrd ('S p)) -> Wrd p -> a -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrd p -> Wrd ('S p)
forall (n1 :: Nat). Wrd n1 -> Wrd ('S n1)
W0) Tree p a
x m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` (Wrd p -> a -> m) -> Tree p a -> m
go (Wrd ('S p) -> a -> m
f (Wrd ('S p) -> a -> m) -> (Wrd p -> Wrd ('S p)) -> Wrd p -> a -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrd p -> Wrd ('S p)
forall (n1 :: Nat). Wrd n1 -> Wrd ('S n1)
W1) Tree p a
y

newtype IFoldMap a n m = IFoldMap { forall a (n :: Nat) m.
IFoldMap a n m -> (Wrd n -> a -> m) -> Tree n a -> m
getIFoldMap :: (Wrd n -> a -> m) -> Tree n a -> m }

-- | There is no type-class for this :(
ifoldMap1 :: forall a n s. (Semigroup s, N.SNatI n) => (Wrd ('S n) -> a -> s) -> Tree ('S n) a -> s
ifoldMap1 :: forall a (n :: Nat) s.
(Semigroup s, SNatI n) =>
(Wrd ('S n) -> a -> s) -> Tree ('S n) a -> s
ifoldMap1 = IFoldMap a ('S n) s -> (Wrd ('S n) -> a -> s) -> Tree ('S n) a -> s
forall a (n :: Nat) m.
IFoldMap a n m -> (Wrd n -> a -> m) -> Tree n a -> m
getIFoldMap (IFoldMap a ('S n) s
 -> (Wrd ('S n) -> a -> s) -> Tree ('S n) a -> s)
-> IFoldMap a ('S n) s
-> (Wrd ('S n) -> a -> s)
-> Tree ('S n) a
-> s
forall a b. (a -> b) -> a -> b
$ IFoldMap a 'Z s
-> (forall (m :: Nat).
    SNatI m =>
    IFoldMap a m s -> IFoldMap a ('S m) s)
-> IFoldMap a ('S n) s
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 IFoldMap a 'Z s
forall m. IFoldMap a 'Z m
start IFoldMap a m s -> IFoldMap a ('S m) s
forall (m :: Nat). SNatI m => IFoldMap a m s -> IFoldMap a ('S m) s
forall (p :: Nat). IFoldMap a p s -> IFoldMap a ('S p) s
step where
    start :: IFoldMap a 'Z m
    start :: forall m. IFoldMap a 'Z m
start = ((Wrd 'Z -> a -> m) -> Tree 'Z a -> m) -> IFoldMap a 'Z m
forall a (n :: Nat) m.
((Wrd n -> a -> m) -> Tree n a -> m) -> IFoldMap a n m
IFoldMap (((Wrd 'Z -> a -> m) -> Tree 'Z a -> m) -> IFoldMap a 'Z m)
-> ((Wrd 'Z -> a -> m) -> Tree 'Z a -> m) -> IFoldMap a 'Z m
forall a b. (a -> b) -> a -> b
$ \Wrd 'Z -> a -> m
f (Leaf a
x) -> Wrd 'Z -> a -> m
f Wrd 'Z
WE a
x

    step :: IFoldMap a p s -> IFoldMap a ('S p) s
    step :: forall (p :: Nat). IFoldMap a p s -> IFoldMap a ('S p) s
step (IFoldMap (Wrd p -> a -> s) -> Tree p a -> s
go) = ((Wrd ('S p) -> a -> s) -> Tree ('S p) a -> s)
-> IFoldMap a ('S p) s
forall a (n :: Nat) m.
((Wrd n -> a -> m) -> Tree n a -> m) -> IFoldMap a n m
IFoldMap (((Wrd ('S p) -> a -> s) -> Tree ('S p) a -> s)
 -> IFoldMap a ('S p) s)
-> ((Wrd ('S p) -> a -> s) -> Tree ('S p) a -> s)
-> IFoldMap a ('S p) s
forall a b. (a -> b) -> a -> b
$ \Wrd ('S p) -> a -> s
f (Node Tree p a
x Tree p a
y) -> (Wrd p -> a -> s) -> Tree p a -> s
go (Wrd ('S p) -> a -> s
f (Wrd ('S p) -> a -> s) -> (Wrd p -> Wrd ('S p)) -> Wrd p -> a -> s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrd p -> Wrd ('S p)
forall (n1 :: Nat). Wrd n1 -> Wrd ('S n1)
W0) Tree p a
x s -> s -> s
forall a. Semigroup a => a -> a -> a
<> (Wrd p -> a -> s) -> Tree p a -> s
go (Wrd ('S p) -> a -> s
f (Wrd ('S p) -> a -> s) -> (Wrd p -> Wrd ('S p)) -> Wrd p -> a -> s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrd p -> Wrd ('S p)
forall (n1 :: Nat). Wrd n1 -> Wrd ('S n1)
W1) Tree p a
y




-- | Right fold.
foldr :: forall a b n. N.SNatI n => (a -> b -> b) -> b -> Tree n a -> b
foldr :: forall a b (n :: Nat).
SNatI n =>
(a -> b -> b) -> b -> Tree n a -> b
foldr a -> b -> b
f = Foldr a n b -> b -> Tree n a -> b
forall a (n :: Nat) b. Foldr a n b -> b -> Tree n a -> b
getFoldr (Foldr a 'Z b
-> (forall (m :: Nat). SNatI m => Foldr a m b -> Foldr a ('S m) b)
-> Foldr a n b
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 Foldr a 'Z b
start Foldr a m b -> Foldr a ('S m) b
forall (m :: Nat). SNatI m => Foldr a m b -> Foldr a ('S m) b
forall (m :: Nat). Foldr a m b -> Foldr a ('S m) b
step) where
    start :: Foldr a 'Z b
    start :: Foldr a 'Z b
start = (b -> Tree 'Z a -> b) -> Foldr a 'Z b
forall a (n :: Nat) b. (b -> Tree n a -> b) -> Foldr a n b
Foldr ((b -> Tree 'Z a -> b) -> Foldr a 'Z b)
-> (b -> Tree 'Z a -> b) -> Foldr a 'Z b
forall a b. (a -> b) -> a -> b
$ \b
z (Leaf a
x) -> a -> b -> b
f a
x b
z

    step :: Foldr a m b -> Foldr a ('S m) b
    step :: forall (m :: Nat). Foldr a m b -> Foldr a ('S m) b
step (Foldr b -> Tree m a -> b
go) = (b -> Tree ('S m) a -> b) -> Foldr a ('S m) b
forall a (n :: Nat) b. (b -> Tree n a -> b) -> Foldr a n b
Foldr ((b -> Tree ('S m) a -> b) -> Foldr a ('S m) b)
-> (b -> Tree ('S m) a -> b) -> Foldr a ('S m) b
forall a b. (a -> b) -> a -> b
$ \b
z (Node Tree m a
x Tree m a
y) -> b -> Tree m a -> b
go (b -> Tree m a -> b
go b
z Tree m a
y) Tree m a
x

newtype Foldr a n b = Foldr { forall a (n :: Nat) b. Foldr a n b -> b -> Tree n a -> b
getFoldr :: b -> Tree n a -> b }

-- | Right fold with an index.
ifoldr :: forall a b n. N.SNatI n => (Wrd n -> a -> b -> b) -> b -> Tree n a -> b
ifoldr :: forall a b (n :: Nat).
SNatI n =>
(Wrd n -> a -> b -> b) -> b -> Tree n a -> b
ifoldr = IFoldr a n b -> (Wrd n -> a -> b -> b) -> b -> Tree n a -> b
forall a (n :: Nat) b.
IFoldr a n b -> (Wrd n -> a -> b -> b) -> b -> Tree n a -> b
getIFoldr (IFoldr a n b -> (Wrd n -> a -> b -> b) -> b -> Tree n a -> b)
-> IFoldr a n b -> (Wrd n -> a -> b -> b) -> b -> Tree n a -> b
forall a b. (a -> b) -> a -> b
$ IFoldr a 'Z b
-> (forall (m :: Nat).
    SNatI m =>
    IFoldr a m b -> IFoldr a ('S m) b)
-> IFoldr a n b
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 IFoldr a 'Z b
start IFoldr a m b -> IFoldr a ('S m) b
forall (m :: Nat). SNatI m => IFoldr a m b -> IFoldr a ('S m) b
forall (m :: Nat). IFoldr a m b -> IFoldr a ('S m) b
step where
    start :: IFoldr a 'Z b
    start :: IFoldr a 'Z b
start = ((Wrd 'Z -> a -> b -> b) -> b -> Tree 'Z a -> b) -> IFoldr a 'Z b
forall a (n :: Nat) b.
((Wrd n -> a -> b -> b) -> b -> Tree n a -> b) -> IFoldr a n b
IFoldr (((Wrd 'Z -> a -> b -> b) -> b -> Tree 'Z a -> b) -> IFoldr a 'Z b)
-> ((Wrd 'Z -> a -> b -> b) -> b -> Tree 'Z a -> b)
-> IFoldr a 'Z b
forall a b. (a -> b) -> a -> b
$ \Wrd 'Z -> a -> b -> b
f b
z (Leaf a
x) -> Wrd 'Z -> a -> b -> b
f Wrd 'Z
WE a
x b
z

    step :: IFoldr a m b -> IFoldr a ('S m) b
    step :: forall (m :: Nat). IFoldr a m b -> IFoldr a ('S m) b
step (IFoldr (Wrd m -> a -> b -> b) -> b -> Tree m a -> b
go) = ((Wrd ('S m) -> a -> b -> b) -> b -> Tree ('S m) a -> b)
-> IFoldr a ('S m) b
forall a (n :: Nat) b.
((Wrd n -> a -> b -> b) -> b -> Tree n a -> b) -> IFoldr a n b
IFoldr (((Wrd ('S m) -> a -> b -> b) -> b -> Tree ('S m) a -> b)
 -> IFoldr a ('S m) b)
-> ((Wrd ('S m) -> a -> b -> b) -> b -> Tree ('S m) a -> b)
-> IFoldr a ('S m) b
forall a b. (a -> b) -> a -> b
$ \Wrd ('S m) -> a -> b -> b
f b
z (Node Tree m a
x Tree m a
y) -> (Wrd m -> a -> b -> b) -> b -> Tree m a -> b
go (Wrd ('S m) -> a -> b -> b
f (Wrd ('S m) -> a -> b -> b)
-> (Wrd m -> Wrd ('S m)) -> Wrd m -> a -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrd m -> Wrd ('S m)
forall (n1 :: Nat). Wrd n1 -> Wrd ('S n1)
W0) ((Wrd m -> a -> b -> b) -> b -> Tree m a -> b
go (Wrd ('S m) -> a -> b -> b
f (Wrd ('S m) -> a -> b -> b)
-> (Wrd m -> Wrd ('S m)) -> Wrd m -> a -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrd m -> Wrd ('S m)
forall (n1 :: Nat). Wrd n1 -> Wrd ('S n1)
W1) b
z Tree m a
y) Tree m a
x

newtype IFoldr a n b = IFoldr { forall a (n :: Nat) b.
IFoldr a n b -> (Wrd n -> a -> b -> b) -> b -> Tree n a -> b
getIFoldr :: (Wrd n -> a -> b -> b) -> b -> Tree n a -> b }

foldr1Map :: forall a b n. N.SNatI n => (a -> b -> b) -> (a -> b) -> Tree n a -> b
foldr1Map :: forall a b (n :: Nat).
SNatI n =>
(a -> b -> b) -> (a -> b) -> Tree n a -> b
foldr1Map a -> b -> b
f = Foldr1 a n b -> (a -> b) -> Tree n a -> b
forall a (n :: Nat) b. Foldr1 a n b -> (a -> b) -> Tree n a -> b
getFoldr1 (Foldr1 a 'Z b
-> (forall (m :: Nat).
    SNatI m =>
    Foldr1 a m b -> Foldr1 a ('S m) b)
-> Foldr1 a n b
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 Foldr1 a 'Z b
start Foldr1 a m b -> Foldr1 a ('S m) b
forall (m :: Nat). SNatI m => Foldr1 a m b -> Foldr1 a ('S m) b
forall (m :: Nat). Foldr1 a m b -> Foldr1 a ('S m) b
step) where
    start :: Foldr1 a 'Z b
    start :: Foldr1 a 'Z b
start = ((a -> b) -> Tree 'Z a -> b) -> Foldr1 a 'Z b
forall a (n :: Nat) b. ((a -> b) -> Tree n a -> b) -> Foldr1 a n b
Foldr1 (((a -> b) -> Tree 'Z a -> b) -> Foldr1 a 'Z b)
-> ((a -> b) -> Tree 'Z a -> b) -> Foldr1 a 'Z b
forall a b. (a -> b) -> a -> b
$ \a -> b
z (Leaf a
x) -> a -> b
z a
x

    step :: Foldr1 a m b -> Foldr1 a ('S m) b
    step :: forall (m :: Nat). Foldr1 a m b -> Foldr1 a ('S m) b
step (Foldr1 (a -> b) -> Tree m a -> b
go) = ((a -> b) -> Tree ('S m) a -> b) -> Foldr1 a ('S m) b
forall a (n :: Nat) b. ((a -> b) -> Tree n a -> b) -> Foldr1 a n b
Foldr1 (((a -> b) -> Tree ('S m) a -> b) -> Foldr1 a ('S m) b)
-> ((a -> b) -> Tree ('S m) a -> b) -> Foldr1 a ('S m) b
forall a b. (a -> b) -> a -> b
$ \a -> b
z (Node Tree m a
x Tree m a
y) -> (a -> b) -> Tree m a -> b
go (\a
z0 -> a -> b -> b
f a
z0 ((a -> b) -> Tree m a -> b
go a -> b
z Tree m a
y)) Tree m a
x

newtype Foldr1 a n b = Foldr1 { forall a (n :: Nat) b. Foldr1 a n b -> (a -> b) -> Tree n a -> b
getFoldr1 :: (a -> b) -> Tree n a -> b }

ifoldr1Map :: (Wrd n -> a -> b -> b) -> (Wrd n -> a -> b) -> Tree n a -> b
ifoldr1Map :: forall (n :: Nat) a b.
(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
forall (n :: Nat) a b.
(Wrd n -> a -> b -> b) -> (Wrd n -> a -> b) -> Tree n a -> b
ifoldr1Map

-- | Left fold.
foldl :: forall a b n. N.SNatI n => (b -> a -> b) -> b -> Tree n a -> b
foldl :: forall a b (n :: Nat).
SNatI n =>
(b -> a -> b) -> b -> Tree n a -> b
foldl b -> a -> b
f = Foldl a n b -> b -> Tree n a -> b
forall a (n :: Nat) b. Foldl a n b -> b -> Tree n a -> b
getFoldl (Foldl a 'Z b
-> (forall (m :: Nat). SNatI m => Foldl a m b -> Foldl a ('S m) b)
-> Foldl a n b
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 Foldl a 'Z b
start Foldl a m b -> Foldl a ('S m) b
forall (m :: Nat). SNatI m => Foldl a m b -> Foldl a ('S m) b
forall (m :: Nat). Foldl a m b -> Foldl a ('S m) b
step) where
    start :: Foldl a 'Z b
    start :: Foldl a 'Z b
start = (b -> Tree 'Z a -> b) -> Foldl a 'Z b
forall a (n :: Nat) b. (b -> Tree n a -> b) -> Foldl a n b
Foldl ((b -> Tree 'Z a -> b) -> Foldl a 'Z b)
-> (b -> Tree 'Z a -> b) -> Foldl a 'Z b
forall a b. (a -> b) -> a -> b
$ \b
z (Leaf a
x) -> b -> a -> b
f b
z a
x

    step :: Foldl a m b -> Foldl a ('S m) b
    step :: forall (m :: Nat). Foldl a m b -> Foldl a ('S m) b
step (Foldl b -> Tree m a -> b
go) = (b -> Tree ('S m) a -> b) -> Foldl a ('S m) b
forall a (n :: Nat) b. (b -> Tree n a -> b) -> Foldl a n b
Foldl ((b -> Tree ('S m) a -> b) -> Foldl a ('S m) b)
-> (b -> Tree ('S m) a -> b) -> Foldl a ('S m) b
forall a b. (a -> b) -> a -> b
$ \b
z (Node Tree m a
x Tree m a
y) -> b -> Tree m a -> b
go (b -> Tree m a -> b
go b
z Tree m a
x) Tree m a
y

newtype Foldl a n b = Foldl { forall a (n :: Nat) b. Foldl a n b -> b -> Tree n a -> b
getFoldl :: b -> Tree n a -> b }

-- | Left fold with an index.
ifoldl :: forall a b n. N.SNatI n => (Wrd n -> b -> a -> b) -> b -> Tree n a -> b
ifoldl :: forall a b (n :: Nat).
SNatI n =>
(Wrd n -> b -> a -> b) -> b -> Tree n a -> b
ifoldl = IFoldl a n b -> (Wrd n -> b -> a -> b) -> b -> Tree n a -> b
forall a (n :: Nat) b.
IFoldl a n b -> (Wrd n -> b -> a -> b) -> b -> Tree n a -> b
getIFoldl (IFoldl a n b -> (Wrd n -> b -> a -> b) -> b -> Tree n a -> b)
-> IFoldl a n b -> (Wrd n -> b -> a -> b) -> b -> Tree n a -> b
forall a b. (a -> b) -> a -> b
$ IFoldl a 'Z b
-> (forall (m :: Nat).
    SNatI m =>
    IFoldl a m b -> IFoldl a ('S m) b)
-> IFoldl a n b
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 IFoldl a 'Z b
start IFoldl a m b -> IFoldl a ('S m) b
forall (m :: Nat). SNatI m => IFoldl a m b -> IFoldl a ('S m) b
forall (m :: Nat). IFoldl a m b -> IFoldl a ('S m) b
step where
    start :: IFoldl a 'Z b
    start :: IFoldl a 'Z b
start = ((Wrd 'Z -> b -> a -> b) -> b -> Tree 'Z a -> b) -> IFoldl a 'Z b
forall a (n :: Nat) b.
((Wrd n -> b -> a -> b) -> b -> Tree n a -> b) -> IFoldl a n b
IFoldl (((Wrd 'Z -> b -> a -> b) -> b -> Tree 'Z a -> b) -> IFoldl a 'Z b)
-> ((Wrd 'Z -> b -> a -> b) -> b -> Tree 'Z a -> b)
-> IFoldl a 'Z b
forall a b. (a -> b) -> a -> b
$ \Wrd 'Z -> b -> a -> b
f b
z (Leaf a
x) -> Wrd 'Z -> b -> a -> b
f Wrd 'Z
WE b
z a
x

    step :: IFoldl a m b -> IFoldl a ('S m) b
    step :: forall (m :: Nat). IFoldl a m b -> IFoldl a ('S m) b
step (IFoldl (Wrd m -> b -> a -> b) -> b -> Tree m a -> b
go) = ((Wrd ('S m) -> b -> a -> b) -> b -> Tree ('S m) a -> b)
-> IFoldl a ('S m) b
forall a (n :: Nat) b.
((Wrd n -> b -> a -> b) -> b -> Tree n a -> b) -> IFoldl a n b
IFoldl (((Wrd ('S m) -> b -> a -> b) -> b -> Tree ('S m) a -> b)
 -> IFoldl a ('S m) b)
-> ((Wrd ('S m) -> b -> a -> b) -> b -> Tree ('S m) a -> b)
-> IFoldl a ('S m) b
forall a b. (a -> b) -> a -> b
$ \Wrd ('S m) -> b -> a -> b
f b
z (Node Tree m a
x Tree m a
y) -> (Wrd m -> b -> a -> b) -> b -> Tree m a -> b
go (Wrd ('S m) -> b -> a -> b
f (Wrd ('S m) -> b -> a -> b)
-> (Wrd m -> Wrd ('S m)) -> Wrd m -> b -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrd m -> Wrd ('S m)
forall (n1 :: Nat). Wrd n1 -> Wrd ('S n1)
W0) ((Wrd m -> b -> a -> b) -> b -> Tree m a -> b
go (Wrd ('S m) -> b -> a -> b
f (Wrd ('S m) -> b -> a -> b)
-> (Wrd m -> Wrd ('S m)) -> Wrd m -> b -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrd m -> Wrd ('S m)
forall (n1 :: Nat). Wrd n1 -> Wrd ('S n1)
W1) b
z Tree m a
x) Tree m a
y

newtype IFoldl a n b = IFoldl { forall a (n :: Nat) b.
IFoldl a n b -> (Wrd n -> b -> a -> b) -> b -> Tree n a -> b
getIFoldl :: (Wrd n -> b -> a -> b) -> b -> Tree n a -> b }

-- | Yield the length of a 'Tree'. /O(n)/
length :: forall n a. N.SNatI n => Tree n a -> Int
length :: forall (n :: Nat) a. SNatI n => Tree n a -> Int
length Tree n a
_ = Length n -> Int
forall (n :: Nat). Length n -> Int
getLength Length n
l where
    l :: Length n
    l :: Length n
l = Length 'Z
-> (forall {m :: Nat}. SNatI m => Length m -> Length ('S m))
-> Length n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
forall (f :: Nat -> *).
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction (Int -> Length 'Z
forall (n :: Nat). Int -> Length n
Length Int
1) ((forall {m :: Nat}. SNatI m => Length m -> Length ('S m))
 -> Length n)
-> (forall {m :: Nat}. SNatI m => Length m -> Length ('S m))
-> Length n
forall a b. (a -> b) -> a -> b
$ \(Length Int
n) -> Int -> Length ('S m)
forall (n :: Nat). Int -> Length n
Length (Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
n)

newtype Length (n :: Nat) = Length { forall (n :: Nat). Length n -> Int
getLength :: Int }

-- | Test whether a 'Tree' is empty. It never is. /O(1)/
null :: Tree n a -> Bool
null :: forall (n :: Nat) a. Tree n a -> Bool
null Tree n a
_ = Bool
False

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

-- | Non-strict 'sum'.
sum :: (Num a, N.SNatI n) => Tree n a -> a
sum :: forall a (n :: Nat). (Num a, SNatI n) => Tree n a -> a
sum = Fold a n a -> Tree n a -> a
forall a (n :: Nat) b. Fold a n b -> Tree n a -> b
getFold (Fold a n a -> Tree n a -> a) -> Fold a n a -> Tree n a -> a
forall a b. (a -> b) -> a -> b
$ Fold a 'Z a
-> (forall (m :: Nat). SNatI m => Fold a m a -> Fold a ('S m) a)
-> Fold a 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 Fold a 'Z a
forall a. Num a => Fold a 'Z a
start Fold a m a -> Fold a ('S m) a
forall a (m :: Nat). Num a => Fold a m a -> Fold a ('S m) a
forall (m :: Nat). SNatI m => Fold a m a -> Fold a ('S m) a
step where
    start :: Num a => Fold a 'Z a
    start :: forall a. Num a => Fold a 'Z a
start = (Tree 'Z a -> a) -> Fold a 'Z a
forall a (n :: Nat) b. (Tree n a -> b) -> Fold a n b
Fold ((Tree 'Z a -> a) -> Fold a 'Z a)
-> (Tree 'Z a -> a) -> Fold a 'Z a
forall a b. (a -> b) -> a -> b
$ \(Leaf a
x) -> a
x

    step :: Num a => Fold a m a -> Fold a ('S m) a
    step :: forall a (m :: Nat). Num a => Fold a m a -> Fold a ('S m) a
step (Fold Tree m a -> a
f) = (Tree ('S m) a -> a) -> Fold a ('S m) a
forall a (n :: Nat) b. (Tree n a -> b) -> Fold a n b
Fold ((Tree ('S m) a -> a) -> Fold a ('S m) a)
-> (Tree ('S m) a -> a) -> Fold a ('S m) a
forall a b. (a -> b) -> a -> b
$ \(Node Tree m a
x Tree m a
y) -> Tree m a -> a
f Tree m a
x a -> a -> a
forall a. Num a => a -> a -> a
+ Tree m a -> a
f Tree m a
y

-- | Non-strict 'product'.
product :: (Num a, N.SNatI n) => Tree n a -> a
product :: forall a (n :: Nat). (Num a, SNatI n) => Tree n a -> a
product = Fold a n a -> Tree n a -> a
forall a (n :: Nat) b. Fold a n b -> Tree n a -> b
getFold (Fold a n a -> Tree n a -> a) -> Fold a n a -> Tree n a -> a
forall a b. (a -> b) -> a -> b
$ Fold a 'Z a
-> (forall (m :: Nat). SNatI m => Fold a m a -> Fold a ('S m) a)
-> Fold a 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 Fold a 'Z a
forall a. Num a => Fold a 'Z a
start Fold a m a -> Fold a ('S m) a
forall a (m :: Nat). Num a => Fold a m a -> Fold a ('S m) a
forall (m :: Nat). SNatI m => Fold a m a -> Fold a ('S m) a
step where
    start :: Num a => Fold a 'Z a
    start :: forall a. Num a => Fold a 'Z a
start = (Tree 'Z a -> a) -> Fold a 'Z a
forall a (n :: Nat) b. (Tree n a -> b) -> Fold a n b
Fold ((Tree 'Z a -> a) -> Fold a 'Z a)
-> (Tree 'Z a -> a) -> Fold a 'Z a
forall a b. (a -> b) -> a -> b
$ \(Leaf a
x) -> a
x

    step :: Num a => Fold a m a -> Fold a ('S m) a
    step :: forall a (m :: Nat). Num a => Fold a m a -> Fold a ('S m) a
step (Fold Tree m a -> a
f) = (Tree ('S m) a -> a) -> Fold a ('S m) a
forall a (n :: Nat) b. (Tree n a -> b) -> Fold a n b
Fold ((Tree ('S m) a -> a) -> Fold a ('S m) a)
-> (Tree ('S m) a -> a) -> Fold a ('S m) a
forall a b. (a -> b) -> a -> b
$ \(Node Tree m a
x Tree m a
y) -> Tree m a -> a
f Tree m a
x a -> a -> a
forall a. Num a => a -> a -> a
* Tree m a -> a
f Tree m a
y

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

-- | Zip two 'Tree's with a function.
zipWith :: forall a b c n. N.SNatI n => (a -> b -> c) -> Tree n a -> Tree n b -> Tree n c
zipWith :: forall a b c (n :: Nat).
SNatI n =>
(a -> b -> c) -> Tree n a -> Tree n b -> Tree n c
zipWith a -> b -> c
f = ZipWith a b c n -> Tree n a -> Tree n b -> Tree n c
forall a b c (n :: Nat).
ZipWith a b c n -> Tree n a -> Tree n b -> Tree n c
getZipWith (ZipWith a b c n -> Tree n a -> Tree n b -> Tree n c)
-> ZipWith a b c n -> Tree n a -> Tree n b -> Tree n c
forall a b. (a -> b) -> a -> b
$ ZipWith a b c 'Z
-> (forall (m :: Nat).
    SNatI m =>
    ZipWith a b c m -> ZipWith a b c ('S m))
-> ZipWith a b c n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
forall (f :: Nat -> *).
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction ZipWith a b c 'Z
start ZipWith a b c m -> ZipWith a b c ('S m)
forall (m :: Nat).
SNatI m =>
ZipWith a b c m -> ZipWith a b c ('S m)
forall (m :: Nat). ZipWith a b c m -> ZipWith a b c ('S m)
step where
    start :: ZipWith a b c 'Z
    start :: ZipWith a b c 'Z
start = (Tree 'Z a -> Tree 'Z b -> Tree 'Z c) -> ZipWith a b c 'Z
forall a b c (n :: Nat).
(Tree n a -> Tree n b -> Tree n c) -> ZipWith a b c n
ZipWith ((Tree 'Z a -> Tree 'Z b -> Tree 'Z c) -> ZipWith a b c 'Z)
-> (Tree 'Z a -> Tree 'Z b -> Tree 'Z c) -> ZipWith a b c 'Z
forall a b. (a -> b) -> a -> b
$ \(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)

    step :: ZipWith a b c m -> ZipWith a b c ('S m)
    step :: forall (m :: Nat). ZipWith a b c m -> ZipWith a b c ('S m)
step (ZipWith Tree m a -> Tree m b -> Tree m c
go) = (Tree ('S m) a -> Tree ('S m) b -> Tree ('S m) c)
-> ZipWith a b c ('S m)
forall a b c (n :: Nat).
(Tree n a -> Tree n b -> Tree n c) -> ZipWith a b c n
ZipWith ((Tree ('S m) a -> Tree ('S m) b -> Tree ('S m) c)
 -> ZipWith a b c ('S m))
-> (Tree ('S m) a -> Tree ('S m) b -> Tree ('S m) c)
-> ZipWith a b c ('S m)
forall a b. (a -> b) -> a -> b
$ \(Node Tree m a
x Tree m a
y) (Node Tree m b
u Tree m b
v) -> Tree m c -> Tree m c -> Tree ('S m) c
forall (n :: Nat) a. Tree n a -> Tree n a -> Tree ('S n) a
Node (Tree m a -> Tree m b -> Tree m c
go Tree m a
x Tree m b
u) (Tree m a -> Tree m b -> Tree m c
go Tree m a
y Tree m b
v)

newtype ZipWith a b c n = ZipWith { forall a b c (n :: Nat).
ZipWith a b c n -> Tree n a -> Tree n b -> Tree n c
getZipWith :: Tree n a -> Tree n b -> Tree n c }

-- | Zip two 'Tree's. with a function that also takes the elements' indices.
izipWith :: N.SNatI n => (Wrd n -> a -> b -> c) -> Tree n a -> Tree n b -> Tree n c
izipWith :: forall (n :: Nat) a b c.
SNatI n =>
(Wrd n -> a -> b -> c) -> Tree n a -> Tree n b -> Tree n c
izipWith = IZipWith a b c n
-> (Wrd n -> a -> b -> c) -> Tree n a -> Tree n b -> Tree n c
forall a b c (n :: Nat).
IZipWith a b c n
-> (Wrd n -> a -> b -> c) -> Tree n a -> Tree n b -> Tree n c
getIZipWith (IZipWith a b c n
 -> (Wrd n -> a -> b -> c) -> Tree n a -> Tree n b -> Tree n c)
-> IZipWith a b c n
-> (Wrd n -> a -> b -> c)
-> Tree n a
-> Tree n b
-> Tree n c
forall a b. (a -> b) -> a -> b
$ IZipWith a b c 'Z
-> (forall (m :: Nat).
    SNatI m =>
    IZipWith a b c m -> IZipWith a b c ('S m))
-> IZipWith a b c n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
forall (f :: Nat -> *).
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction IZipWith a b c 'Z
forall a b c. IZipWith a b c 'Z
start IZipWith a b c m -> IZipWith a b c ('S m)
forall a b c (m :: Nat). IZipWith a b c m -> IZipWith a b c ('S m)
forall (m :: Nat).
SNatI m =>
IZipWith a b c m -> IZipWith a b c ('S m)
step where
    start :: IZipWith a b c 'Z
    start :: forall a b c. IZipWith a b c 'Z
start = ((Wrd 'Z -> a -> b -> c) -> Tree 'Z a -> Tree 'Z b -> Tree 'Z c)
-> IZipWith a b c 'Z
forall a b c (n :: Nat).
((Wrd n -> a -> b -> c) -> Tree n a -> Tree n b -> Tree n c)
-> IZipWith a b c n
IZipWith (((Wrd 'Z -> a -> b -> c) -> Tree 'Z a -> Tree 'Z b -> Tree 'Z c)
 -> IZipWith a b c 'Z)
-> ((Wrd 'Z -> a -> b -> c) -> Tree 'Z a -> Tree 'Z b -> Tree 'Z c)
-> IZipWith a b c 'Z
forall a b. (a -> b) -> a -> b
$ \Wrd 'Z -> a -> b -> c
f (Leaf a
x) (Leaf b
y) -> c -> Tree 'Z c
forall a. a -> Tree 'Z a
Leaf (Wrd 'Z -> a -> b -> c
f Wrd 'Z
WE a
x b
y)

    step :: IZipWith a b c m -> IZipWith a b c ('S m)
    step :: forall a b c (m :: Nat). IZipWith a b c m -> IZipWith a b c ('S m)
step (IZipWith (Wrd m -> a -> b -> c) -> Tree m a -> Tree m b -> Tree m c
go) = ((Wrd ('S m) -> a -> b -> c)
 -> Tree ('S m) a -> Tree ('S m) b -> Tree ('S m) c)
-> IZipWith a b c ('S m)
forall a b c (n :: Nat).
((Wrd n -> a -> b -> c) -> Tree n a -> Tree n b -> Tree n c)
-> IZipWith a b c n
IZipWith (((Wrd ('S m) -> a -> b -> c)
  -> Tree ('S m) a -> Tree ('S m) b -> Tree ('S m) c)
 -> IZipWith a b c ('S m))
-> ((Wrd ('S m) -> a -> b -> c)
    -> Tree ('S m) a -> Tree ('S m) b -> Tree ('S m) c)
-> IZipWith a b c ('S m)
forall a b. (a -> b) -> a -> b
$ \Wrd ('S m) -> a -> b -> c
f (Node Tree m a
x Tree m a
y) (Node Tree m b
u Tree m b
v) -> Tree m c -> Tree m c -> Tree ('S m) c
forall (n :: Nat) a. Tree n a -> Tree n a -> Tree ('S n) a
Node ((Wrd m -> a -> b -> c) -> Tree m a -> Tree m b -> Tree m c
go (Wrd ('S m) -> a -> b -> c
f (Wrd ('S m) -> a -> b -> c)
-> (Wrd m -> Wrd ('S m)) -> Wrd m -> a -> b -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrd m -> Wrd ('S m)
forall (n1 :: Nat). Wrd n1 -> Wrd ('S n1)
W0) Tree m a
x Tree m b
u) ((Wrd m -> a -> b -> c) -> Tree m a -> Tree m b -> Tree m c
go (Wrd ('S m) -> a -> b -> c
f (Wrd ('S m) -> a -> b -> c)
-> (Wrd m -> Wrd ('S m)) -> Wrd m -> a -> b -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrd m -> Wrd ('S m)
forall (n1 :: Nat). Wrd n1 -> Wrd ('S n1)
W1) Tree m a
y Tree m b
v)

newtype IZipWith a b c n = IZipWith { forall a b c (n :: Nat).
IZipWith a b c n
-> (Wrd n -> a -> b -> c) -> Tree n a -> Tree n b -> Tree n c
getIZipWith :: (Wrd n -> a -> b -> c) -> Tree n a -> Tree n b -> Tree n c }

-- | Repeat value
--
-- >>> repeat 'x' :: Tree N.Nat2 Char
-- Node (Node (Leaf 'x') (Leaf 'x')) (Node (Leaf 'x') (Leaf 'x'))
--
repeat :: N.SNatI n => x -> Tree n x
repeat :: forall (n :: Nat) x. SNatI n => x -> Tree n x
repeat x
x = Tree 'Z x
-> (forall {m :: Nat}. SNatI m => Tree m x -> Tree ('S m) x)
-> Tree n x
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 (x -> Tree 'Z x
forall a. a -> Tree 'Z a
Leaf x
x) ((forall {m :: Nat}. SNatI m => Tree m x -> Tree ('S m) x)
 -> Tree n x)
-> (forall {m :: Nat}. SNatI m => Tree m x -> Tree ('S m) x)
-> Tree n x
forall a b. (a -> b) -> a -> b
$ \Tree m x
t -> Tree m x -> Tree m x -> Tree ('S m) x
forall (n :: Nat) a. Tree n a -> Tree n a -> Tree ('S n) a
Node Tree m x
t Tree m x
t

-------------------------------------------------------------------------------
-- Monadic
-------------------------------------------------------------------------------

-- TODO

-------------------------------------------------------------------------------
-- universe
-------------------------------------------------------------------------------

-- | Get all @'Wrd' n@ in a @'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 :: forall (n :: Nat). SNatI n => 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

-------------------------------------------------------------------------------
-- EnsureSpine
-------------------------------------------------------------------------------

-- | Ensure spine.
--
-- If we have an undefined 'Tree',
--
-- >>> let v = error "err" :: Tree N.Nat2 Char
--
-- And insert data into it later:
--
-- >>> let setHead :: a -> Tree N.Nat2 a -> Tree N.Nat2 a; setHead x (Node (Node _ u) v) = Node (Node (Leaf x) u) v
--
-- Then without a spine, it will fail:
--
-- >>> leftmost $ setHead 'x' v
-- *** Exception: err
-- ...
--
-- But with the spine, it won't:
--
-- >>> leftmost $ setHead 'x' $ ensureSpine v
-- 'x'
--
ensureSpine :: N.SNatI n => Tree n a -> Tree n a
ensureSpine :: forall (n :: Nat) a. SNatI n => Tree n a -> Tree n a
ensureSpine = EnsureSpine n a -> Tree n a -> Tree n a
forall (n :: Nat) a. EnsureSpine n a -> Tree n a -> Tree n a
getEnsureSpine (EnsureSpine 'Z a
-> (forall (m :: Nat).
    SNatI m =>
    EnsureSpine m a -> EnsureSpine ('S m) a)
-> EnsureSpine 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 EnsureSpine 'Z a
forall a. EnsureSpine 'Z a
first EnsureSpine m a -> EnsureSpine ('S m) a
forall (m :: Nat).
SNatI m =>
EnsureSpine m a -> EnsureSpine ('S m) a
forall (m :: Nat) a. EnsureSpine m a -> EnsureSpine ('S m) a
step) where
    first :: EnsureSpine 'Z a
    first :: forall a. EnsureSpine 'Z a
first = (Tree 'Z a -> Tree 'Z a) -> EnsureSpine 'Z a
forall (n :: Nat) a. (Tree n a -> Tree n a) -> EnsureSpine n a
EnsureSpine ((Tree 'Z a -> Tree 'Z a) -> EnsureSpine 'Z a)
-> (Tree 'Z a -> Tree 'Z a) -> EnsureSpine 'Z a
forall a b. (a -> b) -> a -> b
$ \ ~(Leaf a
x) -> a -> Tree 'Z a
forall a. a -> Tree 'Z a
Leaf a
x

    step :: EnsureSpine m a -> EnsureSpine ('S m) a
    step :: forall (m :: Nat) a. EnsureSpine m a -> EnsureSpine ('S m) a
step (EnsureSpine Tree m a -> Tree m a
go) = (Tree ('S m) a -> Tree ('S m) a) -> EnsureSpine ('S m) a
forall (n :: Nat) a. (Tree n a -> Tree n a) -> EnsureSpine n a
EnsureSpine ((Tree ('S m) a -> Tree ('S m) a) -> EnsureSpine ('S m) a)
-> (Tree ('S m) a -> Tree ('S m) a) -> EnsureSpine ('S m) a
forall a b. (a -> b) -> a -> b
$ \ ~(Node Tree m a
x Tree m a
y) -> 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
go Tree m a
x) (Tree m a -> Tree m a
go Tree m a
y)

newtype EnsureSpine n a = EnsureSpine { forall (n :: Nat) a. EnsureSpine n a -> Tree n a -> Tree n a
getEnsureSpine :: Tree n a -> Tree n a }

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

instance N.SNatI n => QC.Arbitrary1 (Tree n) where
    liftArbitrary :: forall a. 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 :: forall a. (a -> [a]) -> Tree n a -> [Tree n a]
liftShrink    = (a -> [a]) -> Tree n a -> [Tree n a]
forall (n :: Nat) a.
SNatI n =>
(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 :: forall (n :: Nat) a. SNatI n => 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 Arb 'Z a
start Arb m a -> Arb ('S m) a
forall (m :: Nat). SNatI m => Arb m a -> Arb ('S m) a
forall (m :: Nat). Arb m a -> Arb ('S m) a
step where
    start :: Arb 'Z a
    start :: Arb 'Z a
start = Gen (Tree 'Z a) -> Arb 'Z a
forall (n :: Nat) a. Gen (Tree n a) -> Arb n a
Arb (Gen (Tree 'Z a) -> Arb 'Z a) -> Gen (Tree 'Z a) -> Arb 'Z a
forall a b. (a -> b) -> a -> b
$ a -> Tree 'Z a
forall a. a -> Tree 'Z a
Leaf (a -> Tree 'Z a) -> Gen a -> Gen (Tree 'Z a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen a
arb

    step :: Arb m a -> Arb ('S m) a
    step :: forall (m :: Nat). 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)
-> Gen (Tree m a) -> Gen (Tree m a) -> Gen (Tree ('S m) a)
forall a b c. (a -> b -> c) -> Gen a -> Gen b -> Gen c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 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 Gen (Tree m a)
rec Gen (Tree m a)
rec

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

liftShrink :: forall n a. N.SNatI n => (a -> [a]) -> Tree n a -> [Tree n a]
liftShrink :: forall (n :: Nat) a.
SNatI n =>
(a -> [a]) -> Tree n a -> [Tree n a]
liftShrink a -> [a]
shr = Shr n a -> Tree n a -> [Tree n a]
forall (n :: Nat) a. Shr n a -> Tree n a -> [Tree n a]
getShr (Shr n a -> Tree n a -> [Tree n a])
-> Shr n a -> Tree n a -> [Tree n a]
forall a b. (a -> b) -> a -> b
$ Shr 'Z a
-> (forall (m :: Nat). SNatI m => Shr m a -> Shr ('S m) a)
-> Shr 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 Shr 'Z a
start Shr m a -> Shr ('S m) a
forall (m :: Nat). SNatI m => Shr m a -> Shr ('S m) a
forall (m :: Nat). Shr m a -> Shr ('S m) a
step where
    start :: Shr 'Z a
    start :: Shr 'Z a
start = (Tree 'Z a -> [Tree 'Z a]) -> Shr 'Z a
forall (n :: Nat) a. (Tree n a -> [Tree n a]) -> Shr n a
Shr ((Tree 'Z a -> [Tree 'Z a]) -> Shr 'Z a)
-> (Tree 'Z a -> [Tree 'Z a]) -> Shr 'Z a
forall a b. (a -> b) -> a -> b
$ \(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

    step :: Shr m a -> Shr ('S m) a
    step :: forall (m :: Nat). Shr m a -> Shr ('S m) a
step (Shr Tree m a -> [Tree m a]
rec) = (Tree ('S m) a -> [Tree ('S m) a]) -> Shr ('S m) a
forall (n :: Nat) a. (Tree n a -> [Tree n a]) -> Shr n a
Shr ((Tree ('S m) a -> [Tree ('S m) a]) -> Shr ('S m) a)
-> (Tree ('S m) a -> [Tree ('S m) a]) -> Shr ('S m) a
forall a b. (a -> b) -> a -> b
$ \(Node Tree m a
x Tree m a
y) ->
        (Tree m a -> Tree m a -> Tree ('S m) a)
-> (Tree m a, Tree m a) -> Tree ('S m) a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry 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)
-> [(Tree m a, Tree m a)] -> [Tree ('S m) a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Tree m a -> [Tree m a])
-> (Tree m a -> [Tree m a])
-> (Tree m a, Tree m a)
-> [(Tree m a, Tree m a)]
forall a b. (a -> [a]) -> (b -> [b]) -> (a, b) -> [(a, b)]
forall (f :: * -> * -> *) a b.
Arbitrary2 f =>
(a -> [a]) -> (b -> [b]) -> f a b -> [f a b]
QC.liftShrink2 Tree m a -> [Tree m a]
rec Tree m a -> [Tree m a]
rec (Tree m a
x, Tree m a
y)

newtype Shr n a = Shr { forall (n :: Nat) a. Shr n a -> Tree n a -> [Tree n a]
getShr :: Tree n a -> [Tree n a] }

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 (N.SNatI n, QC.CoArbitrary a) => QC.CoArbitrary (Tree n a) where
    coarbitrary :: forall b. Tree n a -> Gen b -> Gen b
coarbitrary Tree n a
v = case SNat n
forall (n :: Nat). SNatI n => SNat n
N.snat :: N.SNat n of
        SNat n
N.SZ -> 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
. (case Tree n a
v of (Leaf a
x) -> a -> Gen b -> Gen b
forall b. a -> Gen b -> Gen b
forall a b. CoArbitrary a => a -> Gen b -> Gen b
QC.coarbitrary a
x)
        SNat n
N.SS -> 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
. (case Tree n a
v of (Node Tree n1 a
x Tree n1 a
y) -> (Tree n1 a, Tree n1 a) -> Gen b -> Gen b
forall b. (Tree n1 a, Tree n1 a) -> Gen b -> Gen b
forall a b. CoArbitrary a => a -> Gen b -> Gen b
QC.coarbitrary (Tree n1 a
x, Tree n1 a
y))

instance (N.SNatI n, QC.Function a) => QC.Function (Tree n a) where
    function :: forall b. (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 n a -> a)
-> (a -> Tree n a) -> (Tree n a -> b) -> Tree n 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 n a
a -> Tree 'Z a
forall a. a -> Tree 'Z a
Leaf
        SNat n
N.SS -> (Tree n a -> (Tree n1 a, Tree n1 a))
-> ((Tree n1 a, Tree n1 a) -> Tree n a)
-> (Tree n a -> b)
-> Tree n a :-> b
forall b a c.
Function b =>
(a -> b) -> (b -> a) -> (a -> c) -> a :-> c
QC.functionMap (\(Node Tree n1 a
x Tree n1 a
y) -> (Tree n1 a
x, Tree n1 a
y)) (\(Tree n1 a
x,Tree n1 a
y) -> 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 Tree n1 a
x Tree n1 a
y)