summaryrefslogtreecommitdiff
path: root/dhall/src
diff options
context:
space:
mode:
authorFintanH2019-07-31 12:05:48 +0100
committerFintanH2019-08-01 00:03:32 +0100
commita53fc6e6767bba80bf1697d732d88c4a1e0e9e42 (patch)
tree34fb4f39e4dd90f75c48f1f70065f25b6fadcd56 /dhall/src
parent2a6a37398394a33e281fa4f2055a3b33c21502c3 (diff)
Add the typechecking of RecursiveRecordMerge.
This introduces an external function for HashMaps to perform an outer join so that you can do a unionWith but with more power by having a new tagert type. Using outer_join and recursively looking through records of records we have an implementation for combining records.
Diffstat (limited to '')
-rw-r--r--dhall/src/error/mod.rs3
-rw-r--r--dhall/src/phase/normalize.rs53
-rw-r--r--dhall/src/phase/typecheck.rs81
3 files changed, 129 insertions, 8 deletions
diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs
index 125d013..2345348 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),
@@ -63,6 +64,7 @@ pub(crate) enum TypeMessage {
IfBranchMustBeTerm(bool, Typed),
InvalidFieldType(Label, Type),
NotARecord(Label, Normalized),
+ MustCombineRecord(Typed),
MissingRecordField(Label, Typed),
MissingUnionField(Label, Normalized),
BinOpTypeMismatch(BinOp, Typed),
@@ -78,6 +80,7 @@ pub(crate) enum TypeMessage {
MergeHandlerReturnTypeMustNotBeDependent,
ProjectionMustBeRecord,
ProjectionMissingEntry,
+ RecordMismatch(Typed, Typed),
Sort,
RecordTypeDuplicateField,
UnionTypeDuplicateField,
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index be2ba51..e3c5d68 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -372,6 +372,59 @@ enum Ret<'a> {
Expr(ExprF<Thunk, X>),
}
+/// Performs an outer join of two HashMaps.
+///
+/// # Arguments
+///
+/// * `ft` - Will convert the values of the first map
+/// into the target value.
+///
+/// * `fu` - Will convert the values of the second map
+/// into the target value.
+///
+/// * `ftu` - Will convert the key and values from both maps
+/// into the target type.
+///
+/// # Description
+///
+/// If the key is present in both maps then the final value for
+/// that key is computed via the `ftu` function. Otherwise, the
+/// final value will be calculated by either the `ft` or `fu` value
+/// depending on which map the key is present in.
+///
+/// The final map will contain all keys from the two input maps with
+/// also values computed as per above.
+pub(crate) fn outer_join<K, T, U, V>(
+ mut ft: impl FnMut(&T) -> V,
+ mut fu: impl FnMut(&U) -> V,
+ mut ftu: 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 kus = HashMap::new();
+ for (k1, t) in map1 {
+ let v = if let Some(u) = map2.get(k1) {
+ // The key exists in both maps
+ // so use all values for computation
+ ftu(k1, t, u)
+ } else {
+ // Key only exists in map1
+ ft(t)
+ };
+ kus.insert(k1.clone(), v);
+ }
+
+ for (k1, u) in map2 {
+ // Insert if key was missing in map1
+ kus.entry(k1.clone()).or_insert(fu(u));
+ }
+
+ kus
+}
+
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..7aaee42 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -598,6 +598,71 @@ fn type_last_layer(
}
Ok(RetTypeOnly(text_type))
}
+ BinOp(RecursiveRecordMerge, 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::outer_join;
+
+ // 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, inner_l: &TypeThunk, inner_r: &TypeThunk|
+ -> Result<Typed, TypeError> {
+ match (inner_l.to_value(), inner_r.to_value()) {
+ (Value::RecordType(inner_l_kvs), Value::RecordType(inner_r_kvs)) =>
+ combine_record_types(ctx, inner_l_kvs, inner_r_kvs),
+ (_, _) => Err(TypeError::new(ctx, FieldCollision(k.clone()))),
+ }
+ };
+
+ let kts: HashMap<Label, Result<Typed, TypeError>> = outer_join(
+ |l| Ok(l.to_type()),
+ |r| Ok(r.to_type()),
+ |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())
+ };
+
+ 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()))),
+ };
+
+ combine_record_types(ctx, kts_x, kts_y).map(|r| RetTypeOnly(r))
+ }
BinOp(o @ ListAppend, l, r) => {
match l.get_type()?.to_value() {
Value::AppliedBuiltin(List, _) => {}
@@ -1120,14 +1185,14 @@ mod spec_tests {
ti_success!(ti_success_unit_RecordTypeNestedKind, "unit/RecordTypeNestedKind");
ti_success!(ti_success_unit_RecordTypeNestedKindLike, "unit/RecordTypeNestedKindLike");
ti_success!(ti_success_unit_RecordTypeType, "unit/RecordTypeType");
- // ti_success!(ti_success_unit_RecursiveRecordMergeLhsEmpty, "unit/RecursiveRecordMergeLhsEmpty");
- // ti_success!(ti_success_unit_RecursiveRecordMergeRecursively, "unit/RecursiveRecordMergeRecursively");
- // ti_success!(ti_success_unit_RecursiveRecordMergeRecursivelyKinds, "unit/RecursiveRecordMergeRecursivelyKinds");
- // ti_success!(ti_success_unit_RecursiveRecordMergeRecursivelyTypes, "unit/RecursiveRecordMergeRecursivelyTypes");
- // ti_success!(ti_success_unit_RecursiveRecordMergeRhsEmpty, "unit/RecursiveRecordMergeRhsEmpty");
- // 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_RecursiveRecordMergeLhsEmpty, "unit/RecursiveRecordMergeLhsEmpty");
+ ti_success!(ti_success_unit_RecursiveRecordMergeRecursively, "unit/RecursiveRecordMergeRecursively");
+ ti_success!(ti_success_unit_RecursiveRecordMergeRecursivelyKinds, "unit/RecursiveRecordMergeRecursivelyKinds");
+ ti_success!(ti_success_unit_RecursiveRecordMergeRecursivelyTypes, "unit/RecursiveRecordMergeRecursivelyTypes");
+ ti_success!(ti_success_unit_RecursiveRecordMergeRhsEmpty, "unit/RecursiveRecordMergeRhsEmpty");
+ 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");