Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Bool #391

Merged
merged 11 commits into from
Oct 4, 2024
Merged

Bool #391

merged 11 commits into from
Oct 4, 2024

Conversation

mrjazzybread
Copy link
Contributor

@mrjazzybread mrjazzybread commented Mar 30, 2024

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.

@mariojppereira mariojppereira self-requested a review March 30, 2024 21:26
@n-osborne n-osborne mentioned this pull request Apr 3, 2024
@n-osborne
Copy link
Contributor

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
Copy link
Contributor Author

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
Copy link
Contributor Author

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 n-osborne linked an issue May 6, 2024 that may be closed by this pull request
@n-osborne
Copy link
Contributor

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

@mrjazzybread
Copy link
Contributor Author

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
Copy link
Contributor

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
Copy link
Contributor Author

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
Copy link
Contributor

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
Copy link
Contributor

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

@n-osborne
Copy link
Contributor

n-osborne commented Jun 5, 2024

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
Copy link
Contributor Author

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
Copy link
Contributor

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?

Copy link
Contributor

@n-osborne n-osborne left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks.

I would have enjoyed a bit of context in the commit messages when you remove redundant checks (a pointer to where they have already been done for example). But the core of the PR, which is removing the prop type is well handled. Thanks again.

Should I wait for @mariojppereira approval to merge?

src/tterm_printer.ml Outdated Show resolved Hide resolved
@n-osborne
Copy link
Contributor

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

@n-osborne
Copy link
Contributor

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
Copy link
Contributor

Approved and CI happy, merging.
Thanks again!

@n-osborne n-osborne merged commit f1f1860 into ocaml-gospel:main Oct 4, 2024
3 checks passed
@n-osborne n-osborne mentioned this pull request Dec 19, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Difference between prop and bool
2 participants