hermit-0.6.0.0: Haskell Equational Reasoning Model-to-Implementation Tunnel

Safe HaskellNone
LanguageHaskell2010

HERMIT.Kernel

Contents

Synopsis

The HERMIT Kernel

data AST Source

A handle for a specific version of the ModGuts.

Instances

data Kernel Source

A Kernel is a repository for complete Core syntax trees (ModGuts). For now, operations on a Kernel are sequential, but later it will be possible to have two applyKs running in parallel.

data KernelEnv Source

Constructors

KernelEnv 

Fields

kEnvChan :: DebugMessage -> HermitM ()
 

hermitKernel :: (Kernel -> AST -> IO ()) -> ModGuts -> CoreM ModGuts Source

Start a HERMIT client by providing an IO function that takes the initial Kernel and inital AST handle. The Modguts to CoreM Modguts' function required by GHC Plugins is returned. The callback is only ever called once.

resumeK :: Kernel -> AST -> IO () Source

Halt the Kernel and return control to GHC, which compiles the specified AST.

abortK :: Kernel -> IO () Source

Halt the Kernel and abort GHC without compiling.

applyK :: Kernel -> AST -> RewriteH ModGuts -> KernelEnv -> IO (KureM AST) Source

Apply a Rewrite to the specified AST and return a handle to the resulting AST.

queryK :: Kernel -> forall a. AST -> TransformH ModGuts a -> KernelEnv -> IO (KureM a) Source

Apply a TransformH to the AST and return the resulting value.

deleteK :: Kernel -> AST -> IO () Source

Delete the internal record of the specified AST.

listK :: Kernel -> IO [AST] Source

List all the ASTs tracked by the Kernel.