Make names in scope in functors accessible when their instantiations are loaded at the REPL #1559
Conversation
qsctr
added
parameterized modules
|
Thank you! Say, does this capability port over to SAW? That is, when a Cryptol module is loaded in SAW, will the scope be the same as when a module is loaded into Cryptol, or does this work need to be ported to SAW as well? |
|
For the most part, this change only fixes the behavior of what is in scope in the Cryptol REPL, so it does not affect SAW. However I don't think we need a fix for SAW since SAW does not follow Cryptol's normal module system scoping rules and everything would already be accessible in a SAW The one exception is instantiated type parameters: currently these are not available when an instantiation is imported in SAW since they are treated slightly differently internally in Cryptol. This PR should fix that. |
|
Reviewed in person by @yav |
This is primarily motivated by a need to bring in a fix for GaloisInc/crucible#1105 into SAW soon. In order to do this, I will need to bump the `crucible` submodule to a more recent commit, so this patch lays the groundwork for doing so. Most of the changes can be brought in directly without any further changes to SAW. One exception in `cryptol`, where I had to explicitly initialize `mInScope` to accommodate the changes from GaloisInc/cryptol#1559. Just like how `cryptol` initializes `mInScope` to `mempty` after parsing a Cryptol `NormalModule`, so too does SAW.
Fixes #1455, making anything in scope of the functor in scope at the REPL as well when an instantiation of the functor is loaded and focused. In particular, the prelude will be in scope. As part of handling functor parameters correctly, this also fixes #1556, fixes #1237, fixes #1561, and fixes #1562.
In addition, this does some work towards implementing #1382, by storing the in-scope information for nested modules into
Cryptol.ModuleSystem.Interface.IFaceNames.