detect "import submodule" and give proper errors#3215
detect "import submodule" and give proper errors#3215
Conversation
- update all callers - argument currently unused
- giving proper errors
RyanGlScott
left a comment
RyanGlScott
left a comment
There was a problem hiding this comment.
It would be worth adding a test case to check that SAW is actually detecting import submodule as expected.
| let import' = mkImport vis (locatedUnknown (T.mName mod')) as imps | ||
| return $ env' {eImports = import' : eImports env } | ||
| importCryptolModule _sc _env (Right __nm) _as True _vis _imps = | ||
| -- importing submodule by name: |
| -- - `importCryptolModule`, which is the back end for SAWScript @import@ | ||
| -- - `importCryptolModule`, which is the back end for SAWScript @import@ | ||
| -- - `loadExtCryptolModule`, which is the back end for SAWScript @cryptol_load@ | ||
| -- - `loadCryptolModule`, which is used for Rocq export and from crux-mir-comp | ||
| -- - `loadCryptolModule`, which is used for Rocq export and from crux-mir-comp |
There was a problem hiding this comment.
The whitespace changes here appear unnecessary. I think there should only be a single space after each comma.
| import CryptolSAWCore.TypedTerm | ||
|
|
||
| import SAWCore.Name (nameInfo) | ||
| import SAWCore.Recognizer (asConstant) | ||
| import SAWCore.SharedTerm (NameInfo, SharedContext, Term, ppTerm) | ||
|
|
||
| import SAWSupport.Console | ||
| import qualified SAWSupport.Pretty as PPS | ||
|
|
||
| import qualified CryptolSAWCore.Cryptol as C | ||
| import CryptolSAWCore.Cryptol (ImportVisibility(..), CryptolEnv(..)) | ||
| -- These used to live in this file, so import them unqualified for now. | ||
| -- XXX: tidy up | ||
|
|
There was a problem hiding this comment.
If you're going to fix up the import list, can you put them in structural order? (SAWSupport first, then SAWCore, then CryptolSAWCore)
There was a problem hiding this comment.
Also, SAWSupport.Pretty is more fundamental than SAWSupport.Console so should really come before it.
| importCryptolModule _sc _env (Left _) _as True _vis _imps = | ||
| -- importing submodule by FilePath: disallowed: | ||
| fail $ "`import submodule PATHNAME` is not allowed." | ||
| -- this allowed by parser? |
There was a problem hiding this comment.
It is allowed by the parser. That could be changed, but TBH I think it's probably better to reject it explicitly than to generate "Parse error". We could, though, reject it in the SAWScript typechecker instead of here.
3 participants
Plumb parsing data to the
importCryptolModuleso as to give proper error messages.(Does not support the
import submodule SUBMODULENAMEyet)