{-# LANGUAGE CPP                   #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE DeriveDataTypeable    #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE Safe                  #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE StandaloneDeriving    #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}
-- | Non-empty length-indexed random access list.
module Data.RAVec.NonEmpty (
    -- * Random access list
    NERAVec (..),
    NERAVec' (..),

    -- * Construction
    singleton, singleton',
    cons, consTree,
    withCons, withConsTree,

    -- * Conversion
    toList, toList',
    toNonEmpty, toNonEmpty',
    reifyNonEmpty, reifyNonEmpty',

    -- * Indexing
    (!), index',
    tabulate, tabulate',

    unsingleton,
    head, head',
    last, last',

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

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

    -- * Zipping
    zipWith, zipWith',
    izipWith, izipWith',
    repeat, repeat',

    -- * Universe
    universe, universe',

    -- * QuickCheck
    liftArbitrary, liftArbitrary',
    liftShrink, liftShrink',
    ) where

import Prelude
       (Bool (..), Eq (..), Functor (..), Int, Ord (..), Show, seq, uncurry,
       ($), (.))

import Control.Applicative (Applicative (..), (<$>))
import Control.DeepSeq     (NFData (..))
import Data.Bin            (BinP (..))
import Data.BinP.PosP      (PosP (..), PosP' (..))
import Data.Hashable       (Hashable (..))
import Data.List.NonEmpty  (NonEmpty (..))
import Data.Monoid         (Monoid (..))
import Data.Nat            (Nat (..))
import Data.Semigroup      (Semigroup (..))
import Data.Type.BinP      (SBinP (..), SBinPI (..))
import Data.Typeable       (Typeable)

import qualified Data.List.NonEmpty as NEList
import qualified Data.RAVec.Tree    as Tree
import qualified Data.Type.BinP     as BP
import qualified Data.Type.Nat      as N

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

import Data.RAVec.Tree   (Tree (..))
import TrustworthyCompat

-- $setup
-- >>> :set -XScopedTypeVariables -XDataKinds
-- >>> import Prelude (print, Char, Bounded (..))
-- >>> import Data.List (sort)
-- >>> import Data.Wrd (Wrd (..))
-- >>> import Data.Bin.Pos (top, pop)
-- >>> import qualified Data.Bin.Pos as P

-------------------------------------------------------------------------------
-- Random access vec
-------------------------------------------------------------------------------

-- | Non-empty random access list.
newtype NERAVec (b :: BinP) a = NE (NERAVec' 'Z b a)
  deriving (NERAVec b a -> NERAVec b a -> Bool
(NERAVec b a -> NERAVec b a -> Bool)
-> (NERAVec b a -> NERAVec b a -> Bool) -> Eq (NERAVec b a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (b :: BinP) a. Eq a => NERAVec b a -> NERAVec b a -> Bool
$c== :: forall (b :: BinP) a. Eq a => NERAVec b a -> NERAVec b a -> Bool
== :: NERAVec b a -> NERAVec b a -> Bool
$c/= :: forall (b :: BinP) a. Eq a => NERAVec b a -> NERAVec b a -> Bool
/= :: NERAVec b a -> NERAVec b a -> Bool
Eq, Eq (NERAVec b a)
Eq (NERAVec b a) =>
(NERAVec b a -> NERAVec b a -> Ordering)
-> (NERAVec b a -> NERAVec b a -> Bool)
-> (NERAVec b a -> NERAVec b a -> Bool)
-> (NERAVec b a -> NERAVec b a -> Bool)
-> (NERAVec b a -> NERAVec b a -> Bool)
-> (NERAVec b a -> NERAVec b a -> NERAVec b a)
-> (NERAVec b a -> NERAVec b a -> NERAVec b a)
-> Ord (NERAVec b a)
NERAVec b a -> NERAVec b a -> Bool
NERAVec b a -> NERAVec b a -> Ordering
NERAVec b a -> NERAVec b a -> NERAVec b a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall (b :: BinP) a. Ord a => Eq (NERAVec b a)
forall (b :: BinP) a. Ord a => NERAVec b a -> NERAVec b a -> Bool
forall (b :: BinP) a.
Ord a =>
NERAVec b a -> NERAVec b a -> Ordering
forall (b :: BinP) a.
Ord a =>
NERAVec b a -> NERAVec b a -> NERAVec b a
$ccompare :: forall (b :: BinP) a.
Ord a =>
NERAVec b a -> NERAVec b a -> Ordering
compare :: NERAVec b a -> NERAVec b a -> Ordering
$c< :: forall (b :: BinP) a. Ord a => NERAVec b a -> NERAVec b a -> Bool
< :: NERAVec b a -> NERAVec b a -> Bool
$c<= :: forall (b :: BinP) a. Ord a => NERAVec b a -> NERAVec b a -> Bool
<= :: NERAVec b a -> NERAVec b a -> Bool
$c> :: forall (b :: BinP) a. Ord a => NERAVec b a -> NERAVec b a -> Bool
> :: NERAVec b a -> NERAVec b a -> Bool
$c>= :: forall (b :: BinP) a. Ord a => NERAVec b a -> NERAVec b a -> Bool
>= :: NERAVec b a -> NERAVec b a -> Bool
$cmax :: forall (b :: BinP) a.
Ord a =>
NERAVec b a -> NERAVec b a -> NERAVec b a
max :: NERAVec b a -> NERAVec b a -> NERAVec b a
$cmin :: forall (b :: BinP) a.
Ord a =>
NERAVec b a -> NERAVec b a -> NERAVec b a
min :: NERAVec b a -> NERAVec b a -> NERAVec b a
Ord, Int -> NERAVec b a -> ShowS
[NERAVec b a] -> ShowS
NERAVec b a -> String
(Int -> NERAVec b a -> ShowS)
-> (NERAVec b a -> String)
-> ([NERAVec b a] -> ShowS)
-> Show (NERAVec b a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (b :: BinP) a. Show a => Int -> NERAVec b a -> ShowS
forall (b :: BinP) a. Show a => [NERAVec b a] -> ShowS
forall (b :: BinP) a. Show a => NERAVec b a -> String
$cshowsPrec :: forall (b :: BinP) a. Show a => Int -> NERAVec b a -> ShowS
showsPrec :: Int -> NERAVec b a -> ShowS
$cshow :: forall (b :: BinP) a. Show a => NERAVec b a -> String
show :: NERAVec b a -> String
$cshowList :: forall (b :: BinP) a. Show a => [NERAVec b a] -> ShowS
showList :: [NERAVec b a] -> ShowS
Show, Typeable)

-- | Non-empty random access list, undelying representation.
data NERAVec' (n :: Nat) (b :: BinP) a where
    Last  :: Tree n a -> NERAVec' n 'BE a
    Cons0 ::             NERAVec' ('S n) b a -> NERAVec' n ('B0 b) a
    Cons1 :: Tree n a -> NERAVec' ('S n) b a -> NERAVec' n ('B1 b) a
  deriving (Typeable)

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

deriving instance Eq a   => Eq   (NERAVec' n b a)
deriving instance Show a => Show (NERAVec' n b a)

instance Ord a => Ord (NERAVec' n b a) where
    compare :: NERAVec' n b a -> NERAVec' n b a -> Ordering
compare NERAVec' n b a
xs NERAVec' n b a
ys = [a] -> [a] -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (NERAVec' n b a -> [a]
forall (n :: Nat) (b :: BinP) a. NERAVec' n b a -> [a]
toList' NERAVec' n b a
xs) (NERAVec' n b a -> [a]
forall (n :: Nat) (b :: BinP) a. NERAVec' n b a -> [a]
toList' NERAVec' n b a
ys)

instance Functor (NERAVec b) where
    fmap :: forall a b. (a -> b) -> NERAVec b a -> NERAVec b b
fmap = (a -> b) -> NERAVec b a -> NERAVec b b
forall a b (m :: BinP). (a -> b) -> NERAVec m a -> NERAVec m b
map

instance Functor (NERAVec' n b) where
    fmap :: forall a b. (a -> b) -> NERAVec' n b a -> NERAVec' n b b
fmap = (a -> b) -> NERAVec' n b a -> NERAVec' n b b
forall a b (n :: Nat) (m :: BinP).
(a -> b) -> NERAVec' n m a -> NERAVec' n m b
map'

instance I.Foldable (NERAVec b) where
    foldMap :: forall m a. Monoid m => (a -> m) -> NERAVec b a -> m
foldMap = (a -> m) -> NERAVec b a -> m
forall m a (b :: BinP). Monoid m => (a -> m) -> NERAVec b a -> m
foldMap
    foldr :: forall a b. (a -> b -> b) -> b -> NERAVec b a -> b
foldr   = (a -> b -> b) -> b -> NERAVec b a -> b
forall a b (m :: BinP). (a -> b -> b) -> b -> NERAVec m a -> b
foldr

    null :: forall a. NERAVec b a -> Bool
null NERAVec b a
_ = Bool
False

instance I.Foldable (NERAVec' n b) where
    foldMap :: forall m a. Monoid m => (a -> m) -> NERAVec' n b a -> m
foldMap = (a -> m) -> NERAVec' n b a -> m
forall m a (n :: Nat) (b :: BinP).
Monoid m =>
(a -> m) -> NERAVec' n b a -> m
foldMap'
    foldr :: forall a b. (a -> b -> b) -> b -> NERAVec' n b a -> b
foldr   = (a -> b -> b) -> b -> NERAVec' n b a -> b
forall a b (n :: Nat) (m :: BinP).
(a -> b -> b) -> b -> NERAVec' n m a -> b
foldr'

    null :: forall a. NERAVec' n b a -> Bool
null NERAVec' n b a
_ = Bool
False

instance I.Traversable (NERAVec b) where
    traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> NERAVec b a -> f (NERAVec b b)
traverse = (a -> f b) -> NERAVec b a -> f (NERAVec b b)
forall (f :: * -> *) a b (m :: BinP).
Applicative f =>
(a -> f b) -> NERAVec m a -> f (NERAVec m b)
traverse

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

-- | @since 0.2
instance WI.FunctorWithIndex (PosP n) (NERAVec n) where
    imap :: forall a b. (PosP n -> a -> b) -> NERAVec n a -> NERAVec n b
imap = (PosP n -> a -> b) -> NERAVec n a -> NERAVec n b
forall (n :: BinP) a b.
(PosP n -> a -> b) -> NERAVec n a -> NERAVec n b
imap

-- | @since 0.2
instance WI.FoldableWithIndex (PosP n) (NERAVec n) where
    ifoldMap :: forall m a. Monoid m => (PosP n -> a -> m) -> NERAVec n a -> m
ifoldMap = (PosP n -> a -> m) -> NERAVec n a -> m
forall m (b :: BinP) a.
Monoid m =>
(PosP b -> a -> m) -> NERAVec b a -> m
ifoldMap
    ifoldr :: forall a b. (PosP n -> a -> b -> b) -> b -> NERAVec n a -> b
ifoldr   = (PosP n -> a -> b -> b) -> b -> NERAVec n a -> b
forall (n :: BinP) a b.
(PosP n -> a -> b -> b) -> b -> NERAVec n a -> b
ifoldr

-- | @since 0.2
instance WI.TraversableWithIndex (PosP n) (NERAVec n) where
    itraverse :: forall (f :: * -> *) a b.
Applicative f =>
(PosP n -> a -> f b) -> NERAVec n a -> f (NERAVec n b)
itraverse = (PosP n -> a -> f b) -> NERAVec n a -> f (NERAVec n b)
forall (f :: * -> *) (m :: BinP) a b.
Applicative f =>
(PosP m -> a -> f b) -> NERAVec m a -> f (NERAVec m b)
itraverse

-- | @since 0.2
instance WI.FunctorWithIndex (PosP' n m) (NERAVec' n m) where
    imap :: forall a b.
(PosP' n m -> a -> b) -> NERAVec' n m a -> NERAVec' n m b
imap = (PosP' n m -> a -> b) -> NERAVec' n m a -> NERAVec' n m b
forall (n :: Nat) (m :: BinP) a b.
(PosP' n m -> a -> b) -> NERAVec' n m a -> NERAVec' n m b
imap'

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

-- | @since 0.2
instance WI.TraversableWithIndex (PosP' n m) (NERAVec' n m) where
    itraverse :: forall (f :: * -> *) a b.
Applicative f =>
(PosP' n m -> a -> f b) -> NERAVec' n m a -> f (NERAVec' n m b)
itraverse = (PosP' n m -> a -> f b) -> NERAVec' n m a -> f (NERAVec' n m b)
forall (f :: * -> *) (n :: Nat) (m :: BinP) a b.
Applicative f =>
(PosP' n m -> a -> f b) -> NERAVec' n m a -> f (NERAVec' n m b)
itraverse'

#ifdef MIN_VERSION_semigroupoids
instance I.Foldable1 (NERAVec b) where
    foldMap1 :: forall m a. Semigroup m => (a -> m) -> NERAVec b a -> m
foldMap1   = (a -> m) -> NERAVec b a -> m
forall m a (b :: BinP). Semigroup m => (a -> m) -> NERAVec b a -> m
foldMap1
    toNonEmpty :: forall a. NERAVec b a -> NonEmpty a
toNonEmpty = NERAVec b a -> NonEmpty a
forall (b :: BinP) a. NERAVec b a -> NonEmpty a
toNonEmpty

instance I.Foldable1 (NERAVec' n b) where
    foldMap1 :: forall m a. Semigroup m => (a -> m) -> NERAVec' n b a -> m
foldMap1   = (a -> m) -> NERAVec' n b a -> m
forall m a (n :: Nat) (b :: BinP).
Semigroup m =>
(a -> m) -> NERAVec' n b a -> m
foldMap1'
    toNonEmpty :: forall a. NERAVec' n b a -> NonEmpty a
toNonEmpty = NERAVec' n b a -> NonEmpty a
forall (n :: Nat) (b :: BinP) a. NERAVec' n b a -> NonEmpty a
toNonEmpty'

instance I.Traversable1 (NERAVec b) where
    traverse1 :: forall (f :: * -> *) a b.
Apply f =>
(a -> f b) -> NERAVec b a -> f (NERAVec b b)
traverse1 = (a -> f b) -> NERAVec b a -> f (NERAVec b b)
forall (f :: * -> *) a b (m :: BinP).
Apply f =>
(a -> f b) -> NERAVec m a -> f (NERAVec m b)
traverse1

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

instance NFData a => NFData (NERAVec b a) where
    rnf :: NERAVec b a -> ()
rnf (NE NERAVec' 'Z b a
xs) = NERAVec' 'Z b a -> ()
forall a. NFData a => a -> ()
rnf NERAVec' 'Z b a
xs

instance NFData a => NFData (NERAVec' n b a) where
    rnf :: NERAVec' n b a -> ()
rnf (Last  Tree n a
t)   = Tree n a -> ()
forall a. NFData a => a -> ()
rnf Tree n a
t
    rnf (Cons0   NERAVec' ('S n) b a
r) = NERAVec' ('S n) b a -> ()
forall a. NFData a => a -> ()
rnf NERAVec' ('S n) b a
r
    rnf (Cons1 Tree n a
t NERAVec' ('S n) b a
r) = Tree n a -> ()
forall a. NFData a => a -> ()
rnf Tree n a
t () -> () -> ()
forall a b. a -> b -> b
`seq` NERAVec' ('S n) b a -> ()
forall a. NFData a => a -> ()
rnf NERAVec' ('S n) b a
r

instance Hashable a => Hashable (NERAVec b a) where
    hashWithSalt :: Int -> NERAVec b a -> Int
hashWithSalt Int
salt (NE NERAVec' 'Z b a
xs) = Int -> NERAVec' 'Z b a -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
salt NERAVec' 'Z b a
xs

instance Hashable a => Hashable (NERAVec' n b a) where
    hashWithSalt :: Int -> NERAVec' n b a -> Int
hashWithSalt Int
salt = Int -> [a] -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
salt ([a] -> Int) -> (NERAVec' n b a -> [a]) -> NERAVec' n b a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NERAVec' n b a -> [a]
forall (n :: Nat) (b :: BinP) a. NERAVec' n b a -> [a]
toList'

instance SBinPI b => Applicative (NERAVec b) where
    pure :: forall a. a -> NERAVec b a
pure   = a -> NERAVec b a
forall (b :: BinP) a. SBinPI b => a -> NERAVec b a
repeat
    <*> :: forall a b. NERAVec b (a -> b) -> NERAVec b a -> NERAVec b b
(<*>)  = ((a -> b) -> a -> b)
-> NERAVec b (a -> b) -> NERAVec b a -> NERAVec b b
forall a b c (m :: BinP).
(a -> b -> c) -> NERAVec m a -> NERAVec m b -> NERAVec m c
zipWith (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
($)
    NERAVec b a
x <* :: forall a b. NERAVec b a -> NERAVec b b -> NERAVec b a
<* NERAVec b b
_ = NERAVec b a
x
    NERAVec b a
_ *> :: forall a b. NERAVec b a -> NERAVec b b -> NERAVec b b
*> NERAVec b b
x = NERAVec b b
x
    liftA2 :: forall a b c.
(a -> b -> c) -> NERAVec b a -> NERAVec b b -> NERAVec b c
liftA2 = (a -> b -> c) -> NERAVec b a -> NERAVec b b -> NERAVec b c
forall a b c (m :: BinP).
(a -> b -> c) -> NERAVec m a -> NERAVec m b -> NERAVec m c
zipWith

instance (SBinPI b, N.SNatI n) => Applicative (NERAVec' n b) where
    pure :: forall a. a -> NERAVec' n b a
pure   = a -> NERAVec' n b a
forall (b :: BinP) (n :: Nat) a.
(SNatI n, SBinPI b) =>
a -> NERAVec' n b a
repeat'
    <*> :: forall a b.
NERAVec' n b (a -> b) -> NERAVec' n b a -> NERAVec' n b b
(<*>)  = ((a -> b) -> a -> b)
-> NERAVec' n b (a -> b) -> NERAVec' n b a -> NERAVec' n b b
forall a b c (n :: Nat) (m :: BinP).
(a -> b -> c) -> NERAVec' n m a -> NERAVec' n m b -> NERAVec' n m c
zipWith' (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
($)
    NERAVec' n b a
x <* :: forall a b. NERAVec' n b a -> NERAVec' n b b -> NERAVec' n b a
<* NERAVec' n b b
_ = NERAVec' n b a
x
    NERAVec' n b a
_ *> :: forall a b. NERAVec' n b a -> NERAVec' n b b -> NERAVec' n b b
*> NERAVec' n b b
x = NERAVec' n b b
x
    liftA2 :: forall a b c.
(a -> b -> c) -> NERAVec' n b a -> NERAVec' n b b -> NERAVec' n b c
liftA2 = (a -> b -> c) -> NERAVec' n b a -> NERAVec' n b b -> NERAVec' n b c
forall a b c (n :: Nat) (m :: BinP).
(a -> b -> c) -> NERAVec' n m a -> NERAVec' n m b -> NERAVec' n m c
zipWith'

#ifdef MIN_VERSION_distributive
instance SBinPI b => I.Distributive (NERAVec b) where
    distribute :: forall (f :: * -> *) a.
Functor f =>
f (NERAVec b a) -> NERAVec b (f a)
distribute f (NERAVec b a)
f = (PosP b -> f a) -> NERAVec b (f a)
forall (b :: BinP) a. SBinPI b => (PosP b -> a) -> NERAVec b a
tabulate (\PosP b
k -> (NERAVec b a -> a) -> f (NERAVec b 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 (NERAVec b a -> PosP b -> a
forall (b :: BinP) a. NERAVec b a -> PosP b -> a
! PosP b
k) f (NERAVec b a)
f)

instance (SBinPI b, N.SNatI n) => I.Distributive (NERAVec' n b) where
    distribute :: forall (f :: * -> *) a.
Functor f =>
f (NERAVec' n b a) -> NERAVec' n b (f a)
distribute f (NERAVec' n b a)
f = (PosP' n b -> f a) -> NERAVec' n b (f a)
forall (b :: BinP) (n :: Nat) a.
(SBinPI b, SNatI n) =>
(PosP' n b -> a) -> NERAVec' n b a
tabulate' (\PosP' n b
k -> (NERAVec' n b a -> a) -> f (NERAVec' n b 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 (NERAVec' n b a -> PosP' n b -> a
forall (n :: Nat) (b :: BinP) a. NERAVec' n b a -> PosP' n b -> a
`index'` PosP' n b
k) f (NERAVec' n b a)
f)

#ifdef MIN_VERSION_adjunctions
instance SBinPI b => I.Representable (NERAVec b) where
    type Rep (NERAVec b) = PosP b
    index :: forall a. NERAVec b a -> Rep (NERAVec b) -> a
index    = NERAVec b a -> Rep (NERAVec b) -> a
NERAVec b a -> PosP b -> a
forall (b :: BinP) a. NERAVec b a -> PosP b -> a
(!)
    tabulate :: forall a. (Rep (NERAVec b) -> a) -> NERAVec b a
tabulate = (Rep (NERAVec b) -> a) -> NERAVec b a
(PosP b -> a) -> NERAVec b a
forall (b :: BinP) a. SBinPI b => (PosP b -> a) -> NERAVec b a
tabulate

instance (SBinPI b, N.SNatI n) => I.Representable (NERAVec' n b) where
    type Rep (NERAVec' n b) = PosP' n b
    index :: forall a. NERAVec' n b a -> Rep (NERAVec' n b) -> a
index    = NERAVec' n b a -> Rep (NERAVec' n b) -> a
NERAVec' n b a -> PosP' n b -> a
forall (n :: Nat) (b :: BinP) a. NERAVec' n b a -> PosP' n b -> a
index'
    tabulate :: forall a. (Rep (NERAVec' n b) -> a) -> NERAVec' n b a
tabulate = (Rep (NERAVec' n b) -> a) -> NERAVec' n b a
(PosP' n b -> a) -> NERAVec' n b a
forall (b :: BinP) (n :: Nat) a.
(SBinPI b, SNatI n) =>
(PosP' n b -> a) -> NERAVec' n b a
tabulate'
#endif
#endif

instance Semigroup a => Semigroup (NERAVec b a) where
    <> :: NERAVec b a -> NERAVec b a -> NERAVec b a
(<>) = (a -> a -> a) -> NERAVec b a -> NERAVec b a -> NERAVec b a
forall a b c (m :: BinP).
(a -> b -> c) -> NERAVec m a -> NERAVec m b -> NERAVec m c
zipWith a -> a -> a
forall a. Semigroup a => a -> a -> a
(<>)

instance Semigroup a => Semigroup (NERAVec' n b a) where
    <> :: NERAVec' n b a -> NERAVec' n b a -> NERAVec' n b a
(<>) = (a -> a -> a) -> NERAVec' n b a -> NERAVec' n b a -> NERAVec' n b a
forall a b c (n :: Nat) (m :: BinP).
(a -> b -> c) -> NERAVec' n m a -> NERAVec' n m b -> NERAVec' n m c
zipWith' a -> a -> a
forall a. Semigroup a => a -> a -> a
(<>)

instance (Monoid a, SBinPI b) => Monoid (NERAVec b a) where
    mempty :: NERAVec b a
mempty  = a -> NERAVec b a
forall (b :: BinP) a. SBinPI b => a -> NERAVec b a
repeat a
forall a. Monoid a => a
mempty
    mappend :: NERAVec b a -> NERAVec b a -> NERAVec b a
mappend = (a -> a -> a) -> NERAVec b a -> NERAVec b a -> NERAVec b a
forall a b c (m :: BinP).
(a -> b -> c) -> NERAVec m a -> NERAVec m b -> NERAVec m c
zipWith a -> a -> a
forall a. Monoid a => a -> a -> a
mappend

instance (Monoid a, SBinPI b, N.SNatI n) => Monoid (NERAVec' n b a) where
    mempty :: NERAVec' n b a
mempty  = a -> NERAVec' n b a
forall (b :: BinP) (n :: Nat) a.
(SNatI n, SBinPI b) =>
a -> NERAVec' n b a
repeat' a
forall a. Monoid a => a
mempty
    mappend :: NERAVec' n b a -> NERAVec' n b a -> NERAVec' n b a
mappend = (a -> a -> a) -> NERAVec' n b a -> NERAVec' n b a -> NERAVec' n b a
forall a b c (n :: Nat) (m :: BinP).
(a -> b -> c) -> NERAVec' n m a -> NERAVec' n m b -> NERAVec' n m c
zipWith' a -> a -> a
forall a. Monoid a => a -> a -> a
mappend

#ifdef MIN_VERSION_semigroupoids
instance Apply (NERAVec b) where
    <.> :: forall a b. NERAVec b (a -> b) -> NERAVec b a -> NERAVec b b
(<.>)  = ((a -> b) -> a -> b)
-> NERAVec b (a -> b) -> NERAVec b a -> NERAVec b b
forall a b c (m :: BinP).
(a -> b -> c) -> NERAVec m a -> NERAVec m b -> NERAVec m c
zipWith (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
($)
    liftF2 :: forall a b c.
(a -> b -> c) -> NERAVec b a -> NERAVec b b -> NERAVec b c
liftF2 = (a -> b -> c) -> NERAVec b a -> NERAVec b b -> NERAVec b c
forall a b c (m :: BinP).
(a -> b -> c) -> NERAVec m a -> NERAVec m b -> NERAVec m c
zipWith
    NERAVec b a
_ .> :: forall a b. NERAVec b a -> NERAVec b b -> NERAVec b b
.> NERAVec b b
x = NERAVec b b
x
    NERAVec b a
x <. :: forall a b. NERAVec b a -> NERAVec b b -> NERAVec b a
<. NERAVec b b
_ = NERAVec b a
x

instance Apply (NERAVec' n b) where
    <.> :: forall a b.
NERAVec' n b (a -> b) -> NERAVec' n b a -> NERAVec' n b b
(<.>) = ((a -> b) -> a -> b)
-> NERAVec' n b (a -> b) -> NERAVec' n b a -> NERAVec' n b b
forall a b c (n :: Nat) (m :: BinP).
(a -> b -> c) -> NERAVec' n m a -> NERAVec' n m b -> NERAVec' n m c
zipWith' (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
($)
    liftF2 :: forall a b c.
(a -> b -> c) -> NERAVec' n b a -> NERAVec' n b b -> NERAVec' n b c
liftF2 = (a -> b -> c) -> NERAVec' n b a -> NERAVec' n b b -> NERAVec' n b c
forall a b c (n :: Nat) (m :: BinP).
(a -> b -> c) -> NERAVec' n m a -> NERAVec' n m b -> NERAVec' n m c
zipWith'
    NERAVec' n b a
_ .> :: forall a b. NERAVec' n b a -> NERAVec' n b b -> NERAVec' n b b
.> NERAVec' n b b
x = NERAVec' n b b
x
    NERAVec' n b a
x <. :: forall a b. NERAVec' n b a -> NERAVec' n b b -> NERAVec' n b a
<. NERAVec' n b b
_ = NERAVec' n b a
x
#endif

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

singleton :: forall a. a -> NERAVec BP.BinP1 a
singleton :: forall a. a -> NERAVec 'BE a
singleton = (a -> NERAVec' 'Z 'BE a) -> a -> NERAVec 'BE a
forall a b. Coercible @(*) a b => a -> b
coerce (a -> NERAVec' 'Z 'BE a
forall a. a -> NERAVec' 'Z 'BE a
singleton' :: a -> NERAVec' 'Z BP.BinP1 a)

singleton' :: a -> NERAVec' 'Z BP.BinP1 a
singleton' :: forall a. a -> NERAVec' 'Z 'BE a
singleton' = Tree 'Z a -> NERAVec' 'Z 'BE a
forall (n :: Nat) a. Tree n a -> NERAVec' n 'BE a
Last (Tree 'Z a -> NERAVec' 'Z 'BE a)
-> (a -> Tree 'Z a) -> a -> NERAVec' 'Z 'BE a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Tree 'Z a
forall a. a -> Tree 'Z a
Tree.singleton

-- | 'cons' for non-empty rals.
cons :: forall a b. a -> NERAVec b a -> NERAVec (BP.Succ b) a
cons :: forall a (b :: BinP). a -> NERAVec b a -> NERAVec (Succ b) a
cons a
x (NE NERAVec' 'Z b a
xs) = NERAVec' 'Z (Succ b) a -> NERAVec (Succ b) a
forall (b :: BinP) a. NERAVec' 'Z b a -> NERAVec b a
NE (Tree 'Z a -> NERAVec' 'Z b a -> NERAVec' 'Z (Succ b) a
forall (n :: Nat) a (b :: BinP).
Tree n a -> NERAVec' n b a -> NERAVec' n (Succ b) a
consTree (a -> Tree 'Z a
forall a. a -> Tree 'Z a
Leaf a
x) NERAVec' 'Z b a
xs)

consTree :: Tree n a -> NERAVec' n b a -> NERAVec' n (BP.Succ b) a
consTree :: forall (n :: Nat) a (b :: BinP).
Tree n a -> NERAVec' n b a -> NERAVec' n (Succ b) a
consTree Tree n a
x (Last Tree n a
t)    = NERAVec' ('S n) 'BE a -> NERAVec' n ('B0 'BE) a
forall (n :: Nat) (b :: BinP) a.
NERAVec' ('S n) b a -> NERAVec' n ('B0 b) a
Cons0 (Tree ('S n) a -> NERAVec' ('S n) 'BE a
forall (n :: Nat) a. Tree n a -> NERAVec' n 'BE a
Last (Tree n a -> Tree n a -> Tree ('S n) a
forall (n1 :: Nat) a. Tree n1 a -> Tree n1 a -> Tree ('S n1) a
Node Tree n a
x Tree n a
t))
consTree Tree n a
x (Cons0 NERAVec' ('S n) b a
r)   = Tree n a -> NERAVec' ('S n) b a -> NERAVec' n ('B1 b) a
forall (n :: Nat) a (b :: BinP).
Tree n a -> NERAVec' ('S n) b a -> NERAVec' n ('B1 b) a
Cons1 Tree n a
x NERAVec' ('S n) b a
r
consTree Tree n a
x (Cons1 Tree n a
t NERAVec' ('S n) b a
r) = NERAVec' ('S n) (Succ b) a -> NERAVec' n ('B0 (Succ b)) a
forall (n :: Nat) (b :: BinP) a.
NERAVec' ('S n) b a -> NERAVec' n ('B0 b) a
Cons0 (Tree ('S n) a -> NERAVec' ('S n) b a -> NERAVec' ('S n) (Succ b) a
forall (n :: Nat) a (b :: BinP).
Tree n a -> NERAVec' n b a -> NERAVec' n (Succ b) a
consTree (Tree n a -> Tree n a -> Tree ('S n) a
forall (n1 :: Nat) a. Tree n1 a -> Tree n1 a -> Tree ('S n1) a
Node Tree n a
x Tree n a
t) NERAVec' ('S n) b a
r)

-- | 'withCons' for non-empty rals.
withCons :: SBinPI b => a -> NERAVec b a -> (SBinPI (BP.Succ b) => NERAVec (BP.Succ b) a -> r) -> r
withCons :: forall (b :: BinP) a r.
SBinPI b =>
a
-> NERAVec b a -> (SBinPI (Succ b) => NERAVec (Succ b) a -> r) -> r
withCons a
x (NE NERAVec' 'Z b a
xs) SBinPI (Succ b) => NERAVec (Succ b) a -> r
k = SBinP b
-> Tree 'Z a
-> NERAVec' 'Z b a
-> (SBinPI (Succ b) => NERAVec' 'Z (Succ b) a -> r)
-> r
forall (b :: BinP) (n :: Nat) a r.
SBinP b
-> Tree n a
-> NERAVec' n b a
-> (SBinPI (Succ b) => NERAVec' n (Succ b) a -> r)
-> r
withConsTree SBinP b
forall (b :: BinP). SBinPI b => SBinP b
sbinp (a -> Tree 'Z a
forall a. a -> Tree 'Z a
Leaf a
x) NERAVec' 'Z b a
xs ((SBinPI (Succ b) => NERAVec' 'Z (Succ b) a -> r) -> r)
-> (SBinPI (Succ b) => NERAVec' 'Z (Succ b) a -> r) -> r
forall a b. (a -> b) -> a -> b
$ SBinPI (Succ b) => NERAVec (Succ b) a -> r
NERAVec (Succ b) a -> r
k (NERAVec (Succ b) a -> r)
-> (NERAVec' 'Z (Succ b) a -> NERAVec (Succ b) a)
-> NERAVec' 'Z (Succ b) a
-> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NERAVec' 'Z (Succ b) a -> NERAVec (Succ b) a
forall (b :: BinP) a. NERAVec' 'Z b a -> NERAVec b a
NE

withConsTree :: SBinP b -> Tree n a -> NERAVec' n b a -> (SBinPI (BP.Succ b) => NERAVec' n (BP.Succ b) a -> r) -> r
withConsTree :: forall (b :: BinP) (n :: Nat) a r.
SBinP b
-> Tree n a
-> NERAVec' n b a
-> (SBinPI (Succ b) => NERAVec' n (Succ b) a -> r)
-> r
withConsTree SBinP b
SBE Tree n a
x (Last Tree n a
t)    SBinPI (Succ b) => NERAVec' n (Succ b) a -> r
k = SBinPI (Succ b) => NERAVec' n (Succ b) a -> r
NERAVec' n (Succ b) a -> r
k (NERAVec' ('S n) 'BE a -> NERAVec' n ('B0 'BE) a
forall (n :: Nat) (b :: BinP) a.
NERAVec' ('S n) b a -> NERAVec' n ('B0 b) a
Cons0 (Tree ('S n) a -> NERAVec' ('S n) 'BE a
forall (n :: Nat) a. Tree n a -> NERAVec' n 'BE a
Last (Tree n a -> Tree n a -> Tree ('S n) a
forall (n1 :: Nat) a. Tree n1 a -> Tree n1 a -> Tree ('S n1) a
Node Tree n a
x Tree n a
t)))
withConsTree SBinP b
SB0 Tree n a
x (Cons0 NERAVec' ('S n) b a
r)   SBinPI (Succ b) => NERAVec' n (Succ b) a -> r
k = SBinPI (Succ b) => NERAVec' n (Succ b) a -> r
NERAVec' n (Succ b) a -> r
k (Tree n a -> NERAVec' ('S n) b a -> NERAVec' n ('B1 b) a
forall (n :: Nat) a (b :: BinP).
Tree n a -> NERAVec' ('S n) b a -> NERAVec' n ('B1 b) a
Cons1 Tree n a
x NERAVec' ('S n) b a
r)
withConsTree SBinP b
SB1 Tree n a
x (Cons1 Tree n a
t NERAVec' ('S n) b a
r) SBinPI (Succ b) => NERAVec' n (Succ b) a -> r
k = SBinP b
-> Tree ('S n) a
-> NERAVec' ('S n) b a
-> (SBinPI (Succ b) => NERAVec' ('S n) (Succ b) a -> r)
-> r
forall (b :: BinP) (n :: Nat) a r.
SBinP b
-> Tree n a
-> NERAVec' n b a
-> (SBinPI (Succ b) => NERAVec' n (Succ b) a -> r)
-> r
withConsTree SBinP b
forall (b :: BinP). SBinPI b => SBinP b
sbinp (Tree n a -> Tree n a -> Tree ('S n) a
forall (n1 :: Nat) a. Tree n1 a -> Tree n1 a -> Tree ('S n1) a
Node Tree n a
x Tree n a
t) NERAVec' ('S n) b a
r ((SBinPI (Succ b) => NERAVec' ('S n) (Succ b) a -> r) -> r)
-> (SBinPI (Succ b) => NERAVec' ('S n) (Succ b) a -> r) -> r
forall a b. (a -> b) -> a -> b
$ SBinPI (Succ b) => NERAVec' n (Succ b) a -> r
NERAVec' n ('B0 (Succ b1)) a -> r
NERAVec' n (Succ b) a -> r
k (NERAVec' n ('B0 (Succ b1)) a -> r)
-> (NERAVec' ('S n) (Succ b1) a -> NERAVec' n ('B0 (Succ b1)) a)
-> NERAVec' ('S n) (Succ b1) a
-> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NERAVec' ('S n) (Succ b1) a -> NERAVec' n ('B0 (Succ b1)) a
forall (n :: Nat) (b :: BinP) a.
NERAVec' ('S n) b a -> NERAVec' n ('B0 b) a
Cons0

unsingleton :: NERAVec 'BE a -> a
unsingleton :: forall a. NERAVec 'BE a -> a
unsingleton (NE (Last (Tree.Leaf a
x))) = a
x

head :: NERAVec b a -> a
head :: forall (b :: BinP) a. NERAVec b a -> a
head (NE NERAVec' 'Z b a
x) = NERAVec' 'Z b a -> a
forall (n :: Nat) (b :: BinP) a. NERAVec' n b a -> a
head' NERAVec' 'Z b a
x

head' :: NERAVec' n b a -> a
head' :: forall (n :: Nat) (b :: BinP) a. NERAVec' n b a -> a
head' (Last Tree n a
t)     = Tree n a -> a
forall (n :: Nat) a. Tree n a -> a
Tree.leftmost Tree n a
t
head' (Cons0 NERAVec' ('S n) b a
ral) = NERAVec' ('S n) b a -> a
forall (n :: Nat) (b :: BinP) a. NERAVec' n b a -> a
head' NERAVec' ('S n) b a
ral
head' (Cons1 Tree n a
t NERAVec' ('S n) b a
_) = Tree n a -> a
forall (n :: Nat) a. Tree n a -> a
Tree.leftmost Tree n a
t

last :: NERAVec b a -> a
last :: forall (b :: BinP) a. NERAVec b a -> a
last (NE NERAVec' 'Z b a
x) = NERAVec' 'Z b a -> a
forall (n :: Nat) (b :: BinP) a. NERAVec' n b a -> a
last' NERAVec' 'Z b a
x

last' :: NERAVec' n b a -> a
last' :: forall (n :: Nat) (b :: BinP) a. NERAVec' n b a -> a
last' (Last Tree n a
t)       = Tree n a -> a
forall (n :: Nat) a. Tree n a -> a
Tree.rightmost Tree n a
t
last' (Cons0 NERAVec' ('S n) b a
ral)   = NERAVec' ('S n) b a -> a
forall (n :: Nat) (b :: BinP) a. NERAVec' n b a -> a
head' NERAVec' ('S n) b a
ral
last' (Cons1 Tree n a
_ NERAVec' ('S n) b a
ral) = NERAVec' ('S n) b a -> a
forall (n :: Nat) (b :: BinP) a. NERAVec' n b a -> a
last' NERAVec' ('S n) b a
ral

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

toList :: NERAVec b a -> [a]
toList :: forall (b :: BinP) a. NERAVec b a -> [a]
toList (NE NERAVec' 'Z b a
xs) = NERAVec' 'Z b a -> [a]
forall (n :: Nat) (b :: BinP) a. NERAVec' n b a -> [a]
toList' NERAVec' 'Z b a
xs

toList' :: NERAVec' n b a -> [a]
toList' :: forall (n :: Nat) (b :: BinP) a. NERAVec' n b a -> [a]
toList' = (a -> [a] -> [a]) -> [a] -> NERAVec' n b a -> [a]
forall a b (n :: Nat) (m :: BinP).
(a -> b -> b) -> b -> NERAVec' n m a -> b
foldr' (:) []

toNonEmpty :: NERAVec b a -> NonEmpty a
toNonEmpty :: forall (b :: BinP) a. NERAVec b a -> NonEmpty a
toNonEmpty (NE NERAVec' 'Z b a
xs) = NERAVec' 'Z b a -> NonEmpty a
forall (n :: Nat) (b :: BinP) a. NERAVec' n b a -> NonEmpty a
toNonEmpty' NERAVec' 'Z b a
xs

toNonEmpty' :: NERAVec' n b a -> NonEmpty a
toNonEmpty' :: forall (n :: Nat) (b :: BinP) a. NERAVec' n b a -> NonEmpty a
toNonEmpty' = (a -> NonEmpty a -> NonEmpty a)
-> (a -> NonEmpty a) -> NERAVec' n b a -> NonEmpty a
forall a b (n :: Nat) (m :: BinP).
(a -> b -> b) -> (a -> b) -> NERAVec' n m a -> b
foldr1Map' a -> NonEmpty a -> NonEmpty a
forall a. a -> NonEmpty a -> NonEmpty a
NEList.cons (a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:|[])

reifyNonEmpty :: NonEmpty a -> (forall b. SBinPI b => NERAVec b a -> r) -> r
reifyNonEmpty :: forall a r.
NonEmpty a
-> (forall (b :: BinP). SBinPI b => NERAVec b a -> r) -> r
reifyNonEmpty NonEmpty a
xs forall (b :: BinP). SBinPI b => NERAVec b a -> r
k = NonEmpty a
-> (forall {b :: BinP}. SBinPI b => NERAVec' 'Z b a -> r) -> r
forall a r.
NonEmpty a
-> (forall (b :: BinP). SBinPI b => NERAVec' 'Z b a -> r) -> r
reifyNonEmpty' NonEmpty a
xs ((forall {b :: BinP}. SBinPI b => NERAVec' 'Z b a -> r) -> r)
-> (forall {b :: BinP}. SBinPI b => NERAVec' 'Z b a -> r) -> r
forall a b. (a -> b) -> a -> b
$ NERAVec b a -> r
forall (b :: BinP). SBinPI b => NERAVec b a -> r
k (NERAVec b a -> r)
-> (NERAVec' 'Z b a -> NERAVec b a) -> NERAVec' 'Z b a -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NERAVec' 'Z b a -> NERAVec b a
forall (b :: BinP) a. NERAVec' 'Z b a -> NERAVec b a
NE

reifyNonEmpty' :: forall a r. NonEmpty a -> (forall b. SBinPI b => NERAVec' 'Z b a -> r) -> r
reifyNonEmpty' :: forall a r.
NonEmpty a
-> (forall (b :: BinP). SBinPI b => NERAVec' 'Z b a -> r) -> r
reifyNonEmpty' (a
x0 :| [a]
xs0) = a
-> [a]
-> (forall (b :: BinP). SBinPI b => NERAVec' 'Z b a -> r)
-> r
forall k.
a
-> [a]
-> (forall (b :: BinP). SBinPI b => NERAVec' 'Z b a -> k)
-> k
go a
x0 [a]
xs0 where
    go :: forall k. a -> [a] -> (forall b. SBinPI b => NERAVec' 'Z b a -> k) -> k
    go :: forall k.
a
-> [a]
-> (forall (b :: BinP). SBinPI b => NERAVec' 'Z b a -> k)
-> k
go a
x []     forall (b :: BinP). SBinPI b => NERAVec' 'Z b a -> k
k = NERAVec' 'Z 'BE a -> k
forall (b :: BinP). SBinPI b => NERAVec' 'Z b a -> k
k (Tree 'Z a -> NERAVec' 'Z 'BE a
forall (n :: Nat) a. Tree n a -> NERAVec' n 'BE a
Last (a -> Tree 'Z a
forall a. a -> Tree 'Z a
Leaf a
x))
    go a
x (a
y:[a]
ys) forall (b :: BinP). SBinPI b => NERAVec' 'Z b a -> k
k = a
-> [a]
-> (forall (b :: BinP). SBinPI b => NERAVec' 'Z b a -> k)
-> k
forall k.
a
-> [a]
-> (forall (b :: BinP). SBinPI b => NERAVec' 'Z b a -> k)
-> k
go a
y [a]
ys ((forall (b :: BinP). SBinPI b => NERAVec' 'Z b a -> k) -> k)
-> (forall (b :: BinP). SBinPI b => NERAVec' 'Z b a -> k) -> k
forall a b. (a -> b) -> a -> b
$ \NERAVec' 'Z b a
zs -> SBinP b
-> Tree 'Z a
-> NERAVec' 'Z b a
-> (SBinPI (Succ b) => NERAVec' 'Z (Succ b) a -> k)
-> k
forall (b :: BinP) (n :: Nat) a r.
SBinP b
-> Tree n a
-> NERAVec' n b a
-> (SBinPI (Succ b) => NERAVec' n (Succ b) a -> r)
-> r
withConsTree SBinP b
forall (b :: BinP). SBinPI b => SBinP b
sbinp (a -> Tree 'Z a
forall a. a -> Tree 'Z a
Leaf a
x) NERAVec' 'Z b a
zs SBinPI (Succ b) => NERAVec' 'Z (Succ b) a -> k
NERAVec' 'Z (Succ b) a -> k
forall (b :: BinP). SBinPI b => NERAVec' 'Z b a -> k
k

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

(!) :: NERAVec b a -> PosP b -> a
! :: forall (b :: BinP) a. NERAVec b a -> PosP b -> a
(!) (NE NERAVec' 'Z b a
xs) (PosP PosP' 'Z b
p) = NERAVec' 'Z b a -> PosP' 'Z b -> a
forall (n :: Nat) (b :: BinP) a. NERAVec' n b a -> PosP' n b -> a
index' NERAVec' 'Z b a
xs PosP' 'Z b
p

index' :: NERAVec' n b a -> PosP' n b -> a
index' :: forall (n :: Nat) (b :: BinP) a. NERAVec' n b a -> PosP' n b -> a
index' (Last Tree n a
t)      (AtEnd Wrd n
i)  = Tree n a
t Tree n a -> Wrd n -> a
forall (n :: Nat) a. Tree n a -> Wrd n -> a
Tree.! Wrd n
i
index' (Cons0 NERAVec' ('S n) b a
ral)   (There0 PosP' ('S n) b1
i) = NERAVec' ('S n) b a -> PosP' ('S n) b -> a
forall (n :: Nat) (b :: BinP) a. NERAVec' n b a -> PosP' n b -> a
index' NERAVec' ('S n) b a
ral PosP' ('S n) b
PosP' ('S n) b1
i
index' (Cons1 Tree n a
t NERAVec' ('S n) b a
_)   (Here Wrd n
i)   = Tree n a
t Tree n a -> Wrd n -> a
forall (n :: Nat) a. Tree n a -> Wrd n -> a
Tree.! Wrd n
i
index' (Cons1 Tree n a
_ NERAVec' ('S n) b a
ral) (There1 PosP' ('S n) b1
i) = NERAVec' ('S n) b a -> PosP' ('S n) b -> a
forall (n :: Nat) (b :: BinP) a. NERAVec' n b a -> PosP' n b -> a
index' NERAVec' ('S n) b a
ral PosP' ('S n) b
PosP' ('S n) b1
i

tabulate :: SBinPI b => (PosP b -> a) -> NERAVec b a
tabulate :: forall (b :: BinP) a. SBinPI b => (PosP b -> a) -> NERAVec b a
tabulate PosP b -> a
f = NERAVec' 'Z b a -> NERAVec b a
forall (b :: BinP) a. NERAVec' 'Z b a -> NERAVec b a
NE ((PosP' 'Z b -> a) -> NERAVec' 'Z b a
forall (b :: BinP) (n :: Nat) a.
(SBinPI b, SNatI n) =>
(PosP' n b -> a) -> NERAVec' n b a
tabulate' (PosP b -> a
f (PosP b -> a) -> (PosP' 'Z b -> PosP b) -> PosP' 'Z b -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PosP' 'Z b -> PosP b
forall (b :: BinP). PosP' 'Z b -> PosP b
PosP))

tabulate' :: forall b n a. (SBinPI b, N.SNatI n) => (PosP' n b -> a) -> NERAVec' n b a
tabulate' :: forall (b :: BinP) (n :: Nat) a.
(SBinPI b, SNatI n) =>
(PosP' n b -> a) -> NERAVec' n b a
tabulate' PosP' n b -> a
f = case SBinP b
forall (b :: BinP). SBinPI b => SBinP b
sbinp :: SBinP b of
    SBinP b
SBE -> Tree n a -> NERAVec' n 'BE a
forall (n :: Nat) a. Tree n a -> NERAVec' n 'BE a
Last ((Wrd n -> a) -> Tree n a
forall (n :: Nat) a. SNatI n => (Wrd n -> a) -> Tree n a
Tree.tabulate (PosP' n b -> a
f (PosP' n b -> a) -> (Wrd n -> PosP' n b) -> Wrd n -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrd n -> PosP' n b
Wrd n -> PosP' n 'BE
forall (n :: Nat). Wrd n -> PosP' n 'BE
AtEnd))
    SBinP b
SB0 -> NERAVec' ('S n) b1 a -> NERAVec' n ('B0 b1) a
forall (n :: Nat) (b :: BinP) a.
NERAVec' ('S n) b a -> NERAVec' n ('B0 b) a
Cons0 ((PosP' ('S n) b1 -> a) -> NERAVec' ('S n) b1 a
forall (b :: BinP) (n :: Nat) a.
(SBinPI b, SNatI n) =>
(PosP' n b -> a) -> NERAVec' n b a
tabulate' (PosP' n b -> a
f (PosP' n b -> a)
-> (PosP' ('S n) b1 -> PosP' n b) -> PosP' ('S n) b1 -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PosP' ('S n) b1 -> PosP' n b
PosP' ('S n) b1 -> PosP' n ('B0 b1)
forall (n :: Nat) (b1 :: BinP). PosP' ('S n) b1 -> PosP' n ('B0 b1)
There0))
    SBinP b
SB1 -> Tree n a -> NERAVec' ('S n) b1 a -> NERAVec' n ('B1 b1) a
forall (n :: Nat) a (b :: BinP).
Tree n a -> NERAVec' ('S n) b a -> NERAVec' n ('B1 b) a
Cons1 ((Wrd n -> a) -> Tree n a
forall (n :: Nat) a. SNatI n => (Wrd n -> a) -> Tree n a
Tree.tabulate (PosP' n b -> a
f (PosP' n b -> a) -> (Wrd n -> PosP' n b) -> Wrd n -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrd n -> PosP' n b
Wrd n -> PosP' n ('B1 b1)
forall (n :: Nat) (b1 :: BinP). Wrd n -> PosP' n ('B1 b1)
Here)) ((PosP' ('S n) b1 -> a) -> NERAVec' ('S n) b1 a
forall (b :: BinP) (n :: Nat) a.
(SBinPI b, SNatI n) =>
(PosP' n b -> a) -> NERAVec' n b a
tabulate' (PosP' n b -> a
f (PosP' n b -> a)
-> (PosP' ('S n) b1 -> PosP' n b) -> PosP' ('S n) b1 -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PosP' ('S n) b1 -> PosP' n b
PosP' ('S n) b1 -> PosP' n ('B1 b1)
forall (n :: Nat) (b1 :: BinP). PosP' ('S n) b1 -> PosP' n ('B1 b1)
There1))

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

foldMap :: Monoid m => (a -> m) -> NERAVec b a -> m
foldMap :: forall m a (b :: BinP). Monoid m => (a -> m) -> NERAVec b a -> m
foldMap a -> m
f (NE NERAVec' 'Z b a
xs) = (a -> m) -> NERAVec' 'Z b a -> m
forall m a (n :: Nat) (b :: BinP).
Monoid m =>
(a -> m) -> NERAVec' n b a -> m
foldMap' a -> m
f NERAVec' 'Z b a
xs

foldMap' :: Monoid m => (a -> m) -> NERAVec' n b a -> m
foldMap' :: forall m a (n :: Nat) (b :: BinP).
Monoid m =>
(a -> m) -> NERAVec' n b a -> m
foldMap' a -> m
f (Last  Tree n a
t)   = (a -> m) -> Tree n a -> m
forall m a (n :: Nat). Monoid m => (a -> m) -> Tree n a -> m
Tree.foldMap a -> m
f Tree n a
t
foldMap' a -> m
f (Cons0   NERAVec' ('S n) b a
r) = (a -> m) -> NERAVec' ('S n) b a -> m
forall m a (n :: Nat) (b :: BinP).
Monoid m =>
(a -> m) -> NERAVec' n b a -> m
foldMap' a -> m
f NERAVec' ('S n) b a
r
foldMap' a -> m
f (Cons1 Tree n a
t NERAVec' ('S n) b a
r) = m -> m -> m
forall a. Monoid a => a -> a -> a
mappend ((a -> m) -> Tree n a -> m
forall m a (n :: Nat). Monoid m => (a -> m) -> Tree n a -> m
Tree.foldMap a -> m
f Tree n a
t) ((a -> m) -> NERAVec' ('S n) b a -> m
forall m a (n :: Nat) (b :: BinP).
Monoid m =>
(a -> m) -> NERAVec' n b a -> m
foldMap' a -> m
f NERAVec' ('S n) b a
r)

ifoldMap :: Monoid m => (PosP b -> a -> m) -> NERAVec b a -> m
ifoldMap :: forall m (b :: BinP) a.
Monoid m =>
(PosP b -> a -> m) -> NERAVec b a -> m
ifoldMap PosP b -> a -> m
f (NE NERAVec' 'Z b a
xs) = (PosP' 'Z b -> a -> m) -> NERAVec' 'Z b a -> m
forall m (n :: Nat) (b :: BinP) a.
Monoid m =>
(PosP' n b -> a -> m) -> NERAVec' n b a -> m
ifoldMap' (PosP b -> a -> m
f (PosP b -> a -> m)
-> (PosP' 'Z b -> PosP b) -> PosP' 'Z b -> a -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PosP' 'Z b -> PosP b
forall (b :: BinP). PosP' 'Z b -> PosP b
PosP) NERAVec' 'Z b a
xs

ifoldMap' :: Monoid m => (PosP' n b -> a -> m) -> NERAVec' n b a -> m
ifoldMap' :: forall m (n :: Nat) (b :: BinP) a.
Monoid m =>
(PosP' n b -> a -> m) -> NERAVec' n b a -> m
ifoldMap' PosP' n b -> a -> m
f (Last  Tree n a
t)   = (Wrd n -> a -> m) -> Tree n a -> m
forall m (n :: Nat) a.
Monoid m =>
(Wrd n -> a -> m) -> Tree n a -> m
Tree.ifoldMap (PosP' n b -> a -> m
f (PosP' n b -> a -> m) -> (Wrd n -> PosP' n b) -> Wrd n -> a -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrd n -> PosP' n b
Wrd n -> PosP' n 'BE
forall (n :: Nat). Wrd n -> PosP' n 'BE
AtEnd) Tree n a
t
ifoldMap' PosP' n b -> a -> m
f (Cons0   NERAVec' ('S n) b a
r) = (PosP' ('S n) b -> a -> m) -> NERAVec' ('S n) b a -> m
forall m (n :: Nat) (b :: BinP) a.
Monoid m =>
(PosP' n b -> a -> m) -> NERAVec' n b a -> m
ifoldMap' (PosP' n b -> a -> m
f (PosP' n b -> a -> m)
-> (PosP' ('S n) b -> PosP' n b) -> PosP' ('S n) b -> a -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PosP' ('S n) b -> PosP' n b
PosP' ('S n) b -> PosP' n ('B0 b)
forall (n :: Nat) (b1 :: BinP). PosP' ('S n) b1 -> PosP' n ('B0 b1)
There0) NERAVec' ('S n) b a
r
ifoldMap' PosP' n b -> a -> m
f (Cons1 Tree n a
t NERAVec' ('S n) b a
r) = (Wrd n -> a -> m) -> Tree n a -> m
forall m (n :: Nat) a.
Monoid m =>
(Wrd n -> a -> m) -> Tree n a -> m
Tree.ifoldMap (PosP' n b -> a -> m
f (PosP' n b -> a -> m) -> (Wrd n -> PosP' n b) -> Wrd n -> a -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrd n -> PosP' n b
Wrd n -> PosP' n ('B1 b)
forall (n :: Nat) (b1 :: BinP). Wrd n -> PosP' n ('B1 b1)
Here) Tree n a
t m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` (PosP' ('S n) b -> a -> m) -> NERAVec' ('S n) b a -> m
forall m (n :: Nat) (b :: BinP) a.
Monoid m =>
(PosP' n b -> a -> m) -> NERAVec' n b a -> m
ifoldMap' (PosP' n b -> a -> m
f (PosP' n b -> a -> m)
-> (PosP' ('S n) b -> PosP' n b) -> PosP' ('S n) b -> a -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PosP' ('S n) b -> PosP' n b
PosP' ('S n) b -> PosP' n ('B1 b)
forall (n :: Nat) (b1 :: BinP). PosP' ('S n) b1 -> PosP' n ('B1 b1)
There1) NERAVec' ('S n) b a
r

foldMap1 :: Semigroup m => (a -> m) -> NERAVec b a -> m
foldMap1 :: forall m a (b :: BinP). Semigroup m => (a -> m) -> NERAVec b a -> m
foldMap1 a -> m
f (NE NERAVec' 'Z b a
xs) = (a -> m) -> NERAVec' 'Z b a -> m
forall m a (n :: Nat) (b :: BinP).
Semigroup m =>
(a -> m) -> NERAVec' n b a -> m
foldMap1' a -> m
f NERAVec' 'Z b a
xs

foldMap1' :: Semigroup m => (a -> m) -> NERAVec' n b a -> m
foldMap1' :: forall m a (n :: Nat) (b :: BinP).
Semigroup m =>
(a -> m) -> NERAVec' n b a -> m
foldMap1' a -> m
f (Last  Tree n a
t)   = (a -> m) -> Tree n a -> m
forall s a (n :: Nat). Semigroup s => (a -> s) -> Tree n a -> s
Tree.foldMap1 a -> m
f Tree n a
t
foldMap1' a -> m
f (Cons0   NERAVec' ('S n) b a
r) = (a -> m) -> NERAVec' ('S n) b a -> m
forall m a (n :: Nat) (b :: BinP).
Semigroup m =>
(a -> m) -> NERAVec' n b a -> m
foldMap1' a -> m
f NERAVec' ('S n) b a
r
foldMap1' a -> m
f (Cons1 Tree n a
t NERAVec' ('S n) b a
r) = (a -> m) -> Tree n a -> m
forall s a (n :: Nat). Semigroup s => (a -> s) -> Tree n a -> s
Tree.foldMap1 a -> m
f Tree n a
t m -> m -> m
forall a. Semigroup a => a -> a -> a
<> (a -> m) -> NERAVec' ('S n) b a -> m
forall m a (n :: Nat) (b :: BinP).
Semigroup m =>
(a -> m) -> NERAVec' n b a -> m
foldMap1' a -> m
f NERAVec' ('S n) b a
r

ifoldMap1 :: Semigroup m => (PosP b -> a -> m) -> NERAVec b a -> m
ifoldMap1 :: forall m (b :: BinP) a.
Semigroup m =>
(PosP b -> a -> m) -> NERAVec b a -> m
ifoldMap1 PosP b -> a -> m
f (NE NERAVec' 'Z b a
xs) = (PosP' 'Z b -> a -> m) -> NERAVec' 'Z b a -> m
forall m (n :: Nat) (b :: BinP) a.
Semigroup m =>
(PosP' n b -> a -> m) -> NERAVec' n b a -> m
ifoldMap1' (PosP b -> a -> m
f (PosP b -> a -> m)
-> (PosP' 'Z b -> PosP b) -> PosP' 'Z b -> a -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PosP' 'Z b -> PosP b
forall (b :: BinP). PosP' 'Z b -> PosP b
PosP) NERAVec' 'Z b a
xs

ifoldMap1' :: Semigroup m => (PosP' n b -> a -> m) -> NERAVec' n b a -> m
ifoldMap1' :: forall m (n :: Nat) (b :: BinP) a.
Semigroup m =>
(PosP' n b -> a -> m) -> NERAVec' n b a -> m
ifoldMap1' PosP' n b -> a -> m
f (Last  Tree n a
t)   = (Wrd n -> a -> m) -> Tree n a -> m
forall s (n :: Nat) a.
Semigroup s =>
(Wrd n -> a -> s) -> Tree n a -> s
Tree.ifoldMap1 (PosP' n b -> a -> m
f (PosP' n b -> a -> m) -> (Wrd n -> PosP' n b) -> Wrd n -> a -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrd n -> PosP' n b
Wrd n -> PosP' n 'BE
forall (n :: Nat). Wrd n -> PosP' n 'BE
AtEnd) Tree n a
t
ifoldMap1' PosP' n b -> a -> m
f (Cons0   NERAVec' ('S n) b a
r) = (PosP' ('S n) b -> a -> m) -> NERAVec' ('S n) b a -> m
forall m (n :: Nat) (b :: BinP) a.
Semigroup m =>
(PosP' n b -> a -> m) -> NERAVec' n b a -> m
ifoldMap1' (PosP' n b -> a -> m
f (PosP' n b -> a -> m)
-> (PosP' ('S n) b -> PosP' n b) -> PosP' ('S n) b -> a -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PosP' ('S n) b -> PosP' n b
PosP' ('S n) b -> PosP' n ('B0 b)
forall (n :: Nat) (b1 :: BinP). PosP' ('S n) b1 -> PosP' n ('B0 b1)
There0) NERAVec' ('S n) b a
r
ifoldMap1' PosP' n b -> a -> m
f (Cons1 Tree n a
t NERAVec' ('S n) b a
r) = (Wrd n -> a -> m) -> Tree n a -> m
forall s (n :: Nat) a.
Semigroup s =>
(Wrd n -> a -> s) -> Tree n a -> s
Tree.ifoldMap1 (PosP' n b -> a -> m
f (PosP' n b -> a -> m) -> (Wrd n -> PosP' n b) -> Wrd n -> a -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrd n -> PosP' n b
Wrd n -> PosP' n ('B1 b)
forall (n :: Nat) (b1 :: BinP). Wrd n -> PosP' n ('B1 b1)
Here) Tree n a
t m -> m -> m
forall a. Semigroup a => a -> a -> a
<> (PosP' ('S n) b -> a -> m) -> NERAVec' ('S n) b a -> m
forall m (n :: Nat) (b :: BinP) a.
Semigroup m =>
(PosP' n b -> a -> m) -> NERAVec' n b a -> m
ifoldMap1' (PosP' n b -> a -> m
f (PosP' n b -> a -> m)
-> (PosP' ('S n) b -> PosP' n b) -> PosP' ('S n) b -> a -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PosP' ('S n) b -> PosP' n b
PosP' ('S n) b -> PosP' n ('B1 b)
forall (n :: Nat) (b1 :: BinP). PosP' ('S n) b1 -> PosP' n ('B1 b1)
There1) NERAVec' ('S n) b a
r

foldr :: (a -> b -> b) -> b -> NERAVec m a -> b
foldr :: forall a b (m :: BinP). (a -> b -> b) -> b -> NERAVec m a -> b
foldr a -> b -> b
f b
z (NE NERAVec' 'Z m a
xs) = (a -> b -> b) -> b -> NERAVec' 'Z m a -> b
forall a b (n :: Nat) (m :: BinP).
(a -> b -> b) -> b -> NERAVec' n m a -> b
foldr' a -> b -> b
f b
z NERAVec' 'Z m a
xs

foldr1Map :: (a -> b -> b) -> (a -> b) -> NERAVec m a -> b
foldr1Map :: forall a b (m :: BinP).
(a -> b -> b) -> (a -> b) -> NERAVec m a -> b
foldr1Map a -> b -> b
f a -> b
z (NE NERAVec' 'Z m a
xs) = (a -> b -> b) -> (a -> b) -> NERAVec' 'Z m a -> b
forall a b (n :: Nat) (m :: BinP).
(a -> b -> b) -> (a -> b) -> NERAVec' n m a -> b
foldr1Map' a -> b -> b
f a -> b
z NERAVec' 'Z m a
xs

ifoldr1Map :: (PosP m -> a -> b -> b) -> (PosP m -> a -> b) -> NERAVec m a -> b
ifoldr1Map :: forall (m :: BinP) a b.
(PosP m -> a -> b -> b) -> (PosP m -> a -> b) -> NERAVec m a -> b
ifoldr1Map PosP m -> a -> b -> b
f PosP m -> a -> b
z (NE NERAVec' 'Z m a
xs) = (PosP' 'Z m -> a -> b -> b)
-> (PosP' 'Z m -> a -> b) -> NERAVec' 'Z m a -> b
forall (n :: Nat) (m :: BinP) a b.
(PosP' n m -> a -> b -> b)
-> (PosP' n m -> a -> b) -> NERAVec' n m a -> b
ifoldr1Map' (PosP m -> a -> b -> b
f (PosP m -> a -> b -> b)
-> (PosP' 'Z m -> PosP m) -> PosP' 'Z m -> a -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PosP' 'Z m -> PosP m
forall (b :: BinP). PosP' 'Z b -> PosP b
PosP) (PosP m -> a -> b
z (PosP m -> a -> b)
-> (PosP' 'Z m -> PosP m) -> PosP' 'Z m -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PosP' 'Z m -> PosP m
forall (b :: BinP). PosP' 'Z b -> PosP b
PosP) NERAVec' 'Z m a
xs

foldr' :: (a -> b -> b) -> b -> NERAVec' n m a -> b
foldr' :: forall a b (n :: Nat) (m :: BinP).
(a -> b -> b) -> b -> NERAVec' n m a -> b
foldr' a -> b -> b
f b
z (Last  Tree n a
t)   = (a -> b -> b) -> b -> Tree n a -> b
forall a b (n :: Nat). (a -> b -> b) -> b -> Tree n a -> b
Tree.foldr a -> b -> b
f b
z Tree n a
t
foldr' a -> b -> b
f b
z (Cons0   NERAVec' ('S n) b a
r) = (a -> b -> b) -> b -> NERAVec' ('S n) b a -> b
forall a b (n :: Nat) (m :: BinP).
(a -> b -> b) -> b -> NERAVec' n m a -> b
foldr' a -> b -> b
f b
z NERAVec' ('S n) b a
r
foldr' a -> b -> b
f b
z (Cons1 Tree n a
t NERAVec' ('S n) b a
r) = (a -> b -> b) -> b -> Tree n a -> b
forall a b (n :: Nat). (a -> b -> b) -> b -> Tree n a -> b
Tree.foldr a -> b -> b
f ((a -> b -> b) -> b -> NERAVec' ('S n) b a -> b
forall a b (n :: Nat) (m :: BinP).
(a -> b -> b) -> b -> NERAVec' n m a -> b
foldr' a -> b -> b
f b
z NERAVec' ('S n) b a
r) Tree n a
t

foldr1Map' :: (a -> b -> b) -> (a -> b) -> NERAVec' n m a -> b
foldr1Map' :: forall a b (n :: Nat) (m :: BinP).
(a -> b -> b) -> (a -> b) -> NERAVec' n m a -> b
foldr1Map' a -> b -> b
f a -> b
z (Last Tree n a
t)    = (a -> b -> b) -> (a -> b) -> Tree n a -> b
forall a b (n :: Nat). (a -> b -> b) -> (a -> b) -> Tree n a -> b
Tree.foldr1Map a -> b -> b
f a -> b
z Tree n a
t
foldr1Map' a -> b -> b
f a -> b
z (Cons0   NERAVec' ('S n) b a
r) = (a -> b -> b) -> (a -> b) -> NERAVec' ('S n) b a -> b
forall a b (n :: Nat) (m :: BinP).
(a -> b -> b) -> (a -> b) -> NERAVec' n m a -> b
foldr1Map' a -> b -> b
f a -> b
z NERAVec' ('S n) b a
r
foldr1Map' a -> b -> b
f a -> b
z (Cons1 Tree n a
t NERAVec' ('S n) b a
r) = (a -> b -> b) -> b -> Tree n a -> b
forall a b (n :: Nat). (a -> b -> b) -> b -> Tree n a -> b
Tree.foldr a -> b -> b
f ((a -> b -> b) -> (a -> b) -> NERAVec' ('S n) b a -> b
forall a b (n :: Nat) (m :: BinP).
(a -> b -> b) -> (a -> b) -> NERAVec' n m a -> b
foldr1Map' a -> b -> b
f a -> b
z NERAVec' ('S n) b a
r) Tree n a
t

ifoldr1Map' :: (PosP' n m -> a -> b -> b) -> (PosP' n m -> a -> b) -> NERAVec' n m a -> b
ifoldr1Map' :: forall (n :: Nat) (m :: BinP) a b.
(PosP' n m -> a -> b -> b)
-> (PosP' n m -> a -> b) -> NERAVec' n m a -> b
ifoldr1Map' PosP' n m -> a -> b -> b
f PosP' n m -> a -> b
z (Last Tree n a
t)    = (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
Tree.ifoldr1Map (PosP' n m -> a -> b -> b
f (PosP' n m -> a -> b -> b)
-> (Wrd n -> PosP' n m) -> Wrd n -> a -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrd n -> PosP' n m
Wrd n -> PosP' n 'BE
forall (n :: Nat). Wrd n -> PosP' n 'BE
AtEnd) (PosP' n m -> a -> b
z (PosP' n m -> a -> b) -> (Wrd n -> PosP' n m) -> Wrd n -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrd n -> PosP' n m
Wrd n -> PosP' n 'BE
forall (n :: Nat). Wrd n -> PosP' n 'BE
AtEnd) Tree n a
t
ifoldr1Map' PosP' n m -> a -> b -> b
f PosP' n m -> a -> b
z (Cons0   NERAVec' ('S n) b a
r) = (PosP' ('S n) b -> a -> b -> b)
-> (PosP' ('S n) b -> a -> b) -> NERAVec' ('S n) b a -> b
forall (n :: Nat) (m :: BinP) a b.
(PosP' n m -> a -> b -> b)
-> (PosP' n m -> a -> b) -> NERAVec' n m a -> b
ifoldr1Map' (PosP' n m -> a -> b -> b
f (PosP' n m -> a -> b -> b)
-> (PosP' ('S n) b -> PosP' n m) -> PosP' ('S n) b -> a -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PosP' ('S n) b -> PosP' n m
PosP' ('S n) b -> PosP' n ('B0 b)
forall (n :: Nat) (b1 :: BinP). PosP' ('S n) b1 -> PosP' n ('B0 b1)
There0) (PosP' n m -> a -> b
z (PosP' n m -> a -> b)
-> (PosP' ('S n) b -> PosP' n m) -> PosP' ('S n) b -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PosP' ('S n) b -> PosP' n m
PosP' ('S n) b -> PosP' n ('B0 b)
forall (n :: Nat) (b1 :: BinP). PosP' ('S n) b1 -> PosP' n ('B0 b1)
There0) NERAVec' ('S n) b a
r
ifoldr1Map' PosP' n m -> a -> b -> b
f PosP' n m -> a -> b
z (Cons1 Tree n a
t NERAVec' ('S n) b a
r) = (Wrd n -> a -> b -> b) -> b -> Tree n a -> b
forall (n :: Nat) a b. (Wrd n -> a -> b -> b) -> b -> Tree n a -> b
Tree.ifoldr (PosP' n m -> a -> b -> b
f (PosP' n m -> a -> b -> b)
-> (Wrd n -> PosP' n m) -> Wrd n -> a -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrd n -> PosP' n m
Wrd n -> PosP' n ('B1 b)
forall (n :: Nat) (b1 :: BinP). Wrd n -> PosP' n ('B1 b1)
Here) ((PosP' ('S n) b -> a -> b -> b)
-> (PosP' ('S n) b -> a -> b) -> NERAVec' ('S n) b a -> b
forall (n :: Nat) (m :: BinP) a b.
(PosP' n m -> a -> b -> b)
-> (PosP' n m -> a -> b) -> NERAVec' n m a -> b
ifoldr1Map' (PosP' n m -> a -> b -> b
f (PosP' n m -> a -> b -> b)
-> (PosP' ('S n) b -> PosP' n m) -> PosP' ('S n) b -> a -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PosP' ('S n) b -> PosP' n m
PosP' ('S n) b -> PosP' n ('B1 b)
forall (n :: Nat) (b1 :: BinP). PosP' ('S n) b1 -> PosP' n ('B1 b1)
There1) (PosP' n m -> a -> b
z (PosP' n m -> a -> b)
-> (PosP' ('S n) b -> PosP' n m) -> PosP' ('S n) b -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PosP' ('S n) b -> PosP' n m
PosP' ('S n) b -> PosP' n ('B1 b)
forall (n :: Nat) (b1 :: BinP). PosP' ('S n) b1 -> PosP' n ('B1 b1)
There1) NERAVec' ('S n) b a
r) Tree n a
t

ifoldr :: (PosP m -> a -> b -> b) -> b -> NERAVec m a -> b
ifoldr :: forall (n :: BinP) a b.
(PosP n -> a -> b -> b) -> b -> NERAVec n a -> b
ifoldr  PosP m -> a -> b -> b
f b
z (NE NERAVec' 'Z m a
xs) = (PosP' 'Z m -> a -> b -> b) -> b -> NERAVec' 'Z m a -> b
forall (n :: Nat) (m :: BinP) a b.
(PosP' n m -> a -> b -> b) -> b -> NERAVec' n m a -> b
ifoldr' (PosP m -> a -> b -> b
f (PosP m -> a -> b -> b)
-> (PosP' 'Z m -> PosP m) -> PosP' 'Z m -> a -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PosP' 'Z m -> PosP m
forall (b :: BinP). PosP' 'Z b -> PosP b
PosP) b
z NERAVec' 'Z m a
xs

ifoldr' :: (PosP' n m -> a -> b -> b) -> b -> NERAVec' n m a -> b
ifoldr' :: forall (n :: Nat) (m :: BinP) a b.
(PosP' n m -> a -> b -> b) -> b -> NERAVec' n m a -> b
ifoldr' PosP' n m -> a -> b -> b
f b
z (Last  Tree n a
t)   = (Wrd n -> a -> b -> b) -> b -> Tree n a -> b
forall (n :: Nat) a b. (Wrd n -> a -> b -> b) -> b -> Tree n a -> b
Tree.ifoldr (PosP' n m -> a -> b -> b
f (PosP' n m -> a -> b -> b)
-> (Wrd n -> PosP' n m) -> Wrd n -> a -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrd n -> PosP' n m
Wrd n -> PosP' n 'BE
forall (n :: Nat). Wrd n -> PosP' n 'BE
AtEnd) b
z Tree n a
t
ifoldr' PosP' n m -> a -> b -> b
f b
z (Cons0   NERAVec' ('S n) b a
r) = (PosP' ('S n) b -> a -> b -> b) -> b -> NERAVec' ('S n) b a -> b
forall (n :: Nat) (m :: BinP) a b.
(PosP' n m -> a -> b -> b) -> b -> NERAVec' n m a -> b
ifoldr' (PosP' n m -> a -> b -> b
f (PosP' n m -> a -> b -> b)
-> (PosP' ('S n) b -> PosP' n m) -> PosP' ('S n) b -> a -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PosP' ('S n) b -> PosP' n m
PosP' ('S n) b -> PosP' n ('B0 b)
forall (n :: Nat) (b1 :: BinP). PosP' ('S n) b1 -> PosP' n ('B0 b1)
There0) b
z NERAVec' ('S n) b a
r
ifoldr' PosP' n m -> a -> b -> b
f b
z (Cons1 Tree n a
t NERAVec' ('S n) b a
r) = (Wrd n -> a -> b -> b) -> b -> Tree n a -> b
forall (n :: Nat) a b. (Wrd n -> a -> b -> b) -> b -> Tree n a -> b
Tree.ifoldr (PosP' n m -> a -> b -> b
f (PosP' n m -> a -> b -> b)
-> (Wrd n -> PosP' n m) -> Wrd n -> a -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrd n -> PosP' n m
Wrd n -> PosP' n ('B1 b)
forall (n :: Nat) (b1 :: BinP). Wrd n -> PosP' n ('B1 b1)
Here) ((PosP' ('S n) b -> a -> b -> b) -> b -> NERAVec' ('S n) b a -> b
forall (n :: Nat) (m :: BinP) a b.
(PosP' n m -> a -> b -> b) -> b -> NERAVec' n m a -> b
ifoldr' (PosP' n m -> a -> b -> b
f (PosP' n m -> a -> b -> b)
-> (PosP' ('S n) b -> PosP' n m) -> PosP' ('S n) b -> a -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PosP' ('S n) b -> PosP' n m
PosP' ('S n) b -> PosP' n ('B1 b)
forall (n :: Nat) (b1 :: BinP). PosP' ('S n) b1 -> PosP' n ('B1 b1)
There1) b
z NERAVec' ('S n) b a
r) Tree n a
t

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

-- TBW

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

map :: (a -> b) -> NERAVec m a -> NERAVec m b
map :: forall a b (m :: BinP). (a -> b) -> NERAVec m a -> NERAVec m b
map a -> b
f (NE NERAVec' 'Z m a
xs) = NERAVec' 'Z m b -> NERAVec m b
forall (b :: BinP) a. NERAVec' 'Z b a -> NERAVec b a
NE ((a -> b) -> NERAVec' 'Z m a -> NERAVec' 'Z m b
forall a b (n :: Nat) (m :: BinP).
(a -> b) -> NERAVec' n m a -> NERAVec' n m b
map' a -> b
f NERAVec' 'Z m a
xs)

map' :: (a -> b) -> NERAVec' n m a -> NERAVec' n m b
map' :: forall a b (n :: Nat) (m :: BinP).
(a -> b) -> NERAVec' n m a -> NERAVec' n m b
map' a -> b
f (Last   Tree n a
t ) = Tree n b -> NERAVec' n 'BE b
forall (n :: Nat) a. Tree n a -> NERAVec' n 'BE a
Last ((a -> b) -> Tree n a -> Tree n b
forall a b (n :: Nat). (a -> b) -> Tree n a -> Tree n b
Tree.map a -> b
f Tree n a
t)
map' a -> b
f (Cons0   NERAVec' ('S n) b a
r) = NERAVec' ('S n) b b -> NERAVec' n ('B0 b) b
forall (n :: Nat) (b :: BinP) a.
NERAVec' ('S n) b a -> NERAVec' n ('B0 b) a
Cons0 ((a -> b) -> NERAVec' ('S n) b a -> NERAVec' ('S n) b b
forall a b (n :: Nat) (m :: BinP).
(a -> b) -> NERAVec' n m a -> NERAVec' n m b
map' a -> b
f NERAVec' ('S n) b a
r)
map' a -> b
f (Cons1 Tree n a
t NERAVec' ('S n) b a
r) = Tree n b -> NERAVec' ('S n) b b -> NERAVec' n ('B1 b) b
forall (n :: Nat) a (b :: BinP).
Tree n a -> NERAVec' ('S n) b a -> NERAVec' n ('B1 b) a
Cons1 ((a -> b) -> Tree n a -> Tree n b
forall a b (n :: Nat). (a -> b) -> Tree n a -> Tree n b
Tree.map a -> b
f Tree n a
t) ((a -> b) -> NERAVec' ('S n) b a -> NERAVec' ('S n) b b
forall a b (n :: Nat) (m :: BinP).
(a -> b) -> NERAVec' n m a -> NERAVec' n m b
map' a -> b
f NERAVec' ('S n) b a
r)

imap :: (PosP m -> a -> b) -> NERAVec m a -> NERAVec m b
imap :: forall (n :: BinP) a b.
(PosP n -> a -> b) -> NERAVec n a -> NERAVec n b
imap PosP m -> a -> b
f (NE NERAVec' 'Z m a
xs) = NERAVec' 'Z m b -> NERAVec m b
forall (b :: BinP) a. NERAVec' 'Z b a -> NERAVec b a
NE ((PosP' 'Z m -> a -> b) -> NERAVec' 'Z m a -> NERAVec' 'Z m b
forall (n :: Nat) (m :: BinP) a b.
(PosP' n m -> a -> b) -> NERAVec' n m a -> NERAVec' n m b
imap' (PosP m -> a -> b
f (PosP m -> a -> b)
-> (PosP' 'Z m -> PosP m) -> PosP' 'Z m -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PosP' 'Z m -> PosP m
forall (b :: BinP). PosP' 'Z b -> PosP b
PosP) NERAVec' 'Z m a
xs)

imap' :: (PosP' n m -> a -> b) -> NERAVec' n m a -> NERAVec' n m b
imap' :: forall (n :: Nat) (m :: BinP) a b.
(PosP' n m -> a -> b) -> NERAVec' n m a -> NERAVec' n m b
imap' PosP' n m -> a -> b
f (Last  Tree n a
t)   = Tree n b -> NERAVec' n 'BE b
forall (n :: Nat) a. Tree n a -> NERAVec' n 'BE a
Last ((Wrd n -> a -> b) -> Tree n a -> Tree n b
forall (n :: Nat) a b. (Wrd n -> a -> b) -> Tree n a -> Tree n b
Tree.imap (PosP' n m -> a -> b
f (PosP' n m -> a -> b) -> (Wrd n -> PosP' n m) -> Wrd n -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrd n -> PosP' n m
Wrd n -> PosP' n 'BE
forall (n :: Nat). Wrd n -> PosP' n 'BE
AtEnd) Tree n a
t)
imap' PosP' n m -> a -> b
f (Cons0   NERAVec' ('S n) b a
r) = NERAVec' ('S n) b b -> NERAVec' n ('B0 b) b
forall (n :: Nat) (b :: BinP) a.
NERAVec' ('S n) b a -> NERAVec' n ('B0 b) a
Cons0 ((PosP' ('S n) b -> a -> b)
-> NERAVec' ('S n) b a -> NERAVec' ('S n) b b
forall (n :: Nat) (m :: BinP) a b.
(PosP' n m -> a -> b) -> NERAVec' n m a -> NERAVec' n m b
imap' (PosP' n m -> a -> b
f (PosP' n m -> a -> b)
-> (PosP' ('S n) b -> PosP' n m) -> PosP' ('S n) b -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PosP' ('S n) b -> PosP' n m
PosP' ('S n) b -> PosP' n ('B0 b)
forall (n :: Nat) (b1 :: BinP). PosP' ('S n) b1 -> PosP' n ('B0 b1)
There0) NERAVec' ('S n) b a
r)
imap' PosP' n m -> a -> b
f (Cons1 Tree n a
t NERAVec' ('S n) b a
r) = Tree n b -> NERAVec' ('S n) b b -> NERAVec' n ('B1 b) b
forall (n :: Nat) a (b :: BinP).
Tree n a -> NERAVec' ('S n) b a -> NERAVec' n ('B1 b) a
Cons1 ((Wrd n -> a -> b) -> Tree n a -> Tree n b
forall (n :: Nat) a b. (Wrd n -> a -> b) -> Tree n a -> Tree n b
Tree.imap (PosP' n m -> a -> b
f (PosP' n m -> a -> b) -> (Wrd n -> PosP' n m) -> Wrd n -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrd n -> PosP' n m
Wrd n -> PosP' n ('B1 b)
forall (n :: Nat) (b1 :: BinP). Wrd n -> PosP' n ('B1 b1)
Here) Tree n a
t) ((PosP' ('S n) b -> a -> b)
-> NERAVec' ('S n) b a -> NERAVec' ('S n) b b
forall (n :: Nat) (m :: BinP) a b.
(PosP' n m -> a -> b) -> NERAVec' n m a -> NERAVec' n m b
imap' (PosP' n m -> a -> b
f (PosP' n m -> a -> b)
-> (PosP' ('S n) b -> PosP' n m) -> PosP' ('S n) b -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PosP' ('S n) b -> PosP' n m
PosP' ('S n) b -> PosP' n ('B1 b)
forall (n :: Nat) (b1 :: BinP). PosP' ('S n) b1 -> PosP' n ('B1 b1)
There1) NERAVec' ('S n) b a
r)

traverse :: Applicative f => (a -> f b) -> NERAVec m a -> f (NERAVec m b)
traverse :: forall (f :: * -> *) a b (m :: BinP).
Applicative f =>
(a -> f b) -> NERAVec m a -> f (NERAVec m b)
traverse a -> f b
f (NE NERAVec' 'Z m a
xs) = (NERAVec' 'Z m b -> NERAVec m b)
-> f (NERAVec' 'Z m b) -> f (NERAVec m b)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NERAVec' 'Z m b -> NERAVec m b
forall (b :: BinP) a. NERAVec' 'Z b a -> NERAVec b a
NE ((a -> f b) -> NERAVec' 'Z m a -> f (NERAVec' 'Z m b)
forall (f :: * -> *) a b (n :: Nat) (m :: BinP).
Applicative f =>
(a -> f b) -> NERAVec' n m a -> f (NERAVec' n m b)
traverse' a -> f b
f NERAVec' 'Z m a
xs)

traverse' :: Applicative f => (a -> f b) -> NERAVec' n m a -> f (NERAVec' n m b)
traverse' :: forall (f :: * -> *) a b (n :: Nat) (m :: BinP).
Applicative f =>
(a -> f b) -> NERAVec' n m a -> f (NERAVec' n m b)
traverse' a -> f b
f (Last  Tree n a
t)   = Tree n b -> NERAVec' n m b
Tree n b -> NERAVec' n 'BE b
forall (n :: Nat) a. Tree n a -> NERAVec' n 'BE a
Last (Tree n b -> NERAVec' n m b) -> f (Tree n b) -> f (NERAVec' n m b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> f b) -> Tree n a -> f (Tree n b)
forall (f :: * -> *) a b (n :: Nat).
Applicative f =>
(a -> f b) -> Tree n a -> f (Tree n b)
Tree.traverse a -> f b
f Tree n a
t
traverse' a -> f b
f (Cons0   NERAVec' ('S n) b a
r) = NERAVec' ('S n) b b -> NERAVec' n m b
NERAVec' ('S n) b b -> NERAVec' n ('B0 b) b
forall (n :: Nat) (b :: BinP) a.
NERAVec' ('S n) b a -> NERAVec' n ('B0 b) a
Cons0 (NERAVec' ('S n) b b -> NERAVec' n m b)
-> f (NERAVec' ('S n) b b) -> f (NERAVec' n m b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> f b) -> NERAVec' ('S n) b a -> f (NERAVec' ('S n) b b)
forall (f :: * -> *) a b (n :: Nat) (m :: BinP).
Applicative f =>
(a -> f b) -> NERAVec' n m a -> f (NERAVec' n m b)
traverse' a -> f b
f NERAVec' ('S n) b a
r
traverse' a -> f b
f (Cons1 Tree n a
t NERAVec' ('S n) b a
r) = Tree n b -> NERAVec' ('S n) b b -> NERAVec' n m b
Tree n b -> NERAVec' ('S n) b b -> NERAVec' n ('B1 b) b
forall (n :: Nat) a (b :: BinP).
Tree n a -> NERAVec' ('S n) b a -> NERAVec' n ('B1 b) a
Cons1 (Tree n b -> NERAVec' ('S n) b b -> NERAVec' n m b)
-> f (Tree n b) -> f (NERAVec' ('S n) b b -> NERAVec' n m b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> f b) -> Tree n a -> f (Tree n b)
forall (f :: * -> *) a b (n :: Nat).
Applicative f =>
(a -> f b) -> Tree n a -> f (Tree n b)
Tree.traverse a -> f b
f Tree n a
t f (NERAVec' ('S n) b b -> NERAVec' n m b)
-> f (NERAVec' ('S n) b b) -> f (NERAVec' n m b)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (a -> f b) -> NERAVec' ('S n) b a -> f (NERAVec' ('S n) b b)
forall (f :: * -> *) a b (n :: Nat) (m :: BinP).
Applicative f =>
(a -> f b) -> NERAVec' n m a -> f (NERAVec' n m b)
traverse' a -> f b
f NERAVec' ('S n) b a
r

itraverse :: Applicative f => (PosP m -> a -> f b) -> NERAVec m a -> f (NERAVec m b)
itraverse :: forall (f :: * -> *) (m :: BinP) a b.
Applicative f =>
(PosP m -> a -> f b) -> NERAVec m a -> f (NERAVec m b)
itraverse PosP m -> a -> f b
f (NE NERAVec' 'Z m a
xs) = (NERAVec' 'Z m b -> NERAVec m b)
-> f (NERAVec' 'Z m b) -> f (NERAVec m b)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NERAVec' 'Z m b -> NERAVec m b
forall (b :: BinP) a. NERAVec' 'Z b a -> NERAVec b a
NE ((PosP' 'Z m -> a -> f b) -> NERAVec' 'Z m a -> f (NERAVec' 'Z m b)
forall (f :: * -> *) (n :: Nat) (m :: BinP) a b.
Applicative f =>
(PosP' n m -> a -> f b) -> NERAVec' n m a -> f (NERAVec' n m b)
itraverse' (PosP m -> a -> f b
f (PosP m -> a -> f b)
-> (PosP' 'Z m -> PosP m) -> PosP' 'Z m -> a -> f b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PosP' 'Z m -> PosP m
forall (b :: BinP). PosP' 'Z b -> PosP b
PosP) NERAVec' 'Z m a
xs)

itraverse' :: Applicative f => (PosP' n m -> a -> f b) -> NERAVec' n m a -> f (NERAVec' n m b)
itraverse' :: forall (f :: * -> *) (n :: Nat) (m :: BinP) a b.
Applicative f =>
(PosP' n m -> a -> f b) -> NERAVec' n m a -> f (NERAVec' n m b)
itraverse' PosP' n m -> a -> f b
f (Last  Tree n a
t)   = Tree n b -> NERAVec' n m b
Tree n b -> NERAVec' n 'BE b
forall (n :: Nat) a. Tree n a -> NERAVec' n 'BE a
Last (Tree n b -> NERAVec' n m b) -> f (Tree n b) -> f (NERAVec' n m b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Wrd n -> a -> f b) -> Tree n a -> f (Tree n b)
forall (f :: * -> *) (n :: Nat) a b.
Applicative f =>
(Wrd n -> a -> f b) -> Tree n a -> f (Tree n b)
Tree.itraverse (PosP' n m -> a -> f b
f (PosP' n m -> a -> f b)
-> (Wrd n -> PosP' n m) -> Wrd n -> a -> f b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrd n -> PosP' n m
Wrd n -> PosP' n 'BE
forall (n :: Nat). Wrd n -> PosP' n 'BE
AtEnd) Tree n a
t
itraverse' PosP' n m -> a -> f b
f (Cons0   NERAVec' ('S n) b a
r) = NERAVec' ('S n) b b -> NERAVec' n m b
NERAVec' ('S n) b b -> NERAVec' n ('B0 b) b
forall (n :: Nat) (b :: BinP) a.
NERAVec' ('S n) b a -> NERAVec' n ('B0 b) a
Cons0 (NERAVec' ('S n) b b -> NERAVec' n m b)
-> f (NERAVec' ('S n) b b) -> f (NERAVec' n m b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (PosP' ('S n) b -> a -> f b)
-> NERAVec' ('S n) b a -> f (NERAVec' ('S n) b b)
forall (f :: * -> *) (n :: Nat) (m :: BinP) a b.
Applicative f =>
(PosP' n m -> a -> f b) -> NERAVec' n m a -> f (NERAVec' n m b)
itraverse' (PosP' n m -> a -> f b
f (PosP' n m -> a -> f b)
-> (PosP' ('S n) b -> PosP' n m) -> PosP' ('S n) b -> a -> f b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PosP' ('S n) b -> PosP' n m
PosP' ('S n) b -> PosP' n ('B0 b)
forall (n :: Nat) (b1 :: BinP). PosP' ('S n) b1 -> PosP' n ('B0 b1)
There0) NERAVec' ('S n) b a
r
itraverse' PosP' n m -> a -> f b
f (Cons1 Tree n a
t NERAVec' ('S n) b a
r) = Tree n b -> NERAVec' ('S n) b b -> NERAVec' n m b
Tree n b -> NERAVec' ('S n) b b -> NERAVec' n ('B1 b) b
forall (n :: Nat) a (b :: BinP).
Tree n a -> NERAVec' ('S n) b a -> NERAVec' n ('B1 b) a
Cons1 (Tree n b -> NERAVec' ('S n) b b -> NERAVec' n m b)
-> f (Tree n b) -> f (NERAVec' ('S n) b b -> NERAVec' n m b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Wrd n -> a -> f b) -> Tree n a -> f (Tree n b)
forall (f :: * -> *) (n :: Nat) a b.
Applicative f =>
(Wrd n -> a -> f b) -> Tree n a -> f (Tree n b)
Tree.itraverse (PosP' n m -> a -> f b
f (PosP' n m -> a -> f b)
-> (Wrd n -> PosP' n m) -> Wrd n -> a -> f b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrd n -> PosP' n m
Wrd n -> PosP' n ('B1 b)
forall (n :: Nat) (b1 :: BinP). Wrd n -> PosP' n ('B1 b1)
Here) Tree n a
t f (NERAVec' ('S n) b b -> NERAVec' n m b)
-> f (NERAVec' ('S n) b b) -> f (NERAVec' n m b)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (PosP' ('S n) b -> a -> f b)
-> NERAVec' ('S n) b a -> f (NERAVec' ('S n) b b)
forall (f :: * -> *) (n :: Nat) (m :: BinP) a b.
Applicative f =>
(PosP' n m -> a -> f b) -> NERAVec' n m a -> f (NERAVec' n m b)
itraverse' (PosP' n m -> a -> f b
f (PosP' n m -> a -> f b)
-> (PosP' ('S n) b -> PosP' n m) -> PosP' ('S n) b -> a -> f b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PosP' ('S n) b -> PosP' n m
PosP' ('S n) b -> PosP' n ('B1 b)
forall (n :: Nat) (b1 :: BinP). PosP' ('S n) b1 -> PosP' n ('B1 b1)
There1) NERAVec' ('S n) b a
r

#ifdef MIN_VERSION_semigroupoids
traverse1 :: Apply f => (a -> f b) -> NERAVec m a -> f (NERAVec m b)
traverse1 :: forall (f :: * -> *) a b (m :: BinP).
Apply f =>
(a -> f b) -> NERAVec m a -> f (NERAVec m b)
traverse1 a -> f b
f (NE NERAVec' 'Z m a
xs) = (NERAVec' 'Z m b -> NERAVec m b)
-> f (NERAVec' 'Z m b) -> f (NERAVec m b)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NERAVec' 'Z m b -> NERAVec m b
forall (b :: BinP) a. NERAVec' 'Z b a -> NERAVec b a
NE ((a -> f b) -> NERAVec' 'Z m a -> f (NERAVec' 'Z m b)
forall (f :: * -> *) a b (n :: Nat) (m :: BinP).
Apply f =>
(a -> f b) -> NERAVec' n m a -> f (NERAVec' n m b)
traverse1' a -> f b
f NERAVec' 'Z m a
xs)

traverse1' :: Apply f => (a -> f b) -> NERAVec' n m a -> f (NERAVec' n m b)
traverse1' :: forall (f :: * -> *) a b (n :: Nat) (m :: BinP).
Apply f =>
(a -> f b) -> NERAVec' n m a -> f (NERAVec' n m b)
traverse1' a -> f b
f (Last  Tree n a
t)   = Tree n b -> NERAVec' n m b
Tree n b -> NERAVec' n 'BE b
forall (n :: Nat) a. Tree n a -> NERAVec' n 'BE a
Last (Tree n b -> NERAVec' n m b) -> f (Tree n b) -> f (NERAVec' n m b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> f b) -> Tree n a -> f (Tree n b)
forall (f :: * -> *) a b (n :: Nat).
Apply f =>
(a -> f b) -> Tree n a -> f (Tree n b)
Tree.traverse1 a -> f b
f Tree n a
t
traverse1' a -> f b
f (Cons0   NERAVec' ('S n) b a
r) = NERAVec' ('S n) b b -> NERAVec' n m b
NERAVec' ('S n) b b -> NERAVec' n ('B0 b) b
forall (n :: Nat) (b :: BinP) a.
NERAVec' ('S n) b a -> NERAVec' n ('B0 b) a
Cons0 (NERAVec' ('S n) b b -> NERAVec' n m b)
-> f (NERAVec' ('S n) b b) -> f (NERAVec' n m b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> f b) -> NERAVec' ('S n) b a -> f (NERAVec' ('S n) b b)
forall (f :: * -> *) a b (n :: Nat) (m :: BinP).
Apply f =>
(a -> f b) -> NERAVec' n m a -> f (NERAVec' n m b)
traverse1' a -> f b
f NERAVec' ('S n) b a
r
traverse1' a -> f b
f (Cons1 Tree n a
t NERAVec' ('S n) b a
r) = Tree n b -> NERAVec' ('S n) b b -> NERAVec' n m b
Tree n b -> NERAVec' ('S n) b b -> NERAVec' n ('B1 b) b
forall (n :: Nat) a (b :: BinP).
Tree n a -> NERAVec' ('S n) b a -> NERAVec' n ('B1 b) a
Cons1 (Tree n b -> NERAVec' ('S n) b b -> NERAVec' n m b)
-> f (Tree n b) -> f (NERAVec' ('S n) b b -> NERAVec' n m b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> f b) -> Tree n a -> f (Tree n b)
forall (f :: * -> *) a b (n :: Nat).
Apply f =>
(a -> f b) -> Tree n a -> f (Tree n b)
Tree.traverse1 a -> f b
f Tree n a
t f (NERAVec' ('S n) b b -> NERAVec' n m b)
-> f (NERAVec' ('S n) b b) -> f (NERAVec' n m b)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Apply f => f (a -> b) -> f a -> f b
<.> (a -> f b) -> NERAVec' ('S n) b a -> f (NERAVec' ('S n) b b)
forall (f :: * -> *) a b (n :: Nat) (m :: BinP).
Apply f =>
(a -> f b) -> NERAVec' n m a -> f (NERAVec' n m b)
traverse1' a -> f b
f NERAVec' ('S n) b a
r

itraverse1 :: Apply f => (PosP m -> a -> f b) -> NERAVec m a -> f (NERAVec m b)
itraverse1 :: forall (f :: * -> *) (m :: BinP) a b.
Apply f =>
(PosP m -> a -> f b) -> NERAVec m a -> f (NERAVec m b)
itraverse1 PosP m -> a -> f b
f (NE NERAVec' 'Z m a
xs) = (NERAVec' 'Z m b -> NERAVec m b)
-> f (NERAVec' 'Z m b) -> f (NERAVec m b)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NERAVec' 'Z m b -> NERAVec m b
forall (b :: BinP) a. NERAVec' 'Z b a -> NERAVec b a
NE ((PosP' 'Z m -> a -> f b) -> NERAVec' 'Z m a -> f (NERAVec' 'Z m b)
forall (f :: * -> *) (n :: Nat) (m :: BinP) a b.
Apply f =>
(PosP' n m -> a -> f b) -> NERAVec' n m a -> f (NERAVec' n m b)
itraverse1' (PosP m -> a -> f b
f (PosP m -> a -> f b)
-> (PosP' 'Z m -> PosP m) -> PosP' 'Z m -> a -> f b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PosP' 'Z m -> PosP m
forall (b :: BinP). PosP' 'Z b -> PosP b
PosP) NERAVec' 'Z m a
xs)

itraverse1' :: Apply f => (PosP' n m -> a -> f b) -> NERAVec' n m a -> f (NERAVec' n m b)
itraverse1' :: forall (f :: * -> *) (n :: Nat) (m :: BinP) a b.
Apply f =>
(PosP' n m -> a -> f b) -> NERAVec' n m a -> f (NERAVec' n m b)
itraverse1' PosP' n m -> a -> f b
f (Last  Tree n a
t)   = Tree n b -> NERAVec' n m b
Tree n b -> NERAVec' n 'BE b
forall (n :: Nat) a. Tree n a -> NERAVec' n 'BE a
Last (Tree n b -> NERAVec' n m b) -> f (Tree n b) -> f (NERAVec' n m b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Wrd n -> a -> f b) -> Tree n a -> f (Tree n b)
forall (f :: * -> *) (n :: Nat) a b.
Apply f =>
(Wrd n -> a -> f b) -> Tree n a -> f (Tree n b)
Tree.itraverse1 (PosP' n m -> a -> f b
f (PosP' n m -> a -> f b)
-> (Wrd n -> PosP' n m) -> Wrd n -> a -> f b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrd n -> PosP' n m
Wrd n -> PosP' n 'BE
forall (n :: Nat). Wrd n -> PosP' n 'BE
AtEnd) Tree n a
t
itraverse1' PosP' n m -> a -> f b
f (Cons0   NERAVec' ('S n) b a
r) = NERAVec' ('S n) b b -> NERAVec' n m b
NERAVec' ('S n) b b -> NERAVec' n ('B0 b) b
forall (n :: Nat) (b :: BinP) a.
NERAVec' ('S n) b a -> NERAVec' n ('B0 b) a
Cons0 (NERAVec' ('S n) b b -> NERAVec' n m b)
-> f (NERAVec' ('S n) b b) -> f (NERAVec' n m b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (PosP' ('S n) b -> a -> f b)
-> NERAVec' ('S n) b a -> f (NERAVec' ('S n) b b)
forall (f :: * -> *) (n :: Nat) (m :: BinP) a b.
Apply f =>
(PosP' n m -> a -> f b) -> NERAVec' n m a -> f (NERAVec' n m b)
itraverse1' (PosP' n m -> a -> f b
f (PosP' n m -> a -> f b)
-> (PosP' ('S n) b -> PosP' n m) -> PosP' ('S n) b -> a -> f b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PosP' ('S n) b -> PosP' n m
PosP' ('S n) b -> PosP' n ('B0 b)
forall (n :: Nat) (b1 :: BinP). PosP' ('S n) b1 -> PosP' n ('B0 b1)
There0) NERAVec' ('S n) b a
r
itraverse1' PosP' n m -> a -> f b
f (Cons1 Tree n a
t NERAVec' ('S n) b a
r) = Tree n b -> NERAVec' ('S n) b b -> NERAVec' n m b
Tree n b -> NERAVec' ('S n) b b -> NERAVec' n ('B1 b) b
forall (n :: Nat) a (b :: BinP).
Tree n a -> NERAVec' ('S n) b a -> NERAVec' n ('B1 b) a
Cons1 (Tree n b -> NERAVec' ('S n) b b -> NERAVec' n m b)
-> f (Tree n b) -> f (NERAVec' ('S n) b b -> NERAVec' n m b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Wrd n -> a -> f b) -> Tree n a -> f (Tree n b)
forall (f :: * -> *) (n :: Nat) a b.
Apply f =>
(Wrd n -> a -> f b) -> Tree n a -> f (Tree n b)
Tree.itraverse1 (PosP' n m -> a -> f b
f (PosP' n m -> a -> f b)
-> (Wrd n -> PosP' n m) -> Wrd n -> a -> f b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrd n -> PosP' n m
Wrd n -> PosP' n ('B1 b)
forall (n :: Nat) (b1 :: BinP). Wrd n -> PosP' n ('B1 b1)
Here) Tree n a
t f (NERAVec' ('S n) b b -> NERAVec' n m b)
-> f (NERAVec' ('S n) b b) -> f (NERAVec' n m b)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Apply f => f (a -> b) -> f a -> f b
<.> (PosP' ('S n) b -> a -> f b)
-> NERAVec' ('S n) b a -> f (NERAVec' ('S n) b b)
forall (f :: * -> *) (n :: Nat) (m :: BinP) a b.
Apply f =>
(PosP' n m -> a -> f b) -> NERAVec' n m a -> f (NERAVec' n m b)
itraverse1' (PosP' n m -> a -> f b
f (PosP' n m -> a -> f b)
-> (PosP' ('S n) b -> PosP' n m) -> PosP' ('S n) b -> a -> f b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PosP' ('S n) b -> PosP' n m
PosP' ('S n) b -> PosP' n ('B1 b)
forall (n :: Nat) (b1 :: BinP). PosP' ('S n) b1 -> PosP' n ('B1 b1)
There1) NERAVec' ('S n) b a
r
#endif

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

zipWith :: (a -> b -> c) -> NERAVec m a -> NERAVec m b -> NERAVec m c
zipWith :: forall a b c (m :: BinP).
(a -> b -> c) -> NERAVec m a -> NERAVec m b -> NERAVec m c
zipWith a -> b -> c
f (NE NERAVec' 'Z m a
xs) (NE NERAVec' 'Z m b
ys) = NERAVec' 'Z m c -> NERAVec m c
forall (b :: BinP) a. NERAVec' 'Z b a -> NERAVec b a
NE ((a -> b -> c)
-> NERAVec' 'Z m a -> NERAVec' 'Z m b -> NERAVec' 'Z m c
forall a b c (n :: Nat) (m :: BinP).
(a -> b -> c) -> NERAVec' n m a -> NERAVec' n m b -> NERAVec' n m c
zipWith' a -> b -> c
f NERAVec' 'Z m a
xs NERAVec' 'Z m b
ys)

-- | Zip two 'NERAVec''s with a function.
zipWith' :: (a -> b -> c) -> NERAVec' n m a -> NERAVec' n m b -> NERAVec' n m c
zipWith' :: forall a b c (n :: Nat) (m :: BinP).
(a -> b -> c) -> NERAVec' n m a -> NERAVec' n m b -> NERAVec' n m c
zipWith' a -> b -> c
f (Last  Tree n a
t)   (Last  Tree n b
t')    = Tree n c -> NERAVec' n 'BE c
forall (n :: Nat) a. Tree n a -> NERAVec' n 'BE a
Last ((a -> b -> c) -> Tree n a -> Tree n b -> Tree n c
forall a b c (n :: Nat).
(a -> b -> c) -> Tree n a -> Tree n b -> Tree n c
Tree.zipWith a -> b -> c
f Tree n a
t Tree n b
t')
zipWith' a -> b -> c
f (Cons0   NERAVec' ('S n) b a
r) (Cons0    NERAVec' ('S n) b b
r') = NERAVec' ('S n) b c -> NERAVec' n ('B0 b) c
forall (n :: Nat) (b :: BinP) a.
NERAVec' ('S n) b a -> NERAVec' n ('B0 b) a
Cons0 ((a -> b -> c)
-> NERAVec' ('S n) b a
-> NERAVec' ('S n) b b
-> NERAVec' ('S n) b c
forall a b c (n :: Nat) (m :: BinP).
(a -> b -> c) -> NERAVec' n m a -> NERAVec' n m b -> NERAVec' n m c
zipWith' a -> b -> c
f NERAVec' ('S n) b a
r NERAVec' ('S n) b b
NERAVec' ('S n) b b
r')
zipWith' a -> b -> c
f (Cons1 Tree n a
t NERAVec' ('S n) b a
r) (Cons1 Tree n b
t' NERAVec' ('S n) b b
r') = Tree n c -> NERAVec' ('S n) b c -> NERAVec' n ('B1 b) c
forall (n :: Nat) a (b :: BinP).
Tree n a -> NERAVec' ('S n) b a -> NERAVec' n ('B1 b) a
Cons1 ((a -> b -> c) -> Tree n a -> Tree n b -> Tree n c
forall a b c (n :: Nat).
(a -> b -> c) -> Tree n a -> Tree n b -> Tree n c
Tree.zipWith a -> b -> c
f Tree n a
t Tree n b
t') ((a -> b -> c)
-> NERAVec' ('S n) b a
-> NERAVec' ('S n) b b
-> NERAVec' ('S n) b c
forall a b c (n :: Nat) (m :: BinP).
(a -> b -> c) -> NERAVec' n m a -> NERAVec' n m b -> NERAVec' n m c
zipWith' a -> b -> c
f NERAVec' ('S n) b a
r NERAVec' ('S n) b b
NERAVec' ('S n) b b
r')

izipWith :: (PosP m -> a -> b -> c) -> NERAVec m a -> NERAVec m b -> NERAVec m c
izipWith :: forall (m :: BinP) a b c.
(PosP m -> a -> b -> c)
-> NERAVec m a -> NERAVec m b -> NERAVec m c
izipWith PosP m -> a -> b -> c
f (NE NERAVec' 'Z m a
xs) (NE NERAVec' 'Z m b
ys) = NERAVec' 'Z m c -> NERAVec m c
forall (b :: BinP) a. NERAVec' 'Z b a -> NERAVec b a
NE ((PosP' 'Z m -> a -> b -> c)
-> NERAVec' 'Z m a -> NERAVec' 'Z m b -> NERAVec' 'Z m c
forall (n :: Nat) (m :: BinP) a b c.
(PosP' n m -> a -> b -> c)
-> NERAVec' n m a -> NERAVec' n m b -> NERAVec' n m c
izipWith' (PosP m -> a -> b -> c
f (PosP m -> a -> b -> c)
-> (PosP' 'Z m -> PosP m) -> PosP' 'Z m -> a -> b -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PosP' 'Z m -> PosP m
forall (b :: BinP). PosP' 'Z b -> PosP b
PosP) NERAVec' 'Z m a
xs NERAVec' 'Z m b
ys)

-- | Zip two 'NERAVec''s with a function which also takes 'PosP'' index.
izipWith' :: (PosP' n m -> a -> b -> c) -> NERAVec' n m a -> NERAVec' n m b -> NERAVec' n m c
izipWith' :: forall (n :: Nat) (m :: BinP) a b c.
(PosP' n m -> a -> b -> c)
-> NERAVec' n m a -> NERAVec' n m b -> NERAVec' n m c
izipWith' PosP' n m -> a -> b -> c
f (Last  Tree n a
t)   (Last  Tree n b
t')    = Tree n c -> NERAVec' n 'BE c
forall (n :: Nat) a. Tree n a -> NERAVec' n 'BE a
Last ((Wrd n -> a -> b -> c) -> Tree n a -> Tree n b -> Tree n c
forall (n :: Nat) a b c.
(Wrd n -> a -> b -> c) -> Tree n a -> Tree n b -> Tree n c
Tree.izipWith (PosP' n m -> a -> b -> c
f (PosP' n m -> a -> b -> c)
-> (Wrd n -> PosP' n m) -> Wrd n -> a -> b -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrd n -> PosP' n m
Wrd n -> PosP' n 'BE
forall (n :: Nat). Wrd n -> PosP' n 'BE
AtEnd) Tree n a
t Tree n b
t')
izipWith' PosP' n m -> a -> b -> c
f (Cons0   NERAVec' ('S n) b a
r) (Cons0    NERAVec' ('S n) b b
r') = NERAVec' ('S n) b c -> NERAVec' n ('B0 b) c
forall (n :: Nat) (b :: BinP) a.
NERAVec' ('S n) b a -> NERAVec' n ('B0 b) a
Cons0 ((PosP' ('S n) b -> a -> b -> c)
-> NERAVec' ('S n) b a
-> NERAVec' ('S n) b b
-> NERAVec' ('S n) b c
forall (n :: Nat) (m :: BinP) a b c.
(PosP' n m -> a -> b -> c)
-> NERAVec' n m a -> NERAVec' n m b -> NERAVec' n m c
izipWith' (PosP' n m -> a -> b -> c
f (PosP' n m -> a -> b -> c)
-> (PosP' ('S n) b -> PosP' n m) -> PosP' ('S n) b -> a -> b -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PosP' ('S n) b -> PosP' n m
PosP' ('S n) b -> PosP' n ('B0 b)
forall (n :: Nat) (b1 :: BinP). PosP' ('S n) b1 -> PosP' n ('B0 b1)
There0) NERAVec' ('S n) b a
r NERAVec' ('S n) b b
NERAVec' ('S n) b b
r')
izipWith' PosP' n m -> a -> b -> c
f (Cons1 Tree n a
t NERAVec' ('S n) b a
r) (Cons1 Tree n b
t' NERAVec' ('S n) b b
r') = Tree n c -> NERAVec' ('S n) b c -> NERAVec' n ('B1 b) c
forall (n :: Nat) a (b :: BinP).
Tree n a -> NERAVec' ('S n) b a -> NERAVec' n ('B1 b) a
Cons1 ((Wrd n -> a -> b -> c) -> Tree n a -> Tree n b -> Tree n c
forall (n :: Nat) a b c.
(Wrd n -> a -> b -> c) -> Tree n a -> Tree n b -> Tree n c
Tree.izipWith (PosP' n m -> a -> b -> c
f (PosP' n m -> a -> b -> c)
-> (Wrd n -> PosP' n m) -> Wrd n -> a -> b -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrd n -> PosP' n m
Wrd n -> PosP' n ('B1 b)
forall (n :: Nat) (b1 :: BinP). Wrd n -> PosP' n ('B1 b1)
Here) Tree n a
t Tree n b
t') ((PosP' ('S n) b -> a -> b -> c)
-> NERAVec' ('S n) b a
-> NERAVec' ('S n) b b
-> NERAVec' ('S n) b c
forall (n :: Nat) (m :: BinP) a b c.
(PosP' n m -> a -> b -> c)
-> NERAVec' n m a -> NERAVec' n m b -> NERAVec' n m c
izipWith' (PosP' n m -> a -> b -> c
f (PosP' n m -> a -> b -> c)
-> (PosP' ('S n) b -> PosP' n m) -> PosP' ('S n) b -> a -> b -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PosP' ('S n) b -> PosP' n m
PosP' ('S n) b -> PosP' n ('B1 b)
forall (n :: Nat) (b1 :: BinP). PosP' ('S n) b1 -> PosP' n ('B1 b1)
There1) NERAVec' ('S n) b a
r NERAVec' ('S n) b b
NERAVec' ('S n) b b
r')

repeat :: SBinPI b => a -> NERAVec b a
repeat :: forall (b :: BinP) a. SBinPI b => a -> NERAVec b a
repeat = NERAVec' 'Z b a -> NERAVec b a
forall (b :: BinP) a. NERAVec' 'Z b a -> NERAVec b a
NE (NERAVec' 'Z b a -> NERAVec b a)
-> (a -> NERAVec' 'Z b a) -> a -> NERAVec b a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> NERAVec' 'Z b a
forall (b :: BinP) (n :: Nat) a.
(SNatI n, SBinPI b) =>
a -> NERAVec' n b a
repeat'

repeat' :: forall b n a. (N.SNatI n, SBinPI b) => a -> NERAVec' n b a
repeat' :: forall (b :: BinP) (n :: Nat) a.
(SNatI n, SBinPI b) =>
a -> NERAVec' n b a
repeat' a
x = case SBinP b
forall (b :: BinP). SBinPI b => SBinP b
sbinp :: SBinP b of
    SBinP b
SBE -> Tree n a -> NERAVec' n 'BE a
forall (n :: Nat) a. Tree n a -> NERAVec' n 'BE a
Last (a -> Tree n a
forall (n :: Nat) a. SNatI n => a -> Tree n a
Tree.repeat a
x)
    SBinP b
SB0 -> NERAVec' ('S n) b1 a -> NERAVec' n ('B0 b1) a
forall (n :: Nat) (b :: BinP) a.
NERAVec' ('S n) b a -> NERAVec' n ('B0 b) a
Cons0 (a -> NERAVec' ('S n) b1 a
forall (b :: BinP) (n :: Nat) a.
(SNatI n, SBinPI b) =>
a -> NERAVec' n b a
repeat' a
x)
    SBinP b
SB1 -> Tree n a -> NERAVec' ('S n) b1 a -> NERAVec' n ('B1 b1) a
forall (n :: Nat) a (b :: BinP).
Tree n a -> NERAVec' ('S n) b a -> NERAVec' n ('B1 b) a
Cons1 (a -> Tree n a
forall (n :: Nat) a. SNatI n => a -> Tree n a
Tree.repeat a
x) (a -> NERAVec' ('S n) b1 a
forall (b :: BinP) (n :: Nat) a.
(SNatI n, SBinPI b) =>
a -> NERAVec' n b a
repeat' a
x)

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

universe :: forall b. SBinPI b => NERAVec b (PosP b)
universe :: forall (b :: BinP). SBinPI b => NERAVec b (PosP b)
universe = NERAVec' 'Z b (PosP' 'Z b) -> NERAVec b (PosP b)
forall a b. Coercible @(*) a b => a -> b
coerce (NERAVec' 'Z b (PosP' 'Z b)
forall (n :: Nat) (b :: BinP).
(SNatI n, SBinPI b) =>
NERAVec' n b (PosP' n b)
universe' :: NERAVec' 'Z b (PosP' 'Z b))

universe' :: forall n b. (N.SNatI n, SBinPI b) => NERAVec' n b (PosP' n b)
universe' :: forall (n :: Nat) (b :: BinP).
(SNatI n, SBinPI b) =>
NERAVec' n b (PosP' n b)
universe' = case SBinP b
forall (b :: BinP). SBinPI b => SBinP b
sbinp :: SBinP b of
    SBinP b
SBE -> Tree n (PosP' n b) -> NERAVec' n 'BE (PosP' n b)
forall (n :: Nat) a. Tree n a -> NERAVec' n 'BE a
Last  ((Wrd n -> PosP' n b) -> Tree n (Wrd n) -> Tree n (PosP' n b)
forall a b. (a -> b) -> Tree n a -> Tree n b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Wrd n -> PosP' n b
Wrd n -> PosP' n 'BE
forall (n :: Nat). Wrd n -> PosP' n 'BE
AtEnd Tree n (Wrd n)
forall (n :: Nat). SNatI n => Tree n (Wrd n)
Tree.universe)
    SBinP b
SB0 -> NERAVec' ('S n) b1 (PosP' n b) -> NERAVec' n ('B0 b1) (PosP' n b)
forall (n :: Nat) (b :: BinP) a.
NERAVec' ('S n) b a -> NERAVec' n ('B0 b) a
Cons0 ((PosP' ('S n) b1 -> PosP' n b)
-> NERAVec' ('S n) b1 (PosP' ('S n) b1)
-> NERAVec' ('S n) b1 (PosP' n b)
forall a b.
(a -> b) -> NERAVec' ('S n) b1 a -> NERAVec' ('S n) b1 b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PosP' ('S n) b1 -> PosP' n b
PosP' ('S n) b1 -> PosP' n ('B0 b1)
forall (n :: Nat) (b1 :: BinP). PosP' ('S n) b1 -> PosP' n ('B0 b1)
There0 NERAVec' ('S n) b1 (PosP' ('S n) b1)
forall (n :: Nat) (b :: BinP).
(SNatI n, SBinPI b) =>
NERAVec' n b (PosP' n b)
universe')
    SBinP b
SB1 -> Tree n (PosP' n b)
-> NERAVec' ('S n) b1 (PosP' n b)
-> NERAVec' n ('B1 b1) (PosP' n b)
forall (n :: Nat) a (b :: BinP).
Tree n a -> NERAVec' ('S n) b a -> NERAVec' n ('B1 b) a
Cons1 ((Wrd n -> PosP' n b) -> Tree n (Wrd n) -> Tree n (PosP' n b)
forall a b. (a -> b) -> Tree n a -> Tree n b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Wrd n -> PosP' n b
Wrd n -> PosP' n ('B1 b1)
forall (n :: Nat) (b1 :: BinP). Wrd n -> PosP' n ('B1 b1)
Here Tree n (Wrd n)
forall (n :: Nat). SNatI n => Tree n (Wrd n)
Tree.universe) ((PosP' ('S n) b1 -> PosP' n b)
-> NERAVec' ('S n) b1 (PosP' ('S n) b1)
-> NERAVec' ('S n) b1 (PosP' n b)
forall a b.
(a -> b) -> NERAVec' ('S n) b1 a -> NERAVec' ('S n) b1 b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PosP' ('S n) b1 -> PosP' n b
PosP' ('S n) b1 -> PosP' n ('B1 b1)
forall (n :: Nat) (b1 :: BinP). PosP' ('S n) b1 -> PosP' n ('B1 b1)
There1 NERAVec' ('S n) b1 (PosP' ('S n) b1)
forall (n :: Nat) (b :: BinP).
(SNatI n, SBinPI b) =>
NERAVec' n b (PosP' n b)
universe')

-------------------------------------------------------------------------------
-- Out-of-order combining
-------------------------------------------------------------------------------

{-
appendB0 :: NERAVec b a -> NERAVec b a -> NERAVec ('B0 b) a
appendB0 (NE xs) (NE ys) = NE (Cons0 (appendB' xs ys)) where

appendB1 :: a -> NERAVec b a -> NERAVec b a -> NERAVec ('B1 b) a
appendB1 x (NE ys) (NE zs) = NE (Cons1 (Tree.Leaf x) (appendB' ys zs))

appendB' :: NERAVec' n b a -> NERAVec' n b a -> NERAVec' ('S n) b a
appendB' (Last  t)   (Last  t')    = Last (Tree.Node t t')
appendB' (Cons0   r) (Cons0    r') = Cons0 (appendB' r r')
appendB' (Cons1 t r) (Cons1 t' r') = Cons1 (Tree.Node t t') (appendB' r r')

splitB0 :: NERAVec ('B0 b) a -> (NERAVec b a, NERAVec b a)
splitB0 (NE (Cons0 xs)) =
    let (ys, zs) = splitB' xs in (NE ys, NE zs)

splitB1 :: NERAVec ('B1 b) a -> (a, NERAVec b a, NERAVec b a)
splitB1 (NE (Cons1 (Tree.Leaf x) xs)) =
    let (ys, zs) = splitB' xs in (x, NE ys, NE zs)

splitB' :: NERAVec' ('S n) b a -> (NERAVec' n b a, NERAVec' n b a)
splitB' (Last (Tree.Node t t'))    = (Last t, Last t')
splitB' (Cons0                  r) =
    let (a, b) = splitB' r in (Cons0 a, Cons0 b)
splitB' (Cons1 (Tree.Node t t') r) =
    let (a, b) = splitB' r in (Cons1 t a, Cons1 t' b)
-}

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

instance BP.SBinPI b => QC.Arbitrary1 (NERAVec b) where
    liftArbitrary :: forall a. Gen a -> Gen (NERAVec b a)
liftArbitrary = Gen a -> Gen (NERAVec b a)
forall (b :: BinP) a. SBinPI b => Gen a -> Gen (NERAVec b a)
liftArbitrary
    liftShrink :: forall a. (a -> [a]) -> NERAVec b a -> [NERAVec b a]
liftShrink    = (a -> [a]) -> NERAVec b a -> [NERAVec b a]
forall a (b :: BinP). (a -> [a]) -> NERAVec b a -> [NERAVec b a]
liftShrink

liftArbitrary :: BP.SBinPI b => QC.Gen a -> QC.Gen (NERAVec b a)
liftArbitrary :: forall (b :: BinP) a. SBinPI b => Gen a -> Gen (NERAVec b a)
liftArbitrary = (NERAVec' 'Z b a -> NERAVec b a)
-> Gen (NERAVec' 'Z b a) -> Gen (NERAVec b a)
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NERAVec' 'Z b a -> NERAVec b a
forall (b :: BinP) a. NERAVec' 'Z b a -> NERAVec b a
NE (Gen (NERAVec' 'Z b a) -> Gen (NERAVec b a))
-> (Gen a -> Gen (NERAVec' 'Z b a)) -> Gen a -> Gen (NERAVec b a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Gen a -> Gen (NERAVec' 'Z b a)
forall (b :: BinP) (n :: Nat) a.
(SBinPI b, SNatI n) =>
Gen a -> Gen (NERAVec' n b a)
liftArbitrary'

liftShrink :: (a -> [a]) -> NERAVec b a -> [NERAVec b a]
liftShrink :: forall a (b :: BinP). (a -> [a]) -> NERAVec b a -> [NERAVec b a]
liftShrink a -> [a]
shr (NE NERAVec' 'Z b a
r) = (NERAVec' 'Z b a -> NERAVec b a)
-> [NERAVec' 'Z b a] -> [NERAVec b a]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NERAVec' 'Z b a -> NERAVec b a
forall (b :: BinP) a. NERAVec' 'Z b a -> NERAVec b a
NE ((a -> [a]) -> NERAVec' 'Z b a -> [NERAVec' 'Z b a]
forall (b :: BinP) (n :: Nat) a.
(a -> [a]) -> NERAVec' n b a -> [NERAVec' n b a]
liftShrink' a -> [a]
shr NERAVec' 'Z b a
r)

instance (BP.SBinPI b, N.SNatI n) => QC.Arbitrary1 (NERAVec' n b) where
    liftArbitrary :: forall a. Gen a -> Gen (NERAVec' n b a)
liftArbitrary = Gen a -> Gen (NERAVec' n b a)
forall (b :: BinP) (n :: Nat) a.
(SBinPI b, SNatI n) =>
Gen a -> Gen (NERAVec' n b a)
liftArbitrary'
    liftShrink :: forall a. (a -> [a]) -> NERAVec' n b a -> [NERAVec' n b a]
liftShrink    = (a -> [a]) -> NERAVec' n b a -> [NERAVec' n b a]
forall (b :: BinP) (n :: Nat) a.
(a -> [a]) -> NERAVec' n b a -> [NERAVec' n b a]
liftShrink'

liftArbitrary' :: forall b n a. (BP.SBinPI b, N.SNatI n) => QC.Gen a -> QC.Gen (NERAVec' n b a)
liftArbitrary' :: forall (b :: BinP) (n :: Nat) a.
(SBinPI b, SNatI n) =>
Gen a -> Gen (NERAVec' n b a)
liftArbitrary' Gen a
arb = case SBinP b
forall (b :: BinP). SBinPI b => SBinP b
BP.sbinp :: BP.SBinP b of
    SBinP b
BP.SBE -> Tree n a -> NERAVec' n b a
Tree n a -> NERAVec' n 'BE a
forall (n :: Nat) a. Tree n a -> NERAVec' n 'BE a
Last  (Tree n a -> NERAVec' n b a)
-> Gen (Tree n a) -> Gen (NERAVec' n b a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen a -> Gen (Tree n a)
forall a. Gen a -> Gen (Tree n a)
forall (f :: * -> *) a. Arbitrary1 f => Gen a -> Gen (f a)
QC.liftArbitrary Gen a
arb
    SBinP b
BP.SB0 -> NERAVec' ('S n) b1 a -> NERAVec' n b a
NERAVec' ('S n) b1 a -> NERAVec' n ('B0 b1) a
forall (n :: Nat) (b :: BinP) a.
NERAVec' ('S n) b a -> NERAVec' n ('B0 b) a
Cons0 (NERAVec' ('S n) b1 a -> NERAVec' n b a)
-> Gen (NERAVec' ('S n) b1 a) -> Gen (NERAVec' n b a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen a -> Gen (NERAVec' ('S n) b1 a)
forall (b :: BinP) (n :: Nat) a.
(SBinPI b, SNatI n) =>
Gen a -> Gen (NERAVec' n b a)
liftArbitrary' Gen a
arb
    SBinP b
BP.SB1 -> Tree n a -> NERAVec' ('S n) b1 a -> NERAVec' n b a
Tree n a -> NERAVec' ('S n) b1 a -> NERAVec' n ('B1 b1) a
forall (n :: Nat) a (b :: BinP).
Tree n a -> NERAVec' ('S n) b a -> NERAVec' n ('B1 b) a
Cons1 (Tree n a -> NERAVec' ('S n) b1 a -> NERAVec' n b a)
-> Gen (Tree n a) -> Gen (NERAVec' ('S n) b1 a -> NERAVec' n b a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen a -> Gen (Tree n a)
forall a. Gen a -> Gen (Tree n a)
forall (f :: * -> *) a. Arbitrary1 f => Gen a -> Gen (f a)
QC.liftArbitrary Gen a
arb Gen (NERAVec' ('S n) b1 a -> NERAVec' n b a)
-> Gen (NERAVec' ('S n) b1 a) -> Gen (NERAVec' n b a)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen a -> Gen (NERAVec' ('S n) b1 a)
forall (b :: BinP) (n :: Nat) a.
(SBinPI b, SNatI n) =>
Gen a -> Gen (NERAVec' n b a)
liftArbitrary' Gen a
arb

liftShrink' :: forall b n a. (a -> [a]) -> NERAVec' n b a -> [NERAVec' n b a]
liftShrink' :: forall (b :: BinP) (n :: Nat) a.
(a -> [a]) -> NERAVec' n b a -> [NERAVec' n b a]
liftShrink' a -> [a]
shr (Last  Tree n a
t)   = Tree n a -> NERAVec' n b a
Tree n a -> NERAVec' n 'BE a
forall (n :: Nat) a. Tree n a -> NERAVec' n 'BE a
Last (Tree n a -> NERAVec' n b a) -> [Tree n a] -> [NERAVec' n b a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> [a]) -> Tree n a -> [Tree n a]
forall (n :: Nat) a. (a -> [a]) -> Tree n a -> [Tree n a]
Tree.liftShrink a -> [a]
shr Tree n a
t
liftShrink' a -> [a]
shr (Cons0   NERAVec' ('S n) b a
r) = NERAVec' ('S n) b a -> NERAVec' n b a
NERAVec' ('S n) b a -> NERAVec' n ('B0 b) a
forall (n :: Nat) (b :: BinP) a.
NERAVec' ('S n) b a -> NERAVec' n ('B0 b) a
Cons0 (NERAVec' ('S n) b a -> NERAVec' n b a)
-> [NERAVec' ('S n) b a] -> [NERAVec' n b a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> [a]) -> NERAVec' ('S n) b a -> [NERAVec' ('S n) b a]
forall (b :: BinP) (n :: Nat) a.
(a -> [a]) -> NERAVec' n b a -> [NERAVec' n b a]
liftShrink' a -> [a]
shr NERAVec' ('S n) b a
r
liftShrink' a -> [a]
shr (Cons1 Tree n a
t NERAVec' ('S n) b a
r) = (Tree n a -> NERAVec' ('S n) b a -> NERAVec' n b a)
-> (Tree n a, NERAVec' ('S n) b a) -> NERAVec' n b a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Tree n a -> NERAVec' ('S n) b a -> NERAVec' n b a
Tree n a -> NERAVec' ('S n) b a -> NERAVec' n ('B1 b) a
forall (n :: Nat) a (b :: BinP).
Tree n a -> NERAVec' ('S n) b a -> NERAVec' n ('B1 b) a
Cons1 ((Tree n a, NERAVec' ('S n) b a) -> NERAVec' n b a)
-> [(Tree n a, NERAVec' ('S n) b a)] -> [NERAVec' n b a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Tree n a -> [Tree n a])
-> (NERAVec' ('S n) b a -> [NERAVec' ('S n) b a])
-> (Tree n a, NERAVec' ('S n) b a)
-> [(Tree n a, NERAVec' ('S n) b 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 ((a -> [a]) -> Tree n a -> [Tree n a]
forall (n :: Nat) a. (a -> [a]) -> Tree n a -> [Tree n a]
Tree.liftShrink a -> [a]
shr) ((a -> [a]) -> NERAVec' ('S n) b a -> [NERAVec' ('S n) b a]
forall (b :: BinP) (n :: Nat) a.
(a -> [a]) -> NERAVec' n b a -> [NERAVec' n b a]
liftShrink' a -> [a]
shr) (Tree n a
t, NERAVec' ('S n) b a
r)

instance (BP.SBinPI b, QC.Arbitrary a) => QC.Arbitrary (NERAVec b a) where
    arbitrary :: Gen (NERAVec b a)
arbitrary = Gen (NERAVec b a)
forall (f :: * -> *) a. (Arbitrary1 f, Arbitrary a) => Gen (f a)
QC.arbitrary1
    shrink :: NERAVec b a -> [NERAVec b a]
shrink    = NERAVec b a -> [NERAVec b a]
forall (f :: * -> *) a. (Arbitrary1 f, Arbitrary a) => f a -> [f a]
QC.shrink1

instance QC.CoArbitrary a => QC.CoArbitrary (NERAVec b a) where
    coarbitrary :: forall b. NERAVec b a -> Gen b -> Gen b
coarbitrary (NE NERAVec' 'Z b a
r) = NERAVec' 'Z b a -> Gen b -> Gen b
forall a b. CoArbitrary a => a -> Gen b -> Gen b
forall b. NERAVec' 'Z b a -> Gen b -> Gen b
QC.coarbitrary NERAVec' 'Z b a
r

instance QC.CoArbitrary a => QC.CoArbitrary (NERAVec' n b a) where
    coarbitrary :: forall b. NERAVec' n b a -> Gen b -> Gen b
coarbitrary (Last  Tree n a
t)   = 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
. Tree n a -> Gen b -> Gen b
forall a b. CoArbitrary a => a -> Gen b -> Gen b
forall b. Tree n a -> Gen b -> Gen b
QC.coarbitrary Tree n a
t
    coarbitrary (Cons0   NERAVec' ('S n) b a
r) = Int -> Gen b -> Gen b
forall n a. Integral n => n -> Gen a -> Gen a
QC.variant (Int
1 :: Int) (Gen b -> Gen b) -> (Gen b -> Gen b) -> Gen b -> Gen b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NERAVec' ('S n) b a -> Gen b -> Gen b
forall a b. CoArbitrary a => a -> Gen b -> Gen b
forall b. NERAVec' ('S n) b a -> Gen b -> Gen b
QC.coarbitrary NERAVec' ('S n) b a
r
    coarbitrary (Cons1 Tree n a
t NERAVec' ('S n) b a
r) = Int -> Gen b -> Gen b
forall n a. Integral n => n -> Gen a -> Gen a
QC.variant (Int
2 :: Int) (Gen b -> Gen b) -> (Gen b -> Gen b) -> Gen b -> Gen b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Tree n a, NERAVec' ('S n) b a) -> Gen b -> Gen b
forall b. (Tree n a, NERAVec' ('S n) b a) -> Gen b -> Gen b
forall a b. CoArbitrary a => a -> Gen b -> Gen b
QC.coarbitrary (Tree n a
t, NERAVec' ('S n) b a
r)

instance (BP.SBinPI b, QC.Function a) => QC.Function (NERAVec b a) where
    function :: forall b. (NERAVec b a -> b) -> NERAVec b a :-> b
function = (NERAVec b a -> NERAVec' 'Z b a)
-> (NERAVec' 'Z b a -> NERAVec b a)
-> (NERAVec b a -> b)
-> NERAVec b a :-> b
forall b a c.
Function b =>
(a -> b) -> (b -> a) -> (a -> c) -> a :-> c
QC.functionMap (\(NE NERAVec' 'Z b a
r) -> NERAVec' 'Z b a
r) NERAVec' 'Z b a -> NERAVec b a
forall (b :: BinP) a. NERAVec' 'Z b a -> NERAVec b a
NE

instance (N.SNatI n, BP.SBinPI b, QC.Function a) => QC.Function (NERAVec' n b a) where
    function :: forall b. (NERAVec' n b a -> b) -> NERAVec' n b a :-> b
function = case SBinP b
forall (b :: BinP). SBinPI b => SBinP b
BP.sbinp :: BP.SBinP b of
        SBinP b
SBE -> (NERAVec' n b a -> Tree n a)
-> (Tree n a -> NERAVec' n b a)
-> (NERAVec' n b a -> b)
-> NERAVec' n b a :-> b
forall b a c.
Function b =>
(a -> b) -> (b -> a) -> (a -> c) -> a :-> c
QC.functionMap (\(Last Tree n a
t) -> Tree n a
t)         Tree n a -> NERAVec' n b a
Tree n a -> NERAVec' n 'BE a
forall (n :: Nat) a. Tree n a -> NERAVec' n 'BE a
Last
        SBinP b
SB0 -> (NERAVec' n b a -> NERAVec' ('S n) b1 a)
-> (NERAVec' ('S n) b1 a -> NERAVec' n b a)
-> (NERAVec' n b a -> b)
-> NERAVec' n b a :-> b
forall b a c.
Function b =>
(a -> b) -> (b -> a) -> (a -> c) -> a :-> c
QC.functionMap (\(Cons0 NERAVec' ('S n) b a
r) -> NERAVec' ('S n) b1 a
NERAVec' ('S n) b a
r)        NERAVec' ('S n) b1 a -> NERAVec' n b a
NERAVec' ('S n) b1 a -> NERAVec' n ('B0 b1) a
forall (n :: Nat) (b :: BinP) a.
NERAVec' ('S n) b a -> NERAVec' n ('B0 b) a
Cons0
        SBinP b
SB1 -> (NERAVec' n b a -> (Tree n a, NERAVec' ('S n) b1 a))
-> ((Tree n a, NERAVec' ('S n) b1 a) -> NERAVec' n b a)
-> (NERAVec' n b a -> b)
-> NERAVec' n b a :-> b
forall b a c.
Function b =>
(a -> b) -> (b -> a) -> (a -> c) -> a :-> c
QC.functionMap (\(Cons1 Tree n a
t NERAVec' ('S n) b a
r) -> (Tree n a
t, NERAVec' ('S n) b a
r)) ((Tree n a -> NERAVec' ('S n) b1 a -> NERAVec' n b a)
-> (Tree n a, NERAVec' ('S n) b1 a) -> NERAVec' n b a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Tree n a -> NERAVec' ('S n) b1 a -> NERAVec' n b a
Tree n a -> NERAVec' ('S n) b1 a -> NERAVec' n ('B1 b1) a
forall (n :: Nat) a (b :: BinP).
Tree n a -> NERAVec' ('S n) b a -> NERAVec' n ('B1 b) a
Cons1)