Repository: tweag/nickel
Pull request #809 (2022-08-29 14:59:09)

Merge lazy array contracts
Since the time the `topic/lazy-array-contracts` branch was finalized, master has diverged quite a bit and it's time merge it in finally. 

Let's also use this chance to pick up on any issues that might've been missed before.

yannham: @fuzzypixelz maybe you've noticed, but there are conflicts to solve before being able to give it a review.

Patch:
diff --git a/src/eval/merge.rs b/src/eval/merge.rs
index 3437635d..16422ddd 100644
--- a/src/eval/merge.rs
+++ b/src/eval/merge.rs
@@ -228,7 +228,7 @@ pub fn merge(
             if arr1.is_empty() && arr2.is_empty() =>
         {
             Ok(Closure::atomic_closure(RichTerm::new(
-                Term::Array(arr1, ArrayAttrs { closurized: true }),
+                Term::Array(arr1, ArrayAttrs::new().closurized()),
                 pos_op.into_inherited(),
             )))
         }
diff --git a/src/eval/mod.rs b/src/eval/mod.rs
index f1ed62e4..9643236f 100644
--- a/src/eval/mod.rs
+++ b/src/eval/mod.rs
@@ -93,10 +93,10 @@ use crate::{
     environment::Environment as GenericEnvironment,
     error::EvalError,
     identifier::Ident,
-    match_sharedterm, mk_app,
+    match_sharedterm,
     term::{
-        make as mk_term, ArrayAttrs, BinaryOp, BindingType, LetAttrs, MetaValue, RichTerm,
-        SharedTerm, StrChunk, Term, UnaryOp,
+        make as mk_term, ArrayAttrs, BinaryOp, BindingType, LetAttrs, MetaValue, PendingContract,
+        RichTerm, SharedTerm, StrChunk, Term, UnaryOp,
     },
     transform::Closurizable,
 };
@@ -216,25 +216,14 @@ where
 }
 
 fn eval_deep_closure<R>(
-    t0: RichTerm,
+    rt: RichTerm,
     initial_env: &Environment,
     resolver: &mut R,
 ) -> Result<(RichTerm, Environment), EvalError>
 where
     R: ImportResolver,
 {
-    use crate::transform::fresh_var;
-
-    let var = fresh_var();
-    // Desugar to let x = term in %deep_seq% x x
-    let wrapper = mk_term::let_in(
-        var.clone(),
-        t0,
-        mk_app!(
-            mk_term::op1(UnaryOp::DeepSeq(None), Term::Var(var.clone())),
-            Term::Var(var)
-        ),
-    );
+    let wrapper = mk_term::op1(UnaryOp::Force(None), rt);
     eval_closure(
         Closure::atomic_closure(wrapper),
         initial_env,
@@ -459,7 +448,7 @@ where
                 // Special casing (hopefully temporary) due to the need for `DeepSeq` to produce
                 // acceptable error message for missing field definition occurring when sequencing
                 // a record. See the definition of `UnaryOp::DeepSeq`.
-                if let UnaryOp::DeepSeq(Some(stack_elem)) = op {
+                if let UnaryOp::DeepSeq(Some(stack_elem)) | UnaryOp::Force(Some(stack_elem)) = op {
                     call_stack.0.push(stack_elem.clone());
                 }
 
@@ -656,9 +645,27 @@ where
                     .iter()
                     .map(|t| t.clone().closurize(&mut local_env, env.clone()))
                     .collect();
+
+                let closurized_ctrs = attrs
+                    .pending_contracts
+                    .iter()
+                    .map(|ctr| {
+                        PendingContract::new(
+                            ctr.contract.clone().closurize(&mut local_env, env.clone()),
+                            ctr.label.clone(),
+                        )
+                    })
+                    .collect();
+
                 Closure {
                     body: RichTerm::new(
-                        Term::Array(closurized_array, ArrayAttrs { closurized: true }),
+                        Term::Array(
+                            closurized_array,
+                            ArrayAttrs {
+                                closurized: true,
+                                pending_contracts: closurized_ctrs,
+                            },
+                        ),
                         pos,
                     ),
                     env: local_env,
diff --git a/src/eval/operation.rs b/src/eval/operation.rs
index 6cb248e7..7747d415 100644
--- a/src/eval/operation.rs
+++ b/src/eval/operation.rs
@@ -21,12 +21,13 @@ use crate::{
     position::TermPos,
     serialize,
     serialize::ExportFormat,
-    term::{make as mk_term, ArrayAttrs},
-    term::{BinaryOp, NAryOp, RichTerm, StrChunk, Term, UnaryOp},
-    transform::{fresh_var, Closurizable},
+    term::{make as mk_term, PendingContract},
+    term::{ArrayAttrs, BinaryOp, NAryOp, RichTerm, StrChunk, Term, UnaryOp},
+    transform::{apply_contracts::apply_contracts, fresh_var, Closurizable},
 };
 use md5::digest::Digest;
 use simple_counter::*;
+use std::collections::HashMap;
 use std::iter::Extend;
 
 generate_counter!(FreshVariableCounter, usize);
@@ -472,7 +473,7 @@ fn process_unary_operation(
                     fields.sort();
                     let terms = fields.into_iter().map(mk_term::string).collect();
                     Ok(Closure::atomic_closure(RichTerm::new(
-                        Term::Array(terms, ArrayAttrs { closurized: true }),
+                        Term::Array(terms, ArrayAttrs::new().closurized()),
                         pos_op_inh,
                     )))
                 }
@@ -520,7 +521,7 @@ fn process_unary_operation(
                 .pop_arg()
                 .ok_or_else(|| EvalError::NotEnoughArgs(2, String::from("map"), pos_op))?;
             match_sharedterm! {t, with {
-                    Term::Array(ts, _) => {
+                    Term::Array(ts, attrs) => {
                         let mut shared_env = Environment::new();
                         let f_as_var = f.body.closurize(&mut env, f.env);
 
@@ -530,13 +531,19 @@ fn process_unary_operation(
                         let ts = ts
                             .into_iter()
                             .map(|t| {
-                                RichTerm::new(Term::App(f_as_var.clone(), t), pos_op_inh)
+                                let t_with_ctrs = apply_contracts(
+                                    t,
+                                    attrs.pending_contracts.iter().cloned(),
+                                    pos.into_inherited(),
+                                );
+
+                                RichTerm::new(Term::App(f_as_var.clone(), t_with_ctrs), pos_op_inh)
                                     .closurize(&mut shared_env, env.clone())
                             })
                             .collect();
 
                         Ok(Closure {
-                            body: RichTerm::new(Term::Array(ts, ArrayAttrs { closurized: true }), pos_op_inh),
+                            body: RichTerm::new(Term::Array(ts, attrs.contracts_cleared().closurized()), pos_op_inh),
                             env: shared_env,
                         })
                     }
@@ -581,7 +588,7 @@ fn process_unary_operation(
 
                     Ok(Closure {
                         body: RichTerm::new(
-                            Term::Array(ts, ArrayAttrs { closurized: true }),
+                            Term::Array(ts, ArrayAttrs::new().closurized()),
                             pos_op_inh,
                         ),
                         env: shared_env,
@@ -645,28 +652,27 @@ fn process_unary_operation(
             }
         }
         UnaryOp::DeepSeq(_) => {
-            /// Build a closure that forces a given list of terms, and at the end resumes the
+            /// Build a RichTerm that forces a given list of terms, and at the end resumes the
             /// evaluation of the argument on the top of the stack. The argument must iterate over
             /// a tuple, which first element is an optional call stack element to add to the
             /// callstack before starting evaluation. This is a temporary fix to have reasonable
             /// missing definition error when deepsequing a record.
             ///
             /// Requires its first argument to be non-empty.
-            fn seq_terms<I>(mut it: I, env: Environment, pos_op_inh: TermPos) -> Closure
+            fn seq_terms<I>(mut it: I, pos_op_inh: TermPos) -> RichTerm
             where
                 I: Iterator<Item = (Option<callstack::StackElem>, RichTerm)>,
             {
                 let (first_elem, first) = it
                     .next()
                     .expect("expected the argument to be a non-empty iterator");
-                let body = it.fold(
+
+                it.fold(
                     mk_term::op1(UnaryOp::DeepSeq(first_elem), first).with_pos(pos_op_inh),
                     |acc, (elem, t)| {
                         mk_app!(mk_term::op1(UnaryOp::DeepSeq(elem), t), acc).with_pos(pos_op_inh)
                     },
-                );
-
-                Closure { body, env }
+                )
             }
 
             match t.into_owned() {
@@ -688,10 +694,30 @@ fn process_unary_operation(
                                 t,
                             )
                         });
-                    Ok(seq_terms(terms, env.clone(), pos_op))
+                    Ok(Closure {
+                        body: seq_terms(terms, pos_op),
+                        env,
+                    })
                 }
-                Term::Array(ts, _) if !ts.is_empty() => {
-                    Ok(seq_terms(ts.into_iter().map(|t| (None, t)), env, pos_op))
+                Term::Array(ts, attrs) if !ts.is_empty() => {
+                    let mut shared_env = Environment::new();
+                    let terms = seq_terms(
+                        ts.into_iter().map(|t| {
+                            let t_with_ctr = apply_contracts(
+                                t,
+                                attrs.pending_contracts.iter().cloned(),
+                                pos.into_inherited(),
+                            )
+                            .closurize(&mut shared_env, env.clone());
+                            (None, t_with_ctr)
+                        }),
+                        pos_op,
+                    );
+
+                    Ok(Closure {
+                        body: terms,
+                        env: shared_env,
+                    })
                 }
                 _ => {
                     if let Some((next, ..)) = stack.pop_arg() {
@@ -703,10 +729,16 @@ fn process_unary_operation(
             }
         }
         UnaryOp::ArrayHead() => {
-            if let Term::Array(ts, _) = &*t {
+            if let Term::Array(ts, attrs) = &*t {
                 if let Some(head) = ts.first() {
+                    let head_with_ctr = apply_contracts(
+                        head.clone(),
+                        attrs.pending_contracts.iter().cloned(),
+                        pos.into_inherited(),
+                    );
+
                     Ok(Closure {
-                        body: head.clone(),
+                        body: head_with_ctr,
                         env,
                     })
                 } else {
@@ -827,7 +859,7 @@ fn process_unary_operation(
                     .map(|c| RichTerm::from(Term::Str(c.to_string())))
                     .collect();
                 Ok(Closure::atomic_closure(RichTerm::new(
-                    Term::Array(ts, ArrayAttrs { closurized: true }),
+                    Term::Array(ts, ArrayAttrs::new().closurized()),
                     pos_op_inh,
                 )))
             } else {
@@ -1071,7 +1103,7 @@ fn process_unary_operation(
                         ("index", Term::Num(first_match.start() as f64)),
                         (
                             "groups",
-                            Term::Array(groups, ArrayAttrs { closurized: true })
+                            Term::Array(groups, ArrayAttrs::new().closurized())
                         )
                     )
                 } else {
@@ -1093,6 +1125,87 @@ fn process_unary_operation(
                 ))
             }
         }
+        UnaryOp::Force(_) => {
+            /// `Seq` the `terms` iterator and then resume evaluating the `cont` continuation.
+            fn seq_terms<I>(terms: I, pos: TermPos, cont: RichTerm) -> RichTerm
+            where
+                I: Iterator<Item = RichTerm>,
+            {
+                terms
+                    .fold(cont, |acc, t| mk_app!(mk_term::op1(UnaryOp::Seq(), t), acc))
+                    .with_pos(pos)
+            }
+
+            match_sharedterm! {t,
+                with {
+                    Term::Record(map, attrs) if !map.is_empty() => {
+                        let mut shared_env = Environment::new();
+
+                        let map = map
+                            .into_iter()
+                            // We ignore empty optional fields
+                            .filter(|(_, t)| !is_empty_optional(t, &env))
+                            .map(|(id, t)| {
+                                let stack_elem = Some(callstack::StackElem::Field {
+                                    id: id.clone(),
+                                    pos_record: pos,
+                                    pos_field: t.pos,
+                                    pos_access: pos_op,
+                                });
+
+                                (
+                                    id,
+                                    mk_term::op1(UnaryOp::Force(stack_elem), t)
+                                        .closurize(&mut shared_env, env.clone()),
+                                )
+                            })
+                            // It's important to collect here, otherwise the two usages below
+                            // will each do their own .closurize(...) calls and end up with
+                            // different variables, which means that `cont` won't be properly updated.
+                            .collect::<HashMap<_, _>>();
+
+                        let terms = map.clone().into_values();
+                        let cont = RichTerm::new(Term::Record(map, attrs), pos.into_inherited());
+
+                        Ok(Closure {
+                            body: seq_terms(terms, pos_op, cont),
+                            env: shared_env,
+                        })
+                    },
+                    Term::Array(ts, attrs) if !ts.is_empty() => {
+                        let mut shared_env = Environment::new();
+                        let ts = ts
+                            .into_iter()
+                            .map(|t| {
+                                mk_term::op1(
+                                    UnaryOp::Force(None),
+                                    apply_contracts(
+                                        t,
+                                        attrs.pending_contracts.iter().cloned(),
+                                        pos.into_inherited(),
+                                    ),
+                                )
+                                .closurize(&mut shared_env, env.clone())
+                            })
+                            // It's important to collect here, otherwise the two usages below
+                            // will each do their own .closurize(...) calls and end up with
+                            // different variables, which means that `cont` won't be properly updated.
+                            .collect::<Vec<_>>();
+
+                        let terms = ts.clone().into_iter();
+                        let cont = RichTerm::new(Term::Array(ts, attrs), pos.into_inherited());
+
+                        Ok(Closure {
+                            body: seq_terms(terms, pos_op, cont),
+                            env: shared_env,
+                        })
+                    }
+                } else Ok(Closure {
+                    body: RichTerm { term : t, pos},
+                    env
+                })
+            }
+        }
     }
 }
 
@@ -1878,8 +1991,10 @@ fn process_binary_operation(
                 ))
             }
         },
-        BinaryOp::ArrayConcat() => match_sharedterm! {t1, with {
-                Term::Array(ts1, attrs1) => match_sharedterm! {t2, with {
+        BinaryOp::ArrayConcat() => match_sharedterm! {t1,
+            with {
+                Term::Array(ts1, attrs1) => match_sharedterm! {t2,
+                    with {
                         Term::Array(ts2, attrs2) => {
                             // NOTE: the [eval_closure] function in [eval] should've made sure
                             // that the array is closurized. We leave a debug_assert! here just
@@ -1890,15 +2005,45 @@ fn process_binary_operation(
 
                             let mut ts: Vec<RichTerm> = Vec::with_capacity(ts1.len() + ts2.len());
 
-                            ts.extend(ts1.into_iter());
-                            ts.extend(ts2.into_iter());
-
-                            let mut env = env1;
+                            let mut env = env1.clone();
                             // TODO: Is there a cheaper way to "merge" two environements?
                             env.extend(env2.iter_elems().map(|(k, v)| (k.clone(), v.clone())));
 
+                            // We have two sets of contracts from the LHS and RHS arrays.
+                            // - Common contracts between the two sides can be put into
+                            // `pending_contracts` of the resulting concatenation as they're
+                            // shared by all elements: we don't have to apply them just yet.
+                            // - Contracts thats are specific to the LHS or the RHS have to
+                            // applied because we don't have a way of tracking which elements
+                            // should take which contracts.
+
+                            let (ctrs_left, ctrs_common) : (Vec<_>, Vec<_>) = attrs1
+                                .pending_contracts
+                                .into_iter()
+                                .partition(|ctr| !attrs2.pending_contracts.contains(ctr));
+
+                            let ctrs_right = attrs2
+                                .pending_contracts
+                                .into_iter()
+                                .filter(|ctr| !ctrs_left.contains(ctr) && !ctrs_common.contains(ctr));
+
+                            ts.extend(ts1.into_iter().map(|t|
+                                apply_contracts(t, ctrs_left.iter().cloned(), pos1)
+                                .closurize(&mut env, env1.clone())
+                            ));
+
+                            ts.extend(ts2.into_iter().map(|t|
+                                apply_contracts(t, ctrs_right.clone(), pos2)
+                                .closurize(&mut env, env2.clone())
+                            ));
+
+                            let attrs = ArrayAttrs {
+                                closurized: true,
+                                pending_contracts: ctrs_common,
+                            };
+
                             Ok(Closure {
-                                body: RichTerm::new(Term::Array(ts, ArrayAttrs { closurized: true }), pos_op_inh),
+                                body: RichTerm::new(Term::Array(ts, attrs), pos_op_inh),
                                 env,
                             })
                         }
@@ -1928,15 +2073,20 @@ fn process_binary_operation(
             }
         },
         BinaryOp::ArrayElemAt() => match (&*t1, &*t2) {
-            (Term::Array(ts, _), Term::Num(n)) => {
+            (Term::Array(ts, attrs), Term::Num(n)) => {
                 let n_int = *n as usize;
                 if n.fract() != 0.0 {
                     Err(EvalError::Other(format!("elemAt: expected the 2nd agument to be an integer, got the floating-point value {}", n), pos_op))
                 } else if *n < 0.0 || n_int >= ts.len() {
                     Err(EvalError::Other(format!("elemAt: index out of bounds. Expected a value between 0 and {}, got {}", ts.len(), n), pos_op))
                 } else {
+                    let elem_with_ctr = apply_contracts(
+                        ts[n_int].clone(),
+                        attrs.pending_contracts.iter().cloned(),
+                        pos1.into_inherited(),
+                    );
                     Ok(Closure {
-                        body: ts[n_int].clone(),
+                        body: elem_with_ctr,
                         env: env1,
                     })
                 }
@@ -2138,7 +2288,7 @@ fn process_binary_operation(
                     .map(|s| Term::Str(String::from(s)).into())
                     .collect();
                 Ok(Closure::atomic_closure(RichTerm::new(
-                    Term::Array(array, ArrayAttrs { closurized: true }),
+                    Term::Array(array, ArrayAttrs::new().closurized()),
                     pos_op_inh,
                 )))
             }
@@ -2185,6 +2335,57 @@ fn process_binary_operation(
                 },
             )),
         },
+        BinaryOp::ArrayLazyAssume() => {
+            let (ctr, _) = stack.pop_arg().ok_or_else(|| {
+                EvalError::NotEnoughArgs(3, String::from("arrayLazyAssume"), pos_op)
+            })?;
+
+            let Closure {
+                body: rt3,
+                env: env3,
+            } = ctr;
+
+            // FIXME: use match?
+            let lbl = match_sharedterm! {t1, with {
+                    Term::Lbl(lbl) => lbl
+                } else return Err(EvalError::TypeError(
+                    String::from("Lbl"),
+                    String::from("arrayLazyAssume, 2nd argument"),
+                    fst_pos,
+                    RichTerm {
+                        term: t2,
+                        pos: pos2,
+                    },
+                ))
+            };
+
+            match_sharedterm! {t2,
+                with {
+                    Term::Array(ts, attrs) => {
+                        // Preserve the environment of the contract in the resulting array.
+                        let rt3 = rt3.closurize(&mut env2, env3);
+
+                        let array_with_ctr = Closure {
+                            body: RichTerm::new(
+                                Term::Array(ts, attrs.with_extra_contracts([PendingContract::new(rt3, lbl)])),
+                                pos2,
+                            ),
+                            env: env2,
+                        };
+
+                        Ok(array_with_ctr)
+                    }
+                } else Err(EvalError::TypeError(
+                    String::from("Array"),
+                    String::from("arrayLazyAssume, 2nd argument"),
+                    snd_pos,
+                    RichTerm {
+                        term: t2,
+                        pos: pos2,
+                    },
+                ))
+            }
+        }
     }
 }
 
@@ -2453,11 +2654,55 @@ fn eq(env: &mut Environment, c1: Closure, c2: Closure) -> EqResult {
                 gen_eqs(eqs, env, env1, env2)
             }
         }
-        (Term::Array(l1, _), Term::Array(l2, _)) if l1.len() == l2.len() => {
+        (Term::Array(l1, a1), Term::Array(l2, a2)) if l1.len() == l2.len() => {
             // Equalities are tested in reverse order, but that shouldn't matter. If it
             // does, just do `eqs.rev()`
-            let eqs = l1.into_iter().zip(l2.into_iter());
-            gen_eqs(eqs, env, env1, env2)
+
+            // We should apply all contracts here, otheriwse we risk having wrong values,
+            // think record contrats with default contracts, wrapped terms, etc.
+            let mut shared_env1 = env1.clone();
+            let mut shared_env2 = env2.clone();
+
+            let mut eqs = l1
+                .into_iter()
+                .map(|t| {
+                    let pos = t.pos.into_inherited();
+                    apply_contracts(t, a1.pending_contracts.iter().cloned(), pos)
+                        .closurize(&mut shared_env1, env1.clone())
+                })
+                .zip(l2.into_iter().map(|t| {
+                    let pos = t.pos.into_inherited();
+                    apply_contracts(t, a2.pending_contracts.iter().cloned(), pos)
+                        .closurize(&mut shared_env2, env2.clone())
+                }))
+                .collect::<Vec<_>>();
+
+            match eqs.pop() {
+                None => EqResult::Bool(true),
+                Some((t1, t2)) => {
+                    let eqs = eqs
+                        .into_iter()
+                        .map(|(t1, t2)| {
+                            (
+                                Closure {
+                                    body: t1,
+                                    env: shared_env1.clone(),
+                                },
+                                Closure {
+                                    body: t2,
+                                    env: shared_env2.clone(),
+                                },
+                            )
+                        })
+                        .collect::<Vec<_>>();
+
+                    EqResult::Eqs(
+                        t1.closurize(env, shared_env1),
+                        t2.closurize(env, shared_env2),
+                        eqs,
+                    )
+                }
+            }
         }
         (_, _) => EqResult::Bool(false),
     }
diff --git a/src/parser/grammar.lalrpop b/src/parser/grammar.lalrpop
index 76597bcf..8decf3f6 100644
--- a/src/parser/grammar.lalrpop
+++ b/src/parser/grammar.lalrpop
@@ -532,6 +532,7 @@ UOp: UnaryOp = {
     "record_map" => UnaryOp::RecordMap(),
     "seq" => UnaryOp::Seq(),
     "deep_seq" => UnaryOp::DeepSeq(None),
+    "force" => UnaryOp::Force(None),
     "head" => UnaryOp::ArrayHead(),
     "tail" => UnaryOp::ArrayTail(),
     "length" => UnaryOp::ArrayLength(),
@@ -715,6 +716,7 @@ InfixExpr: UniTerm = {
 
 BOpPre: BinaryOp = {
     "assume" => BinaryOp::Assume(),
+    "array_lazy_assume" => BinaryOp::ArrayLazyAssume(),
     "unseal" => BinaryOp::Unseal(),
     "seal" => BinaryOp::Seal(),
     "go_field" => BinaryOp::GoField(),
@@ -846,6 +848,8 @@ extern {
         "tag" => Token::Normal(NormalToken::Tag),
         "typeof" => Token::Normal(NormalToken::Typeof),
         "assume" => Token::Normal(NormalToken::Assume),
+        "array_lazy_assume" => Token::Normal(NormalToken::ArrayLazyAssume),
+        "force" => Token::Normal(NormalToken::Force),
         "blame" => Token::Normal(NormalToken::Blame),
         "chng_pol" => Token::Normal(NormalToken::ChangePol),
         "polarity" => Token::Normal(NormalToken::Polarity),
diff --git a/src/parser/lexer.rs b/src/parser/lexer.rs
index 017b2dde..9dc25a83 100644
--- a/src/parser/lexer.rs
+++ b/src/parser/lexer.rs
@@ -152,6 +152,8 @@ pub enum NormalToken<'input> {
 
     #[token("%assume%")]
     Assume,
+    #[token("%array_lazy_assume%")]
+    ArrayLazyAssume,
     #[token("%blame%")]
     Blame,
     #[token("%chng_pol%")]
@@ -183,6 +185,8 @@ pub enum NormalToken<'input> {
     Seq,
     #[token("%deep_seq%")]
     DeepSeq,
+    #[token("%force%")]
+    Force,
     #[token("%head%")]
     Head,
     #[token("%tail%")]
diff --git a/src/pretty.rs b/src/pretty.rs
index 1ac7f9ac..4528d684 100644
--- a/src/pretty.rs
+++ b/src/pretty.rs
@@ -684,9 +684,7 @@ where
                 .append(allocator.space())
                 .append(allocator.as_string(f.to_string_lossy()).double_quotes()),
             ResolvedImport(id) => allocator.text(format!("import <file_id: {:?}>", id)),
-            ParseError(_) => allocator
-                .text("#<PARSE ERROR!>")
-                .append(allocator.hardline()),
+            ParseError(_) => allocator.text("#<PARSE ERROR!>"),
         }
     }
 }
diff --git a/src/term.rs b/src/term.rs
index 44dc38b9..5f98a5bc 100644
--- a/src/term.rs
+++ b/src/term.rs
@@ -186,14 +186,70 @@ impl Default for BindingType {
     }
 }
 
+/// A contract with its associated data.
+#[derive(Debug, PartialEq, Clone)]
+pub struct PendingContract {
+    /// The pending contract, can be a function or a record.
+    pub contract: RichTerm,
+    /// The blame label.
+    pub label: Label,
+}
+
+impl PendingContract {
+    pub fn new(contract: RichTerm, label: Label) -> Self {
+        PendingContract { contract, label }
+    }
+}
+
 /// The attributes of an Array.
-#[derive(Debug, Default, Eq, PartialEq, Copy, Clone)]
+#[derive(Debug, Default, PartialEq, Clone)]
 pub struct ArrayAttrs {
     /// A `closurized` array verifies the following conditions:
     ///   - Each element is a generated variable with a unique name (although the same
     ///     variable can occur in several places, it should always refer to the same thunk anyway).
     ///   - The environment of the array's closure only contains those generated variables.
     pub closurized: bool,
+    /// List of lazily-applied contracts.
+    /// These are only observed when data enters or leaves the array.
+    pub pending_contracts: Vec<PendingContract>,
+}
+
+impl ArrayAttrs {
+    /// Create an `ArrayAttrs`.
+    /// By default, the `closurized` flag is set to `false`,
+    /// and `pending_contracts` is empty.
+    pub fn new() -> Self {
+        Default::default()
+    }
+
+    /// Set the `closurized` flag to `true`.
+    pub fn closurized(mut self) -> Self {
+        self.closurized = true;
+        self
+    }
+
+    /// Drop the pending contracts.
+    pub fn contracts_cleared(mut self) -> Self {
+        self.pending_contracts.clear();
+        self
+    }
+
+    /// Extend contracts from an iterator of `PendingContract`.
+    /// De-duplicate equal contracts. Note that current contract
+    /// equality testing is very limited, but this may change in the
+    /// future
+    pub fn with_extra_contracts<I>(mut self, iter: I) -> Self
+    where
+        I: IntoIterator<Item = PendingContract>,
+    {
+        for ctr in iter {
+            if !self.pending_contracts.contains(&ctr) {
+                self.pending_contracts.push(ctr)
+            }
+        }
+
+        self
+    }
 }
 
 #[derive(Debug, Default, Eq, PartialEq, Copy, Clone)]
@@ -837,6 +893,23 @@ pub enum UnaryOp {
     StrIsMatchCompiled(CompiledRegex),
     /// Version of [`UnaryOp::StrMatch`] which remembers the compiled regex.
     StrMatchCompiled(CompiledRegex),
+    /// Force full evaluation of a term and return it.
+    ///
+    /// This was added in the context of [`BinaryOp::ArrayLazyAssume`],
+    /// in particular to make serialization work with lazy array contracts.
+    ///
+    /// # `Force` vs. `DeepSeq`
+    ///
+    /// [`UnaryOp::Force`] updates the thunks containing arrays with a new version where the lazy contracts have all been applied,
+    /// whereas [`UnaryOp::DeepSeq`] evaluates the same expressions, but it never updates the thunk of an array with lazy contracts
+    /// with an array where those contracts have been applied. In a way, the result of lazy contract application in arrays is "lost"
+    /// in [`UnaryOp::DeepSeq`], while it's returned in [`UnaryOp::Force`].
+    ///
+    /// This means we can observe different results between `deep_seq x x` and `force x`, in some cases.
+    ///
+    /// It's also worth noting that [`UnaryOp::DeepSeq`] should be, in principle, more efficient that [`UnaryOp::Force`]
+    /// as it does less cloning.
+    Force(Option<crate::eval::callstack::StackElem>),
 }
 
 // See: https://github.com/rust-lang/regex/issues/178
@@ -962,6 +1035,10 @@ pub enum BinaryOp {
     StrContains(),
     /// Seal a term with a sealing key (see [`Term::Sealed`]).
     Seal(),
+
+    /// Lazily apply a contract to an Array.
+    /// This simply inserts a contract into the array attributes.
+    ArrayLazyAssume(),
 }
 
 impl BinaryOp {
diff --git a/src/transform/apply_contracts.rs b/src/transform/apply_contracts.rs
index b4162d36..a80de31d 100644
--- a/src/transform/apply_contracts.rs
+++ b/src/transform/apply_contracts.rs
@@ -10,7 +10,8 @@
 //! value is unwrapped.
 use crate::{
     match_sharedterm, mk_app,
-    term::{make as mk_term, BinaryOp, RichTerm, Term},
+    position::TermPos,
+    term::{make as mk_term, BinaryOp, PendingContract, RichTerm, Term},
     types::UnboundTypeVariableError,
 };
 
@@ -24,21 +25,15 @@ pub fn transform_one(rt: RichTerm) -> Result<RichTerm, UnboundTypeVariableError>
             Term::MetaValue(meta) if meta.value.is_some() => {
                 let mut meta = meta;
                 let pos_inh = pos.into_inherited();
-                let inner = meta.types.iter().chain(meta.contracts.iter()).try_fold(
-                    meta.value.take().unwrap(),
-                    |acc, ctr| {
-                        Ok(mk_app!(
-                            mk_term::op2(
-                                BinaryOp::Assume(),
-                                ctr.types.contract()?,
-                                Term::Lbl(ctr.label.clone())
-                            )
-                            .with_pos(pos_inh),
-                            acc
-                        )
-                        .with_pos(pos_inh))
-                    },
-                )?;
+
+                let ctrs = meta
+                    .types
+                    .iter()
+                    .chain(meta.contracts.iter())
+                    .map(|ctr| Ok(PendingContract::new(ctr.types.contract()?, ctr.label.clone())))
+                    .collect::<Result<Vec<_>, _>>()?;
+
+                let inner = apply_contracts(meta.value.take().unwrap(), ctrs.into_iter(), pos_inh);
 
                 meta.value.replace(inner);
                 RichTerm::new(Term::MetaValue(meta), pos)
@@ -47,3 +42,16 @@ pub fn transform_one(rt: RichTerm) -> Result<RichTerm, UnboundTypeVariableError>
     };
     Ok(result)
 }
+
+pub fn apply_contracts<I>(rt: RichTerm, contracts: I, pos: TermPos) -> RichTerm
+where
+    I: Iterator<Item = PendingContract>,
+{
+    contracts.fold(rt, |acc, ctr| {
+        mk_app!(
+            mk_term::op2(BinaryOp::Assume(), ctr.contract, Term::Lbl(ctr.label)).with_pos(pos),
+            acc
+        )
+        .with_pos(pos)
+    })
+}
diff --git a/src/typecheck/operation.rs b/src/typecheck/operation.rs
index b8a382b3..7d239a09 100644
--- a/src/typecheck/operation.rs
+++ b/src/typecheck/operation.rs
@@ -190,6 +190,8 @@ pub fn get_uop_type(
                 ("groups", mk_typewrapper::array(AbsType::Str()))
             ),
         ),
+        // Dyn -> Dyn
+        UnaryOp::Force(_) => (mk_typewrapper::dynamic(), mk_typewrapper::dynamic()),
     })
 }
 
@@ -358,6 +360,17 @@ pub fn get_bop_type(
             mk_typewrapper::str(),
             mk_typewrapper::array(AbsType::Str()),
         ),
+        // The first argument is a contract, the second is a label.
+        // forall a. Dyn -> Dyn -> Array a -> Array a
+        BinaryOp::ArrayLazyAssume() => {
+            let ty_elt = TypeWrapper::Ptr(state.table.fresh_var());
+            let ty_array = mk_typewrapper::array(ty_elt);
+            (
+                mk_typewrapper::dynamic(),
+                mk_typewrapper::dynamic(),
+                mk_tyw_arrow!(ty_array.clone(), ty_array),
+            )
+        }
     })
 }
 
diff --git a/stdlib/builtin.ncl b/stdlib/builtin.ncl
index 0cd9150f..3090a88c 100644
--- a/stdlib/builtin.ncl
+++ b/stdlib/builtin.ncl
@@ -180,7 +180,7 @@
           }"
       ```
       "%m
-    = fun format x => %serialize% format (%deep_seq% x x),
+    = fun format x => %serialize% format (%force% x),
 
     deserialize : [| `Json, `Toml, `Yaml |] -> Str -> Dyn
     | doc m%"
diff --git a/stdlib/contract.ncl b/stdlib/contract.ncl
index aeb98fcb..dc31920c 100644
--- a/stdlib/contract.ncl
+++ b/stdlib/contract.ncl
@@ -11,8 +11,9 @@
 
   "$array" = fun elt l t =>
     if %typeof% t == `Array then
-      %map% t (fun value => %assume% elt (%go_array% l) value)
-    else %blame% l,
+        %array_lazy_assume% (%go_array% l) t elt
+    else
+        %blame% l,
 
   "$func" = fun s t l e =>
       if %typeof% e == `Fun then


Test patch:
diff --git a/tests/contracts_fail.rs b/tests/contracts_fail.rs
index ea200921..c98b5a8c 100644
--- a/tests/contracts_fail.rs
+++ b/tests/contracts_fail.rs
@@ -137,7 +137,7 @@ fn lists_contracts() {
     use nickel_lang::label::ty_path::Elem;
 
     assert_matches!(
-        eval("%deep_seq% ([1, \"a\"] | Array Num) 0"),
+        eval("%force% ([1, \"a\"] | Array Num) 0"),
         Err(Error::EvalError(EvalError::BlameError(..)))
     );
     assert_matches!(
@@ -149,7 +149,7 @@ fn lists_contracts() {
         Err(Error::EvalError(EvalError::BlameError(..)))
     );
 
-    let res = eval("%deep_seq% ([{a = [1]}] | Array {a: Array Str}) false");
+    let res = eval("%force% ([{a = [1]}] | Array {a: Array Str}) false");
     match &res {
         Err(Error::EvalError(EvalError::BlameError(ref l, _))) => {
             assert_matches!(l.path.as_slice(), [Elem::Array, Elem::Field(id), Elem::Array] if &id.to_string() == "a")