module Agda.Utils.Either
( mapEither, mapLeft, mapRight
, isLeft, isRight
, allRight
, tests
) where
import Control.Arrow
import Agda.Utils.QuickCheck
import Agda.Utils.TestHelpers
#include "../undefined.h"
import Agda.Utils.Impossible
mapEither :: (a -> c) -> (b -> d) -> Either a b -> Either c d
mapEither f g = either (Left . f) (Right . g)
mapLeft :: (a -> c) -> Either a b -> Either c b
mapLeft f = mapEither f id
mapRight :: (b -> d) -> Either a b -> Either a d
mapRight = mapEither id
isRight :: Either a b -> Bool
isRight (Right _) = True
isRight (Left _) = False
isLeft :: Either a b -> Bool
isLeft (Right _) = False
isLeft (Left _) = True
allRight :: [Either a b] -> Either [Either a b] [b]
allRight [] = Right []
allRight xs@(Left _ : _) = Left xs
allRight (Right b : xs) = case allRight xs of
Left xs -> Left (Right b : xs)
Right bs -> Right (b : bs)
prop_allRight xs =
allRight xs ==
if all isRight xs then
Right (map fromRight xs)
else
Left xs
where
fromRight (Right x) = x
fromRight (Left _) = __IMPOSSIBLE__
tests :: IO Bool
tests = runTests "Agda.Utils.Either"
[ quickCheck' (prop_allRight :: [Either Integer Bool] -> Bool)
]