From 5dd9be0e4410c2ab605c65bdc07ee4f4ea173c8d Mon Sep 17 00:00:00 2001 From: Andrew Kent Date: Fri, 26 Mar 2021 16:19:56 -0700 Subject: [PATCH] feat(rpc): extend search path, remove cd --- .../cryptol-eval-server/Main.hs | 10 ++++- cryptol-remote-api/cryptol-remote-api.cabal | 5 +-- cryptol-remote-api/cryptol-remote-api/Main.hs | 17 +++---- cryptol-remote-api/python/cryptol/__init__.py | 21 +++++---- .../cryptol/test-files/test-subdir/Bar.cry | 7 +++ .../python/tests/cryptol/test_basics.py | 45 +++++++++++++++++++ .../test-files/test-subdir/Bar.cry | 7 +++ cryptol-remote-api/src/CryptolServer.hs | 9 ++-- .../src/CryptolServer/ChangeDir.hs | 40 ----------------- .../src/CryptolServer/ExtendSearchPath.hs | 38 ++++++++++++++++ 10 files changed, 134 insertions(+), 65 deletions(-) create mode 100644 cryptol-remote-api/python/tests/cryptol/test-files/test-subdir/Bar.cry create mode 100644 cryptol-remote-api/python/tests/cryptol/test_basics.py create mode 100644 cryptol-remote-api/python/tests/cryptol_eval/test-files/test-subdir/Bar.cry delete mode 100644 cryptol-remote-api/src/CryptolServer/ChangeDir.hs create mode 100644 cryptol-remote-api/src/CryptolServer/ExtendSearchPath.hs diff --git a/cryptol-remote-api/cryptol-eval-server/Main.hs b/cryptol-remote-api/cryptol-eval-server/Main.hs index 90f379064..d11a732a9 100644 --- a/cryptol-remote-api/cryptol-eval-server/Main.hs +++ b/cryptol-remote-api/cryptol-eval-server/Main.hs @@ -33,10 +33,12 @@ import qualified Argo.Doc as Doc import CryptolServer - ( ServerState, moduleEnv, tcSolver, initialState, setSearchPath, command, notification ) + ( ServerState, moduleEnv, tcSolver, initialState, extendSearchPath, command, notification ) import CryptolServer.Call ( call ) import CryptolServer.EvalExpr ( evalExpressionDescr, evalExpression ) +import CryptolServer.ExtendSearchPath + ( extSearchPath, extSearchPathDescr ) import CryptolServer.FocusedModule ( focusedModuleDescr, focusedModule ) import CryptolServer.Names ( visibleNamesDescr, visibleNames ) @@ -56,7 +58,7 @@ main = customMain initMod initMod initMod initMod description buildApp startingState (StartingFile file) reader = do paths <- getSearchPaths - initSt <- setSearchPath paths <$> initialState + initSt <- extendSearchPath paths <$> initialState let s = view tcSolver initSt let menv = view moduleEnv initSt let minp = ModuleInput False (pure evOpts) reader menv s @@ -125,6 +127,10 @@ cryptolEvalMethods = "evaluate expression" evalExpressionDescr evalExpression + , command + "extend search path" + extSearchPathDescr + extSearchPath , command "call" (Doc.Paragraph [Doc.Text "Evaluate the result of calling a Cryptol function on one or more parameters."]) diff --git a/cryptol-remote-api/cryptol-remote-api.cabal b/cryptol-remote-api/cryptol-remote-api.cabal index eb2df2ac9..b6cb9ce9c 100644 --- a/cryptol-remote-api/cryptol-remote-api.cabal +++ b/cryptol-remote-api/cryptol-remote-api.cabal @@ -40,9 +40,8 @@ common deps aeson >= 1.4.2, base64-bytestring >= 1.0, bytestring ^>= 0.10.8, - containers >=0.5.11 && <0.7, + containers >=0.6.0.1 && <0.7, cryptol >= 2.9.0, - directory ^>= 1.3.1, filepath ^>= 1.4, lens >= 4.17 && < 4.20, mtl ^>= 2.2, @@ -60,11 +59,11 @@ library exposed-modules: CryptolServer CryptolServer.Call - CryptolServer.ChangeDir CryptolServer.ClearState CryptolServer.Data.Expression CryptolServer.Data.Type CryptolServer.EvalExpr + CryptolServer.ExtendSearchPath CryptolServer.Exceptions CryptolServer.FocusedModule CryptolServer.LoadModule diff --git a/cryptol-remote-api/cryptol-remote-api/Main.hs b/cryptol-remote-api/cryptol-remote-api/Main.hs index 1e0b26028..9f9dd7bb8 100644 --- a/cryptol-remote-api/cryptol-remote-api/Main.hs +++ b/cryptol-remote-api/cryptol-remote-api/Main.hs @@ -13,13 +13,14 @@ import qualified Argo.Doc as Doc import CryptolServer - ( command, notification, initialState, setSearchPath, ServerState ) + ( command, notification, initialState, extendSearchPath, ServerState ) import CryptolServer.Call ( call, callDescr ) -import CryptolServer.ChangeDir ( cd, cdDescr ) import CryptolServer.ClearState ( clearState, clearStateDescr, clearAllStates, clearAllStatesDescr ) import CryptolServer.EvalExpr ( evalExpression, evalExpressionDescr ) +import CryptolServer.ExtendSearchPath + ( extSearchPath, extSearchPathDescr ) import CryptolServer.FocusedModule ( focusedModule, focusedModuleDescr ) import CryptolServer.LoadModule @@ -31,7 +32,7 @@ import CryptolServer.TypeCheck ( checkType, checkTypeDescr ) main :: IO () main = do paths <- getSearchPaths - initSt <- setSearchPath paths <$> initialState + initSt <- extendSearchPath paths <$> initialState theApp <- mkApp "Cryptol RPC Server" serverDocs @@ -57,11 +58,7 @@ getSearchPaths = cryptolMethods :: [AppMethod ServerState] cryptolMethods = - [ command - "change directory" - cdDescr - cd - , notification + [ notification "clear state" clearStateDescr clearState @@ -69,6 +66,10 @@ cryptolMethods = "clear all states" clearAllStatesDescr clearAllStates + , command + "extend search path" + extSearchPathDescr + extSearchPath , command "load module" loadModuleDescr diff --git a/cryptol-remote-api/python/cryptol/__init__.py b/cryptol-remote-api/python/cryptol/__init__.py index 69a481a1a..c993eb4d2 100644 --- a/cryptol-remote-api/python/cryptol/__init__.py +++ b/cryptol-remote-api/python/cryptol/__init__.py @@ -22,15 +22,6 @@ -# Current status: -# It can currently launch a server, given a suitable command line as an argument. Try this: -# >>> c = CryptolConnection("cabal -v0 run cryptol-remote-api") -# >>> f = c.load_file(FILE) -# >>> f.result() -# - - - def extend_hex(string : str) -> str: if len(string) % 2 == 1: return '0' + string @@ -105,6 +96,13 @@ def __init__(self, connection : HasProtocolState, filename : str) -> None: def process_result(self, res : Any) -> Any: return res +class CryptolExtendSearchPath(argo.Command): + def __init__(self, connection : HasProtocolState, dirs : List[str]) -> None: + super(CryptolExtendSearchPath, self).__init__('extend search path', {'paths': dirs}, connection) + + def process_result(self, res : Any) -> Any: + return res + class CryptolEvalExpr(argo.Command): def __init__(self, connection : HasProtocolState, expr : Any) -> None: @@ -361,6 +359,11 @@ def evaluate_expression(self, expression : Any) -> argo.Command: """ return self.eval(expression) + def extend_search_path(self, *dir : str) -> argo.Command: + """Load a Cryptol module, like ``:module`` at the Cryptol REPL.""" + self.most_recent_result = CryptolExtendSearchPath(self, list(dir)) + return self.most_recent_result + def call(self, fun : str, *args : List[Any]) -> argo.Command: encoded_args = [cryptoltypes.CryptolType().from_python(a) for a in args] self.most_recent_result = CryptolCall(self, fun, encoded_args) diff --git a/cryptol-remote-api/python/tests/cryptol/test-files/test-subdir/Bar.cry b/cryptol-remote-api/python/tests/cryptol/test-files/test-subdir/Bar.cry new file mode 100644 index 000000000..f33c74a10 --- /dev/null +++ b/cryptol-remote-api/python/tests/cryptol/test-files/test-subdir/Bar.cry @@ -0,0 +1,7 @@ +module Bar where + +id : {n} (fin n) => [n] -> [n] +id a = a + +theAnswer : [8] +theAnswer = 42 diff --git a/cryptol-remote-api/python/tests/cryptol/test_basics.py b/cryptol-remote-api/python/tests/cryptol/test_basics.py new file mode 100644 index 000000000..7eef7f964 --- /dev/null +++ b/cryptol-remote-api/python/tests/cryptol/test_basics.py @@ -0,0 +1,45 @@ +import unittest +from pathlib import Path +import os +from pathlib import Path +import subprocess +import time +import unittest +import signal +from distutils.spawn import find_executable +import cryptol +import argo_client.connection as argo +import cryptol.cryptoltypes +from cryptol import solver +from cryptol.bitvector import BV +from BitVector import * #type: ignore + + +# Tests of the core server functionality and less +# focused on intricate Cryptol specifics per se. + +class BasicServerTests(unittest.TestCase): + # Connection to cryptol + c = None + + @classmethod + def setUpClass(self): + self.c = cryptol.connect() + + @classmethod + def tearDownClass(self): + if self.c: + self.c.reset() + + def test_extend_search_path(self): + """Test that extending the search path acts as expected w.r.t. loads.""" + c = self.c + + c.extend_search_path(str(Path('tests','cryptol','test-files', 'test-subdir'))) + c.load_module('Bar') + ans1 = c.evaluate_expression("theAnswer").result() + ans2 = c.evaluate_expression("id theAnswer").result() + self.assertEqual(ans1, ans2) + +if __name__ == "__main__": + unittest.main() diff --git a/cryptol-remote-api/python/tests/cryptol_eval/test-files/test-subdir/Bar.cry b/cryptol-remote-api/python/tests/cryptol_eval/test-files/test-subdir/Bar.cry new file mode 100644 index 000000000..f33c74a10 --- /dev/null +++ b/cryptol-remote-api/python/tests/cryptol_eval/test-files/test-subdir/Bar.cry @@ -0,0 +1,7 @@ +module Bar where + +id : {n} (fin n) => [n] -> [n] +id a = a + +theAnswer : [8] +theAnswer = 42 diff --git a/cryptol-remote-api/src/CryptolServer.hs b/cryptol-remote-api/src/CryptolServer.hs index a269c5df5..2bf61679d 100644 --- a/cryptol-remote-api/src/CryptolServer.hs +++ b/cryptol-remote-api/src/CryptolServer.hs @@ -9,6 +9,7 @@ import Control.Lens import Control.Monad.IO.Class import Control.Monad.Reader (ReaderT(ReaderT)) import qualified Data.Aeson as JSON +import Data.Containers.ListUtils (nubOrd) import Data.Text (Text) import Cryptol.Eval (EvalOpts(..)) @@ -143,9 +144,11 @@ defaultSolverConfig searchPath = , solverPreludePath = searchPath } -setSearchPath :: [FilePath] -> ServerState -> ServerState -setSearchPath paths = - over moduleEnv $ \me -> me { meSearchPath = paths ++ meSearchPath me } +extendSearchPath :: [FilePath] -> ServerState -> ServerState +extendSearchPath paths = + over moduleEnv $ \me -> me { meSearchPath = nubOrd $ paths ++ meSearchPath me } + + -- | Check that all of the modules loaded in the Cryptol environment diff --git a/cryptol-remote-api/src/CryptolServer/ChangeDir.hs b/cryptol-remote-api/src/CryptolServer/ChangeDir.hs deleted file mode 100644 index 1202f86f5..000000000 --- a/cryptol-remote-api/src/CryptolServer/ChangeDir.hs +++ /dev/null @@ -1,40 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} -module CryptolServer.ChangeDir - ( cd - , cdDescr - , ChangeDirectoryParams(..) - ) where - -import qualified Argo.Doc as Doc -import Control.Monad.IO.Class -import Data.Aeson as JSON -import System.Directory - -import CryptolServer -import CryptolServer.Exceptions - - -cdDescr :: Doc.Block -cdDescr = Doc.Paragraph - [Doc.Text "Changes the server's working directory to the given path."] - -cd :: ChangeDirectoryParams -> CryptolCommand () -cd (ChangeDirectoryParams newDir) = - do exists <- liftIO $ doesDirectoryExist newDir - if exists - then liftIO $ setCurrentDirectory newDir - else raise (dirNotFound newDir) - -data ChangeDirectoryParams - = ChangeDirectoryParams FilePath - -instance FromJSON ChangeDirectoryParams where - parseJSON = - withObject "params for \"change directory\"" $ - \o -> ChangeDirectoryParams <$> o .: "directory" - -instance Doc.DescribedParams ChangeDirectoryParams where - parameterFieldDescription = - [("directory", - Doc.Paragraph [Doc.Text "The path to change the current directory."]) - ] diff --git a/cryptol-remote-api/src/CryptolServer/ExtendSearchPath.hs b/cryptol-remote-api/src/CryptolServer/ExtendSearchPath.hs new file mode 100644 index 000000000..eccd21dcc --- /dev/null +++ b/cryptol-remote-api/src/CryptolServer/ExtendSearchPath.hs @@ -0,0 +1,38 @@ +{-# LANGUAGE OverloadedStrings #-} +module CryptolServer.ExtendSearchPath + ( extSearchPath + , extSearchPathDescr + , ExtendSearchPathParams(..) + ) where + + +import qualified Argo +import qualified Argo.Doc as Doc +import Data.Aeson as JSON ( (.:), withObject, FromJSON(parseJSON) ) + +import CryptolServer + +-- | Documentation for @extendSearchPath@ +extSearchPathDescr :: Doc.Block +extSearchPathDescr = + Doc.Paragraph + [Doc.Text "Extend the server's search path with the given paths."] + +-- | Extend the search path with the provided directories. +extSearchPath :: ExtendSearchPathParams -> CryptolCommand () +extSearchPath (ExtendSearchPathParams newDirs) = + CryptolCommand $ const $ Argo.modifyState (extendSearchPath newDirs) + +data ExtendSearchPathParams + = ExtendSearchPathParams [FilePath] + +instance FromJSON ExtendSearchPathParams where + parseJSON = + withObject "params for \"extend search path\"" $ + \o -> ExtendSearchPathParams <$> o .: "paths" + +instance Doc.DescribedParams ExtendSearchPathParams where + parameterFieldDescription = + [("paths", + Doc.Paragraph [Doc.Text "The paths to add to the search path."]) + ]