From 3a66cea2c7dd12b55f9311938522d827417339df Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Tue, 29 Nov 2022 11:14:10 -0800 Subject: [PATCH] Make the REPL and Python API more similar * Also adds a test * updates CHANGES * Add `file_deps` to synchronous and single_connection --- CHANGES.md | 4 ++++ cryptol-remote-api/cryptol-remote-api/Main.hs | 2 +- cryptol-remote-api/docs/Cryptol.rst | 12 ++++++------ cryptol-remote-api/python/cryptol/commands.py | 2 +- .../python/cryptol/single_connection.py | 6 ++++++ .../python/cryptol/synchronous.py | 4 ++++ .../python/tests/cryptol/test_filedeps.py | 19 +++++++++++++++++++ .../src/CryptolServer/FileDeps.hs | 10 +++++----- src/Cryptol/REPL/Command.hs | 4 ++-- 9 files changed, 48 insertions(+), 15 deletions(-) create mode 100644 cryptol-remote-api/python/tests/cryptol/test_filedeps.py diff --git a/CHANGES.md b/CHANGES.md index d12b799e6..e1885fea9 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -34,6 +34,10 @@ These affect random test generation, and help write reproducable Cryptol scripts. +* Add `:file-deps` commnads ro the REPL and Python API. + It shows information about the source files and dependencies of + loaded modules. + ## Bug fixes * Fix a bug in the What4 backend that could cause applications of `(@)` with diff --git a/cryptol-remote-api/cryptol-remote-api/Main.hs b/cryptol-remote-api/cryptol-remote-api/Main.hs index e56b73ab1..1008f5947 100644 --- a/cryptol-remote-api/cryptol-remote-api/Main.hs +++ b/cryptol-remote-api/cryptol-remote-api/Main.hs @@ -93,7 +93,7 @@ cryptolMethods = loadFileDescr loadFile , command - "file deps" + "file-deps" fileDepsDescr fileDeps , command diff --git a/cryptol-remote-api/docs/Cryptol.rst b/cryptol-remote-api/docs/Cryptol.rst index 84ed315d5..27849c329 100644 --- a/cryptol-remote-api/docs/Cryptol.rst +++ b/cryptol-remote-api/docs/Cryptol.rst @@ -388,10 +388,10 @@ No return fields -file deps (command) +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 loaded top-level module. The dependencies include the dependencies of modules nested in this one. Parameter fields ++++++++++++++++ @@ -407,7 +407,7 @@ Return fields ``source`` - File containing the module.For internal modules this is an object { internal: LABEL } + File containing the module. For internal modules this is an object { internal: "LABEL" }. @@ -417,17 +417,17 @@ Return fields ``includes`` - Files included in this module + Files included in this module. ``imports`` - Modules imported by this module + Modules imported by this module. ``foreign`` - Foreign libraries loaded by this module + Foreign libraries loaded by this module. diff --git a/cryptol-remote-api/python/cryptol/commands.py b/cryptol-remote-api/python/cryptol/commands.py index d76c43dde..1fb1acc2e 100644 --- a/cryptol-remote-api/python/cryptol/commands.py +++ b/cryptol-remote-api/python/cryptol/commands.py @@ -77,7 +77,7 @@ def process_result(self, res : Any) -> Any: 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) + super(CryptolFileDeps, self).__init__('file-deps', {'module name': mod_name}, connection, timeout=timeout) def process_result(self, res : Any) -> Any: return res diff --git a/cryptol-remote-api/python/cryptol/single_connection.py b/cryptol-remote-api/python/cryptol/single_connection.py index c498463b3..b8105eea2 100644 --- a/cryptol-remote-api/python/cryptol/single_connection.py +++ b/cryptol-remote-api/python/cryptol/single_connection.py @@ -242,3 +242,9 @@ def interrupt() -> None: 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) + + diff --git a/cryptol-remote-api/python/cryptol/synchronous.py b/cryptol-remote-api/python/cryptol/synchronous.py index f9b54d456..9d3230028 100644 --- a/cryptol-remote-api/python/cryptol/synchronous.py +++ b/cryptol-remote-api/python/cryptol/synchronous.py @@ -379,3 +379,7 @@ def interrupt(self) -> None: 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() diff --git a/cryptol-remote-api/python/tests/cryptol/test_filedeps.py b/cryptol-remote-api/python/tests/cryptol/test_filedeps.py new file mode 100644 index 000000000..d90dd5c24 --- /dev/null +++ b/cryptol-remote-api/python/tests/cryptol/test_filedeps.py @@ -0,0 +1,19 @@ +import unittest +from pathlib import Path +import unittest +import cryptol +from cryptol.single_connection import * + +class TestFileDeps(unittest.TestCase): + def test_FileDeps(self): + connect(verify=False) + load_file(str(Path('tests','cryptol','test-files','Id.cry'))) + result = file_deps('Id') + self.assertEqual(result['fingerprint'],"8A49C6A461AF276DF56C4FE4279BCFC51D891214") + self.assertEqual(result['foreign'],[]) + self.assertEqual(result['imports'],['Cryptol']) + self.assertEqual(result['includes'],[]) + # we don't check source because it is system dependent + +if __name__ == "__main__": + unittest.main() diff --git a/cryptol-remote-api/src/CryptolServer/FileDeps.hs b/cryptol-remote-api/src/CryptolServer/FileDeps.hs index cf25d94ad..f57f9b3f8 100644 --- a/cryptol-remote-api/src/CryptolServer/FileDeps.hs +++ b/cryptol-remote-api/src/CryptolServer/FileDeps.hs @@ -48,7 +48,7 @@ fileDeps (FileDepsOfModule m) = fileDepsDescr :: Doc.Block fileDepsDescr = txt [ "Get information about the dependencies of a loaded top-level module." - , "The dependencies include the dependencies of modules nested in this one." + , " The dependencies include the dependencies of modules nested in this one." ] txt :: [Text] -> Doc.Block @@ -88,12 +88,12 @@ instance Doc.DescribedMethod FileDepsParams FileDeps where resultFieldDescription = [ ("source", txt [ "File containing the module." - , "For internal modules this is an object { internal: LABEL }" + , " For internal modules this is an object { internal: \"LABEL\" }." ]) , ("fingerprint", txt ["A hash of the module content."]) - , ("includes", txt ["Files included in this module"]) - , ("imports", txt ["Modules imported by this module"]) - , ("foreign", txt ["Foreign libraries loaded by this module"]) + , ("includes", txt ["Files included in this module."]) + , ("imports", txt ["Modules imported by this module."]) + , ("foreign", txt ["Foreign libraries loaded by this module."]) ] diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index b32be2261..cb2ae4b47 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -337,7 +337,7 @@ commandList = , "but with a .h extension." ]) - , CommandDescr [ ":module-info" ] [ "[MODULE]" ] (FilenameArg moduleInfoCmd) + , CommandDescr [ ":file-deps" ] [ "[MODULE]" ] (FilenameArg moduleInfoCmd) "Show information about the source of a loaded module." (unlines [ "If the module name is not specified," @@ -1832,7 +1832,7 @@ moduleInfoCmd modString M.InMem l _ -> rPutStrLn ("{ \"internal\": " ++ show l ++ " }") let fi = M.lmFileInfo lm - rPutStrLn (tab (", \"fingerprint\":\" 0x" ++ + rPutStrLn (tab (", \"fingerprint\": \"0x" ++ fingerprintHexString (M.fiFingerprint fi) ++ "\""))