From c27d8ff15988b914d21135dadffe9871441c127f Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 6 Feb 2020 16:34:08 +0000
Subject: Implement some record simplifications

---
 dhall/build.rs                       | 17 +++----
 dhall/src/semantics/nze/normalize.rs | 94 +++++++++++++++++++++++++++++++++++-
 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(_, _) => {
-- 
cgit v1.2.3