proof-assistant-bot-0.2.1: Telegram bot for proof assistants
Safe HaskellNone
LanguageHaskell2010

Proof.Assistant.Interpreter

Synopsis

Documentation

runInterpreter :: Interpreter state settings => BotState -> state -> IO () Source #

Main worker function. Reads input from Telegram, calls CLI or API, could be anything. Returns ByteString, wraps it in InterpreterResponse and sends back to Telegram.

class Interpreter state settings | state -> settings where Source #

Worker abstraction over Proof assistant as Interpreter. Could be CLI, Haskell function, network, whatever. It should have the state and associated settings with the state.

Instances

Instances details
Interpreter AgdaState AgdaSettings Source # 
Instance details

Defined in Proof.Assistant.Interpreter

Interpreter InternalState InternalInterpreterSettings Source # 
Instance details

Defined in Proof.Assistant.Interpreter

Interpreter ExternalState ExternalInterpreterSettings Source # 
Instance details

Defined in Proof.Assistant.Interpreter

Interpreter (InterpreterState IdrisSettings) IdrisSettings Source # 
Instance details

Defined in Proof.Assistant.Interpreter

Interpreter (InterpreterState ArendSettings) ArendSettings Source # 
Instance details

Defined in Proof.Assistant.Interpreter

Interpreter (InterpreterState LeanSettings) LeanSettings Source # 
Instance details

Defined in Proof.Assistant.Interpreter

External Interpreter

callExternalInterpreter :: ExternalInterpreterSettings -> (FilePath, FilePath) -> IO ByteString Source #

Call some external CLI application, probably Coq.