diff options
author | Nadrieril | 2019-04-19 22:22:58 +0200 |
---|---|---|
committer | Nadrieril | 2019-04-19 22:22:58 +0200 |
commit | 976647b1a887ee0753bf39dacd9528f62d9e086a (patch) | |
tree | 0ec9f2b19a2a0d661e8264324ac853375a5724c2 | |
parent | b127f516cde72cf3c090e8e01fe40c00d8e0ff9c (diff) |
Handle RecordLits fully semantically
Diffstat (limited to '')
-rw-r--r-- | dhall/src/normalize.rs | 44 |
1 files changed, 28 insertions, 16 deletions
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs index 955ac4f..bd479d0 100644 --- a/dhall/src/normalize.rs +++ b/dhall/src/normalize.rs @@ -240,10 +240,10 @@ where /// typechecking, but only construct `Value`s. /// /// Values usually store subexpressions unnormalized, to enable lazy normalization. They -/// approximate Weak Head Normal-Form (WHNF). This means that the expression is normalized -/// as little as possible, but just enough to know the first constructor of the -/// normal form. This is identical to full normalization for simple types like integers, -/// but for example for a record literal this means only knowing the field names. +/// approximate what's called Weak Head Normal-Form (WHNF). This means that the expression is +/// normalized as little as possible, but just enough to know the first constructor of the normal +/// form. This is identical to full normalization for simple types like integers, but for example +/// for a record literal this means knowing just the field names. #[derive(Debug, Clone)] enum Value { Closure(Closure), @@ -557,6 +557,27 @@ fn normalize_last_layer( Field(Value::UnionType(ctx, kts), l) => { return Value::Closure(Closure::UnionConstructor(ctx, l, kts)) } + Field(Value::RecordLit(record_ctx, mut kvs), l) => match kvs.remove(&l) + { + Some(r) => return normalize_value(&record_ctx, r), + // Return ownership + None => Field(Value::RecordLit(record_ctx, kvs), l), + }, + // Always simplify `x.{}` to `{}` + Projection(_, ls) if ls.is_empty() => { + return Value::RecordLit( + ctx.clone(), + std::collections::BTreeMap::new(), + ) + } + Projection(Value::RecordLit(record_ctx, mut kvs), ls) => { + return Value::RecordLit( + record_ctx, + ls.into_iter() + .filter_map(|l| kvs.remove(&l).map(|x| (l, x))) + .collect(), + ) + } Merge( Value::RecordLit(record_ctx, mut handlers), Value::Closure(Closure::UnionConstructor(ctor_ctx, l, kts)), @@ -615,19 +636,10 @@ fn normalize_last_layer( None => DoneAsIs, } } - Field(RecordLit(kvs), l) => match kvs.get(&l) { - Some(r) => DoneRefSub(r), - None => DoneAsIs, - }, + Field(RecordLit(_), _) => unreachable!(), Field(UnionType(_), _) => unreachable!(), - Projection(_, ls) if ls.is_empty() => { - Done(RecordLit(std::collections::BTreeMap::new())) - } - Projection(RecordLit(kvs), ls) => Done(RecordLit( - ls.iter() - .filter_map(|l| kvs.get(l).map(|x| (l.clone(), x.clone()))) - .collect(), - )), + Projection(_, ls) if ls.is_empty() => unreachable!(), + Projection(RecordLit(_), _) => unreachable!(), _ => DoneAsIs, }; |