{-# 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 :: 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 :: (a -> Some b) -> [a] -> Some (All b)
makeAll a -> Some b
f [] = All b '[] -> Some (All b)
forall k (f :: k -> *) (i :: k). f i -> 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 -> *) (i :: k). f i -> Some f
Some (b i -> All b i -> All b (i : i)
forall a (p :: a -> *) (x :: a) (xs :: [a]).
p x -> All p xs -> All p (x : xs)
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 :: 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 :: 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 :: 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 a (p :: a -> *) (x :: a) (xs :: [a]).
p x -> All p xs -> All p (x : xs)
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 :: 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 a (p :: a -> *) (x :: a) (xs :: [a]).
p x -> All p xs -> All p (x : xs)
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 -> (p x -> f (p x)) -> All p xs -> f (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 a (p :: a -> *) (x :: a) (xs :: [a]).
p x -> All p xs -> All p (x : xs)
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 :: 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 :: 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 :: 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