Skip to content

Commit

Permalink
Merge pull request #1477 from GaloisInc/file-deps
Browse files Browse the repository at this point in the history
Module dependencies without loading
  • Loading branch information
yav authored Dec 5, 2022
2 parents 1dd175b + a85c3a9 commit b35170a
Show file tree
Hide file tree
Showing 14 changed files with 246 additions and 159 deletions.
2 changes: 1 addition & 1 deletion CHANGES.md
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,7 @@

* Add `:file-deps` commnads ro the REPL and Python API.
It shows information about the source files and dependencies of
loaded modules.
modules or Cryptol files.

## Bug fixes

Expand Down
11 changes: 8 additions & 3 deletions cryptol-remote-api/docs/Cryptol.rst
Original file line number Diff line number Diff line change
Expand Up @@ -391,14 +391,19 @@ No return fields
file-deps (command)
~~~~~~~~~~~~~~~~~~~

Get information about the dependencies of a loaded top-level module. The dependencies include the dependencies of modules nested in this one.
Get information about the dependencies of a file or module. The dependencies include the dependencies of modules nested in this one.

Parameter fields
++++++++++++++++


``module name``
Get information about this loaded module.
``name``
Get information about this entity.



``is-file``
Indicates if the name is a file (true) or module (false)



Expand Down
12 changes: 10 additions & 2 deletions cryptol-remote-api/python/cryptol/commands.py
Original file line number Diff line number Diff line change
Expand Up @@ -76,8 +76,16 @@ def process_result(self, res : Any) -> Any:
return res

class CryptolFileDeps(argo.Command):
def __init__(self, connection : HasProtocolState, mod_name : str, timeout: Optional[float]) -> None:
super(CryptolFileDeps, self).__init__('file-deps', {'module name': mod_name}, connection, timeout=timeout)
def __init__( self
, connection : HasProtocolState
, name : str, isFile : bool
, timeout: Optional[float]
) -> None:
super(CryptolFileDeps, self).__init__('file-deps'
, {'name': name, 'is-file': isFile }
, connection
, timeout=timeout
)

def process_result(self, res : Any) -> Any:
return res
Expand Down
6 changes: 3 additions & 3 deletions cryptol-remote-api/python/cryptol/connection.py
Original file line number Diff line number Diff line change
Expand Up @@ -213,13 +213,13 @@ def load_module(self, module_name : str, *, timeout:Optional[float] = None) -> a
self.most_recent_result = CryptolLoadModule(self, module_name, timeout)
return self.most_recent_result

def file_deps(self, module_name : str, *, timeout:Optional[float] = None) -> argo.Command:
"""Get information about a loaded module.
def file_deps(self, name : str, isFile : bool, *, timeout:Optional[float] = None) -> argo.Command:
"""Get information about a module or a file.
:param timeout: Optional timeout for this request (in seconds).
"""
timeout = timeout if timeout is not None else self.timeout
self.most_recent_result = CryptolFileDeps(self, module_name, timeout)
self.most_recent_result = CryptolFileDeps(self, name, isFile, timeout)
return self.most_recent_result

def eval_raw(self, expression : Any, *, timeout:Optional[float] = None) -> argo.Command:
Expand Down
14 changes: 14 additions & 0 deletions cryptol-remote-api/python/cryptol/file_deps.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
from typing import Dict, Any

def nestedFileDeps(getDeps : Any, name : str, isFile : bool) -> Any:
done : Dict[str,Any] = {}
start = getDeps(name, isFile)
todo = start["imports"].copy()
while len(todo) > 0:
m = todo.pop()
if m in done:
continue
deps = getDeps(m, False)
todo.extend(deps["imports"])
return (start, deps)

6 changes: 3 additions & 3 deletions cryptol-remote-api/python/cryptol/single_connection.py
Original file line number Diff line number Diff line change
Expand Up @@ -243,8 +243,8 @@ def logging(on : bool, *, dest : TextIO = sys.stderr) -> None:
"""Whether to log received and transmitted JSON."""
__get_designated_connection().logging(on=on,dest=dest)

def file_deps(m : str, timeout:Optional[float] = None) -> Any:
"""Get information about a loaded module."""
return __get_designated_connection().file_deps(m,timeout=timeout)
def file_deps(m : str, isFile:bool, timeout:Optional[float] = None) -> Any:
"""Get information about a module or a file."""
return __get_designated_connection().file_deps(m,isFile,timeout=timeout)


8 changes: 5 additions & 3 deletions cryptol-remote-api/python/cryptol/synchronous.py
Original file line number Diff line number Diff line change
Expand Up @@ -380,6 +380,8 @@ def logging(self, on : bool, *, dest : TextIO = sys.stderr) -> None:
"""Whether to log received and transmitted JSON."""
self.connection.server_connection.logging(on=on,dest=dest)

def file_deps(self, m : str, timeout:Optional[float] = None) -> Any:
"""Get information about a loaded module."""
return self.connection.file_deps(m,timeout=timeout).result()
def file_deps( self
, m : str, isFile:bool
, timeout:Optional[float] = None) -> Any:
"""Get information about a module or a file."""
return self.connection.file_deps(m,isFile,timeout=timeout).result()
62 changes: 31 additions & 31 deletions cryptol-remote-api/python/poetry.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

7 changes: 4 additions & 3 deletions cryptol-remote-api/python/tests/cryptol/test_filedeps.py
Original file line number Diff line number Diff line change
Expand Up @@ -4,11 +4,12 @@
import cryptol
from cryptol.single_connection import *


class TestFileDeps(unittest.TestCase):
def test_FileDeps(self):
def test_FileDeps(self) -> None:
connect(verify=False)
load_file(str(Path('tests','cryptol','test-files','Id.cry')))
result = file_deps('Id')
path = str(Path('tests','cryptol','test-files','Id.cry'))
result = file_deps(path,True)
self.assertEqual(result['fingerprint'],"8A49C6A461AF276DF56C4FE4279BCFC51D891214")
self.assertEqual(result['foreign'],[])
self.assertEqual(result['imports'],['Cryptol'])
Expand Down
44 changes: 19 additions & 25 deletions cryptol-remote-api/src/CryptolServer/FileDeps.hs
Original file line number Diff line number Diff line change
Expand Up @@ -7,47 +7,39 @@ module CryptolServer.FileDeps
) where

import Data.Text (Text)
import qualified Data.Text as Text
import qualified Data.Set as Set
import Control.Monad.IO.Class(liftIO)
import System.Directory(canonicalizePath)

import qualified Data.Aeson as JSON
import Data.Aeson (FromJSON(..),ToJSON(..),(.=),(.:))
import qualified Argo.Doc as Doc

import Cryptol.Parser.AST (ModName)
import Cryptol.Parser (parseModName)
import Cryptol.ModuleSystem.Env
(LoadedModuleG(..), FileInfo(..), lookupTCEntity, ModulePath(..))
import Cryptol.ModuleSystem(getFileDependencies,getModuleDependencies)
import Cryptol.ModuleSystem.Env (FileInfo(..), ModulePath(..))
import Cryptol.ModuleSystem.Fingerprint(fingerprintHexString)
import Cryptol.Utils.PP(pp)

import CryptolServer
import CryptolServer.Exceptions(moduleNotLoaded)

data FileDepsParams = FileDepsOfModule ModName
| FileDepsOfFile FilePath

data FileDeps = FileDeps
{ fdSource :: ModulePath
, fdInfo :: FileInfo
}

fileDeps :: FileDepsParams -> CryptolCommand FileDeps
fileDeps (FileDepsOfModule m) =
do env <- getModuleEnv
case lookupTCEntity m env of
Nothing -> raise (moduleNotLoaded m)
Just lm ->
do src <- case lmFilePath lm of
InFile f' -> InFile <$> liftIO (canonicalizePath f')
InMem l x -> pure (InMem l x)
pure FileDeps { fdSource = src, fdInfo = lmFileInfo lm }

fileDeps param =
do (p,fi) <- case param of
FileDepsOfFile f -> liftModuleCmd (getFileDependencies f)
FileDepsOfModule m -> liftModuleCmd (getModuleDependencies m)
pure FileDeps { fdSource = p, fdInfo = fi }

fileDepsDescr :: Doc.Block
fileDepsDescr =
txt [ "Get information about the dependencies of a loaded top-level module."
txt [ "Get information about the dependencies of a file or module."
, " The dependencies include the dependencies of modules nested in this one."
]

Expand All @@ -57,14 +49,15 @@ txt xs = Doc.Paragraph (map Doc.Text xs)
instance FromJSON FileDepsParams where
parseJSON =
JSON.withObject "params for \"file deps\"" $
\o -> do val <- o .: "module name"
JSON.withText
"module name"
(\str ->
case parseModName (Text.unpack str) of
\o -> do name <- o .: "name"
isFile <- o .: "is-file"
if isFile
then pure (FileDepsOfFile name)
else case parseModName name of
Nothing -> mempty
Just n -> return (FileDepsOfModule n))
val
Just n -> return (FileDepsOfModule n)



instance ToJSON FileDeps where
toJSON fd =
Expand All @@ -83,7 +76,8 @@ instance ToJSON FileDeps where

instance Doc.DescribedMethod FileDepsParams FileDeps where
parameterFieldDescription =
[ ("module name", txt ["Get information about this loaded module."])
[ ("name", txt ["Get information about this entity."])
, ("is-file", txt ["Indicates if the name is a file (true) or module (false)"])
]

resultFieldDescription =
Expand Down
Loading

0 comments on commit b35170a

Please sign in to comment.