{-|
Description : A type-indexed parameterized list
Copyright   : (c) Galois, Inc 2017-2019
Maintainer  : Joe Hendrix <jhendrix@galois.com>

This module defines a list over two parameters.  The first
is a fixed type-level function @k -> *@ for some kind @k@, and the
second is a list of types with kind @k@ that provide the indices for
the values in the list.

This type is closely related to the
'Data.Parameterized.Context.Assignment' type in
"Data.Parameterized.Context".

= Motivating example - the 'Data.Parameterized.List.List' type

For this example, we need the following extensions:

@
\{\-\# LANGUAGE DataKinds \#\-\}
\{\-\# LANGUAGE GADTs \#\-\}
\{\-\# LANGUAGE KindSignatures \#\-\}
\{\-\# LANGUAGE TypeOperators \#\-\}
@

We also require the following imports:

@
import Data.Parameterized
import Data.Parameterized.List
import GHC.TypeLits
@

Suppose we have a bitvector type:

@
data BitVector (w :: Nat) :: * where
  BV :: NatRepr w -> Integer -> BitVector w
@

This type contains a 'Data.Parameterized.NatRepr.NatRepr', a value-level
representative of the vector width, and an 'Integer', containing the
actual value of the bitvector. We can create values of this type as
follows:

@
BV (knownNat @8) 0xAB
@

We can also create a smart constructor to handle the
'Data.Parameterized.NatRepr.NatRepr' automatically, when the width is known
from the type context:

@
bitVector :: KnownNat w => Integer -> BitVector w
bitVector x = BV knownNat x
@

Note that this does not check that the value can be represented in the
given number of bits; that is not important for this example.

If we wish to construct a list of @BitVector@s of a particular length,
we can do:

@
[bitVector 0xAB, bitVector 0xFF, bitVector 0] :: BitVector 8
@

However, what if we wish to construct a list of 'BitVector's of
different lengths? We could try:

@
[bitVector 0xAB :: BitVector 8, bitVector 0x1234 :: BitVector 16]
@

However, this gives us an error:

@
\<interactive\>:3:33: error:
    • Couldn't match type ‘16’ with ‘8’
      Expected type: BitVector 8
        Actual type: BitVector 16
    • In the expression: bitVector 0x1234 :: BitVector 16
      In the expression:
        [bitVector 0xAB :: BitVector 8, bitVector 0x1234 :: BitVector 16]
      In an equation for ‘it’:
          it
            = [bitVector 0xAB :: BitVector 8, bitVector 0x1234 :: BitVector 16]
@

A vanilla Haskell list cannot contain two elements of different types,
and even though the two elements here are both @BitVector@s, they do
not have the same type! One solution is to use the
'Data.Parameterized.Some.Some' type:

@
[Some (bitVector 0xAB :: BitVector 8), Some (bitVector 0x1234 :: BitVector 16)]
@

The type of the above expression is @[Some BitVector]@, which may be
perfectly acceptable. However, there is nothing in this type that
tells us what the widths of the bitvectors are, or what the length of
the overall list is. If we want to actually track that information on
the type level, we can use the 'List' type from this module.

@
(bitVector 0xAB :: BitVector 8) :< (bitVector 0x1234 :: BitVector 16) :< Nil
@

The type of the above expression is @List BitVector '[8, 16]@ -- That
is, a two-element list of @BitVector@s, where the first element has
width 8 and the second has width 16.

== Summary

In general, if we have a type constructor @Foo@ of kind @k -> *@ (in
our example, @Foo@ is just @BitVector@, and we want to create a list
of @Foo@s where the parameter @k@ varies, /and/ we wish to keep track
of what each value of @k@ is inside the list at compile time, we can
use the 'Data.Parameterized.List.List' type for this purpose.

-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Data.Parameterized.List
  ( List(..)
  , fromSomeList
  , fromListWith
  , fromListWithM
  , Index(..)
  , indexValue
  , (!!)
  , update
  , indexed
  , imap
  , ifoldlM
  , ifoldr
  , izipWith
  , itraverse
    -- * Constants
  , index0
  , index1
  , index2
  , index3
  ) where

import qualified Control.Lens as Lens
import           Data.Foldable
import           Data.Kind
import           Prelude hiding ((!!))
import           Unsafe.Coerce (unsafeCoerce)

import           Data.Parameterized.Classes
import           Data.Parameterized.Some
import           Data.Parameterized.TraversableFC
import           Data.Parameterized.TraversableFC.WithIndex

-- | Parameterized list of elements.
data List :: (k -> Type) -> [k] -> Type where
  Nil  :: List f '[]
  (:<) :: f tp -> List f tps -> List f (tp : tps)

infixr 5 :<

instance ShowF f => Show (List f sh) where
  showsPrec :: Int -> List f sh -> ShowS
showsPrec Int
_ List f sh
Nil = String -> ShowS
showString String
"Nil"
  showsPrec Int
p (f tp
elt :< List f tps
rest) = Bool -> ShowS -> ShowS
showParen (Int
p forall a. Ord a => a -> a -> Bool
> Int
precCons) forall a b. (a -> b) -> a -> b
$
    -- Unlike a derived 'Show' instance, we don't print parens implied
    -- by right associativity.
    forall k (f :: k -> *) (tp :: k). ShowF f => Int -> f tp -> ShowS
showsPrecF (Int
precConsforall a. Num a => a -> a -> a
+Int
1) f tp
elt forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" :< " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => Int -> a -> ShowS
showsPrec Int
0 List f tps
rest
    where
      precCons :: Int
precCons = Int
5

instance ShowF f => ShowF (List f)

instance FunctorFC List where
  fmapFC :: forall (f :: k -> *) (g :: k -> *).
(forall (x :: k). f x -> g x)
-> forall (x :: [k]). List f x -> List g x
fmapFC forall (x :: k). f x -> g x
_ List f x
Nil = forall {k} (f :: k -> *). List f '[]
Nil
  fmapFC forall (x :: k). f x -> g x
f (f tp
x :< List f tps
xs) = forall (x :: k). f x -> g x
f f tp
x forall {k} (f :: k -> *) (r :: k) (x :: [k]).
f r -> List f x -> List f (r : x)
:< forall k l (t :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
fmapFC forall (x :: k). f x -> g x
f List f tps
xs

instance FoldableFC List where
  foldrFC :: forall (f :: k -> *) b.
(forall (x :: k). f x -> b -> b)
-> forall (x :: [k]). b -> List f x -> b
foldrFC forall (x :: k). f x -> b -> b
_ b
z List f x
Nil = b
z
  foldrFC forall (x :: k). f x -> b -> b
f b
z (f tp
x :< List f tps
xs) = forall (x :: k). f x -> b -> b
f f tp
x (forall k l (t :: (k -> *) -> l -> *) (f :: k -> *) b.
FoldableFC t =>
(forall (x :: k). f x -> b -> b)
-> forall (x :: l). b -> t f x -> b
foldrFC forall (x :: k). f x -> b -> b
f b
z List f tps
xs)

instance TraversableFC List where
  traverseFC :: forall (f :: k -> *) (g :: k -> *) (m :: * -> *).
Applicative m =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: [k]). List f x -> m (List g x)
traverseFC forall (x :: k). f x -> m (g x)
_ List f x
Nil = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall {k} (f :: k -> *). List f '[]
Nil
  traverseFC forall (x :: k). f x -> m (g x)
f (f tp
h :< List f tps
r) = forall {k} (f :: k -> *) (r :: k) (x :: [k]).
f r -> List f x -> List f (r : x)
(:<) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (x :: k). f x -> m (g x)
f f tp
h forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall k l (t :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *)
       (m :: * -> *).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
traverseFC forall (x :: k). f x -> m (g x)
f List f tps
r

type instance IndexF   (List (f :: k -> Type) sh) = Index sh
type instance IxValueF (List (f :: k -> Type) sh) = f

instance FunctorFCWithIndex List where
  imapFC :: forall (f :: k -> *) (g :: k -> *) (z :: [k]).
(forall (x :: k). IndexF (List f z) x -> f x -> g x)
-> List f z -> List g z
imapFC = forall {k} (f :: k -> *) (g :: k -> *) (l :: [k]).
(forall (x :: k). Index l x -> f x -> g x) -> List f l -> List g l
imap

instance FoldableFCWithIndex List where
  ifoldrFC :: forall (z :: [k]) (f :: k -> *) b.
(forall (x :: k). IndexF (List f z) x -> f x -> b -> b)
-> b -> List f z -> b
ifoldrFC = forall {k} (sh :: [k]) (a :: k -> *) b.
(forall (tp :: k). Index sh tp -> a tp -> b -> b)
-> b -> List a sh -> b
ifoldr

instance TraversableFCWithIndex List where
  itraverseFC :: forall (m :: * -> *) (z :: [k]) (f :: k -> *) (g :: k -> *).
Applicative m =>
(forall (x :: k). IndexF (List f z) x -> f x -> m (g x))
-> List f z -> m (List g z)
itraverseFC = forall {k} (a :: k -> *) (b :: k -> *) (sh :: [k]) (t :: * -> *).
Applicative t =>
(forall (tp :: k). Index sh tp -> a tp -> t (b tp))
-> List a sh -> t (List b sh)
itraverse

instance TestEquality f => TestEquality (List f) where
  testEquality :: forall (a :: [k]) (b :: [k]).
List f a -> List f b -> Maybe (a :~: b)
testEquality List f a
Nil List f b
Nil = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
  testEquality (f tp
xh :< List f tps
xl) (f tp
yh :< List f tps
yl) = do
    tp :~: tp
Refl <- forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality f tp
xh f tp
yh
    tps :~: tps
Refl <- forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality List f tps
xl List f tps
yl
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall {k} (a :: k). a :~: a
Refl
  testEquality List f a
_ List f b
_ = forall a. Maybe a
Nothing

instance OrdF f => OrdF (List f) where
  compareF :: forall (x :: [k]) (y :: [k]). List f x -> List f y -> OrderingF x y
compareF List f x
Nil List f y
Nil = forall {k} (x :: k). OrderingF x x
EQF
  compareF List f x
Nil List f y
_ = forall {k} (x :: k) (y :: k). OrderingF x y
LTF
  compareF List f x
_ List f y
Nil = forall {k} (x :: k) (y :: k). OrderingF x y
GTF
  compareF (f tp
xh :< List f tps
xl) (f tp
yh :< List f tps
yl) =
    forall j k (f :: j -> *) (a :: j) (b :: j) (c :: k) (d :: k).
OrdF f =>
f a -> f b -> ((a ~ b) => OrderingF c d) -> OrderingF c d
lexCompareF f tp
xh f tp
yh forall a b. (a -> b) -> a -> b
$
    forall j k (f :: j -> *) (a :: j) (b :: j) (c :: k) (d :: k).
OrdF f =>
f a -> f b -> ((a ~ b) => OrderingF c d) -> OrderingF c d
lexCompareF List f tps
xl List f tps
yl forall a b. (a -> b) -> a -> b
$
    forall {k} (x :: k). OrderingF x x
EQF

instance KnownRepr (List f) '[] where
  knownRepr :: List f '[]
knownRepr = forall {k} (f :: k -> *). List f '[]
Nil

instance (KnownRepr f s, KnownRepr (List f) sh) => KnownRepr (List f) (s ': sh) where
  knownRepr :: List f (s : sh)
knownRepr = forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall {k} (f :: k -> *) (r :: k) (x :: [k]).
f r -> List f x -> List f (r : x)
:< forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

-- | Apply function to list to yield a parameterized list.
fromListWith :: forall a f . (a -> Some f) -> [a] -> Some (List f)
fromListWith :: forall {k} a (f :: k -> *). (a -> Some f) -> [a] -> Some (List f)
fromListWith a -> Some f
f = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr a -> Some (List f) -> Some (List f)
g (forall k (f :: k -> *) (x :: k). f x -> Some f
Some forall {k} (f :: k -> *). List f '[]
Nil)
  where g :: a -> Some (List f) -> Some (List f)
        g :: a -> Some (List f) -> Some (List f)
g a
x (Some List f x
r) = forall {k} (f :: k -> *) r.
(forall (tp :: k). f tp -> r) -> Some f -> r
viewSome (\f tp
h -> forall k (f :: k -> *) (x :: k). f x -> Some f
Some (f tp
h forall {k} (f :: k -> *) (r :: k) (x :: [k]).
f r -> List f x -> List f (r : x)
:< List f x
r)) (a -> Some f
f a
x)

-- | Apply monadic action to list to yield a parameterized list.
fromListWithM :: forall a f m
                  .  Monad m
                  => (a -> m (Some f))
                  -> [a]
                  -> m (Some (List f))
fromListWithM :: forall {k} a (f :: k -> *) (m :: * -> *).
Monad m =>
(a -> m (Some f)) -> [a] -> m (Some (List f))
fromListWithM a -> m (Some f)
f = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> b -> m b) -> b -> t a -> m b
foldrM a -> Some (List f) -> m (Some (List f))
g (forall k (f :: k -> *) (x :: k). f x -> Some f
Some forall {k} (f :: k -> *). List f '[]
Nil)
  where g :: a -> Some (List f) -> m (Some (List f))
        g :: a -> Some (List f) -> m (Some (List f))
g a
x (Some List f x
r) = forall {k} (f :: k -> *) r.
(forall (tp :: k). f tp -> r) -> Some f -> r
viewSome (\f tp
h -> forall k (f :: k -> *) (x :: k). f x -> Some f
Some (f tp
h forall {k} (f :: k -> *) (r :: k) (x :: [k]).
f r -> List f x -> List f (r : x)
:< List f x
r)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m (Some f)
f a
x

-- | Map from list of Some to Some list
fromSomeList :: [Some f] -> Some (List f)
fromSomeList :: forall {k} (f :: k -> *). [Some f] -> Some (List f)
fromSomeList = forall {k} a (f :: k -> *). (a -> Some f) -> [a] -> Some (List f)
fromListWith forall a. a -> a
id

{-# INLINABLE fromListWith #-}
{-# INLINABLE fromListWithM #-}

--------------------------------------------------------------------------------
-- * Indexed operations

-- | Represents an index into a type-level list. Used in place of integers to
--   1. ensure that the given index *does* exist in the list
--   2. guarantee that it has the given kind
data Index :: [k] -> k -> Type  where
  IndexHere :: Index (x:r) x
  IndexThere :: !(Index r y) -> Index (x:r) y

deriving instance Eq (Index l x)
deriving instance Show  (Index l x)

instance ShowF (Index l)

instance TestEquality (Index l) where
  testEquality :: forall (a :: k) (b :: k). Index l a -> Index l b -> Maybe (a :~: b)
testEquality Index l a
IndexHere Index l b
IndexHere = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
  testEquality (IndexThere Index r a
x) (IndexThere Index r b
y) = forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Index r a
x Index r b
y
  testEquality Index l a
_ Index l b
_ = forall a. Maybe a
Nothing

instance OrdF (Index l) where
  compareF :: forall (x :: k) (y :: k). Index l x -> Index l y -> OrderingF x y
compareF Index l x
IndexHere Index l y
IndexHere = forall {k} (x :: k). OrderingF x x
EQF
  compareF Index l x
IndexHere IndexThere{} = forall {k} (x :: k) (y :: k). OrderingF x y
LTF
  compareF IndexThere{} Index l y
IndexHere = forall {k} (x :: k) (y :: k). OrderingF x y
GTF
  compareF (IndexThere Index r x
x) (IndexThere Index r y
y) = forall k (ktp :: k -> *) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
compareF Index r x
x Index r y
y

instance Ord (Index sh x) where
  Index sh x
x compare :: Index sh x -> Index sh x -> Ordering
`compare` Index sh x
y = forall {k} (x :: k) (y :: k). OrderingF x y -> Ordering
toOrdering forall a b. (a -> b) -> a -> b
$ Index sh x
x forall k (ktp :: k -> *) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
`compareF` Index sh x
y

-- | Return the index as an integer.
indexValue :: Index l tp -> Integer
indexValue :: forall {k} (l :: [k]) (tp :: k). Index l tp -> Integer
indexValue = forall {k} (l :: [k]) (tp :: k). Integer -> Index l tp -> Integer
go Integer
0
  where go :: Integer -> Index l tp -> Integer
        go :: forall {k} (l :: [k]) (tp :: k). Integer -> Index l tp -> Integer
go Integer
i Index l tp
IndexHere = Integer
i
        go Integer
i (IndexThere Index r tp
x) = seq :: forall a b. a -> b -> b
seq Integer
j forall a b. (a -> b) -> a -> b
$ forall {k} (l :: [k]) (tp :: k). Integer -> Index l tp -> Integer
go Integer
j Index r tp
x
          where j :: Integer
j = Integer
iforall a. Num a => a -> a -> a
+Integer
1

instance Hashable (Index l x) where
  hashWithSalt :: Int -> Index l x -> Int
hashWithSalt Int
s Index l x
i = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (forall {k} (l :: [k]) (tp :: k). Index l tp -> Integer
indexValue Index l x
i)

-- | Index 0
index0 :: Index (x:r) x
index0 :: forall {k} (x :: k) (r :: [k]). Index (x : r) x
index0 = forall {k} (x :: k) (r :: [k]). Index (x : r) x
IndexHere

-- | Index 1
index1 :: Index (x0:x1:r) x1
index1 :: forall {k} (x0 :: k) (x1 :: k) (r :: [k]). Index (x0 : x1 : r) x1
index1 = forall {k} (r :: [k]) (y :: k) (x :: k).
Index r y -> Index (x : r) y
IndexThere forall {k} (x :: k) (r :: [k]). Index (x : r) x
index0

-- | Index 2
index2 :: Index (x0:x1:x2:r) x2
index2 :: forall {k} (x0 :: k) (x1 :: k) (x2 :: k) (r :: [k]).
Index (x0 : x1 : x2 : r) x2
index2 = forall {k} (r :: [k]) (y :: k) (x :: k).
Index r y -> Index (x : r) y
IndexThere forall {k} (x0 :: k) (x1 :: k) (r :: [k]). Index (x0 : x1 : r) x1
index1

-- | Index 3
index3 :: Index (x0:x1:x2:x3:r) x3
index3 :: forall {k} (x0 :: k) (x1 :: k) (x2 :: k) (x3 :: k) (r :: [k]).
Index (x0 : x1 : x2 : x3 : r) x3
index3 = forall {k} (r :: [k]) (y :: k) (x :: k).
Index r y -> Index (x : r) y
IndexThere forall {k} (x0 :: k) (x1 :: k) (x2 :: k) (r :: [k]).
Index (x0 : x1 : x2 : r) x2
index2

-- | Return the value in a list at a given index
(!!) :: List f l -> Index l x -> f x
List f l
l !! :: forall {k} (f :: k -> *) (l :: [k]) (x :: k).
List f l -> Index l x -> f x
!! (IndexThere Index r x
i) =
  case List f l
l of
    f tp
_ :< List f tps
r -> List f tps
r forall {k} (f :: k -> *) (l :: [k]) (x :: k).
List f l -> Index l x -> f x
!! Index r x
i
List f l
l !! Index l x
IndexHere =
  case List f l
l of
    (f tp
h :< List f tps
_) -> f tp
h

-- | Update the 'List' at an index
update :: List f l -> Index l s -> (f s -> f s) -> List f l
update :: forall {k} (f :: k -> *) (l :: [k]) (s :: k).
List f l -> Index l s -> (f s -> f s) -> List f l
update List f l
vals Index l s
IndexHere f s -> f s
upd =
  case List f l
vals of
    f tp
x :< List f tps
rest -> f s -> f s
upd f tp
x forall {k} (f :: k -> *) (r :: k) (x :: [k]).
f r -> List f x -> List f (r : x)
:< List f tps
rest
update List f l
vals (IndexThere Index r s
th) f s -> f s
upd =
  case List f l
vals of
    f tp
x :< List f tps
rest -> f tp
x forall {k} (f :: k -> *) (r :: k) (x :: [k]).
f r -> List f x -> List f (r : x)
:< forall {k} (f :: k -> *) (l :: [k]) (s :: k).
List f l -> Index l s -> (f s -> f s) -> List f l
update List f tps
rest Index r s
th f s -> f s
upd

-- | Provides a lens for manipulating the element at the given index.
indexed :: Index l x -> Lens.Lens' (List f l) (f x)
indexed :: forall {k} (l :: [k]) (x :: k) (f :: k -> *).
Index l x -> Lens' (List f l) (f x)
indexed Index l x
IndexHere      f x -> f (f x)
f (f tp
x :< List f tps
rest) = (forall {k} (f :: k -> *) (r :: k) (x :: [k]).
f r -> List f x -> List f (r : x)
:< List f tps
rest) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f x -> f (f x)
f f tp
x
indexed (IndexThere Index r x
i) f x -> f (f x)
f (f tp
x :< List f tps
rest) = (f tp
x forall {k} (f :: k -> *) (r :: k) (x :: [k]).
f r -> List f x -> List f (r : x)
:<) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {k} (l :: [k]) (x :: k) (f :: k -> *).
Index l x -> Lens' (List f l) (f x)
indexed Index r x
i f x -> f (f x)
f List f tps
rest

--------------------------------------------------------------------------------
-- Indexed operations

-- | Map over the elements in the list, and provide the index into
-- each element along with the element itself.
--
-- This is a specialization of 'imapFC'.
imap :: forall f g l
     . (forall x . Index l x -> f x -> g x)
     -> List f l
     -> List g l
imap :: forall {k} (f :: k -> *) (g :: k -> *) (l :: [k]).
(forall (x :: k). Index l x -> f x -> g x) -> List f l -> List g l
imap forall (x :: k). Index l x -> f x -> g x
f = forall (l' :: [k]).
(forall (tp :: k). Index l' tp -> Index l tp)
-> List f l' -> List g l'
go forall a. a -> a
id
  where
    go :: forall l'
        . (forall tp . Index l' tp -> Index l tp)
       -> List f l'
       -> List g l'
    go :: forall (l' :: [k]).
(forall (tp :: k). Index l' tp -> Index l tp)
-> List f l' -> List g l'
go forall (tp :: k). Index l' tp -> Index l tp
g List f l'
l =
      case List f l'
l of
        List f l'
Nil -> forall {k} (f :: k -> *). List f '[]
Nil
        f tp
e :< List f tps
rest -> forall (x :: k). Index l x -> f x -> g x
f (forall (tp :: k). Index l' tp -> Index l tp
g forall {k} (x :: k) (r :: [k]). Index (x : r) x
IndexHere) f tp
e forall {k} (f :: k -> *) (r :: k) (x :: [k]).
f r -> List f x -> List f (r : x)
:< forall (l' :: [k]).
(forall (tp :: k). Index l' tp -> Index l tp)
-> List f l' -> List g l'
go (forall (tp :: k). Index l' tp -> Index l tp
g forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (r :: [k]) (y :: k) (x :: k).
Index r y -> Index (x : r) y
IndexThere) List f tps
rest

-- | Left fold with an additional index.
ifoldlM :: forall sh a b m
        . Monad m
        => (forall tp . b -> Index sh tp -> a tp -> m b)
        -> b
        -> List a sh
        -> m b
ifoldlM :: forall {k} (sh :: [k]) (a :: k -> *) b (m :: * -> *).
Monad m =>
(forall (tp :: k). b -> Index sh tp -> a tp -> m b)
-> b -> List a sh -> m b
ifoldlM forall (tp :: k). b -> Index sh tp -> a tp -> m b
_ b
b List a sh
Nil = forall (f :: * -> *) a. Applicative f => a -> f a
pure b
b
ifoldlM forall (tp :: k). b -> Index sh tp -> a tp -> m b
f b
b0 (a tp
a0 :< List a tps
r0) = forall (tp :: k). b -> Index sh tp -> a tp -> m b
f b
b0 forall {k} (x :: k) (r :: [k]). Index (x : r) x
IndexHere a tp
a0 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (tps :: [k]) (tp :: k).
Index sh tp -> List a tps -> b -> m b
go forall {k} (x :: k) (r :: [k]). Index (x : r) x
IndexHere List a tps
r0
  where
    go :: forall tps tp
        . Index sh tp
       -> List a tps
       -> b
       -> m b
    go :: forall (tps :: [k]) (tp :: k).
Index sh tp -> List a tps -> b -> m b
go Index sh tp
_ List a tps
Nil b
b = forall (f :: * -> *) a. Applicative f => a -> f a
pure b
b
    go Index sh tp
idx (a tp
a :< List a tps
rest) b
b =
      let idx' :: Index sh tp
idx' = forall a b. a -> b
unsafeCoerce (forall {k} (r :: [k]) (y :: k) (x :: k).
Index r y -> Index (x : r) y
IndexThere Index sh tp
idx)
       in forall (tp :: k). b -> Index sh tp -> a tp -> m b
f b
b Index sh tp
idx' a tp
a forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (tps :: [k]) (tp :: k).
Index sh tp -> List a tps -> b -> m b
go Index sh tp
idx' List a tps
rest

-- | Right-fold with an additional index.
--
-- This is a specialization of 'ifoldrFC'.
ifoldr :: forall sh a b . (forall tp . Index sh tp -> a tp -> b -> b) -> b -> List a sh -> b
ifoldr :: forall {k} (sh :: [k]) (a :: k -> *) b.
(forall (tp :: k). Index sh tp -> a tp -> b -> b)
-> b -> List a sh -> b
ifoldr forall (tp :: k). Index sh tp -> a tp -> b -> b
f b
seed0 List a sh
l = forall (tps :: [k]).
(forall (tp :: k). Index tps tp -> Index sh tp)
-> List a tps -> b -> b
go forall a. a -> a
id List a sh
l b
seed0
  where
    go :: forall tps
        . (forall tp . Index tps tp -> Index sh tp)
       -> List a tps
       -> b
       -> b
    go :: forall (tps :: [k]).
(forall (tp :: k). Index tps tp -> Index sh tp)
-> List a tps -> b -> b
go forall (tp :: k). Index tps tp -> Index sh tp
g List a tps
ops b
b =
      case List a tps
ops of
        List a tps
Nil -> b
b
        a tp
a :< List a tps
rest -> forall (tp :: k). Index sh tp -> a tp -> b -> b
f (forall (tp :: k). Index tps tp -> Index sh tp
g forall {k} (x :: k) (r :: [k]). Index (x : r) x
IndexHere) a tp
a (forall (tps :: [k]).
(forall (tp :: k). Index tps tp -> Index sh tp)
-> List a tps -> b -> b
go (\Index tps tp
ix -> forall (tp :: k). Index tps tp -> Index sh tp
g (forall {k} (r :: [k]) (y :: k) (x :: k).
Index r y -> Index (x : r) y
IndexThere Index tps tp
ix)) List a tps
rest b
b)

-- | Zip up two lists with a zipper function, which can use the index.
izipWith :: forall a b c sh . (forall tp. Index sh tp -> a tp -> b tp -> c tp)
         -> List a sh
         -> List b sh
         -> List c sh
izipWith :: forall {k} (a :: k -> *) (b :: k -> *) (c :: k -> *) (sh :: [k]).
(forall (tp :: k). Index sh tp -> a tp -> b tp -> c tp)
-> List a sh -> List b sh -> List c sh
izipWith forall (tp :: k). Index sh tp -> a tp -> b tp -> c tp
f = forall (sh' :: [k]).
(forall (tp :: k). Index sh' tp -> Index sh tp)
-> List a sh' -> List b sh' -> List c sh'
go forall a. a -> a
id
  where
    go :: forall sh' .
          (forall tp . Index sh' tp -> Index sh tp)
       -> List a sh'
       -> List b sh'
       -> List c sh'
    go :: forall (sh' :: [k]).
(forall (tp :: k). Index sh' tp -> Index sh tp)
-> List a sh' -> List b sh' -> List c sh'
go forall (tp :: k). Index sh' tp -> Index sh tp
g List a sh'
as List b sh'
bs =
      case (List a sh'
as, List b sh'
bs) of
        (List a sh'
Nil, List b sh'
Nil) -> forall {k} (f :: k -> *). List f '[]
Nil
        (a tp
a :< List a tps
as', b tp
b :< List b tps
bs') ->
          forall (tp :: k). Index sh tp -> a tp -> b tp -> c tp
f (forall (tp :: k). Index sh' tp -> Index sh tp
g forall {k} (x :: k) (r :: [k]). Index (x : r) x
IndexHere) a tp
a b tp
b forall {k} (f :: k -> *) (r :: k) (x :: [k]).
f r -> List f x -> List f (r : x)
:< forall (sh' :: [k]).
(forall (tp :: k). Index sh' tp -> Index sh tp)
-> List a sh' -> List b sh' -> List c sh'
go (forall (tp :: k). Index sh' tp -> Index sh tp
g forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (r :: [k]) (y :: k) (x :: k).
Index r y -> Index (x : r) y
IndexThere) List a tps
as' List b tps
bs'

-- | Traverse with an additional index.
--
-- This is a specialization of 'itraverseFC'.
itraverse :: forall a b sh t
          . Applicative t
          => (forall tp . Index sh tp -> a tp -> t (b tp))
          -> List a sh
          -> t (List b sh)
itraverse :: forall {k} (a :: k -> *) (b :: k -> *) (sh :: [k]) (t :: * -> *).
Applicative t =>
(forall (tp :: k). Index sh tp -> a tp -> t (b tp))
-> List a sh -> t (List b sh)
itraverse forall (tp :: k). Index sh tp -> a tp -> t (b tp)
f = forall (tps :: [k]).
(forall (tp :: k). Index tps tp -> Index sh tp)
-> List a tps -> t (List b tps)
go forall a. a -> a
id
  where
    go :: forall tps . (forall tp . Index tps tp -> Index sh tp)
       -> List a tps
       -> t (List b tps)
    go :: forall (tps :: [k]).
(forall (tp :: k). Index tps tp -> Index sh tp)
-> List a tps -> t (List b tps)
go forall (tp :: k). Index tps tp -> Index sh tp
g List a tps
l =
      case List a tps
l of
        List a tps
Nil -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall {k} (f :: k -> *). List f '[]
Nil
        a tp
e :< List a tps
rest -> forall {k} (f :: k -> *) (r :: k) (x :: [k]).
f r -> List f x -> List f (r : x)
(:<) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (tp :: k). Index sh tp -> a tp -> t (b tp)
f (forall (tp :: k). Index tps tp -> Index sh tp
g forall {k} (x :: k) (r :: [k]). Index (x : r) x
IndexHere) a tp
e forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (tps :: [k]).
(forall (tp :: k). Index tps tp -> Index sh tp)
-> List a tps -> t (List b tps)
go (\Index tps tp
ix -> forall (tp :: k). Index tps tp -> Index sh tp
g (forall {k} (r :: [k]) (y :: k) (x :: k).
Index r y -> Index (x : r) y
IndexThere Index tps tp
ix)) List a tps
rest