-- | An empty type with some useful instances.
module Agda.Utils.Empty where

import Control.DeepSeq
import Control.Exception (evaluate)

import Agda.Utils.Impossible


data Empty

-- | Values of type 'Empty' are not forced, because 'Empty' is used as
-- a constructor argument in 'Agda.Syntax.Internal.Substitution''.

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 e@ extracts the @Impossible@ value raised via
--   @__IMPOSSIBLE__@ to create the element @e@ of type @Empty@.
--   It proceeds by evaluating @e@ to weak head normal form and
--   catching the exception.
--   We are forced to wrap things in a @Maybe@ because of
--   @catchImpossible@'s type.

toImpossible :: Empty -> IO Impossible
toImpossible :: Empty -> IO Impossible
toImpossible Empty
e = do
  Maybe Impossible
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 Maybe Impossible
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 -- this should never happen