-
Notifications
You must be signed in to change notification settings - Fork 1
Support user-defined predicate call in annotation #22
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
base: main
Are you sure you want to change the base?
Conversation
Support logical connectives in annotations
Define rty::Formula and replace UnboundAssumption and Refinement with it
Introduce PlaceTypeBuilder to simplify PlaceType construction
Add documentation to annot, chc, and pretty modules
Add documentation to rty and some other modules
Add GitHub Actions workflow to host docs in GitHub pages
Handle parens in annotations properly
Ignore lifetime parameters properly when numbering type params
…nto annot-preds-call
a user-defined predicate call
8b90c59 to
4cd0a34
Compare
src/chc.rs
Outdated
| } | ||
|
|
||
| #[derive(Debug, Clone, PartialEq, Eq, Hash)] | ||
| pub struct UserDefinedPred { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This struct seems to be unused. I think it's more natural to rename UserDefinedPredSymbol to UserDefinedPred and remove this one.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Originally I defined this struct to implement a parser for definitions of user-defined predicates. If the parser is implemented in the future, it might be fine to leave this definition as is.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I’d like to avoid leaving unused structs because it makes the intent harder to understand later. Requirements might change by the time we write the parser for the definitions, so I don’t think there's a need to define them speculatively right now. (Either way, I think cargo clippy or something will probably flag it.)
|
I reflected the comments in above review. |
…o `UserDefinedPred`
This extention allows users to call arbitrary user-defined predicates (e.g., is_double(x, result)) within annotations.
Currently, a dedicated syntax for defining user-defined predicates is not yet supported. Therefore, users must define them using the #![thrust::raw_define()] (introduced in #21 ) attribute for now.
The predicate
is_double()defined using#![thrust::raw_define()]can be called in the annotations such as#[thrust::ensures()]: