{-# 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
_ -> 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