| Copyright | (c) Galois Inc, 2015 |
|---|---|
| License | Apache-2 |
| Maintainer | jhendrix@galois.com, lcasburn@galois.com |
| Safe Haskell | Safe |
| Language | Haskell98 |
Language.Lean.Internal.Exception
Description
Internal operations for working with Lean exceptions.
- data LeanException = LeanException {}
- data LeanExceptionKind
- type ExceptionPtr = Ptr LeanException
- type OutExceptionPtr = Ptr ExceptionPtr
- throwLeanException :: ExceptionPtr -> IO a
- leanKernelException :: String -> LeanException
- leanOtherException :: String -> LeanException
- type LeanPartialAction = Ptr ExceptionPtr -> IO Bool
- runLeanPartialAction :: LeanPartialAction -> IO ()
- type LeanPartialFn a = Ptr a -> LeanPartialAction
- runLeanPartialFn :: Storable a => LeanPartialFn a -> IO a
- runLeanMaybeFn :: Storable p => LeanPartialFn p -> IO (Maybe p)
- class Storable p => IsLeanValue v p | v -> p where
- mkLeanValue :: p -> IO v
- tryAllocLeanValue :: IsLeanValue a p => LeanPartialFn p -> IO a
Documentation
data LeanExceptionKind Source
Information about the Kind of exception thrown.
Constructors
| LeanSystemException | |
| LeanOutOfMemory | |
| LeanInterrupted | |
| LeanKernelException | Errors from Lean misuse |
| LeanOtherException |
Instances
FFI types
type ExceptionPtr = Ptr LeanException Source
Pointer used as input parameter for exceptions in FFI bindings
type OutExceptionPtr = Ptr ExceptionPtr Source
Pointer used as output parameter for exceptions in FFI bindings
throwLeanException :: ExceptionPtr -> IO a Source
Convert the ExceptionPtr to a Lean exception and throw it while releasing the ExceptionPtr
leanKernelException :: String -> LeanException Source
Create a Lean kernel exception from the given messasge.
leanOtherException :: String -> LeanException Source
Create a Lean other exception from the given messasge.
Partial operations
type LeanPartialAction = Ptr ExceptionPtr -> IO Bool Source
A lean partial function is an action that may fail
runLeanPartialAction :: LeanPartialAction -> IO () Source
Run a lean partial action, throwing an exception if it fails.
type LeanPartialFn a = Ptr a -> LeanPartialAction Source
A lean partial function is a function that returns a value of type a, but
may fail.
runLeanPartialFn :: Storable a => LeanPartialFn a -> IO a Source
Run a lean partial function
runLeanMaybeFn :: Storable p => LeanPartialFn p -> IO (Maybe p) Source
Run a lean partial function where false does not automatically imply an exception was thrown.
class Storable p => IsLeanValue v p | v -> p where Source
Typeclass that associates Haskell types with their type in the FFI layer.
Instances
Functions that return a result in IO
tryAllocLeanValue :: IsLeanValue a p => LeanPartialFn p -> IO a Source
Try to run a Lean partial function that returns a Lean value that will need to be freed.