feat(rpc): extend search path, remove cd

GaloisInc · Mar 29, 2021 · 8e024a5 · 8e024a5
1 parent b4e0a7f
commit 8e024a5
Show file tree

Hide file tree

Showing 6 changed files with 58 additions and 54 deletions.
diff --git 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
@@ -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

diff --git 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,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

diff --git a/cryptol-remote-api/src/CryptolServer.hs b/cryptol-remote-api/src/CryptolServer.hs
@@ -143,8 +143,8 @@ defaultSolverConfig searchPath =
   , solverPreludePath = searchPath
   }
 
-setSearchPath :: [FilePath] -> ServerState -> ServerState
-setSearchPath paths =
+extendSearchPath :: [FilePath] -> ServerState -> ServerState
+extendSearchPath paths =
   over moduleEnv $ \me -> me { meSearchPath = paths ++ meSearchPath me }
 
 

diff --git a/cryptol-remote-api/src/CryptolServer/ChangeDir.hs b/cryptol-remote-api/src/CryptolServer/ChangeDir.hs
diff --git a/cryptol-remote-api/src/CryptolServer/ExtendSearchPath.hs 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."])
+    ]