alt-ergo icon indicating copy to clipboard operation
alt-ergo copied to clipboard

Use constant terms as identifiers in names and variables

Open Halbaroth opened this issue 10 months ago • 1 comments

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 Id module.
  • 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.typed yet. 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 Id prevents 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:
    1. the notion of local variables is AE-specific, whereas the local name in Dolmen identifiers is a distinct concept.
    2. After this PR, variables are typed but what is the type of Underscore? May be forall a. a?

This PR have been tested on ae-format (+2-2).

Halbaroth avatar Jan 30 '25 15:01 Halbaroth