| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Interaction.State
Synopsis
- data AgdaState = AgdaState {
- interpreterState :: !(InterpreterState AgdaSettings)
- agdaEnvRef :: !(IORef TCEnv)
- agdaStateRef :: !(IORef TCState)
- newAgdaState :: AgdaSettings -> IO AgdaState
- readTCState :: AgdaState -> IO TCState
- writeTCState :: TCState -> AgdaState -> IO ()
- readTCEnv :: AgdaState -> IO TCEnv
- writeTCEnv :: TCEnv -> AgdaState -> IO ()
- runAgda :: AgdaState -> TCM ByteString -> IO ByteString
- catchAgdaError :: MonadTCM m => TCErr -> m ByteString
- setEnv :: AgdaState -> (TCEnv -> TCEnv) -> IO ()
Documentation
Agda has its own env (TCEnv) and state (TCState).
We are using them in combination with communication channel between Agda and bot.
Constructors
| AgdaState | |
Fields
| |
Instances
| Interpreter AgdaState AgdaSettings Source # | |
Defined in Proof.Assistant.Interpreter Methods interpretSafe :: AgdaState -> InterpreterRequest -> IO ByteString Source # getSettings :: AgdaState -> InterpreterState AgdaSettings Source # | |
newAgdaState :: AgdaSettings -> IO AgdaState Source #
Initiate AgdaState from AgdaSettings.
readTCState :: AgdaState -> IO TCState Source #
Helper to get access to TCState.
writeTCState :: TCState -> AgdaState -> IO () Source #
Helper to store new TCState.
writeTCEnv :: TCEnv -> AgdaState -> IO () Source #
Helper to store new TCEnv.
runAgda :: AgdaState -> TCM ByteString -> IO ByteString Source #
Run chosen typechecking action in the typechecking monad (TCM).
catchAgdaError :: MonadTCM m => TCErr -> m ByteString Source #
Catch error from Agda and make it looks pretty.