diff options
author | Nadrieril Feneanar | 2019-08-03 19:01:40 +0200 |
---|---|---|
committer | GitHub | 2019-08-03 19:01:40 +0200 |
commit | 9113e15534f57626ae9be662738e1d3d22434e88 (patch) | |
tree | b29bf3db1ee8b482c9c41bec6b3ebabccb3465c9 /dhall/src | |
parent | 4b82e03dfaaeec98562aa2bff25ad38079d35c9c (diff) | |
parent | dceabb85e407b8e0e52105a725f3bb782fa474de (diff) |
Merge pull request #88 from FintanH/fintan/typecheck-prefer
Add case for RightBasedRecordMerge in the typechecking phase.
Diffstat (limited to 'dhall/src')
-rw-r--r-- | dhall/src/error/mod.rs | 2 | ||||
-rw-r--r-- | dhall/src/phase/normalize.rs | 2 | ||||
-rw-r--r-- | dhall/src/phase/typecheck.rs | 52 |
3 files changed, 50 insertions, 6 deletions
diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs index 125d013..20b8636 100644 --- a/dhall/src/error/mod.rs +++ b/dhall/src/error/mod.rs @@ -76,9 +76,11 @@ pub(crate) enum TypeMessage { MergeAnnotMismatch, MergeHandlerTypeMismatch, MergeHandlerReturnTypeMustNotBeDependent, + MustCombineRecord(Typed), ProjectionMustBeRecord, ProjectionMissingEntry, Sort, + RecordMismatch(Typed, Typed), RecordTypeDuplicateField, UnionTypeDuplicateField, Unimplemented, diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs index be2ba51..da19dc1 100644 --- a/dhall/src/phase/normalize.rs +++ b/dhall/src/phase/normalize.rs @@ -372,7 +372,7 @@ enum Ret<'a> { Expr(ExprF<Thunk, X>), } -fn merge_maps<K, V>( +pub(crate) fn merge_maps<K, V>( map1: &HashMap<K, V>, map2: &HashMap<K, V>, mut f: impl FnMut(&V, &V) -> V, diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index 419b2e2..ecd0a69 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -598,6 +598,47 @@ fn type_last_layer( } Ok(RetTypeOnly(text_type)) } + BinOp(RightBiasedRecordMerge, l, r) => { + use crate::phase::normalize::merge_maps; + + let l_type = l.get_type()?; + let l_kind = l_type.get_type()?; + let r_type = r.get_type()?; + let r_kind = r_type.get_type()?; + + // Check the equality of kinds. + // This is to disallow expression such as: + // "{ x = Text } // { y = 1 }" + ensure_equal!( + l_kind, + r_kind, + mkerr(RecordMismatch(l.clone(), r.clone())), + ); + + // Extract the LHS record type + let kts_x = match l_type.to_value() { + Value::RecordType(kts) => kts, + _ => return Err(mkerr(MustCombineRecord(l.clone()))), + }; + + // Extract the RHS record type + let kts_y = match r_type.to_value() { + Value::RecordType(kts) => kts, + _ => return Err(mkerr(MustCombineRecord(r.clone()))), + }; + + // Union the two records, prefering + // the values found in the RHS. + let kts = merge_maps(&kts_x, &kts_y, |_, r_t| r_t.clone()); + + // Construct the final record type from the union + Ok(RetTypeOnly(tck_record_type( + ctx, + kts.iter() + .map(|(x, v)| Ok((x.clone(), v.to_type()))), + )? + .into_type())) + } BinOp(o @ ListAppend, l, r) => { match l.get_type()?.to_value() { Value::AppliedBuiltin(List, _) => {} @@ -622,6 +663,7 @@ fn type_last_layer( NaturalTimes => Natural, TextAppend => Text, ListAppend => unreachable!(), + RightBiasedRecordMerge => unreachable!(), _ => return Err(mkerr(Unimplemented)), })?; @@ -1135,11 +1177,11 @@ mod spec_tests { // 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"); - // ti_success!(ti_success_unit_RightBiasedRecordMergeTwoKinds, "unit/RightBiasedRecordMergeTwoKinds"); - // ti_success!(ti_success_unit_RightBiasedRecordMergeTwoTypes, "unit/RightBiasedRecordMergeTwoTypes"); + ti_success!(ti_success_unit_RightBiasedRecordMergeRhsEmpty, "unit/RightBiasedRecordMergeRhsEmpty"); + ti_success!(ti_success_unit_RightBiasedRecordMergeTwo, "unit/RightBiasedRecordMergeTwo"); + ti_success!(ti_success_unit_RightBiasedRecordMergeTwoDifferent, "unit/RightBiasedRecordMergeTwoDifferent"); + ti_success!(ti_success_unit_RightBiasedRecordMergeTwoKinds, "unit/RightBiasedRecordMergeTwoKinds"); + ti_success!(ti_success_unit_RightBiasedRecordMergeTwoTypes, "unit/RightBiasedRecordMergeTwoTypes"); ti_success!(ti_success_unit_SomeTrue, "unit/SomeTrue"); ti_success!(ti_success_unit_Text, "unit/Text"); ti_success!(ti_success_unit_TextLiteral, "unit/TextLiteral"); |