HERMIT.Shell.Types

Documentation

data QueryFun :: * where

Constructors

QueryString :: Injection a LCoreTC => TransformH a String -> QueryFun

QueryDocH :: Injection a LCoreTC => TransformH a DocH -> QueryFun

QueryPrettyH :: Injection a LCoreTC => PrettyH a -> QueryFun

Diff :: AST -> AST -> QueryFun

Inquiry :: (PluginReader -> CommandLineState -> IO String) -> QueryFun

QueryUnit :: Injection a LCoreTC => TransformH a () -> QueryFun

Instances

Extern QueryFun

Typeable * QueryFun

type Box QueryFun = QueryFun

message :: String -> QueryFun

performQuery :: (MonadCatch m, CLMonad m) => QueryFun -> ExprH -> m ()

ppWholeProgram :: (CLMonad m, MonadCatch m) => AST -> m DocH

type TagName = String

data VersionCmd

Constructors

Back

Step

Goto AST

GotoTag TagName

Tag TagName

Instances

Show VersionCmd

data CLException

Constructors

CLAbort

CLResume AST

CLContinue CommandLineState

CLError String

Instances

Monad m => MonadError CLException (CLT m)

abort :: MonadError CLException m => m a

resume :: MonadError CLException m => AST -> m a

continue :: MonadError CLException m => CommandLineState -> m a

rethrowCLE :: CLException -> PluginM a

rethrowPE :: MonadError CLException m => PException -> m a

newtype CLT m a

This type is similiar to PluginM, except that its exception and state types are supersets of those for PluginM, and it is a transformer. There are two functions: clm and pluginM for converting between the two. The reason we do this is to obtain a clean separation of plugin state from commandline state without nesting state transformers. Nesting StateT leads to a lot of awkward lifting and manual state management in the command line code.

NB: an alternative to monad transformers, like Oleg's Extensible Effects, might be useful here.

Constructors

CLT

Fields

unCLT :: ExceptT CLException (ReaderT PluginReader (StateT CommandLineState m)) a

Instances

MonadTrans CLT

Monad m => MonadError CLException (CLT m)

Monad m => MonadReader PluginReader (CLT m)

Monad m => MonadState CommandLineState (CLT m)

Monad m => Monad (CLT m)

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

Functor m => Functor (CLT m)

(Monad m, Functor m) => Applicative (CLT m)

MonadIO m => MonadIO (CLT m)

MonadException m => MonadException (CLT m)

Monad m => MonadCatch (CLT m)

type CLMonad m = (MonadIO m, MonadState CommandLineState m, MonadReader PluginReader m, MonadError CLException m)

runCLT :: PluginReader -> CommandLineState -> CLT m a -> m (Either CLException a, CommandLineState)

Run a CLT computation.

clm2clt :: CLMonad m => CLT IO a -> m a

Lift a CLT IO computation into a computation in an arbitrary CLMonad.

clm :: CLT IO a -> PluginM a

Lift a CLM computation into the PluginM monad.

pluginM :: CLMonad m => PluginM a -> m a

Lift a PluginM computation into the CLM monad.

data CommandLineState

Constructors

CommandLineState

Fields

cl_pstate :: PluginState

Access to the enclosing plugin state. This is propagated back to the plugin after the CLT computation ends. We do it this way because nested StateT is a pain.

cl_height :: Int

console height, in lines

cl_scripts :: [(ScriptName, Script)]

cl_nav :: Bool

keyboard input the nav panel

cl_foci :: Map AST PathStack

focus assigned to each AST

cl_tags :: Map AST [String]

list of tags on an AST

cl_proofstack :: Map AST [ProofTodo]

stack of todos for the proof shell

cl_window :: PathH

path to beginning of window, always a prefix of focus path in kernel

cl_externals :: [External]

Currently visible externals

cl_running_script :: Maybe Script

Nothing = no script running, otherwise the remaining script commands

cl_safety :: Safety

which level of safety we are running in

cl_templemmas :: TVar [(HermitC, LemmaName, Lemma)]

updated by kernel env with temporary obligations

cl_failhard :: Bool

Any exception will cause an abort.

cl_diffonly :: Bool

Print diffs instead of full focus.

Instances

Extern CommandLineState

Typeable * CommandLineState

Monad m => MonadState CommandLineState (CLT m)

type Box CommandLineState = CLSBox

type PathStack = ([LocalPathH], LocalPathH)

data ProofTodo

Constructors

Unproven

Fields

ptName :: LemmaName

lemma we are proving

ptLemma :: Lemma

ptContext :: HermitC

context in which lemma is being proved

ptPath :: PathStack

path into lemma to focus on

data Safety

Constructors

StrictSafety

NormalSafety

NoSafety

Instances

Eq Safety

Read Safety

Show Safety

Typeable * Safety

filterSafety :: Safety -> [External] -> [External]

cl_corelint :: CommandLineState -> Bool

setCoreLint :: CommandLineState -> Bool -> CommandLineState

cl_cursor :: CommandLineState -> AST

setCursor :: AST -> CommandLineState -> CommandLineState

cl_kernel_env :: CommandLineState -> KernelEnv

cl_pretty :: CommandLineState -> PrettyPrinter

setPretty :: CommandLineState -> PrettyPrinter -> CommandLineState

cl_pretty_opts :: CommandLineState -> PrettyOptions

setPrettyOpts :: CommandLineState -> PrettyOptions -> CommandLineState

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

mkCLS :: PluginM CommandLineState

Create default CommandLineState from PluginState. Note: the dictionary (cl_dict) will be empty, and should be populated if needed.

getTermDimensions :: IO (Int, Int)

newtype CLSBox

Constructors

CLSBox CommandLineState

Instances

Typeable * CLSBox

type ScriptName = String

tick :: TVar (Map String Int) -> String -> IO Int

cl_putStr :: CLMonad m => String -> m ()

cl_putStrLn :: CLMonad m => String -> m ()

isRunningScript :: MonadState CommandLineState m => m Bool

setRunningScript :: MonadState CommandLineState m => Maybe Script -> m ()

putStrToConsole :: CLMonad m => String -> m ()

pathStack2Path :: ([LocalPath crumb], LocalPath crumb) -> Path crumb

data Direction

A primitive means of denoting navigation of a tree (within a local scope).

Constructors

U

Up

T

Top

Instances

Eq Direction

Show Direction

pathStackToLens :: (Injection a g, Walker HermitC g) => [LocalPathH] -> LocalPathH -> LensH a g

getPathStack :: CLMonad m => m ([LocalPathH], LocalPathH)

getFocusPath :: CLMonad m => m PathH

addFocusT :: (Injection a g, Walker HermitC g, CLMonad m) => TransformH g b -> m (TransformH a b)

addFocusR :: (Injection a g, Walker HermitC g, CLMonad m) => RewriteH g -> m (RewriteH a)

addAST :: CLMonad m => AST -> m ()

modifyLocalPath :: (MonadCatch m, CLMonad m) => (LocalPathH -> LocalPathH) -> ExprH -> m ()

requireDifferent :: Monad m => LocalPathH -> LocalPathH -> m ()

copyPathStack :: CLMonad m => AST -> m ()

copyProofStack :: CLMonad m => AST -> m ()

pushProofStack :: CLMonad m => ProofTodo -> m ()

popProofStack :: CLMonad m => m ProofTodo

announceUnprovens :: (MonadCatch m, CLMonad m) => m ()

getProofStack :: CLMonad m => m [ProofTodo]

Always returns a non-empty list.

getProofStackEmpty :: CLMonad m => m [ProofTodo]

fixWindow :: CLMonad m => m ()

showWindow :: (MonadCatch m, CLMonad m) => Maybe Handle -> m ()

showWindowAlways :: (MonadCatch m, CLMonad m) => Maybe Handle -> m ()

printLemma :: (MonadCatch m, CLMonad m) => Handle -> HermitC -> PathStack -> (LemmaName, Lemma) -> m ()

queryInFocus :: (Walker HermitC g, Injection ModGuts g, MonadCatch m, CLMonad m) => TransformH g b -> CommitMsg -> m b

inProofFocusT :: ProofTodo -> TransformH LCoreTC b -> TransformH Core b

inProofFocusR :: ProofTodo -> RewriteH LCoreTC -> TransformH Core Clause

queryInContext :: forall b m. (MonadCatch m, CLMonad m) => TransformH LCoreTC b -> CommitMsg -> m b