Parse <t> and <t1, t2> in annotations

Author: coord-e

src/annot.rs

@@ -502,6 +502,31 @@ where
                     ),
                     _ => unimplemented!(),
                 },
+                TokenKind::Lt => {
+                    let (t1, s1) = self
+                        .parse_binop_2()?
+                        .into_term()
+                        .ok_or_else(|| ParseAttrError::unexpected_formula("in box/mut term"))?;
+
+                    match self.next_token("> or ,")? {
+                        Token {
+                            kind: TokenKind::Gt,
+                            ..
+                        } => FormulaOrTerm::Term(chc::Term::box_(t1), chc::Sort::box_(s1)),
+                        Token {
+                            kind: TokenKind::Comma,
+                            ..
+                        } => {
+                            let (t2, _s2) = self
+                                .parse_binop_2()?
+                                .into_term()
+                                .ok_or_else(|| ParseAttrError::unexpected_formula("in mut term"))?;
+                            self.expect_next_token(TokenKind::Gt, ">")?;
+                            FormulaOrTerm::Term(chc::Term::mut_(t1, t2), chc::Sort::mut_(s1))
+                        }
+                        t => return Err(ParseAttrError::unexpected_token("> or ,", t.clone())),
+                    }
+                }
                 _ => {
                     return Err(ParseAttrError::unexpected_token(
                         "identifier, or literal",

tests/ui/fail/annot_box_term.rs

@@ -0,0 +1,17 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+
+#[thrust::sig(fn(x: int) -> {r: Box<int> | r == <x>})]
+fn box_create(x: i64) -> Box<i64> {
+    Box::new(x)
+}
+
+#[thrust::requires(b == <v>)]
+fn box_consume(b: Box<i64>, v: i64) {
+    assert!(*b == v);
+}
+
+fn main() {
+    let b = box_create(42);
+    box_consume(b, 10);
+}

tests/ui/fail/annot_mut_term.rs

@@ -0,0 +1,13 @@
+//@error-in-other-file: Unsat
+
+#[thrust::requires(true)]
+#[thrust::ensures(x == <*x, y>)]
+fn f(x: &mut i64, y: i64) {
+    *x = y;
+}
+
+fn main() {
+    let mut a = 1;
+    f(&mut a, 2);
+    assert!(a == 1);
+}

tests/ui/pass/annot_box_term.rs

@@ -0,0 +1,17 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+
+#[thrust::sig(fn(x: int) -> {r: Box<int> | r == <x>})]
+fn box_create(x: i64) -> Box<i64> {
+    Box::new(x)
+}
+
+#[thrust::requires(b == <v>)]
+fn box_consume(b: Box<i64>, v: i64) {
+    assert!(*b == v);
+}
+
+fn main() {
+    let b = box_create(42);
+    box_consume(b, 42);
+}

tests/ui/pass/annot_mut_term.rs

@@ -0,0 +1,13 @@
+//@check-pass
+
+#[thrust::requires(true)]
+#[thrust::ensures(x == <*x, y>)]
+fn f(x: &mut i64, y: i64) {
+    *x = y;
+}
+
+fn main() {
+    let mut a = 1;
+    f(&mut a, 2);
+    assert!(a == 2);
+}