hermit- Haskell Equational Reasoning Model-to-Implementation Tunnel

Safe HaskellNone




The HERMIT Kernel

data AST Source

A handle for a specific version of the ModGuts.


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.

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

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 -> HermitMEnv -> IO (KureM AST)Source

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

queryK :: Kernel -> forall a. AST -> TranslateH ModGuts a -> HermitMEnv -> IO (KureM a)Source

Apply a TranslateH 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.