Structured names #87
Structured names #87
Conversation
|
I don't think we need this |
|
I think the one concern I have with just using Cryptol's names is that we also have names imported from other languages, like LLVM and JVM to concern ourselves with. Do we just wan to shoehorn everything in to the Cryptol namespace by inventing special modules for those identifiers to live in? |
|
We really don't do much importing of LLVM/JVM names into saw-core, except if we're doing a function extraction. So yeah, I'd be fine with shoehorning everything into the Cryptol namespace. We could even just have the user provide a name to use for each extracted function, so we don't even have to reserve any particular part of the namespace in advance. One advantage of using the Cryptol namespace for module names is that users already know the syntax for it; having to refer to the same name two different ways in two contexts would be confusing. |
robdockins
force-pushed
the
structured-names
branch
from
ba43a24
to
8f78fee
Compare
|
I think the main ideas here are now in place, per our last conversation. There are still a few details to work out, but it seems like this method allows us to install structured names and still be backward compatible in SAW with our test suite of proofs, so I think that's a really strong start. |
robdockins
force-pushed
the
structured-names
branch
from
8f78fee
to
2867106
Compare
robdockins
force-pushed
the
structured-names
branch
from
bc7d067
to
b4ecaa6
Compare
|
@brianhuffman, I think this is just about ready to merge. I'd love your thoughts. |
`NameInfo` datatype that is attached to `ExtCns` (and thus `Constant`) nodes. In addition, we implement a more organized naming environment, and a notion of abolute names, which are intended to be a unique "name of last resort". Each name that doesn't derive from a SAWCore module is required to have a unique URI. Dynamically-created values incorporate the unique VarIndex into their name, whereas concepts from, e.g., Cryptol modules have URIs that are derived from their fully-qualified name. In addition to the absolute name, imported names may have a collection of aliases, which are the more typical way to refer to the name. All the aliases for a name are put into a naming environment, which map strings arising from user input, etc, into a set of names they might refer to. When the set contains more than one "true" name, the identifier is ambiguous, and we can report all the names to which that identifier might refer, as well as unambiguous alternate identifiers for each name.
in the external format. This allows us to retain the full information present in the `NameInfo` structure without complicating the main term parsing code.
for resolving identifiers using the Cryptol naming environment. Also, improve some error messages.
held uninterpreted as a `Set VarIndex` instead of a `[String]`. This shifts the burden of resolving user-provided names closer to the front-end.
robdockins
force-pushed
the
structured-names
branch
from
4282ce3
to
dc36a11
Compare
from SAWCore (CF GaloisInc/saw-core#87). Add logic for first attempting to resolve user-supplied names using the Cryptol interactive scope, then fall back on the SAWCore naming environment.
from SAWCore (CF GaloisInc/saw-core#87). Add logic for first attempting to resolve user-supplied names using the Cryptol interactive scope, then fall back on the SAWCore naming environment.
from SAWCore (CF GaloisInc/saw-core#87). Add logic for first attempting to resolve user-supplied names using the Cryptol interactive scope, then fall back on the SAWCore naming environment.
from SAWCore (CF GaloisInc/saw-core#87). Add logic for first attempting to resolve user-supplied names using the Cryptol interactive scope, then fall back on the SAWCore naming environment.
from SAWCore (CF GaloisInc/saw-core#87). Add logic for first attempting to resolve user-supplied names using the Cryptol interactive scope, then fall back on the SAWCore naming environment.
Some early work on adding structured names to SAWCore. For now, this is really only addressing naming concerns for
ExtCnsandConstantterms, but there are already quite a lot of design issues to untangle.