{-# 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.List as List
import Control.Applicative (Applicative, liftA2)
import Data.Traversable (Traversable, foldMapDefault)
import Data.Foldable (Foldable, foldMap)
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 :: List n a -> T n a
fromFixedList = List n a -> T n a
forall n a. List n a -> T n a
Cons

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


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

infixr 5 !:

(!:) :: {- (Natural n) => -} a -> T n a -> T (Unary.Succ n) a
a
x !: :: a -> T n a -> T (Succ n) a
!: Cons List n a
xs = List (Succ n) a -> T (Succ n) a
forall n a. List n a -> T n a
Cons (List (Succ n) a -> T (Succ n) a)
-> List (Succ n) a -> T (Succ n) a
forall a b. (a -> b) -> a -> b
$ a -> List n a -> T (List n) a
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 :: T (Succ n) a -> (a, T n a)
viewL (Cons (NonEmpty.Cons x xs)) = (a
x, List n a -> T n a
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 :: (a -> T n a -> b) -> T (Succ n) a -> b
switchL a -> T n a -> b
f = (a -> T n a -> b) -> (a, T n a) -> b
forall a b c. (a -> b -> c) -> (a, b) -> c
P.uncurry a -> T n a -> b
f ((a, T n a) -> b)
-> (T (Succ n) a -> (a, T n a)) -> T (Succ n) a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T (Succ n) a -> (a, T n a)
forall n a. T (Succ n) a -> (a, T n a)
viewL

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


newtype WithPos a b n = WithPos {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 m. Natural m => T (Succ m) a -> b) -> T n a -> b
withPos forall m. Natural m => T (Succ m) a -> b
f = WithPos a b n -> T n a -> b
forall a b n. WithPos a b n -> T n a -> b
runWithPos (WithPos a b n -> T n a -> b) -> WithPos a b n -> T n a -> b
forall a b. (a -> b) -> a -> b
$ (forall m. Natural m => WithPos a b (Succ m)) -> WithPos a b n
forall n (f :: * -> *).
Positive n =>
(forall m. Natural m => f (Succ m)) -> f n
Unary.switchPos ((T (Succ m) a -> b) -> WithPos a b (Succ m)
forall a b n. (T n a -> b) -> WithPos a b n
WithPos T (Succ m) a -> b
forall m. Natural m => T (Succ m) a -> b
f)

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

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

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

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

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



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

showsPrec :: (Natural n, Show a) => Int -> T n a -> ShowS
showsPrec :: Int -> T n a -> ShowS
showsPrec Int
p =
   Bool -> ShowS -> ShowS
P.showParen (Int
pInt -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>Int
5) (ShowS -> ShowS) -> (T n a -> ShowS) -> T n a -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ShowS] -> ShowS
concatS ([ShowS] -> ShowS) -> (T n a -> [ShowS]) -> T n a -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
   ShowS -> [ShowS] -> [ShowS]
forall a. a -> [a] -> [a]
List.intersperse (String -> ShowS
P.showString String
"!:") ([ShowS] -> [ShowS]) -> (T n a -> [ShowS]) -> T n a -> [ShowS]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
   ([ShowS] -> [ShowS] -> [ShowS]
forall a. [a] -> [a] -> [a]
++ [String -> ShowS
P.showString String
"end"]) ([ShowS] -> [ShowS]) -> (T n a -> [ShowS]) -> T n a -> [ShowS]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
   (a -> ShowS) -> [a] -> [ShowS]
forall a b. (a -> b) -> [a] -> [b]
List.map (Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
P.showsPrec Int
6) ([a] -> [ShowS]) -> (T n a -> [a]) -> T n a -> [ShowS]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T n a -> [a]
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 = Int -> T n a -> ShowS
forall n a. (Natural n, Show a) => Int -> T n a -> ShowS
showsPrec


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


newtype Map a b n = Map {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 :: (a -> b) -> T n a -> T n b
map a -> b
f =
   Map a b n -> T n a -> T n b
forall a b n. Map a b n -> T n a -> T n b
runMap (Map a b n -> T n a -> T n b) -> Map a b n -> T n a -> T n b
forall a b. (a -> b) -> a -> b
$
   Map a b Zero
-> (forall m. Natural m => Map a b (Succ m)) -> Map a b n
forall n (f :: * -> *).
Natural n =>
f Zero -> (forall m. Natural m => f (Succ m)) -> f n
switchNat
      ((T Zero a -> T Zero b) -> Map a b Zero
forall a b n. (T n a -> T n b) -> Map a b n
Map ((T Zero a -> T Zero b) -> Map a b Zero)
-> (T Zero a -> T Zero b) -> Map a b Zero
forall a b. (a -> b) -> a -> b
$ T Zero b -> T Zero a -> T Zero b
forall b a. b -> T Zero a -> b
switchEnd T Zero b
forall a. T Zero a
end)
      ((T (Succ m) a -> T (Succ m) b) -> Map a b (Succ m)
forall a b n. (T n a -> T n b) -> Map a b n
Map ((T (Succ m) a -> T (Succ m) b) -> Map a b (Succ m))
-> (T (Succ m) a -> T (Succ m) b) -> Map a b (Succ m)
forall a b. (a -> b) -> a -> b
$ (a -> T m a -> T (Succ m) b) -> T (Succ m) a -> T (Succ m) b
forall a n b. (a -> T n a -> b) -> T (Succ n) a -> b
switchL ((a -> T m a -> T (Succ m) b) -> T (Succ m) a -> T (Succ m) b)
-> (a -> T m a -> T (Succ m) b) -> T (Succ m) a -> T (Succ m) b
forall a b. (a -> b) -> a -> b
$ \a
x T m a
xs -> a -> b
f a
x b -> T m b -> T (Succ m) b
forall a n. a -> T n a -> T (Succ n) a
!: (a -> b) -> T m a -> T m b
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 {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 :: T n (f a) -> f (T n a)
sequenceA =
   Sequence f a n -> T n (f a) -> f (T n a)
forall (f :: * -> *) a n. Sequence f a n -> T n (f a) -> f (T n a)
runSequence (Sequence f a n -> T n (f a) -> f (T n a))
-> Sequence f a n -> T n (f a) -> f (T n a)
forall a b. (a -> b) -> a -> b
$
   Sequence f a Zero
-> (forall m. Natural m => Sequence f a (Succ m)) -> Sequence f a n
forall n (f :: * -> *).
Natural n =>
f Zero -> (forall m. Natural m => f (Succ m)) -> f n
switchNat
      ((T Zero (f a) -> f (T Zero a)) -> Sequence f a Zero
forall (f :: * -> *) a n.
(T n (f a) -> f (T n a)) -> Sequence f a n
Sequence ((T Zero (f a) -> f (T Zero a)) -> Sequence f a Zero)
-> (T Zero (f a) -> f (T Zero a)) -> Sequence f a Zero
forall a b. (a -> b) -> a -> b
$ f (T Zero a) -> T Zero (f a) -> f (T Zero a)
forall b a. b -> T Zero a -> b
switchEnd (f (T Zero a) -> T Zero (f a) -> f (T Zero a))
-> f (T Zero a) -> T Zero (f a) -> f (T Zero a)
forall a b. (a -> b) -> a -> b
$ T Zero a -> f (T Zero a)
forall (f :: * -> *) a. Applicative f => a -> f a
App.pure T Zero a
forall a. T Zero a
end)
      ((T (Succ m) (f a) -> f (T (Succ m) a)) -> Sequence f a (Succ m)
forall (f :: * -> *) a n.
(T n (f a) -> f (T n a)) -> Sequence f a n
Sequence ((T (Succ m) (f a) -> f (T (Succ m) a)) -> Sequence f a (Succ m))
-> (T (Succ m) (f a) -> f (T (Succ m) a)) -> Sequence f a (Succ m)
forall a b. (a -> b) -> a -> b
$ (f a -> T m (f a) -> f (T (Succ m) a))
-> T (Succ m) (f a) -> f (T (Succ m) a)
forall a n b. (a -> T n a -> b) -> T (Succ n) a -> b
switchL ((f a -> T m (f a) -> f (T (Succ m) a))
 -> T (Succ m) (f a) -> f (T (Succ m) a))
-> (f a -> T m (f a) -> f (T (Succ m) a))
-> T (Succ m) (f a)
-> f (T (Succ m) a)
forall a b. (a -> b) -> a -> b
$ \f a
x T m (f a)
xs -> (a -> T m a -> T (Succ m) a)
-> f a -> f (T m a) -> f (T (Succ m) a)
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 a -> T m a -> T (Succ m) a
forall a n. a -> T n a -> T (Succ n) a
(!:) f a
x (f (T m a) -> f (T (Succ m) a)) -> f (T m a) -> f (T (Succ m) a)
forall a b. (a -> b) -> a -> b
$ T m (f a) -> f (T m a)
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 {Repeat a n -> T n a
runRepeat :: T n a}

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


newtype Zip a b c n = Zip {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 :: (a -> b -> c) -> T n a -> T n b -> T n c
zipWith a -> b -> c
f =
   Zip a b c n -> T n a -> T n b -> T n c
forall a b c n. Zip a b c n -> T n a -> T n b -> T n c
runZip (Zip a b c n -> T n a -> T n b -> T n c)
-> Zip a b c n -> T n a -> T n b -> T n c
forall a b. (a -> b) -> a -> b
$
   Zip a b c Zero
-> (forall m. Natural m => Zip a b c (Succ m)) -> Zip a b c n
forall n (f :: * -> *).
Natural n =>
f Zero -> (forall m. Natural m => f (Succ m)) -> f n
switchNat
      ((T Zero a -> T Zero b -> T Zero c) -> Zip a b c Zero
forall a b c n. (T n a -> T n b -> T n c) -> Zip a b c n
Zip ((T Zero a -> T Zero b -> T Zero c) -> Zip a b c Zero)
-> (T Zero a -> T Zero b -> T Zero c) -> Zip a b c Zero
forall a b. (a -> b) -> a -> b
$ (T Zero b -> T Zero c) -> T Zero a -> T Zero b -> T Zero c
forall b a. b -> T Zero a -> b
switchEnd ((T Zero b -> T Zero c) -> T Zero a -> T Zero b -> T Zero c)
-> (T Zero b -> T Zero c) -> T Zero a -> T Zero b -> T Zero c
forall a b. (a -> b) -> a -> b
$ T Zero c -> T Zero b -> T Zero c
forall b a. b -> T Zero a -> b
switchEnd T Zero c
forall a. T Zero a
end)
      ((T (Succ m) a -> T (Succ m) b -> T (Succ m) c)
-> Zip a b c (Succ m)
forall a b c n. (T n a -> T n b -> T n c) -> Zip a b c n
Zip ((T (Succ m) a -> T (Succ m) b -> T (Succ m) c)
 -> Zip a b c (Succ m))
-> (T (Succ m) a -> T (Succ m) b -> T (Succ m) c)
-> Zip a b c (Succ m)
forall a b. (a -> b) -> a -> b
$ (a -> T m a -> T (Succ m) b -> T (Succ m) c)
-> T (Succ m) a -> T (Succ m) b -> T (Succ m) c
forall a n b. (a -> T n a -> b) -> T (Succ n) a -> b
switchL ((a -> T m a -> T (Succ m) b -> T (Succ m) c)
 -> T (Succ m) a -> T (Succ m) b -> T (Succ m) c)
-> (a -> T m a -> T (Succ m) b -> T (Succ m) c)
-> T (Succ m) a
-> T (Succ m) b
-> T (Succ m) c
forall a b. (a -> b) -> a -> b
$ \a
a T m a
as -> (b -> T m b -> T (Succ m) c) -> T (Succ m) b -> T (Succ m) c
forall a n b. (a -> T n a -> b) -> T (Succ n) a -> b
switchL ((b -> T m b -> T (Succ m) c) -> T (Succ m) b -> T (Succ m) c)
-> (b -> T m b -> T (Succ m) c) -> T (Succ m) b -> T (Succ m) c
forall a b. (a -> b) -> a -> b
$ \b
b T m b
bs -> a -> b -> c
f a
a b
b c -> T m c -> T (Succ m) c
forall a n. a -> T n a -> T (Succ n) a
!: (a -> b -> c) -> T m a -> T m b -> T m c
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 :: (a -> b) -> T n a -> T n b
fmap = (a -> b) -> T n a -> T n b
forall n a b. Natural n => (a -> b) -> T n a -> T n b
map

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

instance Natural n => Traversable (T n) where
   sequenceA :: T n (f a) -> f (T n a)
sequenceA = T n (f a) -> f (T n a)
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 :: a -> T n a
pure = a -> T n a
forall n a. Natural n => a -> T n a
repeat
   T n (a -> b)
f <*> :: T n (a -> b) -> T n a -> T n b
<*> T n a
x = ((a -> b) -> a -> b) -> T n (a -> b) -> T n a -> T n b
forall n a b c.
Natural n =>
(a -> b -> c) -> T n a -> T n b -> T n c
zipWith (a -> b) -> a -> b
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
(Succ pos -> Succ pos -> Bool)
-> (Succ pos -> Succ pos -> Bool) -> Eq (Succ pos)
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, Eq (Succ pos)
Eq (Succ pos)
-> (Succ pos -> Succ pos -> Ordering)
-> (Succ pos -> Succ pos -> Bool)
-> (Succ pos -> Succ pos -> Bool)
-> (Succ pos -> Succ pos -> Bool)
-> (Succ pos -> Succ pos -> Bool)
-> (Succ pos -> Succ pos -> Succ pos)
-> (Succ pos -> Succ pos -> Succ pos)
-> Ord (Succ pos)
Succ pos -> Succ pos -> Bool
Succ pos -> Succ pos -> Ordering
Succ pos -> Succ pos -> Succ pos
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
$cp1Ord :: forall pos. Ord pos => Eq (Succ pos)
Ord, Int -> Succ pos -> ShowS
[Succ pos] -> ShowS
Succ pos -> String
(Int -> Succ pos -> ShowS)
-> (Succ pos -> String) -> ([Succ pos] -> ShowS) -> Show (Succ pos)
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)

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


newtype Update a n = Update {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 :: (a -> a) -> Index n -> T n a -> T n a
update a -> a
f =
   Update a n -> Index n -> T n a -> T n a
forall a n. Update a n -> Index n -> T n a -> T n a
runUpdate (Update a n -> Index n -> T n a -> T n a)
-> Update a n -> Index n -> T n a -> T n a
forall a b. (a -> b) -> a -> b
$
   Update a Zero
-> (forall m. Natural m => Update a (Succ m)) -> Update a n
forall n (f :: * -> *).
Natural n =>
f Zero -> (forall m. Natural m => f (Succ m)) -> f n
switchNat
      ((Index Zero -> T Zero a -> T Zero a) -> Update a Zero
forall a n. (Index n -> T n a -> T n a) -> Update a n
Update ((Index Zero -> T Zero a -> T Zero a) -> Update a Zero)
-> (Index Zero -> T Zero a -> T Zero a) -> Update a Zero
forall a b. (a -> b) -> a -> b
$ \ Index Zero
_ T Zero a
xs -> T Zero a
xs)
      ((Index (Succ m) -> T (Succ m) a -> T (Succ m) a)
-> Update a (Succ m)
forall a n. (Index n -> T n a -> T n a) -> Update a n
Update ((Index (Succ m) -> T (Succ m) a -> T (Succ m) a)
 -> Update a (Succ m))
-> (Index (Succ m) -> T (Succ m) a -> T (Succ m) a)
-> Update a (Succ m)
forall a b. (a -> b) -> a -> b
$ \Index (Succ m)
pos0 -> (a -> T m a -> T (Succ m) a) -> T (Succ m) a -> T (Succ m) a
forall a n b. (a -> T n a -> b) -> T (Succ n) a -> b
switchL ((a -> T m a -> T (Succ m) a) -> T (Succ m) a -> T (Succ m) a)
-> (a -> T m a -> T (Succ m) a) -> T (Succ m) a -> T (Succ m) a
forall a b. (a -> b) -> a -> b
$ \a
x T m a
xs ->
         case Index (Succ m) -> Succ (Index m)
forall n. Index (Succ n) -> Succ (Index n)
unpackSucc Index (Succ m)
pos0 of
            Succ (Index m)
Stop -> a -> a
f a
x a -> T m a -> T (Succ m) a
forall a n. a -> T n a -> T (Succ n) a
!: T m a
xs
            Succ Index m
pos1 -> a
x a -> T m a -> T (Succ m) a
forall a n. a -> T n a -> T (Succ n) a
!: (a -> a) -> Index m -> T m a -> T m 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 {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 :: Index n -> T n a -> a
index =
   PeekIndex a n -> Index n -> T n a -> a
forall a n. PeekIndex a n -> Index n -> T n a -> a
runIndex (PeekIndex a n -> Index n -> T n a -> a)
-> PeekIndex a n -> Index n -> T n a -> a
forall a b. (a -> b) -> a -> b
$
   PeekIndex a Zero
-> (forall m. Natural m => PeekIndex a (Succ m)) -> PeekIndex a n
forall n (f :: * -> *).
Natural n =>
f Zero -> (forall m. Natural m => f (Succ m)) -> f n
switchNat
      ((Index Zero -> T Zero a -> a) -> PeekIndex a Zero
forall a n. (Index n -> T n a -> a) -> PeekIndex a n
PeekIndex ((Index Zero -> T Zero a -> a) -> PeekIndex a Zero)
-> (Index Zero -> T Zero a -> a) -> PeekIndex a Zero
forall a b. (a -> b) -> a -> b
$ \ Index Zero
_ {- Zero -} -> a -> T Zero a -> a
forall b a. b -> T Zero a -> b
switchEnd (a -> T Zero a -> a) -> a -> T Zero a -> a
forall a b. (a -> b) -> a -> b
$ String -> a
forall a. HasCallStack => String -> a
error String
"impossible index")
      ((Index (Succ m) -> T (Succ m) a -> a) -> PeekIndex a (Succ m)
forall a n. (Index n -> T n a -> a) -> PeekIndex a n
PeekIndex ((Index (Succ m) -> T (Succ m) a -> a) -> PeekIndex a (Succ m))
-> (Index (Succ m) -> T (Succ m) a -> a) -> PeekIndex a (Succ m)
forall a b. (a -> b) -> a -> b
$ \Index (Succ m)
pos0 -> (a -> T m a -> a) -> T (Succ m) a -> a
forall a n b. (a -> T n a -> b) -> T (Succ n) a -> b
switchL ((a -> T m a -> a) -> T (Succ m) a -> a)
-> (a -> T m a -> a) -> T (Succ m) a -> a
forall a b. (a -> b) -> a -> b
$ \a
x T m a
xs ->
          case Index (Succ m) -> Succ (Index m)
forall n. Index (Succ n) -> Succ (Index n)
unpackSucc Index (Succ m)
pos0 of
             Succ (Index m)
Stop -> a
x
             Succ Index m
pos1 -> Index m -> T m a -> a
forall n a. Natural n => Index n -> T n a -> a
index Index m
pos1 T m a
xs)

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

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

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


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

numFromIndex :: Natural n => Index n -> Word
numFromIndex :: Index n -> Word
numFromIndex =
   NumFromIndex n -> Index n -> Word
forall n. NumFromIndex n -> Index n -> Word
runNumFromIndex (NumFromIndex n -> Index n -> Word)
-> NumFromIndex n -> Index n -> Word
forall a b. (a -> b) -> a -> b
$
   NumFromIndex Zero
-> (forall m. Natural m => NumFromIndex (Succ m)) -> NumFromIndex n
forall n (f :: * -> *).
Natural n =>
f Zero -> (forall m. Natural m => f (Succ m)) -> f n
switchNat
      ((Index Zero -> Word) -> NumFromIndex Zero
forall n. (Index n -> Word) -> NumFromIndex n
NumFromIndex ((Index Zero -> Word) -> NumFromIndex Zero)
-> (Index Zero -> Word) -> NumFromIndex Zero
forall a b. (a -> b) -> a -> b
$ \Index Zero
_ -> String -> Word
forall a. HasCallStack => String -> a
error String
"numFromIndex")
      ((Index (Succ m) -> Word) -> NumFromIndex (Succ m)
forall n. (Index n -> Word) -> NumFromIndex n
NumFromIndex ((Index (Succ m) -> Word) -> NumFromIndex (Succ m))
-> (Index (Succ m) -> Word) -> NumFromIndex (Succ m)
forall a b. (a -> b) -> a -> b
$ \Index (Succ m)
n ->
         case Index (Succ m) -> Succ (Index m)
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 Word -> Word -> Word
forall a. Num a => a -> a -> a
+ Index m -> Word
forall n. Natural n => Index n -> Word
numFromIndex Index m
m)


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

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


newtype Compare a n = Compare {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
(==) =
      Compare Bool n -> Index n -> Index n -> Bool
forall a n. Compare a n -> Index n -> Index n -> a
runCompare (Compare Bool n -> Index n -> Index n -> Bool)
-> Compare Bool n -> Index n -> Index n -> Bool
forall a b. (a -> b) -> a -> b
$
      Compare Bool Zero
-> (forall m. Natural m => Compare Bool (Succ m)) -> Compare Bool n
forall n (f :: * -> *).
Natural n =>
f Zero -> (forall m. Natural m => f (Succ m)) -> f n
switchNat
         ((Index Zero -> Index Zero -> Bool) -> Compare Bool Zero
forall a n. (Index n -> Index n -> a) -> Compare a n
Compare ((Index Zero -> Index Zero -> Bool) -> Compare Bool Zero)
-> (Index Zero -> Index Zero -> Bool) -> Compare Bool Zero
forall a b. (a -> b) -> a -> b
$ \Index Zero
_ Index Zero
_ -> String -> Bool
forall a. HasCallStack => String -> a
error String
"equalIndex")
         ((Index (Succ m) -> Index (Succ m) -> Bool) -> Compare Bool (Succ m)
forall a n. (Index n -> Index n -> a) -> Compare a n
Compare ((Index (Succ m) -> Index (Succ m) -> Bool)
 -> Compare Bool (Succ m))
-> (Index (Succ m) -> Index (Succ m) -> Bool)
-> Compare Bool (Succ m)
forall a b. (a -> b) -> a -> b
$ \Index (Succ m)
i Index (Succ m)
j ->
            case (Index (Succ m) -> Succ (Index m)
forall n. Index (Succ n) -> Succ (Index n)
unpackSucc Index (Succ m)
i, Index (Succ m) -> Succ (Index m)
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 Index m -> Index m -> Bool
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 =
      Compare Ordering n -> Index n -> Index n -> Ordering
forall a n. Compare a n -> Index n -> Index n -> a
runCompare (Compare Ordering n -> Index n -> Index n -> Ordering)
-> Compare Ordering n -> Index n -> Index n -> Ordering
forall a b. (a -> b) -> a -> b
$
      Compare Ordering Zero
-> (forall m. Natural m => Compare Ordering (Succ m))
-> Compare Ordering n
forall n (f :: * -> *).
Natural n =>
f Zero -> (forall m. Natural m => f (Succ m)) -> f n
switchNat
         ((Index Zero -> Index Zero -> Ordering) -> Compare Ordering Zero
forall a n. (Index n -> Index n -> a) -> Compare a n
Compare ((Index Zero -> Index Zero -> Ordering) -> Compare Ordering Zero)
-> (Index Zero -> Index Zero -> Ordering) -> Compare Ordering Zero
forall a b. (a -> b) -> a -> b
$ \Index Zero
_ Index Zero
_ -> String -> Ordering
forall a. HasCallStack => String -> a
error String
"compareIndex")
         ((Index (Succ m) -> Index (Succ m) -> Ordering)
-> Compare Ordering (Succ m)
forall a n. (Index n -> Index n -> a) -> Compare a n
Compare ((Index (Succ m) -> Index (Succ m) -> Ordering)
 -> Compare Ordering (Succ m))
-> (Index (Succ m) -> Index (Succ m) -> Ordering)
-> Compare Ordering (Succ m)
forall a b. (a -> b) -> a -> b
$ \Index (Succ m)
i Index (Succ m)
j ->
            case (Index (Succ m) -> Succ (Index m)
forall n. Index (Succ n) -> Succ (Index n)
unpackSucc Index (Succ m)
i, Index (Succ m) -> Succ (Index m)
forall n. Index (Succ n) -> Succ (Index n)
unpackSucc Index (Succ m)
j) of
               (Succ Index m
k, Succ Index m
l) -> Index m -> Index m -> Ordering
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 :: Index n -> Index (Succ n)
succ (Index Position n
n) = Position (Succ n) -> Index (Succ n)
forall n. Position n -> Index n
Index (Position n -> Succ (Position n)
forall pos. pos -> Succ pos
Succ Position n
n)

i0 :: Index (GE1 n); i0 :: Index (GE1 n)
i0 = Position (GE1 n) -> Index (GE1 n)
forall n. Position n -> Index n
Index Position (GE1 n)
forall pos. Succ pos
Stop
i1 :: Index (GE2 n); i1 :: Index (GE2 n)
i1 = Index (GE1 n) -> Index (GE2 n)
forall n. Index n -> Index (Succ n)
succ Index (GE1 n)
forall n. Index (GE1 n)
i0
i2 :: Index (GE3 n); i2 :: Index (GE3 n)
i2 = Index (GE2 n) -> Index (GE3 n)
forall n. Index n -> Index (Succ n)
succ Index (GE2 n)
forall n. Index (GE2 n)
i1
i3 :: Index (GE4 n); i3 :: Index (GE4 n)
i3 = Index (GE3 n) -> Index (GE4 n)
forall n. Index n -> Index (Succ n)
succ Index (GE3 n)
forall n. Index (GE3 n)
i2
i4 :: Index (GE5 n); i4 :: Index (GE5 n)
i4 = Index (GE4 n) -> Index (GE5 n)
forall n. Index n -> Index (Succ n)
succ Index (GE4 n)
forall n. Index (GE4 n)
i3
i5 :: Index (GE6 n); i5 :: Index (GE6 n)
i5 = Index (GE5 n) -> Index (GE6 n)
forall n. Index n -> Index (Succ n)
succ Index (GE5 n)
forall n. Index (GE5 n)
i4
i6 :: Index (GE7 n); i6 :: Index (GE7 n)
i6 = Index (GE6 n) -> Index (GE7 n)
forall n. Index n -> Index (Succ n)
succ Index (GE6 n)
forall n. Index (GE6 n)
i5
i7 :: Index (GE8 n); i7 :: Index (GE8 n)
i7 = Index (GE7 n) -> Index (GE8 n)
forall n. Index n -> Index (Succ n)
succ Index (GE7 n)
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 {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 :: (T n a -> b) -> Curried n a b
curry =
   Curry a b n -> (T n a -> b) -> Curried n a b
forall a b n. Curry a b n -> (T n a -> b) -> Curried n a b
runCurry (Curry a b n -> (T n a -> b) -> Curried n a b)
-> Curry a b n -> (T n a -> b) -> Curried n a b
forall a b. (a -> b) -> a -> b
$
   Curry a b Zero
-> (forall m. Natural m => Curry a b (Succ m)) -> Curry a b n
forall n (f :: * -> *).
Natural n =>
f Zero -> (forall m. Natural m => f (Succ m)) -> f n
Unary.switchNat
      (((T Zero a -> b) -> Curried Zero a b) -> Curry a b Zero
forall a b n. ((T n a -> b) -> Curried n a b) -> Curry a b n
Curry (((T Zero a -> b) -> Curried Zero a b) -> Curry a b Zero)
-> ((T Zero a -> b) -> Curried Zero a b) -> Curry a b Zero
forall a b. (a -> b) -> a -> b
$ ((T Zero a -> b) -> T Zero a -> b
forall a b. (a -> b) -> a -> b
$T Zero a
forall a. T Zero a
end))
      (((T (Succ m) a -> b) -> Curried (Succ m) a b) -> Curry a b (Succ m)
forall a b n. ((T n a -> b) -> Curried n a b) -> Curry a b n
Curry (((T (Succ m) a -> b) -> Curried (Succ m) a b)
 -> Curry a b (Succ m))
-> ((T (Succ m) a -> b) -> Curried (Succ m) a b)
-> Curry a b (Succ m)
forall a b. (a -> b) -> a -> b
$ \T (Succ m) a -> b
f a
a -> (T m a -> b) -> Curried m a b
forall n a b. Natural n => (T n a -> b) -> Curried n a b
curry ((T m a -> b) -> Curried m a b) -> (T m a -> b) -> Curried m a b
forall a b. (a -> b) -> a -> b
$ \T m a
xs -> T (Succ m) a -> b
f (a
aa -> T m a -> T (Succ m) a
forall a n. a -> T n a -> T (Succ n) a
!:T m a
xs))

newtype Uncurry a b n = Uncurry {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 :: Curried n a b -> T n a -> b
uncurry =
   Uncurry a b n -> Curried n a b -> T n a -> b
forall a b n. Uncurry a b n -> Curried n a b -> T n a -> b
runUncurry (Uncurry a b n -> Curried n a b -> T n a -> b)
-> Uncurry a b n -> Curried n a b -> T n a -> b
forall a b. (a -> b) -> a -> b
$
   Uncurry a b Zero
-> (forall m. Natural m => Uncurry a b (Succ m)) -> Uncurry a b n
forall n (f :: * -> *).
Natural n =>
f Zero -> (forall m. Natural m => f (Succ m)) -> f n
Unary.switchNat
      ((Curried Zero a b -> T Zero a -> b) -> Uncurry a b Zero
forall a b n. (Curried n a b -> T n a -> b) -> Uncurry a b n
Uncurry Curried Zero a b -> T Zero a -> b
forall b a. b -> T Zero a -> b
switchEnd)
      ((Curried (Succ m) a b -> T (Succ m) a -> b) -> Uncurry a b (Succ m)
forall a b n. (Curried n a b -> T n a -> b) -> Uncurry a b n
Uncurry ((Curried (Succ m) a b -> T (Succ m) a -> b)
 -> Uncurry a b (Succ m))
-> (Curried (Succ m) a b -> T (Succ m) a -> b)
-> Uncurry a b (Succ m)
forall a b. (a -> b) -> a -> b
$ \Curried (Succ m) a b
f -> (a -> T m a -> b) -> T (Succ m) a -> b
forall a n b. (a -> T n a -> b) -> T (Succ n) a -> b
switchL (\a
x -> Curried m a b -> T m a -> b
forall n a b. Natural n => Curried n a b -> T n a -> b
uncurry (Curried (Succ m) a b
a -> Curried 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 :: (T m a -> T n a) -> T n a
consAux T m a -> T n a
f = T m a -> T n a
f T m a
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 :: (T m a -> T n a) -> a -> f
consAux T m a -> T n a
f a
x = (T (NumberOfArguments f) a -> T n a) -> f
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 (T m a -> T n a)
-> (T (NumberOfArguments f) a -> T m a)
-> T (NumberOfArguments f) a
-> T n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a
a
xa -> T (NumberOfArguments f) a -> T (Succ (NumberOfArguments f)) a
forall a n. a -> T n a -> T (Succ n) a
!:))

consAll ::
   (ConsAll f, ResultSize f ~ n, NumberOfArguments f ~ n, Natural n) => f
consAll :: f
consAll = (T n (ResultElement f) -> T n (ResultElement f)) -> f
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 n (ResultElement f) -> T n (ResultElement f)
forall a. a -> a
P.id


undefinedElem :: T n a -> a
undefinedElem :: T n a -> a
undefinedElem T n a
_ = String -> 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 = Int -> a -> Int
forall a. Storable a => Int -> a -> Int
StoreArray.sizeOfArray ([a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
P.length ([a] -> Int) -> [a] -> Int
forall a b. (a -> b) -> a -> b
$ T n a -> [a]
forall n a. Natural n => T n a -> [a]
toList T n a
xs) (T n a -> a
forall n a. T n a -> a
undefinedElem T n a
xs)
   alignment :: T n a -> Int
alignment = a -> Int
forall a. Storable a => a -> Int
alignment (a -> Int) -> (T n a -> a) -> T n a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T n a -> a
forall n a. T n a -> a
undefinedElem
   peek :: Ptr (T n a) -> IO (T n a)
peek = Ptr (T n a) -> IO (T n a)
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 = Ptr (T n a) -> T n a -> IO ()
forall (f :: * -> *) a.
(Foldable f, Storable a) =>
Ptr (f a) -> f a -> IO ()
StoreTrav.poke