-- | A pure MonadFail.
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
module Agda.Utils.Fail where

import Control.Monad.Fail

newtype Fail a = Fail { Fail a -> Either String a
runFail :: Either String a }
  deriving (a -> Fail b -> Fail a
(a -> b) -> Fail a -> Fail b
(forall a b. (a -> b) -> Fail a -> Fail b)
-> (forall a b. a -> Fail b -> Fail a) -> Functor Fail
forall a b. a -> Fail b -> Fail a
forall a b. (a -> b) -> Fail a -> Fail b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Fail b -> Fail a
$c<$ :: forall a b. a -> Fail b -> Fail a
fmap :: (a -> b) -> Fail a -> Fail b
$cfmap :: forall a b. (a -> b) -> Fail a -> Fail b
Functor, Functor Fail
a -> Fail a
Functor Fail
-> (forall a. a -> Fail a)
-> (forall a b. Fail (a -> b) -> Fail a -> Fail b)
-> (forall a b c. (a -> b -> c) -> Fail a -> Fail b -> Fail c)
-> (forall a b. Fail a -> Fail b -> Fail b)
-> (forall a b. Fail a -> Fail b -> Fail a)
-> Applicative Fail
Fail a -> Fail b -> Fail b
Fail a -> Fail b -> Fail a
Fail (a -> b) -> Fail a -> Fail b
(a -> b -> c) -> Fail a -> Fail b -> Fail c
forall a. a -> Fail a
forall a b. Fail a -> Fail b -> Fail a
forall a b. Fail a -> Fail b -> Fail b
forall a b. Fail (a -> b) -> Fail a -> Fail b
forall a b c. (a -> b -> c) -> Fail a -> Fail b -> Fail c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: Fail a -> Fail b -> Fail a
$c<* :: forall a b. Fail a -> Fail b -> Fail a
*> :: Fail a -> Fail b -> Fail b
$c*> :: forall a b. Fail a -> Fail b -> Fail b
liftA2 :: (a -> b -> c) -> Fail a -> Fail b -> Fail c
$cliftA2 :: forall a b c. (a -> b -> c) -> Fail a -> Fail b -> Fail c
<*> :: Fail (a -> b) -> Fail a -> Fail b
$c<*> :: forall a b. Fail (a -> b) -> Fail a -> Fail b
pure :: a -> Fail a
$cpure :: forall a. a -> Fail a
$cp1Applicative :: Functor Fail
Applicative, Applicative Fail
a -> Fail a
Applicative Fail
-> (forall a b. Fail a -> (a -> Fail b) -> Fail b)
-> (forall a b. Fail a -> Fail b -> Fail b)
-> (forall a. a -> Fail a)
-> Monad Fail
Fail a -> (a -> Fail b) -> Fail b
Fail a -> Fail b -> Fail b
forall a. a -> Fail a
forall a b. Fail a -> Fail b -> Fail b
forall a b. Fail a -> (a -> Fail b) -> Fail b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: a -> Fail a
$creturn :: forall a. a -> Fail a
>> :: Fail a -> Fail b -> Fail b
$c>> :: forall a b. Fail a -> Fail b -> Fail b
>>= :: Fail a -> (a -> Fail b) -> Fail b
$c>>= :: forall a b. Fail a -> (a -> Fail b) -> Fail b
$cp1Monad :: Applicative Fail
Monad)

instance MonadFail Fail where
  fail :: String -> Fail a
fail = Either String a -> Fail a
forall a. Either String a -> Fail a
Fail (Either String a -> Fail a)
-> (String -> Either String a) -> String -> Fail a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Either String a
forall a b. a -> Either a b
Left

runFail_ :: Fail a -> a
runFail_ :: Fail a -> a
runFail_ = (String -> a) -> (a -> a) -> Either String a -> a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either String -> a
forall a. HasCallStack => String -> a
error a -> a
forall a. a -> a
id (Either String a -> a)
-> (Fail a -> Either String a) -> Fail a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fail a -> Either String a
forall a. Fail a -> Either String a
runFail