diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,9 @@ # Revision history for proof-assistant-bot +## 0.2.1 -- 2023-02-07 + +- Agda bumped to 2.6.3, telegram-bot-simple bumped to 0.9 (see [#29](https://github.com/swamp-agr/proof-assistant-bot/pull/29)). + ## 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)); diff --git a/proof-assistant-bot.cabal b/proof-assistant-bot.cabal --- a/proof-assistant-bot.cabal +++ b/proof-assistant-bot.cabal @@ -1,6 +1,6 @@ cabal-version: 2.4 name: proof-assistant-bot -version: 0.2.0 +version: 0.2.1 synopsis: Telegram bot for proof assistants description: Bridge between Telegram Bot and several proof assistants. . @@ -32,12 +32,12 @@ , process , rzk , stm - , telegram-bot-simple >= 0.5.2 + , telegram-bot-simple >= 0.9 , text , unix , unordered-containers -- interpreters - , Agda + , Agda >= 2.6.3 exposed-modules: Proof.Assistant.Agda , Proof.Assistant.Arend , Proof.Assistant.Idris diff --git a/src/Agda/Interaction/Command/Internal/Parser.hs b/src/Agda/Interaction/Command/Internal/Parser.hs --- a/src/Agda/Interaction/Command/Internal/Parser.hs +++ b/src/Agda/Interaction/Command/Internal/Parser.hs @@ -4,9 +4,10 @@ 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.Syntax.Translation.ConcreteToAbstract + (checkCohesionAttributes, concreteToAbstract, localToAbstract) import Agda.TypeChecking.Monad.Base -import Agda.TypeChecking.Monad.MetaVars (lookupInteractionId, lookupMeta, withInteractionId) +import Agda.TypeChecking.Monad.MetaVars (lookupInteractionId, lookupLocalMeta, withInteractionId) import Agda.TypeChecking.Warnings (runPM) import Agda.Utils.Impossible (__IMPOSSIBLE__) import Agda.Utils.Pretty (text) @@ -20,11 +21,12 @@ metaParseExpr :: InteractionId -> ByteString -> TCM Expr metaParseExpr ii s = do m <- lookupInteractionId ii - scope <- getMetaScope <$> lookupMeta m - r <- getRange <$> lookupMeta m + scope <- getMetaScope <$> lookupLocalMeta m + r <- getRange <$> lookupLocalMeta m -- liftIO $ putStrLn $ prettyShow scope let pos = fromMaybe (__IMPOSSIBLE__) (rStart r) - e <- runPM $ parsePosString exprParser pos (BS8.unpack s) + (e, coh) <- runPM $ parsePosString exprParser pos (BS8.unpack s) + checkCohesionAttributes coh concreteToAbstract scope e actOnMeta :: [ByteString] -> (InteractionId -> Expr -> TCM a) -> TCM a @@ -37,7 +39,8 @@ parseExpr :: String -> TCM Expr parseExpr s = do - e <- runPM $ parse exprParser s + (e, coh) <- runPM $ parse exprParser s + checkCohesionAttributes coh localToAbstract e return readM :: Read a => String -> TCM a diff --git a/src/Agda/Interaction/Command/ShowContext.hs b/src/Agda/Interaction/Command/ShowContext.hs --- a/src/Agda/Interaction/Command/ShowContext.hs +++ b/src/Agda/Interaction/Command/ShowContext.hs @@ -6,7 +6,7 @@ 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.Monad.MetaVars (lookupInteractionId, lookupLocalMeta, withMetaInfo) import Agda.TypeChecking.Pretty (prettyTCM) import Agda.TypeChecking.Reduce (normalise) import Agda.TypeChecking.Substitute.Class (raise) @@ -21,7 +21,7 @@ showContext :: [ByteString] -> TCM ByteString showContext (meta:args) = do i <- InteractionId <$> readM (BS8.unpack meta) - mi <- lookupMeta =<< lookupInteractionId i + mi <- lookupLocalMeta =<< lookupInteractionId i BS8.unlines <$> withMetaInfo (getMetaInfo mi) displayMore where display (x, t) n = do diff --git a/src/Proof/Assistant/Agda.hs b/src/Proof/Assistant/Agda.hs --- a/src/Proof/Assistant/Agda.hs +++ b/src/Proof/Assistant/Agda.hs @@ -19,6 +19,7 @@ import Agda.TypeChecking.Monad.Base (envCurrentPath) import Agda.Utils.FileName (absolute) import Proof.Assistant.Helpers +import Proof.Assistant.RefreshFile (validate) import Proof.Assistant.Request import Proof.Assistant.Settings import Proof.Assistant.State @@ -42,7 +43,7 @@ -- | 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 -> AgdaState -> IO ByteString -> IO ByteString withChat chatId state action = do tmpDir <- getTemporaryDirectory let InternalInterpreterSettings{..} = (internal . settings . interpreterState) state @@ -54,7 +55,7 @@ absSourceFile <- absolute sourceFile let modifiedEnv s = s { envCurrentPath = Just absSourceFile } setEnv state modifiedEnv - action + pure . validate sourceFile =<< action -- | Parse user input as command and execute in Agda. interpretAgda :: AgdaState -> ByteString -> IO ByteString diff --git a/src/Proof/Assistant/Lean.hs b/src/Proof/Assistant/Lean.hs --- a/src/Proof/Assistant/Lean.hs +++ b/src/Proof/Assistant/Lean.hs @@ -5,6 +5,7 @@ import Control.Concurrent.Async (race) import Data.ByteString (ByteString) import Data.Coerce (coerce) +import Data.Foldable (foldl') import Data.Text (unpack) import System.Directory (withCurrentDirectory) import System.Process (readProcessWithExitCode) @@ -16,11 +17,13 @@ import Proof.Assistant.Settings import Proof.Assistant.State +import qualified Data.Text as Text + callLean :: InterpreterState LeanSettings -> InterpreterRequest -> IO ByteString callLean InterpreterState{..} ir = do - let LeanSettings{..} = coerce settings + let ls@LeanSettings{..} = coerce settings s@ExternalInterpreterSettings{..} = externalLean - (dir, path) <- refreshTmpFile s ir (Just projectDir) + (dir, path) <- refreshTmpFile s (validateLean ls ir) (Just projectDir) withCurrentDirectory dir $ do let fullArgs = (unpack <$> coerce args) <> [path] runProcess = readProcessWithExitCode (t2s executable) fullArgs "" @@ -33,3 +36,13 @@ case eresult of Left () -> pure "Time limit exceeded" Right bs -> pure bs + +validateLean :: LeanSettings -> InterpreterRequest -> InterpreterRequest +validateLean LeanSettings{..} ir@InterpreterRequest{..} + = ir { interpreterRequestMessage = validatedMsg } + where + remove txt blockedPrefix = Text.replace blockedPrefix "" txt + removeAllFromLine x = foldl' remove x leanBlockList + removeUnsafeImports = textToBS . removeAllFromLine . bsToText + + validatedMsg = removeUnsafeImports interpreterRequestMessage diff --git a/src/Proof/Assistant/Response.hs b/src/Proof/Assistant/Response.hs --- a/src/Proof/Assistant/Response.hs +++ b/src/Proof/Assistant/Response.hs @@ -24,6 +24,7 @@ toSendMessageRequest :: Bool -> InterpreterResponse -> SendMessageRequest toSendMessageRequest isMonospace InterpreterResponse{..} = SendMessageRequest { sendMessageChatId = SomeChatId interpreterResponseTelegramChatId + , sendMessageMessageThreadId = Nothing , sendMessageText = if isMonospace then "```\n" <> decodeUtf8 interpreterResponseResponse <> "\n```\n" diff --git a/src/Proof/Assistant/Settings.hs b/src/Proof/Assistant/Settings.hs --- a/src/Proof/Assistant/Settings.hs +++ b/src/Proof/Assistant/Settings.hs @@ -44,6 +44,7 @@ data LeanSettings = LeanSettings { projectDir :: !FilePath -- ^ Lean requires project where to store source files for typechecking. + , leanBlockList :: [Text] , externalLean :: !ExternalInterpreterSettings } deriving (Generic, FromDhall)