alt-ergo
alt-ergo copied to clipboard
Use constant terms as identifiers in names and variables
This PR changes the way we construct identifiers for names (in Symbols) and variables (in Var).
We plan to completely replace the AE identifiers with identifiers from Dolmen. This PR serves as an intermediate step from string-based identifiers to Dolmen identifiers.
- All the identifiers are now managed in the
Idmodule. - Constant terms are used for declared or defined identifiers in the input file.
- Internal identifiers are still pre-mangled strings. Replacing them with Dolmen identifiers requires careful investigation, particularly in the AC(X) implementation.
- I haven't removed
Id.typedyet. After this PR, the user identifiers will be typed, so we do not need to store them separately. If we use the internal type of the identifier, we will need to implement a conversion function from Dolmen type to Alt-Ergo type, which is not trivial. I prefer keeping this type and remove it after transitioning from Alt-Ergo types to Dolmen types. - The new API of
Idprevents us from creating duplicate fresh/fresh_ac/abstract identifiers. - I still check that user identifiers do not start with
.or@. In Before this PR, we mangled the identifier if it happened. In this PR, we crash. I don't have a strong opinion on this behavior, it was just simpler to implement this way. - I use identifiers for term variables too. I preserved the internal representation because:
- the notion of local variables is AE-specific, whereas the local name in Dolmen identifiers is a distinct concept.
- After this PR, variables are typed but what is the type of
Underscore? May beforall a. a?
This PR have been tested on ae-format (+2-2).