Skip to content

Commit

Permalink
Add a freeze primop and stdlib wrapper
Browse files Browse the repository at this point in the history
Following a confusing behavior around the interaction of recursive
fields and dictionary operations (insert, remove, update), it was
proposed in #1877 to freeze
recursive records before applying dictionary operations.

This commit adds a primitive operation to do so, which applies pending
contracts, flushes them, and remove any dependency data, effectively
freezing recursive fields to their current value.

A flag is also added to record attributes, in order to remember that
some record has already been frozen. Indeed, freezing is linear in the
number of fields and pending contracts: freezing at every dictionary
operation thus could be costly. Instead, as for closurization, we do it
once and then remember that it's been done in flag. It helps dictionary
operations preserve frozenness. Only merging or lazy contract
applications might require freezing again.
  • Loading branch information
yannham committed Nov 29, 2024
1 parent 768e1d2 commit c66126d
Show file tree
Hide file tree
Showing 12 changed files with 203 additions and 6 deletions.
2 changes: 2 additions & 0 deletions core/src/bytecode/ast/compat.rs
Original file line number Diff line number Diff line change
Expand Up @@ -540,6 +540,7 @@ impl From<&term::UnaryOp> for PrimOp {
ignore_not_exported: *ignore_not_exported,
},
term::UnaryOp::RecordEmptyWithTail => PrimOp::RecordEmptyWithTail,
term::UnaryOp::RecordFreeze => PrimOp::RecordFreeze,
term::UnaryOp::Trace => PrimOp::Trace,
term::UnaryOp::LabelPushDiag => PrimOp::LabelPushDiag,
#[cfg(feature = "nix-experimental")]
Expand Down Expand Up @@ -1081,6 +1082,7 @@ impl FromAst<PrimOp> for TermPrimOp {
ignore_not_exported: *ignore_not_exported,
}),
PrimOp::RecordEmptyWithTail => TermPrimOp::Unary(term::UnaryOp::RecordEmptyWithTail),
PrimOp::RecordFreeze => TermPrimOp::Unary(term::UnaryOp::RecordFreeze),
PrimOp::Trace => TermPrimOp::Unary(term::UnaryOp::Trace),
PrimOp::LabelPushDiag => TermPrimOp::Unary(term::UnaryOp::LabelPushDiag),
PrimOp::EnumGetArg => TermPrimOp::Unary(term::UnaryOp::EnumGetArg),
Expand Down
11 changes: 11 additions & 0 deletions core/src/bytecode/ast/primop.rs
Original file line number Diff line number Diff line change
Expand Up @@ -336,6 +336,15 @@ pub enum PrimOp {
/// 1. The model record to take the tail from.
RecordEmptyWithTail,

/// Freezes a recursive record to make it a static dictionary. Apply all pending lazy contracts
/// (and flush them), and remove all dependency information, so that the value of the fields is
/// fixed in time and subsequent overrides will only impact the overriden field.
///
/// # Arguments
///
/// 1. The record to freeze.
RecordFreeze,

/// Print a message when encountered during evaluation and proceed with the evaluation of the
/// argument on the top of the stack. Operationally the same as the identity function
///
Expand Down Expand Up @@ -967,6 +976,7 @@ impl fmt::Display for PrimOp {
StringFindAll => write!(f, "string/find_all"),
Force { .. } => write!(f, "force"),
RecordEmptyWithTail => write!(f, "record/empty_with_tail"),
RecordFreeze => write!(f, "record/freeze"),
Trace => write!(f, "trace"),
LabelPushDiag => write!(f, "label/push_diag"),

Expand Down Expand Up @@ -1094,6 +1104,7 @@ impl PrimOp {
| StringFindAll
| Force { .. }
| RecordEmptyWithTail
| RecordFreeze
| Trace
| LabelPushDiag
| EnumGetArg
Expand Down
6 changes: 4 additions & 2 deletions core/src/error/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -251,7 +251,8 @@ pub enum IllegalPolymorphicTailAction {
FieldAccess { field: String },
Map,
Merge,
RecordRemove { field: String },
FieldRemove { field: String },
Freeze,
}

impl IllegalPolymorphicTailAction {
Expand All @@ -264,9 +265,10 @@ impl IllegalPolymorphicTailAction {
}
Map => "cannot map over a record sealed by a polymorphic contract".to_owned(),
Merge => "cannot merge a record sealed by a polymorphic contract".to_owned(),
RecordRemove { field } => {
FieldRemove { field } => {
format!("cannot remove field `{field}` sealed by a polymorphic contract")
}
Freeze => "cannot freeze a record sealed by a polymorphic contract".to_owned(),
}
}
}
Expand Down
87 changes: 85 additions & 2 deletions core/src/eval/operation.rs
Original file line number Diff line number Diff line change
Expand Up @@ -645,9 +645,18 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
missing_field_err.into_eval_err(pos, pos_op)
})?;

// By construction, mapping freezes the record. We set the frozen flag so
// that operations that require the record to be frozen don't have to
// perform the work again.
let attrs = record.attrs.frozen();

Ok(Closure {
body: RichTerm::new(
Term::Record(RecordData { fields, ..record }),
Term::Record(RecordData {
fields,
attrs,
..record
}),
pos_op_inh,
),
env: Environment::new(),
Expand Down Expand Up @@ -1181,6 +1190,73 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
}
_ => mk_type_error!("Record"),
}),
UnaryOp::RecordFreeze => match_sharedterm!(match (t) {
Term::Record(record) => {
let mut record = record;

if record.attrs.frozen {
// A frozen record shouldn't have a polymorphic tail
debug_assert!(record.sealed_tail.is_none());

return Ok(Closure {
body: RichTerm::new(Term::Record(record), pos),
env,
});
}

// It's not clear what the semantics of freezing a record with a sealed tail
// would be, as their might be dependencies between the sealed part and the
// unsealed part. Merging is disallowed on records with tail, so we disallow
// freezing as well.
if let Some(record::SealedTail { label, .. }) = record.sealed_tail {
return Err(EvalError::IllegalPolymorphicTailAccess {
action: IllegalPolymorphicTailAction::Freeze,
evaluated_arg: label.get_evaluated_arg(&self.cache),
label,
call_stack: std::mem::take(&mut self.call_stack),
});
}

let fields = record
.fields
.into_iter()
.map(|(id, field)| {
let value = field.value.map(|value| {
let pos = value.pos;
RuntimeContract::apply_all(
value,
field.pending_contracts.into_iter(),
pos,
)
});

let field = Field {
value,
pending_contracts: Vec::new(),
..field
}
.closurize(&mut self.cache, env.clone());

(id, field)
})
.collect();

let attrs = record.attrs.frozen();

Ok(Closure {
body: RichTerm::new(
Term::Record(RecordData {
fields,
attrs,
sealed_tail: None,
}),
pos_op.into_inherited(),
),
env,
})
}
_ => mk_type_error!("Record"),
}),
UnaryOp::Trace => {
if let Term::Str(s) = &*t {
let _ = writeln!(self.trace, "std.trace: {s}");
Expand Down Expand Up @@ -2250,6 +2326,7 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
))
}
_ => Ok(Closure {
// Insertion preserves the frozenness
body: Term::Record(RecordData { fields, ..record }).into(),
env: env2,
}),
Expand Down Expand Up @@ -2282,7 +2359,7 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
match record.sealed_tail.as_ref() {
Some(t) if t.has_dyn_field(&id) => {
Err(EvalError::IllegalPolymorphicTailAccess {
action: IllegalPolymorphicTailAction::RecordRemove {
action: IllegalPolymorphicTailAction::FieldRemove {
field: id.to_string(),
},
evaluated_arg: t.label.get_evaluated_arg(&self.cache),
Expand All @@ -2307,6 +2384,7 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
} else {
Ok(Closure {
body: RichTerm::new(
// Removal preserves the frozenness
Term::Record(RecordData { fields, ..record }),
pos_op_inh,
),
Expand Down Expand Up @@ -2745,6 +2823,11 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
// documentation
let mut record_data = record_data;

// Applying a lazy contract unfreezes a record, as frozen record are
// expected to have all their contracts applied and thus an empty list of
// pending contracts.
record_data.attrs.frozen = false;

let mut contract_at_field = |id: LocIdent| {
let pos = contract_term.pos;
mk_app!(
Expand Down
2 changes: 2 additions & 0 deletions core/src/parser/grammar.lalrpop
Original file line number Diff line number Diff line change
Expand Up @@ -1170,6 +1170,7 @@ UOp: PrimOp = {
// "op rec_force" => PrimOp::RecForce,
// "op rec_default" => PrimOp::RecDefault,
"record/empty_with_tail" => PrimOp::RecordEmptyWithTail,
"record/freeze" => PrimOp::RecordFreeze,
"trace" => PrimOp::Trace,
"label/push_diag" => PrimOp::LabelPushDiag,
<l: @L> "eval_nix" <r: @R> =>? {
Expand Down Expand Up @@ -1617,6 +1618,7 @@ extern {
"record/split_pair" => Token::Normal(NormalToken::RecordSplitPair),
"record/disjoint_merge" => Token::Normal(NormalToken::RecordDisjointMerge),
"record/merge_contract" => Token::Normal(NormalToken::RecordMergeContract),
"record/freeze" => Token::Normal(NormalToken::RecordFreeze),
"array/map" => Token::Normal(NormalToken::ArrayMap),
"array/generate" => Token::Normal(NormalToken::ArrayGen),
"array/at" => Token::Normal(NormalToken::ArrayAt),
Expand Down
2 changes: 2 additions & 0 deletions core/src/parser/lexer.rs
Original file line number Diff line number Diff line change
Expand Up @@ -311,6 +311,8 @@ pub enum NormalToken<'input> {
RecordDisjointMerge,
#[token("%record/merge_contract%")]
RecordMergeContract,
#[token("%record/freeze%")]
RecordFreeze,

#[token("merge")]
Merge,
Expand Down
6 changes: 6 additions & 0 deletions core/src/term/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1538,6 +1538,11 @@ pub enum UnaryOp {
/// function that preserves the sealed polymorphic tail of its argument.
RecordEmptyWithTail,

/// Freezes a recursive record to make it a static dictionary. Apply all pending lazy contracts
/// (and flush them), and remove all dependency information, so that the value of the fields is
/// fixed in time and subsequent overrides will only impact the overriden field.
RecordFreeze,

/// Print a message when encountered during evaluation and proceed with the evaluation of the
/// argument on the top of the stack. Operationally the same as the identity function
Trace,
Expand Down Expand Up @@ -1655,6 +1660,7 @@ impl fmt::Display for UnaryOp {
RecDefault => write!(f, "rec_default"),
RecForce => write!(f, "rec_force"),
RecordEmptyWithTail => write!(f, "record/empty_with_tail"),
RecordFreeze => write!(f, "record/freeze"),
Trace => write!(f, "trace"),
LabelPushDiag => write!(f, "label/push_diag"),

Expand Down
23 changes: 22 additions & 1 deletion core/src/term/record.rs
Original file line number Diff line number Diff line change
Expand Up @@ -23,25 +23,46 @@ pub struct RecordAttrs {
/// be closurized by construction. In the meantime, while we need to cope with a unique AST
/// across the whole pipeline, we use this flag.
pub closurized: bool,
/// If the record has been frozen.
///
/// A recursive record is frozen when all the lazy contracts are applied to their corresponding
/// fields and flushed from the lazy contracts list. The values of the fields are computed but
/// all dependencies are erased. That is, we turn a recursive, overridable record into a static
/// dictionary. The information about field dependencies is lost and future overriding won't
/// update reverse dependencies.
///
/// Like `closurized`, we store this information for performance reason: freezing is expensive
/// (linear in the number of fields of the record), and we might need to do it on every
/// dictionary operation such as `insert`, `remove`, etc. (see
/// [#1877](https://github.com/tweag/nickel/issues/1877)). This flags avoid repeated, useless
/// freezing.
pub frozen: bool,
}

impl RecordAttrs {
pub fn new() -> Self {
Self::default()
}

/// Set the `closurized` flag to true and return the updated attributes.
/// Sets the `closurized` flag to true and return the updated attributes.
pub fn closurized(mut self) -> Self {
self.closurized = true;
self
}

/// Sets the `frozen` flag to true and return the updated attributes.
pub fn frozen(mut self) -> Self {
self.frozen = true;
self
}
}

impl Combine for RecordAttrs {
fn combine(left: Self, right: Self) -> Self {
RecordAttrs {
open: left.open || right.open,
closurized: left.closurized && right.closurized,
frozen: left.frozen && right.frozen,
}
}
}
Expand Down
6 changes: 5 additions & 1 deletion core/src/typecheck/operation.rs
Original file line number Diff line number Diff line change
Expand Up @@ -231,7 +231,11 @@ pub fn get_uop_type(
(ty.clone(), ty)
}
UnaryOp::RecordEmptyWithTail => (mk_uniftype::dynamic(), mk_uniftype::dynamic()),

// forall a. { _ : a} -> { _ : a }
UnaryOp::RecordFreeze => {
let dict = mk_uniftype::dict(state.table.fresh_type_uvar(var_level));
(dict.clone(), dict)
}
// forall a. Str -> a -> a
UnaryOp::Trace => {
let ty = state.table.fresh_type_uvar(var_level);
Expand Down
38 changes: 38 additions & 0 deletions core/stdlib/std.ncl
Original file line number Diff line number Diff line change
Expand Up @@ -3317,6 +3317,44 @@
record
|> fields
|> std.array.length,

freeze
: forall a. { _ : a } -> { _ : a }
| doc m%"
Freezes a recursive record:

- The values of recursive fields are frozen at the current values, and
the dependencies are forgotten. **This means that subsequent overrides
through merging will only affect the overriden fields, but will no
longer update reverse dependencies**.
- All lazy pending contracts accumulated through merging and annotations
will be applied and flushed. **This means that the contracts of this
record won't propagate through future merges anymore after freezing**.

Note that the documentation and the priority of the fields aren't
affected.

`freeze` is used internally in the stdlib when applying dictionary
operations, such as `std.record.insert` or `std.record.remove`. Indeed,
interleaving dictionary operations and recursive records can lean to
surprising and unintuitive results. The Nickel stdlib tries to avoid
using records in both recursive and dictionary modes at the same time.

Freezing is idempotent: freezing an already frozen record has no effect.

# Examples

```nickel multiline
let frozen = std.record.freeze { x = "old", y = x } in
frozen & { x | force = "new" }
# => { x = "new", y = "old" }

let frozen = std.record.freeze { x | Number = 1 } in
frozen & { x | force = "bypass number contract" }
# => { x = "bypass number contract" }
```
"%
= fun record => %record/freeze% record,
},

string = {
Expand Down
14 changes: 14 additions & 0 deletions core/tests/integration/inputs/records/freezing.ncl
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
# test.type = 'pass'
[
(%record/freeze% { x = 1, y = x }) & { x | force = 2 } == { x = 2, y = 1 },
(%record/freeze% { x | default = 1, y = x }) & { x = 2 } == { x = 2, y = 1 },
(%record/freeze% { x | default = 1, y = x })
& (%record/freeze% { x = 2, z = x })
& { x | force = 3 } == { x = 3, y = 1, z = 2 },

# freezing, as record mapping, flushes pending contracts and make them not
# propagate anymore
(%record/freeze% {x | String = "a"}) & {x | force = 1} == {x = 1},

]
|> std.test.assert_all
12 changes: 12 additions & 0 deletions core/tests/integration/inputs/records/merge_unfreezes.ncl
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
# test.type = 'error'
#
# [test.metadata]
# error = 'EvalError::BlameError'

# Test that even if freezing makes the initial `String` contract to not
# propagate, it doesn't prevent other contracts coming from unfrozen records to
# propagate.
%force% ((%record/freeze% { x | String = "a" })
& { x | priority 1 | Number = 2 }
& { x | priority 2 = false })

0 comments on commit c66126d

Please sign in to comment.