diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,18 @@
+# Revision history for proof-assistant-bot
+
+## 0.2.0 -- 2022-12-10
+
+- Import Agda primitives for every `/(re)load` (see [#21](https://github.com/swamp-agr/proof-assistant-bot/pull/21));
+- Increase timeout for Agda to `60s` (see [#20](https://github.com/swamp-agr/proof-assistant-bot/pull/20));
+- Fix replies in topics (see [#17](https://github.com/swamp-agr/proof-assistant-bot/pull/17), [#18](https://github.com/swamp-agr/proof-assistant-bot/pull/18), [#19](https://github.com/swamp-agr/proof-assistant-bot/pull/19));
+- Rzk support (see [#15](https://github.com/swamp-agr/proof-assistant-bot/pull/15));
+- Arend support (see [#13](https://github.com/swamp-agr/proof-assistant-bot/pull/13), [#14](https://github.com/swamp-agr/proof-assistant-bot/pull/14));
+- Lean 3 support (see [#10](https://github.com/swamp-agr/proof-assistant-bot/pull/10), [#11](https://github.com/swamp-agr/proof-assistant-bot/pull/11), [#12](https://github.com/swamp-agr/proof-assistant-bot/pull/12));
+- Set default timeout for CLI to `5s` (see [#9](https://github.com/swamp-agr/proof-assistant-bot/pull/9));
+- Idris 2 support (see [#7](https://github.com/swamp-agr/proof-assistant-bot/pull/7), [#8]([#7](https://github.com/swamp-agr/proof-assistant-bot/pull/7)));
+- Increase allocation limit for Agda (see [#3](https://github.com/swamp-agr/proof-assistant-bot/pull/3));
+- Add maintenance scripts for `proof-assistant-bot` executable (see [#1](https://github.com/swamp-agr/proof-assistant-bot/pull/1));
+
+## 0.1.0 -- 2022-12-03 (not yet released on Hackage)
+
+- First version. Released on an unsuspecting world.
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,20 @@
+Copyright (c) 2022 Andrey Prokopenko
+
+Permission is hereby granted, free of charge, to any person obtaining
+a copy of this software and associated documentation files (the
+"Software"), to deal in the Software without restriction, including
+without limitation the rights to use, copy, modify, merge, publish,
+distribute, sublicense, and/or sell copies of the Software, and to
+permit persons to whom the Software is furnished to do so, subject
+to the following conditions:
+
+The above copyright notice and this permission notice shall be included
+in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY
+KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE
+WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
+LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
+OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
+WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,376 @@
+# Proof Assistant Bot
+
+1. [Description](#descriprion)
+2. [Installation](#installation)
+ 1. [Coq](#coq)
+ 2. [Agda](#agda)
+ 3. [Idris 2](#idris-2)
+ 4. [Lean](#lean)
+ 5. [Arend](#arend)
+ 6. [Rzk](#rzk)
+3. [Usage](#usage)
+4. [Available instances](#available-instances)
+5. [Acknowledgements](#acknowledgements)
+
+## Description
+
+This bot provides limited Telegram interfaces to following proof assistant programs (in order of implementation):
+
+- Coq
+- Agda
+- Idris 2
+- Lean
+- Arend
+- Rzk
+
+## Installation
+
+1. Bot could be built via following commands:
+
+```bash
+cabal update
+cabal build
+cabal install --overwrite-policy=always
+```
+
+2. To launch bot you need to set environmental variables, see `./config/settings.dhall` for more details.
+
+One of them is `PROOF_ASSISTANT_BOT_TOKEN`. Obtain it via `@BotFather` and set it:
+
+```
+export PROOF_ASSISTANT_BOT_TOKEN="..."
+```
+
+### Coq
+
+1. Install `opam >= 2.1.0`, e.g. [from here](https://ocaml.org/docs/up-and-running#installation-for-unix).
+
+```bash
+cd $HOME
+opam --version
+2.1.3
+```
+
+2. Install `Coq`.
+
+```bash
+cd $HOME
+opam init
+eval $(opam env)
+opam pin add coq 8.16.1
+```
+
+3. Locate `coqtop` and set enviromental variable. Should be similar to:
+
+```
+export COQ_BIN_PATH="$HOME/.opam/default/bin/coqtop"
+```
+
+### Agda
+
+We do not need to worry about `Agda` since it is included in package dependencies. It will be installed automatically. Meantime, Agda standard library should be installed manually.
+
+1. Get `agda-stdlib` from [Github](https://github.com/agda/agda-stdlib/releases/tag/v1.7.1).
+
+2. Unpack archive.
+
+```
+mkdir -p $PROOF_ASSISTANT_BOT_DIR/agda
+cp agda-stdlib-1.7.1.tar.gz $PROOF_ASSISTANT_BOT_DIR/agda
+cd $PROOF_ASSISTANT_BOT_DIR/agda
+tar -xzvf agda-stdlib-1.7.1.tar.gz
+export AGDA_STDLIB_PATH=$PROOF_ASSISTANT_BOT_DIR/agda/agda-stdlib-1.7.1
+```
+
+3. Create file `$HOME/.agda/defaults` with following content:
+
+```
+standard-library
+```
+
+4. Create file `$HOME/.agda/libraries` with following content:
+
+```
+$AGDA_STDLIB_PATH/standard-library.agda-lib
+```
+
+### Idris 2
+
+1. Get `nix` from [nixos.org](https://nixos.org/download.html#download-nix).
+
+2. Install `idris2` via `nix`:
+
+```bash
+nix-env -i idris2
+```
+
+3. Set environmental variable:
+
+```bash
+export IDRIS2_BIN_PATH="$HOME/.nix-profile/bin/idris2"
+```
+
+### Lean
+
+1. Get `nix` from [nixos.org](https://nixos.org/download.html#download-nix).
+
+2. Install `lean` via `nix`:
+
+```bash
+nix-env -i lean
+```
+
+3. Install `leanproject` via `nix`:
+
+```bash
+nix-env -i mathlibtools
+```
+
+4. Run `leanproject new lean`.
+
+5. Set `LEAN_BIN_PATH` environmental variable:
+
+```bash
+export LEAN_BIN_PATH="$HOME/.nix-profile/bin/lean"
+```
+
+6. Set `LEAN_PROJECT_PATH` to the newly created project directory.
+
+### Arend
+
+1. Get `nix` from [nixos.org](https://nixos.org/download.html#download-nix).
+
+2. Get `java` and `openjdk17` via `nix`:
+
+```bash
+nix-env -i openjdk-17.0.4+8
+```
+
+3. Set `JAVA_HOME` environment variable to your openjdk location. You can use `readlink $HOME/.nix-profile/bin/java` and strip `/bin/java` from the end.
+
+4. Create project directory to store arend projects (for different Telegram chats)
+and set `AREND_ROOT_PROJECT_DIR`.
+
+5. Get Arend standard library from [the official site](https://arend-lang.github.io/download#standard-library) and store in `${AREND_ROOT_PROJECT_DIR}/libs`.
+
+6. Point `AREND_STDLIB_PATH` environment variable to the same location as `AREND_ROOT_PROJECT_DIR`.
+
+7. Download [`Arend.jar`](https://github.com/JetBrains/Arend/releases/latest/download/Arend.jar) and set `AREND_PATH` environment variable to its location, e.g.
+
+```bash
+export AREND_PATH="${AREND_ROOT_PROJECT_DIR}/Arend.jar"
+```
+
+### Rzk
+
+No actions required. See `cabal.project` for more details.
+
+## Usage
+
+- Coq supports only typecheck of the user input via `/coq` command. Example:
+
+```coq
+/coq Inductive day : Type :=
+ | monday
+ | tuesday
+ | wednesday
+ | thursday
+ | friday
+ | saturday
+ | sunday.
+
+Definition next_weekday (d:day) : day :=
+ match d with
+ | monday => tuesday
+ | tuesday => wednesday
+ | wednesday => thursday
+ | thursday => friday
+ | friday => monday
+ | saturday => monday
+ | sunday => monday
+ end.
+
+Compute (next_weekday friday).
+
+Compute (next_weekday (next_weekday saturday)).
+
+Example test_next_weekday:
+ (next_weekday (next_weekday saturday)) = tuesday.
+
+Proof. simpl. reflexivity. Qed.
+```
+
+- Agda is available via `/agda` command. Bot supports several subcommands for Agda:
+ - `/agda /load `. E.g.
+
+ ```agda
+ /agda /load import Relation.Binary.PropositionalEquality as Eq
+ open Eq using (_≡_; refl)
+ open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎)
+
+ data ℕ : Set where
+ zero : ℕ
+ suc : ℕ → ℕ
+
+ {-# BUILTIN NATURAL ℕ #-}
+
+ _+_ : ℕ → ℕ → ℕ
+ zero + n = n
+ (suc m) + n = suc (m + n)
+
+ _ : 2 + 3 ≡ 5
+ _ =
+ begin
+ 2 + 3
+ ≡⟨⟩ -- is shorthand for
+ (suc (suc zero)) + (suc (suc (suc zero)))
+ ≡⟨⟩ -- inductive case
+ suc ((suc zero) + (suc (suc (suc zero))))
+ ≡⟨⟩ -- inductive case
+ suc (suc (zero + (suc (suc (suc zero)))))
+ ≡⟨⟩ -- base case
+ suc (suc (suc (suc (suc zero))))
+ ≡⟨⟩ -- is longhand for
+ 5
+ ∎
+ ```
+
+ - `/agda /reload`
+ - `/agda /typeOf `. E.g. `/agda /typeOf suc`.
+ - `/agda `. E.g. `/agda suc zero + suc zero`.
+
+- Idris 2 via `/idris2` command. Bot supports several subcommands for Idris 2:
+ - `/idris2 /load `. E.g.
+
+ ```idris
+ /idris2 /load module Main
+
+ import System.File.ReadWrite
+
+ tryPrint : Either FileError String -> IO ()
+ tryPrint (Left _) = putStrLn "error"
+ tryPrint (Right r) = putStrLn r
+
+ main : IO ()
+ main = do c <- readFile "hello.idr"
+ tryPrint c
+ ```
+
+ - `/idris2 /typeOf `. E.g. `/idris2 /typeOf Nat`.
+ - `/idris2 `. E.g. `/idris2 2 + 3`.
+
+- Lean is available via `/lean` command. Typecheck supported for the user input. Only several modes were tested (calc mode, conv mode, simplifier).
+
+ - Example 1:
+
+ ```lean
+ /lean import data.nat.basic
+
+ variables (a b c d e : ℕ)
+ variable h1 : a = b
+ variable h2 : b = c + 1
+ variable h3 : c = d
+ variable h4 : e = 1 + d
+
+ theorem T : a = e :=
+ calc
+ a = b : h1
+ ... = c + 1 : h2
+ ... = d + 1 : congr_arg _ h3
+ ... = 1 + d : add_comm d (1 : ℕ)
+ ... = e : eq.symm h4
+ ```
+
+ - Example 2:
+
+ ```lean
+ /lean import topology.basic
+
+ #check topological_space
+ ```
+
+ - Example 3:
+
+ ```lean
+ /lean import algebra.group.defs
+
+ variables (G : Type) [group G] (a b c : G)
+
+ example : a * a⁻¹ * 1 * b = b * c * c⁻¹ :=
+ begin
+ simp
+ end
+ ```
+
+- Arend is available via `/arend` command. Only typecheck supported.
+
+ - Example:
+
+ ```arend
+ /arend \func f => 0
+ ```
+
+- Rzk is available via `/rzk` command. Typechecker supported for every language.
+
+ - Example:
+
+ ```rzk
+ /rzk #lang rzk-1
+
+ #def prod : (A : U) -> (B : U) -> U
+ := \A -> \B -> ∑ (x : A), B
+
+ #def isweq : (A : U) -> (B : U) -> (f : (_ : A) -> B) -> U
+ := \A -> \B -> \f ->
+ ∑ (g : (_ : B) -> A),
+ prod ((x : A) -> g (f x) =_{A} x)
+ ((y : B) -> f (g y) =_{B} y)
+
+ #def weq : (A : U) -> (B : U) -> U
+ := \A -> \B -> ∑ (f : (_ : A) -> B), isweq A B f
+
+ #def Theorem-4.1
+ : (I : CUBE)
+ -> (psi : (t : I) -> TOPE)
+ -> (phi : {(t : I) | psi t} -> TOPE)
+ -> (X : U)
+ -> (Y : <{t : I | psi t} -> (x : X) -> U >)
+ -> (f : <{t : I | phi t} -> (x : X) -> Y t x >)
+ -> weq <{t : I | psi t} -> (x : X) -> Y t x [phi t |-> f t]>
+ ((x : X) -> <{t : I | psi t} -> Y t x [phi t |-> f t x]>)
+ := \I -> \psi -> \phi -> \X -> \Y -> \f ->
+ (\k -> \x -> \t -> k t x,
+ (\k -> \{t : I | psi t} -> \x -> (k x) t,
+ (\k -> refl_{k}, \k -> refl_{k})))
+
+ #def Theorem-4.2_uncurry_ext
+ : (I : CUBE)
+ -> (J : CUBE)
+ -> (psi : (t : I) -> TOPE)
+ -> (zeta : (s : J) -> TOPE)
+ -> (X : <{t : I | psi t} -> <{s : J | zeta s} -> U> >)
+ -> (chi : {(t : I) | psi t} -> TOPE)
+ -> (phi : {(s : J) | zeta s} -> TOPE)
+ -> (f : <{(t, s) : I * J | psi t /\ zeta s} -> X t s >)
+ -> (_ : <{t : I | psi t}
+ -> <{s : J | zeta s}
+ -> X t s [chi s |-> f (t, s)]>
+ [phi t |-> \s -> f (t, s)]>)
+ -> <{(t, s) : I * J | psi t /\ zeta s}
+ -> X t s [(phi t /\ zeta s) \/ (psi t /\ chi s) |-> f (t, s)]>
+ := \I -> \J -> \psi -> \zeta -> \X -> \chi -> \phi -> \f ->
+ \k -> \(t, s) -> k t s
+ ```
+
+## Available instances
+
+1. [@ProofBot](https://t.me/ProofAssistantBot) (online)
+2. [@ProofDebugBot](https://t.me/ProofDebugBot) (for debug purpose, offline most of the time)
+
+## Acknowledgements
+
+- PLTT Community
+- Nikolay Kudasov
+- Andrey Borzenkov
+- Matúš Tejiščák
+- My wife
diff --git a/app/Main.hs b/app/Main.hs
new file mode 100644
--- /dev/null
+++ b/app/Main.hs
@@ -0,0 +1,6 @@
+module Main where
+
+import Proof.Assistant.Bot (run)
+
+main :: IO ()
+main = run
diff --git a/proof-assistant-bot.cabal b/proof-assistant-bot.cabal
new file mode 100644
--- /dev/null
+++ b/proof-assistant-bot.cabal
@@ -0,0 +1,93 @@
+cabal-version: 2.4
+name: proof-assistant-bot
+version: 0.2.0
+synopsis: Telegram bot for proof assistants
+description: Bridge between Telegram Bot and several proof assistants.
+ .
+ Currently following proof assistant supported: Agda, Arend, Coq, Idris 2, Lean, Rzk
+ .
+ See README.md for more details.
+category: Dependent types
+homepage: https://github.com/swamp-agr/proof-assistant-bot/
+bug-reports: https://github.com/swamp-agr/proof-assistant-bot/issues
+license: MIT
+license-file: LICENSE
+author: Andrey Prokopenko
+maintainer: persiantiger@yandex.ru
+
+extra-source-files: CHANGELOG.md
+ README.md
+
+library
+ hs-source-dirs: src
+ ghc-options: -Wall
+ default-language: Haskell2010
+ build-depends: base < 4.17
+ , async
+ , bytestring
+ , dhall
+ , directory
+ , filepath
+ , mtl
+ , process
+ , rzk
+ , stm
+ , telegram-bot-simple >= 0.5.2
+ , text
+ , unix
+ , unordered-containers
+ -- interpreters
+ , Agda
+ exposed-modules: Proof.Assistant.Agda
+ , Proof.Assistant.Arend
+ , Proof.Assistant.Idris
+ , Proof.Assistant.Lean
+ , Proof.Assistant.Rzk
+
+ , Proof.Assistant.Bot
+ , Proof.Assistant.Helpers
+ , Proof.Assistant.Interpreter
+ , Proof.Assistant.RefreshFile
+ , Proof.Assistant.Request
+ , Proof.Assistant.ResourceLimit
+ , Proof.Assistant.Response
+ , Proof.Assistant.State
+ , Proof.Assistant.Settings
+ , Proof.Assistant.Transport
+ , Proof.Assistant.Version
+
+ , Agda.Interaction.Command
+ , Agda.Interaction.Command.EvalIn
+ , Agda.Interaction.Command.EvalTerm
+ , Agda.Interaction.Command.GiveMeta
+ , Agda.Interaction.Command.Internal.Parser
+ , Agda.Interaction.Command.RefineMeta
+ , Agda.Interaction.Command.Reload
+ , Agda.Interaction.Command.RetryConstraints
+ , Agda.Interaction.Command.ShowConstraints
+ , Agda.Interaction.Command.ShowContext
+ , Agda.Interaction.Command.ShowMetas
+ , Agda.Interaction.Command.ShowScope
+ , Agda.Interaction.Command.TypeIn
+ , Agda.Interaction.Command.TypeOf
+ , Agda.Interaction.State
+
+ , Idris.Interaction.Command
+ autogen-modules:
+ Paths_proof_assistant_bot
+ other-modules:
+ Paths_proof_assistant_bot
+
+executable proof-assistant-bot
+ main-is: Main.hs
+
+ -- Modules included in this executable, other than Main.
+ -- other-modules:
+
+ -- LANGUAGE extensions used by modules in this package.
+ -- other-extensions:
+ build-depends: base ^>=4.14.3.0
+ , proof-assistant-bot
+ hs-source-dirs: app
+ ghc-options: -Wall -O2 -threaded -rtsopts -with-rtsopts=-N
+ default-language: Haskell2010
diff --git a/src/Agda/Interaction/Command.hs b/src/Agda/Interaction/Command.hs
new file mode 100644
--- /dev/null
+++ b/src/Agda/Interaction/Command.hs
@@ -0,0 +1,99 @@
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE FlexibleContexts #-}
+
+module Agda.Interaction.Command where
+
+import Data.ByteString (ByteString)
+import Data.HashMap.Strict (HashMap)
+import GHC.Generics (Generic)
+import System.FilePath
+
+import Agda.Interaction.Command.EvalIn
+import Agda.Interaction.Command.EvalTerm
+import Agda.Interaction.Command.GiveMeta
+import Agda.Interaction.Command.RefineMeta
+import Agda.Interaction.Command.Reload
+import Agda.Interaction.Command.RetryConstraints
+import Agda.Interaction.Command.ShowConstraints
+import Agda.Interaction.Command.ShowContext
+import Agda.Interaction.Command.ShowMetas
+import Agda.Interaction.Command.ShowScope
+import Agda.Interaction.Command.TypeOf
+import Agda.Interaction.Command.TypeIn
+
+import Agda.Interaction.State
+import Agda.TypeChecking.Monad.Base (TCEnv (..), TCM)
+import Agda.Utils.FileName (AbsolutePath, filePath)
+
+import qualified Data.ByteString.Char8 as BS8
+import qualified Data.HashMap.Strict as HashMap
+
+-- | Supported sub-commands for Agda.
+data AgdaCommand
+ = Reload | Help | Constraints | Context | Give | Refine | Meta | Load
+ | Eval | TypeOf | TypeIn | WakeUp | Scope
+ deriving (Eq, Show, Generic)
+
+-- | Map of supported Agda sub-commands. We use it instead of parser.
+supportedCommands :: HashMap ByteString AgdaCommand
+supportedCommands = HashMap.fromList
+ [ (,) "/reload" Reload
+ , (,) "/?" Help
+ , (,) "/constraints" Constraints
+ , (,) "/context" Context
+ , (,) "/give" Give
+ , (,) "/refine" Refine
+ , (,) "/meta" Meta
+ , (,) "/load" Load
+ , (,) "/eval" Eval
+ , (,) "/typeOf" TypeOf
+ , (,) "/typeIn" TypeIn
+ , (,) "/wakeup" WakeUp
+ , (,) "/scope" Scope
+ ]
+
+-- | Check user input to identify 'AgdaCommand'.
+matchSupported :: ByteString -> Maybe AgdaCommand
+matchSupported = (`HashMap.lookup` supportedCommands)
+
+-- | Choose an action based on either 'AgdaCommand' or raw input.
+chooseCommand :: AgdaState -> Either () AgdaCommand -> ByteString -> IO (TCM ByteString)
+chooseCommand _state (Left _) input = pure (evalTerm input)
+chooseCommand state (Right cmd) input = do
+ mfilePath <- envCurrentPath <$> readTCEnv state
+ case cmd of
+ Constraints -> pure (showConstraints (BS8.words input))
+ Context -> pure (showContext (BS8.words input))
+ Give -> pure (giveMeta (BS8.words input))
+ Refine -> pure (refineMeta (BS8.words input))
+ Scope -> pure showScope
+ Meta -> pure (showMetas (BS8.words input))
+ Load -> case mfilePath of
+ Nothing -> pure (pure "Failed to load.")
+ Just filepath -> do
+ storeRequestContent filepath input
+ pure $ reload (Just filepath)
+ Reload -> pure (reload mfilePath)
+ WakeUp -> pure retryConstraints
+ TypeOf -> pure (typeOf (BS8.words input))
+ TypeIn -> pure (typeIn (BS8.words input))
+ Eval -> pure (evalIn (BS8.words input))
+ _ -> pure (pure tbd)
+ where
+ tbd = BS8.unwords
+ [ "Command"
+ , BS8.pack (show cmd)
+ , "is not supported yet."
+ ]
+
+-- | Store raw user input in the file given by 'TCEnv'.
+storeRequestContent :: AbsolutePath -> ByteString -> IO ()
+storeRequestContent absFilepath content = do
+ let moduleName = (BS8.pack . dropExtension . takeFileName . filePath) absFilepath
+ moduleContent = BS8.unlines
+ [ BS8.unwords [ "module", moduleName, "where" ]
+ , ""
+ , content
+ ]
+ BS8.writeFile (filePath absFilepath) moduleContent
diff --git a/src/Agda/Interaction/Command/EvalIn.hs b/src/Agda/Interaction/Command/EvalIn.hs
new file mode 100644
--- /dev/null
+++ b/src/Agda/Interaction/Command/EvalIn.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE OverloadedStrings #-}
+module Agda.Interaction.Command.EvalIn where
+
+import Agda.Interaction.Base (ComputeMode (..))
+import Agda.Interaction.BasicOps (evalInCurrent)
+import Agda.Syntax.Abstract.Pretty (prettyA)
+import Agda.TypeChecking.Monad.Base (TCM)
+import Agda.Utils.Pretty (prettyShow)
+import Data.ByteString (ByteString)
+
+import Agda.Interaction.Command.Internal.Parser
+import Proof.Assistant.Helpers (toBS)
+
+evalIn :: [ByteString] -> TCM ByteString
+evalIn s | length s >= 2 =
+ do d <- actOnMeta s $ \_ e -> prettyA =<< evalInCurrent DefaultCompute e
+ pure . toBS . prettyShow $ d
+evalIn _ = pure ":eval metaid expr"
diff --git a/src/Agda/Interaction/Command/EvalTerm.hs b/src/Agda/Interaction/Command/EvalTerm.hs
new file mode 100644
--- /dev/null
+++ b/src/Agda/Interaction/Command/EvalTerm.hs
@@ -0,0 +1,21 @@
+module Agda.Interaction.Command.EvalTerm where
+
+import Agda.Interaction.Command.Internal.Parser
+
+import Agda.Interaction.Base (ComputeMode (..))
+import Agda.Interaction.BasicOps hiding (parseExpr)
+import Agda.TypeChecking.Monad.Base (TCM)
+import Agda.TypeChecking.Pretty (prettyTCM)
+import Agda.Utils.Pretty (prettyShow)
+import Proof.Assistant.Helpers (toBS)
+
+import Data.ByteString (ByteString)
+
+import qualified Data.ByteString.Char8 as BS8
+
+evalTerm :: ByteString -> TCM ByteString
+evalTerm s = do
+ e <- parseExpr (BS8.unpack s)
+ v <- evalInCurrent DefaultCompute e
+ r <- prettyTCM v
+ pure . toBS $ prettyShow r
diff --git a/src/Agda/Interaction/Command/GiveMeta.hs b/src/Agda/Interaction/Command/GiveMeta.hs
new file mode 100644
--- /dev/null
+++ b/src/Agda/Interaction/Command/GiveMeta.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE OverloadedStrings #-}
+module Agda.Interaction.Command.GiveMeta where
+
+import Agda.TypeChecking.Monad.Base (TCM)
+import Agda.TypeChecking.Pretty (prettyTCM)
+import Agda.Utils.Pretty (prettyShow)
+import Data.ByteString (ByteString)
+
+import Agda.Interaction.Base (UseForce (..))
+import Agda.Interaction.BasicOps (give)
+import Agda.Interaction.Command.Internal.Parser
+import Proof.Assistant.Helpers (toBS)
+
+giveMeta :: [ByteString] -> TCM ByteString
+giveMeta s | length s >= 2 = do
+ expr <- actOnMeta s $ \ ii e -> give WithoutForce ii Nothing e
+ r <- prettyTCM expr
+ pure $ toBS $ prettyShow r
+giveMeta _ = pure $ "give" <> " metaid expr"
diff --git a/src/Agda/Interaction/Command/Internal/Parser.hs b/src/Agda/Interaction/Command/Internal/Parser.hs
new file mode 100644
--- /dev/null
+++ b/src/Agda/Interaction/Command/Internal/Parser.hs
@@ -0,0 +1,47 @@
+module Agda.Interaction.Command.Internal.Parser where
+
+import Agda.Syntax.Abstract (Expr)
+import Agda.Syntax.Common (InteractionId (..))
+import Agda.Syntax.Parser (exprParser, parse, parsePosString)
+import Agda.Syntax.Position (getRange, noRange, rStart)
+import Agda.Syntax.Translation.ConcreteToAbstract (concreteToAbstract, localToAbstract)
+import Agda.TypeChecking.Monad.Base
+import Agda.TypeChecking.Monad.MetaVars (lookupInteractionId, lookupMeta, withInteractionId)
+import Agda.TypeChecking.Warnings (runPM)
+import Agda.Utils.Impossible (__IMPOSSIBLE__)
+import Agda.Utils.Pretty (text)
+import Control.Monad.Except (MonadError(..))
+import Data.ByteString (ByteString)
+import Data.Maybe (fromMaybe)
+import Text.Read (readMaybe)
+
+import qualified Data.ByteString.Char8 as BS8
+
+metaParseExpr :: InteractionId -> ByteString -> TCM Expr
+metaParseExpr ii s =
+ do m <- lookupInteractionId ii
+ scope <- getMetaScope <$> lookupMeta m
+ r <- getRange <$> lookupMeta m
+ -- liftIO $ putStrLn $ prettyShow scope
+ let pos = fromMaybe (__IMPOSSIBLE__) (rStart r)
+ e <- runPM $ parsePosString exprParser pos (BS8.unpack s)
+ concreteToAbstract scope e
+
+actOnMeta :: [ByteString] -> (InteractionId -> Expr -> TCM a) -> TCM a
+actOnMeta (is:es) f =
+ do i <- readM (BS8.unpack is)
+ let ii = InteractionId i
+ e <- metaParseExpr ii (BS8.unwords es)
+ withInteractionId ii $ f ii e
+actOnMeta _ _ = __IMPOSSIBLE__
+
+parseExpr :: String -> TCM Expr
+parseExpr s = do
+ e <- runPM $ parse exprParser s
+ localToAbstract e return
+
+readM :: Read a => String -> TCM a
+readM s = maybe err return $ readMaybe s
+ where
+ err = throwError $ strMsg $ "Cannot parse: " ++ s
+ strMsg = Exception noRange . text
diff --git a/src/Agda/Interaction/Command/RefineMeta.hs b/src/Agda/Interaction/Command/RefineMeta.hs
new file mode 100644
--- /dev/null
+++ b/src/Agda/Interaction/Command/RefineMeta.hs
@@ -0,0 +1,18 @@
+module Agda.Interaction.Command.RefineMeta where
+
+import Agda.TypeChecking.Monad.Base (TCM)
+import Agda.TypeChecking.Pretty (prettyTCM)
+import Agda.Utils.Pretty (prettyShow)
+import Data.ByteString (ByteString)
+
+import Agda.Interaction.Base (UseForce (..))
+import Agda.Interaction.BasicOps (refine)
+import Agda.Interaction.Command.Internal.Parser
+import Proof.Assistant.Helpers (toBS)
+
+refineMeta :: [ByteString] -> TCM ByteString
+refineMeta s | length s >= 2 = do
+ expr <- actOnMeta s $ \ ii e -> refine WithoutForce ii Nothing e
+ r <- prettyTCM expr
+ pure $ toBS $ prettyShow r
+refineMeta _ = pure $ toBS $ ": refine" <> " metaid expr"
diff --git a/src/Agda/Interaction/Command/Reload.hs b/src/Agda/Interaction/Command/Reload.hs
new file mode 100644
--- /dev/null
+++ b/src/Agda/Interaction/Command/Reload.hs
@@ -0,0 +1,47 @@
+{-# LANGUAGE OverloadedStrings #-}
+module Agda.Interaction.Command.Reload where
+
+import Agda.Interaction.Imports
+ ( CheckResult, Mode (..), crInterface, crMode, crWarnings
+ , typeCheckMain, parseSource
+ )
+import Agda.Interaction.FindFile (SourceFile (..))
+import Agda.Interaction.Options (optOnlyScopeChecking)
+import Agda.Syntax.Translation.ConcreteToAbstract (importPrimitives)
+import Agda.TypeChecking.Errors (applyFlagsToTCWarnings, prettyError)
+import Agda.TypeChecking.Monad.Base
+ (ModuleCheckMode (..), TypeError (..), TCM, commandLineOptions, iInsideScope, typeError)
+import Agda.TypeChecking.Monad.State (setScope)
+import Agda.Utils.FileName (AbsolutePath)
+import Agda.Utils.Null (unlessNullM)
+import Control.Monad.Except (MonadError(..), unless)
+import Data.ByteString (ByteString)
+
+import Proof.Assistant.Helpers (toBS)
+
+reload :: Maybe AbsolutePath -> TCM ByteString
+reload Nothing = pure "Failed to type check."
+reload (Just file) = do
+ checked <- checkFile file
+ setScope $ iInsideScope (crInterface checked)
+ _ <- importPrimitives
+ pure "Type checked succesfully."
+ `catchError` \e -> do
+ s <- prettyError e
+ pure $ "Failed. " <> toBS s
+
+checkFile :: AbsolutePath -> TCM CheckResult
+checkFile inputFile = do
+ opts <- commandLineOptions
+ let mode =
+ if optOnlyScopeChecking opts
+ then ScopeCheck
+ else TypeCheck
+
+ result <- typeCheckMain mode =<< parseSource (SourceFile inputFile)
+
+ unless (crMode result == ModuleScopeChecked) $
+ unlessNullM (applyFlagsToTCWarnings (crWarnings result)) $ \ ws ->
+ typeError $ NonFatalErrors ws
+
+ pure result
diff --git a/src/Agda/Interaction/Command/RetryConstraints.hs b/src/Agda/Interaction/Command/RetryConstraints.hs
new file mode 100644
--- /dev/null
+++ b/src/Agda/Interaction/Command/RetryConstraints.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE OverloadedStrings #-}
+module Agda.Interaction.Command.RetryConstraints where
+
+import Agda.TypeChecking.Constraints (wakeupConstraints_)
+import Agda.TypeChecking.Monad.Base (TCM)
+import Data.ByteString (ByteString)
+
+retryConstraints :: TCM ByteString
+retryConstraints = wakeupConstraints_ >> pure "Awaken."
diff --git a/src/Agda/Interaction/Command/ShowConstraints.hs b/src/Agda/Interaction/Command/ShowConstraints.hs
new file mode 100644
--- /dev/null
+++ b/src/Agda/Interaction/Command/ShowConstraints.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE OverloadedStrings #-}
+module Agda.Interaction.Command.ShowConstraints where
+
+import Agda.Interaction.BasicOps (getConstraints)
+import Agda.TypeChecking.Monad.Base (TCM)
+import Agda.Utils.Pretty (prettyShow)
+import Data.ByteString (ByteString)
+
+import qualified Data.ByteString.Char8 as BS8
+import qualified Data.List as List
+
+showConstraints :: [ByteString] -> TCM ByteString
+showConstraints = \case
+ [] -> constraints
+ [""] -> constraints
+ _ -> pure "/agda constraints [cid]"
+ where
+ constraintToBS = BS8.pack . unlines . List.map prettyShow
+ constraints = getConstraints >>= pure . constraintToBS
+
diff --git a/src/Agda/Interaction/Command/ShowContext.hs b/src/Agda/Interaction/Command/ShowContext.hs
new file mode 100644
--- /dev/null
+++ b/src/Agda/Interaction/Command/ShowContext.hs
@@ -0,0 +1,37 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE OverloadedStrings #-}
+module Agda.Interaction.Command.ShowContext where
+
+import Agda.Interaction.Command.Internal.Parser
+import Agda.Syntax.Common (InteractionId (..), argNameToString)
+import Agda.TypeChecking.Monad.Base (TCM, getMetaInfo)
+import Agda.TypeChecking.Monad.Context (getContextTelescope)
+import Agda.TypeChecking.Monad.MetaVars (lookupInteractionId, lookupMeta, withMetaInfo)
+import Agda.TypeChecking.Pretty (prettyTCM)
+import Agda.TypeChecking.Reduce (normalise)
+import Agda.TypeChecking.Substitute.Class (raise)
+import Agda.Utils.Pretty ((<+>), render, text)
+import Control.Monad.Except (zipWithM)
+import Data.ByteString (ByteString)
+
+import qualified Agda.Syntax.Internal as I
+import qualified Data.ByteString.Char8 as BS8
+import qualified Data.List as List
+
+showContext :: [ByteString] -> TCM ByteString
+showContext (meta:args) = do
+ i <- InteractionId <$> readM (BS8.unpack meta)
+ mi <- lookupMeta =<< lookupInteractionId i
+ BS8.unlines <$> withMetaInfo (getMetaInfo mi) displayMore
+ where
+ display (x, t) n = do
+ t0 <- case args of
+ ["normal"] -> normalise $ raise n t
+ _ -> return $ raise n t
+ d <- prettyTCM t0
+ pure $ BS8.pack $ render $ text (argNameToString x) <+> ":" <+> d
+ displayMore = do
+ ctx <- List.map I.unDom . I.telToList <$> getContextTelescope
+ zipWithM display ctx $ reverse $ zipWith const [1..] ctx
+showContext _ = pure "context meta"
+
diff --git a/src/Agda/Interaction/Command/ShowMetas.hs b/src/Agda/Interaction/Command/ShowMetas.hs
new file mode 100644
--- /dev/null
+++ b/src/Agda/Interaction/Command/ShowMetas.hs
@@ -0,0 +1,65 @@
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE FlexibleContexts #-}
+module Agda.Interaction.Command.ShowMetas where
+
+import Agda.Interaction.Base (OutputConstraint (..), OutputForm (..), Rewrite (..))
+import Agda.Interaction.BasicOps
+ (outputFormId, typeOfMeta, typesOfHiddenMetas, typesOfVisibleMetas)
+import Agda.Syntax.Abstract.Pretty (prettyA)
+import Agda.Syntax.Common (InteractionId (..))
+import Agda.Syntax.Position (noRange)
+import Agda.TypeChecking.Monad.Base (TCM, nmid)
+import Agda.TypeChecking.Monad.MetaVars
+ (getInteractionRange, getMetaRange, withInteractionId, withMetaId)
+import Agda.Utils.Impossible (__IMPOSSIBLE__)
+import Agda.Utils.Pretty (prettyShow, render)
+import Data.ByteString (ByteString)
+
+import Agda.Interaction.Command.Internal.Parser
+import Proof.Assistant.Helpers (toBS)
+
+import qualified Agda.Syntax.Internal as I
+import qualified Data.ByteString.Char8 as BS8
+
+showMetas :: [ByteString] -> TCM ByteString
+showMetas [m] =
+ do i <- InteractionId <$> readM (BS8.unpack m)
+ withInteractionId i $ do
+ s <- typeOfMeta AsIs i
+ r <- getInteractionRange i
+ d <- prettyA s
+ pure $ toBS $ render d ++ " " ++ prettyShow r
+showMetas [m,"normal"] =
+ do i <- InteractionId <$> readM (BS8.unpack m)
+ withInteractionId i $ do
+ s <- prettyA =<< typeOfMeta Normalised i
+ r <- getInteractionRange i
+ pure $ toBS $ render s ++ " " ++ prettyShow r
+showMetas [] =
+ do interactionMetas <- typesOfVisibleMetas AsIs
+ hiddenMetas <- typesOfHiddenMetas AsIs
+ shownInteractionMetas <- mapM printII interactionMetas
+ shownHiddenMetas <- mapM printM hiddenMetas
+ pure $ BS8.unlines
+ [ "Interaction metas: " <> BS8.unwords shownInteractionMetas
+ , ""
+ , "Hidden metas: " <> BS8.unwords shownHiddenMetas
+ ]
+ where
+ showII o = withInteractionId (outputFormId $ OutputForm noRange [] I.alwaysUnblock o) $ prettyA o
+ showM o = withMetaId (nmid $ outputFormId $ OutputForm noRange [] I.alwaysUnblock o) $ prettyA o
+
+ metaId (OfType i _) = i
+ metaId (JustType i) = i
+ metaId (JustSort i) = i
+ metaId (Assign i _e) = i
+ metaId _ = __IMPOSSIBLE__
+ printM x = do
+ r <- getMetaRange $ nmid $ metaId x
+ d <- showM x
+ pure $ toBS $ render d ++ " [ at " ++ prettyShow r ++ " ]"
+ printII x = do
+ d <- showII x
+ pure $ toBS $ render d
+showMetas _ = pure ":meta [metaid]"
+
diff --git a/src/Agda/Interaction/Command/ShowScope.hs b/src/Agda/Interaction/Command/ShowScope.hs
new file mode 100644
--- /dev/null
+++ b/src/Agda/Interaction/Command/ShowScope.hs
@@ -0,0 +1,13 @@
+module Agda.Interaction.Command.ShowScope where
+
+import Agda.TypeChecking.Monad.Base (TCM)
+import Agda.TypeChecking.Monad.State (getScope)
+import Agda.Utils.Pretty (prettyShow)
+import Data.ByteString (ByteString)
+
+import Proof.Assistant.Helpers (toBS)
+
+showScope :: TCM ByteString
+showScope = do
+ scope <- getScope
+ pure . toBS $ prettyShow scope
diff --git a/src/Agda/Interaction/Command/TypeIn.hs b/src/Agda/Interaction/Command/TypeIn.hs
new file mode 100644
--- /dev/null
+++ b/src/Agda/Interaction/Command/TypeIn.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE OverloadedStrings #-}
+module Agda.Interaction.Command.TypeIn where
+
+import Agda.Interaction.Base (Rewrite (..))
+import Agda.Interaction.BasicOps (typeInMeta)
+import Agda.TypeChecking.Monad.Base (TCM)
+import Agda.TypeChecking.Pretty (prettyTCM)
+import Agda.Utils.Pretty (prettyShow)
+import Data.ByteString (ByteString)
+
+import Agda.Interaction.Command.Internal.Parser
+import Proof.Assistant.Helpers (toBS)
+
+typeIn :: [ByteString] -> TCM ByteString
+typeIn s@(_:_:_) =
+ actOnMeta s $ \i e ->
+ do e1 <- typeInMeta i Normalised e
+ _e2 <- typeInMeta i AsIs e
+ r <- prettyTCM e1
+ pure . toBS $ prettyShow r
+
+typeIn _ = pure ":typeIn meta expr"
diff --git a/src/Agda/Interaction/Command/TypeOf.hs b/src/Agda/Interaction/Command/TypeOf.hs
new file mode 100644
--- /dev/null
+++ b/src/Agda/Interaction/Command/TypeOf.hs
@@ -0,0 +1,21 @@
+module Agda.Interaction.Command.TypeOf where
+
+import Agda.Interaction.Base (Rewrite (..))
+import Agda.Interaction.BasicOps (typeInCurrent)
+import Agda.TypeChecking.Monad.Base (TCM)
+import Agda.TypeChecking.Pretty (prettyTCM)
+import Agda.Utils.Pretty (prettyShow)
+import Data.ByteString (ByteString)
+
+import Agda.Interaction.Command.Internal.Parser
+import Proof.Assistant.Helpers (toBS)
+
+import qualified Data.ByteString.Char8 as BS8
+
+typeOf :: [ByteString] -> TCM ByteString
+typeOf s =
+ do e <- parseExpr (BS8.unpack $ BS8.unwords s)
+ _e0 <- typeInCurrent Normalised e
+ e1 <- typeInCurrent AsIs e
+ r <- prettyTCM e1
+ pure . toBS $ prettyShow r
diff --git a/src/Agda/Interaction/State.hs b/src/Agda/Interaction/State.hs
new file mode 100644
--- /dev/null
+++ b/src/Agda/Interaction/State.hs
@@ -0,0 +1,77 @@
+{-# LANGUAGE RecordWildCards #-}
+
+module Agda.Interaction.State where
+
+import Agda.Interaction.Options
+import Agda.Syntax.Translation.ConcreteToAbstract (importPrimitives)
+import Agda.TypeChecking.Errors (prettyError)
+import Agda.TypeChecking.Monad.Base
+import Agda.TypeChecking.Monad.Options (setCommandLineOptions)
+import Control.Monad.Except (MonadError(..))
+import Data.ByteString (ByteString)
+import Data.IORef (IORef, newIORef, readIORef, atomicWriteIORef, atomicModifyIORef')
+import System.Directory (getTemporaryDirectory, withCurrentDirectory)
+
+import Proof.Assistant.Helpers (toBS)
+import Proof.Assistant.Settings
+import Proof.Assistant.State
+
+-- | Agda has its own env ('TCEnv') and state ('TCState').
+-- We are using them in combination with communication channel between Agda and bot.
+data AgdaState = AgdaState
+ { interpreterState :: !(InterpreterState AgdaSettings)
+ , agdaEnvRef :: !(IORef TCEnv)
+ , agdaStateRef :: !(IORef TCState)
+ }
+
+-- | Initiate 'AgdaState' from 'AgdaSettings'.
+newAgdaState :: AgdaSettings -> IO AgdaState
+newAgdaState settings = do
+ interpreterState <- newInterpreterState $ settings
+ let state0 = initState
+ env = initEnv
+ tmpDir <- getTemporaryDirectory
+ (_, state1) <- withCurrentDirectory tmpDir
+ $ runTCM env state0
+ $ setCommandLineOptions defaultOptions >> importPrimitives
+
+ agdaStateRef <- newIORef state1
+ agdaEnvRef <- newIORef env
+ pure AgdaState {..}
+
+-- | Helper to get access to 'TCState'.
+readTCState :: AgdaState -> IO TCState
+readTCState = readIORef . agdaStateRef
+
+-- | Helper to store new 'TCState'.
+writeTCState :: TCState -> AgdaState -> IO ()
+writeTCState tcState state = atomicWriteIORef (agdaStateRef state) $! tcState
+
+-- | Helper to get access to 'TCEnv'.
+readTCEnv :: AgdaState -> IO TCEnv
+readTCEnv = readIORef . agdaEnvRef
+
+-- | Helper to store new 'TCEnv'.
+writeTCEnv :: TCEnv -> AgdaState -> IO ()
+writeTCEnv tcEnv state = atomicWriteIORef (agdaEnvRef state) $! tcEnv
+
+-- | Run chosen typechecking action in the typechecking monad ('TCM').
+runAgda :: AgdaState -> TCM ByteString -> IO ByteString
+runAgda as action = do
+ tcState <- readTCState as
+ tcEnv <- readTCEnv as
+ (response, newTCState) <- runTCM tcEnv tcState (action `catchError` catchAgdaError)
+ writeTCState newTCState as
+ pure response
+
+-- | Catch error from Agda and make it looks pretty.
+catchAgdaError :: MonadTCM m => TCErr -> m ByteString
+catchAgdaError e = do
+ s <- prettyError e
+ return $ toBS s
+
+-- | Helper to modify 'TCEnv'.
+setEnv :: AgdaState -> (TCEnv -> TCEnv) -> IO ()
+setEnv state modifier =
+ let modify st = (modifier st, ())
+ in atomicModifyIORef' (agdaEnvRef state) $ modify
diff --git a/src/Idris/Interaction/Command.hs b/src/Idris/Interaction/Command.hs
new file mode 100644
--- /dev/null
+++ b/src/Idris/Interaction/Command.hs
@@ -0,0 +1,94 @@
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RecordWildCards #-}
+
+module Idris.Interaction.Command where
+
+import Data.ByteString (ByteString)
+import Data.Char (isSpace)
+import Data.Coerce (coerce)
+import Data.Text (unpack)
+import Data.HashMap.Strict (HashMap)
+import GHC.Generics (Generic)
+import System.Directory
+import System.FilePath (takeFileName)
+import System.Exit (ExitCode (..))
+import System.Process (readProcessWithExitCode)
+
+import Proof.Assistant.Helpers
+import Proof.Assistant.RefreshFile
+import Proof.Assistant.Request
+import Proof.Assistant.Settings
+
+import qualified Data.ByteString.Char8 as BS8
+import qualified Data.HashMap.Strict as HashMap
+
+-- | Supported sub-commands for Idris 2.
+data IdrisCommand
+ = Load | TypeOf | Help
+ deriving (Eq, Show, Generic)
+
+-- | Map of supported Idris 2 sub-commands. We use it instead of parser.
+supportedCommands :: HashMap ByteString IdrisCommand
+supportedCommands = HashMap.fromList
+ [ (,) "/load" Load
+ , (,) "/?" Help
+ , (,) "/typeOf" TypeOf
+ ]
+
+-- | Check user input to identify 'IdrisCommand'.
+matchSupported :: ByteString -> Maybe IdrisCommand
+matchSupported = (`HashMap.lookup` supportedCommands)
+
+-- | Choose an action based on either 'IdrisCommand' or raw input.
+chooseCommand
+ :: ExternalInterpreterSettings
+ -> InterpreterRequest
+ -> Either () IdrisCommand -> ByteString -> IO (IO (ExitCode, String, String))
+chooseCommand settings request ecmd input = case ecmd of
+ Left () ->
+ withResource settings request
+ $ runProcess settings (BS8.unpack $ validateCmd input) . takeFileName
+ Right cmd -> case cmd of
+ Load -> do
+ (dir, path) <- refreshTmpFile settings request Nothing
+ pure $ withCurrentDirectory dir $ runProcess settings "main" (takeFileName path)
+ TypeOf ->
+ withResource settings request
+ $ runProcess settings (":ti " <> BS8.unpack input) . takeFileName
+ Help -> pure $ textResponse "TBD"
+
+-- | Helper to wrap given text as stdout.
+textResponse :: String -> IO (ExitCode, String, String)
+textResponse txt = pure (ExitSuccess, txt, "")
+
+-- | Wrapper around temp directory that will try to identify whether associated file exists.
+-- And if file exists given action will be performed.
+withResource
+ :: ExternalInterpreterSettings
+ -> InterpreterRequest
+ -> (FilePath -> IO (ExitCode, String, String))
+ -> IO (IO (ExitCode, String, String))
+withResource settings request action = do
+ tmpDir <- getTemporaryDirectory
+ let path = getTempFilePath settings request tmpDir
+ pure $ withCurrentDirectory tmpDir $ do
+ exist <- doesFileExist path
+ if exist
+ then action path
+ else textResponse "Not found"
+
+-- | Wrapper around CLI execution.
+runProcess :: ExternalInterpreterSettings -> String -> FilePath -> IO (ExitCode, String, String)
+runProcess ExternalInterpreterSettings{..} input path =
+ readProcessWithExitCode (t2s executable) fullArgs ""
+ where
+ fullArgs = (unpack <$> coerce args) <> [input, path]
+
+-- | We are trying to filter out some potentially dangerous operations such as @:x@.
+validateCmd :: ByteString -> ByteString
+validateCmd xs =
+ let cut = if BS8.take 1 xs == ":"
+ then BS8.dropWhile isSpace . BS8.dropWhile (not . isSpace)
+ else id
+ in cut xs
diff --git a/src/Proof/Assistant/Agda.hs b/src/Proof/Assistant/Agda.hs
new file mode 100644
--- /dev/null
+++ b/src/Proof/Assistant/Agda.hs
@@ -0,0 +1,78 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+module Proof.Assistant.Agda where
+
+import Control.Concurrent.Async
+import Data.ByteString (ByteString)
+import Data.Coerce
+import System.Directory (getTemporaryDirectory)
+import System.FilePath ((), (<.>))
+import System.Mem
+import Telegram.Bot.API (ChatId (..))
+
+import Agda.Interaction.Command
+import Agda.Interaction.State
+import Agda.TypeChecking.Monad.Base (envCurrentPath)
+import Agda.Utils.FileName (absolute)
+import Proof.Assistant.Helpers
+import Proof.Assistant.Request
+import Proof.Assistant.Settings
+import Proof.Assistant.State
+
+import qualified Data.ByteString.Char8 as BS8
+
+-- | Call Agda with its state. It will parse and execute command from the 'InterpreterRequest'.
+callAgda :: AgdaState -> InterpreterRequest -> IO ByteString
+callAgda currentAgdaState@AgdaState{..} InterpreterRequest{..} = do
+ let InternalInterpreterSettings{..} = internal (settings interpreterState)
+ asyncApi = withChat interpreterRequestTelegramChatId currentAgdaState $ do
+ enableAllocationLimit
+ setAllocationCounter (fromIntegral allocations)
+ interpretAgda currentAgdaState interpreterRequestMessage
+
+ asyncTimer = asyncWait (coerce timeout)
+ eresult <- race asyncTimer (handleErrorMaybe asyncApi)
+ case eresult of
+ Left () -> pure "Time limit exceeded"
+ Right result -> pure result
+
+-- | Since every chat associated with its own Agda state, we need to modify 'TCEnv'
+-- by setting 'envCurrentPath' with an absolute path to the corresponding file.
+withChat :: ChatId -> AgdaState -> IO a -> IO a
+withChat chatId state action = do
+ tmpDir <- getTemporaryDirectory
+ let InternalInterpreterSettings{..} = (internal . settings . interpreterState) state
+ chatIdToString = show . coerce @ChatId @Integer
+ sourceFile = tmpDir
+ sourceFilePrefix
+ <> chatIdToString chatId
+ <.> sourceFileExtension
+ absSourceFile <- absolute sourceFile
+ let modifiedEnv s = s { envCurrentPath = Just absSourceFile }
+ setEnv state modifiedEnv
+ action
+
+-- | Parse user input as command and execute in Agda.
+interpretAgda :: AgdaState -> ByteString -> IO ByteString
+interpretAgda state req = case parseRequest req of
+ Left err -> pure err
+ Right (ecmd, request) -> do
+ let fetchResponse = chooseCommand state ecmd
+ runAgda state =<< fetchResponse request
+
+-- | Parse command. It could be unknown command or 'AgdaCommand' sub-command with its arguments
+-- or even expression to evaluate.
+parseRequest :: ByteString -> Either ByteString (Either () AgdaCommand, ByteString)
+parseRequest rawCmd = case BS8.words rawSubCommand of
+ [] -> Left "Empty command"
+ cmd : _ -> if BS8.isPrefixOf "/" cmd
+ then case matchSupported cmd of
+ Nothing -> Left $ "Unknown command: " <> cmd
+ Just aCmd -> Right (Right aCmd, dropCommand rawSubCommand)
+ else Right (Left (), rawSubCommand)
+ where
+ rawSubCommand = dropCommand rawCmd
diff --git a/src/Proof/Assistant/Arend.hs b/src/Proof/Assistant/Arend.hs
new file mode 100644
--- /dev/null
+++ b/src/Proof/Assistant/Arend.hs
@@ -0,0 +1,61 @@
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RecordWildCards #-}
+module Proof.Assistant.Arend where
+
+import Control.Concurrent.Async (race)
+import Data.ByteString (ByteString)
+import Data.Coerce (coerce)
+import Data.Text (unpack)
+import System.Directory (createDirectoryIfMissing, withCurrentDirectory)
+import System.FilePath
+import System.Process (readProcessWithExitCode)
+
+import Proof.Assistant.Helpers
+import Proof.Assistant.RefreshFile
+import Proof.Assistant.Request
+import Proof.Assistant.ResourceLimit
+import Proof.Assistant.Settings
+import Proof.Assistant.State
+
+import qualified Data.ByteString.Char8 as BS8
+import qualified Data.Text.IO as Text
+
+-- | Call Arend typechecker as CLI application.
+-- It prepares the CLI command, executes it and waits for response.
+callArend :: InterpreterState ArendSettings -> InterpreterRequest -> IO ByteString
+callArend InterpreterState{..} ir = do
+ let ArendSettings{..} = coerce settings
+ ExternalInterpreterSettings{..} = externalArend
+ currentProjectDir <- setArendProject settings ir
+ withCurrentDirectory arendRootProjectDir $ do
+ let fullArgs = (unpack <$> coerce args) <> [currentProjectDir]
+ runProcess = readProcessWithExitCode (t2s executable) fullArgs ""
+ asyncExecutable = do
+ setPriority priority
+ (_exitCode, stdout, stderr) <- runProcess
+ pure . validate currentProjectDir . toBS . unlines $ [stdout, stderr]
+ asyncTimer = asyncWait time
+ eresult <- race asyncTimer (handleErrorMaybe asyncExecutable)
+ case eresult of
+ Left () -> pure "Time limit exceeded"
+ Right bs -> pure bs
+
+-- | Arend requires a project for every file to typecheck.
+-- It reads project configuration, finds all files in a project directory
+-- and tries to typecheck all of them.
+--
+-- Since we need to isolate different chats from each other we need to ensure
+-- that every chat has its own project. And every project has its own configuration.
+--
+-- As result, project directory will be created, set and returned.
+setArendProject :: ArendSettings -> InterpreterRequest -> IO FilePath
+setArendProject ArendSettings{..} InterpreterRequest{..} = do
+ let ExternalInterpreterSettings{..} = externalArend
+ projectDir = arendRootProjectDir (tempFilePrefix <> chatIdToString interpreterRequestTelegramChatId)
+ projectConfigPath = projectDir arendYamlFilename
+ projectSourcePath = projectDir arendModuleName <.> fileExtension
+ createDirectoryIfMissing True projectDir
+ Text.writeFile projectConfigPath arendYamlContent
+ BS8.writeFile projectSourcePath $ dropSubCommand interpreterRequestMessage
+ pure projectDir
+
diff --git a/src/Proof/Assistant/Bot.hs b/src/Proof/Assistant/Bot.hs
new file mode 100644
--- /dev/null
+++ b/src/Proof/Assistant/Bot.hs
@@ -0,0 +1,135 @@
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RecordWildCards #-}
+module Proof.Assistant.Bot where
+
+import Control.Concurrent
+import Control.Concurrent.Async
+import Control.Monad (forever, void)
+import Control.Monad.IO.Class (liftIO)
+import Data.Coerce (coerce)
+import Data.Maybe (isJust)
+
+import Telegram.Bot.API
+import Telegram.Bot.Simple
+import Telegram.Bot.Simple.UpdateParser
+
+import qualified Data.HashMap.Strict as HashMap
+
+import Proof.Assistant.Helpers
+import Proof.Assistant.Interpreter
+import Proof.Assistant.Request
+import Proof.Assistant.Response
+import Proof.Assistant.Settings
+import Agda.Interaction.State
+import Proof.Assistant.Transport
+import Proof.Assistant.Version
+
+-- | Telegram Model.
+type Model = BotState
+
+-- | Supported actions by bot.
+data Action
+ = Call Backend InterpreterRequest -- ^ Call backend and send request to it.
+ | SendBack InterpreterResponse -- ^ Send response back as reply.
+ | Help InterpreterRequest -- ^ Reply with help message.
+ | Version InterpreterRequest -- ^ Reply with version message.
+ | Debug String -- ^ Write in STDOUT unknown input.
+
+-- | Supported backends.
+data Backend = Agda | Arend | Idris | Coq | Lean | Rzk
+
+-- | Initiate bot app based on a 'Model'.
+proofAssistantBot :: Model -> BotApp Model Action
+proofAssistantBot state = BotApp
+ { botInitialModel = state
+ , botAction = flip updateToAction
+ , botHandler = handleAction
+ , botJobs = []
+ }
+
+-- | How to handle updates from Telegram.
+updateToAction :: Model -> Update -> Maybe Action
+updateToAction BotState{..} update
+ -- interpreters
+ | isCommand "coq" update = Call <$> Just Coq <*> updateToRequest update
+ | isCommand "agda" update = Call <$> Just Agda <*> updateToRequest update
+ | isCommand "idris2" update = Call <$> Just Idris <*> updateToRequest update
+ | isCommand "lean" update = Call <$> Just Lean <*> updateToRequest update
+ | isCommand "arend" update = Call <$> Just Arend <*> updateToRequest update
+ | isCommand "rzk" update = Call <$> Just Rzk <*> updateToRequest update
+ -- other
+ | isCommand "help" update = Help <$> updateToRequest update
+ | isCommand "version" update = Version <$> updateToRequest update
+ | otherwise = Just $ Debug $ show update
+ where
+ Settings{..} = botSettings
+ isCommand cmd = isJust . parseUpdate (commandWithBotName botName cmd)
+
+-- | How to handle actions after parsing updates.
+handleAction :: Action -> Model -> Eff Action Model
+handleAction (Call backend request) model = model <# do
+ liftIO $ do
+ let BotState{..} = model
+ Interpreters{..} = interpreters
+ handle = writeInput request
+ handleAgda = handle . interpreterState
+ case backend of
+ Agda -> handleAgda agda
+ Arend -> handle arend
+ Coq -> handle coq
+ Idris -> handle idris
+ Lean -> handle lean
+ Rzk -> handle rzk
+handleAction (SendBack response) model = model <# sendResponseBack True response
+handleAction (Help req) model = model <# do
+ let BotState {..} = model
+ Settings{..} = botSettings
+ case HashMap.lookup (bsToText $ interpreterRequestMessage req) helpMessages of
+ Nothing -> sendResponseBack False $ makeTelegramResponse req (textToBS help)
+ Just helpMessage -> sendResponseBack False
+ $ makeTelegramResponse req (textToBS helpMessage)
+handleAction (Version req) model = model <# do
+ let BotState {..} = model
+ Settings{..} = botSettings
+ sendResponseBack False $ makeTelegramResponse req (textToBS $ makeVersion version)
+handleAction (Debug str) model = model <# (liftIO $ putStrLn str)
+
+-- | Helper that will try to deliver message even when Telegram failed to send it.
+sendResponseBack :: Bool -> InterpreterResponse -> BotM ()
+sendResponseBack isMonospace response =
+ let req = toSendMessageRequest isMonospace response
+ waitAndRetry result = if responseOk result
+ then pure ()
+ else case responseParameters result >>= responseParametersRetryAfter of
+ Nothing -> pure ()
+ Just sec -> do
+ liftIO . threadDelay $ coerce sec * 1000000
+ void (sendMessage req)
+ in liftClientM $ do
+ result <- sendMessage req
+ waitAndRetry result
+
+-- | Initiate Telegram Env, 'Model', start Bot, start backends concurrently.
+runTelegramBot :: Model -> IO ()
+runTelegramBot state@BotState{..} = do
+ env <- defaultTelegramClientEnv (Token $ botToken botSettings)
+ botActionFun <- startBotAsync (proofAssistantBot state) env
+ void $ runConcurrently $
+ Concurrently (botResponseHandlerJob botActionFun) *>
+ Concurrently (interpreterJobs interpreters)
+ where
+ botResponseHandlerJob fun = forever $ do
+ interpreterResponse <- readOutput state
+ fun (SendBack interpreterResponse)
+ interpreterJobs Interpreters{..} = void $ runConcurrently $
+ Concurrently (runInterpreter state agda) *>
+ Concurrently (runInterpreter state arend) *>
+ Concurrently (runInterpreter state coq) *>
+ Concurrently (runInterpreter state idris) *>
+ Concurrently (runInterpreter state lean) *>
+ Concurrently (runInterpreter state rzk)
+
+-- | Main function.
+run :: IO ()
+run = runTelegramBot =<< newBotState =<< loadDefaultSettings
+
diff --git a/src/Proof/Assistant/Helpers.hs b/src/Proof/Assistant/Helpers.hs
new file mode 100644
--- /dev/null
+++ b/src/Proof/Assistant/Helpers.hs
@@ -0,0 +1,66 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+module Proof.Assistant.Helpers where
+
+import Control.Concurrent (threadDelay)
+import Control.Exception
+import Data.Coerce (Coercible, coerce)
+import Data.Char (isSpace)
+import Data.ByteString (ByteString)
+import Data.Text (Text)
+import Dhall (Natural)
+
+import Proof.Assistant.Settings (Time (..))
+
+import qualified Data.ByteString.Char8 as BS8
+import qualified Data.Text as Text
+import qualified Data.Text.Encoding as Text
+
+-- | Cast something to 'Int'.
+toInt :: forall a b. (Num b, Integral b, Coercible a b) => a -> Int
+toInt = fromIntegral . coerce @_ @b
+
+-- | Cast something to 'String'.
+t2s :: Coercible a Text => a -> String
+t2s = Text.unpack . coerce
+
+-- | Wait N seconds.
+asyncWait :: Time -> IO ()
+asyncWait n = threadDelay (toInt @_ @Natural n * 1000000)
+
+-- | If input starts with @/@ drop the whole command with a space and return the remaining part.
+dropCommand :: ByteString -> ByteString
+dropCommand xs = if BS8.take 1 xs == "/" then drop' xs else xs
+ where
+ drop' = BS8.dropWhile isSpace . BS8.dropWhile (not . isSpace)
+
+-- | Drop not only command but sub-command too.
+dropSubCommand :: ByteString -> ByteString
+dropSubCommand = dropCommand . dropCommand
+
+-- | Cast UTF-8 'String' to 'ByteString'.
+toBS :: String -> ByteString
+toBS = Text.encodeUtf8 . Text.pack
+
+-- | Cast UTF-8 'ByteString' to 'String'.
+fromBS :: ByteString -> String
+fromBS = Text.unpack . Text.decodeUtf8
+
+-- | Cast UTF-8 'ByteString' to 'Text'.
+bsToText :: ByteString -> Text
+bsToText = Text.decodeUtf8
+
+-- | Cast UTF-8 'ByteString' to 'Text'.
+textToBS :: Text -> ByteString
+textToBS = Text.encodeUtf8
+
+-- | Cast some exception to 'ByteString'.
+processError :: SomeException -> IO ByteString
+processError (SomeException ex) = pure (toBS $ show ex)
+
+-- | Wrap IO action with 'processError' and return error message as 'ByteString'.
+handleErrorMaybe :: IO ByteString -> IO ByteString
+handleErrorMaybe = (`catch` processError)
diff --git a/src/Proof/Assistant/Idris.hs b/src/Proof/Assistant/Idris.hs
new file mode 100644
--- /dev/null
+++ b/src/Proof/Assistant/Idris.hs
@@ -0,0 +1,49 @@
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RecordWildCards #-}
+module Proof.Assistant.Idris where
+
+import Control.Concurrent.Async (race)
+import Data.ByteString (ByteString)
+import Data.Coerce (coerce)
+
+import Idris.Interaction.Command
+import Proof.Assistant.Helpers
+import Proof.Assistant.Request
+import Proof.Assistant.ResourceLimit
+import Proof.Assistant.Settings
+import Proof.Assistant.State
+
+import qualified Data.ByteString.Char8 as BS8
+
+-- | Call Idris 2 as CLI application.
+-- It prepares the CLI command, executes it and waits for response.
+callIdris2 :: InterpreterState IdrisSettings -> InterpreterRequest -> IO ByteString
+callIdris2 InterpreterState{..} ir@InterpreterRequest{..}
+ = case parseRequest interpreterRequestMessage of
+ Left err -> pure err
+ Right (ecmd, request) -> do
+ let s@ExternalInterpreterSettings{..} = coerce settings
+ action <- chooseCommand s ir ecmd request
+ let asyncExecutable = do
+ setPriority priority
+ (_exitCode, stdout, stderr) <- action
+ let response = unlines [if stdout == "\n" then "Done." else stdout, stderr]
+ pure $ toBS response
+ asyncTimer = asyncWait time
+ eresult <- race asyncTimer (handleErrorMaybe asyncExecutable)
+ case eresult of
+ Left () -> pure "Time limit exceeded"
+ Right bs -> pure bs
+
+-- | Parse command. It could be unknown command or 'IdrisCommand' sub-command with its arguments
+-- or even expression to evaluate.
+parseRequest :: ByteString -> Either ByteString (Either () IdrisCommand, ByteString)
+parseRequest rawCmd = case BS8.words rawSubCommand of
+ [] -> Left "empty command"
+ cmd : _ -> if BS8.isPrefixOf "/" cmd
+ then case matchSupported cmd of
+ Nothing -> Left $ "Unknown command: " <> cmd
+ Just aCmd -> Right (Right aCmd, dropCommand rawSubCommand)
+ else Right (Left (), rawSubCommand)
+ where
+ rawSubCommand = dropCommand rawCmd
diff --git a/src/Proof/Assistant/Interpreter.hs b/src/Proof/Assistant/Interpreter.hs
new file mode 100644
--- /dev/null
+++ b/src/Proof/Assistant/Interpreter.hs
@@ -0,0 +1,100 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+module Proof.Assistant.Interpreter where
+
+import Control.Concurrent.Async
+import Control.Monad (forever)
+import Data.ByteString (ByteString)
+import Data.Coerce (coerce)
+import Data.Text (unpack)
+import System.Directory
+import System.Process
+
+import Agda.Interaction.State
+
+import Proof.Assistant.Agda
+import Proof.Assistant.Arend
+import Proof.Assistant.Idris
+import Proof.Assistant.Lean
+import Proof.Assistant.Rzk
+
+import Proof.Assistant.Helpers
+import Proof.Assistant.Request
+import Proof.Assistant.RefreshFile
+import Proof.Assistant.ResourceLimit
+import Proof.Assistant.Response
+import Proof.Assistant.Settings
+import Proof.Assistant.State
+import Proof.Assistant.Transport
+
+-- | 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.
+runInterpreter :: (Interpreter state settings) => BotState -> state -> IO ()
+runInterpreter botState is = forever $ do
+ incomingMessage <- readInput (getSettings is)
+ response <- interpretSafe is incomingMessage
+ let telegramResponse = makeTelegramResponse incomingMessage response
+ writeOutput telegramResponse botState
+
+-- | 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@.
+class Interpreter state settings | state -> settings where
+ interpretSafe :: state -> InterpreterRequest -> IO ByteString
+ getSettings :: state -> InterpreterState settings
+
+instance Interpreter InternalState InternalInterpreterSettings where
+ interpretSafe state request = callRzk state request
+ getSettings = id
+
+instance Interpreter AgdaState AgdaSettings where
+ interpretSafe state request = callAgda state request
+ getSettings state = interpreterState state
+
+instance Interpreter ExternalState ExternalInterpreterSettings where
+ interpretSafe is request = do
+ let settings' = settings is
+ tmpFilePath <- refreshTmpFile settings' request Nothing
+ callExternalInterpreter settings' tmpFilePath
+ getSettings = id
+
+instance Interpreter (InterpreterState IdrisSettings) IdrisSettings where
+ interpretSafe state request = callIdris2 state request
+ getSettings = id
+
+instance Interpreter (InterpreterState LeanSettings) LeanSettings where
+ interpretSafe state request = callLean state request
+ getSettings = id
+
+instance Interpreter (InterpreterState ArendSettings) ArendSettings where
+ interpretSafe state request = callArend state request
+ getSettings = id
+
+-- ** External Interpreter
+
+-- | Call some external CLI application, probably Coq.
+callExternalInterpreter
+ :: ExternalInterpreterSettings -> (FilePath, FilePath) -> IO ByteString
+callExternalInterpreter ExternalInterpreterSettings{..} (dir, path)
+ = withCurrentDirectory dir $ do
+ contents <- readFile path
+ let asyncExecutable = do
+ setPriority priority
+ (_exitCode, stdout, stderr) <- readProcessWithExitCode (t2s executable) (unpack <$> coerce args) contents
+ pure $ toBS $ unlines [stdout, stderr]
+ asyncTimer = asyncWait time
+ eresult <- race asyncTimer (handleErrorMaybe asyncExecutable)
+ case eresult of
+ Left () -> pure "Time limit exceeded"
+ Right bs -> pure bs
diff --git a/src/Proof/Assistant/Lean.hs b/src/Proof/Assistant/Lean.hs
new file mode 100644
--- /dev/null
+++ b/src/Proof/Assistant/Lean.hs
@@ -0,0 +1,35 @@
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RecordWildCards #-}
+module Proof.Assistant.Lean where
+
+import Control.Concurrent.Async (race)
+import Data.ByteString (ByteString)
+import Data.Coerce (coerce)
+import Data.Text (unpack)
+import System.Directory (withCurrentDirectory)
+import System.Process (readProcessWithExitCode)
+
+import Proof.Assistant.Helpers
+import Proof.Assistant.RefreshFile
+import Proof.Assistant.Request
+import Proof.Assistant.ResourceLimit
+import Proof.Assistant.Settings
+import Proof.Assistant.State
+
+callLean :: InterpreterState LeanSettings -> InterpreterRequest -> IO ByteString
+callLean InterpreterState{..} ir = do
+ let LeanSettings{..} = coerce settings
+ s@ExternalInterpreterSettings{..} = externalLean
+ (dir, path) <- refreshTmpFile s ir (Just projectDir)
+ withCurrentDirectory dir $ do
+ let fullArgs = (unpack <$> coerce args) <> [path]
+ runProcess = readProcessWithExitCode (t2s executable) fullArgs ""
+ asyncExecutable = do
+ setPriority priority
+ (_exitCode, stdout, stderr) <- runProcess
+ pure . validate path . toBS . unlines $ [stdout, stderr]
+ asyncTimer = asyncWait time
+ eresult <- race asyncTimer (handleErrorMaybe asyncExecutable)
+ case eresult of
+ Left () -> pure "Time limit exceeded"
+ Right bs -> pure bs
diff --git a/src/Proof/Assistant/RefreshFile.hs b/src/Proof/Assistant/RefreshFile.hs
new file mode 100644
--- /dev/null
+++ b/src/Proof/Assistant/RefreshFile.hs
@@ -0,0 +1,60 @@
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TypeApplications #-}
+module Proof.Assistant.RefreshFile where
+
+import Data.ByteString (ByteString)
+import Data.Coerce (coerce)
+import System.Directory
+import System.FilePath
+import Telegram.Bot.API (ChatId (..))
+
+import Proof.Assistant.Helpers
+import Proof.Assistant.Request
+import Proof.Assistant.Settings
+
+import qualified Data.ByteString.Char8 as BS8
+import qualified Data.Text as Text
+
+-- | Most interpreters work with files. Therefore, we need to store user input as a file.
+-- Remember that input could come from different chats, so we need to store input separately.
+-- Unless directory specified, temporary directory will be used to store the files.
+refreshTmpFile
+ :: ExternalInterpreterSettings
+ -> InterpreterRequest
+ -> Maybe FilePath
+ -> IO (FilePath, FilePath)
+refreshTmpFile
+ settings
+ ir@InterpreterRequest{interpreterRequestMessage} mDir = do
+ tmpDir <- maybe getTemporaryDirectory pure mDir
+ let tmpFilepath = getTempFilePath settings ir tmpDir
+ createFile = do
+ BS8.writeFile tmpFilepath $ dropSubCommand interpreterRequestMessage
+ pure (tmpDir, tmpFilepath)
+ exist <- doesFileExist tmpFilepath
+ if (not exist)
+ then createFile
+ else removeFile tmpFilepath >> createFile
+
+-- | Make absolute filepath based on settings, request and directory.
+getTempFilePath :: ExternalInterpreterSettings -> InterpreterRequest -> FilePath -> FilePath
+getTempFilePath
+ ExternalInterpreterSettings{tempFilePrefix, fileExtension}
+ InterpreterRequest{interpreterRequestTelegramChatId} dir =
+ let tmpFilepath = dir
+ tempFilePrefix
+ <> chatIdToString interpreterRequestTelegramChatId
+ <.> fileExtension
+ in tmpFilepath
+
+-- | Helper to convert Telegram ChatId to 'String' (for filepath).
+chatIdToString :: ChatId -> String
+chatIdToString = show . coerce @_ @Integer
+
+-- | Helper to cut filepath from the output.
+validate :: FilePath -> ByteString -> ByteString
+validate path bs = textToBS (Text.replace textPath "" txt)
+ where
+ textPath = Text.pack path
+ txt = bsToText bs
diff --git a/src/Proof/Assistant/Request.hs b/src/Proof/Assistant/Request.hs
new file mode 100644
--- /dev/null
+++ b/src/Proof/Assistant/Request.hs
@@ -0,0 +1,20 @@
+module Proof.Assistant.Request where
+
+import Data.ByteString (ByteString)
+import Data.Text.Encoding (encodeUtf8)
+import Telegram.Bot.API
+import Telegram.Bot.Simple.UpdateParser
+
+-- | Request from Telegram.
+data InterpreterRequest = InterpreterRequest
+ { interpreterRequestTelegramChatId :: !ChatId -- ^ Telegram ChatId (for reply and isolation).
+ , interpreterRequestTelegramMessageId :: !MessageId -- ^ Telegram MessageId (for reply).
+ , interpreterRequestMessage :: !ByteString -- ^ Message content.
+ }
+
+-- | Cast Telegram Update to 'InterpreterRequest'.
+updateToRequest :: Update -> Maybe InterpreterRequest
+updateToRequest upd = InterpreterRequest
+ <$> updateChatId upd -- chatId
+ <*> (fmap messageMessageId . extractUpdateMessage) upd -- messageId
+ <*> (encodeUtf8 <$> updateMessageText upd)
diff --git a/src/Proof/Assistant/ResourceLimit.hs b/src/Proof/Assistant/ResourceLimit.hs
new file mode 100644
--- /dev/null
+++ b/src/Proof/Assistant/ResourceLimit.hs
@@ -0,0 +1,35 @@
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE TypeApplications #-}
+module Proof.Assistant.ResourceLimit where
+
+import GHC.Natural
+import System.Posix.Process (nice)
+import System.Posix.Resource
+
+import Proof.Assistant.Helpers
+import Proof.Assistant.Settings
+
+-- | Make ResourceLimits from soft/hard limits.
+makeResourceLimits :: Limit -> ResourceLimits
+makeResourceLimits (Limit soft hard)
+ = ResourceLimits (toResourceLimit soft) (toResourceLimit hard)
+ where
+ toResourceLimit = ResourceLimit . fromIntegral
+
+-- | Read Resources from 'ResourceSettings'.
+makeLimits :: ResourceSettings -> [(Resource, ResourceLimits)]
+makeLimits ResourceSettings{..} =
+ [ (ResourceTotalMemory, makeResourceLimits totalMemory)
+ , (ResourceOpenFiles, makeResourceLimits openFiles)
+ , (ResourceFileSize, makeResourceLimits fileSize)
+ , (ResourceDataSize, makeResourceLimits dataSize)
+ , (ResourceCPUTime, makeResourceLimits cpuTime)
+ ]
+
+-- | Read limits from 'ResourceSettings' and set them for current thread.
+setLimits :: ResourceSettings -> IO ()
+setLimits = mapM_ (uncurry setResourceLimit) . makeLimits
+
+-- | Set 'Priority' for current thread.
+setPriority :: Priority -> IO ()
+setPriority = nice . toInt @_ @Natural
diff --git a/src/Proof/Assistant/Response.hs b/src/Proof/Assistant/Response.hs
new file mode 100644
--- /dev/null
+++ b/src/Proof/Assistant/Response.hs
@@ -0,0 +1,48 @@
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE OverloadedStrings #-}
+module Proof.Assistant.Response where
+
+import Data.ByteString (ByteString)
+import Data.Text.Encoding (decodeUtf8)
+import Telegram.Bot.API
+ (ChatId, MessageId, ParseMode (..), SendMessageRequest (..), SomeChatId (..))
+
+import Proof.Assistant.Request
+
+-- | Response for Telegram.
+data InterpreterResponse = InterpreterResponse
+ { interpreterResponseTelegramChatId :: !ChatId -- ^ Telegram ChatId (for reply).
+ , interpreterResponseTelegramMessageId :: !MessageId -- ^ Telegram MessageId (for reply).
+ , interpreterResponseResponse :: !ByteString -- ^ output data.
+ }
+
+-- | Cast 'InterpreterResponse' to 'SendMessageRequest'.
+-- If first argument is 'True'
+-- then it will wrap message in Monospace font and mark it with @MarkdownV2@ parse mode.
+-- Otherwise, text message will be sent.
+-- For all responses from Backends 'True' should be specified.
+toSendMessageRequest :: Bool -> InterpreterResponse -> SendMessageRequest
+toSendMessageRequest isMonospace InterpreterResponse{..} = SendMessageRequest
+ { sendMessageChatId = SomeChatId interpreterResponseTelegramChatId
+ , sendMessageText
+ = if isMonospace
+ then "```\n" <> decodeUtf8 interpreterResponseResponse <> "\n```\n"
+ else decodeUtf8 interpreterResponseResponse <> "\n"
+ , sendMessageParseMode = if isMonospace then Just MarkdownV2 else Nothing
+ , sendMessageEntities = Nothing
+ , sendMessageDisableWebPagePreview = Nothing
+ , sendMessageDisableNotification = Nothing
+ , sendMessageProtectContent = Nothing
+ , sendMessageReplyToMessageId = Just interpreterResponseTelegramMessageId
+ , sendMessageAllowSendingWithoutReply = Nothing
+ , sendMessageReplyMarkup = Nothing
+ }
+
+-- | Cast 'InterpreterRequest' and output data to 'InterpreterResponse'.
+makeTelegramResponse :: InterpreterRequest -> ByteString -> InterpreterResponse
+makeTelegramResponse InterpreterRequest{..} response =
+ InterpreterResponse
+ { interpreterResponseTelegramChatId = interpreterRequestTelegramChatId
+ , interpreterResponseTelegramMessageId = interpreterRequestTelegramMessageId
+ , interpreterResponseResponse = response
+ }
diff --git a/src/Proof/Assistant/Rzk.hs b/src/Proof/Assistant/Rzk.hs
new file mode 100644
--- /dev/null
+++ b/src/Proof/Assistant/Rzk.hs
@@ -0,0 +1,32 @@
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RecordWildCards #-}
+module Proof.Assistant.Rzk where
+
+import Control.Concurrent.Async (race)
+import Data.ByteString (ByteString)
+import Data.Coerce (coerce)
+import System.Mem
+
+import Rzk.Polylingual
+
+import Proof.Assistant.Helpers
+import Proof.Assistant.Request
+import Proof.Assistant.Settings
+import Proof.Assistant.State
+
+-- | Call Polilyngual API. Rzk will do all the job and return response or an error as result.
+callRzk :: InterpreterState InternalInterpreterSettings -> InterpreterRequest -> IO ByteString
+callRzk InterpreterState{..} ir = do
+ let InternalInterpreterSettings{..} = settings
+ asyncApi = do
+ enableAllocationLimit
+ setAllocationCounter (fromIntegral allocations)
+ let makeResult = pure
+ . either toBS (toBS . compileSomeModule)
+ . safeParseSomeModule . fromBS . dropCommand
+ makeResult (interpreterRequestMessage ir)
+ asyncTimer = asyncWait (coerce timeout)
+ eresult <- race asyncTimer (handleErrorMaybe asyncApi)
+ case eresult of
+ Left () -> pure "Time limit exceeded"
+ Right result -> pure result
diff --git a/src/Proof/Assistant/Settings.hs b/src/Proof/Assistant/Settings.hs
new file mode 100644
--- /dev/null
+++ b/src/Proof/Assistant/Settings.hs
@@ -0,0 +1,128 @@
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE DuplicateRecordFields #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE OverloadedStrings #-}
+module Proof.Assistant.Settings where
+
+import Dhall
+import Data.HashMap.Strict (HashMap)
+
+data Settings = Settings
+ { botName :: !Text -- ^ Telegram bot name. Used to parse @/command\@botname@.
+ , botToken :: !Text -- ^ Bot token.
+ , outputSize :: !Natural -- ^ output size in bytes.
+ , help :: Text -- ^ Help message.
+ , helpMessages :: HashMap Text Text -- ^ Help messages for sub-commands.
+ , version :: Text -- ^ Version message.
+ , interpretersSettings :: !InterpretersSettings -- ^ Settings for backend interpreters.
+ } deriving (Generic, FromDhall)
+
+data ExternalInterpreterSettings = ExternalInterpreterSettings
+ { args :: !CmdArgs -- ^ CLI arguments.
+ , executable :: !Executable -- ^ Path to executable.
+ , time :: !Time -- ^ Time, in seconds.
+ , priority :: !Priority -- ^ Priority for the thread.
+ , resources :: !ResourceSettings -- ^ Different resources.
+ , tempFilePrefix :: !FilePath -- ^ Prefix to filepath to avoid confusion between different interpreters.
+ , fileExtension :: !FilePath -- ^ File extension used by interpreter.
+ , inputSize :: !Natural -- ^ input size in bytes.
+ } deriving (Generic, FromDhall)
+
+data InternalInterpreterSettings = InternalInterpreterSettings
+ { timeout :: !Natural -- ^ Timeout in seconds.
+ , allocations :: !Natural -- ^ Max number of GHC allocations for the interpreter thread.
+ , inputSize :: !Natural -- ^ input size in bytes.
+ , sourceFilePrefix :: !FilePath -- ^ Prefix to filepath to avoid confusion between different interpreters.
+ , sourceFileExtension :: !FilePath -- ^ File extension used by interpreter.
+ } deriving (Generic, FromDhall)
+
+data AgdaSettings = AgdaSettings
+ { internal :: !InternalInterpreterSettings
+ } deriving (Generic, FromDhall)
+
+data LeanSettings = LeanSettings
+ { projectDir :: !FilePath -- ^ Lean requires project where to store source files for typechecking.
+ , externalLean :: !ExternalInterpreterSettings
+ } deriving (Generic, FromDhall)
+
+data ArendSettings = ArendSettings
+ { arendRootProjectDir :: !FilePath -- ^ Arend requires different directories to work correctly. One of them used to store libraries, settings, user projects. We call it "root directory".
+ , arendYamlFilename :: !FilePath -- ^ For each project Arend requires yaml file with a specific name.
+ , arendYamlContent :: !Text -- ^ For each project Arend requires yaml file to store specific settings inside.
+ , arendModuleName :: !FilePath -- ^ Since Arend requires project per chat, it will have a single module inside and we want to give it a common specific configurable name.
+ , externalArend :: !ExternalInterpreterSettings
+ } deriving (Generic, FromDhall)
+
+newtype IdrisSettings = IdrisSettings ExternalInterpreterSettings
+ deriving newtype (FromDhall, ToInterpreterState)
+ deriving stock Generic
+
+newtype CmdArgs = CmdArgs [Text]
+ deriving stock Generic
+ deriving newtype FromDhall
+
+newtype Executable = Executable Text
+ deriving stock Generic
+ deriving newtype FromDhall
+
+newtype Time = Time Natural
+ deriving stock Generic
+ deriving newtype FromDhall
+
+newtype Priority = Priority Natural
+ deriving stock Generic
+ deriving newtype FromDhall
+
+-- | Resource settings.
+data ResourceSettings = ResourceSettings
+ { totalMemory :: !Limit
+ , dataSize :: !Limit
+ , openFiles :: !Limit
+ , fileSize :: !Limit
+ , cpuTime :: !Limit
+ } deriving (Generic, FromDhall)
+
+-- | Limits.
+data Limit = Limit
+ { soft :: !Natural
+ , hard :: !Natural
+ } deriving (Generic, FromDhall)
+
+-- | Combination of all supported interpreters settings.
+data InterpretersSettings = InterpretersSettings
+ { agda :: !AgdaSettings
+ , arend :: !ArendSettings
+ , idris :: !IdrisSettings
+ , coq :: !ExternalInterpreterSettings
+ , lean :: !LeanSettings
+ , rzk :: !InternalInterpreterSettings
+ } deriving (Generic, FromDhall)
+
+-- | Load settings from file.
+loadSettings :: Text -> IO Settings
+loadSettings = input auto
+
+-- | Load default settings.
+loadDefaultSettings :: IO Settings
+loadDefaultSettings = loadSettings "./config/settings.dhall"
+
+-- | Helper to get queue size (communication model between bot and backend worker).
+class ToInterpreterState settings where
+ getQueueSize :: settings -> Natural
+
+instance ToInterpreterState InternalInterpreterSettings where
+ getQueueSize = inputSize
+
+instance ToInterpreterState ExternalInterpreterSettings where
+ getQueueSize = inputSize
+
+instance ToInterpreterState AgdaSettings where
+ getQueueSize = getQueueSize . internal
+
+instance ToInterpreterState LeanSettings where
+ getQueueSize = getQueueSize . externalLean
+
+instance ToInterpreterState ArendSettings where
+ getQueueSize = getQueueSize . externalArend
diff --git a/src/Proof/Assistant/State.hs b/src/Proof/Assistant/State.hs
new file mode 100644
--- /dev/null
+++ b/src/Proof/Assistant/State.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE RecordWildCards #-}
+module Proof.Assistant.State where
+
+import Control.Concurrent.STM (TBQueue, newTBQueueIO)
+
+import Proof.Assistant.Request (InterpreterRequest)
+import Proof.Assistant.Settings
+
+-- | Simple state with settings and queue as communication model between bot and backend.
+data InterpreterState settings = InterpreterState
+ { settings :: !settings
+ , input :: !(TBQueue InterpreterRequest)
+ }
+
+-- | Initialise a state based on its settings.
+newInterpreterState
+ :: forall settings. ToInterpreterState settings => settings -> IO (InterpreterState settings)
+newInterpreterState settings = do
+ input <- newTBQueueIO (getQueueSize settings)
+ pure InterpreterState{..}
diff --git a/src/Proof/Assistant/Transport.hs b/src/Proof/Assistant/Transport.hs
new file mode 100644
--- /dev/null
+++ b/src/Proof/Assistant/Transport.hs
@@ -0,0 +1,70 @@
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE RecordWildCards #-}
+module Proof.Assistant.Transport where
+
+import Control.Concurrent.STM (TBQueue, atomically, newTBQueueIO, readTBQueue, writeTBQueue)
+
+import Agda.Interaction.State
+
+import Proof.Assistant.Request (InterpreterRequest)
+import Proof.Assistant.Response (InterpreterResponse)
+import Proof.Assistant.Settings hiding (InterpretersSettings)
+import Proof.Assistant.State
+
+import qualified Proof.Assistant.Settings as Settings
+
+-- | Combination of all supported backend interpreters.
+data Interpreters = Interpreters
+ { agda :: !AgdaState
+ , arend :: !(InterpreterState ArendSettings)
+ , idris :: !(InterpreterState IdrisSettings)
+ , coq :: !ExternalState
+ , lean :: !(InterpreterState LeanSettings)
+ , rzk :: !InternalState
+ }
+
+-- | Initiate new interpreters from settings.
+newInterpreters :: Settings.InterpretersSettings -> IO Interpreters
+newInterpreters settings = do
+ agda <- newAgdaState $ Settings.agda settings
+ arend <- newInterpreterState $ Settings.arend settings
+ idris <- newInterpreterState $ Settings.idris settings
+ coq <- newInterpreterState $ Settings.coq settings
+ lean <- newInterpreterState $ Settings.lean settings
+ rzk <- newInterpreterState $ Settings.rzk settings
+ pure Interpreters{..}
+
+type ExternalState = InterpreterState ExternalInterpreterSettings
+
+type InternalState = InterpreterState InternalInterpreterSettings
+
+-- | Bot has its own state.
+data BotState = BotState
+ { output :: !(TBQueue InterpreterResponse) -- ^ Queue to read messages from backend interpreters.
+ , botSettings :: !Settings -- ^ Bot settings.
+ , interpreters :: !Interpreters -- ^ All interpreters with their states.
+ }
+
+-- | Initiate 'BotState' from 'Settings'.
+newBotState :: Settings -> IO BotState
+newBotState botSettings@Settings{..} = do
+ output <- newTBQueueIO outputSize
+ interpreters <- newInterpreters interpretersSettings
+ pure BotState{..}
+
+-- | Read message from "input" queue.
+readInput :: InterpreterState settings -> IO InterpreterRequest
+readInput state = atomically $! readTBQueue (input state)
+
+-- | Read message from "output" queue.
+readOutput :: BotState -> IO InterpreterResponse
+readOutput state = atomically $! readTBQueue (output state)
+
+-- | Write message to "input" queue.
+writeInput :: InterpreterRequest -> InterpreterState settings -> IO ()
+writeInput message state = atomically $! writeTBQueue (input state) message
+
+-- | Write message to "output" queue.
+writeOutput :: InterpreterResponse -> BotState -> IO ()
+writeOutput message state = atomically $! writeTBQueue (output state) message
diff --git a/src/Proof/Assistant/Version.hs b/src/Proof/Assistant/Version.hs
new file mode 100644
--- /dev/null
+++ b/src/Proof/Assistant/Version.hs
@@ -0,0 +1,24 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE OverloadedStrings #-}
+module Proof.Assistant.Version where
+
+import Data.Text (Text)
+import Data.Version
+import Paths_proof_assistant_bot
+
+import qualified Data.Text as Text
+
+-- | Version of Rzk.
+rzkVersion :: String
+rzkVersion = VERSION_rzk
+
+-- | Version of this package.
+proofAssistantBotVersion :: String
+proofAssistantBotVersion = showVersion version
+
+-- | Helper to build version from template message.
+makeVersion :: Text -> Text
+makeVersion txt = Text.unlines
+ [ Text.replace "" (Text.pack proofAssistantBotVersion) txt
+ , "rzk v." <> Text.pack rzkVersion
+ ]