Structured names

[robdockins]

I'm working on being able to selectively decide what functions to evaluate when setting up symbolic simulator states for SAW. One of the strategies I'm considering is to unfold all the functions from specified modules, and not others. More generally, it would be nice for users to have some control over what symbols in scope get unfolded, etc.

Right now, the Constant and ExtCns types only contain a String for the name and a VarIndex, which is a unique nonce for memo table purposes. Neither is really the right information for what I want to do, which has to do with tying symbols back to source locations and modules. Does saw-core have some notion of resolved name we can use for this? Do we need to build one?

[brianhuffman]

No, it doesn't, but we really need one. We should define a reasonable Name type and use it consistently across Constant, ExtCns, and GlobalVar terms. (Currently GlobalVars use type Ident, which is basically just a qualified identifier, and doesn't even have a unique int.)

[andreistefanescu]

This is badly needed. I've looked at x = x that wasn't trivially true because the two xs had the same String for the name but different VarIndexs.

[brianhuffman]

Along with introducing a proper Name type, we will also need to introduce something like the NamingEnv that cryptol has, which represents the mapping between Names and the strings that users provide. We'll use the NamingEnv to do renaming during parsing, and also when pretty-printing, so we can ensure that all printed names can be parsed back appropriately. Having a NamingEnv will make it easier to solve #17.

[robdockins]

Do you think the Cryptol naming and enviromnment APIs could be reused as-is or with minor modifications?

[brianhuffman]

My current thinking is that we should reuse Cryptol types like Ident, Name, and NamingEnv as much as possible. When we translate from Cryptol to saw-core, we can reuse the same exact Name for each translated constant.

I am increasingly noticing that SAW users are confused by any inconsistencies between Cryptol and saw-core. We should make it an explicit goal to make the two languages share as much as possible. The relationship between Cryptol and saw-core should be just like the relationship between Haskell and GHC-Core.

[brianhuffman]

As a first easy step, I propose that we replace the ModuleName and Ident types defined in Verifier.SAW.Term.Functor with the similarly-named types from Cryptol.

[robdockins]

Implemented via #87