Implement the record_lazy_assume primop

The contract.Equal requires a new primop, akin to the existing
array_lazy_assume, which adds a contract to the `pending_contracts` of
each field of a record. This primop also reverts recursive records, as
this new contract may alter fields, and thus trigger a recomputation of
the recursive record's fixpoint.

Doing so, we got rid of the `dictionary_assume` contract, which can be
subsumed (more easily and more efficiently!) by this new primop.

src/eval/fixpoint.rs

@@ -1,5 +1,5 @@
 //! Compute the fixpoint of a recursive record.
-use super::*;
+use super::{merge::RevertClosurize, *};
 use crate::{label::Label, position::TermPos};
 
 // Update the environment of a term by extending it with a recursive environment. In the general
@@ -203,3 +203,43 @@ pub fn patch_field<C: Cache>(
 
     Ok(())
 }
+
+/// Revert an evaluated record (`Record`) back to a recursive record (`RecRecord`). The fixpoint
+/// will be recomputed again at evaluation.
+///
+/// `revert` is used when an operation (excluding `merge`, which has its own reverting logic) might
+/// have changed the value of fields (e.g. a lazy contract application on a record), requiring to
+/// update recursive dependencies.
+///
+/// # Parameters
+///
+/// `env` and `local_env` are similar to the parameters of
+/// `[crate::transform::Closurize::closurize]`.
+///
+/// - `cache`: the evaluation cache
+/// - `record_data`: the data of the record to revert
+/// - `env`: the final environment in which the fields of the result will be closurized
+/// - `local_env`: the environment of the record represented by `record_data`
+pub fn revert<C: Cache>(
+    cache: &mut C,
+    record_data: RecordData,
+    env: &mut Environment,
+    local_env: &Environment,
+) -> Term {
+    let fields = record_data
+        .fields
+        .into_iter()
+        // In fact, we don't really need to closurize, and could revert alone. However, that would
+        // mean duplicating code from
+        .map(|(id, field)| (id, field.revert_closurize(cache, env, local_env.clone())))
+        .collect();
+
+    let record_data = RecordData {
+        fields,
+        ..record_data
+    };
+
+    // At run-time, we don't care about `RecordDeps`, because this information is already stored in
+    // the cache (formerly thunks in call-by-need). We set it to `None`.
+    Term::RecRecord(record_data, Vec::new(), None)
+}

src/eval/merge.rs

@@ -562,7 +562,7 @@ fn fields_merge_closurize<'a, I: DoubleEndedIterator<Item = &'a Ident> + Clone,
 }
 
 /// Same as [Closurizable], but also revert the element if the term is a variable.
-trait RevertClosurize {
+pub(super) trait RevertClosurize {
     /// Revert the element at the index inside the term (if any), and closurize the result inside `env`.
     fn revert_closurize<C: Cache>(
         self,

src/eval/operation.rs

@@ -25,7 +25,7 @@ use crate::{
     term::{
         array::{Array, ArrayAttrs},
         make as mk_term,
-        record::{self, Field, FieldMetadata, RecordAttrs, RecordData},
+        record::{self, Field, FieldMetadata, RecordData},
         BinaryOp, MergePriority, NAryOp, Number, PendingContract, RecordExtKind, RichTerm,
         SharedTerm, StrChunk, Term, UnaryOp,
     },
@@ -2515,31 +2515,24 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                     ))
                 }
             }
-            // This implementation of `%dictionary_assume%` internally creates
-            // essentially a copy of the record that is being checked, albeit
-            // without values for the fields. If the record in question is
-            // particularly huge, this could have performance implications.
-            //
-            // An alternative implementation would be to duplicate some of the
-            // logic from `eval::merge` in here. We decided not to do that for
-            // simplicity and to keep all the magic operations on revertible
-            // thunks contained in their own module.
-            BinaryOp::DictionaryAssume() => {
+            BinaryOp::RecordLazyAssume() => {
+                // The contract is expected to be of type `String -> Contract`: it takes the name
+                // of the field as a parameter, and returns a contract.
                 let (
                     Closure {
                         body: contract_term,
                         env: contract_env,
                     },
                     _,
                 ) = self.stack.pop_arg(&self.cache).ok_or_else(|| {
-                    EvalError::NotEnoughArgs(3, String::from("dictionary_assume"), pos_op)
+                    EvalError::NotEnoughArgs(3, String::from("record_lazy_assume"), pos_op)
                 })?;
 
-                let lbl = match_sharedterm! {t1, with {
-                        Term::Lbl(lbl) => lbl
+                let label = match_sharedterm! {t1, with {
+                        Term::Lbl(label) => label
                     } else return Err(EvalError::TypeError(
-                        String::from("Lbl"),
-                        String::from("dictionary_assume, 2nd argument"),
+                        String::from("Label"),
+                        String::from("record_lazy_assume, 2nd argument"),
                         fst_pos,
                         RichTerm {
                             term: t1,
@@ -2551,55 +2544,47 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                 match_sharedterm! {t2,
                     with {
                         Term::Record(record_data) => {
-                            let contract = contract_term.closurize(&mut self.cache, &mut env2, contract_env);
-                            let record_contract = Term::Record(RecordData {
-                                fields: record_data
-                                    .fields
-                                    .iter()
-                                    .map(|(key, value)| {
-                                        (
-                                            *key,
-                                            Field {
-                                                value: None,
-                                                pending_contracts: vec![PendingContract::new(
-                                                    contract.clone(),
-                                                    lbl.clone(),
-                                                )],
-                                                // This is intentionally not written as
-                                                // `{ opt: value.metadata.opt, ..Default::default() }`
-                                                //
-                                                // When `FieldMetadata` is changed in the future, we will need to consider
-                                                // which values should be inherited from `value.metadata`.
-                                                //
-                                                // The `metadata` field here must be chosen such that, upon merging it
-                                                // with `value.metadata`, the result is identical to the original metadata
-                                                // `value.metadata` of the field.
-                                                metadata: FieldMetadata {
-                                                    opt: value.metadata.opt,
-
-                                                    doc: None,
-                                                    annotation: Default::default(),
-                                                    not_exported: false,
-                                                    priority: Default::default(),
-                                                },
-                                            },
-                                        )
-                                    })
-                                    .collect(),
-                                attrs: RecordAttrs { open: true },
-                                ..Default::default()
-                            });
-
-                            let merge_term = Closure {
-                                body: mk_opn!(
-                                    NAryOp::MergeContract(),
-                                    Term::Lbl(lbl),
-                                    Term::Record(record_data),
-                                    record_contract
-                                ),
-                                env: env2,
+                            // due to a limitation of `match_sharedterm`: see the macro's
+                            // documentation
+                            let mut record_data = record_data;
+
+                            let mut contract_at_field = |id: Ident| {
+                                let pos = contract_term.pos;
+                                mk_app!(
+                                    contract_term.clone(),
+                                    RichTerm::new(Term::Str(id.into()), id.pos))
+                                        .with_pos(pos)
+                                        .closurize(&mut self.cache, &mut env2, contract_env.clone(),
+                                )
                             };
-                            Ok(merge_term)
+
+                            for (id, field) in record_data.fields.iter_mut() {
+                                field.pending_contracts.push(PendingContract {
+                                    contract: contract_at_field(id.clone()),
+                                    label: label.clone(),
+                                });
+                            }
+
+                            // IMPORTANT: here, we revert the record back to a `RecRecord`. The
+                            // reason is that applying a contract over fields might change the
+                            // value of said fields (the typical example is adding a value to a
+                            // subrecord via the default value of a contract).
+                            //
+                            // We want recursive occurrences of fields to pick this new value as
+                            // well: hence, we need to recompute the fixpoint, which is done by
+                            // `fixpoint::revert`.
+                            let mut env = Environment::new();
+                            let reverted = super::fixpoint::revert(
+                                &mut self.cache,
+                                record_data,
+                                &mut env,
+                                &env2
+                            );
+
+                            Ok(Closure {
+                                body: RichTerm::new(reverted, pos2),
+                                env,
+                            })
                         }
                     } else Err(EvalError::TypeError(
                         String::from("Record"),

src/parser/grammar.lalrpop

@@ -842,7 +842,7 @@ InfixExpr: UniTerm = {
 BOpPre: BinaryOp = {
     "assume" => BinaryOp::Assume(),
     "array_lazy_assume" => BinaryOp::ArrayLazyAssume(),
-    "dictionary_assume" => BinaryOp::DictionaryAssume(),
+    "record_lazy_assume" => BinaryOp::RecordLazyAssume(),
     "unseal" => BinaryOp::Unseal(),
     "seal" => BinaryOp::Seal(),
     "go_field" => BinaryOp::GoField(),
@@ -1003,7 +1003,7 @@ extern {
         "typeof" => Token::Normal(NormalToken::Typeof),
         "assume" => Token::Normal(NormalToken::Assume),
         "array_lazy_assume" => Token::Normal(NormalToken::ArrayLazyAssume),
-        "dictionary_assume" => Token::Normal(NormalToken::DictionaryAssume),
+        "record_lazy_assume" => Token::Normal(NormalToken::RecordLazyAssume),
         "op force" => Token::Normal(NormalToken::OpForce),
         "blame" => Token::Normal(NormalToken::Blame),
         "chng_pol" => Token::Normal(NormalToken::ChangePol),

src/parser/lexer.rs

@@ -186,8 +186,8 @@ pub enum NormalToken<'input> {
     Assume,
     #[token("%array_lazy_assume%")]
     ArrayLazyAssume,
-    #[token("%dictionary_assume%")]
-    DictionaryAssume,
+    #[token("%record_lazy_assume%")]
+    RecordLazyAssume,
     #[token("%blame%")]
     Blame,
     #[token("%chng_pol%")]

src/term/mod.rs

@@ -1286,15 +1286,18 @@ pub enum BinaryOp {
     /// This simply inserts a contract into the array attributes.
     ArrayLazyAssume(),
 
-    /// Apply a dictionary contract to a record. The arguments are a label
-    /// and the contract contained in the dictionary type. Results in a function from
-    /// records to records that applies the dictionary contract to its argument.
+    /// Lazily map contracts over a record. The arguments are a label and a function which takes
+    /// the name of the field as a parameter and returns the corresponding contract.
     ///
+    /// Results in a function from records to records that applies the dictionary contract to its
+    /// argument.
+    ///
+    /// TODO: fixdoc
     /// When used with a dictionary contract `{_: C}` and a record `R`,
     /// synthesizes a record contract whose fields are the fields of `R` with the
     /// contract `C` attached to each of them. Then uses `NAryOp::MergeContract` to
     /// apply this record contract to `R`.
-    DictionaryAssume(),
+    RecordLazyAssume(),
 
     /// Set the message of the current diagnostic of a label.
     LabelWithMessage(),

src/typecheck/operation.rs

@@ -386,7 +386,7 @@ pub fn get_bop_type(
         }
         // The first argument is a label, the third is a contract.
         // forall a. Dyn -> {_: a} -> Dyn -> {_: a}
-        BinaryOp::DictionaryAssume() => {
+        BinaryOp::RecordLazyAssume() => {
             let ty_field = UnifType::UnifVar(state.table.fresh_type_var_id());
             let ty_dict = mk_uniftype::dyn_record(ty_field);
             (

stdlib/internals.ncl

@@ -100,7 +100,7 @@
 
   "$dyn_record" = fun contract label value =>
     if %typeof% value == `Record then
-      %dictionary_assume% (%go_dict% label) value contract
+      %record_lazy_assume% (%go_dict% label) value (fun _field => contract)
     else
       %blame% (%label_with_message% "not a record" label),