diff options
author | Fintan Halpenny | 2019-07-27 15:09:31 +0100 |
---|---|---|
committer | FintanH | 2019-07-31 10:35:03 +0100 |
commit | e51b89d717a1f1aaba7e59c79c9fb4b8e7031bab (patch) | |
tree | cef94e9c2c4af33555d457dcd7b19e91e1be185a /dhall/src/phase | |
parent | 2a6a37398394a33e281fa4f2055a3b33c21502c3 (diff) |
Add case for RightBasedRecordMerge in the typechecking phase.
The implementation checks the types and kinds of the LHS and RHS.
In the happy path it unions the HashMap prefering keys on the RHS over
the LHS, and the result is the type of the resulting HashMap.
The error cases are:
- If the kinds of the records differ it results in a RecordMismatch error.
- If either the LHS or RHS are not records it results in a
MustCombineRecord error.
Diffstat (limited to 'dhall/src/phase')
-rw-r--r-- | dhall/src/phase/typecheck.rs | 51 |
1 files changed, 46 insertions, 5 deletions
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index 419b2e2..2315edb 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) => { + 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 mut 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. + for (label, value) in kts_y { + kts_x.insert(label, value); + } + + // Construct the final record type from the union + Ok(RetTypeOnly(tck_record_type( + ctx, + kts_x.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, _) => {} @@ -1135,11 +1176,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"); |