diff options
| -rw-r--r-- | dhall/src/phase/normalize.rs | 75 | ||||
| -rw-r--r-- | dhall/src/phase/typecheck.rs | 37 | ||||
| -rw-r--r-- | tests_buffer | 4 |
3 files changed, 26 insertions, 90 deletions
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs index 0c4e185..28dc0f6 100644 --- a/dhall/src/phase/normalize.rs +++ b/dhall/src/phase/normalize.rs @@ -452,53 +452,20 @@ pub(crate) fn squash_textlit( ret } -/// 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 -} - -pub(crate) fn merge_maps<K, V>( +pub(crate) fn merge_maps<K, V, F, Err>( map1: &HashMap<K, V>, map2: &HashMap<K, V>, - mut f: impl FnMut(&V, &V) -> V, -) -> HashMap<K, V> + mut f: F, +) -> Result<HashMap<K, V>, Err> where + F: FnMut(&V, &V) -> Result<V, Err>, K: std::hash::Hash + Eq + Clone, V: Clone, { let mut kvs = HashMap::new(); for (x, v2) in map2 { let newv = if let Some(v1) = map1.get(x) { - f(v1, v2) + f(v1, v2)? } else { v2.clone() }; @@ -508,7 +475,7 @@ where // Insert only if key not already present kvs.entry(x.clone()).or_insert_with(|| v1.clone()); } - kvs + Ok(kvs) } fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> { @@ -518,8 +485,7 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> { RightBiasedRecordMerge, TextAppend, }; use ValueF::{ - BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType, - TextLit, + BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, TextLit, }; let x_borrow = x.as_whnf(); let y_borrow = y.as_whnf(); @@ -604,31 +570,16 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> { Ret::ValueRef(y) } (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => { - let kvs = merge_maps(kvs1, kvs2, |v1, v2| { - Value::from_valuef_untyped(ValueF::PartialExpr(ExprF::BinOp( - RecursiveRecordMerge, - v1.clone(), - v2.clone(), + let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |v1, v2| { + Ok(Value::from_valuef_untyped(ValueF::PartialExpr( + ExprF::BinOp(RecursiveRecordMerge, v1.clone(), v2.clone()), ))) - }); + })?; Ret::ValueF(RecordLit(kvs)) } - (RecursiveRecordTypeMerge, _, RecordType(kvs)) if kvs.is_empty() => { - Ret::ValueRef(x) - } - (RecursiveRecordTypeMerge, RecordType(kvs), _) if kvs.is_empty() => { - Ret::ValueRef(y) - } - (RecursiveRecordTypeMerge, RecordType(kvs1), RecordType(kvs2)) => { - let kvs = merge_maps(kvs1, kvs2, |v1, v2| { - Value::from_valuef_untyped(ValueF::PartialExpr(ExprF::BinOp( - RecursiveRecordTypeMerge, - v1.clone(), - v2.clone(), - ))) - }); - Ret::ValueF(RecordType(kvs)) + (RecursiveRecordTypeMerge, _, _) => { + unreachable!("This case should have been handled in typecheck") } (Equivalence, _, _) => { diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index abe05a3..363d733 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -567,7 +567,9 @@ fn type_last_layer( // Union the two records, prefering // the values found in the RHS. - let kts = merge_maps(kts_x, kts_y, |_, r_t| r_t.clone()); + let kts = merge_maps::<_, _, _, !>(kts_x, kts_y, |_, r_t| { + Ok(r_t.clone()) + })?; // Construct the final record type from the union RetTypeOnly(tck_record_type( @@ -584,25 +586,7 @@ fn type_last_layer( ), )?), BinOp(RecursiveRecordTypeMerge, l, r) => { - use crate::phase::normalize::intersection_with_key; - - // Extract the Const of the LHS - let k_l = match l.get_type()?.as_const() { - Some(k) => k, - _ => { - return mkerr(RecordTypeMergeRequiresRecordType(l.clone())) - } - }; - - // Extract the Const of the RHS - let k_r = match r.get_type()?.as_const() { - Some(k) => k, - _ => { - return mkerr(RecordTypeMergeRequiresRecordType(r.clone())) - } - }; - - let k = max(k_l, k_r); + use crate::phase::normalize::merge_maps; // Extract the LHS record type let borrow_l = l.as_whnf(); @@ -623,9 +607,11 @@ fn type_last_layer( }; // Ensure that the records combine without a type error - let kts = intersection_with_key( + let kts = merge_maps( + kts_x, + kts_y, // If the Label exists for both records, then we hit the recursive case. - |_: &Label, l: &Value, r: &Value| { + |l: &Value, r: &Value| { type_last_layer( ctx, ExprF::BinOp( @@ -635,12 +621,9 @@ fn type_last_layer( ), ) }, - kts_x, - kts_y, - ); - tck_record_type(ctx, kts.into_iter().map(|(x, v)| Ok((x, v?))))?; + )?; - RetTypeOnly(Value::from_const(k)) + RetWhole(tck_record_type(ctx, kts.into_iter().map(Ok))?) } BinOp(o @ ListAppend, l, r) => { match &*l.get_type()?.as_whnf() { diff --git a/tests_buffer b/tests_buffer index 15dc9c5..511ea49 100644 --- a/tests_buffer +++ b/tests_buffer @@ -32,7 +32,9 @@ variables across import boundaries typecheck: something that involves destructuring a recordtype after merge add some of the more complicated Prelude tests back, like List/enumerate -failure on old-style optional literal +success/ + regression/ + RecursiveRecordTypeMergeTripleCollision { x : { a : Bool } } ⩓ { x : { b : Bool } } ⩓ { x : { c : Bool } } failure/ merge { x = λ(x : Bool) → x } (< x: Bool | y: Natural >.x True) merge { x = λ(_ : Bool) → _, y = 1 } < x = True | y > |