summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/error/mod.rs3
-rw-r--r--dhall/src/phase/normalize.rs32
-rw-r--r--dhall/src/phase/typecheck.rs92
3 files changed, 120 insertions, 7 deletions
diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs
index 125d013..2f65443 100644
--- a/dhall/src/error/mod.rs
+++ b/dhall/src/error/mod.rs
@@ -55,6 +55,7 @@ pub(crate) enum TypeMessage {
TypeMismatch(Typed, Normalized, Typed),
AnnotMismatch(Typed, Normalized),
Untyped,
+ FieldCollision(Label),
InvalidListElement(usize, Normalized, Typed),
InvalidListType(Normalized),
InvalidOptionalType(Normalized),
@@ -80,6 +81,8 @@ pub(crate) enum TypeMessage {
ProjectionMissingEntry,
Sort,
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 be2ba51..653f415 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
+}
+
fn merge_maps<K, V>(
map1: &HashMap<K, V>,
map2: &HashMap<K, V>,
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 419b2e2..bd8e1bb 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -598,6 +598,83 @@ fn type_last_layer(
}
Ok(RetTypeOnly(text_type))
}
+ 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 = match (k_l, k_r) {
+ (dhall_syntax::Const::Type, dhall_syntax::Const::Type) => dhall_syntax::Const::Type,
+ (dhall_syntax::Const::Kind, dhall_syntax::Const::Kind) => dhall_syntax::Const::Kind,
+ (dhall_syntax::Const::Sort, dhall_syntax::Const::Sort) => dhall_syntax::Const::Sort,
+ (l_mismatch, r_mismatch) =>
+ return Err(mkerr(RecordTypeMismatch(
+ Typed::from_const(l_mismatch),
+ Typed::from_const(r_mismatch),
+ 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, _) => {}
@@ -622,6 +699,7 @@ fn type_last_layer(
NaturalTimes => Natural,
TextAppend => Text,
ListAppend => unreachable!(),
+ RecursiveRecordTypeMerge => unreachable!(),
_ => return Err(mkerr(Unimplemented)),
})?;
@@ -1128,13 +1206,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");
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-25 06:29:06 +0000