{-# OPTIONS_GHC -Wunused-imports #-}
module Agda.Utils.Empty where
import Control.DeepSeq
import Control.Exception (evaluate)
import Agda.Utils.Impossible
data Empty
instance NFData Empty where
rnf :: Empty -> ()
rnf Empty
_ = ()
instance Eq Empty where
Empty
_ == :: Empty -> Empty -> Bool
== Empty
_ = Bool
True
instance Ord Empty where
compare :: Empty -> Empty -> Ordering
compare Empty
_ Empty
_ = Ordering
EQ
instance Show Empty where
showsPrec :: Int -> Empty -> ShowS
showsPrec Int
p Empty
_ = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"error \"Agda.Utils.Empty.Empty\""
absurd :: Empty -> a
absurd :: forall a. Empty -> a
absurd Empty
e = Empty -> a -> a
forall a b. a -> b -> b
seq Empty
e a
forall a. HasCallStack => a
__IMPOSSIBLE__
toImpossible :: Empty -> IO Impossible
toImpossible :: Empty -> IO Impossible
toImpossible Empty
e = do
s <- IO (Maybe Impossible)
-> (Impossible -> IO (Maybe Impossible)) -> IO (Maybe Impossible)
forall a. IO a -> (Impossible -> IO a) -> IO a
forall (m :: * -> *) a.
CatchImpossible m =>
m a -> (Impossible -> m a) -> m a
catchImpossible (Maybe Impossible
forall a. Maybe a
Nothing Maybe Impossible -> IO Empty -> IO (Maybe Impossible)
forall a b. a -> IO b -> IO a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Empty -> IO Empty
forall a. a -> IO a
evaluate Empty
e) (Maybe Impossible -> IO (Maybe Impossible)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Impossible -> IO (Maybe Impossible))
-> (Impossible -> Maybe Impossible)
-> Impossible
-> IO (Maybe Impossible)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Impossible -> Maybe Impossible
forall a. a -> Maybe a
Just)
case s of
Just Impossible
i -> Impossible -> IO Impossible
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Impossible
i
Maybe Impossible
Nothing -> Empty -> IO Impossible
forall a. Empty -> a
absurd Empty
e