-
Notifications
You must be signed in to change notification settings - Fork 85
Add :cbrowse to print imported Cryptol modules #2680
Copy link
Copy link
Open
Labels
missing cryptol featuresIssues about features in Cryptol that don't work in SAWIssues about features in Cryptol that don't work in SAWneeds testIssues for which we should add a regression testIssues for which we should add a regression testsubsystem: cryptol-saw-coreIssues related to Cryptol -> saw-core translation with cryptol-saw-coreIssues related to Cryptol -> saw-core translation with cryptol-saw-coresubsystem: saw-scriptIssues related to the SAWScript language and/or its interpretation and executionIssues related to the SAWScript language and/or its interpretation and executiontype: feature requestIssues requesting a new feature or capabilityIssues requesting a new feature or capabilityusabilityAn issue that impedes efficient understanding and useAn issue that impedes efficient understanding and use
Milestone
Description
Activity
Metadata
Metadata
Assignees
Labels
missing cryptol featuresIssues about features in Cryptol that don't work in SAWIssues about features in Cryptol that don't work in SAWneeds testIssues for which we should add a regression testIssues for which we should add a regression testsubsystem: cryptol-saw-coreIssues related to Cryptol -> saw-core translation with cryptol-saw-coreIssues related to Cryptol -> saw-core translation with cryptol-saw-coresubsystem: saw-scriptIssues related to the SAWScript language and/or its interpretation and executionIssues related to the SAWScript language and/or its interpretation and executiontype: feature requestIssues requesting a new feature or capabilityIssues requesting a new feature or capabilityusabilityAn issue that impedes efficient understanding and useAn issue that impedes efficient understanding and use
In the Cryptol repl you can do
:browseto print the contents of a module. We ought to be able to do that from the SAWScript repo.Currently if you use
cryptol_loadthat gives you aCryptolModulethat can beprinted, but there's no way to do that with animportand we'd rather people used theimportsyntax. (And we're planning to deprecatecryptol_loadandCryptolModuleeventually.) Also, we can likely reuse the Cryptol:browsecode for a:cbrowserepl command.An alternative would be to keep
CryptolModuleand its print code and haveimportbindCryptolModules; there are some complications with that, though, for selective or partial imports. Also it's messier from a name handling perspective. Unless there's some reason to want to be able to print module contents from inside SAWScript code (vs. a:-command) I think:cbrowseis a better solution.