proof-assistant-bot-0.2.0: Telegram bot for proof assistants

Safe Haskell	None
Language	Haskell2010

Proof.Assistant.Transport

Synopsis

data Interpreters = Interpreters {
- agda :: !AgdaState
- arend :: !(InterpreterState ArendSettings)
- idris :: !(InterpreterState IdrisSettings)
- coq :: !ExternalState
- lean :: !(InterpreterState LeanSettings)
- rzk :: !InternalState
}
newInterpreters :: InterpretersSettings -> IO Interpreters
type ExternalState = InterpreterState ExternalInterpreterSettings
type InternalState = InterpreterState InternalInterpreterSettings
data BotState = BotState {
- output :: !(TBQueue InterpreterResponse)
- botSettings :: !Settings
- interpreters :: !Interpreters
}
newBotState :: Settings -> IO BotState
readInput :: InterpreterState settings -> IO InterpreterRequest
readOutput :: BotState -> IO InterpreterResponse
writeInput :: InterpreterRequest -> InterpreterState settings -> IO ()
writeOutput :: InterpreterResponse -> BotState -> IO ()

Documentation

data Interpreters Source #

Combination of all supported backend interpreters.

Constructors

Interpreters
Fields agda :: !AgdaState arend :: !(InterpreterState ArendSettings) idris :: !(InterpreterState IdrisSettings) coq :: !ExternalState lean :: !(InterpreterState LeanSettings) rzk :: !InternalState

newInterpreters :: InterpretersSettings -> IO Interpreters Source #

Initiate new interpreters from settings.

type ExternalState = InterpreterState ExternalInterpreterSettings Source #

type InternalState = InterpreterState InternalInterpreterSettings Source #

data BotState Source #

Bot has its own state.

Constructors

BotState
Fields output :: !(TBQueue InterpreterResponse) Queue to read messages from backend interpreters. botSettings :: !Settings Bot settings. interpreters :: !Interpreters All interpreters with their states.

newBotState :: Settings -> IO BotState Source #

Initiate BotState from Settings.

readInput :: InterpreterState settings -> IO InterpreterRequest Source #

Read message from "input" queue.

readOutput :: BotState -> IO InterpreterResponse Source #

Read message from "output" queue.

writeInput :: InterpreterRequest -> InterpreterState settings -> IO () Source #

Write message to "input" queue.

writeOutput :: InterpreterResponse -> BotState -> IO () Source #

Write message to "output" queue.