-- | 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 forall a. Ord a => a -> a -> Bool
> Int
9) 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 = seq :: forall a b. a -> b -> b
seq Empty
e 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 <- forall (m :: * -> *) a.
CatchImpossible m =>
m a -> (Impossible -> m a) -> m a
catchImpossible (forall a. Maybe a
Nothing forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall a. a -> IO a
evaluate Empty
e) (forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just)
  case Maybe Impossible
s of
    Just Impossible
i  -> forall (m :: * -> *) a. Monad m => a -> m a
return Impossible
i
    Maybe Impossible
Nothing -> forall a. Empty -> a
absurd Empty
e -- this should never happen