Types in HERMIT

The layers in HERMIT are

• Command Line (CommandLineState, PluginReader, CLException)
• Plugin (PluginState, PluginReader):
• Kernel: raw rewrites or queries on Core; keeps a dictionary of all rewrite results.

Command Line

Command line uses a class, CLMonad. This can be

• An IO action
• CommandLineState (contains the PluginState)
• PluginReader
• CLException

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

data CommandLineState = CommandLineState
    { 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           :: M.Map AST PathStack    -- ^ focus assigned to each AST
    , cl_tags           :: M.Map AST [String]     -- ^ list of tags on an AST
    , cl_proofstack     :: M.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.
    } 

data CLException = CLAbort
                 | CLResume AST
                 | CLContinue CommandLineState -- TODO: needed?
                 | CLError String

Plugin

data PluginState = PluginState
    { ps_cursor         :: AST                                      -- ^ the current AST
    , ps_pretty         :: PrettyPrinter                            -- ^ which pretty printer to use
    , ps_render         :: Handle -> PrettyOptions -> Either String DocH -> IO () -- ^ the way of outputing to the screen
    , ps_tick           :: TVar (M.Map String Int)                  -- ^ the list of ticked messages
    , ps_corelint       :: Bool                                     -- ^ if true, run Core Lint on module after each rewrite
    }

data PluginReader = PluginReader
    { pr_kernel         :: Kernel
    , pr_pass           :: PassInfo
    }

Kernel

Kernel uses a record of update methods to act on, basically, mod-guts.

data Kernel = Kernel
  { -- | Halt the 'Kernel' and return control to GHC, which compiles the specified 'AST'.
    resumeK :: forall m. MonadIO m =>                                   AST -> m ()
    -- | Halt the 'Kernel' and abort GHC without compiling.
  , abortK  :: forall m. MonadIO m =>                                          m ()
    -- | Apply a 'Rewrite' to the specified 'AST' and return a handle to the resulting 'AST'.
  , applyK  :: forall m. (MonadIO m, MonadCatch m)
            => RewriteH ModGuts     -> CommitMsg -> KernelEnv ->        AST -> m AST
    -- | Apply a 'TransformH' to the 'AST', return the resulting value, and potentially a new 'AST'.
  , queryK  :: forall m a. (MonadIO m, MonadCatch m)
            => TransformH ModGuts a -> CommitMsg -> KernelEnv ->        AST -> m (AST,a)
    -- | Delete the internal record of the specified 'AST'.
  , deleteK :: forall m. MonadIO m =>                                   AST -> m ()
    -- | List all the 'AST's tracked by the 'Kernel', including version data.
  , listK   :: forall m. MonadIO m =>                                          m [(AST,Maybe String, Maybe AST)]
    -- | Log a new AST with same Lemmas/ModGuts as given AST.
  , tellK   :: forall m. (MonadIO m, MonadCatch m) => String         -> AST -> m AST
  } 
```

Question: Why does `queryK` return an AST?

## Plan

 * (X) -- to delete 
 * (?) -- Not sure how to remove


Name | Plan | Type | Notes
-----|------|------|------- 
cl_pstate | X        | 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 | X       | Int                    | console height, in lines |
cl_scripts | X       | [(ScriptName, Script)]  | |
cl_nav | X           | Bool                   | keyboard input the nav panel |
cl_foci | ?          | M.Map AST PathStack    | focus assigned to each AST |
cl_tags | ?          | M.Map AST [String]     | list of tags on an AST |
cl_proofstack | ?     | M.Map AST [ProofTodo]  | stack of todos for the proof shell |
cl_window | X     | PathH                  | path to beginning of window, always a prefix of focus path in kernel |
cl_externals | X     | [External]             | Currently visible externals |
cl_running_script | X | 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 | X     | Bool                   | Print diffs instead of full focus. |