Bool

[mrjazzybread]

Hello

This pull request changes the Gospel typed AST so that the types of terms are represented with ty instead of ty option, thereby eliminating the distinction between terms that evaluate to bool and propositions. This also means that programs are no longer transformed to turn bools into props. A few caveats:

• There are still some functions that I want to refactor/rethink their usefulness.
• Predicates are now just syntatic sugar for functions that return bools. Should I remove them from the parser now or should I do another pr?
• Some of the tests didn't pass initially: a test about the variant clause didn't pass because now the error message is different. The ill typed program was variant i = 0. The old error message was "A term was expected" and the new error message is now "this term has type bool but was expected a value of type integer". In my opinion this message is a bit more clear, but I'm wondering what you think. Another test that failed was one where a predicate is used as an argument for a higher order function that receives a function of type 'a -> bool. This is now valid under the new typechecker, I suppose this is fine? Another test that failed was the location test, but that is only because it dumps the entire ast, so any changes are always gonna effect it. (side note: this test seems very fragile, may I change it in a future commit so it uses grep and only prints the locations?) Edit: I just realised that I also have the commits for the path pr here :|, not sure if I should do another pr or if we should wrap up the identifiers one first.

[n-osborne]

Thanks!

• There are still some functions that I want to refactor/rethink their usefulness.

Feel free do do so, some code base cleanup is always welcome and one of the points of this modification is to make the type-checker simpler.

• Predicates are now just syntatic sugar for functions that return bools. Should I
remove them from the parser now or should I do another pr?

As stated in #393, there are other problems in the preprocessor, so maybe we can have another PR dealing with syntax. Also, I'm not sure we are completely decided about removing predicate as a keyword, but we do want to remove the bool/prop disctinction.

• Some of the tests didn't pass initially: a test about the variant clause didn't
pass because now the error message is different. The ill typed program was variant i = 0 . The old error message was "A term was expected" and the new error message is now
"this term has type bool but was expected a value of type integer". In my opinion this message is a bit more clear, but I'm wondering what you think.

This is indeed a nice improvement in the error message!

Another test that failed was one where a predicate is used as an argument for a higher order function that
receives a function of type 'a -> bool . This is now valid under the new typechecker, I suppose this is fine?

That makes sense and I believe this makes gospel a bit more natural from a programmer point of view :-)

Another test that failed was the location test, but that is only because it dumps the entire ast, so any changes are always gonna effect it. (side note: this test seems very fragile, may I change it in a future commit so it uses grep and
only prints the locations?)

This was to be expected but your idea of using grep is very nice! (As grep seems to be available on all the CI platform.) Though we may want to keep this PR focused on removing the bool/prop disctinction. This can be done in another PR that focuses on cleaning up tests. You can add a short explanation why these tests changed in the commit adding them if you want. (this is really not a strong opinion, feel free to add the grep filter if the test modification noise annoys you too much :-) )

Edit: I just realised that I also have the commits for the path pr here :|, not sure if I should do another pr or if we should wrap up the identifiers one first.

No need to make another PR! This one is already great! There are two possible situations here:

1. if the modifications in PR 2 depends on the ones done in PR 1, it is natural to base PR 2 on PR 1 (to avoid too many conficts or to use the new modifications)
2. if there is no dependencies, there is no need for PR 2 to be based on PR 1 (although, it is not a big problem, we will just have to be careful in the order in which we merge them).

If in situation 2. and you want to correct the situation, a git rebase --onto=UPSTREAM/main @^^ should do the trick (UPSTREAM being the name you gave to the remote ocaml-gospel repo).

[mrjazzybread]

Hello

There are some functions in the Tast_helper module that perform checks that are already performed by the typechecker. For example, in mk_function we perform a series of type checking validations that are already done by the typechecker (for example, checking if the type of the returned value is equal to the function's return type). I am either removing these extra verfications or placing them in the typechecker itself whenever is necessary, this way we keep all the typechecking logic in the same place.

[mrjazzybread]

Ok, I think this is all I want to do. Besides the unification of the type of booleans and propositions, I need some refactoring, which consisted mostly of removing redundant checks. One of them was checking if a function's spec had no undefined variables. I removed the check, but kept the function that collects all the free variables since it may be useful at some point down the line.

[n-osborne]

There are some conflicts that need to be resolved. This would be a shame to lose the benefit of this PR!

[mrjazzybread]

Hello

I have resolved the conflicts, but one of the checks failed, specifically with regards to the changelog. I'm not sure what I did wrong :(

[n-osborne]

Thanks! This is the changelog check. There is no new entry in CHANGES.md compared to main. I'm more confused by the presence of commits from #396.

[mrjazzybread]

Yes I had already mentioned that I accidentally had the commits for the identifiers PR in this one.

Edit: I just realised that I also have the commits for the path pr here :|, not sure if I should do another pr or if we should wrap up the identifiers one first.

And you said

No need to make another PR! This one is already great!

But yes, it is a bit awkward :| As for the changelog, I will add an entry to it ASAP.

[n-osborne]

Yes, but what puzzles me is that it seems to be a mix of commits from both PRs now. The heavy solution would be to check that the last commit put the code in the state you want and then make a squash merge. The more subtle solution would be to rebase your PR on main, removing the unwanted commits in the process.

[n-osborne]

But I believe a rebase on main is necessary as the PR seems to remove some changes done by previous ones.

[n-osborne]

For review purpose I've rebased the PR on main there. You can take it if you want (and if I didn't miss anything) :-) I believe that if you fetch my branch and then reset yours on it I should disappear from the authors of the commits according to github (which I'm totally ok with).

Apart from the rebasing, I've allowed myself to run ocamlformat on each commit and reformat the commit messages. Some of the commit messages could use some some love (for example, Refactoring is a bit fuzzy).

I've noticed that Dterm.dterms still has an optional type (where None means bool IIUC). Is there a reason why or could we also remove this?

@mariojppereira do you still want to review this PR?

[mrjazzybread]

Ok, I reset the branch with the commits from your rebase, I think everything should be in order. I'll try and rename some of the commit messages tomorrow. Regarding Dterm.dterm, the reason why it is an option is because it is a late initialized variable that is defined during type unification. When we generate the final typed term from a dterm we may assume that all dtypes are different from None. In fact, during the typing phase, when I access the type of a dterm I just use Option.get. I tried to refactor the code to remove it, however, it requires a lot of modifications that would distract from the main point of the PR.

[n-osborne]

ocaml-ci failling seems unrelated.

I believe the PR is just waiting for on entry in the changelog to be mergeable.

@mariojppereira did you had a chance to look at it?

[n-osborne]

CI failing: you should run ocamlformat on the penultimate commit.

[n-osborne]

I've just spotted that the changelog is still update in the 0.3.0 section. 0.3.0 has been released, this PR should go in Unreleased section

[n-osborne]

Approved and CI happy, merging. Thanks again!