git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2163 from JakobBruenker/vecfin
217c669David Christiansen
CHANGELOG+2
compare with master
unifiedsplit
@@ -28,6 +28,8 @@ New in 0.9.18:
28 choice, keeping the first success as Alternative does. The version that
28 choice, keeping the first success as Alternative does. The version that
29 collects successes is now a named instance.
29 collects successes is now a named instance.
30* :exec REPL command now takes an optional expression to compile and run/show
30* :exec REPL command now takes an optional expression to compile and run/show
31+* The return types of `Vect.findIndex`, `Vect.elemIndex` and
32+ `Vect.elemIndexBy` were changed from `Maybe Nat` to `Maybe (Fin n)`
31
33
32New in 0.9.17:
34New in 0.9.17:
33--------------
35--------------
libs/base/Data/VectType.idr+7−10
@@ -372,14 +372,11 @@ find p (x::xs) with (p x)
372 | False = find p xs
372 | False = find p xs
373
373
374||| Find the index of the first element of the vector that satisfies some test
374||| Find the index of the first element of the vector that satisfies some test
375−findIndex : (a -> Bool) -> Vect n a -> Maybe Nat
375+findIndex : (a -> Bool) -> Vect n a -> Maybe (Fin n)
376−findIndex = findIndex' 0
377− where
378− findIndex' : Nat -> (a -> Bool) -> Vect n a -> Maybe Nat
379− findIndex' cnt p [] = Nothing
376+findIndex p [] = Nothing
380− findIndex' cnt p (x::xs) with (p x)
377+findIndex p (x :: xs) with (p x)
381− | True = Just cnt
378+ | True = Just 0
382− | False = findIndex' (S cnt) p xs
379+ | False = map FS (findIndex p xs)
383
380
384||| Find the indices of all elements that satisfy some test
381||| Find the indices of all elements that satisfy some test
385total findIndices : (a -> Bool) -> Vect m a -> (p ** Vect p Nat)
382total findIndices : (a -> Bool) -> Vect m a -> (p ** Vect p Nat)
@@ -394,10 +391,10 @@ findIndices = findIndices' 0
394 else
391 else
395 (_ ** tail)
392 (_ ** tail)
396
393
397−elemIndexBy : (a -> a -> Bool) -> a -> Vect m a -> Maybe Nat
394+elemIndexBy : (a -> a -> Bool) -> a -> Vect m a -> Maybe (Fin m)
398elemIndexBy p e = findIndex $ p e
395elemIndexBy p e = findIndex $ p e
399
396
400−elemIndex : Eq a => a -> Vect m a -> Maybe Nat
397+elemIndex : Eq a => a -> Vect m a -> Maybe (Fin m)
401elemIndex = elemIndexBy (==)
398elemIndex = elemIndexBy (==)
402
399
403total elemIndicesBy : (a -> a -> Bool) -> a -> Vect m a -> (p ** Vect p Nat)
400total elemIndicesBy : (a -> a -> Bool) -> a -> Vect m a -> (p ** Vect p Nat)