Parse tuples in annotations

Author: coord-e

src/annot.rs

@@ -168,6 +168,28 @@ where
         }
     }
 
+    fn parse_term_or_tuple(&mut self) -> Result<(chc::Term<T::Output>, chc::Sort)> {
+        let mut terms_and_sorts = Vec::new();
+        loop {
+            terms_and_sorts.push(self.parse_term()?);
+            if let Some(Token {
+                kind: TokenKind::Comma,
+                ..
+            }) = self.look_ahead_token(0)
+            {
+                self.consume();
+            } else {
+                break;
+            }
+        }
+        if terms_and_sorts.len() == 1 {
+            Ok(terms_and_sorts.pop().unwrap())
+        } else {
+            let (terms, sorts) = terms_and_sorts.into_iter().unzip();
+            Ok((chc::Term::tuple(terms), chc::Sort::tuple(sorts)))
+        }
+    }
+
     fn parse_atom_term(&mut self) -> Result<(chc::Term<T::Output>, chc::Sort)> {
         let tt = self.next_token_tree("term")?.clone();
 
@@ -178,103 +200,145 @@ where
                     resolver: self.boxed_resolver(),
                     cursor: s.trees(),
                 };
-                let term = parser.parse_term()?;
+                let (term, sort) = parser.parse_term_or_tuple()?;
                 parser.end_of_input()?;
-                return Ok(term);
+                return Ok((term, sort));
             }
-            _ => unimplemented!(),
+            _ => return Err(ParseAttrError::unexpected_token_tree("token", tt)),
         };
 
-        if let Some((ident, _)) = t.ident() {
+        let (term, sort) = if let Some((ident, _)) = t.ident() {
             let (v, sort) = self.resolve(ident)?;
-            return Ok((chc::Term::var(v), sort));
+            (chc::Term::var(v), sort)
+        } else {
+            match t.kind {
+                TokenKind::Literal(lit) => match lit.kind {
+                    LitKind::Integer => (
+                        chc::Term::int(lit.symbol.as_str().parse().unwrap()),
+                        chc::Sort::int(),
+                    ),
+                    _ => unimplemented!(),
+                },
+                _ => {
+                    return Err(ParseAttrError::unexpected_token(
+                        "identifier, or literal",
+                        t.clone(),
+                    ));
+                }
+            }
+        };
+
+        Ok((term, sort))
+    }
+
+    fn parse_postfix_term(&mut self) -> Result<(chc::Term<T::Output>, chc::Sort)> {
+        let (term, sort) = self.parse_atom_term()?;
+
+        let mut fields = Vec::new();
+        loop {
+            if let Some(Token {
+                kind: TokenKind::Dot,
+                ..
+            }) = self.look_ahead_token(0)
+            {
+                self.consume();
+                match self.next_token("field")? {
+                    Token {
+                        kind: TokenKind::Literal(lit),
+                        ..
+                    } if matches!(lit.kind, LitKind::Integer) => {
+                        let idx = lit.symbol.as_str().parse().unwrap();
+                        fields.push(idx);
+                    }
+                    t => return Err(ParseAttrError::unexpected_token("field", t.clone())),
+                }
+            } else {
+                break;
+            }
         }
-        let (term, sort) = match t.kind {
-            TokenKind::Literal(lit) => match lit.kind {
-                LitKind::Integer => (
-                    chc::Term::int(lit.symbol.as_str().parse().unwrap()),
-                    chc::Sort::int(),
-                ),
-                _ => unimplemented!(),
-            },
-            TokenKind::BinOp(BinOpToken::Minus) => {
-                let (operand, sort) = self.parse_atom_term()?;
+
+        let term = fields.iter().fold(term, |acc, idx| acc.tuple_proj(*idx));
+        let sort = fields.iter().fold(sort, |acc, idx| acc.tuple_elem(*idx));
+        Ok((term, sort))
+    }
+
+    fn parse_prefix_term(&mut self) -> Result<(chc::Term<T::Output>, chc::Sort)> {
+        let (term, sort) = match self.look_ahead_token(0).map(|t| &t.kind) {
+            Some(TokenKind::BinOp(BinOpToken::Minus)) => {
+                self.consume();
+                let (operand, sort) = self.parse_postfix_term()?;
                 (operand.neg(), sort)
             }
-            TokenKind::BinOp(BinOpToken::Star) => {
-                let (operand, sort) = self.parse_atom_term()?;
+            Some(TokenKind::BinOp(BinOpToken::Star)) => {
+                self.consume();
+                let (operand, sort) = self.parse_postfix_term()?;
                 match sort {
                     chc::Sort::Box(inner) => (chc::Term::box_current(operand), *inner),
                     chc::Sort::Mut(inner) => (chc::Term::mut_current(operand), *inner),
                     _ => return Err(ParseAttrError::unsorted_op("*", sort)),
                 }
             }
-            TokenKind::BinOp(BinOpToken::Caret) => {
-                let (operand, sort) = self.parse_atom_term()?;
+            Some(TokenKind::BinOp(BinOpToken::Caret)) => {
+                self.consume();
+                let (operand, sort) = self.parse_postfix_term()?;
                 if let chc::Sort::Mut(inner) = sort {
                     (chc::Term::mut_final(operand), *inner)
                 } else {
                     return Err(ParseAttrError::unsorted_op("^", sort));
                 }
             }
-            _ => {
-                return Err(ParseAttrError::unexpected_token_tree(
-                    "-, *, ^, (, identifier, or literal",
-                    tt,
-                ))
-            }
+            _ => self.parse_postfix_term()?,
         };
-
         Ok((term, sort))
     }
 
     fn parse_term(&mut self) -> Result<(chc::Term<T::Output>, chc::Sort)> {
-        let (lhs, lhs_sort) = self.parse_atom_term()?;
+        let (lhs, lhs_sort) = self.parse_prefix_term()?;
 
         let (term, sort) = match self.look_ahead_token(0).map(|t| &t.kind) {
             Some(TokenKind::BinOp(BinOpToken::Plus)) => {
                 self.consume();
-                let (rhs, _) = self.parse_atom_term()?;
+                let (rhs, _) = self.parse_prefix_term()?;
                 (lhs.add(rhs), chc::Sort::int())
             }
             Some(TokenKind::BinOp(BinOpToken::Minus)) => {
                 self.consume();
-                let (rhs, _) = self.parse_atom_term()?;
+                let (rhs, _) = self.parse_prefix_term()?;
                 (lhs.sub(rhs), chc::Sort::int())
             }
             Some(TokenKind::BinOp(BinOpToken::Star)) => {
                 self.consume();
-                let (rhs, _) = self.parse_atom_term()?;
+                let (rhs, _) = self.parse_prefix_term()?;
                 (lhs.mul(rhs), chc::Sort::int())
             }
             Some(TokenKind::EqEq) => {
                 self.consume();
-                let (rhs, _) = self.parse_atom_term()?;
+                let (rhs, _) = self.parse_prefix_term()?;
                 (lhs.eq(rhs), chc::Sort::bool())
             }
             Some(TokenKind::Ne) => {
                 self.consume();
-                let (rhs, _) = self.parse_atom_term()?;
+                let (rhs, _) = self.parse_prefix_term()?;
                 (lhs.ne(rhs), chc::Sort::bool())
             }
             Some(TokenKind::Ge) => {
                 self.consume();
-                let (rhs, _) = self.parse_atom_term()?;
+                let (rhs, _) = self.parse_prefix_term()?;
                 (lhs.ge(rhs), chc::Sort::bool())
             }
             Some(TokenKind::Le) => {
                 self.consume();
-                let (rhs, _) = self.parse_atom_term()?;
+                let (rhs, _) = self.parse_prefix_term()?;
                 (lhs.le(rhs), chc::Sort::bool())
             }
             Some(TokenKind::Gt) => {
                 self.consume();
-                let (rhs, _) = self.parse_atom_term()?;
+                let (rhs, _) = self.parse_prefix_term()?;
                 (lhs.gt(rhs), chc::Sort::bool())
             }
             Some(TokenKind::Lt) => {
                 self.consume();
-                let (rhs, _) = self.parse_atom_term()?;
+                let (rhs, _) = self.parse_prefix_term()?;
                 (lhs.lt(rhs), chc::Sort::bool())
             }
             _ => return Ok((lhs, lhs_sort)),
@@ -295,7 +359,7 @@ where
             }
         }
 
-        let (lhs, _) = self.parse_atom_term()?;
+        let (lhs, _) = self.parse_prefix_term()?;
         let pred = match self.next_token("<=, >=, <, >, == or !=")? {
             Token {
                 kind: TokenKind::EqEq,
@@ -321,7 +385,12 @@ where
                 kind: TokenKind::Lt,
                 ..
             } => chc::KnownPred::LESS_THAN,
-            t => return Err(ParseAttrError::unexpected_token("==", t.clone())),
+            t => {
+                return Err(ParseAttrError::unexpected_token(
+                    "<=, >=, <, >, == or !=",
+                    t.clone(),
+                ))
+            }
         };
         let (rhs, _) = self.parse_term()?;
         Ok(chc::Atom::new(pred.into(), vec![lhs, rhs]))
@@ -340,16 +409,16 @@ where
                 let atom = self.parse_atom()?;
                 Ok(chc::Formula::Atom(atom).not())
             }
-            Some(TokenTree::Delimited(_, _, Delimiter::Parenthesis, s)) => {
-                self.consume();
-                let mut parser = Parser {
-                    resolver: self.boxed_resolver(),
-                    cursor: s.trees(),
-                };
-                let formula = parser.parse_formula()?;
-                parser.end_of_input()?;
-                Ok(formula)
-            }
+            //Some(TokenTree::Delimited(_, _, Delimiter::Parenthesis, s)) => {
+            //    self.consume();
+            //    let mut parser = Parser {
+            //        resolver: self.boxed_resolver(),
+            //        cursor: s.trees(),
+            //    };
+            //    let formula = parser.parse_formula()?;
+            //    parser.end_of_input()?;
+            //    Ok(formula)
+            //}
             _ => {
                 let atom = self.parse_atom()?;
                 Ok(chc::Formula::Atom(atom))

src/chc.rs

@@ -176,7 +176,7 @@ impl Sort {
         }
     }
 
-    fn tuple_elem(self, index: usize) -> Self {
+    pub fn tuple_elem(self, index: usize) -> Self {
         match self {
             Sort::Tuple(ss) => ss[index].clone(),
             _ => panic!("invalid tuple_elem"),

tests/ui/fail/take_max_annot.rs

@@ -8,8 +8,8 @@ fn rand() -> i64 { unimplemented!() }
 
 #[thrust::requires(true)]
 #[thrust::ensures(
-    (*ma >= *mb && *ma == ^ma && ma == result) ||
-    (*ma < *mb && *mb == ^mb && mb == result)
+    *ma >= *mb && *ma == ^ma && ma == result ||
+    *ma < *mb && *mb == ^mb && mb == result
 )]
 fn take_max<'a>(ma: &'a mut i64, mb: &'a mut i64) -> &'a mut i64 {
   if *ma >= *mb {

tests/ui/fail/tuple_annot.rs

@@ -0,0 +1,11 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+
+#[thrust::requires(true)]
+#[thrust::ensures(^x == ((*x).1, (*x).1))]
+fn swap_tuple(x: &mut (i32, i32)) {
+    let v = *x;
+    *x = (v.1, v.0);
+}
+
+fn main() {}

tests/ui/pass/take_max_annot.rs

@@ -8,8 +8,8 @@ fn rand() -> i64 { unimplemented!() }
 
 #[thrust::requires(true)]
 #[thrust::ensures(
-    (*ma >= *mb && *mb == ^mb && ma == result) ||
-    (*ma < *mb && *ma == ^ma && mb == result)
+    *ma >= *mb && *mb == ^mb && ma == result ||
+    *ma < *mb && *ma == ^ma && mb == result
 )]
 fn take_max<'a>(ma: &'a mut i64, mb: &'a mut i64) -> &'a mut i64 {
   if *ma >= *mb {

tests/ui/pass/tuple_annot.rs

@@ -0,0 +1,11 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+
+#[thrust::requires(true)]
+#[thrust::ensures(^x == ((*x).1, (*x).0))]
+fn swap_tuple(x: &mut (i32, i32)) {
+    let v = *x;
+    *x = (v.1, v.0);
+}
+
+fn main() {}