Skip to content

Commit e3c3f88

Browse files
committed
Parse pointer sorts in annotation
1 parent b31654d commit e3c3f88

1 file changed

Lines changed: 20 additions & 0 deletions

File tree

src/annot.rs

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -835,6 +835,26 @@ where
835835
fn parse_sort(&mut self) -> Result<chc::Sort> {
836836
let tt = self.next_token_tree("sort")?.clone();
837837
match tt {
838+
TokenTree::Token(
839+
Token {
840+
kind: TokenKind::BinOp(BinOpToken::And),
841+
..
842+
},
843+
_,
844+
) => match self.look_ahead_token(0) {
845+
Some(Token {
846+
kind: TokenKind::Ident(sym, _),
847+
..
848+
}) if sym.as_str() == "mut" => {
849+
self.consume();
850+
let inner_sort = self.parse_sort()?;
851+
Ok(chc::Sort::mut_(inner_sort))
852+
}
853+
_ => {
854+
let inner_sort = self.parse_sort()?;
855+
Ok(chc::Sort::box_(inner_sort))
856+
}
857+
},
838858
TokenTree::Token(
839859
Token {
840860
kind: TokenKind::Ident(sym, _),

0 commit comments

Comments
 (0)