    {-|
    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 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 (tp :: k). 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 (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 = List g x
    List g '[]
    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 {k} (f :: k -> *) (r :: k) (x :: [k]).
    f r -> List f x -> List f (r : x)
    :< (forall (x :: k). f x -> g x)
    -> forall (x :: [k]). List f x -> List g 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
    forall (f :: k -> *) (g :: k -> *).
    (forall (x :: k). f x -> g x)
    -> forall (x :: [k]). List f x -> List g x
    fmapFC f x -> g x
    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) = f tp -> b -> b
    forall (x :: k). f x -> b -> b
    f f tp
    x ((forall (x :: k). f x -> b -> b)
    -> forall (x :: [k]). b -> List f x -> 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
    forall (f :: k -> *) b.
    (forall (x :: k). f x -> b -> b)
    -> forall (x :: [k]). b -> List f x -> b
    foldrFC f x -> b -> b
    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 = List g x -> m (List g x)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure List g x
    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 x
    g tp -> List g tps -> List g (tp : tps)
    forall {k} (f :: k -> *) (r :: k) (x :: [k]).
    f r -> List f x -> List f (r : x)
    (:<) (g tp -> List g tps -> List g x)
    -> m (g tp) -> m (List g tps -> List g x)
    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 x) -> m (List g tps) -> m (List g x)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (forall (x :: k). f x -> m (g x))
    -> forall (x :: [k]). List f x -> m (List g x)
    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)
    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 f x -> m (g x)
    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 (x :: k). IndexF (List f z) x -> f x -> g x)
    -> List f z -> List g z
    (forall (x :: k). Index z x -> f x -> g x) -> List f z -> List g z
    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 (x :: k). IndexF (List f z) x -> f x -> b -> b)
    -> b -> List f z -> b
    (forall (tp :: k). Index z tp -> f tp -> b -> b)
    -> b -> List f z -> b
    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 (x :: k). IndexF (List f z) x -> f x -> m (g x))
    -> List f z -> m (List g z)
    (forall (tp :: k). Index z tp -> f tp -> m (g tp))
    -> List f z -> m (List g z)
    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 = (a :~: b) -> Maybe (a :~: b)
    forall a. a -> Maybe a
    Just a :~: a
    a :~: b
    forall {k} (a :: k). a :~: a
    Refl
      testEquality (f tp
    xh :< List f tps
    xl) (f tp
    yh :< List f tps
    yl) = do
        Refl <- f tp -> f tp -> Maybe (tp :~: tp)
    forall (a :: k) (b :: k). f a -> f b -> Maybe (a :~: b)
    forall {k} (f :: k -> *) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    testEquality f tp
    xh f tp
    yh
        Refl <- testEquality xl yl
        pure Refl
      testEquality List f a
    _ List f b
    _ = Maybe (a :~: b)
    forall a. Maybe a
    Nothing

    instance EqF f => EqF (List f) where
      eqF :: forall (a :: [k]). List f a -> List f a -> Bool
    eqF List f a
    Nil List f a
    Nil =
        Bool
    True
      eqF (f tp
    xh :< List f tps
    xl) (f tp
    yh :< List f tps
    yl) =
        f tp -> f tp -> Bool
    forall (a :: k). f a -> f a -> Bool
    forall k (f :: k -> *) (a :: k). EqF f => f a -> f a -> Bool
    eqF f tp
    xh f tp
    f tp
    yh Bool -> Bool -> Bool
    && List f tps -> List f tps -> Bool
    forall (a :: [k]). List f a -> List f a -> Bool
    forall k (f :: k -> *) (a :: k). EqF f => f a -> f a -> Bool
    eqF List f tps
    xl List f tps
    List f tps
    yl

    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 = OrderingF x x
    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
    $
        OrderingF x x
    OrderingF x y
    (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 {k} (f :: k -> *) (r :: k) (x :: [k]).
    f r -> List f x -> List f (r : x)
    :< List f sh
    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 = (a -> Some (List f) -> Some (List f))
    -> Some (List f) -> [a] -> Some (List f)
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr a -> Some (List f) -> Some (List f)
    g (List f '[] -> Some (List f)
    forall k (f :: k -> *) (x :: k). f x -> Some f
    Some List f '[]
    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 (tp :: k). f tp -> Some (List f))
    -> Some f -> Some (List f)
    forall {k} (f :: k -> *) r.
    (forall (tp :: k). f tp -> r) -> Some f -> r
    viewSome (\f tp
    h -> List f (tp : x) -> Some (List f)
    forall k (f :: k -> *) (x :: k). f x -> Some f
    Some (f tp
    h f tp -> List f x -> List f (tp : x)
    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 = (a -> Some (List f) -> m (Some (List f)))
    -> Some (List f) -> [a] -> m (Some (List 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 (List f '[] -> Some (List f)
    forall k (f :: k -> *) (x :: k). f x -> Some f
    Some List f '[]
    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 (tp :: k). f tp -> Some (List f))
    -> Some f -> Some (List f)
    forall {k} (f :: k -> *) r.
    (forall (tp :: k). f tp -> r) -> Some f -> r
    viewSome (\f tp
    h -> List f (tp : x) -> Some (List f)
    forall k (f :: k -> *) (x :: k). f x -> Some f
    Some (f tp
    h f tp -> List f x -> List f (tp : x)
    forall {k} (f :: k -> *) (r :: k) (x :: [k]).
    f r -> List f x -> List f (r : x)
    :< List f x
    r)) (Some f -> Some (List f)) -> m (Some f) -> m (Some (List f))
    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 = (Some f -> Some f) -> [Some f] -> Some (List f)
    forall {k} a (f :: k -> *). (a -> Some f) -> [a] -> Some (List f)
    fromListWith Some f -> Some f
    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 = (a :~: b) -> Maybe (a :~: b)
    forall a. a -> Maybe a
    Just a :~: a
    a :~: b
    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 (a :: k) (b :: k). 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 :: forall (x :: k) (y :: k). Index l x -> Index l y -> OrderingF x y
    compareF Index l x
    IndexHere Index l y
    IndexHere = OrderingF x x
    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 (x :: k) (y :: k). 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 (x :: k) (y :: k). Index sh x -> Index sh y -> OrderingF x y
    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 = 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 :: 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) = Integer -> Integer -> Integer
    forall a b. a -> b -> b
    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 :: forall {k} (x :: k) (r :: [k]). 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 :: forall {k} (x0 :: k) (x1 :: k) (r :: [k]). 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 :: forall {k} (x0 :: k) (x1 :: k) (x2 :: k) (r :: [k]).
    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 :: forall {k} (x0 :: k) (x1 :: k) (x2 :: k) (x3 :: k) (r :: [k]).
    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 !! :: 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 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 :: 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 s
    f tp
    x f s -> List f tps -> List f (s : tps)
    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 f tp -> List f tps -> List f (tp : tps)
    forall {k} (f :: k -> *) (r :: k) (x :: [k]).
    f r -> List f x -> List f (r : x)
    :< 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 :: 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) = (f x -> List f tps -> List f (x : tps)
    forall {k} (f :: k -> *) (r :: k) (x :: [k]).
    f r -> List f x -> List f (r : x)
    :< List f tps
    rest) (f x -> List f l) -> f (f x) -> f (List f l)
    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 {k} (f :: k -> *) (r :: k) (x :: [k]).
    f r -> List f x -> List f (r : x)
    :<) (List f r -> List f l) -> f (List f r) -> f (List f l)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Index r x -> Lens' (List f r) (f x)
    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.
    --
    -- 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 (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 Index l tp -> Index l tp
    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 (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 -> List g l'
    List g '[]
    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
    Index (tp : tps) 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 {k} (f :: k -> *) (r :: k) (x :: [k]).
    f r -> List f x -> List f (r : x)
    :< (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
    Index tps tp -> Index (tp : tps) tp
    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 = b -> m b
    forall a. a -> m a
    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) = b -> Index sh tp -> a tp -> m b
    forall (tp :: k). b -> Index sh tp -> a tp -> m b
    f b
    b0 Index sh tp
    Index (tp : tps) tp
    forall {k} (x :: k) (r :: [k]). Index (x : r) x
    IndexHere a tp
    a0 m b -> (b -> m b) -> m b
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= Index sh tp -> List a tps -> b -> m b
    forall (tps :: [k]) (tp :: k).
    Index sh tp -> List a tps -> b -> m b
    go Index sh tp
    Index (tp : tps) tp
    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 = b -> m b
    forall a. a -> m a
    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' = Index (ZonkAny 0 : sh) tp -> Index sh tp
    forall a b. a -> b
    unsafeCoerce (Index sh tp -> Index (ZonkAny 0 : sh) tp
    forall {k} (r :: [k]) (y :: k) (x :: k).
    Index r y -> Index (x : r) y
    IndexThere Index sh tp
    idx)
           in b -> Index sh tp -> a tp -> m b
    forall (tp :: k). b -> Index sh tp -> a tp -> m b
    f b
    b Index sh tp
    idx' a tp
    a m b -> (b -> m b) -> m b
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= Index sh tp -> List a tps -> 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 (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 Index sh tp -> Index sh tp
    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 (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 -> 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
    Index (tp : 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 {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 (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 Index sh tp -> Index sh tp
    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 (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) -> List c sh'
    List c '[]
    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
    Index (tp : tps) 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 {k} (f :: k -> *) (r :: k) (x :: [k]).
    f r -> List f x -> List f (r : x)
    :< (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
    Index tps tp -> Index (tp : tps) 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.
    --
    -- 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 (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 Index sh tp -> Index sh tp
    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 (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 -> List b tps -> t (List b tps)
    forall a. a -> t a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure List b tps
    List b '[]
    forall {k} (f :: k -> *). List f '[]
    Nil
            a tp
    e :< List a tps
    rest -> b tp -> List b tps -> List b tps
    b tp -> List b tps -> List b (tp : tps)
    forall {k} (f :: k -> *) (r :: k) (x :: [k]).
    f r -> List f x -> List f (r : x)
    (:<) (b tp -> List b tps -> List b tps)
    -> t (b tp) -> t (List b tps -> List b 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
    Index (tp : tps) tp
    forall {k} (x :: k) (r :: [k]). Index (x : r) x
    IndexHere) a tp
    e t (List b tps -> List b tps) -> t (List b tps) -> t (List b tps)
    forall a b. t (a -> b) -> t a -> t b
    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