HERMIT.Shell.Types

Documentation

data QueryFun :: * where

Constructors

QueryString :: (Injection ModGuts g, Walker HermitC g) => TransformH g String -> QueryFun

QueryDocH :: (PrettyC -> PrettyH CoreTC -> TransformH CoreTC DocH) -> QueryFun

Diff :: SAST -> SAST -> QueryFun

Display :: QueryFun

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

CorrectnessCritera :: (Injection ModGuts g, Walker HermitC g) => TransformH g () -> QueryFun

Instances

Extern QueryFun

Typeable * QueryFun

type Box QueryFun = QueryFun

message :: String -> QueryFun

performQuery :: (MonadCatch m, MonadError CLException m, MonadIO m, MonadState CommandLineState m) => QueryFun -> ExprH -> m ()

ppWholeProgram :: (MonadIO m, MonadState CommandLineState m) => AST -> m DocH

data VersionCmd

Constructors

Back

Step

Goto Int

GotoTag String

AddTag String

Instances

Show VersionCmd

data CLException

Constructors

CLAbort

CLResume SAST

CLContinue CommandLineState

CLError String

Instances

Error CLException

Monad m => MonadError CLException (CLT m)

abort :: MonadError CLException m => m ()

resume :: MonadError CLException m => SAST -> m ()

continue :: MonadError CLException m => CommandLineState -> m ()

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 :: ErrorT CLException (StateT CommandLineState m) a

Instances

MonadTrans CLT

Monad m => MonadError CLException (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)

Monad m => MonadCatch (CLT m)

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

Run a CLT computation.

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

Lift a CLT IO computation into a CLT computation over an arbitrary MonadIO.

clm :: CLT IO a -> PluginM a

Lift a CLM computation into the PluginM monad.

pluginM :: (MonadError CLException m, MonadIO m, MonadState CommandLineState m) => PluginM a -> m a

Lift a PluginM computation into the CLM monad.

data VersionStore

Constructors

VersionStore

Fields

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

vs_tags :: [(String, SAST)]

newSAST :: ExprH -> SAST -> CommandLineState -> CommandLineState

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_lemmas :: [Lemma]

list of lemmas, with flag indicating whether proven

cl_nav :: Bool

keyboard input the nav panel

cl_version :: VersionStore

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 this should be in a reader

cl_initSAST :: SAST

Instances

Extern CommandLineState

Typeable * CommandLineState

Monad m => MonadState CommandLineState (CLT m)

type Box CommandLineState = CLSBox

cl_corelint :: CommandLineState -> Bool

setCoreLint :: CommandLineState -> Bool -> CommandLineState

cl_cursor :: CommandLineState -> SAST

setCursor :: CommandLineState -> SAST -> CommandLineState

cl_diffonly :: CommandLineState -> Bool

setDiffOnly :: CommandLineState -> Bool -> CommandLineState

cl_failhard :: CommandLineState -> Bool

setFailHard :: CommandLineState -> Bool -> CommandLineState

cl_kernel :: CommandLineState -> ScopedKernel

cl_kernel_env :: CommandLineState -> HermitMEnv

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

type LemmaName = String

type Lemma = (LemmaName, CoreExprEquality, Bool)

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

cl_putStr :: (MonadError CLException m, MonadIO m, MonadState CommandLineState m) => String -> m ()

cl_putStrLn :: (MonadError CLException m, MonadIO m, MonadState CommandLineState m) => String -> m ()

isRunningScript :: MonadState CommandLineState m => m Bool

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

putStrToConsole :: (MonadError CLException m, MonadIO m, MonadState CommandLineState m) => String -> m ()

shellComplete :: MVar CommandLineState -> String -> String -> IO [Completion]

data CompletionType

Constructors

ConsiderC

BindingOfC

BindingGroupOfC

RhsOfC

OccurrenceOfC

InlineC

CommandC

AmbiguousC [CompletionType]

Instances

Show CompletionType

completionType :: String -> CompletionType

completionQuery :: CommandLineState -> CompletionType -> IO (TransformH CoreTC [String])

fixWindow :: (MonadError CLException m, MonadIO m, MonadState CommandLineState m) => m ()

showWindow :: (MonadError CLException m, MonadIO m, MonadState CommandLineState m) => m ()

showGraph :: [(SAST, ExprH, SAST)] -> [(String, SAST)] -> SAST -> String