Add a modules() method to the cryptol python api for listing modules …

…and their documentation (#1755)

* Add a modules() method to the cryptol python api for listing modules and their documentation

* Changelog!

* update rpc docs

* Additional changelog

* Add modules() to the many layers of the API and add a test case

* Put the space back into the manually line-wrapped documentation

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
 

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."])

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

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

cryptol-remote-api/docs/Cryptol.rst

@@ -677,6 +677,37 @@ Return fields
 
 
 
+visible modules (command)
+~~~~~~~~~~~~~~~~~~~~~~~~~
+
+List the currently visible (i.e., in scope) module names.
+
+Parameter fields
+++++++++++++++++
+
+No parameters
+
+
+Return fields
++++++++++++++
+
+
+``module``
+  A human-readable representation of the module's name
+
+
+
+``documentation``
+  An optional field containing documentation strings for the module, if it is documented
+
+
+
+``parameterized``
+  A Boolean value indicating whether the focused module is parameterized
+
+
+
+
 check type (command)
 ~~~~~~~~~~~~~~~~~~~~
 

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

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:

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.
 

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

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)

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()

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

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()

cryptol-remote-api/src/CryptolServer/Modules.hs

@@ -0,0 +1,83 @@
+{-# 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, pp)
+
+import CryptolServer (CryptolCommand, getModuleEnv)
+
+
+data VisibleModulesParams = VisibleNamesParams
+
+instance JSON.FromJSON VisibleModulesParams where
+  parseJSON _ = pure VisibleNamesParams
+
+instance Doc.DescribedMethod VisibleModulesParams [VisibleModuleInfo] where
+  parameterFieldDescription = []
+
+  resultFieldDescription =
+    [ ("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.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 [VisibleModuleInfo]
+visibleModules _ = concatMap (moduleToInfos False) . loadedModules <$> getModuleEnv
+
+
+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 VisibleModuleInfo =
+  ModuleInfo
+  { name :: String
+  , parameterized :: Bool
+  , docs :: [String]
+  }
+
+instance JSON.ToJSON VisibleModuleInfo where
+  toJSON ModuleInfo{..} = JSON.object (
+    [ "module" .= name
+    , "parameterized" .= parameterized] ++
+    ["documentation" .= docs | not (null docs)])