Enable to parse enum constructors in annotations #14
Conversation
There was a problem hiding this comment.
Pull request overview
This PR adds support for parsing enum constructors in annotations, enabling the use of datatype constructors like X::A(1) in Thrust's #[thrust::requires(...)] and similar annotations. The implementation is explicitly ad-hoc and limited in scope, with plans for a more comprehensive re-implementation using macros.
Key Changes:
- Added
AnnotPathandAnnotPathSegmentstructs to represent paths in annotations - Implemented path parsing to handle multi-segment paths with optional generic arguments
- Extended the annotation parser to recognize and process enum/datatype constructors
Reviewed changes
Copilot reviewed 3 out of 3 changed files in this pull request and generated 3 comments.
| File | Description |
|---|---|
tests/ui/pass/annot_enum_simple.rs |
Adds a passing test case demonstrating enum constructor usage in requires/ensures annotations |
tests/ui/fail/annot_enum_simple.rs |
Adds a failing test case to verify that incorrect enum constructor constraints are properly detected |
src/annot.rs |
Implements core parsing logic for paths and datatype constructors, including new structs AnnotPath and AnnotPathSegment, and new parsing methods |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| fn parse_datatype_ctor_args(&mut self) -> Result<Vec<chc::Term<T::Output>>> { | ||
| let mut terms = Vec::new(); | ||
| loop { | ||
| let formula_or_term = self.parse_formula_or_term()?; | ||
| let (t, _) = formula_or_term.into_term().ok_or_else(|| { | ||
| ParseAttrError::unexpected_formula("in datatype constructor arguments") | ||
| })?; | ||
| terms.push(t); | ||
| if let Some(Token { | ||
| kind: TokenKind::Comma, | ||
| .. | ||
| }) = self.look_ahead_token(0) | ||
| { | ||
| self.consume(); | ||
| } else { | ||
| break; | ||
| } | ||
| } | ||
| Ok(terms) | ||
| } |
There was a problem hiding this comment.
The function does not handle empty argument lists for datatype constructors. If a constructor has no arguments (e.g., X::A()), the function will attempt to parse a formula or term on line 412 when the token stream is empty, which will cause a parsing error. The function should check if the token stream is empty before attempting to parse arguments.
| pub fn to_datatype_ctor<V>(&self, ctor_args: Vec<chc::Term<V>>) -> (chc::Term<V>, chc::Sort) { | ||
| let mut segments = self.segments.clone(); | ||
|
|
||
| let ctor = segments.pop().unwrap(); | ||
| if !ctor.generic_args.is_empty() { | ||
| unimplemented!("generic arguments in datatype constructor"); | ||
| } | ||
| let Some(ty_last_segment) = segments.last_mut() else { | ||
| unimplemented!("single segment path"); | ||
| }; | ||
| let generic_args: Vec<_> = ty_last_segment.generic_args.drain(..).collect(); | ||
| let ty_path_idents: Vec<_> = segments | ||
| .into_iter() | ||
| .map(|segment| { | ||
| if !segment.generic_args.is_empty() { | ||
| unimplemented!("generic arguments in datatype constructor"); | ||
| } | ||
| segment.ident.to_string() | ||
| }) | ||
| .collect(); | ||
| // see refine::datatype_symbol | ||
| let d_sym = chc::DatatypeSymbol::new(ty_path_idents.join(".")); | ||
| let v_sym = chc::DatatypeSymbol::new(format!("{}.{}", d_sym, ctor.ident.as_str())); | ||
| let term = chc::Term::datatype_ctor(d_sym.clone(), generic_args.clone(), v_sym, ctor_args); | ||
| let sort = chc::Sort::datatype(d_sym, generic_args); | ||
| (term, sort) | ||
| } |
There was a problem hiding this comment.
This public method lacks documentation explaining its purpose, parameters, return value, and the limitations indicated by the unimplemented cases. Consider adding a doc comment that describes what this method does and under what conditions the unimplemented cases occur.
| pub fn single_segment_ident(&self) -> Option<&Ident> { | ||
| if self.segments.len() == 1 && self.segments[0].generic_args.is_empty() { | ||
| Some(&self.segments[0].ident) | ||
| } else { | ||
| None | ||
| } | ||
| } |
There was a problem hiding this comment.
This public method lacks documentation explaining its purpose and return value. Consider adding a doc comment that describes what this method does and when it returns Some vs None.
supports only simple cases in ad-hoc way. I plan to re-implement annotations by lifting annotation expressions into Rust functions using macros. This will allow rustc to parse them into HIR, effectively delegating path resolution to the compiler.