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
+## 2.13.2 -- 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,36 @@ Return fields
 
 
 
+``module``
+  A human-readable representation of the module from which the name originates
+
+
+
+``parameter``
+  An optional field which is present and ``True`` iff the name is a module parameter
+
+
+
+``infix``
+  An optional field which is present and ``True`` iff the name is an infix operator
+
+
+
+``infix associativity``
+  An optional field containing one of the strings ``left-associative``, ``right-associative``, or ``non-associative`` if the name is an infix operator
+
+
+
+``infix level``
+  An optional field containing the name's precedence level, if the name is an infix operator
+
+
+
+``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
 
+## 2.13.2 -- 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/single_connection.py

@@ -219,9 +219,19 @@ 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."""
+    """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]]:
+    """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]]:
+    """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]:
     """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

@@ -348,13 +348,31 @@ def safe(self, expr : Any, solver : Solver = Z3, *, timeout:Optional[float] = No
             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."""
+        """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
         else:
             raise ValueError("Panic! Result of `names()` is malformed: " + str(res))
 
+    def parameter_names(self, *, timeout:Optional[float] = None) -> List[Dict[str,Any]]:
+        """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
+        else:
+            raise ValueError("Panic! Result of `parameter_names()` is malformed: " + str(res))
+
+    def property_names(self, *, timeout:Optional[float] = None) -> List[Dict[str,Any]]:
+        """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
+        else:
+            raise ValueError("Panic! Result of `property_names()` is malformed: " + str(res))
+
     def focused_module(self, *, timeout:Optional[float] = None) -> Dict[str,Any]:
         """Returns the name and other information about the currently-focused module."""
         res = self.connection.focused_module(timeout=timeout).result()

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': True },
+            {'module': 'Names', 'name': 'enc' },
+            {'module': 'Names', 'name': 'enc_correct', 'pragmas': ['property'] },
+            {'module': 'Names', 'name': 'prim' },
+            {'module': 'Names', 'name': '(-!)', 'infix': True, 'infix associativity': 'left-associative', 'infix 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/Names.hs

@@ -1,6 +1,7 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE RecordWildCards #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE TypeApplications #-}
@@ -16,14 +17,18 @@ import qualified Data.Map as Map
 import Data.Map (Map)
 import Data.Text (unpack)
 import Data.Typeable (Proxy(..), typeRep)
+import Data.Maybe (fromMaybe, mapMaybe, isJust)
 
 import Cryptol.Parser.Name (PName(..))
+import Cryptol.Parser.AST (Pragma)
 import Cryptol.ModuleSystem.Env (ModContext(..), ModuleEnv(..), DynamicEnv(..), focusedEnv)
-import Cryptol.ModuleSystem.Interface (IfaceDecl(..), IfaceDecls(..))
+import Cryptol.ModuleSystem.Interface (IfaceParams(..), IfaceDecl(..), IfaceDecls(..))
 import Cryptol.ModuleSystem.Name (Name)
+import qualified Cryptol.ModuleSystem.Name as N (nameInfo, NameInfo(Declared))
 import Cryptol.ModuleSystem.NamingEnv
                   (NamingEnv, namespaceMap, lookupValNames, shadowing)
-import Cryptol.TypeCheck.Type (Schema(..))
+import Cryptol.TypeCheck.Type (Schema(..), ModVParam(..))
+import Cryptol.Utils.Fixity(Fixity(..), defaultFixity)
 import Cryptol.Utils.PP (pp)
 import Cryptol.Utils.Ident(Namespace(..))
 
@@ -47,46 +52,80 @@ instance Doc.DescribedMethod VisibleNamesParams [NameInfo] where
       Doc.Paragraph [ Doc.Text " A"
                     , Doc.Link (Doc.TypeDesc (typeRep (Proxy @JSONSchema))) "JSON Cryptol type"
                     ])
+    , ("module",
+      Doc.Paragraph [Doc.Text "A human-readable representation of the module from which the name originates"])
+    , ("parameter",
+      Doc.Paragraph [ Doc.Text "An optional field which is present and ",
+                      Doc.Literal "True", Doc.Text " iff the name is a module parameter" ])
+    , ("infix",
+      Doc.Paragraph [ Doc.Text "An optional field which is present and ",
+                      Doc.Literal "True", Doc.Text " iff the name is an infix operator" ])
+    , ("infix associativity",
+      Doc.Paragraph [ Doc.Text "An optional field containing one of the strings ",
+                      Doc.Literal "left-associative", Doc.Text ", ",
+                      Doc.Literal "right-associative", Doc.Text ", or ",
+                      Doc.Literal "non-associative", Doc.Text " if the name is an infix operator" ])
+    , ("infix level",
+      Doc.Paragraph [ Doc.Text "An optional field containing the name's precedence level, ",
+                      Doc.Text "if the name is an infix operator" ])
+    , ("pragmas",
+      Doc.Paragraph [ Doc.Text "An optional field containing a list of the name's pragmas (e.g. ",
+                      Doc.Literal "property", Doc.Text "), if it has any"])
     , ("documentation",
       Doc.Paragraph [Doc.Text "An optional field containing documentation string for the name, if it is documented"])
     ]
 
 visibleNamesDescr :: Doc.Block
 visibleNamesDescr =
-  Doc.Paragraph [Doc.Text "List the currently visible (i.e., in scope) names."]
+  Doc.Paragraph [Doc.Text "List the currently visible (i.e., in scope) term names."]
 
 visibleNames :: VisibleNamesParams -> CryptolCommand [NameInfo]
 visibleNames _ =
   do me <- getModuleEnv
      let DEnv { deNames = dyNames } = meDynEnv me
-     let ModContext { mctxDecls = fDecls, mctxNames = fNames} = focusedEnv me
+     let ModContext { mctxParams = fparams, mctxDecls = fDecls, mctxNames = fNames} = focusedEnv me
      let inScope = Map.keys (namespaceMap NSValue $ dyNames `shadowing` fNames)
-     return $ concatMap (getInfo fNames (ifDecls fDecls)) inScope
+     return $ concatMap (getInfo fNames (ifParamFuns fparams) (ifDecls fDecls)) inScope
 
-getInfo :: NamingEnv -> Map Name IfaceDecl -> PName -> [NameInfo]
-getInfo rnEnv info n' =
-  [ case Map.lookup n info of
-       Nothing -> error $ "Name not found, but should have been: " ++ show n
-       Just i ->
-         let ty = ifDeclSig i
-             nameDocs = ifDeclDoc i
-         in NameInfo (show (pp n')) (show (pp ty)) ty (unpack <$> nameDocs)
-  | n <- lookupValNames n' rnEnv
-  ]
+getInfo :: NamingEnv -> Map Name ModVParam -> Map Name IfaceDecl -> PName -> [NameInfo]
+getInfo rnEnv params decls n' =
+  flip mapMaybe (lookupValNames n' rnEnv) $ \n ->
+    case (N.nameInfo n, Map.lookup n params, Map.lookup n decls) of
+      (N.Declared m _, Just (ModVParam _ ty nameDocs fx), _) ->
+        Just $ mkNameInfo True ty m (isJust fx) fx ([]::[Pragma]) nameDocs
+      (N.Declared m _, _, Just (IfaceDecl _ ty prags ifx fx nameDocs)) ->
+        Just $ mkNameInfo False ty m ifx fx prags nameDocs
+      _ -> Nothing
+  where mkNameInfo param ty m ifx fx prags nameDocs = 
+          let fxy = if not ifx then Nothing else case fromMaybe defaultFixity fx of
+                      Fixity assoc lvl -> Just (show (pp assoc), lvl)
+           in NameInfo (show (pp n')) (show (pp ty)) ty (show (pp m)) param
+                       fxy (show . pp <$> prags) (unpack <$> nameDocs)
 
 data NameInfo =
   NameInfo
   { name     :: String
   , typeSig  :: String
   , schema   :: Schema
+  , modl     :: String
+  , isParam  :: Bool
+  , fixity   :: Maybe (String, Int)
+  , pragmas  :: [String]
   , nameDocs :: Maybe String
   }
 
 instance JSON.ToJSON NameInfo where
-  toJSON (NameInfo{name, typeSig, schema, nameDocs}) =
+  toJSON (NameInfo{..}) =
     JSON.object $
     [ "name" .= name
     , "type string" .= typeSig
-    , "type" .= JSON.toJSON (JSONSchema schema)
+    , "type" .= JSONSchema schema
+    , "module" .= modl
     ] ++
+    (if isParam then ["parameter" .= isParam] else []) ++
+    maybe [] (\(assoc, lvl) ->
+              [ "infix" .= True
+              , "infix associativity" .= assoc
+              , "infix level" .= lvl ]) fixity ++
+    (if null pragmas then [] else ["pragmas" .= pragmas]) ++
     maybe [] (\d -> ["documentation" .= d]) nameDocs