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

Make identifiers include the relative path. #411

Open n-osborne opened 5 months ago

n-osborne commented 5 months ago

While working on adding a pretty printer to Gospel, I've stumbled on the fact that I can either print the fully resolved path or just the name of the symbol (Lident in OCaml).

A correct pretty printer should print the symbols the way it is written in the source code in the first place (the relative path).

Also, printing the latter leads to incorrect Gospel code for the symbols defined in another module that is not yet open, while printing the former leads to incorrect Gospel code for symbols defined in the current module (as the fully resolved path contains the name of the said module).

I suggest that identifiers carry, along the newly added fully resolved path, the relative path.

One could also be so bold as to reuse the Longident.t type from the OCaml parsetree!