hermit- Haskell Equational Reasoning Model-to-Implementation Tunnel

Safe HaskellNone




data ShellCommand Source

There are four types of commands.


KernelEffect KernelEffect

Command that modifies the state of the (scoped) kernel.

ShellEffect ShellEffect

Command that modifies the state of the shell.

QueryFun QueryFun

Command that queries the AST with a Translate (read only).

MetaCommand MetaCommand

Command that otherwise controls HERMIT (abort, resume, save, etc).

data KernelEffect whereSource

KernelEffects are things that affect the state of the Kernel - Apply a rewrite (giving a whole new lower-level AST). - Change the current location using a computed path. - Change the currect location using directions. - Begin or end a scope. - Delete an AST - Run a precondition or other predicate that must not fail.

loadAndRun :: FilePath -> MetaCommandSource

A composite meta-command for running a loaded script immediately. The script is given the same name as the filepath.

data CLException Source


Error CLException 
Monad m => MonadError CLException (CLM m) 

newtype CLM m a Source




unCLM :: ErrorT CLException (StateT CommandLineState m) a


MonadTrans CLM 
Monad m => MonadState CommandLineState (CLM m) 
Monad m => MonadError CLException (CLM m) 
Monad m => Monad (CLM m)

Our own custom instance of Monad for CLM m so we don't have to depend on newtype deriving to do the right thing for fail.

Functor m => Functor (CLM m) 
(Monad m, Functor m) => Applicative (CLM m) 
MonadIO m => MonadIO (CLM m) 
Monad m => MonadCatch (CLM m) 

abort :: Monad m => CLM m ()Source

resume :: Monad m => SAST -> CLM m ()Source

iokm2clm' :: MonadIO m => String -> (a -> CLM m b) -> IO (KureM a) -> CLM m bSource

iokm2clm :: MonadIO m => String -> IO (KureM a) -> CLM m aSource

iokm2clm'' :: MonadIO m => IO (KureM a) -> CLM m aSource

data VersionStore Source




vs_graph :: [(SAST, ExprH, SAST)]
vs_tags :: [(String, SAST)]

data CommandLineState Source




cl_cursor :: SAST

the current AST

cl_pretty :: PrettyH CoreTC

which pretty printer to use

cl_pretty_opts :: PrettyOptions

the options for the pretty printer

cl_render :: Handle -> PrettyOptions -> Either String DocH -> IO ()

the way of outputing to the screen

cl_height :: Int

console height, in lines

cl_nav :: Bool

keyboard input the nav panel

cl_running_script :: Bool

if running a script

cl_tick :: TVar (Map String Int)

the list of ticked messages

cl_corelint :: Bool

if true, run Core Lint on module after each rewrite

cl_diffonly :: Bool

if true, show diffs rather than pp full code

cl_failhard :: Bool

if true, abort on *any* failure

cl_window :: PathH

path to beginning of window, always a prefix of focus path in kernel these four should be in a reader

cl_dict :: Dictionary
cl_scripts :: [(ScriptName, Script)]
cl_kernel :: ScopedKernel
cl_initSAST :: SAST
cl_version :: VersionStore


Monad m => MonadState CommandLineState (CLM m)