summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNadrieril2020-02-06 16:34:08 +0000
committerNadrieril2020-02-06 16:34:08 +0000
commitc27d8ff15988b914d21135dadffe9871441c127f (patch)
tree1f60a5f9007fc8a6df15873e55bf46ed2bd4ec26
parent853807b68a8ec8928a4d497fc7ce2b3676036eed (diff)
Implement some record simplifications
-rw-r--r--dhall/build.rs17
-rw-r--r--dhall/src/semantics/nze/normalize.rs94
2 files changed, 98 insertions, 13 deletions
diff --git a/dhall/build.rs b/dhall/build.rs
index b6c30be..83c154e 100644
--- a/dhall/build.rs
+++ b/dhall/build.rs
@@ -258,27 +258,22 @@ fn generate_tests() -> std::io::Result<()> {
|| path == "unit/RecordProjectionByTypeEmpty"
|| path == "unit/RecordProjectionByTypeNonEmpty"
|| path == "unit/RecordProjectionByTypeNormalizeProjection"
+ || path == "unit/RecordProjectionByTypeWithinFieldSelection"
+ || path == "unit/RecursiveRecordMergeWithinFieldSelection1"
+ || path == "unit/NestedRecordProjectionByType"
// TODO: fix Double/show
|| path == "prelude/JSON/number/1"
- // TODO: Further record simplifications
+ // TODO: doesn't typecheck
+ || path == "unit/RightBiasedRecordMergeWithinRecordProjection"
+ // // TODO: Further record simplifications
|| path == "simplifications/rightBiasedMergeWithinRecordProjectionWithinFieldSelection0"
|| path == "simplifications/rightBiasedMergeWithinRecordProjectionWithinFieldSelection1"
|| path == "simplifications/rightBiasedMergeWithinRecursiveRecordMergeWithinFieldselection"
|| path == "simplifications/issue661"
- || path == "unit/RecordProjectionByTypeWithinFieldSelection"
|| path == "unit/RecordProjectionWithinFieldSelection"
|| path == "unit/RecursiveRecordMergeWithinFieldSelection0"
- || path == "unit/RecursiveRecordMergeWithinFieldSelection1"
|| path == "unit/RecursiveRecordMergeWithinFieldSelection2"
|| path == "unit/RecursiveRecordMergeWithinFieldSelection3"
- || path == "unit/RightBiasedMergeWithinFieldSelection0"
- || path == "unit/RightBiasedMergeWithinFieldSelection1"
- || path == "unit/RightBiasedMergeWithinFieldSelection2"
- || path == "unit/RightBiasedMergeWithinFieldSelection3"
- || path == "unit/RightBiasedRecordMergeWithinRecordProjection"
- || path == "unit/RightBiasedMergeEquivalentArguments"
- || path == "unit/NestedRecordProjection"
- || path == "unit/NestedRecordProjectionByType"
// TODO: record completion
|| path == "simple/completion"
|| path == "unit/Completion"
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index fbb3647..a00b7ff 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -185,6 +185,7 @@ fn apply_binop<'a>(
}
Ret::ValueKind(RecordLit(kvs))
}
+ (RightBiasedRecordMerge, _, _) if x == y => Ret::ValueRef(y),
(RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => {
Ret::ValueRef(x)
@@ -244,8 +245,8 @@ pub(crate) fn normalize_one_layer(
) -> ValueKind {
use ValueKind::{
BoolLit, DoubleLit, EmptyListLit, EmptyOptionalLit, IntegerLit,
- NEListLit, NEOptionalLit, NaturalLit, RecordLit, RecordType,
- UnionConstructor, UnionLit, UnionType,
+ NEListLit, NEOptionalLit, NaturalLit, PartialExpr, RecordLit,
+ RecordType, UnionConstructor, UnionLit, UnionType,
};
let ret = match expr {
@@ -331,6 +332,13 @@ pub(crate) fn normalize_one_layer(
.filter_map(|l| kvs.get(l).map(|x| (l.clone(), x.clone())))
.collect(),
)),
+ PartialExpr(ExprKind::Projection(v2, _)) => {
+ return normalize_one_layer(
+ ExprKind::Projection(v2.clone(), ls.clone()),
+ ty,
+ env,
+ )
+ }
_ => Ret::Expr(expr),
},
ExprKind::Field(ref v, ref l) => match v.kind() {
@@ -343,6 +351,88 @@ pub(crate) fn normalize_one_layer(
kts.clone(),
v.get_type().unwrap(),
)),
+ PartialExpr(ExprKind::BinOp(
+ BinOp::RightBiasedRecordMerge,
+ x,
+ y,
+ )) => match (x.kind(), y.kind()) {
+ (_, RecordLit(kvs)) => match kvs.get(l) {
+ Some(r) => Ret::Value(r.clone()),
+ None => {
+ return normalize_one_layer(
+ ExprKind::Field(x.clone(), l.clone()),
+ ty,
+ env,
+ )
+ }
+ },
+ (RecordLit(kvs), _) => match kvs.get(l) {
+ Some(r) => Ret::Expr(ExprKind::Field(
+ Value::from_kind_and_type(
+ PartialExpr(ExprKind::BinOp(
+ BinOp::RightBiasedRecordMerge,
+ Value::from_kind_and_type(
+ RecordLit({
+ let mut kvs = HashMap::new();
+ kvs.insert(l.clone(), r.clone());
+ kvs
+ }),
+ Value::from_kind_and_type(
+ RecordType({
+ let mut kvs = HashMap::new();
+ kvs.insert(
+ l.clone(),
+ r.get_type_not_sort(),
+ );
+ kvs
+ }),
+ r.get_type_not_sort()
+ .get_type_not_sort(),
+ ),
+ ),
+ y.clone(),
+ )),
+ v.get_type_not_sort(),
+ ),
+ l.clone(),
+ )),
+ None => {
+ return normalize_one_layer(
+ ExprKind::Field(y.clone(), l.clone()),
+ ty,
+ env,
+ )
+ }
+ },
+ _ => Ret::Expr(expr),
+ },
+ PartialExpr(ExprKind::BinOp(
+ BinOp::RecursiveRecordTypeMerge,
+ x,
+ y,
+ )) => match (x.kind(), y.kind()) {
+ (RecordLit(kvs), _) => match kvs.get(l) {
+ Some(_) => Ret::Expr(expr),
+ None => {
+ return normalize_one_layer(
+ ExprKind::Field(y.clone(), l.clone()),
+ ty,
+ env,
+ )
+ }
+ },
+ (_, RecordLit(kvs)) => match kvs.get(l) {
+ Some(_) => Ret::Expr(expr),
+ None => {
+ return normalize_one_layer(
+ ExprKind::Field(x.clone(), l.clone()),
+ ty,
+ env,
+ )
+ }
+ },
+ _ => Ret::Expr(expr),
+ },
_ => Ret::Expr(expr),
},
ExprKind::ProjectionByExpr(_, _) => {