Add more info to names() in Python API

cryptol-remote-api/CHANGELOG.md

@@ -1,6 +1,14 @@
 # Revision history for `cryptol-remote-api` and `cryptol-eval-server`
 
-## 2.13.0 -- YYYY-MM-DD
+## NEXT -- YYYY-MM-DD
+
+* Add more fields (such as `pragmas`, `parameter`, `module`, and `infix`) to
+  the response to the RPC `visible names` method.
+* Do not error if `visible names` is called when a parameterized module is
+  loaded (this used to cause the appearance of the server hanging in such a
+  case).
+
+## 2.13.0 -- 2022-05-17
 
 * v2.13.0 release in tandem with the Cryptol 2.13.0 release. See the Cryptol
   2.13.0 release notes for relevant Cryptol changes. No notable changes to the

cryptol-remote-api/docs/Cryptol.rst

@@ -490,7 +490,7 @@ Return fields
 visible names (command)
 ~~~~~~~~~~~~~~~~~~~~~~~
 
-List the currently visible (i.e., in scope) names.
+List the currently visible (i.e., in scope) term names.
 
 Parameter fields
 ++++++++++++++++
@@ -517,6 +517,26 @@ Return fields
 
 
 
+``module``
+  A human-readable representation of the module from which the name originates
+
+
+
+``parameter``
+  An optional field which is present iff the name is a module parameter
+
+
+
+``infix``
+  An optional field which is present iff the name is an infix operator. If present, it contains an object with two fields. One field is ``associativity``, containing one of the strings ``left-associative``, ``right-associative``, or ``non-associative``, and the other is ``level``, containing the name's precedence level.
+
+
+
+``pragmas``
+  An optional field containing a list of the name's pragmas (e.g. ``property``), if it has any
+
+
+
 ``documentation``
   An optional field containing documentation string for the name, if it is documented
 

cryptol-remote-api/python/CHANGELOG.md

@@ -1,7 +1,15 @@
 # Revision history for `cryptol` Python package
 
+## NEXT -- YYYY-MM-DD
 
-## 2.13.0 -- YYYY-MM-DD
+* Add `property_names` and `parameter_names` commands, used to get only those
+  loaded names which are properties or module parameters, respectively.
+* Add more fields (such as `pragmas`, `parameter`, `module`, and `infix`) to
+  the result of `names` (see `cryptol-remote-api` `CHANGELOG`).
+* Do not hang if `names` is called when a parameterized module is loaded
+  (see `cryptol-remote-api` `CHANGELOG`).
+
+## 2.13.0 -- 2022-05-17
 
 * v2.13.0 release in tandem with the Cryptol 2.13.0 release. See the Cryptol
   2.13.0 release notes for relevant Cryptol changes. No notable changes to the

cryptol-remote-api/python/cryptol/commands.py

@@ -270,6 +270,16 @@ def __init__(self, connection : HasProtocolState, timeout: Optional[float]) -> N
     def process_result(self, res : Any) -> Any:
         return res
 
+class CryptolParameterNames(CryptolNames):
+    def process_result(self, res : Any) -> Any:
+        res = super(CryptolParameterNames, self).process_result(res)
+        return [ n for n in res if "parameter" in n ]
+
+class CryptolPropertyNames(CryptolNames):
+    def process_result(self, res : Any) -> Any:
+        res = super(CryptolPropertyNames, self).process_result(res)
+        return [ n for n in res if "pragmas" in n and "property" in n["pragmas"] ]
+
 
 class CryptolFocusedModule(argo.Command):
     def __init__(self, connection : HasProtocolState, timeout: Optional[float]) -> None:

cryptol-remote-api/python/cryptol/connection.py

@@ -379,13 +379,31 @@ def safe(self, expr : Any, solver : solver.Solver = solver.Z3, *, timeout:Option
         return self.most_recent_result
 
     def names(self, *, timeout:Optional[float] = None) -> argo.Command:
-        """Discover the list of names currently in scope in the current context.
+        """Discover the list of term names 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 = CryptolNames(self, timeout)
         return self.most_recent_result
 
+    def parameter_names(self, *, timeout:Optional[float] = None) -> argo.Command:
+        """Discover the list of module parameter names currently in scope in the current context.
+        The result is a subset of the list returned by `names`.
+
+        :param timeout: Optional timeout for this request (in seconds)."""
+        timeout = timeout if timeout is not None else self.timeout
+        self.most_recent_result = CryptolParameterNames(self, timeout)
+        return self.most_recent_result
+
+    def property_names(self, *, timeout:Optional[float] = None) -> argo.Command:
+        """Discover the list of property names currently in scope in the current context.
+        The result is a subset of the list returned by `names`.
+
+        :param timeout: Optional timeout for this request (in seconds)."""
+        timeout = timeout if timeout is not None else self.timeout
+        self.most_recent_result = CryptolPropertyNames(self, timeout)
+        return self.most_recent_result
+
     def focused_module(self, *, timeout:Optional[float] = None) -> argo.Command:
         """Return the name of the currently-focused module.
 

cryptol-remote-api/python/cryptol/cryptoltypes.py

@@ -11,7 +11,7 @@
 import typing
 from typing import cast, Any, Dict, Iterable, List, NoReturn, Optional, TypeVar, Union
 import typing_extensions
-from typing_extensions import Protocol, runtime_checkable
+from typing_extensions import Protocol, runtime_checkable, TypedDict, NotRequired
 
 A = TypeVar('A')
 
@@ -476,3 +476,70 @@ def argument_types(obj : Union[CryptolTypeSchema, CryptolType]) -> List[CryptolT
         return [arg1] + args
     else:
         return []
+
+
+# -----------------------------------------------------------
+# Cryptol Name Info
+# -----------------------------------------------------------
+
+CryptolInfixInfo = TypedDict("CryptolInfixInfo",
+    { "associativity": Union[typing_extensions.Literal["left-associative"],
+                             typing_extensions.Literal["right-associative"],
+                             typing_extensions.Literal["non-associative"]]
+    , "level": int
+    })
+
+CryptolNameInfo = TypedDict("CryptolNameInfo",
+    { "module": str
+    , "name": str
+    , "type": CryptolTypeSchema
+    , "type string": str
+    , "documentation": NotRequired[str]
+    , "pragmas": NotRequired[List[str]]
+    , "parameter": NotRequired[typing.Tuple[()]]
+    , "infix": NotRequired[CryptolInfixInfo]
+    })
+
+def check_dict(d : Any, required_keys : Dict[str, Any], optional_keys : Dict[str, Any] = {}) -> bool:
+    return isinstance(d, dict) and all(k in d for k in required_keys) and \
+           all(k in required_keys and isinstance(d[k], required_keys[k]) or
+               k in optional_keys and isinstance(d[k], optional_keys[k]) for k in d)
+
+def to_cryptol_name_info(d : Any) -> CryptolNameInfo:
+    req_keys = {"module": str, "name": str, "type": Dict, "type string": str}
+    opt_keys = {"documentation": str, "pragmas": List, "parameter": List, "infix": Dict}
+    infix_req_keys = {"associativity": str, "level": int}
+    if check_dict(d, req_keys, opt_keys) and ("infix" not in d or check_dict(d["infix"], infix_req_keys)):
+        d["type"] = to_schema(d["type"])
+        if "parameter" in d: d["parameter"] = ()
+        # the calls to check_dict and the above ensure this cast is OK
+        return cast(CryptolNameInfo, d)
+    else:
+        raise ValueError("Cryptol name info is malformed: " + str(d))
+
+
+# -----------------------------------------------------------
+# Cryptol Module Info
+# -----------------------------------------------------------
+
+CryptolFocusedModuleInfo = TypedDict("CryptolFocusedModuleInfo",
+    { "module": str
+    , "parameterized": bool
+    })
+
+CryptolNoModuleInfo = TypedDict("CryptolNoModuleInfo",
+    { "module": None
+    })
+
+CryptolModuleInfo = Union[CryptolFocusedModuleInfo, CryptolNoModuleInfo]
+
+def to_cryptol_module_info(d : Any) -> CryptolModuleInfo:
+    if check_dict(d, {"module": str, "parameterized": bool}):
+        # the call to check_dict ensures this cast is OK
+        return cast(CryptolFocusedModuleInfo, d)
+    elif check_dict(d, {"module": type(None)}):
+        # the call to check_dict ensures this cast is OK
+        return cast(CryptolNoModuleInfo, d)
+    else:
+        raise ValueError("Cryptol module info is malformed: " + str(d))
+

cryptol-remote-api/python/cryptol/single_connection.py

@@ -218,11 +218,21 @@ def safe(expr : Any, solver : Solver = Z3, *, timeout:Optional[float] = None) ->
     """
     return __get_designated_connection().safe(expr, solver, timeout=timeout)
 
-def names(*, timeout:Optional[float] = None) -> List[Dict[str,Any]]:
-    """Discover the list of names currently in scope in the current context."""
+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)
 
-def focused_module(*, timeout:Optional[float] = None) -> Dict[str,Any]:
+def parameter_names(*, timeout:Optional[float] = None) -> List[cryptoltypes.CryptolNameInfo]:
+    """Discover the list of module parameter names currently in scope in the current context.
+    The result is a subset of the list returned by `names`."""
+    return __get_designated_connection().parameter_names(timeout=timeout)
+
+def property_names(*, timeout:Optional[float] = None) -> List[cryptoltypes.CryptolNameInfo]:
+    """Discover the list of property names currently in scope in the current context.
+    The result is a subset of the list returned by `names`."""
+    return __get_designated_connection().property_names(timeout=timeout)
+
+def focused_module(*, timeout:Optional[float] = None) -> cryptoltypes.CryptolModuleInfo:
     """Returns the name and other information about the currently-focused module."""
     return __get_designated_connection().focused_module(timeout=timeout)
 

cryptol-remote-api/python/cryptol/synchronous.py

@@ -347,21 +347,35 @@ def safe(self, expr : Any, solver : Solver = Z3, *, timeout:Optional[float] = No
         else:
             raise ValueError("Unknown solver type: " + str(solver))
 
-    def names(self, *, timeout:Optional[float] = None) -> List[Dict[str,Any]]:
-        """Discover the list of names currently in scope in the current context."""
+    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()
-        if isinstance(res, list) and all(isinstance(d, dict) and all(isinstance(k, str) for k in d.keys()) for d in res):
-            return res
+        if isinstance(res, list):
+            return [ cryptoltypes.to_cryptol_name_info(entry) for entry in res ]
         else:
-            raise ValueError("Panic! Result of `names()` is malformed: " + str(res))
+            raise ValueError("Result of `names()` is not a list: " + str(res))
+
+    def parameter_names(self, *, timeout:Optional[float] = None) -> List[cryptoltypes.CryptolNameInfo]:
+        """Discover the list of module parameter names currently in scope in the current context.
+        The result is a subset of the list returned by `names`."""
+        res = self.connection.parameter_names(timeout=timeout).result()
+        if isinstance(res, list):
+            return [ cryptoltypes.to_cryptol_name_info(entry) for entry in res ]
+        else:
+            raise ValueError("Result of `parameter_names()` is not a list: " + str(res))
+
+    def property_names(self, *, timeout:Optional[float] = None) -> List[cryptoltypes.CryptolNameInfo]:
+        """Discover the list of property names currently in scope in the current context.
+        The result is a subset of the list returned by `names`."""
+        res = self.connection.property_names(timeout=timeout).result()
+        if isinstance(res, list):
+            return [ cryptoltypes.to_cryptol_name_info(entry) for entry in res ]
+        else:
+            raise ValueError("Result of `property_names()` is not a list: " + str(res))
 
-    def focused_module(self, *, timeout:Optional[float] = None) -> Dict[str,Any]:
+    def focused_module(self, *, timeout:Optional[float] = None) -> cryptoltypes.CryptolModuleInfo:
         """Returns the name and other information about the currently-focused module."""
-        res = self.connection.focused_module(timeout=timeout).result()
-        if isinstance(res, dict) and all(isinstance(k, str) for k in res.keys()):
-            return res
-        else:
-            raise ValueError("Panic! Result of `focused_module()` is malformed: " + str(res))
+        return cryptoltypes.to_cryptol_module_info(self.connection.focused_module(timeout=timeout).result())
 
     def reset(self) -> None:
         """Resets the connection, causing its unique state on the server to be freed (if applicable).

cryptol-remote-api/python/tests/cryptol/test-files/Names.cry

@@ -0,0 +1,33 @@
+module Names where
+
+// Examples of names included in `names()` (term names)
+
+parameter
+  key : [64]
+
+enc : [64] -> [64]
+enc x = x ^ key
+
+enc_correct : [64] -> Bit
+property enc_correct x =
+  x == enc (enc x)
+
+primitive prim : [64] -> [64]
+
+(-!) : [64] -> [64] -> [64]
+x -! y = if y > x then 0 else x - y
+
+// Examples of names not included in `names()` (type and module names)
+
+parameter
+  type a : #
+
+type b = a
+
+type constraint fin_b = fin b
+
+primitive type c : *
+
+newtype d = { un_d : c }
+
+submodule M where

cryptol-remote-api/python/tests/cryptol/test_names.py

@@ -0,0 +1,48 @@
+import unittest
+from pathlib import Path
+import unittest
+import cryptol
+from cryptol.single_connection import *
+
+def filter_names(names, *, module, fields_to_exclude):
+    return [ { k:v for k,v in n.items() if k not in fields_to_exclude } for n in names if n["module"] == module ]
+
+class TestNames(unittest.TestCase):
+    def test_names(self):
+        connect(verify=False)
+        load_file(str(Path('tests','cryptol','test-files', 'Names.cry')))
+
+        # names()
+
+        expected_names = [
+            {'module': 'Names', 'name': 'key', 'parameter': () },
+            {'module': 'Names', 'name': 'enc' },
+            {'module': 'Names', 'name': 'enc_correct', 'pragmas': ['property'] },
+            {'module': 'Names', 'name': 'prim' },
+            {'module': 'Names', 'name': '(-!)', 'infix': {'associativity': 'left-associative', 'level': 100} }
+        ]
+
+        names_to_check = filter_names(names(), module="Names", fields_to_exclude=["type", "type string"])
+
+        self.assertCountEqual(expected_names, names_to_check)
+
+        # property_names()
+
+        prop_names = ['enc_correct']
+        expected_props = [ n for n in expected_names if n['name'] in prop_names ]
+
+        props_to_check = filter_names(property_names(), module="Names", fields_to_exclude=["type", "type string"])
+
+        self.assertCountEqual(expected_props, props_to_check)
+
+        # parameter_names()
+
+        param_names = ['key']
+        expected_params = [ n for n in expected_names if n['name'] in param_names ]
+
+        params_to_check = filter_names(parameter_names(), module="Names", fields_to_exclude=["type", "type string"])
+
+        self.assertCountEqual(expected_params, params_to_check)
+
+if __name__ == "__main__":
+    unittest.main()

cryptol-remote-api/src/CryptolServer/Data/Type.hs

@@ -106,7 +106,7 @@ instance JSON.ToJSON JSONType where
           (other, otherArgs) ->
             [ "type" .= T.pack "unknown"
             , "constructor" .= show other
-            , "arguments" .= show otherArgs
+            , "arguments" .= map (JSONType ns) otherArgs
             ]
       convert (TCon (TF tf) args) =
         JSON.object
@@ -204,7 +204,7 @@ instance JSON.ToJSON JSONType where
           (pc', args') ->
             [ "prop" .= T.pack "unknown"
             , "constructor" .= show pc'
-            , "arguments" .= show args'
+            , "arguments" .= map (JSONType ns) args'
             ]
       convert (TVar v) =
         JSON.object