Making pts_to a method
#232
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Just one type annotation needed in library, and it makes sense. Adding instances for ref, gref, box, vec, array, higher array. It's definitely not ideal to have to mark everything pulse_unfold, but that seems easy to fix: we need to tag instances and methods with a particular attribute and add it to the normalization call done by Pulse.
|
( testing zulip bot :^) ) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
By adding a
pulse_unfoldattribute to thepts_tomethod (and the instances), it gets automatically unfolded by the Pulse checker whenever needed, and we can just work with the polymorphicpts_to. This PR fixes the class, defines some instances for the pointer-like types in the library, and uses it wherever possible.There is tension whenever refinements are involved, as usual. See for instance FStarLang/FStar#3534. I think that if that is fixed, this will become quite robust.
The operator
|->is aliased topts_to(with full permission). However the precedence is wrong: it binds weaker than**, so we would require parenthesis everywhere, and hence I didn't use it. I think we should just add configurable mixfix operators to F* to fix this.Resugaring and context printing do not know about the typeclasses being unfolded, so context dumps are still in the underlying terms (
R.pts_to,A.pts_to, etc). This is sometimes good, sometimes bad. A toggle would be nice, but this is an F* problem.Note: using typeclasses for Pulse functions, instead of just slprops, also somewhat works.