-- | Lists of statically-known length
module Data.Fin.List (Peano, List (..),
                      fromList, uncons, head, tail, init, last, reverse, rotate, at, swap, (!!), findIndex) where

import Prelude ()
import Data.Bool (Bool, bool)
import Control.Applicative
import Control.Category (id)
import Data.Fin.Private as Fin
import Data.Peano (Peano)

-- | Find the indices of all elements satisfying the given predicate, gathering them in @p@.
findIndex :: Alternative p => (a -> Bool) -> List n a -> p (Fin n)
findIndex :: (a -> Bool) -> List n a -> p (Fin n)
findIndex p :: a -> Bool
p = \ case
    Nil -> p (Fin n)
forall (f :: * -> *) a. Alternative f => f a
empty
    a :: a
a:.as :: List n a
as -> (p (Fin ('Succ n)) -> p (Fin ('Succ n)))
-> (p (Fin ('Succ n)) -> p (Fin ('Succ n)))
-> Bool
-> p (Fin ('Succ n))
-> p (Fin n)
forall a. a -> a -> Bool -> a
bool p (Fin ('Succ n)) -> p (Fin ('Succ n))
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id (Fin ('Succ n) -> p (Fin ('Succ n))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Fin ('Succ n)
forall (n :: Peano). Fin ('Succ n)
Zero p (Fin ('Succ n)) -> p (Fin ('Succ n)) -> p (Fin ('Succ n))
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>) (a -> Bool
p a
a) (Fin n -> Fin ('Succ n)
forall (n :: Peano). Fin n -> Fin ('Succ n)
Succ (Fin n -> Fin ('Succ n)) -> p (Fin n) -> p (Fin ('Succ n))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> Bool) -> List n a -> p (Fin n)
forall (p :: * -> *) a (n :: Peano).
Alternative p =>
(a -> Bool) -> List n a -> p (Fin n)
findIndex a -> Bool
p List n a
as)