    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE PolyKinds #-}
    {-# LANGUAGE TypeOperators #-}
    {-# LANGUAGE DataKinds #-}

    module Agda.Utils.IndexedList where

    import Data.Kind ( Type )
    import Agda.Utils.Lens

    -- | Existential wrapper for indexed types.
    data Some :: (k -> Type) -> Type where
      Some :: f i -> Some f

    -- | Unpacking a wrapped value.
    withSome :: Some b -> (forall i. b i -> a) -> a
    withSome :: forall {k} (b :: k -> *) a.
    Some b -> (forall (i :: k). b i -> a) -> a
    withSome (Some b i
    x) forall (i :: k). b i -> a
    f = b i -> a
    forall (i :: k). b i -> a
    f b i
    x

    -- | Lists indexed by a type-level list. A value of type @All p [x₁..xₙ]@ is a
    --   sequence of values of types @p x₁@, .., @p xₙ@.
    data All :: (x -> Type) -> [x] -> Type where
      Nil  :: All p '[]
      Cons :: p x -> All p xs -> All p (x ': xs)

    -- | Constructing an indexed list from a plain list.
    makeAll :: (a -> Some b) -> [a] -> Some (All b)
    makeAll :: forall {x} a (b :: x -> *). (a -> Some b) -> [a] -> Some (All b)
    makeAll a -> Some b
    f [] = All b '[] -> Some (All b)
    forall {k} (f :: k -> *) (xs :: k). f xs -> Some f
    Some All b '[]
    forall {x} (p :: x -> *). All p '[]
    Nil
    makeAll a -> Some b
    f (a
    x : [a]
    xs) =
      case (a -> Some b
    f a
    x, (a -> Some b) -> [a] -> Some (All b)
    forall {x} a (b :: x -> *). (a -> Some b) -> [a] -> Some (All b)
    makeAll a -> Some b
    f [a]
    xs) of
        (Some b i
    y, Some All b i
    ys) -> All b (i : i) -> Some (All b)
    forall {k} (f :: k -> *) (xs :: k). f xs -> Some f
    Some (b i -> All b i -> All b (i : i)
    forall {x} (p :: x -> *) (xs :: x) (y :: [x]).
    p xs -> All p y -> All p (xs : y)
    Cons b i
    y All b i
    ys)

    -- | Turning an indexed list back into a plain list.
    forgetAll :: (forall x. b x -> a) -> All b xs -> [a]
    forgetAll :: forall {x} (b :: x -> *) a (xs :: [x]).
    (forall (x :: x). b x -> a) -> All b xs -> [a]
    forgetAll forall (x :: x). b x -> a
    f All b xs
    Nil         = []
    forgetAll forall (x :: x). b x -> a
    f (Cons b x
    x All b xs
    xs) = b x -> a
    forall (x :: x). b x -> a
    f b x
    x a -> [a] -> [a]
    forall a. a -> [a] -> [a]
    : (forall (x :: x). b x -> a) -> All b xs -> [a]
    forall {x} (b :: x -> *) a (xs :: [x]).
    (forall (x :: x). b x -> a) -> All b xs -> [a]
    forgetAll forall (x :: x). b x -> a
    f All b xs
    xs

    -- | An index into a type-level list.
    data Index :: [x] -> x -> Type where
      Zero :: Index (x ': xs) x
      Suc  :: Index xs x -> Index (y ': xs) x

    -- | Indices are just natural numbers.
    forgetIndex :: Index xs x -> Int
    forgetIndex :: forall {x} (xs :: [x]) (x :: x). Index xs x -> Int
    forgetIndex Index xs x
    Zero    = Int
    0
    forgetIndex (Suc Index xs x
    i) = Int
    1 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Index xs x -> Int
    forall {x} (xs :: [x]) (x :: x). Index xs x -> Int
    forgetIndex Index xs x
    i

    -- | Mapping over an indexed list.
    mapWithIndex :: (forall x. Index xs x -> p x -> q x) -> All p xs -> All q xs
    mapWithIndex :: forall {x} (xs :: [x]) (p :: x -> *) (q :: x -> *).
    (forall (x :: x). Index xs x -> p x -> q x) -> All p xs -> All q xs
    mapWithIndex forall (x :: x). Index xs x -> p x -> q x
    f All p xs
    Nil = All q xs
    forall {x} (p :: x -> *). All p '[]
    Nil
    mapWithIndex forall (x :: x). Index xs x -> p x -> q x
    f (Cons p x
    p All p xs
    ps) = q x -> All q xs -> All q (x : xs)
    forall {x} (p :: x -> *) (xs :: x) (y :: [x]).
    p xs -> All p y -> All p (xs : y)
    Cons (Index xs x -> p x -> q x
    forall (x :: x). Index xs x -> p x -> q x
    f Index xs x
    forall {x} (x :: x) (xs :: [x]). Index (x : xs) x
    Zero p x
    p) (All q xs -> All q (x : xs)) -> All q xs -> All q (x : xs)
    forall a b. (a -> b) -> a -> b
    $ (forall (x :: x). Index xs x -> p x -> q x) -> All p xs -> All q xs
    forall {x} (xs :: [x]) (p :: x -> *) (q :: x -> *).
    (forall (x :: x). Index xs x -> p x -> q x) -> All p xs -> All q xs
    mapWithIndex (Index xs x -> p x -> q x
    forall (x :: x). Index xs x -> p x -> q x
    f (Index xs x -> p x -> q x)
    -> (Index xs x -> Index xs x) -> Index xs x -> p x -> q x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Index xs x -> Index xs x
    forall {x} (xs :: [x]) (x :: x) (y :: x).
    Index xs x -> Index (y : xs) x
    Suc) All p xs
    ps

    -- | If you have an index you can get a lens for the given element.
    lIndex :: Index xs x -> Lens' (p x) (All p xs)
    lIndex :: forall {x} (xs :: [x]) (x :: x) (p :: x -> *).
    Index xs x -> Lens' (p x) (All p xs)
    lIndex Index xs x
    Zero    p x -> f (p x)
    f (Cons p x
    x All p xs
    xs) = p x -> f (p x)
    f p x
    p x
    x           f (p x) -> (p x -> All p (x : xs)) -> f (All p (x : xs))
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \ p x
    x  -> p x -> All p xs -> All p (x : xs)
    forall {x} (p :: x -> *) (xs :: x) (y :: [x]).
    p xs -> All p y -> All p (xs : y)
    Cons p x
    x All p xs
    xs
    lIndex (Suc Index xs x
    i) p x -> f (p x)
    f (Cons p x
    x All p xs
    xs) = Index xs x -> Lens' (p x) (All p xs)
    forall {x} (xs :: [x]) (x :: x) (p :: x -> *).
    Index xs x -> Lens' (p x) (All p xs)
    lIndex Index xs x
    i p x -> f (p x)
    f All p xs
    All p xs
    xs f (All p xs) -> (All p xs -> All p (x : xs)) -> f (All p (x : xs))
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \ All p xs
    xs -> p x -> All p xs -> All p (x : xs)
    forall {x} (p :: x -> *) (xs :: x) (y :: [x]).
    p xs -> All p y -> All p (xs : y)
    Cons p x
    x All p xs
    xs

    -- | Looking up an element in an indexed list.
    lookupIndex :: All p xs -> Index xs x -> p x
    lookupIndex :: forall {x} (p :: x -> *) (xs :: [x]) (x :: x).
    All p xs -> Index xs x -> p x
    lookupIndex = (Index xs x -> All p xs -> p x) -> All p xs -> Index xs x -> p x
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip Index xs x -> All p xs -> p x
    forall {x} (xs :: [x]) (x :: x) (p :: x -> *).
    Index xs x -> All p xs -> p x
    ix
      where
        -- -Wincomplete-patterns fails for the other argument order!
        ix :: Index xs x -> All p xs -> p x
        ix :: forall {x} (xs :: [x]) (x :: x) (p :: x -> *).
    Index xs x -> All p xs -> p x
    ix Index xs x
    Zero    (Cons p x
    x All p xs
    xs) = p x
    p x
    x
        ix (Suc Index xs x
    i) (Cons p x
    x All p xs
    xs) = Index xs x -> All p xs -> p x
    forall {x} (xs :: [x]) (x :: x) (p :: x -> *).
    Index xs x -> All p xs -> p x
    ix Index xs x
    i All p xs
    All p xs
    xs

    -- | All indices into an indexed list.
    allIndices :: All p xs -> All (Index xs) xs
    allIndices :: forall {x} (p :: x -> *) (xs :: [x]). All p xs -> All (Index xs) xs
    allIndices = (forall (x :: x). Index xs x -> p x -> Index xs x)
    -> All p xs -> All (Index xs) xs
    forall {x} (xs :: [x]) (p :: x -> *) (q :: x -> *).
    (forall (x :: x). Index xs x -> p x -> q x) -> All p xs -> All q xs
    mapWithIndex forall (x :: x). Index xs x -> p x -> Index xs x
    forall a b. a -> b -> a
    const