module Agda.Utils.Impossible where
import Control.Exception (Exception(..), throw, catchJust)
import GHC.Stack
(CallStack, HasCallStack, callStack, getCallStack, freezeCallStack
, srcLocModule, srcLocFile, srcLocStartLine)
data Impossible
= Impossible String Integer
| Unreachable String Integer
| ImpMissingDefinitions [String] String
instance Show Impossible where
show (Impossible file line) = unlines
[ "An internal error has occurred. Please report this as a bug."
, "Location of the error: " ++ file ++ ":" ++ show line
]
show (Unreachable file line) = unlines
[ "We reached a program point we did not want to reach."
, "Location of the error: " ++ file ++ ":" ++ show line
]
show (ImpMissingDefinitions needed forthis) = unlines
[ "The following builtins or primitives need to be bound to use " ++ forthis ++ ":"]
++ unwords needed
instance Exception Impossible
throwImpossible :: Impossible -> a
throwImpossible = throw
class CatchImpossible m where
catchImpossible :: m a -> (Impossible -> m a) -> m a
catchImpossible = catchImpossibleJust Just
catchImpossibleJust :: (Impossible -> Maybe b) -> m a -> (b -> m a) -> m a
catchImpossibleJust = flip . handleImpossibleJust
handleImpossible :: (Impossible -> m a) -> m a -> m a
handleImpossible = flip catchImpossible
handleImpossibleJust :: (Impossible -> Maybe b) -> (b -> m a) -> m a -> m a
handleImpossibleJust = flip . catchImpossibleJust
{-# MINIMAL catchImpossibleJust | handleImpossibleJust #-}
instance CatchImpossible IO where
catchImpossibleJust = catchJust
withFileAndLine' :: Integral a => CallStack -> (String -> a -> b) -> b
withFileAndLine' cs ctor = ctor file line
where
callSiteList = getCallStack cs
notHere (_, loc) = srcLocModule loc /= "Agda.Utils.Impossible"
stackLocations = filter notHere callSiteList
(file, line) = case stackLocations of
(_, loc) : _ -> (srcLocFile loc, fromIntegral (srcLocStartLine loc))
[] -> ("?", -1)
withFileAndLine :: (HasCallStack, Integral a) => (String -> a -> b) -> b
withFileAndLine = withFileAndLine' (freezeCallStack callStack)
__IMPOSSIBLE__ :: HasCallStack => a
__IMPOSSIBLE__ = throwImpossible (withFileAndLine Impossible)
__UNREACHABLE__ :: HasCallStack => a
__UNREACHABLE__ = throwImpossible (withFileAndLine Unreachable)