From 33cc8743df0dad6ceb68d55ea8163faa296f0855 Mon Sep 17 00:00:00 2001 From: Eric Mertens Date: Thu, 19 Sep 2024 15:26:30 -0700 Subject: [PATCH 1/6] Add a modules() method to the cryptol python api for listing modules and their documentation --- .../cryptol-eval-server/Main.hs | 5 ++ cryptol-remote-api/cryptol-remote-api.cabal | 1 + cryptol-remote-api/cryptol-remote-api/Main.hs | 5 ++ cryptol-remote-api/python/cryptol/commands.py | 6 ++ .../python/cryptol/connection.py | 16 +++-- .../src/CryptolServer/Modules.hs | 67 +++++++++++++++++++ 6 files changed, 96 insertions(+), 4 deletions(-) create mode 100644 cryptol-remote-api/src/CryptolServer/Modules.hs diff --git a/cryptol-remote-api/cryptol-eval-server/Main.hs b/cryptol-remote-api/cryptol-eval-server/Main.hs index 2ed8796e2..7a27cafe2 100644 --- a/cryptol-remote-api/cryptol-eval-server/Main.hs +++ b/cryptol-remote-api/cryptol-eval-server/Main.hs @@ -48,6 +48,7 @@ import CryptolServer.ExtendSearchPath import CryptolServer.FocusedModule ( focusedModuleDescr, focusedModule ) import CryptolServer.Names ( visibleNamesDescr, visibleNames ) +import CryptolServer.Modules ( visibleModulesDescr, visibleModules ) import CryptolServer.TypeCheck ( checkType ) import CryptolServer.Sat ( proveSatDescr, proveSat ) import Cryptol.REPL.Command (CommandResult, DocstringResult) @@ -156,6 +157,10 @@ cryptolEvalMethods = "visible names" visibleNamesDescr visibleNames + , command + "visible modules" + visibleModulesDescr + visibleModules , command "check type" (Doc.Paragraph [Doc.Text "Check and return the type of the given expression."]) diff --git a/cryptol-remote-api/cryptol-remote-api.cabal b/cryptol-remote-api/cryptol-remote-api.cabal index 89be99a66..5b98fe7b0 100644 --- a/cryptol-remote-api/cryptol-remote-api.cabal +++ b/cryptol-remote-api/cryptol-remote-api.cabal @@ -78,6 +78,7 @@ library CryptolServer.FocusedModule CryptolServer.Interrupt CryptolServer.LoadModule + CryptolServer.Modules CryptolServer.Names CryptolServer.Options CryptolServer.Sat diff --git a/cryptol-remote-api/cryptol-remote-api/Main.hs b/cryptol-remote-api/cryptol-remote-api/Main.hs index 63f3be37e..1bb59bbec 100644 --- a/cryptol-remote-api/cryptol-remote-api/Main.hs +++ b/cryptol-remote-api/cryptol-remote-api/Main.hs @@ -32,6 +32,7 @@ import CryptolServer.Interrupt import CryptolServer.LoadModule ( loadFile, loadFileDescr, loadModule, loadModuleDescr ) import CryptolServer.Names ( visibleNames, visibleNamesDescr ) +import CryptolServer.Modules ( visibleModules, visibleModulesDescr ) import CryptolServer.Sat ( proveSat, proveSatDescr ) import CryptolServer.TypeCheck ( checkType, checkTypeDescr ) import CryptolServer.Version ( version, versionDescr ) @@ -121,6 +122,10 @@ cryptolMethods = "visible names" visibleNamesDescr visibleNames + , command + "visible modules" + visibleModulesDescr + visibleModules , command "check type" checkTypeDescr diff --git a/cryptol-remote-api/python/cryptol/commands.py b/cryptol-remote-api/python/cryptol/commands.py index d429d7595..fef19ae8f 100644 --- a/cryptol-remote-api/python/cryptol/commands.py +++ b/cryptol-remote-api/python/cryptol/commands.py @@ -278,7 +278,13 @@ def __init__(self, connection : HasProtocolState, expr : Any, solver : Solver, t class CryptolSafe(CryptolProveSat): def __init__(self, connection : HasProtocolState, expr : Any, solver : Solver, timeout: Optional[float]) -> None: super(CryptolSafe, self).__init__(connection, SmtQueryType.SAFE, expr, solver, 1, timeout=timeout) + +class CryptolModules(argo.Command): + def __init__(self, connection : HasProtocolState, timeout: Optional[float]) -> None: + super(CryptolModules, self).__init__('visible modules', {}, connection, timeout=timeout) + def process_result(self, res : Any) -> Any: + return res class CryptolNames(argo.Command): def __init__(self, connection : HasProtocolState, timeout: Optional[float]) -> None: diff --git a/cryptol-remote-api/python/cryptol/connection.py b/cryptol-remote-api/python/cryptol/connection.py index aa2bafc8e..d434baf2d 100644 --- a/cryptol-remote-api/python/cryptol/connection.py +++ b/cryptol-remote-api/python/cryptol/connection.py @@ -170,11 +170,11 @@ def __init__(self, def get_default_timeout(self) -> Optional[float]: """Get the value of the optional default timeout for methods (in seconds).""" return self.timeout - + def set_default_timeout(self, timeout : Optional[float]) -> None: """Set the value of the optional default timeout for methods (in seconds).""" self.timeout = timeout - + # Currently disabled in (overly?) conservative effort to not accidentally # duplicate and share mutable state. @@ -203,10 +203,10 @@ def load_file(self, filename : str, *, timeout:Optional[float] = None) -> argo.C timeout = timeout if timeout is not None else self.timeout self.most_recent_result = CryptolLoadFile(self, filename, timeout) return self.most_recent_result - + def check_docstrings(self, timeout: Optional[float] = None) -> argo.Command: """Check docstrings - + :param timeout: Optional timeout for this request (in seconds). """ timeout = timeout if timeout is not None else self.timeout @@ -396,6 +396,14 @@ def safe(self, expr : Any, solver : solver.Solver = solver.Z3, *, timeout:Option self.most_recent_result = CryptolSafe(self, expr, solver, timeout) return self.most_recent_result + def modules(self, *, timeout:Optional[float] = None) -> argo.Command: + """Discover the list of modules and submodules currently in scope in the current context. + + :param timeout: Optional timeout for this request (in seconds).""" + timeout = timeout if timeout is not None else self.timeout + self.most_recent_result = CryptolModules(self, timeout) + return self.most_recent_result + def names(self, *, timeout:Optional[float] = None) -> argo.Command: """Discover the list of term names currently in scope in the current context. diff --git a/cryptol-remote-api/src/CryptolServer/Modules.hs b/cryptol-remote-api/src/CryptolServer/Modules.hs new file mode 100644 index 000000000..1c431ae14 --- /dev/null +++ b/cryptol-remote-api/src/CryptolServer/Modules.hs @@ -0,0 +1,67 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE OverloadedStrings #-} +module CryptolServer.Modules + ( visibleModules + , visibleModulesDescr + ) where + +import qualified Argo.Doc as Doc +import qualified Data.Aeson as JSON +import Data.Aeson ((.=)) +import qualified Data.Map as Map +import Data.Text (unpack) + +import Cryptol.ModuleSystem.Env (loadedModules) +import Cryptol.ModuleSystem.Interface (ifsDoc) +import Cryptol.TypeCheck.AST as T +import Cryptol.Utils.PP (pp) + +import CryptolServer (CryptolCommand, getModuleEnv) + +data VisibleModulesParams = VisibleNamesParams + +instance JSON.FromJSON VisibleModulesParams where + parseJSON _ = pure VisibleNamesParams + +instance Doc.DescribedMethod VisibleModulesParams [ModuleInfo] where + parameterFieldDescription = [] + + resultFieldDescription = + [ ("name", + Doc.Paragraph [Doc.Text "A human-readable representation of the name"]) + , ("documentation", + Doc.Paragraph [Doc.Text "An optional field containing documentation string for the name, if it is documented"]) + ] + +visibleModulesDescr :: Doc.Block +visibleModulesDescr = + Doc.Paragraph [Doc.Text "List the currently visible (i.e., in scope) module names."] + +visibleModules :: VisibleModulesParams -> CryptolCommand [ModuleInfo] +visibleModules _ = concatMap moduleToInfos . loadedModules <$> getModuleEnv + + +moduleToInfos :: T.Module -> [ModuleInfo] +moduleToInfos m = + ModuleInfo + { name = show (pp (T.mName m)) + , docs = map unpack (T.mDoc m) + } : + [ ModuleInfo + { name = show (pp k) + , docs = map unpack (ifsDoc (T.smIface v)) + } + | (k,v) <- Map.assocs (T.mSubmodules m) + ] + +data ModuleInfo = + ModuleInfo + { name :: String + , docs :: [String] + } + +instance JSON.ToJSON ModuleInfo where + toJSON ModuleInfo{..} = JSON.object (("name" .= name) : ["documentation" .= docs | not (null docs)]) From 9fed2c52756dcdbd98a689b22c393e7fdf08a95e Mon Sep 17 00:00:00 2001 From: Eric Mertens Date: Thu, 19 Sep 2024 15:27:35 -0700 Subject: [PATCH 2/6] Changelog! --- cryptol-remote-api/python/CHANGELOG.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/cryptol-remote-api/python/CHANGELOG.md b/cryptol-remote-api/python/CHANGELOG.md index 52f74ea3f..b0a79036d 100644 --- a/cryptol-remote-api/python/CHANGELOG.md +++ b/cryptol-remote-api/python/CHANGELOG.md @@ -1,5 +1,10 @@ # Revision history for `cryptol` Python package +## next + +* Add `modules` command to return the modules, submodules and associated + documentation for them. + ## 3.2.1 -- 2024-08-18 * Require building with `argo-client-0.0.13` or later. `argo-client-0.0.13` uses From a486cb8d36ba711d62b7e0a80d7e58c6540a4f5e Mon Sep 17 00:00:00 2001 From: Eric Mertens Date: Thu, 19 Sep 2024 15:41:52 -0700 Subject: [PATCH 3/6] update rpc docs --- cryptol-remote-api/docs/Cryptol.rst | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) diff --git a/cryptol-remote-api/docs/Cryptol.rst b/cryptol-remote-api/docs/Cryptol.rst index 48956ee63..c7a3e0c51 100644 --- a/cryptol-remote-api/docs/Cryptol.rst +++ b/cryptol-remote-api/docs/Cryptol.rst @@ -677,6 +677,32 @@ Return fields +visible modules (command) +~~~~~~~~~~~~~~~~~~~~~~~~~ + +List the currently visible (i.e., in scope) module names. + +Parameter fields +++++++++++++++++ + +No parameters + + +Return fields ++++++++++++++ + + +``name`` + A human-readable representation of the name + + + +``documentation`` + An optional field containing documentation string for the name, if it is documented + + + + check type (command) ~~~~~~~~~~~~~~~~~~~~ From 122aeea5591bd2778c1b60cd87738360d20026ec Mon Sep 17 00:00:00 2001 From: Eric Mertens Date: Thu, 19 Sep 2024 16:00:03 -0700 Subject: [PATCH 4/6] Additional changelog --- cryptol-remote-api/CHANGELOG.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/cryptol-remote-api/CHANGELOG.md b/cryptol-remote-api/CHANGELOG.md index 9539697da..a09163ef0 100644 --- a/cryptol-remote-api/CHANGELOG.md +++ b/cryptol-remote-api/CHANGELOG.md @@ -2,6 +2,8 @@ ## next -- TBA +* Add `visible modules` command to return the modules, submodules and associated + documentation for them. ## 3.2.0 -- 2024-08-20 From 7735acfa130861b45141ef2642420011b3b22a37 Mon Sep 17 00:00:00 2001 From: Eric Mertens Date: Thu, 19 Sep 2024 17:23:08 -0700 Subject: [PATCH 5/6] Add modules() to the many layers of the API and add a test case --- cryptol-remote-api/docs/Cryptol.rst | 11 +++-- .../python/cryptol/cryptoltypes.py | 16 ++++++++ .../python/cryptol/single_connection.py | 4 ++ .../python/cryptol/synchronous.py | 8 ++++ .../tests/cryptol/test-files/Modules.cry | 18 +++++++++ .../python/tests/cryptol/test_modules.py | 26 ++++++++++++ .../src/CryptolServer/Modules.hs | 40 +++++++++++++------ 7 files changed, 108 insertions(+), 15 deletions(-) create mode 100644 cryptol-remote-api/python/tests/cryptol/test-files/Modules.cry create mode 100644 cryptol-remote-api/python/tests/cryptol/test_modules.py diff --git a/cryptol-remote-api/docs/Cryptol.rst b/cryptol-remote-api/docs/Cryptol.rst index c7a3e0c51..9c623d251 100644 --- a/cryptol-remote-api/docs/Cryptol.rst +++ b/cryptol-remote-api/docs/Cryptol.rst @@ -692,13 +692,18 @@ Return fields +++++++++++++ -``name`` - A human-readable representation of the name +``module`` + A human-readable representation of the module's name ``documentation`` - An optional field containing documentation string for the name, if it is documented + An optional field containing documentation strings for the module,if it is documented + + + +``parameterized`` + A Boolean value indicating whether the focused module isparameterized diff --git a/cryptol-remote-api/python/cryptol/cryptoltypes.py b/cryptol-remote-api/python/cryptol/cryptoltypes.py index 84c0b86fd..3eb27efca 100644 --- a/cryptol-remote-api/python/cryptol/cryptoltypes.py +++ b/cryptol-remote-api/python/cryptol/cryptoltypes.py @@ -476,7 +476,23 @@ def argument_types(obj : Union[CryptolTypeSchema, CryptolType]) -> List[CryptolT return [arg1] + args else: return [] + +# ----------------------------------------------------------- +# Cryptol Module Info +# ----------------------------------------------------------- + +CryptolVisibleModuleInfo = TypedDict("CryptolVisibleModuleInfo", + { "module": str + , "parameterized": bool + , "documentation": Optional[List[str]] + }) +def to_cryptol_visible_module_info(d : Any) -> CryptolVisibleModuleInfo: + if check_dict(d, required_keys={"module": str, "parameterized": bool}, optional_keys={"documentation": List}): + # the call to check_dict ensures this cast is OK + return cast(CryptolVisibleModuleInfo, d) + else: + raise ValueError("Cryptol visible module info is malformed: " + str(d)) # ----------------------------------------------------------- # Cryptol Name Info diff --git a/cryptol-remote-api/python/cryptol/single_connection.py b/cryptol-remote-api/python/cryptol/single_connection.py index 3538ec1ef..cdaf87ca0 100644 --- a/cryptol-remote-api/python/cryptol/single_connection.py +++ b/cryptol-remote-api/python/cryptol/single_connection.py @@ -218,6 +218,10 @@ def safe(expr : Any, solver : Solver = Z3, *, timeout:Optional[float] = None) -> """ return __get_designated_connection().safe(expr, solver, timeout=timeout) +def modules(*, timeout:Optional[float] = None) -> List[cryptoltypes.CryptolVisibleModuleInfo]: + """Discover the list of modules currently in scope in the current context.""" + return __get_designated_connection().modules(timeout=timeout) + def names(*, timeout:Optional[float] = None) -> List[cryptoltypes.CryptolNameInfo]: """Discover the list of term names currently in scope in the current context.""" return __get_designated_connection().names(timeout=timeout) diff --git a/cryptol-remote-api/python/cryptol/synchronous.py b/cryptol-remote-api/python/cryptol/synchronous.py index cc85729d6..af3075793 100644 --- a/cryptol-remote-api/python/cryptol/synchronous.py +++ b/cryptol-remote-api/python/cryptol/synchronous.py @@ -366,6 +366,14 @@ def safe(self, expr : Any, solver : Solver = Z3, *, timeout:Optional[float] = No else: raise ValueError("Unknown solver type: " + str(solver)) + def modules(self, *, timeout:Optional[float] = None) -> List[cryptoltypes.CryptolVisibleModuleInfo]: + """Discover the list of term names currently in scope in the current context.""" + res = self.connection.modules(timeout=timeout).result() + if isinstance(res, list): + return [ cryptoltypes.to_cryptol_visible_module_info(entry) for entry in res ] + else: + raise ValueError("Result of `modules()` is not a list: " + str(res)) + def names(self, *, timeout:Optional[float] = None) -> List[cryptoltypes.CryptolNameInfo]: """Discover the list of term names currently in scope in the current context.""" res = self.connection.names(timeout=timeout).result() diff --git a/cryptol-remote-api/python/tests/cryptol/test-files/Modules.cry b/cryptol-remote-api/python/tests/cryptol/test-files/Modules.cry new file mode 100644 index 000000000..c40df5062 --- /dev/null +++ b/cryptol-remote-api/python/tests/cryptol/test-files/Modules.cry @@ -0,0 +1,18 @@ +/** + * A top-level + * docstring + */ +module Modules where + +/** A functor docstring */ +submodule F where + parameter + type N : # + + /** A submodule in a functor docstring */ + submodule Q where + q = () + +/** A submodule docstring */ +submodule M = submodule F where + type N = 0 diff --git a/cryptol-remote-api/python/tests/cryptol/test_modules.py b/cryptol-remote-api/python/tests/cryptol/test_modules.py new file mode 100644 index 000000000..92ed320b2 --- /dev/null +++ b/cryptol-remote-api/python/tests/cryptol/test_modules.py @@ -0,0 +1,26 @@ +import unittest +from pathlib import Path +import cryptol +from cryptol.single_connection import * + +class TestModules(unittest.TestCase): + def test_modules(self): + connect(verify=False) + load_file(str(Path('tests','cryptol','test-files', 'Modules.cry'))) + + expected = [ + {'module': 'Cryptol', 'parameterized': False}, + {'module': 'Modules', 'parameterized': False, 'documentation': ['A top-level\ndocstring\n']}, + {'module': 'Modules::`where` argument of M', 'parameterized': False}, + {'module': 'Modules::M', 'parameterized': False, 'documentation': ['A submodule docstring\n', 'A functor docstring\n']}, + {'module': 'Modules::M::Q', 'parameterized': False, 'documentation': ['A submodule in a functor docstring\n']}, + {'module': 'Modules::F', 'parameterized': True, 'documentation': ['A functor docstring\n']}, + {'module': 'Modules::F::Q', 'parameterized': True, 'documentation': ['A submodule in a functor docstring\n']}, + ] + + names_to_check = modules() + + self.assertCountEqual(expected, names_to_check) + +if __name__ == "__main__": + unittest.main() diff --git a/cryptol-remote-api/src/CryptolServer/Modules.hs b/cryptol-remote-api/src/CryptolServer/Modules.hs index 1c431ae14..d2a876817 100644 --- a/cryptol-remote-api/src/CryptolServer/Modules.hs +++ b/cryptol-remote-api/src/CryptolServer/Modules.hs @@ -17,51 +17,67 @@ import Data.Text (unpack) import Cryptol.ModuleSystem.Env (loadedModules) import Cryptol.ModuleSystem.Interface (ifsDoc) import Cryptol.TypeCheck.AST as T -import Cryptol.Utils.PP (pp) +import Cryptol.Utils.PP (PP, pp) import CryptolServer (CryptolCommand, getModuleEnv) + data VisibleModulesParams = VisibleNamesParams instance JSON.FromJSON VisibleModulesParams where parseJSON _ = pure VisibleNamesParams -instance Doc.DescribedMethod VisibleModulesParams [ModuleInfo] where +instance Doc.DescribedMethod VisibleModulesParams [VisibleModuleInfo] where parameterFieldDescription = [] resultFieldDescription = - [ ("name", - Doc.Paragraph [Doc.Text "A human-readable representation of the name"]) + [ ("module", + Doc.Paragraph [ Doc.Text "A human-readable representation of the module's name"]) , ("documentation", - Doc.Paragraph [Doc.Text "An optional field containing documentation string for the name, if it is documented"]) + Doc.Paragraph [ Doc.Text "An optional field containing documentation strings for the module," + , Doc.Text "if it is documented"]) + , ("parameterized", + Doc.Paragraph [ Doc.Text "A Boolean value indicating whether the focused module is" + , Doc.Text "parameterized" + ]) ] visibleModulesDescr :: Doc.Block visibleModulesDescr = Doc.Paragraph [Doc.Text "List the currently visible (i.e., in scope) module names."] -visibleModules :: VisibleModulesParams -> CryptolCommand [ModuleInfo] -visibleModules _ = concatMap moduleToInfos . loadedModules <$> getModuleEnv +visibleModules :: VisibleModulesParams -> CryptolCommand [VisibleModuleInfo] +visibleModules _ = concatMap (moduleToInfos False) . loadedModules <$> getModuleEnv -moduleToInfos :: T.Module -> [ModuleInfo] -moduleToInfos m = +moduleToInfos :: PP a => Bool -> T.ModuleG a -> [VisibleModuleInfo] +moduleToInfos p m = ModuleInfo { name = show (pp (T.mName m)) + , parameterized = p , docs = map unpack (T.mDoc m) } : [ ModuleInfo { name = show (pp k) + , parameterized = p , docs = map unpack (ifsDoc (T.smIface v)) } | (k,v) <- Map.assocs (T.mSubmodules m) + ] ++ + [ x + | v <- Map.elems (T.mFunctors m) + , x <- moduleToInfos True v ] -data ModuleInfo = +data VisibleModuleInfo = ModuleInfo { name :: String + , parameterized :: Bool , docs :: [String] } -instance JSON.ToJSON ModuleInfo where - toJSON ModuleInfo{..} = JSON.object (("name" .= name) : ["documentation" .= docs | not (null docs)]) +instance JSON.ToJSON VisibleModuleInfo where + toJSON ModuleInfo{..} = JSON.object ( + [ "module" .= name + , "parameterized" .= parameterized] ++ + ["documentation" .= docs | not (null docs)]) From bda99ac63d41b961387b3198aeee1d79d5ee6c2c Mon Sep 17 00:00:00 2001 From: Eric Mertens Date: Fri, 20 Sep 2024 09:06:08 -0700 Subject: [PATCH 6/6] Put the space back into the manually line-wrapped documentation --- cryptol-remote-api/docs/Cryptol.rst | 4 ++-- cryptol-remote-api/src/CryptolServer/Modules.hs | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/cryptol-remote-api/docs/Cryptol.rst b/cryptol-remote-api/docs/Cryptol.rst index 9c623d251..6d4feb423 100644 --- a/cryptol-remote-api/docs/Cryptol.rst +++ b/cryptol-remote-api/docs/Cryptol.rst @@ -698,12 +698,12 @@ Return fields ``documentation`` - An optional field containing documentation strings for the module,if it is documented + An optional field containing documentation strings for the module, if it is documented ``parameterized`` - A Boolean value indicating whether the focused module isparameterized + A Boolean value indicating whether the focused module is parameterized diff --git a/cryptol-remote-api/src/CryptolServer/Modules.hs b/cryptol-remote-api/src/CryptolServer/Modules.hs index d2a876817..a1de36509 100644 --- a/cryptol-remote-api/src/CryptolServer/Modules.hs +++ b/cryptol-remote-api/src/CryptolServer/Modules.hs @@ -34,10 +34,10 @@ instance Doc.DescribedMethod VisibleModulesParams [VisibleModuleInfo] where [ ("module", Doc.Paragraph [ Doc.Text "A human-readable representation of the module's name"]) , ("documentation", - Doc.Paragraph [ Doc.Text "An optional field containing documentation strings for the module," + Doc.Paragraph [ Doc.Text "An optional field containing documentation strings for the module, " , Doc.Text "if it is documented"]) , ("parameterized", - Doc.Paragraph [ Doc.Text "A Boolean value indicating whether the focused module is" + Doc.Paragraph [ Doc.Text "A Boolean value indicating whether the focused module is " , Doc.Text "parameterized" ]) ]