{-# LANGUAGE CPP #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
module Agda.Utils.IndexedList where
import Agda.Utils.Lens
-- | Existential wrapper for indexed types.
data Some :: (k -> *) -> * where
Some :: f i -> Some f
-- | Unpacking a wrapped value.
withSome :: Some b -> (forall i. b i -> a) -> a
withSome (Some x) f = f 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 -> *) -> [x] -> * 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 f [] = Some Nil
makeAll f (x : xs) =
case (f x, makeAll f xs) of
(Some y, Some ys) -> Some (Cons y ys)
-- | Turning an indexed list back into a plain list.
forgetAll :: (forall x. b x -> a) -> All b xs -> [a]
forgetAll f Nil = []
forgetAll f (Cons x xs) = f x : forgetAll f xs
-- | An index into a type-level list.
data Index :: [x] -> x -> * 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 Zero = 0
forgetIndex (Suc i) = 1 + forgetIndex i
-- | Mapping over an indexed list.
mapWithIndex :: (forall x. Index xs x -> p x -> q x) -> All p xs -> All q xs
mapWithIndex f Nil = Nil
mapWithIndex f (Cons p ps) = Cons (f Zero p) $ mapWithIndex (f . Suc) 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 Zero f (Cons x xs) = f x <&> \ x -> Cons x xs
lIndex (Suc i) f (Cons x xs) = lIndex i f xs <&> \ xs -> Cons x xs
#if __GLASGOW_HASKELL__ < 800
lIndex _ _ Nil = error "-fwarn-incomplete-pattern deficiency"
#endif
-- | Looking up an element in an indexed list.
lookupIndex :: All p xs -> Index xs x -> p x
lookupIndex = flip ix
where
-- -Wincomplete-patterns fails for the other argument order!
ix :: Index xs x -> All p xs -> p x
ix Zero (Cons x xs) = x
ix (Suc i) (Cons x xs) = ix i xs
#if __GLASGOW_HASKELL__ < 800
ix _ Nil = error "-fwarn-incomplete-pattern deficiency"
#endif
-- | All indices into an indexed list.
allIndices :: All p xs -> All (Index xs) xs
allIndices = mapWithIndex const