Agda.Interaction.State

Documentation

data AgdaState

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

• interpreterState :: !(InterpreterState AgdaSettings)
• agdaEnvRef :: !(IORef TCEnv)
• agdaStateRef :: !(IORef TCState)

Instances

Interpreter AgdaState AgdaSettings

Defined in Proof.Assistant.Interpreter

Methods

interpretSafe :: AgdaState -> InterpreterRequest -> IO ByteString

getSettings :: AgdaState -> InterpreterState AgdaSettings

newAgdaState :: AgdaSettings -> IO AgdaState

Initiate AgdaState from AgdaSettings.

readTCState :: AgdaState -> IO TCState

Helper to get access to TCState.

writeTCState :: TCState -> AgdaState -> IO ()

Helper to store new TCState.

readTCEnv :: AgdaState -> IO TCEnv

Helper to get access to TCEnv.

writeTCEnv :: TCEnv -> AgdaState -> IO ()

Helper to store new TCEnv.

runAgda :: AgdaState -> TCM ByteString -> IO ByteString

Run chosen typechecking action in the typechecking monad (TCM).

catchAgdaError :: MonadTCM m => TCErr -> m ByteString

Catch error from Agda and make it looks pretty.

setEnv :: AgdaState -> (TCEnv -> TCEnv) -> IO ()

Helper to modify TCEnv.