------------------------------------------------------------------------
-- | Utilities for the 'Either' type
------------------------------------------------------------------------
module Agda.Utils.Either
( isLeft, isRight
, allRight
, tests
) where
import Control.Arrow
import Agda.Utils.QuickCheck
import Agda.Utils.TestHelpers
-- | Returns 'True' iff the argument is @'Right' x@ for some @x@.
isRight :: Either a b -> Bool
isRight (Right _) = True
isRight (Left _) = False
-- | Returns 'True' iff the argument is @'Left' x@ for some @x@.
isLeft :: Either a b -> Bool
isLeft (Right _) = False
isLeft (Left _) = True
-- | Returns @'Right' @ if all elements are
-- to the right, and otherwise @Left @:
--
-- @
-- allRight xs ==
-- if all isRight xs then
-- Right (map (\(Right x) -> x) xs)
-- else
-- Left xs
-- @
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 (\(Right x) -> x) xs)
else
Left xs
------------------------------------------------------------------------
-- All tests
tests :: IO Bool
tests = runTests "Agda.Utils.Either"
[ quickCheck' (prop_allRight :: [Either Integer Bool] -> Bool)
]