module Agda.Utils.Either
( isLeft, isRight
, allRight
, tests
) where
import Control.Arrow
import Agda.Utils.QuickCheck
import Agda.Utils.TestHelpers
#include "../undefined.h"
import Agda.Utils.Impossible
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)
]