-
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
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. |
…s TokenTrees directly
a user-defined predicate call
…o `UserDefinedPred`
170ea6d to
d602bb3
Compare
coord-e
left a comment
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.
mostly LGTM, please rebase after merging #21
| Pred::Matcher(p) | ||
| } | ||
| } | ||
|
|
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.
please add impl From<UserDefinedPred> for Pred
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()]: