Adding paths to Gospel identifiers

[mrjazzybread]

Hello again :)

As I said previously, I was trying to change the commit history so that the previous commits were well formatted, but I guess something broke. All the previous commits are now well formatted. I also merged the commits that added tests and identifiers into one. I also added a field to module records with the name of the module (not just the path of the file) for convinience's sake.

[n-osborne]

Thanks!

Don't worry about closing the previous PR :-)

This is begining to look great.

In the following example, the call to f in g's specification doesn't have a path.

$ cat > bob.mli << EOF
> module M : sig
>   (*@ function f (i : integer) : bool *)
> end
> 
> open M
> 
> val g : int -> bool
> (*@ b = g i
>     ensures b = f i *)
> EOF
$ gospel dumpast bob.mli | grep "_name.*"
       { Tast.md_name = Bob.M;
                      { Symbols.ls_name = Bob.M.f;
                      [{ Symbols.vs_name = i;
       { Tast.vd_name = Bob.g; vd_type = int -> bool; vd_prim = [];
             { Symbols.vs_name = i_1;
             { Symbols.vs_name = b;
                     { Symbols.vs_name = i_1;
                     { Symbols.vs_name = b;
                       { Symbols.ls_name = infix =;
                            (Ttypes.Tyvar { Ttypes.tv_name = a_1 }) };
                             (Ttypes.Tyvar { Ttypes.tv_name = a_1 }) }
                             { Symbols.vs_name = b;
                              { Symbols.ls_name = f;
                                    { Symbols.ls_name =
                                          { Symbols.vs_name = i_1;

I would have expected it to have one. This would allow to know, from the identifier in a term, where it has been defined. I believe this could lead to a better managment of identifiers in the different translations (why3, cfml, ortac...), and this will be needed for a better integration of gospel in odoc (we don't want to ask odoc to resolve our paths). Do we have reasons not to add it?

On a more general note, we tend to use sentences beginning with an infinitive verb for commit messages and changelog entries. Also I'm not sure we completely understand the message for the second commit without reading the code.

And finally, this PR completely breaks Ortac/QCheckSTM tests (I've not investigated why yet). Hence, I'll postpone merging to after the release of gospel 0.3 (and try to hurry up on that) so that I can release Ortac too. We can break everything afterward.

[mrjazzybread]

Hello

Regarding f's path, I noticed that a few days ago and it was really confusing me why it didn't have a path. I eventually figured out it was a bug in the pretty printer for identifiers :(( I fixed it as well as making the output for the tests less dependent on the specific indentation of the dumpast command.

On the pretty printer for identifiers, is there a reason for why we add numbers to repeated identifiers? As it stands, it makes the pretty printer function more complex than it needs to be, as well as breaking the tests whenever I add anything to the gospel stdlibrary.

Finally, in regards to the ortac tests, I would assume the problem is that the pretty printing function for IDs now prints the full path, which probably breaks your your tests. I also have a pp_simpl function which prints the identifier without its path, if you would like an easy fix (assuming that is the problem)

Edit: just noticed I added a file I was using for some quick tests to the repo, I will remove it later 😞. I will also improve the commit message

[n-osborne]

On the pretty printer for identifiers, is there a reason for why we add numbers to repeated identifiers? As it stands, it makes the pretty printer function more complex than it needs to be, as well as breaking the tests whenever I add anything to the gospel stdlibrary.

I believe tags are printed in order to guarantee unicity (some transformation/translatiuon can reorder the code).

Finally, in regards to the ortac tests, I would assume the problem is that the pretty printing function for IDs now prints the full path, which probably breaks your your tests. I also have a pp_simpl function which prints the identifier without its path, if you would like an easy fix (assuming that is the problem)

I'll update Ortac once this is merged, i just didn't want to break everything just before a release.

[n-osborne]

Apart from the minor comments I made (some can be ignored if you feel like it), this seems good to be merged.

And also that if it is not already done:

Edit: just noticed I added a file I was using for some quick tests to the repo, I will remove it later 😞

[mrjazzybread]

Ok, I've made the requested changes :slightly_smiling_face:

[n-osborne]

I would suggest a git rebase -i aeb411 and removing the notes commit :-) You can also reword the last commit to "Update Changelog" if you will in the same rebase.

[mrjazzybread]

Ok I think that's it! I had to make a few more adjustments changes since I added some notes files that should only exist in my fork. It should be all good now.

[n-osborne]

Merged. Thank you!