add types to names(), etc. in Python, convert argument types to JSON in API

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

@@ -11,7 +11,7 @@ from .opaque import OpaqueValue
 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,21 +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]]:
+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 parameter_names(*, timeout:Optional[float] = None) -> List[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[Dict[str,Any]]:
+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) -> Dict[str,Any]:
+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,39 +347,35 @@ class CryptolSyncConnection:
         else:
             raise ValueError("Unknown solver type: " + str(solver))
 
-    def names(self, *, timeout:Optional[float] = None) -> List[Dict[str,Any]]:
+    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[Dict[str,Any]]:
+    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) 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 `parameter_names()` is malformed: " + str(res))
+            raise ValueError("Result of `parameter_names()` is not a list: " + str(res))
 
-    def property_names(self, *, timeout:Optional[float] = None) -> List[Dict[str,Any]]:
+    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) 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 `property_names()` is malformed: " + str(res))
+            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_names.py

@@ -15,7 +15,7 @@ class TestNames(unittest.TestCase):
         # names()
 
         expected_names = [
-            {'module': 'Names', 'name': 'key', 'parameter': [] },
+            {'module': 'Names', 'name': 'key', 'parameter': () },
             {'module': 'Names', 'name': 'enc' },
             {'module': 'Names', 'name': 'enc_correct', 'pragmas': ['property'] },
             {'module': 'Names', 'name': 'prim' },

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