Also track arguments of sub-contracts

src/transformations.rs

@@ -224,7 +224,7 @@ pub mod import_resolution {
 /// value is unwrapped.
 pub mod apply_contracts {
     use super::{RichTerm, Term};
-    use crate::term::make as mk_term;
+    use crate::mk_app;
 
     /// If the top-level node of the AST is a meta-value, wrap the inner value inside generated
     /// `Assume`s corresponding to the meta-value's contracts. Otherwise, return the term
@@ -237,7 +237,12 @@ pub mod apply_contracts {
                 let inner = meta.types.iter().chain(meta.contracts.iter()).fold(
                     meta.value.take().unwrap(),
                     |acc, ctr| {
-                        mk_term::assume(ctr.types.clone(), ctr.label.clone(), acc).with_pos(pos)
+                        mk_app!(
+                            ctr.types.clone().contract(),
+                            Term::Lbl(ctr.label.clone()),
+                            acc
+                        )
+                        .with_pos(pos)
                     },
                 );
 
@@ -317,7 +322,7 @@ where
 }
 
 /// Generate a new fresh variable which do not clash with user-defined variables.
-fn fresh_var() -> Ident {
+pub fn fresh_var() -> Ident {
     Ident(format!("%{}", FreshVarCounter::next()))
 }
 

src/types.rs

@@ -179,8 +179,9 @@ impl Types {
         sy: &mut i32,
     ) -> RichTerm {
         use crate::stdlib::contracts;
+        use crate::transformations::fresh_var;
 
-        match self.0 {
+        let ctr = match self.0 {
             AbsType::Dyn() => contracts::dynamic(),
             AbsType::Num() => contracts::num(),
             AbsType::Bool() => contracts::bool(),
@@ -292,7 +293,24 @@ impl Types {
             AbsType::DynRecord(ref ty) => {
                 mk_app!(contracts::dyn_record(), ty.contract_open(h, pol, sy))
             }
-        }
+        };
+
+        // To track the argument to contracts, we need to wrap the function contracts as an
+        // `Assume`. Since `Assume` is strict in the label and need to be fully applied, we need
+        // to wrap this assume back as a standard function, that is to form:
+        // `fun l val => %assume% ctr l val`
+        let var_l = fresh_var();
+        let var_val = fresh_var();
+        let pos = ctr.pos;
+        mk_fun!(
+            var_l.clone(),
+            var_val.clone(),
+            mk_app!(
+                mk_term::op2(BinaryOp::Assume(), ctr, Term::Var(var_l)),
+                Term::Var(var_val)
+            )
+        )
+        .with_pos(pos.into_inherited())
     }
 
     /// Find a binding in a record row type. Return `None` if there is no such binding, if the type