Allow importing Cryptol submodules into SAW

[qsctr]

Problem Statement

It seems like SAW currently does not support importing things defined in Cryptol submodules, either through import or cryptol_load. For instance, for a module like

module Test where
submodule M where
  x = 1

we get

sawscript> import "Test.cry"
sawscript> {{ M::x }}

Stack trace:
Cryptol error:
[error] at <stdin>:1:4--1:8
    Value not in scope: M::x

sawscript> Test <- cryptol_load "Test.cry"
sawscript> Test
[22:33:47.218] Symbols
=======

Actually, SAW does import them internally, but they are not accessible. The Cryptol NamingEnv constructed from the imported and cryptol_loaded modules does not include any non-top-level symbols; the name of the submodule itself is there but nothing under it is exposed. This is because ifsDefines which is used when constructing the NamingEnv does not include nested definitions:

saw-script/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs

Lines 273 to 280 in 35396bc

	loadImport (vis, i) = do
	lm <- ME.lookupModule (T.iModule i) (eModuleEnv env)
	let ifc = MI.ifNames (ME.lmInterface lm)
	syms = MN.namingEnvFromNames $
	case vis of
	OnlyPublic -> MI.ifsPublic ifc
	PublicAndPrivate -> MI.ifsDefines ifc
	return $ MN.interpImportEnv i syms

And the CryptolModule object returned by cryptol_load also does not pick up any nested symbols, so they are not able to be cryptol_extracted. This is because the CryptolModule only exposes exported terms:

saw-script/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs

Lines 426 to 432 in 35396bc

	let names = MEx.exported C.NSValue (T.mExports m) -- :: Set T.Name
	let tm' = Map.filterWithKey (\k _ -> Set.member k names) $
	Map.intersectionWith
	(\t x -> TypedTerm (TypedTermSchema t) x)
	types
	newTermEnv

This feature is requested by @WeeknightMVP.

Analysis, Commentary

• This all works in Cryptol compilation and the CLI, but not in sawscript.
• The code for "loading/importing" and then determining what's in scope for a given expression is scattered about in
  cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs
  • the code is duplicating (hard to reuse) code in deps/cryptol/src/Cryptol/ModuleSystem/*.hs
  • in this module internally there is a bit of highly duplicated code.
• The code for the submodules and naming is a bit subtle.

Progress

• found kludgy workaround: use cryptol code that works (that depends on single "focused module") and explicitly set focused module. At least we have localized the problem and found some code that works.
• support submodules when we import multiple sawscript modules
  • when the same symbol is in multiple imported modules, we silently shadow earlier ones, fix this to give error on ambiguous references to maintain the current user interface.
  • this part is finished, see llvm_load_module should support search paths #256
• fix the explicit module load code (implementing cryptol_load, which binds the module to a SAWScript variable) to support submodules
  • (The code here is 80% the same as the import code, will try to capture commonalities as we fix this).
  • have design that will implement this primarily in terms of the now working import command
  • For related discussion on the improvement of the user-facing API, see also Cleanup and Consolidate SAWScript import and load_cryptol (UI and implementation) #2569
  • re-implement the cryptol_load command as just noted: see support submodules in cryptol_load #2593