add shortcut specs also for closures

case_studies/tests/src/closures.rs

@@ -22,10 +22,8 @@ fn closure_test1() {
 
     // Fn-closure
     let x =
-        #[rr::params("i")]
-        #[rr::args("i")]
-        #[rr::requires("(2 * i)%Z ∈ i32")]
-        #[rr::returns("(2 * i)%Z")]
+        #[rr::requires("(2 * x)%Z ∈ i32")]
+        #[rr::returns("(2 * x)%Z")]
         |x: i32| {
             x * 2
         };
@@ -39,10 +37,8 @@ fn closure_test12() {
 
     // Fn-closure
     let x =
-        #[rr::params("i", "j")]
-        #[rr::args("i", "j")]
-        #[rr::requires("(j * i)%Z ∈ i32")]
-        #[rr::returns("(j * i)%Z")]
+        #[rr::requires("(y * x)%Z ∈ i32")]
+        #[rr::returns("(y * x)%Z")]
         |x: i32, y: i32| {
             x * y
         };

rr_frontend/translation/src/body/signature.rs

@@ -358,8 +358,13 @@ impl<'a, 'def: 'a, 'tcx: 'def> TX<'a, 'def, 'tcx> {
                     };
                 }
 
+                // get argument names
+                let arg_names: &'tcx [span::symbol::Ident] = env.tcx().fn_arg_names(proc.get_id());
+                let arg_names: Vec<_> = arg_names.iter().map(|i| i.as_str().to_owned()).collect();
+                info!("arg names: {arg_names:?}");
+
                 // process attributes
-                t.process_closure_attrs(&inputs, output, meta)?;
+                t.process_closure_attrs(&inputs, output, &arg_names, meta)?;
                 Ok(t)
             },
             Err(err) => Err(TranslationError::UnknownError(format!("{:?}", err))),
@@ -647,6 +652,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> TX<'a, 'def, 'tcx> {
         &mut self,
         inputs: &[Ty<'tcx>],
         output: Ty<'tcx>,
+        arg_names: &[String],
         meta: ClosureMetaInfo<'b, 'tcx, 'def>,
     ) -> Result<(), TranslationError<'tcx>> {
         trace!("entering process_closure_attrs");
@@ -694,7 +700,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> TX<'a, 'def, 'tcx> {
             let mut parser = VerboseFunctionSpecParser::new(
                 &translated_arg_types,
                 &translated_ret_type,
-                None,
+                Some(arg_names),
                 &*scope,
                 |lit| ty_translator.translator.intern_literal(lit),
             );

rr_frontend/translation/src/spec_parsers/verbose_function_spec_parser.rs

@@ -690,6 +690,21 @@ where
             }
         }
 
+        // in case we didn't get an args annotation,
+        // implicitly add argument parameters matching their Rust names
+        // IMPORTANT: We do this after `merge_capture_information`, since that adds the first arg
+        if !self.got_args {
+            if let Some(arg_names) = self.arg_names {
+                for (arg, ty) in arg_names.iter().zip(self.arg_types) {
+                    builder
+                        .add_param(coq::binder::Binder::new(Some(arg.to_owned()), coq::term::Type::Infer))?;
+                    let ty_with_ref = specs::TypeWithRef::new(ty.to_owned(), arg.to_owned());
+                    builder.add_arg(ty_with_ref);
+                }
+                self.got_args = true;
+            }
+        }
+
         if self.got_ret && self.got_args {
             builder.have_spec();
         }