search

OCamlPro / alt-ergo

OCamlPro public development repository for Alt-Ergo
https://alt-ergo.ocamlpro.com/
Other
130 stars 33 forks source link

Unique identifiers #1097

Closed Halbaroth closed 4 months ago

Halbaroth commented 4 months ago

The current module Id uses Hstring to compare identifiers. This PR uses a hidden tag in the type t of Id to compare identifiers. This tag is unique by construction and the Hstring field is only used for printing.

In particular, calling twice Sy.name with the same input will produce two differents symbols. The full id (that is with the unique tag stored in it) can be print with Id.pp ~full:true.

This PR has to be tested a lot because we have to be sure we never store a symbol in a string in order to recreate it later for instance.

Halbaroth commented 4 months ago

It seems this modification is too complicated until we get rid of the legacy parser.