diff --git a/core/src/eval/operation.rs b/core/src/eval/operation.rs index 84d8c46b6c..2ca3b7c758 100644 --- a/core/src/eval/operation.rs +++ b/core/src/eval/operation.rs @@ -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, }; @@ -30,7 +30,7 @@ use crate::{ term::{ array::{Array, ArrayAttrs, OutOfBoundError}, make as mk_term, - record::{self, Field, FieldMetadata, RecordData}, + record::*, string::NickelString, *, }, @@ -2580,6 +2580,148 @@ impl VirtualMachine { 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, IndexMap) = + 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); + 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, + ))) + } } } diff --git a/core/src/parser/grammar.lalrpop b/core/src/parser/grammar.lalrpop index a937d5fd36..c6d391dfef 100644 --- a/core/src/parser/grammar.lalrpop +++ b/core/src/parser/grammar.lalrpop @@ -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, @@ -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), diff --git a/core/src/parser/lexer.rs b/core/src/parser/lexer.rs index b0bbae2e69..e8d7c8d1b0 100644 --- a/core/src/parser/lexer.rs +++ b/core/src/parser/lexer.rs @@ -261,9 +261,9 @@ pub enum NormalToken<'input> { RecordFields, #[token("%record/fields_with_opts%")] RecordFieldsWithOpts, - #[token("%record/values%")] RecordValues, + #[token("%pow%")] Pow, #[token("%trace%")] @@ -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, diff --git a/core/src/term/mod.rs b/core/src/term/mod.rs index 505c9c6ba2..dfdfa723c1 100644 --- a/core/src/term/mod.rs +++ b/core/src/term/mod.rs @@ -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, @@ -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"), diff --git a/core/src/typecheck/operation.rs b/core/src/typecheck/operation.rs index e481863d6e..2f8946b37f 100644 --- a/core/src/typecheck/operation.rs +++ b/core/src/typecheck/operation.rs @@ -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) + } }) }