You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
As touched upon in #1492, currently the remote API does not provide as much information about names as the browse command does in the REPL. This PR expands the result of the visible names method (i.e. names() in the Python API) to include:
all the additional information provided by the browse command (i.e. what module the name is from, whether or not it is a parameter, and whether or it not it is a property), as well as
fixity information (i.e. whether or not the name is an infix operator, and if so its associativity and precedence level).
This PR also adds the property_names and parameter_names functions to the Python API, which return only those names which are properties or parameters, respectively.
Finally, this PR also fixes a bug where names() would sometimes hang when a parameterized module is loaded.
See test_names.py for an example of this new output of names as well as the new the property_names and parameter_names functions.
Looking ahead: At some point it might also be nice to have type_names and module_names commands which return similar results to names, just for these other two distinct namespaces in Cryptol. It might also be nice to have an easy way to prove a property retrieved from property_names.
This PR should be ready now. This last commit gives types to the output of names, property_names, parameter_names, and focused_module in the Python API as additional documentation for what sort of values these functions return (see the newly added CryptolNameInfo and CryptolModuleInfo in cryptoltypes.py).
Note that in making that change, I converted the type fields of the output of names() to CryptolSchemas for the first time, and found a bug where for unknown constructors, the arguments field wasn't getting converted to JSON.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
As touched upon in #1492, currently the remote API does not provide as much information about names as the
browsecommand does in the REPL. This PR expands the result of thevisible namesmethod (i.e.names()in the Python API) to include:browsecommand (i.e. what module the name is from, whether or not it is a parameter, and whether or it not it is a property), as well asThis PR also adds the
property_namesandparameter_namesfunctions to the Python API, which return only those names which are properties or parameters, respectively.Finally, this PR also fixes a bug where
names()would sometimes hang when a parameterized module is loaded.See
test_names.pyfor an example of this new output ofnamesas well as the new theproperty_namesandparameter_namesfunctions.Looking ahead: At some point it might also be nice to have
type_namesandmodule_namescommands which return similar results tonames, just for these other two distinct namespaces in Cryptol. It might also be nice to have an easy way to prove a property retrieved fromproperty_names.