[anodized-core] fix: postcondition closure input type ascription (#152)

- If the closure's input already has a type ascription, leave it
unchanged.
- Refactor and comment.

Author: mkovaxx

crates/anodized-core/src/instrument/fns.rs

@@ -243,15 +243,19 @@ impl Config {
             postcondition_clauses.push(clause);
         }
         for postcondition in &spec.ensures {
-            let closure = annotate_postcondition_closure_argument(
-                postcondition.closure.clone(),
-                return_type.clone(),
-            );
-            let expr = parse_quote! { (#closure)(&#output_ident) };
-            let inputs = &postcondition.closure.inputs;
-            let body = &postcondition.closure.body;
+            let closure = &postcondition.closure;
+            let input = &closure.inputs.first().unwrap();
+            let output = &closure.output;
+            let body = &closure.body;
+            let expr = match input {
+                Pat::Type(_) => parse_quote! { (#closure)(&#output_ident) },
+                _ => parse_quote! {
+                    // If the closure's input doesn't have a type ascription, add one.
+                    (|#input: &#return_type| #output { #body })(&#output_ident)
+                },
+            };
             // Omit the closure's return type for brevity.
-            let repr = quote! { |#inputs| #body }.to_string();
+            let repr = quote! { |#input| #body }.to_string();
             let clause = self.build_clause_eval(postcondition.cfg.as_ref(), &expr, &repr);
             postcondition_clauses.push(clause);
         }
@@ -308,26 +312,3 @@ impl Config {
         }
     }
 }
-
-fn annotate_postcondition_closure_argument(
-    mut closure: syn::ExprClosure,
-    return_type: syn::Type,
-) -> syn::ExprClosure {
-    // Add type annotation: convert |param| to |param: &ReturnType|.
-    if let Some(first_input) = closure.inputs.first_mut() {
-        // Wrap the pattern with a type annotation
-        let pattern = first_input.clone();
-        *first_input = syn::Pat::Type(syn::PatType {
-            attrs: vec![],
-            pat: Box::new(pattern),
-            colon_token: Default::default(),
-            ty: Box::new(syn::Type::Reference(syn::TypeReference {
-                and_token: Default::default(),
-                lifetime: None,
-                mutability: None,
-                elem: Box::new(return_type),
-            })),
-        });
-    }
-    closure
-}

crates/anodized-core/src/instrument/fns_tests.rs

@@ -22,7 +22,7 @@ fn embed_spec_item_fn() {
         #[cfg(META_3)]
         ensures: [
             COND_8,
-            |PAT_2| COND_9,
+            |PAT_2: TYPE| COND_9,
         ],
     };
     let item_fn: ItemFn = parse_quote! {
@@ -59,7 +59,7 @@ fn embed_spec_item_fn() {
             let (ALIAS_1, (ALIAS_2, ALIAS_3)) = ((| | EXPR_1)(), (| | EXPR_2)());
             let _ = |PAT_1: &RET_TYPE| -> bool { COND_7 };
             let _ = |PAT_1: &RET_TYPE| -> bool { COND_8 };
-            let _ = |PAT_2: &RET_TYPE| -> bool { COND_9 };
+            let _ = |PAT_2: TYPE| -> bool { COND_9 };
         }
 
         fn FUNC(&self, PARAM_1: TYPE_1, PARAM_2: TYPE_2) -> RET_TYPE {
@@ -87,7 +87,7 @@ fn embed_spec_item_fn() {
                     & (|| -> bool { COND_6 })()
                     & (|PAT_1: &RET_TYPE| -> bool { COND_7 })(&__anodized_output)
                     & (|PAT_1: &RET_TYPE| -> bool { COND_8 })(&__anodized_output)
-                    & (|PAT_2: &RET_TYPE| -> bool { COND_9 })(&__anodized_output);
+                    & (|PAT_2: TYPE| -> bool { COND_9 })(&__anodized_output);
                 if !__anodized_postcond {}
             }
             __anodized_output