Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Module dependencies without loading #1477

Merged
merged 6 commits into from
Dec 5, 2022
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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