{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE EmptyDataDecls #-}
module Data.FixedLength (
   T, Position, List, Length,
   Index, Zero, Succ(Stop, Succ),
   toList, showsPrec,
   map, zipWith, sequenceA, repeat,
   index, update, indices, indicesInt, numFromIndex, indexFromNum,
   GE1, GE2, GE3, GE4, GE5, GE6, GE7, GE8,
   i0, i1, i2, i3, i4, i5, i6, i7,
   fromFixedList, toFixedList,
   (!:), end, singleton,
   viewL, switchL, head, tail, switchEnd,
   Curried, curry, uncurry,
   ConsAll, NumberOfArguments, ResultSize, ResultElement, consAll,
   minimum, maximum,
   ) where

import qualified Type.Data.Num.Unary as Unary
import Type.Data.Num.Unary.Literal (U1)
import Type.Data.Num.Unary (Positive, Natural, switchNat)

import qualified Foreign.Storable.FixedArray as StoreArray
import qualified Foreign.Storable.Traversable as StoreTrav
import Foreign.Storable (Storable, sizeOf, alignment, poke, peek)

import qualified Data.NonEmpty as NonEmpty
import qualified Data.Empty as Empty

import qualified Control.Applicative as App
import qualified Data.Traversable as Trav
import qualified Data.Foldable as Fold
import qualified Data.Functor.Classes as FunctorC
import qualified Data.List as List
import Control.Applicative (Applicative, liftA2)
import Data.Traversable (Traversable, foldMapDefault)
import Data.Foldable (Foldable, foldMap)
import Data.Functor.Classes (Eq1, eq1, Show1, showsPrec1)
import Data.Maybe (Maybe(Nothing, Just))
import Data.List ((++))
import Data.Word (Word)

import Data.Function (($), (.))
import Data.Bool (Bool(False, True))
import Data.Ord (Ord, Ordering(LT,EQ,GT), compare, (>))
import Data.Eq (Eq, (==))

import Text.Show.HT (concatS)

import qualified Prelude as P
import Prelude (Functor, fmap, Show, ShowS, Int, (+), (-), error)


type family List n :: * -> *
type instance List Unary.Zero = Empty.T
type instance List (Unary.Succ n) = NonEmpty.T (List n)

type family Length (f :: * -> *)
type instance Length Empty.T = Unary.Zero
type instance Length (NonEmpty.T f) = Unary.Succ (Length f)


newtype T n a = Cons (List n a)

fromFixedList :: List n a -> T n a
fromFixedList :: forall n a. List n a -> T n a
fromFixedList = forall n a. List n a -> T n a
Cons

toFixedList :: T n a -> List n a
toFixedList :: forall n a. T n a -> List n a
toFixedList (Cons List n a
xs) = List n a
xs


end :: T Unary.Zero a
end :: forall a. T Zero a
end = forall n a. List n a -> T n a
Cons forall a. T a
Empty.Cons

infixr 5 !:

(!:) :: a -> T n a -> T (Unary.Succ n) a
a
x !: :: forall a n. a -> T n a -> T (Succ n) a
!: Cons List n a
xs = forall n a. List n a -> T n a
Cons forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. a -> f a -> T f a
NonEmpty.Cons a
x List n a
xs

viewL :: T (Unary.Succ n) a -> (a, T n a)
viewL :: forall n a. T (Succ n) a -> (a, T n a)
viewL (Cons (NonEmpty.Cons a
x List n a
xs)) = (a
x, forall n a. List n a -> T n a
Cons List n a
xs)

switchL :: (a -> T n a -> b) -> (T (Unary.Succ n) a -> b)
switchL :: forall a n b. (a -> T n a -> b) -> T (Succ n) a -> b
switchL a -> T n a -> b
f = forall a b c. (a -> b -> c) -> (a, b) -> c
P.uncurry a -> T n a -> b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n a. T (Succ n) a -> (a, T n a)
viewL

switchEnd :: b -> T Unary.Zero a -> b
switchEnd :: forall b a. b -> T Zero a -> b
switchEnd b
x (Cons T a
List Zero a
Empty.Cons) = b
x


newtype WithPos a b n = WithPos {forall a b n. WithPos a b n -> T n a -> b
runWithPos :: T n a -> b}

withPos ::
   (Positive n) =>
   (forall m. Natural m => T (Unary.Succ m) a -> b) -> T n a -> b
withPos :: forall n a b.
Positive n =>
(forall m. Natural m => T (Succ m) a -> b) -> T n a -> b
withPos forall m. Natural m => T (Succ m) a -> b
f = forall a b n. WithPos a b n -> T n a -> b
runWithPos forall a b. (a -> b) -> a -> b
$ forall n (f :: * -> *).
Positive n =>
(forall m. Natural m => f (Succ m)) -> f n
Unary.switchPos (forall a b n. (T n a -> b) -> WithPos a b n
WithPos forall m. Natural m => T (Succ m) a -> b
f)

head :: (Positive n) => T n a -> a
head :: forall n a. Positive n => T n a -> a
head = forall n a b.
Positive n =>
(forall m. Natural m => T (Succ m) a -> b) -> T n a -> b
withPos (forall a b. (a, b) -> a
P.fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n a. T (Succ n) a -> (a, T n a)
viewL)

tail :: T (Unary.Succ n) a -> T n a
tail :: forall n a. T (Succ n) a -> T n a
tail = forall a b. (a, b) -> b
P.snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n a. T (Succ n) a -> (a, T n a)
viewL

singleton :: a -> T U1 a
singleton :: forall a. a -> T U1 a
singleton a
x = a
xforall a n. a -> T n a -> T (Succ n) a
!:forall a. T Zero a
end

minimum :: (Positive n, Ord a) => T n a -> a
minimum :: forall n a. (Positive n, Ord a) => T n a -> a
minimum = forall n a b.
Positive n =>
(forall m. Natural m => T (Succ m) a -> b) -> T n a -> b
withPos (forall a (f :: * -> *). (Ord a, Foldable f) => T f a -> a
NonEmpty.minimum forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a n b. (a -> T n a -> b) -> T (Succ n) a -> b
switchL forall a (f :: * -> *). a -> f a -> T f a
NonEmpty.cons)

maximum :: (Positive n, Ord a) => T n a -> a
maximum :: forall n a. (Positive n, Ord a) => T n a -> a
maximum = forall n a b.
Positive n =>
(forall m. Natural m => T (Succ m) a -> b) -> T n a -> b
withPos (forall a (f :: * -> *). (Ord a, Foldable f) => T f a -> a
NonEmpty.maximum forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a n b. (a -> T n a -> b) -> T (Succ n) a -> b
switchL forall a (f :: * -> *). a -> f a -> T f a
NonEmpty.cons)



instance (Natural n, Eq a) => Eq (T n a) where
   == :: T n a -> T n a -> Bool
(==)  =  forall (f :: * -> *) a. (Eq1 f, Eq a) => f a -> f a -> Bool
eq1

instance (Natural n) => Eq1 (T n) where
   liftEq :: forall a b. (a -> b -> Bool) -> T n a -> T n b -> Bool
liftEq a -> b -> Bool
eq T n a
xs T n b
ys  =  forall (t :: * -> *). Foldable t => t Bool -> Bool
Fold.and forall a b. (a -> b) -> a -> b
$ forall n a b c.
Natural n =>
(a -> b -> c) -> T n a -> T n b -> T n c
zipWith a -> b -> Bool
eq T n a
xs T n b
ys


showsPrec :: (Natural n, Show a) => Int -> T n a -> ShowS
showsPrec :: forall n a. (Natural n, Show a) => Int -> T n a -> ShowS
showsPrec = forall (f :: * -> *) a. (Show1 f, Show a) => Int -> f a -> ShowS
showsPrec1

liftShowsPrec_ :: (Natural n) => (Int -> a -> ShowS) -> Int -> T n a -> ShowS
liftShowsPrec_ :: forall n a.
Natural n =>
(Int -> a -> ShowS) -> Int -> T n a -> ShowS
liftShowsPrec_ Int -> a -> ShowS
showsPrec_ Int
p =
   Bool -> ShowS -> ShowS
P.showParen (Int
pforall a. Ord a => a -> a -> Bool
>Int
5) forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ShowS] -> ShowS
concatS forall b c a. (b -> c) -> (a -> b) -> a -> c
.
   forall a. a -> [a] -> [a]
List.intersperse (String -> ShowS
P.showString String
"!:") forall b c a. (b -> c) -> (a -> b) -> a -> c
.
   (forall a. [a] -> [a] -> [a]
++ [String -> ShowS
P.showString String
"end"]) forall b c a. (b -> c) -> (a -> b) -> a -> c
.
   forall a b. (a -> b) -> [a] -> [b]
List.map (Int -> a -> ShowS
showsPrec_ Int
6) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n a. Natural n => T n a -> [a]
toList

instance (Natural n, Show a) => Show (T n a) where
   showsPrec :: Int -> T n a -> ShowS
showsPrec = forall (f :: * -> *) a. (Show1 f, Show a) => Int -> f a -> ShowS
showsPrec1

instance (Natural n) => Show1 (T n) where
   liftShowsPrec :: forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> T n a -> ShowS
liftShowsPrec Int -> a -> ShowS
showsPrec_ [a] -> ShowS
_showsList = forall n a.
Natural n =>
(Int -> a -> ShowS) -> Int -> T n a -> ShowS
liftShowsPrec_ Int -> a -> ShowS
showsPrec_


toList :: (Natural n) => T n a -> [a]
toList :: forall n a. Natural n => T n a -> [a]
toList = forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList


newtype Map a b n = Map {forall a b n. Map a b n -> T n a -> T n b
runMap :: T n a -> T n b}

map :: Natural n => (a -> b) -> T n a -> T n b
map :: forall n a b. Natural n => (a -> b) -> T n a -> T n b
map a -> b
f =
   forall a b n. Map a b n -> T n a -> T n b
runMap forall a b. (a -> b) -> a -> b
$
   forall n (f :: * -> *).
Natural n =>
f Zero -> (forall m. Natural m => f (Succ m)) -> f n
switchNat
      (forall a b n. (T n a -> T n b) -> Map a b n
Map forall a b. (a -> b) -> a -> b
$ forall b a. b -> T Zero a -> b
switchEnd forall a. T Zero a
end)
      (forall a b n. (T n a -> T n b) -> Map a b n
Map forall a b. (a -> b) -> a -> b
$ forall a n b. (a -> T n a -> b) -> T (Succ n) a -> b
switchL forall a b. (a -> b) -> a -> b
$ \a
x T m a
xs -> a -> b
f a
x forall a n. a -> T n a -> T (Succ n) a
!: forall n a b. Natural n => (a -> b) -> T n a -> T n b
map a -> b
f T m a
xs)


newtype Sequence f a n = Sequence {forall (f :: * -> *) a n. Sequence f a n -> T n (f a) -> f (T n a)
runSequence :: T n (f a) -> f (T n a)}

sequenceA :: (Applicative f, Natural n) => T n (f a) -> f (T n a)
sequenceA :: forall (f :: * -> *) n a.
(Applicative f, Natural n) =>
T n (f a) -> f (T n a)
sequenceA =
   forall (f :: * -> *) a n. Sequence f a n -> T n (f a) -> f (T n a)
runSequence forall a b. (a -> b) -> a -> b
$
   forall n (f :: * -> *).
Natural n =>
f Zero -> (forall m. Natural m => f (Succ m)) -> f n
switchNat
      (forall (f :: * -> *) a n.
(T n (f a) -> f (T n a)) -> Sequence f a n
Sequence forall a b. (a -> b) -> a -> b
$ forall b a. b -> T Zero a -> b
switchEnd forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
App.pure forall a. T Zero a
end)
      (forall (f :: * -> *) a n.
(T n (f a) -> f (T n a)) -> Sequence f a n
Sequence forall a b. (a -> b) -> a -> b
$ forall a n b. (a -> T n a -> b) -> T (Succ n) a -> b
switchL forall a b. (a -> b) -> a -> b
$ \f a
x T m (f a)
xs -> forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 forall a n. a -> T n a -> T (Succ n) a
(!:) f a
x forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) n a.
(Applicative f, Natural n) =>
T n (f a) -> f (T n a)
sequenceA T m (f a)
xs)


newtype Repeat a n = Repeat {forall a n. Repeat a n -> T n a
runRepeat :: T n a}

repeat :: Natural n => a -> T n a
repeat :: forall n a. Natural n => a -> T n a
repeat a
a =
   forall a n. Repeat a n -> T n a
runRepeat forall a b. (a -> b) -> a -> b
$
   forall n (f :: * -> *).
Natural n =>
f Zero -> (forall m. Natural m => f (Succ m)) -> f n
switchNat
      (forall a n. T n a -> Repeat a n
Repeat forall a. T Zero a
end)
      (forall a n. T n a -> Repeat a n
Repeat forall a b. (a -> b) -> a -> b
$ a
a forall a n. a -> T n a -> T (Succ n) a
!: forall n a. Natural n => a -> T n a
repeat a
a)


newtype Zip a b c n = Zip {forall a b c n. Zip a b c n -> T n a -> T n b -> T n c
runZip :: T n a -> T n b -> T n c}

zipWith :: Natural n => (a -> b -> c) -> T n a -> T n b -> T n c
zipWith :: forall n a b c.
Natural n =>
(a -> b -> c) -> T n a -> T n b -> T n c
zipWith a -> b -> c
f =
   forall a b c n. Zip a b c n -> T n a -> T n b -> T n c
runZip forall a b. (a -> b) -> a -> b
$
   forall n (f :: * -> *).
Natural n =>
f Zero -> (forall m. Natural m => f (Succ m)) -> f n
switchNat
      (forall a b c n. (T n a -> T n b -> T n c) -> Zip a b c n
Zip forall a b. (a -> b) -> a -> b
$ forall b a. b -> T Zero a -> b
switchEnd forall a b. (a -> b) -> a -> b
$ forall b a. b -> T Zero a -> b
switchEnd forall a. T Zero a
end)
      (forall a b c n. (T n a -> T n b -> T n c) -> Zip a b c n
Zip forall a b. (a -> b) -> a -> b
$ forall a n b. (a -> T n a -> b) -> T (Succ n) a -> b
switchL forall a b. (a -> b) -> a -> b
$ \a
a T m a
as -> forall a n b. (a -> T n a -> b) -> T (Succ n) a -> b
switchL forall a b. (a -> b) -> a -> b
$ \b
b T m b
bs -> a -> b -> c
f a
a b
b forall a n. a -> T n a -> T (Succ n) a
!: forall n a b c.
Natural n =>
(a -> b -> c) -> T n a -> T n b -> T n c
zipWith a -> b -> c
f T m a
as T m b
bs)


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

instance Natural n => Foldable (T n) where
   foldMap :: forall m a. Monoid m => (a -> m) -> T n a -> m
foldMap = forall (t :: * -> *) m a.
(Traversable t, Monoid m) =>
(a -> m) -> t a -> m
foldMapDefault

instance Natural n => Traversable (T n) where
   sequenceA :: forall (f :: * -> *) a. Applicative f => T n (f a) -> f (T n a)
sequenceA = forall (f :: * -> *) n a.
(Applicative f, Natural n) =>
T n (f a) -> f (T n a)
sequenceA

instance Natural n => Applicative (T n) where
   pure :: forall a. a -> T n a
pure = forall n a. Natural n => a -> T n a
repeat
   T n (a -> b)
f <*> :: forall a b. T n (a -> b) -> T n a -> T n b
<*> T n a
x = forall n a b c.
Natural n =>
(a -> b -> c) -> T n a -> T n b -> T n c
zipWith forall a b. (a -> b) -> a -> b
($) T n (a -> b)
f T n a
x


type family Position n
type instance Position Unary.Zero = Zero
type instance Position (Unary.Succ n) = Succ (Position n)

data Zero
data Succ pos = Stop | Succ pos deriving (Succ pos -> Succ pos -> Bool
forall pos. Eq pos => Succ pos -> Succ pos -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Succ pos -> Succ pos -> Bool
$c/= :: forall pos. Eq pos => Succ pos -> Succ pos -> Bool
== :: Succ pos -> Succ pos -> Bool
$c== :: forall pos. Eq pos => Succ pos -> Succ pos -> Bool
Eq, Succ pos -> Succ pos -> Bool
Succ pos -> Succ pos -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {pos}. Ord pos => Eq (Succ pos)
forall pos. Ord pos => Succ pos -> Succ pos -> Bool
forall pos. Ord pos => Succ pos -> Succ pos -> Ordering
forall pos. Ord pos => Succ pos -> Succ pos -> Succ pos
min :: Succ pos -> Succ pos -> Succ pos
$cmin :: forall pos. Ord pos => Succ pos -> Succ pos -> Succ pos
max :: Succ pos -> Succ pos -> Succ pos
$cmax :: forall pos. Ord pos => Succ pos -> Succ pos -> Succ pos
>= :: Succ pos -> Succ pos -> Bool
$c>= :: forall pos. Ord pos => Succ pos -> Succ pos -> Bool
> :: Succ pos -> Succ pos -> Bool
$c> :: forall pos. Ord pos => Succ pos -> Succ pos -> Bool
<= :: Succ pos -> Succ pos -> Bool
$c<= :: forall pos. Ord pos => Succ pos -> Succ pos -> Bool
< :: Succ pos -> Succ pos -> Bool
$c< :: forall pos. Ord pos => Succ pos -> Succ pos -> Bool
compare :: Succ pos -> Succ pos -> Ordering
$ccompare :: forall pos. Ord pos => Succ pos -> Succ pos -> Ordering
Ord, Int -> Succ pos -> ShowS
forall pos. Show pos => Int -> Succ pos -> ShowS
forall pos. Show pos => [Succ pos] -> ShowS
forall pos. Show pos => Succ pos -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Succ pos] -> ShowS
$cshowList :: forall pos. Show pos => [Succ pos] -> ShowS
show :: Succ pos -> String
$cshow :: forall pos. Show pos => Succ pos -> String
showsPrec :: Int -> Succ pos -> ShowS
$cshowsPrec :: forall pos. Show pos => Int -> Succ pos -> ShowS
Show)

instance Eq Zero where Zero
_== :: Zero -> Zero -> Bool
==Zero
_ = Bool
True
instance Ord Zero where compare :: Zero -> Zero -> Ordering
compare Zero
_ Zero
_ = Ordering
EQ


newtype Index n = Index (Position n)

instance (Natural n) => Show (Index n) where
   show :: Index n -> String
show Index n
i = Char
'i' forall a. a -> [a] -> [a]
: forall a. Show a => a -> String
P.show (forall n. Natural n => Index n -> Word
numFromIndex Index n
i)

unpackSucc :: Index (Unary.Succ n) -> Succ (Index n)
unpackSucc :: forall n. Index (Succ n) -> Succ (Index n)
unpackSucc (Index Position (Succ n)
n1) =
   case Position (Succ n)
n1 of
      Succ (Position n)
Position (Succ n)
Stop -> forall pos. Succ pos
Stop
      Succ Position n
n0 -> forall pos. pos -> Succ pos
Succ forall a b. (a -> b) -> a -> b
$ forall n. Position n -> Index n
Index Position n
n0


newtype Update a n = Update {forall a n. Update a n -> Index n -> T n a -> T n a
runUpdate :: Index n -> T n a -> T n a}

update :: Natural n => (a -> a) -> Index n -> T n a -> T n a
update :: forall n a. Natural n => (a -> a) -> Index n -> T n a -> T n a
update a -> a
f =
   forall a n. Update a n -> Index n -> T n a -> T n a
runUpdate forall a b. (a -> b) -> a -> b
$
   forall n (f :: * -> *).
Natural n =>
f Zero -> (forall m. Natural m => f (Succ m)) -> f n
switchNat
      (forall a n. (Index n -> T n a -> T n a) -> Update a n
Update forall a b. (a -> b) -> a -> b
$ \ Index Zero
_ T Zero a
xs -> T Zero a
xs)
      (forall a n. (Index n -> T n a -> T n a) -> Update a n
Update forall a b. (a -> b) -> a -> b
$ \Index (Succ m)
pos0 -> forall a n b. (a -> T n a -> b) -> T (Succ n) a -> b
switchL forall a b. (a -> b) -> a -> b
$ \a
x T m a
xs ->
         case forall n. Index (Succ n) -> Succ (Index n)
unpackSucc Index (Succ m)
pos0 of
            Succ (Index m)
Stop -> a -> a
f a
x forall a n. a -> T n a -> T (Succ n) a
!: T m a
xs
            Succ Index m
pos1 -> a
x forall a n. a -> T n a -> T (Succ n) a
!: forall n a. Natural n => (a -> a) -> Index n -> T n a -> T n a
update a -> a
f Index m
pos1 T m a
xs)

newtype PeekIndex a n = PeekIndex {forall a n. PeekIndex a n -> Index n -> T n a -> a
runIndex :: Index n -> T n a -> a}

index :: Natural n => Index n -> T n a -> a
index :: forall n a. Natural n => Index n -> T n a -> a
index =
   forall a n. PeekIndex a n -> Index n -> T n a -> a
runIndex forall a b. (a -> b) -> a -> b
$
   forall n (f :: * -> *).
Natural n =>
f Zero -> (forall m. Natural m => f (Succ m)) -> f n
switchNat
      (forall a n. (Index n -> T n a -> a) -> PeekIndex a n
PeekIndex forall a b. (a -> b) -> a -> b
$ \ Index Zero
_ {- Zero -} -> forall b a. b -> T Zero a -> b
switchEnd forall a b. (a -> b) -> a -> b
$ forall a. HasCallStack => String -> a
error String
"impossible index")
      (forall a n. (Index n -> T n a -> a) -> PeekIndex a n
PeekIndex forall a b. (a -> b) -> a -> b
$ \Index (Succ m)
pos0 -> forall a n b. (a -> T n a -> b) -> T (Succ n) a -> b
switchL forall a b. (a -> b) -> a -> b
$ \a
x T m a
xs ->
          case forall n. Index (Succ n) -> Succ (Index n)
unpackSucc Index (Succ m)
pos0 of
             Succ (Index m)
Stop -> a
x
             Succ Index m
pos1 -> forall n a. Natural n => Index n -> T n a -> a
index Index m
pos1 T m a
xs)

newtype Indices n = Indices {forall n. Indices n -> T n (Index n)
runIndices :: T n (Index n)}

indices :: Natural n => T n (Index n)
indices :: forall n. Natural n => T n (Index n)
indices =
   forall n. Indices n -> T n (Index n)
runIndices forall a b. (a -> b) -> a -> b
$
   forall n (f :: * -> *).
Natural n =>
f Zero -> (forall m. Natural m => f (Succ m)) -> f n
switchNat
      (forall n. T n (Index n) -> Indices n
Indices forall a. T Zero a
end)
      (forall n. T n (Index n) -> Indices n
Indices forall a b. (a -> b) -> a -> b
$ forall n. Index (GE1 n)
i0 forall a n. a -> T n a -> T (Succ n) a
!: forall n a b. Natural n => (a -> b) -> T n a -> T n b
map forall n. Index n -> Index (Succ n)
succ forall n. Natural n => T n (Index n)
indices)

indicesInt :: Natural n => T n Int
indicesInt :: forall n. Natural n => T n Int
indicesInt =
   forall (f :: * -> *) a. Traversable f => T f a -> f a
NonEmpty.init forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) b a.
Traversable f =>
(b -> a -> b) -> b -> f a -> T f b
NonEmpty.scanl forall a. Num a => a -> a -> a
(+) Int
0 forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
App.pure Int
1


newtype NumFromIndex n = NumFromIndex {forall n. NumFromIndex n -> Index n -> Word
runNumFromIndex :: Index n -> Word}

numFromIndex :: Natural n => Index n -> Word
numFromIndex :: forall n. Natural n => Index n -> Word
numFromIndex =
   forall n. NumFromIndex n -> Index n -> Word
runNumFromIndex forall a b. (a -> b) -> a -> b
$
   forall n (f :: * -> *).
Natural n =>
f Zero -> (forall m. Natural m => f (Succ m)) -> f n
switchNat
      (forall n. (Index n -> Word) -> NumFromIndex n
NumFromIndex forall a b. (a -> b) -> a -> b
$ \Index Zero
_ -> forall a. HasCallStack => String -> a
error String
"numFromIndex")
      (forall n. (Index n -> Word) -> NumFromIndex n
NumFromIndex forall a b. (a -> b) -> a -> b
$ \Index (Succ m)
n ->
         case forall n. Index (Succ n) -> Succ (Index n)
unpackSucc Index (Succ m)
n of
            Succ (Index m)
Stop -> Word
0
            Succ Index m
m -> Word
1 forall a. Num a => a -> a -> a
+ forall n. Natural n => Index n -> Word
numFromIndex Index m
m)


newtype
   IndexFromNum n = IndexFromNum {forall n. IndexFromNum n -> Word -> Maybe (Index n)
runIndexFromNum :: Word -> Maybe (Index n)}

indexFromNum :: Natural n => Word -> Maybe (Index n)
indexFromNum :: forall n. Natural n => Word -> Maybe (Index n)
indexFromNum =
   forall n. IndexFromNum n -> Word -> Maybe (Index n)
runIndexFromNum forall a b. (a -> b) -> a -> b
$
   forall n (f :: * -> *).
Natural n =>
f Zero -> (forall m. Natural m => f (Succ m)) -> f n
switchNat
      (forall n. (Word -> Maybe (Index n)) -> IndexFromNum n
IndexFromNum forall a b. (a -> b) -> a -> b
$ \ Word
_k -> forall a. Maybe a
Nothing)
      (forall n. (Word -> Maybe (Index n)) -> IndexFromNum n
IndexFromNum forall a b. (a -> b) -> a -> b
$ \Word
k ->
         if Word
kforall a. Eq a => a -> a -> Bool
==Word
0 then forall a. a -> Maybe a
Just forall n. Index (GE1 n)
i0 else forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall n. Index n -> Index (Succ n)
succ forall a b. (a -> b) -> a -> b
$ forall n. Natural n => Word -> Maybe (Index n)
indexFromNum (Word
kforall a. Num a => a -> a -> a
-Word
1))


newtype Compare a n = Compare {forall a n. Compare a n -> Index n -> Index n -> a
runCompare :: Index n -> Index n -> a}

instance (Natural n) => Eq (Index n) where
   == :: Index n -> Index n -> Bool
(==) =
      forall a n. Compare a n -> Index n -> Index n -> a
runCompare forall a b. (a -> b) -> a -> b
$
      forall n (f :: * -> *).
Natural n =>
f Zero -> (forall m. Natural m => f (Succ m)) -> f n
switchNat
         (forall a n. (Index n -> Index n -> a) -> Compare a n
Compare forall a b. (a -> b) -> a -> b
$ \Index Zero
_ Index Zero
_ -> forall a. HasCallStack => String -> a
error String
"equalIndex")
         (forall a n. (Index n -> Index n -> a) -> Compare a n
Compare forall a b. (a -> b) -> a -> b
$ \Index (Succ m)
i Index (Succ m)
j ->
            case (forall n. Index (Succ n) -> Succ (Index n)
unpackSucc Index (Succ m)
i, forall n. Index (Succ n) -> Succ (Index n)
unpackSucc Index (Succ m)
j) of
               (Succ Index m
k, Succ Index m
l) -> Index m
k forall a. Eq a => a -> a -> Bool
== Index m
l
               (Succ (Index m)
Stop, Succ (Index m)
Stop) -> Bool
True
               (Succ (Index m), Succ (Index m))
_ -> Bool
False)

instance (Natural n) => Ord (Index n) where
   compare :: Index n -> Index n -> Ordering
compare =
      forall a n. Compare a n -> Index n -> Index n -> a
runCompare forall a b. (a -> b) -> a -> b
$
      forall n (f :: * -> *).
Natural n =>
f Zero -> (forall m. Natural m => f (Succ m)) -> f n
switchNat
         (forall a n. (Index n -> Index n -> a) -> Compare a n
Compare forall a b. (a -> b) -> a -> b
$ \Index Zero
_ Index Zero
_ -> forall a. HasCallStack => String -> a
error String
"compareIndex")
         (forall a n. (Index n -> Index n -> a) -> Compare a n
Compare forall a b. (a -> b) -> a -> b
$ \Index (Succ m)
i Index (Succ m)
j ->
            case (forall n. Index (Succ n) -> Succ (Index n)
unpackSucc Index (Succ m)
i, forall n. Index (Succ n) -> Succ (Index n)
unpackSucc Index (Succ m)
j) of
               (Succ Index m
k, Succ Index m
l) -> forall a. Ord a => a -> a -> Ordering
compare Index m
k Index m
l
               (Succ (Index m)
Stop, Succ (Index m)
Stop) -> Ordering
EQ
               (Succ (Index m)
Stop, Succ Index m
_) -> Ordering
LT
               (Succ Index m
_, Succ (Index m)
Stop) -> Ordering
GT)


type GE1 n = Unary.Succ n
type GE2 n = Unary.Succ (GE1 n)
type GE3 n = Unary.Succ (GE2 n)
type GE4 n = Unary.Succ (GE3 n)
type GE5 n = Unary.Succ (GE4 n)
type GE6 n = Unary.Succ (GE5 n)
type GE7 n = Unary.Succ (GE6 n)
type GE8 n = Unary.Succ (GE7 n)

succ :: Index n -> Index (Unary.Succ n)
succ :: forall n. Index n -> Index (Succ n)
succ (Index Position n
n) = forall n. Position n -> Index n
Index (forall pos. pos -> Succ pos
Succ Position n
n)

i0 :: Index (GE1 n); i0 :: forall n. Index (GE1 n)
i0 = forall n. Position n -> Index n
Index forall pos. Succ pos
Stop
i1 :: Index (GE2 n); i1 :: forall n. Index (GE2 n)
i1 = forall n. Index n -> Index (Succ n)
succ forall n. Index (GE1 n)
i0
i2 :: Index (GE3 n); i2 :: forall n. Index (GE3 n)
i2 = forall n. Index n -> Index (Succ n)
succ forall n. Index (GE2 n)
i1
i3 :: Index (GE4 n); i3 :: forall n. Index (GE4 n)
i3 = forall n. Index n -> Index (Succ n)
succ forall n. Index (GE3 n)
i2
i4 :: Index (GE5 n); i4 :: forall n. Index (GE5 n)
i4 = forall n. Index n -> Index (Succ n)
succ forall n. Index (GE4 n)
i3
i5 :: Index (GE6 n); i5 :: forall n. Index (GE6 n)
i5 = forall n. Index n -> Index (Succ n)
succ forall n. Index (GE5 n)
i4
i6 :: Index (GE7 n); i6 :: forall n. Index (GE7 n)
i6 = forall n. Index n -> Index (Succ n)
succ forall n. Index (GE6 n)
i5
i7 :: Index (GE8 n); i7 :: forall n. Index (GE8 n)
i7 = forall n. Index n -> Index (Succ n)
succ forall n. Index (GE7 n)
i6



type family Curried n a b
type instance Curried Unary.Zero a b = b
type instance Curried (Unary.Succ n) a b = a -> Curried n a b

newtype Curry a b n = Curry {forall a b n. Curry a b n -> (T n a -> b) -> Curried n a b
runCurry :: (T n a -> b) -> Curried n a b}

curry :: (Unary.Natural n) => (T n a -> b) -> Curried n a b
curry :: forall n a b. Natural n => (T n a -> b) -> Curried n a b
curry =
   forall a b n. Curry a b n -> (T n a -> b) -> Curried n a b
runCurry forall a b. (a -> b) -> a -> b
$
   forall n (f :: * -> *).
Natural n =>
f Zero -> (forall m. Natural m => f (Succ m)) -> f n
Unary.switchNat
      (forall a b n. ((T n a -> b) -> Curried n a b) -> Curry a b n
Curry forall a b. (a -> b) -> a -> b
$ (forall a b. (a -> b) -> a -> b
$ forall a. T Zero a
end))
      (forall a b n. ((T n a -> b) -> Curried n a b) -> Curry a b n
Curry forall a b. (a -> b) -> a -> b
$ \T (Succ m) a -> b
f a
a -> forall n a b. Natural n => (T n a -> b) -> Curried n a b
curry forall a b. (a -> b) -> a -> b
$ \T m a
xs -> T (Succ m) a -> b
f (a
aforall a n. a -> T n a -> T (Succ n) a
!:T m a
xs))

newtype Uncurry a b n = Uncurry {forall a b n. Uncurry a b n -> Curried n a b -> T n a -> b
runUncurry :: Curried n a b -> T n a -> b}

uncurry :: (Unary.Natural n) => Curried n a b -> T n a -> b
uncurry :: forall n a b. Natural n => Curried n a b -> T n a -> b
uncurry =
   forall a b n. Uncurry a b n -> Curried n a b -> T n a -> b
runUncurry forall a b. (a -> b) -> a -> b
$
   forall n (f :: * -> *).
Natural n =>
f Zero -> (forall m. Natural m => f (Succ m)) -> f n
Unary.switchNat
      (forall a b n. (Curried n a b -> T n a -> b) -> Uncurry a b n
Uncurry forall b a. b -> T Zero a -> b
switchEnd)
      (forall a b n. (Curried n a b -> T n a -> b) -> Uncurry a b n
Uncurry forall a b. (a -> b) -> a -> b
$ \Curried (Succ m) a b
f -> forall a n b. (a -> T n a -> b) -> T (Succ n) a -> b
switchL (\a
x -> forall n a b. Natural n => Curried n a b -> T n a -> b
uncurry (Curried (Succ m) a b
f a
x)))


class ConsAll f where
   type NumberOfArguments f
   type ResultSize f
   type ResultElement f
   consAux ::
      (NumberOfArguments f ~ m, ResultSize f ~ n, ResultElement f ~ a) =>
      (T m a -> T n a) -> f

instance ConsAll (T n a) where
   type NumberOfArguments (T n a) = Unary.Zero
   type ResultSize (T n a) = n
   type ResultElement (T n a) = a
   consAux :: forall m n a.
(NumberOfArguments (T n a) ~ m, ResultSize (T n a) ~ n,
 ResultElement (T n a) ~ a) =>
(T m a -> T n a) -> T n a
consAux T m a -> T n a
f = T m a -> T n a
f forall a. T Zero a
end

instance (a ~ ResultElement f, ConsAll f) => ConsAll (a -> f) where
   type NumberOfArguments (a->f) = Unary.Succ (NumberOfArguments f)
   type ResultSize (a->f) = ResultSize f
   type ResultElement (a->f) = ResultElement f
   consAux :: forall m n a.
(NumberOfArguments (a -> f) ~ m, ResultSize (a -> f) ~ n,
 ResultElement (a -> f) ~ a) =>
(T m a -> T n a) -> a -> f
consAux T m a -> T n a
f a
x = forall f m n a.
(ConsAll f, NumberOfArguments f ~ m, ResultSize f ~ n,
 ResultElement f ~ a) =>
(T m a -> T n a) -> f
consAux (T m a -> T n a
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a
xforall a n. a -> T n a -> T (Succ n) a
!:))

consAll ::
   (ConsAll f, ResultSize f ~ n, NumberOfArguments f ~ n, Natural n) => f
consAll :: forall f n.
(ConsAll f, ResultSize f ~ n, NumberOfArguments f ~ n,
 Natural n) =>
f
consAll = forall f m n a.
(ConsAll f, NumberOfArguments f ~ m, ResultSize f ~ n,
 ResultElement f ~ a) =>
(T m a -> T n a) -> f
consAux forall a. a -> a
P.id


undefinedElem :: T n a -> a
undefinedElem :: forall n a. T n a -> a
undefinedElem T n a
_ = forall a. HasCallStack => String -> a
error String
"touched element by accident"

instance (Natural n, Storable a) => Storable (T n a) where
   sizeOf :: T n a -> Int
sizeOf T n a
xs = forall a. Storable a => Int -> a -> Int
StoreArray.sizeOfArray (forall (t :: * -> *) a. Foldable t => t a -> Int
P.length forall a b. (a -> b) -> a -> b
$ forall n a. Natural n => T n a -> [a]
toList T n a
xs) (forall n a. T n a -> a
undefinedElem T n a
xs)
   alignment :: T n a -> Int
alignment = forall a. Storable a => a -> Int
alignment forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n a. T n a -> a
undefinedElem
   peek :: Ptr (T n a) -> IO (T n a)
peek = forall (f :: * -> *) a.
(Applicative f, Traversable f, Storable a) =>
Ptr (f a) -> IO (f a)
StoreTrav.peekApplicative
   poke :: Ptr (T n a) -> T n a -> IO ()
poke = forall (f :: * -> *) a.
(Foldable f, Storable a) =>
Ptr (f a) -> f a -> IO ()
StoreTrav.poke