diff --git a/cryptol-remote-api/CHANGELOG.md b/cryptol-remote-api/CHANGELOG.md index 61d485f76..fba61c480 100644 --- a/cryptol-remote-api/CHANGELOG.md +++ b/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 diff --git a/cryptol-remote-api/docs/Cryptol.rst b/cryptol-remote-api/docs/Cryptol.rst index 54a4c6160..f5617da2a 100644 --- a/cryptol-remote-api/docs/Cryptol.rst +++ b/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 diff --git a/cryptol-remote-api/python/CHANGELOG.md b/cryptol-remote-api/python/CHANGELOG.md index 86ee3b302..08f0f58d0 100644 --- a/cryptol-remote-api/python/CHANGELOG.md +++ b/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 diff --git a/cryptol-remote-api/python/cryptol/commands.py b/cryptol-remote-api/python/cryptol/commands.py index 2a49640df..de53f8df3 100644 --- a/cryptol-remote-api/python/cryptol/commands.py +++ b/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: diff --git a/cryptol-remote-api/python/cryptol/connection.py b/cryptol-remote-api/python/cryptol/connection.py index 51d565e48..2a6ac9ca7 100644 --- a/cryptol-remote-api/python/cryptol/connection.py +++ b/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. diff --git a/cryptol-remote-api/python/cryptol/cryptoltypes.py b/cryptol-remote-api/python/cryptol/cryptoltypes.py index 0d9aef611..84c0b86fd 100644 --- a/cryptol-remote-api/python/cryptol/cryptoltypes.py +++ b/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)) + diff --git a/cryptol-remote-api/python/cryptol/single_connection.py b/cryptol-remote-api/python/cryptol/single_connection.py index c498463b3..23f9cd311 100644 --- a/cryptol-remote-api/python/cryptol/single_connection.py +++ b/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) diff --git a/cryptol-remote-api/python/cryptol/synchronous.py b/cryptol-remote-api/python/cryptol/synchronous.py index f9b54d456..9d98063a4 100644 --- a/cryptol-remote-api/python/cryptol/synchronous.py +++ b/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). diff --git a/cryptol-remote-api/python/tests/cryptol/test-files/Names.cry b/cryptol-remote-api/python/tests/cryptol/test-files/Names.cry new file mode 100644 index 000000000..17c9f249c --- /dev/null +++ b/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 diff --git a/cryptol-remote-api/python/tests/cryptol/test_names.py b/cryptol-remote-api/python/tests/cryptol/test_names.py new file mode 100644 index 000000000..d339317eb --- /dev/null +++ b/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() diff --git a/cryptol-remote-api/src/CryptolServer/Data/Type.hs b/cryptol-remote-api/src/CryptolServer/Data/Type.hs index f830c2da6..1cbb9f355 100644 --- a/cryptol-remote-api/src/CryptolServer/Data/Type.hs +++ b/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 diff --git a/cryptol-remote-api/src/CryptolServer/Names.hs b/cryptol-remote-api/src/CryptolServer/Names.hs index 12b73e89c..70404befb 100644 --- a/cryptol-remote-api/src/CryptolServer/Names.hs +++ b/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,76 @@ 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 iff the name is a module parameter" ]) + , ("infix", + Doc.Paragraph [ Doc.Text "An optional field which is present iff the name is an infix operator. ", + Doc.Text "If present, it contains an object with two fields. One field is ", + Doc.Literal "associativity", Doc.Text ", containing one of the strings ", + Doc.Literal "left-associative", Doc.Text ", ", + Doc.Literal "right-associative", Doc.Text ", or ", + Doc.Literal "non-associative", Doc.Text ", and the other is ", + Doc.Literal "level", Doc.Text ", containing the name's precedence level." ]) + , ("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" .= ()] else []) ++ + maybe [] (\(assoc, lvl) -> + ["infix" .= JSON.object + [ "associativity" .= assoc + , "level" .= lvl ]]) fixity ++ + (if null pragmas then [] else ["pragmas" .= pragmas]) ++ maybe [] (\d -> ["documentation" .= d]) nameDocs