diff options
| -rw-r--r-- | dhall/src/error/mod.rs | 3 | ||||
| -rw-r--r-- | dhall/src/phase/normalize.rs | 32 | ||||
| -rw-r--r-- | dhall/src/phase/typecheck.rs | 92 |
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"); |