Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add record/split_pair and record/disjoint_merge #1982

Merged
merged 1 commit into from
Jul 3, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
146 changes: 144 additions & 2 deletions core/src/eval/operation.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
//! receive evaluated operands and implement the actual semantics of operators.
use super::{
cache::lazy::Thunk,
merge::{self, MergeMode},
merge::{self, split, MergeMode},
stack::StrAccData,
subst, Cache, Closure, Environment, ImportResolver, VirtualMachine,
};
Expand All @@ -30,7 +30,7 @@ use crate::{
term::{
array::{Array, ArrayAttrs, OutOfBoundError},
make as mk_term,
record::{self, Field, FieldMetadata, RecordData},
record::*,
string::NickelString,
*,
},
Expand Down Expand Up @@ -2580,6 +2580,148 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
pos_op_inh,
)))
}
BinaryOp::RecordSplitPair => {
let t1 = t1.into_owned();
let t2 = t2.into_owned();

let Term::Record(record1) = t1 else {
return Err(mk_type_error!(
"record/full_difference",
"Record",
1,
t1.into(),
pos1
));
};

let Term::Record(record2) = t2 else {
return Err(mk_type_error!(
"record/full_difference",
"Record",
2,
t2.into(),
pos2
));
};

let split::SplitResult {
left,
center,
right,
} = split::split(record1.fields, record2.fields);

let left_only = Term::Record(RecordData {
fields: left,
sealed_tail: record1.sealed_tail,
attrs: record1.attrs,
});

let right_only = Term::Record(RecordData {
fields: right,
sealed_tail: record2.sealed_tail,
attrs: record2.attrs,
});

let (center1, center2): (IndexMap<LocIdent, Field>, IndexMap<LocIdent, Field>) =
center
.into_iter()
.map(|(id, (left, right))| ((id, left), (id, right)))
.unzip();

let left_center = Term::Record(RecordData {
fields: center1,
sealed_tail: None,
attrs: RecordAttrs::default().closurized(),
});

let right_center = Term::Record(RecordData {
fields: center2,
sealed_tail: None,
attrs: RecordAttrs::default().closurized(),
});

Ok(Closure::atomic_closure(RichTerm::new(
Term::Record(RecordData {
fields: IndexMap::from([
(
LocIdent::from("left_only"),
Field::from(RichTerm::from(left_only)),
),
(
LocIdent::from("left_center"),
Field::from(RichTerm::from(left_center)),
),
(
LocIdent::from("right_center"),
Field::from(RichTerm::from(right_center)),
),
(
LocIdent::from("right_only"),
Field::from(RichTerm::from(right_only)),
),
]),
attrs: RecordAttrs::default().closurized(),
sealed_tail: None,
}),
pos_op_inh,
)))
}
BinaryOp::RecordDisjointMerge => {
let t1 = t1.into_owned();
let t2 = t2.into_owned();

let Term::Record(mut record1) = t1 else {
return Err(mk_type_error!(
"record/disjoint_merge",
"Record",
1,
t1.into(),
pos1
));
};

let Term::Record(record2) = t2 else {
return Err(mk_type_error!(
"record/disjoint_merge",
"Record",
2,
t2.into(),
pos2
));
};

// As for merge, we refuse to combine two records if one of them has a sealed tail
if let Some(record::SealedTail { label, .. }) =
record1.sealed_tail.or(record2.sealed_tail)
{
return Err(EvalError::IllegalPolymorphicTailAccess {
action: IllegalPolymorphicTailAction::Merge,
evaluated_arg: label.get_evaluated_arg(&self.cache),
label,
call_stack: std::mem::take(&mut self.call_stack),
});
}

// Note that because of record closurization, we assume here that the record data
// of each record are already closurized, so we don't really care about
// environments. Should that invariant change, we might get into trouble (trouble
// meaning undue `UnboundIdentifier` errors).
debug_assert!(record1.attrs.closurized && record2.attrs.closurized);
record1.fields.extend(record2.fields);
yannham marked this conversation as resolved.
Show resolved Hide resolved
record1.attrs.open = record1.attrs.open || record2.attrs.open;

Ok(Closure::atomic_closure(RichTerm::new(
Term::Record(RecordData {
fields: record1.fields,
attrs: record1.attrs,
// We need to set the tail to `None` explicitly to appease the borrow
// checker which objects that `sealed_tail` has been moved in the if
// let above.
sealed_tail: None,
}),
pos_op_inh,
)))
}
}
}

Expand Down
4 changes: 4 additions & 0 deletions core/src/parser/grammar.lalrpop
Original file line number Diff line number Diff line change
Expand Up @@ -1330,6 +1330,8 @@ BOpPre: BinaryOp = {
},
"record/remove" => BinaryOp::RecordRemove(RecordOpKind::IgnoreEmptyOpt),
"record/remove_with_opts" => BinaryOp::RecordRemove(RecordOpKind::ConsiderAllFields),
"record/split_pair" => BinaryOp::RecordSplitPair,
"record/disjoint_merge" => BinaryOp::RecordDisjointMerge,
"label/with_message" => BinaryOp::LabelWithMessage,
"label/with_notes" => BinaryOp::LabelWithNotes,
"label/append_note" => BinaryOp::LabelAppendNote,
Expand Down Expand Up @@ -1555,6 +1557,8 @@ extern {
"record/has_field_with_opts" => Token::Normal(NormalToken::RecordHasFieldWithOpts),
"record/field_is_defined" => Token::Normal(NormalToken::RecordFieldIsDefined),
"record/field_is_defined_with_opts" => Token::Normal(NormalToken::RecordFieldIsDefinedWithOpts),
"record/split_pair" => Token::Normal(NormalToken::RecordSplitPair),
"record/disjoint_merge" => Token::Normal(NormalToken::RecordDisjointMerge),
"array/map" => Token::Normal(NormalToken::ArrayMap),
"array/generate" => Token::Normal(NormalToken::ArrayGen),
"array/at" => Token::Normal(NormalToken::ArrayAt),
Expand Down
6 changes: 5 additions & 1 deletion core/src/parser/lexer.rs
Original file line number Diff line number Diff line change
Expand Up @@ -261,9 +261,9 @@ pub enum NormalToken<'input> {
RecordFields,
#[token("%record/fields_with_opts%")]
RecordFieldsWithOpts,

#[token("%record/values%")]
RecordValues,

#[token("%pow%")]
Pow,
#[token("%trace%")]
Expand All @@ -287,6 +287,10 @@ pub enum NormalToken<'input> {
RecordFieldIsDefined,
#[token("%record/field_is_defined_with_opts%")]
RecordFieldIsDefinedWithOpts,
#[token("%record/split_pair%")]
RecordSplitPair,
#[token("%record/disjoint_merge%")]
RecordDisjointMerge,

#[token("merge")]
Merge,
Expand Down
26 changes: 26 additions & 0 deletions core/src/term/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1733,6 +1733,30 @@ pub enum BinaryOp {
/// Test if the field of a record exists and has a definition.
RecordFieldIsDefined(RecordOpKind),

/// Take a pair of records and split them into four separate records:
///
/// - `left_only`: fields of the left argument but not in the right
/// - `left_center`: fields of the left argument that happens to also be in the right (but the
/// value and the metadata are taken from the left)
/// - `right_center`: fields of the right argument that happens to also be in the left (but the
/// value and the metadata are taken from the right)
/// - `right_only`: fields of the right argument but not in the left
///
/// As opposed to an equivalent user-defined implementation, this primop has better performance
/// and is able to preserve field metadata.
///
/// If `left` (resp. `right`) is open or has a sealed tail, then `left_only` (resp.
/// `right_only`) will inherit the same properties. `left_center` (resp. `right_center`) are
/// always closed and without a sealed tail.
RecordSplitPair,

/// Take a pair of disjoint records (i.e. records with no common field) and combine them into
/// one. It's a form of merging, but based on the assumption that the records are disjoint and
/// thus non-conflicting, it's simpler and more efficient than a general merge.
///
/// As for merge, this raises a blame error if one of the arguments has a sealed tail.
RecordDisjointMerge,

/// Concatenate two arrays.
ArrayConcat,

Expand Down Expand Up @@ -1835,6 +1859,8 @@ impl fmt::Display for BinaryOp {
RecordFieldIsDefined(RecordOpKind::ConsiderAllFields) => {
write!(f, "record/field_is_defined_with_opts")
}
Self::RecordSplitPair => write!(f, "record/full_difference"),
Self::RecordDisjointMerge => write!(f, "record/disjoint_merge"),
ArrayConcat => write!(f, "array/concat"),
ArrayAt => write!(f, "array/at"),
Merge(_) => write!(f, "merge"),
Expand Down
27 changes: 27 additions & 0 deletions core/src/typecheck/operation.rs
Original file line number Diff line number Diff line change
Expand Up @@ -500,6 +500,33 @@ pub fn get_bop_type(
mk_uniftype::dynamic(),
TypeVarData::unif_type(),
),
// {_ : a} -> {_ : a}
// -> {
// left_only: {_ : a},
// right_only: {_ : a},
// left_center: {_ : a},
// right_center: {_ : a},
// }
BinaryOp::RecordSplitPair => {
let elt = state.table.fresh_type_uvar(var_level);
let dict = mk_uniftype::dict(elt.clone());

let split_result = mk_uty_record!(
("left_only", dict.clone()),
("right_only", dict.clone()),
("left_center", dict.clone()),
("right_center", dict.clone())
);

(dict.clone(), dict, split_result)
}
// {_ : a} -> {_ : a} -> {_ : a}
BinaryOp::RecordDisjointMerge => {
let elt = state.table.fresh_type_uvar(var_level);
let dict = mk_uniftype::dict(elt.clone());

(dict.clone(), dict.clone(), dict)
}
})
}

Expand Down