From b127f516cde72cf3c090e8e01fe40c00d8e0ff9c Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 19 Apr 2019 21:53:21 +0200
Subject: Split function in two phases

---
 dhall/src/normalize.rs | 36 ++++++++++++++++++++++++------------
 1 file changed, 24 insertions(+), 12 deletions(-)

(limited to 'dhall')

diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 805ee4d..955ac4f 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -238,6 +238,12 @@ where
 /// be limited to syntactic expressions: either written by the user or meant to be printed.
 /// The rule is the following: we must _not_ construct values of type `Expr` while normalizing or
 /// 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.
 #[derive(Debug, Clone)]
 enum Value {
     Closure(Closure),
@@ -492,9 +498,6 @@ fn reval(ctx: &NormalizationContext, expr: OutputSubExpr) -> Value {
 }
 
 fn normalize_value(ctx: &NormalizationContext, expr: InputSubExpr) -> Value {
-    use dhall_core::BinOp::*;
-    use dhall_core::ExprF::*;
-
     let e = match expr.as_ref() {
         ExprF::Let(x, _, r, b) => {
             let r = normalize_value(ctx, r.clone());
@@ -534,6 +537,18 @@ fn normalize_value(ctx: &NormalizationContext, expr: InputSubExpr) -> Value {
             Label::clone,
         );
 
+    normalize_last_layer(ctx, expr)
+}
+
+/// When all sub-expressions have been (partially) normalized, eval the remaining toplevel layer.
+fn normalize_last_layer(
+    ctx: &NormalizationContext,
+    expr: ExprF<Value, Label, X, Normalized<'static>>,
+) -> Value {
+    use dhall_core::BinOp::*;
+    use dhall_core::ExprF::*;
+    use WhatNext::*;
+
     let expr = match expr {
         Var(v) => return ctx.lookup(&v),
         Annot(x, _) => return x,
@@ -548,14 +563,12 @@ fn normalize_value(ctx: &NormalizationContext, expr: InputSubExpr) -> Value {
             t,
         ) => match handlers.remove(&l) {
             Some(h) => return normalize_value(ctx, h),
-            None => {
-                return Value::Expr(rc(Merge(
-                    Value::RecordLit(record_ctx, handlers).normalize_to_expr(),
-                    Value::Closure(Closure::UnionConstructor(ctor_ctx, l, kts))
-                        .normalize_to_expr(),
-                    t.map(|t| t.normalize_to_expr()),
-                )))
-            }
+            // Return ownership
+            None => Merge(
+                Value::RecordLit(record_ctx, handlers),
+                Value::Closure(Closure::UnionConstructor(ctor_ctx, l, kts)),
+                t,
+            ),
         },
         expr => expr,
     };
@@ -563,7 +576,6 @@ fn normalize_value(ctx: &NormalizationContext, expr: InputSubExpr) -> Value {
     let expr: ExprF<Expr<X, X>, Label, X, Normalized<'static>> =
         expr.map_ref_simple(|e| e.clone().normalize_to_expr().unroll());
 
-    use WhatNext::*;
     let what_next = match &expr {
         Embed(e) => DoneRefSub(&e.0),
         Annot(_, _) => unreachable!(),
-- 
cgit v1.2.3