Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Utils.Impossible

Description

An interface for reporting "impossible" errors

Synopsis

- data Impossible
  - = Impossible CallStack
  - | Unreachable CallStack
  - | ImpMissingDefinitions [String] String
- throwImpossible :: Impossible -> a
- class CatchImpossible (m :: Type -> Type) where
  - catchImpossible :: m a -> (Impossible -> m a) -> m a
  - catchImpossibleJust :: (Impossible -> Maybe b) -> m a -> (b -> m a) -> m a
  - handleImpossible :: (Impossible -> m a) -> m a -> m a
  - handleImpossibleJust :: (Impossible -> Maybe b) -> (b -> m a) -> m a -> m a
- impossible :: HasCallStack => Impossible
- __IMPOSSIBLE__ :: HasCallStack => a
- __IMPOSSIBLE__1 :: HasCallStack => a
- __UNREACHABLE__ :: HasCallStack => a

# Documentation

data Impossible Source #

"Impossible" errors, annotated with a file name and a line number corresponding to the source code location of the error.

Constructors

Impossible CallStack | We reached a program point which should be unreachable.
Unreachable CallStack | `Impossible` with a different error message. Used when we reach a program point which can in principle be reached, but not for a certain run.
ImpMissingDefinitions [String] String | We reached a program point without all the required primitives or BUILTIN to proceed forward. `ImpMissingDefinitions neededDefs forThis`

#### Instances

Instances details

EmbPrj Impossible Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Impossible -> S Word32 Source # icod_ :: Impossible -> S Word32 Source # value :: Word32 -> R Impossible Source #
NFData Impossible Source # |
Instance details Defined in Agda.Utils.Impossible Methods rnf :: Impossible -> () Source #
Exception Impossible Source # |
Instance details Defined in Agda.Utils.Impossible Methods toException :: Impossible -> SomeException Source # fromException :: SomeException -> Maybe Impossible Source # displayException :: Impossible -> String Source # backtraceDesired :: Impossible -> Bool Source #
Show Impossible Source # |
Instance details Defined in Agda.Utils.Impossible Methods showsPrec :: Int -> Impossible -> ShowS Source # show :: Impossible -> String Source # showList :: [Impossible] -> ShowS Source #
Eq Impossible Source # |
Instance details Defined in Agda.Utils.Impossible Methods (==) :: Impossible -> Impossible -> Bool Source # (/=) :: Impossible -> Impossible -> Bool Source #
Ord Impossible Source # |

Instance details

Defined in Agda.Utils.Impossible

Methods

compare :: Impossible -> Impossible -> Ordering Source #

(<) :: Impossible -> Impossible -> Bool Source #

(<=) :: Impossible -> Impossible -> Bool Source #

(>) :: Impossible -> Impossible -> Bool Source #

(>=) :: Impossible -> Impossible -> Bool Source #

max :: Impossible -> Impossible -> Impossible Source #

min :: Impossible -> Impossible -> Impossible Source #

throwImpossible :: Impossible -> a Source #

Abort by throwing an "impossible" error. You should not use this function directly. Instead use IMPOSSIBLE

class CatchImpossible (m :: Type -> Type) where Source #

Monads in which we can catch an "impossible" error, if possible.

Minimal complete definition

catchImpossibleJust | handleImpossibleJust

Methods

catchImpossible :: m a -> (Impossible -> m a) -> m a Source #

Catch any `Impossible` exception.

catchImpossibleJust :: (Impossible -> Maybe b) -> m a -> (b -> m a) -> m a Source #

Catch only `Impossible` exceptions selected by the filter.

handleImpossible :: (Impossible -> m a) -> m a -> m a Source #

Version of `catchImpossible` with argument order suiting short handlers.

handleImpossibleJust :: (Impossible -> Maybe b) -> (b -> m a) -> m a -> m a Source #

Version of `catchImpossibleJust` with argument order suiting short handlers.

#### Instances

Instances details

CatchImpossible TCM Source # | Like `catchError`, but resets the state completely before running the handler. This means it also loses changes to the `stPersistentState`. The intended use is to catch internal errors during debug printing. In debug printing, we are not expecting state changes.
Instance details Defined in Agda.TypeChecking.Monad.Base Methods catchImpossible :: TCM a -> (Impossible -> TCM a) -> TCM a Source # catchImpossibleJust :: (Impossible -> Maybe b) -> TCM a -> (b -> TCM a) -> TCM a Source # handleImpossible :: (Impossible -> TCM a) -> TCM a -> TCM a Source # handleImpossibleJust :: (Impossible -> Maybe b) -> (b -> TCM a) -> TCM a -> TCM a Source #
CatchImpossible IO Source # |
Instance details Defined in Agda.Utils.Impossible Methods catchImpossible :: IO a -> (Impossible -> IO a) -> IO a Source # catchImpossibleJust :: (Impossible -> Maybe b) -> IO a -> (b -> IO a) -> IO a Source # handleImpossible :: (Impossible -> IO a) -> IO a -> IO a Source # handleImpossibleJust :: (Impossible -> Maybe b) -> (b -> IO a) -> IO a -> IO a Source #

impossible :: HasCallStack => Impossible Source #

Construct a value of `Impossible` reporting the location where you call this function.

__IMPOSSIBLE__ :: HasCallStack => a Source #

Throw an `Impossible` error reporting the location where you place `__IMPOSSIBLE__`.

__IMPOSSIBLE__1 :: HasCallStack => a Source #

Throw an `Impossible` error reporting the *caller's* call site.

__UNREACHABLE__ :: HasCallStack => a Source #

Throw an Unreachable error reporting the *caller's* call site. Note that this call to "withFileAndLine" will be filtered out due its filter on the srcLocModule.