{-|
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 TypeOperators #-}
module Data.Parameterized.List
  ( List(..)
  , Index(..)
  , indexValue
  , (!!)
  , update
  , indexed
  , imap
  , ifoldr
  , izipWith
  , itraverse
    -- * Constants
  , index0
  , index1
  , index2
  , index3
  ) where

import qualified Control.Lens as Lens
import           Prelude hiding ((!!))

import           Data.Parameterized.Classes
import           Data.Parameterized.TraversableFC

-- | Parameterized list of elements.
data List :: (k -> *) -> [k] -> * 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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
precCons) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
    -- Unlike a derived 'Show' instance, we don't print parens implied
    -- by right associativity.
    Int -> f tp -> ShowS
forall k (f :: k -> *) (tp :: k). ShowF f => Int -> f tp -> ShowS
showsPrecF (Int
precConsInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) f tp
elt ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" :< " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> List f tps -> ShowS
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 (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 = List g x
forall k (f :: k -> *). List f '[]
Nil
  fmapFC forall (x :: k). f x -> g x
f (f tp
x :< List f tps
xs) = f tp -> g tp
forall (x :: k). f x -> g x
f f tp
x g tp -> List g tps -> List g (tp : tps)
forall a (f :: a -> *) (tp :: a) (tps :: [a]).
f tp -> List f tps -> List f (tp : tps)
:< (forall (x :: k). f x -> g x) -> List f tps -> List g tps
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 (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) = f tp -> b -> b
forall (x :: k). f x -> b -> b
f f tp
x ((forall (x :: k). f x -> b -> b) -> b -> List f tps -> b
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 (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 = List g '[] -> m (List g '[])
forall (f :: * -> *) a. Applicative f => a -> f a
pure List g '[]
forall k (f :: k -> *). List f '[]
Nil
  traverseFC forall (x :: k). f x -> m (g x)
f (f tp
h :< List f tps
r) = g tp -> List g tps -> List g (tp : tps)
forall a (f :: a -> *) (tp :: a) (tps :: [a]).
f tp -> List f tps -> List f (tp : tps)
(:<) (g tp -> List g tps -> List g (tp : tps))
-> m (g tp) -> m (List g tps -> List g (tp : tps))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f tp -> m (g tp)
forall (x :: k). f x -> m (g x)
f f tp
h m (List g tps -> List g (tp : tps))
-> m (List g tps) -> m (List g (tp : tps))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall (x :: k). f x -> m (g x)) -> List f tps -> m (List g tps)
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

instance TestEquality f => TestEquality (List f) where
  testEquality :: List f a -> List f b -> Maybe (a :~: b)
testEquality List f a
Nil List f b
Nil = (a :~: a) -> Maybe (a :~: a)
forall a. a -> Maybe a
Just a :~: a
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 <- f tp -> f tp -> Maybe (tp :~: tp)
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 <- List f tps -> List f tps -> Maybe (tps :~: tps)
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
    (a :~: a) -> Maybe (a :~: a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure a :~: a
forall k (a :: k). a :~: a
Refl
  testEquality List f a
_ List f b
_ = Maybe (a :~: b)
forall a. Maybe a
Nothing

instance OrdF f => OrdF (List f) where
  compareF :: List f x -> List f y -> OrderingF x y
compareF List f x
Nil List f y
Nil = OrderingF x y
forall k (x :: k). OrderingF x x
EQF
  compareF List f x
Nil List f y
_ = OrderingF x y
forall k (x :: k) (y :: k). OrderingF x y
LTF
  compareF List f x
_ List f y
Nil = OrderingF x y
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) =
    f tp -> f tp -> ((tp ~ tp) => OrderingF x y) -> OrderingF x y
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 (((tp ~ tp) => OrderingF x y) -> OrderingF x y)
-> ((tp ~ tp) => OrderingF x y) -> OrderingF x y
forall a b. (a -> b) -> a -> b
$
    List f tps
-> List f tps -> ((tps ~ tps) => OrderingF x y) -> OrderingF x y
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 (((tps ~ tps) => OrderingF x y) -> OrderingF x y)
-> ((tps ~ tps) => OrderingF x y) -> OrderingF x y
forall a b. (a -> b) -> a -> b
$
    (tps ~ tps) => OrderingF x y
forall k (x :: k). OrderingF x x
EQF


instance KnownRepr (List f) '[] where
  knownRepr :: List f '[]
knownRepr = List f '[]
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 = f s
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr f s -> List f sh -> List f (s : sh)
forall a (f :: a -> *) (tp :: a) (tps :: [a]).
f tp -> List f tps -> List f (tp : tps)
:< List f sh
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

--------------------------------------------------------------------------------
-- * 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 -> *  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 :: Index l a -> Index l b -> Maybe (a :~: b)
testEquality Index l a
IndexHere Index l b
IndexHere = (a :~: a) -> Maybe (a :~: a)
forall a. a -> Maybe a
Just a :~: a
forall k (a :: k). a :~: a
Refl
  testEquality (IndexThere Index r a
x) (IndexThere Index r b
y) = Index r a -> Index r b -> Maybe (a :~: b)
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
Index r b
y
  testEquality Index l a
_ Index l b
_ = Maybe (a :~: b)
forall a. Maybe a
Nothing

instance OrdF (Index l) where
  compareF :: Index l x -> Index l y -> OrderingF x y
compareF Index l x
IndexHere Index l y
IndexHere = OrderingF x y
forall k (x :: k). OrderingF x x
EQF
  compareF Index l x
IndexHere IndexThere{} = OrderingF x y
forall k (x :: k) (y :: k). OrderingF x y
LTF
  compareF IndexThere{} Index l y
IndexHere = OrderingF x y
forall k (x :: k) (y :: k). OrderingF x y
GTF
  compareF (IndexThere Index r x
x) (IndexThere Index r y
y) = Index r x -> Index r y -> OrderingF x 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
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 = OrderingF x x -> Ordering
forall k (x :: k) (y :: k). OrderingF x y -> Ordering
toOrdering (OrderingF x x -> Ordering) -> OrderingF x x -> Ordering
forall a b. (a -> b) -> a -> b
$ Index sh x
x Index sh x -> Index sh x -> OrderingF 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 :: Index l tp -> Integer
indexValue = Integer -> Index l tp -> Integer
forall k (l :: [k]) (tp :: k). Integer -> Index l tp -> Integer
go Integer
0
  where go :: Integer -> Index l tp -> Integer
        go :: Integer -> Index l tp -> Integer
go Integer
i Index l tp
IndexHere = Integer
i
        go Integer
i (IndexThere Index r tp
x) = Integer -> Integer -> Integer
seq Integer
j (Integer -> Integer) -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ Integer -> Index r tp -> Integer
forall k (l :: [k]) (tp :: k). Integer -> Index l tp -> Integer
go Integer
j Index r tp
x
          where j :: Integer
j = Integer
iInteger -> Integer -> Integer
forall 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 Int -> Integer -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Index l x -> Integer
forall k (l :: [k]) (tp :: k). Index l tp -> Integer
indexValue Index l x
i)

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

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

-- | Index 2
index2 :: Index (x0:x1:x2:r) x2
index2 :: Index (x0 : x1 : x2 : r) x2
index2 = Index (x1 : x2 : r) x2 -> Index (x0 : x1 : x2 : r) x2
forall k (r :: [k]) (y :: k) (x :: k). Index r y -> Index (x : r) y
IndexThere Index (x1 : x2 : r) x2
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 :: Index (x0 : x1 : x2 : x3 : r) x3
index3 = Index (x1 : x2 : x3 : r) x3 -> Index (x0 : x1 : x2 : x3 : r) x3
forall k (r :: [k]) (y :: k) (x :: k). Index r y -> Index (x : r) y
IndexThere Index (x1 : x2 : x3 : r) x3
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 !! :: 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 List f tps -> Index tps x -> f x
forall k (f :: k -> *) (l :: [k]) (x :: k).
List f l -> Index l x -> f x
!! Index r x
Index tps x
i
List f l
l !! Index l x
IndexHere =
  case List f l
l of
    (f tp
h :< List f tps
_) -> f x
f tp
h

-- | Update the 'List' at an index
update :: List f l -> Index l s -> (f s -> f s) -> List f l
update :: 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 s
f tp
x f s -> List f tps -> List f (s : tps)
forall a (f :: a -> *) (tp :: a) (tps :: [a]).
f tp -> List f tps -> List f (tp : tps)
:< 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 f tp -> List f tps -> List f (tp : tps)
forall a (f :: a -> *) (tp :: a) (tps :: [a]).
f tp -> List f tps -> List f (tp : tps)
:< List f tps -> Index tps s -> (f s -> f s) -> List f tps
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
Index tps 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 :: 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) = (f x -> List f tps -> List f (x : tps)
forall a (f :: a -> *) (tp :: a) (tps :: [a]).
f tp -> List f tps -> List f (tp : tps)
:< List f tps
rest) (f x -> List f (x : tps)) -> f (f x) -> f (List f (x : tps))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f x -> f (f x)
f f x
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 f tp -> List f r -> List f (tp : r)
forall a (f :: a -> *) (tp :: a) (tps :: [a]).
f tp -> List f tps -> List f (tp : tps)
:<) (List f r -> List f (tp : r))
-> f (List f r) -> f (List f (tp : r))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Index r x -> (f x -> f (f x)) -> List f r -> f (List f r)
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 r
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.
imap :: forall f g l
     . (forall x . Index l x -> f x -> g x)
     -> List f l
     -> List g l
imap :: (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 (tp :: k). Index l tp -> Index l tp)
-> List f l -> List g l
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
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 (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 -> List g l'
forall k (f :: k -> *). List f '[]
Nil
        f tp
e :< List f tps
rest -> Index l tp -> f tp -> g tp
forall (x :: k). Index l x -> f x -> g x
f (Index l' tp -> Index l tp
forall (tp :: k). Index l' tp -> Index l tp
g Index l' tp
forall k (x :: k) (r :: [k]). Index (x : r) x
IndexHere) f tp
e g tp -> List g tps -> List g (tp : tps)
forall a (f :: a -> *) (tp :: a) (tps :: [a]).
f tp -> List f tps -> List f (tp : tps)
:< (forall (tp :: k). Index tps tp -> Index l tp)
-> List f tps -> List g tps
forall (l' :: [k]).
(forall (tp :: k). Index l' tp -> Index l tp)
-> List f l' -> List g l'
go (Index l' tp -> Index l tp
forall (tp :: k). Index l' tp -> Index l tp
g (Index l' tp -> Index l tp)
-> (Index tps tp -> Index l' tp) -> Index tps tp -> Index l tp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index tps tp -> Index l' tp
forall k (r :: [k]) (y :: k) (x :: k). Index r y -> Index (x : r) y
IndexThere) List f tps
rest

-- | Right-fold with an additional index.
ifoldr :: forall sh a b . (forall tp . Index sh tp -> a tp -> b -> b) -> b -> List a sh -> b
ifoldr :: (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 (tp :: k). Index sh tp -> Index sh tp)
-> List a sh -> b -> b
forall (tps :: [k]).
(forall (tp :: k). Index tps tp -> Index sh tp)
-> List a tps -> b -> b
go forall (tp :: k). Index sh tp -> Index sh tp
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 (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 -> Index sh tp -> a tp -> b -> b
forall (tp :: k). Index sh tp -> a tp -> b -> b
f (Index tps tp -> Index sh tp
forall (tp :: k). Index tps tp -> Index sh tp
g Index tps tp
forall k (x :: k) (r :: [k]). Index (x : r) x
IndexHere) a tp
a ((forall (tp :: k). Index tps tp -> Index sh tp)
-> List a tps -> b -> b
forall (tps :: [k]).
(forall (tp :: k). Index tps tp -> Index sh tp)
-> List a tps -> b -> b
go (\Index tps tp
ix -> Index tps tp -> Index sh tp
forall (tp :: k). Index tps tp -> Index sh tp
g (Index tps tp -> Index (tp : tps) tp
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 (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 (tp :: k). Index sh tp -> Index sh tp)
-> List a sh -> List b sh -> List c sh
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
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 (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) -> List c sh'
forall k (f :: k -> *). List f '[]
Nil
        (a tp
a :< List a tps
as', b tp
b :< List b tps
bs') ->
          Index sh tp -> a tp -> b tp -> c tp
forall (tp :: k). Index sh tp -> a tp -> b tp -> c tp
f (Index sh' tp -> Index sh tp
forall (tp :: k). Index sh' tp -> Index sh tp
g Index sh' tp
forall k (x :: k) (r :: [k]). Index (x : r) x
IndexHere) a tp
a b tp
b tp
b c tp -> List c tps -> List c (tp : tps)
forall a (f :: a -> *) (tp :: a) (tps :: [a]).
f tp -> List f tps -> List f (tp : tps)
:< (forall (tp :: k). Index tps tp -> Index sh tp)
-> List a tps -> List b tps -> List c tps
forall (sh' :: [k]).
(forall (tp :: k). Index sh' tp -> Index sh tp)
-> List a sh' -> List b sh' -> List c sh'
go (Index sh' tp -> Index sh tp
forall (tp :: k). Index sh' tp -> Index sh tp
g (Index sh' tp -> Index sh tp)
-> (Index tps tp -> Index sh' tp) -> Index tps tp -> Index sh tp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index tps tp -> Index sh' tp
forall k (r :: [k]) (y :: k) (x :: k). Index r y -> Index (x : r) y
IndexThere) List a tps
as' List b tps
List b tps
bs'

-- | Traverse with an additional index.
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 (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 (tp :: k). Index sh tp -> Index sh tp)
-> List a sh -> t (List b sh)
forall (tps :: [k]).
(forall (tp :: k). Index tps tp -> Index sh tp)
-> List a tps -> t (List b tps)
go forall (tp :: k). Index sh tp -> Index sh tp
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 (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 -> List b '[] -> t (List b '[])
forall (f :: * -> *) a. Applicative f => a -> f a
pure List b '[]
forall k (f :: k -> *). List f '[]
Nil
        a tp
e :< List a tps
rest -> b tp -> List b tps -> List b (tp : tps)
forall a (f :: a -> *) (tp :: a) (tps :: [a]).
f tp -> List f tps -> List f (tp : tps)
(:<) (b tp -> List b tps -> List b (tp : tps))
-> t (b tp) -> t (List b tps -> List b (tp : tps))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Index sh tp -> a tp -> t (b tp)
forall (tp :: k). Index sh tp -> a tp -> t (b tp)
f (Index tps tp -> Index sh tp
forall (tp :: k). Index tps tp -> Index sh tp
g Index tps tp
forall k (x :: k) (r :: [k]). Index (x : r) x
IndexHere) a tp
e t (List b tps -> List b (tp : tps))
-> t (List b tps) -> t (List b (tp : tps))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall (tp :: k). Index tps tp -> Index sh tp)
-> List a tps -> t (List b tps)
forall (tps :: [k]).
(forall (tp :: k). Index tps tp -> Index sh tp)
-> List a tps -> t (List b tps)
go (\Index tps tp
ix -> Index tps tp -> Index sh tp
forall (tp :: k). Index tps tp -> Index sh tp
g (Index tps tp -> Index (tp : tps) tp
forall k (r :: [k]) (y :: k) (x :: k). Index r y -> Index (x : r) y
IndexThere Index tps tp
ix)) List a tps
rest