saw-core parsing commands only recognize identifiers from Prelude.sawcore

[brianhuffman]

The commands core_thm, core_axiom, and parse_core are supposed to parse saw-core expressions from strings. However, they raise errors if the expressions mention anything defined in Cryptol.sawcore, or any other loaded saw-core module except for the prelude.

sawscript> parse_core "ecToInteger (TCNum 8) (bvNat 8 0)"

user error ("parse_core" (<stdin>:1:1-1:11):
.:1:13:
Unbound name: TCNum
)

[brianhuffman]

We should be able to fix this by changing the saw-core parser/typechecker to use the new SAWNamingEnv introduced by GaloisInc/saw-core#87. GaloisInc/saw-core#118 is a step in the right direction, as it registers all top-level constants from .sawcore files in the naming environment.