Safe Haskell | None |
---|---|
Language | Haskell2010 |
- data QueryFun :: * where
- 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 :: (CommandLineState -> IO String) -> QueryFun
- QueryUnit :: Injection a LCoreTC => TransformH a () -> 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
- data CLException
- 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 = CLT {
- unCLT :: ExceptT CLException (StateT CommandLineState m) a
- type CLMonad m = (MonadIO m, MonadState CommandLineState m, MonadError CLException m)
- runCLT :: CommandLineState -> CLT m a -> m (Either CLException a, CommandLineState)
- clm2clt :: MonadIO m => CLT IO a -> CLT m a
- clm :: CLT IO a -> PluginM a
- pluginM :: CLMonad m => PluginM a -> m a
- data CommandLineState = CommandLineState {
- cl_pstate :: PluginState
- cl_height :: Int
- cl_scripts :: [(ScriptName, Script)]
- cl_nav :: Bool
- cl_foci :: Map AST PathStack
- cl_tags :: Map AST [String]
- cl_proofstack :: Map AST [ProofTodo]
- cl_window :: PathH
- cl_externals :: [External]
- cl_running_script :: Maybe Script
- cl_safety :: Safety
- type PathStack = ([LocalPathH], LocalPathH)
- data ProofTodo
- data Safety
- filterSafety :: Safety -> [External] -> [External]
- cl_corelint :: CommandLineState -> Bool
- setCoreLint :: CommandLineState -> Bool -> CommandLineState
- cl_cursor :: CommandLineState -> AST
- setCursor :: AST -> CommandLineState -> CommandLineState
- cl_diffonly :: CommandLineState -> Bool
- setDiffOnly :: CommandLineState -> Bool -> CommandLineState
- cl_failhard :: CommandLineState -> Bool
- setFailHard :: CommandLineState -> Bool -> CommandLineState
- cl_kernel :: CommandLineState -> Kernel
- 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
- getTermDimensions :: IO (Int, Int)
- newtype CLSBox = CLSBox CommandLineState
- 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
- 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
- currentLemma :: CLMonad m => m (LemmaName, Lemma, HermitC, [NamedLemma], PathStack)
- announceProven :: (MonadCatch m, CLMonad m) => m ()
- announceUnprovens :: (MonadCatch m, CLMonad m) => m ()
- getProofStack :: CLMonad m => m [ProofTodo]
- getProofStackEmpty :: CLMonad m => m [ProofTodo]
- fixWindow :: CLMonad m => m ()
- showWindow :: (MonadCatch m, CLMonad m) => Maybe Handle -> m ()
- printLemma :: (MonadCatch m, MonadError CLException m, MonadIO m, MonadState CommandLineState 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 Quantified
- withLemmasInScope :: HasLemmas m => [(LemmaName, Lemma)] -> Transform c m a b -> Transform c m a b
- queryInContext :: forall b m. (MonadCatch m, CLMonad m) => TransformH LCoreTC b -> CommitMsg -> m b
Documentation
data QueryFun :: * where Source
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 :: (CommandLineState -> IO String) -> QueryFun | |
QueryUnit :: Injection a LCoreTC => TransformH a () -> QueryFun |
performQuery :: (MonadCatch m, CLMonad m) => QueryFun -> ExprH -> m () Source
ppWholeProgram :: (CLMonad m, MonadCatch m) => AST -> m DocH Source
data CLException Source
Monad m => MonadError CLException (CLT m) |
abort :: MonadError CLException m => m a Source
resume :: MonadError CLException m => AST -> m a Source
continue :: MonadError CLException m => CommandLineState -> m a Source
rethrowCLE :: CLException -> PluginM a Source
rethrowPE :: MonadError CLException m => PException -> m a Source
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.
CLT | |
|
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) | |
MonadException m => MonadException (CLT m) | |
Monad m => MonadCatch (CLT m) |
type CLMonad m = (MonadIO m, MonadState CommandLineState m, MonadError CLException m) Source
runCLT :: CommandLineState -> CLT m a -> m (Either CLException a, CommandLineState) Source
Run a CLT computation.
clm2clt :: MonadIO m => CLT IO a -> CLT m a Source
Lift a CLT IO computation into a CLT computation over an arbitrary MonadIO.
data CommandLineState Source
CommandLineState | |
|
Extern CommandLineState | |
Typeable * CommandLineState | |
Monad m => MonadState CommandLineState (CLT m) | |
type Box CommandLineState = CLSBox |
type PathStack = ([LocalPathH], LocalPathH) Source
Unproven | |
MarkProven | lemma successfully proven, temporary status |
filterSafety :: Safety -> [External] -> [External] Source
cl_cursor :: CommandLineState -> AST Source
setCursor :: AST -> CommandLineState -> CommandLineState Source
cl_render :: CommandLineState -> Handle -> PrettyOptions -> Either String DocH -> IO () Source
mkCLS :: PluginM CommandLineState Source
Create default CommandLineState from PluginState. Note: the dictionary (cl_dict) will be empty, and should be populated if needed.
getTermDimensions :: IO (Int, Int) Source
type ScriptName = String Source
cl_putStrLn :: CLMonad m => String -> m () Source
isRunningScript :: MonadState CommandLineState m => m Bool Source
setRunningScript :: MonadState CommandLineState m => Maybe Script -> m () Source
putStrToConsole :: CLMonad m => String -> m () Source
pathStack2Path :: ([LocalPath crumb], LocalPath crumb) -> Path crumb Source
A primitive means of denoting navigation of a tree (within a local scope).
pathStackToLens :: (Injection a g, Walker HermitC g) => [LocalPathH] -> LocalPathH -> LensH a g Source
getPathStack :: CLMonad m => m ([LocalPathH], LocalPathH) Source
getFocusPath :: CLMonad m => m PathH Source
addFocusT :: (Injection a g, Walker HermitC g, CLMonad m) => TransformH g b -> m (TransformH a b) Source
modifyLocalPath :: (MonadCatch m, CLMonad m) => (LocalPathH -> LocalPathH) -> ExprH -> m () Source
requireDifferent :: Monad m => LocalPathH -> LocalPathH -> m () Source
copyPathStack :: CLMonad m => AST -> m () Source
copyProofStack :: CLMonad m => AST -> m () Source
pushProofStack :: CLMonad m => ProofTodo -> m () Source
popProofStack :: CLMonad m => m ProofTodo Source
currentLemma :: CLMonad m => m (LemmaName, Lemma, HermitC, [NamedLemma], PathStack) Source
announceProven :: (MonadCatch m, CLMonad m) => m () Source
announceUnprovens :: (MonadCatch m, CLMonad m) => m () Source
getProofStack :: CLMonad m => m [ProofTodo] Source
Always returns a non-empty list.
getProofStackEmpty :: CLMonad m => m [ProofTodo] Source
showWindow :: (MonadCatch m, CLMonad m) => Maybe Handle -> m () Source
printLemma :: (MonadCatch m, MonadError CLException m, MonadIO m, MonadState CommandLineState m) => Handle -> HermitC -> PathStack -> (LemmaName, Lemma) -> m () Source
queryInFocus :: (Walker HermitC g, Injection ModGuts g, MonadCatch m, CLMonad m) => TransformH g b -> CommitMsg -> m b Source
inProofFocusT :: ProofTodo -> TransformH LCoreTC b -> TransformH Core b Source
withLemmasInScope :: HasLemmas m => [(LemmaName, Lemma)] -> Transform c m a b -> Transform c m a b Source
queryInContext :: forall b m. (MonadCatch m, CLMonad m) => TransformH LCoreTC b -> CommitMsg -> m b Source