feat(rpc): extend search path, remove cd

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."])

cryptol-remote-api/cryptol-remote-api.cabal

@@ -42,7 +42,6 @@ common deps
     bytestring           ^>= 0.10.8,
     containers           >=0.5.11 && <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

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,18 +58,18 @@ getSearchPaths =
 
 cryptolMethods :: [AppMethod ServerState]
 cryptolMethods =
-  [ command
-     "change directory"
-     cdDescr
-     cd
-  , notification
+  [ notification
     "clear state"
     clearStateDescr
     clearState
   , notification
     "clear all states"
     clearAllStatesDescr
     clearAllStates
+  , command
+     "extend search path"
+     extSearchPathDescr
+     extSearchPath
   , command
      "load module"
      loadModuleDescr

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)

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

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()

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

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 qualified Data.Set as Set
 import Data.Text (Text)
 
 import Cryptol.Eval (EvalOpts(..))
@@ -143,9 +144,14 @@ 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 = removeDups $ paths ++ meSearchPath me }
+  where removeDups ps = reverse $ go ps [] Set.empty -- remove duplicates in less than quadratic time (i.e., no `nub`)
+        go [] ys _ = ys
+        go (x:xs) ys seen = if Set.member x seen then go xs ys seen else go xs (x:ys) (Set.insert x seen)
+
+
 
 
 -- | Check that all of the modules loaded in the Cryptol environment

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."])
+    ]