{-# LANGUAGE CPP #-}
{-# OPTIONS_GHC -Wunused-imports #-}
module Agda.Utils.Impossible where
import Control.Exception (Exception(..), throw, catchJust)
import Control.DeepSeq
import Agda.Utils.CallStack.Base
( CallStack
, HasCallStack
, prettyCallStack
, withCallerCallStack
)
data Impossible
= Impossible CallStack
| Unreachable CallStack
| ImpMissingDefinitions [String] String
instance Eq Impossible where
Impossible
_ == :: Impossible -> Impossible -> Bool
== Impossible
_ = Bool
True
instance Ord Impossible where
compare :: Impossible -> Impossible -> Ordering
compare Impossible
_ Impossible
_ = Ordering
EQ
instance NFData Impossible where
rnf :: Impossible -> ()
rnf Impossible
_ = ()
instance Show Impossible where
show :: Impossible -> String
show (Impossible CallStack
loc) = [String] -> String
unlines
[ String
"An internal error has occurred. Please report this as a bug."
, String
"Location of the error: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ CallStack -> String
prettyCallStack CallStack
loc
]
show (Unreachable CallStack
loc) = [String] -> String
unlines
[ String
"We reached a program point we did not want to reach."
, String
"Location of the error: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ CallStack -> String
prettyCallStack CallStack
loc
]
show (ImpMissingDefinitions [String]
needed String
forthis) = [String] -> String
unlines
[ String
"The following builtins or primitives need to be bound to use " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
forthis String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
":"
, [String] -> String
unwords [String]
needed
]
instance Exception Impossible where
#if MIN_VERSION_base(4,20,0)
backtraceDesired :: Impossible -> Bool
backtraceDesired Impossible
_ = Bool
False
#endif
throwImpossible :: Impossible -> a
throwImpossible :: forall a. Impossible -> a
throwImpossible = Impossible -> a
forall a e. (?callStack::CallStack, Exception e) => e -> a
throw
class CatchImpossible m where
catchImpossible :: m a -> (Impossible -> m a) -> m a
catchImpossible = (Impossible -> Maybe Impossible)
-> m a -> (Impossible -> m a) -> m a
forall b a. (Impossible -> Maybe b) -> m a -> (b -> m a) -> m a
forall (m :: * -> *) b a.
CatchImpossible m =>
(Impossible -> Maybe b) -> m a -> (b -> m a) -> m a
catchImpossibleJust Impossible -> Maybe Impossible
forall a. a -> Maybe a
Just
catchImpossibleJust :: (Impossible -> Maybe b) -> m a -> (b -> m a) -> m a
catchImpossibleJust = ((b -> m a) -> m a -> m a) -> m a -> (b -> m a) -> m a
forall a b c. (a -> b -> c) -> b -> a -> c
flip (((b -> m a) -> m a -> m a) -> m a -> (b -> m a) -> m a)
-> ((Impossible -> Maybe b) -> (b -> m a) -> m a -> m a)
-> (Impossible -> Maybe b)
-> m a
-> (b -> m a)
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Impossible -> Maybe b) -> (b -> m a) -> m a -> m a
forall b a. (Impossible -> Maybe b) -> (b -> m a) -> m a -> m a
forall (m :: * -> *) b a.
CatchImpossible m =>
(Impossible -> Maybe b) -> (b -> m a) -> m a -> m a
handleImpossibleJust
handleImpossible :: (Impossible -> m a) -> m a -> m a
handleImpossible = (m a -> (Impossible -> m a) -> m a)
-> (Impossible -> m a) -> m a -> m a
forall a b c. (a -> b -> c) -> b -> a -> c
flip m a -> (Impossible -> m a) -> m a
forall a. m a -> (Impossible -> m a) -> m a
forall (m :: * -> *) a.
CatchImpossible m =>
m a -> (Impossible -> m a) -> m a
catchImpossible
handleImpossibleJust :: (Impossible -> Maybe b) -> (b -> m a) -> m a -> m a
handleImpossibleJust = (m a -> (b -> m a) -> m a) -> (b -> m a) -> m a -> m a
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((m a -> (b -> m a) -> m a) -> (b -> m a) -> m a -> m a)
-> ((Impossible -> Maybe b) -> m a -> (b -> m a) -> m a)
-> (Impossible -> Maybe b)
-> (b -> m a)
-> m a
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Impossible -> Maybe b) -> m a -> (b -> m a) -> m a
forall b a. (Impossible -> Maybe b) -> m a -> (b -> m a) -> m a
forall (m :: * -> *) b a.
CatchImpossible m =>
(Impossible -> Maybe b) -> m a -> (b -> m a) -> m a
catchImpossibleJust
{-# MINIMAL catchImpossibleJust | handleImpossibleJust #-}
instance CatchImpossible IO where
catchImpossibleJust :: forall b a. (Impossible -> Maybe b) -> IO a -> (b -> IO a) -> IO a
catchImpossibleJust = (Impossible -> Maybe b) -> IO a -> (b -> IO a) -> IO a
forall e b a.
Exception e =>
(e -> Maybe b) -> IO a -> (b -> IO a) -> IO a
catchJust
__IMPOSSIBLE__ :: HasCallStack => a
__IMPOSSIBLE__ :: forall a. (?callStack::CallStack) => a
__IMPOSSIBLE__ = (CallStack -> a) -> a
forall b. (?callStack::CallStack) => (CallStack -> b) -> b
withCallerCallStack ((CallStack -> a) -> a) -> (CallStack -> a) -> a
forall a b. (a -> b) -> a -> b
$ Impossible -> a
forall a. Impossible -> a
throwImpossible (Impossible -> a) -> (CallStack -> Impossible) -> CallStack -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CallStack -> Impossible
Impossible
impossible :: HasCallStack => Impossible
impossible :: (?callStack::CallStack) => Impossible
impossible = (CallStack -> Impossible) -> Impossible
forall b. (?callStack::CallStack) => (CallStack -> b) -> b
withCallerCallStack CallStack -> Impossible
Impossible
__UNREACHABLE__ :: HasCallStack => a
__UNREACHABLE__ :: forall a. (?callStack::CallStack) => a
__UNREACHABLE__ = (CallStack -> a) -> a
forall b. (?callStack::CallStack) => (CallStack -> b) -> b
withCallerCallStack ((CallStack -> a) -> a) -> (CallStack -> a) -> a
forall a b. (a -> b) -> a -> b
$ Impossible -> a
forall a. Impossible -> a
throwImpossible (Impossible -> a) -> (CallStack -> Impossible) -> CallStack -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CallStack -> Impossible
Unreachable