remove tuples from the pool of potential auto triggers

verus-lang · Jun 28, 2024 · d94d123 · d94d123
1 parent edb8f53
commit d94d123
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 1 deletion.
diff --git a/source/vir/src/def.rs b/source/vir/src/def.rs
@@ -402,6 +402,16 @@ pub fn prefix_tuple_param(i: usize) -> Ident {
     Arc::new(format!("{}{}", PREFIX_TUPLE_PARAM, i))
 }
 
+pub fn is_tuple(path: &Path, variant: &Ident) -> bool {
+    let it = path.krate.is_none()
+        && path.segments.len() == 1
+        && path.segments[0].starts_with(PREFIX_TUPLE_TYPE);
+    if it {
+        assert!(variant.starts_with(PREFIX_TUPLE_TYPE));
+    }
+    it
+}
+
 pub fn prefix_spec_fn_type(i: usize) -> Path {
     let ident = Arc::new(format!("{}{}", PREFIX_SPEC_FN_TYPE, i));
     Arc::new(PathX { krate: None, segments: Arc::new(vec![ident]) })

diff --git a/source/vir/src/triggers_auto.rs b/source/vir/src/triggers_auto.rs
@@ -323,7 +323,11 @@ fn gather_terms(ctxt: &mut Ctxt, ctx: &Ctx, exp: &Exp, depth: u64) -> (bool, Ter
             let (is_pures, terms): (Vec<bool>, Vec<Term>) =
                 args.map(|e| gather_terms(ctxt, ctx, &e.a, depth + 1)).unzip();
             let is_pure = is_pures.into_iter().all(|b| b);
-            (is_pure, Arc::new(TermX::App(App::Ctor(path.clone(), variant), Arc::new(terms))))
+            if crate::def::is_tuple(path, &variant) {
+                (false, Arc::new(TermX::App(ctxt.other(), Arc::new(terms))))
+            } else {
+                (is_pure, Arc::new(TermX::App(App::Ctor(path.clone(), variant), Arc::new(terms))))
+            }
         }
         ExpX::NullaryOpr(_) => (false, Arc::new(TermX::App(ctxt.other(), Arc::new(vec![])))),
         ExpX::Unary(UnaryOp::Trigger(_), e1) => gather_terms(ctxt, ctx, e1, depth),