Support more annotation expressions

Author: coord-e

src/analyze/annot_fn.rs

@@ -220,6 +220,21 @@ impl<'tcx> AnnotFnTranslator<'tcx> {
                         let rhs = self.to_formula(rhs);
                         return FormulaOrTerm::Formula(lhs.and(rhs));
                     }
+                    rustc_hir::BinOpKind::Add => {
+                        let lhs = self.to_term(lhs);
+                        let rhs = self.to_term(rhs);
+                        return FormulaOrTerm::Term(lhs.add(rhs));
+                    }
+                    rustc_hir::BinOpKind::Sub => {
+                        let lhs = self.to_term(lhs);
+                        let rhs = self.to_term(rhs);
+                        return FormulaOrTerm::Term(lhs.sub(rhs));
+                    }
+                    rustc_hir::BinOpKind::Mul => {
+                        let lhs = self.to_term(lhs);
+                        let rhs = self.to_term(rhs);
+                        return FormulaOrTerm::Term(lhs.mul(rhs));
+                    }
                     _ => {}
                 }
 
@@ -268,6 +283,19 @@ impl<'tcx> AnnotFnTranslator<'tcx> {
                     unimplemented!("unsupported path in formula: {:?}", qpath);
                 }
             }
+            ExprKind::Tup(exprs) => {
+                let terms = exprs.iter().map(|e| self.to_term(e)).collect();
+                FormulaOrTerm::Term(chc::Term::tuple(terms))
+            }
+            ExprKind::Field(expr, field) => {
+                let index = field
+                    .name
+                    .as_str()
+                    .parse::<usize>()
+                    .expect("tuple field index must be a non-negative integer");
+                let term = self.to_term(expr);
+                FormulaOrTerm::Term(term.tuple_proj(index))
+            }
             ExprKind::Block(block, _) => {
                 if block.stmts.is_empty() {
                     self.to_formula_or_term(block.expr.expect("expected an expression in block"))

std.rs

@@ -12,12 +12,97 @@ mod thrust_models {
         #[thrust::def::int_model]
         pub struct Int;
 
+        impl<T> PartialEq<T> for Int where T: super::Model<Ty = Self> {
+            #[thrust::ignored]
+            fn eq(&self, _other: &T) -> bool {
+                unimplemented!()
+            }
+        }
+
+        impl<T> PartialOrd<T> for Int where T: super::Model<Ty = Self> {
+            #[thrust::ignored]
+            fn partial_cmp(&self, _other: &T) -> Option<std::cmp::Ordering> {
+                unimplemented!()
+            }
+        }
+
+        impl<T> std::ops::Add<T> for Int where T: super::Model<Ty = Self> {
+            type Output = Self;
+
+            #[thrust::ignored]
+            fn add(self, _rhs: T) -> Self::Output {
+                unimplemented!()
+            }
+        }
+
+        impl<T> std::ops::Sub<T> for Int where T: super::Model<Ty = Self> {
+            type Output = Self;
+
+            #[thrust::ignored]
+            fn sub(self, _rhs: T) -> Self::Output {
+                unimplemented!()
+            }
+        }
+
+        impl<T> std::ops::Mul<T> for Int where T: super::Model<Ty = Self> {
+            type Output = Self;
+
+            #[thrust::ignored]
+            fn mul(self, _rhs: T) -> Self::Output {
+                unimplemented!()
+            }
+        }
+
+        impl std::ops::Neg for Int {
+            type Output = Self;
+
+            #[thrust::ignored]
+            fn neg(self) -> Self::Output {
+                unimplemented!()
+            }
+        }
+
         #[thrust::def::mut_model]
         pub struct Mut<T>(PhantomData<T>);
 
+        impl<T> Mut<T> {
+            #[thrust::def::mut_new]
+            pub fn new(_a: T, _b: T) -> Self {
+                unimplemented!()
+            }
+        }
+
+        impl<T> std::ops::Deref for Mut<T> {
+            type Target = T;
+            fn deref(&self) -> &Self::Target {
+                unimplemented!()
+            }
+        }
+
+        impl<T> std::ops::Not for Mut<T> {
+            type Output = T;
+            fn not(self) -> Self::Output {
+                unimplemented!()
+            }
+        }
+
         #[thrust::def::box_model]
         pub struct Box<T>(PhantomData<T>);
 
+        impl<T> Box<T> {
+            #[thrust::def::box_new]
+            pub fn new(_x: T) -> Self {
+                unimplemented!()
+            }
+        }
+
+        impl<T> std::ops::Deref for Box<T> {
+            type Target = T;
+            fn deref(&self) -> &Self::Target {
+                unimplemented!()
+            }
+        }
+
         #[thrust::def::array_model]
         pub struct Array<I, T>(PhantomData<I>, PhantomData<T>);
 
@@ -27,6 +112,10 @@ mod thrust_models {
         pub struct Vec<T>(pub Array<Int, T>, pub usize);
     }
 
+    impl Model for model::Int {
+        type Ty = model::Int;
+    }
+
     impl Model for isize {
         type Ty = model::Int;
     }
@@ -75,6 +164,10 @@ mod thrust_models {
         type Ty = (<T0 as Model>::Ty, <T1 as Model>::Ty, <T2 as Model>::Ty);
     }
 
+    impl<T0, T1, T2, T3> Model for (T0, T1, T2, T3) where T0: Model, T1: Model, T2: Model, T3: Model {
+        type Ty = (<T0 as Model>::Ty, <T1 as Model>::Ty, <T2 as Model>::Ty, <T3 as Model>::Ty);
+    }
+
     impl<'a, T> Model for &'a mut T where T: Model {
         type Ty = model::Mut<<T as Model>::Ty>;
     }