summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
authorNadrieril2019-08-23 18:34:43 +0200
committerNadrieril2019-08-23 18:34:43 +0200
commitd9e3bcca9b4350cbc1db2545d7ed28dde4e12be4 (patch)
treeb687609166402035fc93e154d385d2d18e8ceae7 /dhall
parente8a9178ebe4860a8a00a6ec8f77b661fdad84890 (diff)
Keep type information after RecursiveRecordTypeMerge
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/phase/normalize.rs75
-rw-r--r--dhall/src/phase/typecheck.rs37
2 files changed, 23 insertions, 89 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() {