summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/error/mod.rs2
-rw-r--r--dhall/src/phase/normalize.rs32
-rw-r--r--dhall/src/phase/typecheck.rs88
3 files changed, 115 insertions, 7 deletions
diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs
index bc5322a..aed6ccd 100644
--- a/dhall/src/error/mod.rs
+++ b/dhall/src/error/mod.rs
@@ -83,6 +83,8 @@ pub(crate) enum TypeMessage {
Sort,
RecordMismatch(Typed, Typed),
RecordTypeDuplicateField,
+ RecordTypeMergeRequiresRecordType(Type),
+ RecordTypeMismatch(Type, Type, Type, Type),
UnionTypeDuplicateField,
Unimplemented,
}
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index 7d86833..a493b66 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -372,6 +372,38 @@ enum Ret<'a> {
Expr(ExprF<Thunk, X>),
}
+/// Performs an intersection of two HashMaps.
+///
+/// # Arguments
+///
+/// * `f` - Will compute the final value from the intersecting
+/// key and the values from both maps.
+///
+/// # Description
+///
+/// If the key is present in both maps then the final value for
+/// that key is computed via the `f` function.
+///
+/// The final map will contain the shared keys from the
+/// two input maps with the final computed value from `f`.
+pub(crate) fn intersection_with_key<K, T, U, V>(
+ mut f: impl FnMut(&K, &T, &U) -> V,
+ map1: &HashMap<K, T>,
+ map2: &HashMap<K, U>,
+) -> HashMap<K, V>
+where
+ K: std::hash::Hash + Eq + Clone,
+{
+ let mut kvs = HashMap::new();
+
+ for (k, t) in map1 {
+ // Only insert in the final map if the key exists in both
+ if let Some(u) = map2.get(k) { kvs.insert(k.clone(), f(k, t, u)); }
+ }
+
+ kvs
+}
+
/// Performs an outer join of two HashMaps.
///
/// # Arguments
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index d9f6e09..53ad99b 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -704,6 +704,79 @@ fn type_last_layer(
combine_record_types(ctx, kts_x, kts_y).map(|r| RetTypeOnly(r))
}
+ BinOp(RecursiveRecordTypeMerge, l, r) => {
+ // A recursive function to dig down into
+ // records of records when merging.
+ fn combine_record_types(
+ ctx: &TypecheckContext,
+ kts_l: HashMap<Label, TypeThunk>,
+ kts_r: HashMap<Label, TypeThunk>,
+ ) -> Result<Typed, TypeError> {
+ use crate::phase::normalize::intersection_with_key;
+
+ // If the Label exists for both records and Type for the values
+ // are records themselves, then we hit the recursive case.
+ // Otherwise we have a field collision.
+ let combine = |k: &Label, kts_l_inner: &TypeThunk, kts_r_inner: &TypeThunk|
+ -> Result<Typed, TypeError> {
+ match (kts_l_inner.to_value(), kts_r_inner.to_value()) {
+ (Value::RecordType(kvs_l_inner), Value::RecordType(kvs_r_inner)) =>
+ combine_record_types(ctx, kvs_l_inner, kvs_r_inner),
+ (_, _) => Err(TypeError::new(ctx, FieldCollision(k.clone()))),
+ }
+ };
+
+ let kts = intersection_with_key(
+ |k: &Label, l: &TypeThunk, r: &TypeThunk| combine(k, l, r),
+ &kts_l,
+ &kts_r,
+ );
+
+ Ok(tck_record_type(
+ ctx,
+ kts.into_iter().map(|(x, v)| v.map(|r| (x.clone(), r)))
+ )?
+ .into_type())
+ };
+
+ // Extract the Const of the LHS
+ let k_l = match l.get_type()?.to_value() {
+ Value::Const(k) => k,
+ _ => return Err(mkerr(RecordTypeMergeRequiresRecordType(l.clone()))),
+ };
+
+ // Extract the Const of the RHS
+ let k_r = match r.get_type()?.to_value() {
+ Value::Const(k) => k,
+ _ => return Err(mkerr(RecordTypeMergeRequiresRecordType(r.clone()))),
+ };
+
+ // Const values must match for the Records
+ let k = if k_l == k_r { k_l } else {
+ return Err(mkerr(RecordTypeMismatch(
+ Typed::from_const(k_l),
+ Typed::from_const(k_r),
+ l.clone(),
+ r.clone(),
+ )))
+ };
+
+ // Extract the LHS record type
+ let kts_x = match l.to_value() {
+ Value::RecordType(kts) => kts,
+ _ => return Err(mkerr(RecordTypeMergeRequiresRecordType(l.clone()))),
+ };
+
+ // Extract the RHS record type
+ let kts_y = match r.to_value() {
+ Value::RecordType(kts) => kts,
+ _ => return Err(mkerr(RecordTypeMergeRequiresRecordType(r.clone()))),
+ };
+
+ // Ensure that the records combine without a type error
+ // and if not output the final Const value.
+ combine_record_types(ctx, kts_x, kts_y).and(Ok(RetTypeOnly(Typed::from_const(k))))
+ }
BinOp(o @ ListAppend, l, r) => {
match l.get_type()?.to_value() {
Value::AppliedBuiltin(List, _) => {}
@@ -730,6 +803,7 @@ fn type_last_layer(
ListAppend => unreachable!(),
RightBiasedRecordMerge => unreachable!(),
RecursiveRecordMerge => unreachable!(),
+ RecursiveRecordTypeMerge => unreachable!(),
_ => return Err(mkerr(Unimplemented)),
})?;
@@ -1236,13 +1310,13 @@ mod spec_tests {
ti_success!(ti_success_unit_RecursiveRecordMergeTwo, "unit/RecursiveRecordMergeTwo");
ti_success!(ti_success_unit_RecursiveRecordMergeTwoKinds, "unit/RecursiveRecordMergeTwoKinds");
ti_success!(ti_success_unit_RecursiveRecordMergeTwoTypes, "unit/RecursiveRecordMergeTwoTypes");
- // ti_success!(ti_success_unit_RecursiveRecordTypeMergeRecursively, "unit/RecursiveRecordTypeMergeRecursively");
- // ti_success!(ti_success_unit_RecursiveRecordTypeMergeRecursivelyKinds, "unit/RecursiveRecordTypeMergeRecursivelyKinds");
- // ti_success!(ti_success_unit_RecursiveRecordTypeMergeRecursivelyTypes, "unit/RecursiveRecordTypeMergeRecursivelyTypes");
- // ti_success!(ti_success_unit_RecursiveRecordTypeMergeRhsEmpty, "unit/RecursiveRecordTypeMergeRhsEmpty");
- // ti_success!(ti_success_unit_RecursiveRecordTypeMergeTwo, "unit/RecursiveRecordTypeMergeTwo");
- // ti_success!(ti_success_unit_RecursiveRecordTypeMergeTwoKinds, "unit/RecursiveRecordTypeMergeTwoKinds");
- // ti_success!(ti_success_unit_RecursiveRecordTypeMergeTwoTypes, "unit/RecursiveRecordTypeMergeTwoTypes");
+ ti_success!(ti_success_unit_RecursiveRecordTypeMergeRecursively, "unit/RecursiveRecordTypeMergeRecursively");
+ ti_success!(ti_success_unit_RecursiveRecordTypeMergeRecursivelyKinds, "unit/RecursiveRecordTypeMergeRecursivelyKinds");
+ ti_success!(ti_success_unit_RecursiveRecordTypeMergeRecursivelyTypes, "unit/RecursiveRecordTypeMergeRecursivelyTypes");
+ ti_success!(ti_success_unit_RecursiveRecordTypeMergeRhsEmpty, "unit/RecursiveRecordTypeMergeRhsEmpty");
+ ti_success!(ti_success_unit_RecursiveRecordTypeMergeTwo, "unit/RecursiveRecordTypeMergeTwo");
+ ti_success!(ti_success_unit_RecursiveRecordTypeMergeTwoKinds, "unit/RecursiveRecordTypeMergeTwoKinds");
+ ti_success!(ti_success_unit_RecursiveRecordTypeMergeTwoTypes, "unit/RecursiveRecordTypeMergeTwoTypes");
ti_success!(ti_success_unit_RightBiasedRecordMergeRhsEmpty, "unit/RightBiasedRecordMergeRhsEmpty");
ti_success!(ti_success_unit_RightBiasedRecordMergeTwo, "unit/RightBiasedRecordMergeTwo");
ti_success!(ti_success_unit_RightBiasedRecordMergeTwoDifferent, "unit/RightBiasedRecordMergeTwoDifferent");