search

ocaml-gospel / gospel

A tool-agnostic formal specification language for OCaml.
https://ocaml-gospel.github.io/gospel
MIT License
128 stars 16 forks source link

Revise Identifier implementation #381

Closed n-osborne closed 5 months ago

n-osborne commented 9 months ago

If we decide to move forward with #377, unicity of Identifier is expected to be broken across modules. Indeed, the tag in Identifier.Ident.create and Identifier.Ident.of_preid will be reset at every run of the type-checker.

The change should obvioulsy need to preserve equality and comparison in addition to guarantee unicity of identifiers. But I don't think we should be too much concerned about preserving the interface as it is now. For example, I believe one elegant solution would be to resolve identifier with absolute path (I believe it is how it is done in the OCaml compiler). That would implies the two functions above to take a path as extra argument.

n-osborne commented 8 months ago

Apparently, Identifier.t containing only the name and not the path is a problem for translation to Why3 and Coq.

n-osborne commented 5 months ago

Closing as it is superseded and specialised by #411 Also, #389 add fully resolved path