From 700ff482fbff8960bc0e792fec6fd538c5428d70 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 24 Jan 2020 17:07:56 +0000
Subject: Normalize more expressions

---
 dhall/src/semantics/core/value.rs      |  6 +++++-
 dhall/src/semantics/phase/normalize.rs | 13 +++++--------
 2 files changed, 10 insertions(+), 9 deletions(-)

diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs
index 3798053..3e3bfe1 100644
--- a/dhall/src/semantics/core/value.rs
+++ b/dhall/src/semantics/core/value.rs
@@ -10,7 +10,7 @@ use crate::semantics::phase::typecheck::{builtin_to_value, const_to_value};
 use crate::semantics::phase::{
     Normalized, NormalizedExpr, ToExprOptions, Typed,
 };
-use crate::semantics::{TyExpr, TyExprKind, Type};
+use crate::semantics::{TyExpr, TyExprKind};
 use crate::syntax::{
     BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label,
     NaiveDouble, Natural, Span,
@@ -235,6 +235,10 @@ impl Value {
                 v.check_type(t);
                 e.subst_shift(&AlphaVar::default(), &v)
             }
+            ValueKind::PiClosure { annot, closure, .. } => {
+                v.check_type(annot);
+                closure.apply(v.clone())
+            }
             _ => unreachable!("Internal type error"),
         };
         Value::from_kind_and_type_whnf(
diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs
index 8f3953d..ac60ce0 100644
--- a/dhall/src/semantics/phase/normalize.rs
+++ b/dhall/src/semantics/phase/normalize.rs
@@ -594,10 +594,14 @@ fn apply_binop<'a>(
             Ret::ValueKind(RecordLit(kvs))
         }
 
-        (RecursiveRecordTypeMerge, _, _) | (Equivalence, _, _) => {
+        (RecursiveRecordTypeMerge, _, _) => {
             unreachable!("This case should have been handled in typecheck")
         }
 
+        (Equivalence, _, _) => {
+            Ret::ValueKind(ValueKind::Equivalence(x.clone(), y.clone()))
+        }
+
         _ => return None,
     })
 }
@@ -690,13 +694,6 @@ pub(crate) fn normalize_one_layer(
                 }
             }
         }
-        // ExprKind::BinOp(RecursiveRecordTypeMerge, l, r) => { }
-        // ExprKind::BinOp(Equivalence, l, r) => {
-        //     RetWhole(Value::from_kind_and_type(
-        //         ValueKind::Equivalence(l.clone(), r.clone()),
-        //         Value::from_const(Type),
-        //     ))
-        // }
         ExprKind::BinOp(o, ref x, ref y) => match apply_binop(o, x, y, ty) {
             Some(ret) => ret,
             None => Ret::Expr(expr),
-- 
cgit v1.2.3