proof-assistant-bot (empty) → 0.2.0
raw patch · 37 files changed
+2103/−0 lines, 37 filesdep +Agdadep +asyncdep +base
Dependencies added: Agda, async, base, bytestring, dhall, directory, filepath, mtl, process, proof-assistant-bot, rzk, stm, telegram-bot-simple, text, unix, unordered-containers
Files
- CHANGELOG.md +18/−0
- LICENSE +20/−0
- README.md +376/−0
- app/Main.hs +6/−0
- proof-assistant-bot.cabal +93/−0
- src/Agda/Interaction/Command.hs +99/−0
- src/Agda/Interaction/Command/EvalIn.hs +18/−0
- src/Agda/Interaction/Command/EvalTerm.hs +21/−0
- src/Agda/Interaction/Command/GiveMeta.hs +19/−0
- src/Agda/Interaction/Command/Internal/Parser.hs +47/−0
- src/Agda/Interaction/Command/RefineMeta.hs +18/−0
- src/Agda/Interaction/Command/Reload.hs +47/−0
- src/Agda/Interaction/Command/RetryConstraints.hs +9/−0
- src/Agda/Interaction/Command/ShowConstraints.hs +21/−0
- src/Agda/Interaction/Command/ShowContext.hs +37/−0
- src/Agda/Interaction/Command/ShowMetas.hs +65/−0
- src/Agda/Interaction/Command/ShowScope.hs +13/−0
- src/Agda/Interaction/Command/TypeIn.hs +22/−0
- src/Agda/Interaction/Command/TypeOf.hs +21/−0
- src/Agda/Interaction/State.hs +77/−0
- src/Idris/Interaction/Command.hs +94/−0
- src/Proof/Assistant/Agda.hs +78/−0
- src/Proof/Assistant/Arend.hs +61/−0
- src/Proof/Assistant/Bot.hs +135/−0
- src/Proof/Assistant/Helpers.hs +66/−0
- src/Proof/Assistant/Idris.hs +49/−0
- src/Proof/Assistant/Interpreter.hs +100/−0
- src/Proof/Assistant/Lean.hs +35/−0
- src/Proof/Assistant/RefreshFile.hs +60/−0
- src/Proof/Assistant/Request.hs +20/−0
- src/Proof/Assistant/ResourceLimit.hs +35/−0
- src/Proof/Assistant/Response.hs +48/−0
- src/Proof/Assistant/Rzk.hs +32/−0
- src/Proof/Assistant/Settings.hs +128/−0
- src/Proof/Assistant/State.hs +21/−0
- src/Proof/Assistant/Transport.hs +70/−0
- src/Proof/Assistant/Version.hs +24/−0
+ CHANGELOG.md view
@@ -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.
+ LICENSE view
@@ -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.
+ README.md view
@@ -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 <input>`. 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 <expr>`. E.g. `/agda /typeOf suc`.+ - `/agda <expr>`. E.g. `/agda suc zero + suc zero`.++- Idris 2 via `/idris2` command. Bot supports several subcommands for Idris 2:+ - `/idris2 /load <input>`. 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 <expr>`. E.g. `/idris2 /typeOf Nat`.+ - `/idris2 <expr>`. 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
+ app/Main.hs view
@@ -0,0 +1,6 @@+module Main where++import Proof.Assistant.Bot (run)++main :: IO ()+main = run
+ proof-assistant-bot.cabal view
@@ -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
+ src/Agda/Interaction/Command.hs view
@@ -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
+ src/Agda/Interaction/Command/EvalIn.hs view
@@ -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"
+ src/Agda/Interaction/Command/EvalTerm.hs view
@@ -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
+ src/Agda/Interaction/Command/GiveMeta.hs view
@@ -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"
+ src/Agda/Interaction/Command/Internal/Parser.hs view
@@ -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
+ src/Agda/Interaction/Command/RefineMeta.hs view
@@ -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"
+ src/Agda/Interaction/Command/Reload.hs view
@@ -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
+ src/Agda/Interaction/Command/RetryConstraints.hs view
@@ -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."
+ src/Agda/Interaction/Command/ShowConstraints.hs view
@@ -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+
+ src/Agda/Interaction/Command/ShowContext.hs view
@@ -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"+
+ src/Agda/Interaction/Command/ShowMetas.hs view
@@ -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]"+
+ src/Agda/Interaction/Command/ShowScope.hs view
@@ -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
+ src/Agda/Interaction/Command/TypeIn.hs view
@@ -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"
+ src/Agda/Interaction/Command/TypeOf.hs view
@@ -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
+ src/Agda/Interaction/State.hs view
@@ -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
+ src/Idris/Interaction/Command.hs view
@@ -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
+ src/Proof/Assistant/Agda.hs view
@@ -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
+ src/Proof/Assistant/Arend.hs view
@@ -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+
+ src/Proof/Assistant/Bot.hs view
@@ -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+
+ src/Proof/Assistant/Helpers.hs view
@@ -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)
+ src/Proof/Assistant/Idris.hs view
@@ -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
+ src/Proof/Assistant/Interpreter.hs view
@@ -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
+ src/Proof/Assistant/Lean.hs view
@@ -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
+ src/Proof/Assistant/RefreshFile.hs view
@@ -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 "<bot>" txt)+ where+ textPath = Text.pack path+ txt = bsToText bs
+ src/Proof/Assistant/Request.hs view
@@ -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)
+ src/Proof/Assistant/ResourceLimit.hs view
@@ -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
+ src/Proof/Assistant/Response.hs view
@@ -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+ }
+ src/Proof/Assistant/Rzk.hs view
@@ -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
+ src/Proof/Assistant/Settings.hs view
@@ -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
+ src/Proof/Assistant/State.hs view
@@ -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{..}
+ src/Proof/Assistant/Transport.hs view
@@ -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
+ src/Proof/Assistant/Version.hs view
@@ -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 "<bot_version>" (Text.pack proofAssistantBotVersion) txt+ , "rzk v." <> Text.pack rzkVersion+ ]