From fc309bf41dfe53d043766ec9d468389b2b4269ae Mon Sep 17 00:00:00 2001 From: FintanH Date: Thu, 1 Aug 2019 16:26:10 +0100 Subject: Add typechecking for RecursiveRecordTypeMerge. The implementation brings with it intersection_with_key over HashMaps to help with the type checking of records of records. The implementation first checks that the Const values line up with the LHS and RHS. Then checks that combining the records does not result in a FieldCollision. It will finally return the shared Const type of the arguments. --- dhall/src/phase/normalize.rs | 32 +++++++++++++++ dhall/src/phase/typecheck.rs | 92 ++++++++++++++++++++++++++++++++++++++++---- 2 files changed, 117 insertions(+), 7 deletions(-) (limited to 'dhall/src/phase') 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), } +/// 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( + mut f: impl FnMut(&K, &T, &U) -> V, + map1: &HashMap, + map2: &HashMap, +) -> HashMap +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( map1: &HashMap, map2: &HashMap, 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, + kts_r: HashMap, + ) -> Result { + 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 { + 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"); -- cgit v1.2.3 From 8bc33c16e90ff6e1d2b4ddc7317a91190c9d8540 Mon Sep 17 00:00:00 2001 From: FintanH Date: Sat, 3 Aug 2019 18:54:01 +0100 Subject: Simplify Const checking logic --- dhall/src/phase/typecheck.rs | 18 +++++++----------- 1 file changed, 7 insertions(+), 11 deletions(-) (limited to 'dhall/src/phase') diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index 3bff7ca..75f78ac 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -687,17 +687,13 @@ fn type_last_layer( }; // 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(), - ))), + 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 -- cgit v1.2.3