From d1f828961bccf9627ef4fb76ca528f039d180ff7 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 21 Apr 2019 11:30:58 +0200
Subject: Embrace TypeInternal as a semantic value

---
 dhall/src/normalize.rs | 1 +
 1 file changed, 1 insertion(+)

(limited to 'dhall/src/normalize.rs')

diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index f092c4d..7aa8686 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -322,6 +322,7 @@ enum WHNF {
         (NormalizationContext, BTreeMap<Label, Option<InputSubExpr>>),
     ),
     TextLit(Vec<InterpolatedTextContents<Now>>),
+    /// This must not contain a value captured by one of the variants above.
     Expr(OutputSubExpr),
 }
 
-- 
cgit v1.2.3


From ecff0ecd47bb38937fb43e60b8d78ea92e2af01c Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 21 Apr 2019 22:52:00 +0200
Subject: Prepare for interop between two contexts

---
 dhall/src/normalize.rs | 54 ++++++++++++++++++++++++++++++++++----------------
 1 file changed, 37 insertions(+), 17 deletions(-)

(limited to 'dhall/src/normalize.rs')

diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 7aa8686..c17ed78 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -229,7 +229,21 @@ fn apply_builtin(b: Builtin, args: Vec<WHNF>) -> WHNF {
 #[derive(Debug, Clone)]
 enum EnvItem {
     Expr(WHNF),
-    Skip(usize),
+    Skip(V<Label>),
+}
+
+impl EnvItem {
+    fn shift0(&self, delta: isize, x: &Label) -> Self {
+        use EnvItem::*;
+        match self {
+            Expr(e) => {
+                let mut e = e.clone();
+                e.shift0(delta, x);
+                Expr(e)
+            }
+            Skip(var) => Skip(var.shift0(delta, x)),
+        }
+    }
 }
 
 #[derive(Debug, Clone)]
@@ -247,30 +261,36 @@ impl NormalizationContext {
     fn skip(&self, x: &Label) -> Self {
         NormalizationContext(Rc::new(
             self.0
-                .map(|l, e| {
-                    use EnvItem::*;
-                    match e {
-                        Expr(e) => {
-                            let mut e = e.clone();
-                            e.shift0(1, x);
-                            Expr(e)
-                        }
-                        Skip(n) if l == x => Skip(*n + 1),
-                        Skip(n) => Skip(*n),
-                    }
-                })
-                .insert(x.clone(), EnvItem::Skip(0)),
+                .map(|_, e| e.shift0(1, x))
+                .insert(x.clone(), EnvItem::Skip(V(x.clone(), 0))),
         ))
     }
     fn lookup(&self, var: &V<Label>) -> WHNF {
         let V(x, n) = var;
         match self.0.lookup(x, *n) {
             Some(EnvItem::Expr(e)) => e.clone(),
-            Some(EnvItem::Skip(m)) => {
-                WHNF::Expr(rc(ExprF::Var(V(x.clone(), *m))))
+            Some(EnvItem::Skip(newvar)) => {
+                WHNF::Expr(rc(ExprF::Var(newvar.clone())))
+            }
+            None => WHNF::Expr(rc(ExprF::Var(var.clone()))),
+        }
+    }
+    fn from_typecheck_ctx(tc_ctx: &crate::typecheck::TypecheckContext) -> Self {
+        use crate::typecheck::EnvItem::*;
+        let mut ctx = Context::new();
+        for (k, vs) in tc_ctx.0.iter_keys() {
+            for v in vs.iter().rev() {
+                let new_item = match v {
+                    Type(var, _) => EnvItem::Skip(var.clone()),
+                    Value(e) => EnvItem::Expr(normalize_whnf(
+                        NormalizationContext::new(),
+                        e.as_expr().embed_absurd(),
+                    )),
+                };
+                ctx = ctx.insert(k.clone(), new_item);
             }
-            None => WHNF::Expr(rc(ExprF::Var(V(x.clone(), *n)))),
         }
+        NormalizationContext(Rc::new(ctx))
     }
 }
 
-- 
cgit v1.2.3


From 316c6ea1c5512bcc9e0a07aa63fd086eb313abc5 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 22 Apr 2019 00:07:50 +0200
Subject: Avoid shift_subst in typecheck

---
 dhall/src/normalize.rs | 16 +++++++++++++++-
 1 file changed, 15 insertions(+), 1 deletion(-)

(limited to 'dhall/src/normalize.rs')

diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index c17ed78..0301e35 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -18,6 +18,20 @@ impl<'a> Typed<'a> {
     pub fn normalize(self) -> Normalized<'a> {
         Normalized(normalize(self.0), self.1, self.2)
     }
+    pub fn normalize_ctx(
+        self,
+        ctx: &crate::typecheck::TypecheckContext,
+    ) -> Normalized<'a> {
+        Normalized(
+            normalize_whnf(
+                NormalizationContext::from_typecheck_ctx(ctx),
+                self.0,
+            )
+            .normalize_to_expr(),
+            self.1,
+            self.2,
+        )
+    }
     /// Pretends this expression is normalized. Use with care.
     #[allow(dead_code)]
     pub fn skip_normalize(self) -> Normalized<'a> {
@@ -279,7 +293,7 @@ impl NormalizationContext {
         use crate::typecheck::EnvItem::*;
         let mut ctx = Context::new();
         for (k, vs) in tc_ctx.0.iter_keys() {
-            for v in vs.iter().rev() {
+            for v in vs.iter() {
                 let new_item = match v {
                     Type(var, _) => EnvItem::Skip(var.clone()),
                     Value(e) => EnvItem::Expr(normalize_whnf(
-- 
cgit v1.2.3


From a5c94605e29f3694928d6e03de325c0c81fee7b2 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 22 Apr 2019 00:56:47 +0200
Subject: Store context in Typed

---
 dhall/src/normalize.rs | 21 +++++++--------------
 1 file changed, 7 insertions(+), 14 deletions(-)

(limited to 'dhall/src/normalize.rs')

diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 0301e35..35a6b23 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -16,20 +16,13 @@ type OutputSubExpr = SubExpr<X, X>;
 
 impl<'a> Typed<'a> {
     pub fn normalize(self) -> Normalized<'a> {
-        Normalized(normalize(self.0), self.1, self.2)
-    }
-    pub fn normalize_ctx(
-        self,
-        ctx: &crate::typecheck::TypecheckContext,
-    ) -> Normalized<'a> {
         Normalized(
-            normalize_whnf(
-                NormalizationContext::from_typecheck_ctx(ctx),
+            normalize(
+                NormalizationContext::from_typecheck_ctx(&self.2),
                 self.0,
-            )
-            .normalize_to_expr(),
+            ),
             self.1,
-            self.2,
+            self.3,
         )
     }
     /// Pretends this expression is normalized. Use with care.
@@ -38,7 +31,7 @@ impl<'a> Typed<'a> {
         Normalized(
             self.0.unroll().squash_embed(|e| e.0.clone()),
             self.1,
-            self.2,
+            self.3,
         )
     }
 }
@@ -832,8 +825,8 @@ fn normalize_last_layer(expr: ExprF<WHNF, Label, X, X>) -> WHNF {
 /// However, `normalize` will not fail if the expression is ill-typed and will
 /// leave ill-typed sub-expressions unevaluated.
 ///
-fn normalize(e: InputSubExpr) -> OutputSubExpr {
-    normalize_whnf(NormalizationContext::new(), e).normalize_to_expr()
+fn normalize(ctx: NormalizationContext, e: InputSubExpr) -> OutputSubExpr {
+    normalize_whnf(ctx, e).normalize_to_expr()
 }
 
 #[cfg(test)]
-- 
cgit v1.2.3


From 79bb6533ecb60cea40ff743b9651833b833eebde Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 25 Apr 2019 19:45:44 +0200
Subject: Respect import boundary in normalization

---
 dhall/src/normalize.rs | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'dhall/src/normalize.rs')

diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 35a6b23..2222f18 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -639,7 +639,9 @@ fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> WHNF {
         ExprF::Annot(x, _) => normalize_whnf(ctx, x.clone()),
         ExprF::Note(_, e) => normalize_whnf(ctx, e.clone()),
         // TODO: wasteful to retraverse everything
-        ExprF::Embed(e) => normalize_whnf(ctx, e.0.embed_absurd()),
+        ExprF::Embed(e) => {
+            normalize_whnf(NormalizationContext::new(), e.0.embed_absurd())
+        }
         ExprF::Let(x, _, r, b) => {
             let r = normalize_whnf(ctx.clone(), r.clone());
             normalize_whnf(ctx.insert(x, r), b.clone())
-- 
cgit v1.2.3


From 7517610921935727218e94d4ec8116c15e3419ac Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 27 Apr 2019 15:24:57 +0200
Subject: Using only shift0 was not such a great idea

---
 dhall/src/normalize.rs | 42 +++++++++++++++++++-----------------------
 1 file changed, 19 insertions(+), 23 deletions(-)

(limited to 'dhall/src/normalize.rs')

diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 2222f18..7d19ec0 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -36,10 +36,6 @@ impl<'a> Typed<'a> {
     }
 }
 
-fn shift0_mut<N, E>(delta: isize, label: &Label, in_expr: &mut SubExpr<N, E>) {
-    let new_expr = shift0(delta, label, &in_expr);
-    std::mem::replace(in_expr, new_expr);
-}
 
 fn shift_mut<N, E>(delta: isize, var: &V<Label>, in_expr: &mut SubExpr<N, E>) {
     let new_expr = shift(delta, var, &in_expr);
@@ -245,7 +241,7 @@ impl EnvItem {
         match self {
             Expr(e) => {
                 let mut e = e.clone();
-                e.shift0(delta, x);
+                e.shift(delta, &V(x.clone(), 0));
                 Expr(e)
             }
             Skip(var) => Skip(var.shift0(delta, x)),
@@ -537,7 +533,7 @@ impl WHNF {
         WHNF::AppliedBuiltin(b, vec![])
     }
 
-    fn shift0(&mut self, delta: isize, label: &Label) {
+    fn shift(&mut self, delta: isize, var: &V<Label>) {
         match self {
             WHNF::NaturalSuccClosure
             | WHNF::BoolLit(_)
@@ -547,54 +543,54 @@ impl WHNF {
             | WHNF::NEOptionalLit(n)
             | WHNF::OptionalSomeClosure(n)
             | WHNF::EmptyListLit(n) => {
-                n.shift0(delta, label);
+                n.shift(delta, var);
             }
-            WHNF::Lam(_, t, (_, e)) => {
-                t.shift0(delta, label);
-                shift_mut(delta, &V(label.clone(), 1), e);
+            WHNF::Lam(x, t, (_, e)) => {
+                t.shift(delta, var);
+                shift_mut(delta, &var.shift0(1, x), e);
             }
             WHNF::AppliedBuiltin(_, args) => {
                 for x in args.iter_mut() {
-                    x.shift0(delta, label);
+                    x.shift(delta, var);
                 }
             }
             WHNF::ListConsClosure(t, v) => {
-                t.shift0(delta, label);
+                t.shift(delta, var);
                 for x in v.iter_mut() {
-                    x.shift0(delta, label);
+                    x.shift(delta, var);
                 }
             }
             WHNF::NEListLit(elts) => {
                 for x in elts.iter_mut() {
-                    x.shift0(delta, label);
+                    x.shift(delta, var);
                 }
             }
             WHNF::RecordLit(kvs) | WHNF::RecordType(kvs) => {
                 for x in kvs.values_mut() {
-                    x.shift0(delta, label);
+                    x.shift(delta, var);
                 }
             }
             WHNF::UnionType(_, kts) | WHNF::UnionConstructor(_, _, kts) => {
                 for x in kts.values_mut().flat_map(|opt| opt) {
-                    shift0_mut(delta, label, x);
+                    shift_mut(delta, var, x);
                 }
             }
             WHNF::UnionLit(_, v, (_, kts)) => {
-                v.shift0(delta, label);
+                v.shift(delta, var);
                 for x in kts.values_mut().flat_map(|opt| opt) {
-                    shift0_mut(delta, label, x);
+                    shift_mut(delta, var, x);
                 }
             }
             WHNF::TextLit(elts) => {
                 for x in elts.iter_mut() {
                     use InterpolatedTextContents::{Expr, Text};
                     match x {
-                        Expr(n) => n.shift0(delta, label),
+                        Expr(n) => n.shift(delta, var),
                         Text(_) => {}
                     }
                 }
             }
-            WHNF::Expr(e) => shift0_mut(delta, label, e),
+            WHNF::Expr(e) => shift_mut(delta, var, e),
         }
     }
 }
@@ -624,10 +620,10 @@ impl Now {
         }
     }
 
-    fn shift0(&mut self, delta: isize, label: &Label) {
+    fn shift(&mut self, delta: isize, var: &V<Label>) {
         match self {
-            Now::Normalized(v) => v.shift0(delta, label),
-            Now::Unnormalized(_, e) => shift0_mut(delta, label, e),
+            Now::Normalized(v) => v.shift(delta, var),
+            Now::Unnormalized(_, e) => shift_mut(delta, var, e),
         }
     }
 }
-- 
cgit v1.2.3


From a987d01a8d1248f35ba19babb66aebabfad47a6d Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 27 Apr 2019 15:28:16 +0200
Subject: Define new intermediate expression type

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

(limited to 'dhall/src/normalize.rs')

diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 7d19ec0..14b062f 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -9,15 +9,27 @@ use dhall_core::{
 };
 use dhall_generator as dhall;
 
-use crate::expr::{Normalized, Typed};
+use crate::expr::{Normalized, PartiallyNormalized, Typed};
 
 type InputSubExpr = SubExpr<X, Normalized<'static>>;
 type OutputSubExpr = SubExpr<X, X>;
 
 impl<'a> Typed<'a> {
+    /// Reduce an expression to its normal form, performing beta reduction
+    ///
+    /// `normalize` does not type-check the expression.  You may want to type-check
+    /// expressions before normalizing them since normalization can convert an
+    /// ill-typed expression into a well-typed expression.
+    ///
+    /// However, `normalize` will not fail if the expression is ill-typed and will
+    /// leave ill-typed sub-expressions unevaluated.
+    ///
     pub fn normalize(self) -> Normalized<'a> {
-        Normalized(
-            normalize(
+        self.normalize_whnf().normalize()
+    }
+    pub(crate) fn normalize_whnf(self) -> PartiallyNormalized<'a> {
+        PartiallyNormalized(
+            normalize_whnf(
                 NormalizationContext::from_typecheck_ctx(&self.2),
                 self.0,
             ),
@@ -36,6 +48,24 @@ impl<'a> Typed<'a> {
     }
 }
 
+impl<'a> PartiallyNormalized<'a> {
+    pub(crate) fn normalize(self) -> Normalized<'a> {
+        Normalized(
+            self.0.normalize_to_expr(),
+            self.1,
+            self.2,
+        )
+    }
+    pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+        let mut e = self.0.clone();
+        e.shift(delta, var);
+        PartiallyNormalized(
+            e,
+            self.1.as_ref().map(|x| x.shift(delta, var)),
+            self.2,
+        )
+    }
+}
 
 fn shift_mut<N, E>(delta: isize, var: &V<Label>, in_expr: &mut SubExpr<N, E>) {
     let new_expr = shift(delta, var, &in_expr);
@@ -250,7 +280,7 @@ impl EnvItem {
 }
 
 #[derive(Debug, Clone)]
-struct NormalizationContext(Rc<Context<Label, EnvItem>>);
+pub(crate) struct NormalizationContext(Rc<Context<Label, EnvItem>>);
 
 impl NormalizationContext {
     fn new() -> Self {
@@ -312,7 +342,7 @@ impl NormalizationContext {
 /// subexpression has its own context, but in practice some contexts can be shared when sensible, to
 /// avoid unnecessary allocations.
 #[derive(Debug, Clone)]
-enum WHNF {
+pub(crate) enum WHNF {
     /// Closures
     Lam(Label, Now, (NormalizationContext, InputSubExpr)),
     AppliedBuiltin(Builtin, Vec<WHNF>),
@@ -599,7 +629,7 @@ impl WHNF {
 /// non-normalized value alongside a normalization context.
 /// The name is a pun on std::borrow::Cow.
 #[derive(Debug, Clone)]
-enum Now {
+pub(crate) enum Now {
     Normalized(Box<WHNF>),
     Unnormalized(NormalizationContext, InputSubExpr),
 }
@@ -814,19 +844,6 @@ fn normalize_last_layer(expr: ExprF<WHNF, Label, X, X>) -> WHNF {
     }
 }
 
-/// Reduce an expression to its normal form, performing beta reduction
-///
-/// `normalize` does not type-check the expression.  You may want to type-check
-/// expressions before normalizing them since normalization can convert an
-/// ill-typed expression into a well-typed expression.
-///
-/// However, `normalize` will not fail if the expression is ill-typed and will
-/// leave ill-typed sub-expressions unevaluated.
-///
-fn normalize(ctx: NormalizationContext, e: InputSubExpr) -> OutputSubExpr {
-    normalize_whnf(ctx, e).normalize_to_expr()
-}
-
 #[cfg(test)]
 mod spec_tests {
     #![rustfmt::skip]
-- 
cgit v1.2.3


From f10dd510adc8ba292bd2fa1810497ff6cf42f81c Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 27 Apr 2019 15:30:11 +0200
Subject: Rename Now to Thunk

---
 dhall/src/normalize.rs | 89 +++++++++++++++++++++++++-------------------------
 1 file changed, 44 insertions(+), 45 deletions(-)

(limited to 'dhall/src/normalize.rs')

diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 14b062f..f3b0979 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -78,7 +78,7 @@ fn apply_builtin(b: Builtin, args: Vec<WHNF>) -> WHNF {
 
     let ret = match b {
         OptionalNone => improved_slice_patterns::match_vec!(args;
-            [t] => EmptyOptionalLit(Now::from_whnf(t)),
+            [t] => EmptyOptionalLit(Thunk::from_whnf(t)),
         ),
         NaturalIsZero => improved_slice_patterns::match_vec!(args;
             [NaturalLit(n)] => BoolLit(n == 0),
@@ -126,12 +126,12 @@ fn apply_builtin(b: Builtin, args: Vec<WHNF>) -> WHNF {
                 let mut kts = BTreeMap::new();
                 kts.insert(
                     "index".into(),
-                    Now::from_whnf(
+                    Thunk::from_whnf(
                         WHNF::from_builtin(Natural)
                     ),
                 );
                 kts.insert("value".into(), t);
-                EmptyListLit(Now::from_whnf(RecordType(kts)))
+                EmptyListLit(Thunk::from_whnf(RecordType(kts)))
             },
             [_, NEListLit(xs)] => {
                 let xs = xs
@@ -140,9 +140,9 @@ fn apply_builtin(b: Builtin, args: Vec<WHNF>) -> WHNF {
                     .map(|(i, e)| {
                         let i = NaturalLit(i);
                         let mut kvs = BTreeMap::new();
-                        kvs.insert("index".into(), Now::from_whnf(i));
+                        kvs.insert("index".into(), Thunk::from_whnf(i));
                         kvs.insert("value".into(), e);
-                        Now::from_whnf(RecordLit(kvs))
+                        Thunk::from_whnf(RecordLit(kvs))
                     })
                     .collect();
                 NEListLit(xs)
@@ -161,8 +161,8 @@ fn apply_builtin(b: Builtin, args: Vec<WHNF>) -> WHNF {
             },
             [t, g] => g
                 .app(WHNF::from_builtin(List).app(t.clone()))
-                .app(ListConsClosure(Now::from_whnf(t.clone()), None))
-                .app(EmptyListLit(Now::from_whnf(t))),
+                .app(ListConsClosure(Thunk::from_whnf(t.clone()), None))
+                .app(EmptyListLit(Thunk::from_whnf(t))),
         ),
         ListFold => improved_slice_patterns::match_vec!(args;
             // fold/build fusion
@@ -195,8 +195,8 @@ fn apply_builtin(b: Builtin, args: Vec<WHNF>) -> WHNF {
             },
             [t, g] => g
                 .app(WHNF::from_builtin(Optional).app(t.clone()))
-                .app(OptionalSomeClosure(Now::from_whnf(t.clone())))
-                .app(EmptyOptionalLit(Now::from_whnf(t))),
+                .app(OptionalSomeClosure(Thunk::from_whnf(t.clone())))
+                .app(EmptyOptionalLit(Thunk::from_whnf(t))),
         ),
         OptionalFold => improved_slice_patterns::match_vec!(args;
             // fold/build fusion
@@ -344,25 +344,25 @@ impl NormalizationContext {
 #[derive(Debug, Clone)]
 pub(crate) enum WHNF {
     /// Closures
-    Lam(Label, Now, (NormalizationContext, InputSubExpr)),
+    Lam(Label, Thunk, (NormalizationContext, InputSubExpr)),
     AppliedBuiltin(Builtin, Vec<WHNF>),
     /// `λ(x: a) -> Some x`
-    OptionalSomeClosure(Now),
+    OptionalSomeClosure(Thunk),
     /// `λ(x : a) -> λ(xs : List a) -> [ x ] # xs`
     /// `λ(xs : List a) -> [ x ] # xs`
-    ListConsClosure(Now, Option<Now>),
+    ListConsClosure(Thunk, Option<Thunk>),
     /// `λ(x : Natural) -> x + 1`
     NaturalSuccClosure,
 
     BoolLit(bool),
     NaturalLit(Natural),
     IntegerLit(Integer),
-    EmptyOptionalLit(Now),
-    NEOptionalLit(Now),
-    EmptyListLit(Now),
-    NEListLit(Vec<Now>),
-    RecordLit(BTreeMap<Label, Now>),
-    RecordType(BTreeMap<Label, Now>),
+    EmptyOptionalLit(Thunk),
+    NEOptionalLit(Thunk),
+    EmptyListLit(Thunk),
+    NEListLit(Vec<Thunk>),
+    RecordLit(BTreeMap<Label, Thunk>),
+    RecordType(BTreeMap<Label, Thunk>),
     UnionType(NormalizationContext, BTreeMap<Label, Option<InputSubExpr>>),
     UnionConstructor(
         NormalizationContext,
@@ -371,10 +371,10 @@ pub(crate) enum WHNF {
     ),
     UnionLit(
         Label,
-        Now,
+        Thunk,
         (NormalizationContext, BTreeMap<Label, Option<InputSubExpr>>),
     ),
-    TextLit(Vec<InterpolatedTextContents<Now>>),
+    TextLit(Vec<InterpolatedTextContents<Thunk>>),
     /// This must not contain a value captured by one of the variants above.
     Expr(OutputSubExpr),
 }
@@ -490,7 +490,7 @@ impl WHNF {
             )),
             WHNF::TextLit(elts) => {
                 fn normalize_textlit(
-                    elts: Vec<InterpolatedTextContents<Now>>,
+                    elts: Vec<InterpolatedTextContents<Thunk>>,
                 ) -> InterpolatedText<OutputSubExpr> {
                     elts.into_iter()
                         .flat_map(|contents| {
@@ -533,10 +533,10 @@ impl WHNF {
                 apply_builtin(b, args)
             }
             (WHNF::OptionalSomeClosure(_), val) => {
-                WHNF::NEOptionalLit(Now::from_whnf(val))
+                WHNF::NEOptionalLit(Thunk::from_whnf(val))
             }
             (WHNF::ListConsClosure(t, None), val) => {
-                WHNF::ListConsClosure(t, Some(Now::from_whnf(val)))
+                WHNF::ListConsClosure(t, Some(Thunk::from_whnf(val)))
             }
             (WHNF::ListConsClosure(_, Some(x)), WHNF::EmptyListLit(_)) => {
                 WHNF::NEListLit(vec![x])
@@ -549,7 +549,7 @@ impl WHNF {
                 WHNF::NaturalLit(n + 1)
             }
             (WHNF::UnionConstructor(ctx, l, kts), val) => {
-                WHNF::UnionLit(l, Now::from_whnf(val), (ctx, kts))
+                WHNF::UnionLit(l, Thunk::from_whnf(val), (ctx, kts))
             }
             // Can't do anything useful, convert to expr
             (f, a) => WHNF::Expr(rc(ExprF::App(
@@ -625,35 +625,34 @@ impl WHNF {
     }
 }
 
-/// Normalize-on-write smart container. Contains either a (partially) normalized value or a
+/// Contains either a (partially) normalized value or a
 /// non-normalized value alongside a normalization context.
-/// The name is a pun on std::borrow::Cow.
 #[derive(Debug, Clone)]
-pub(crate) enum Now {
+pub(crate) enum Thunk {
     Normalized(Box<WHNF>),
     Unnormalized(NormalizationContext, InputSubExpr),
 }
 
-impl Now {
-    fn new(ctx: NormalizationContext, e: InputSubExpr) -> Now {
-        Now::Unnormalized(ctx, e)
+impl Thunk {
+    fn new(ctx: NormalizationContext, e: InputSubExpr) -> Thunk {
+        Thunk::Unnormalized(ctx, e)
     }
 
-    fn from_whnf(v: WHNF) -> Now {
-        Now::Normalized(Box::new(v))
+    fn from_whnf(v: WHNF) -> Thunk {
+        Thunk::Normalized(Box::new(v))
     }
 
     fn normalize(self) -> WHNF {
         match self {
-            Now::Normalized(v) => *v,
-            Now::Unnormalized(ctx, e) => normalize_whnf(ctx, e),
+            Thunk::Normalized(v) => *v,
+            Thunk::Unnormalized(ctx, e) => normalize_whnf(ctx, e),
         }
     }
 
     fn shift(&mut self, delta: isize, var: &V<Label>) {
         match self {
-            Now::Normalized(v) => v.shift(delta, var),
-            Now::Unnormalized(_, e) => shift_mut(delta, var, e),
+            Thunk::Normalized(v) => v.shift(delta, var),
+            Thunk::Unnormalized(_, e) => shift_mut(delta, var, e),
         }
     }
 }
@@ -674,34 +673,34 @@ fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> WHNF {
         }
         ExprF::Lam(x, t, e) => WHNF::Lam(
             x.clone(),
-            Now::new(ctx.clone(), t.clone()),
+            Thunk::new(ctx.clone(), t.clone()),
             (ctx, e.clone()),
         ),
         ExprF::Builtin(b) => WHNF::AppliedBuiltin(*b, vec![]),
         ExprF::BoolLit(b) => WHNF::BoolLit(*b),
         ExprF::NaturalLit(n) => WHNF::NaturalLit(*n),
         ExprF::OldOptionalLit(None, e) => {
-            WHNF::EmptyOptionalLit(Now::new(ctx, e.clone()))
+            WHNF::EmptyOptionalLit(Thunk::new(ctx, e.clone()))
         }
         ExprF::OldOptionalLit(Some(e), _) => {
-            WHNF::NEOptionalLit(Now::new(ctx, e.clone()))
+            WHNF::NEOptionalLit(Thunk::new(ctx, e.clone()))
         }
-        ExprF::SomeLit(e) => WHNF::NEOptionalLit(Now::new(ctx, e.clone())),
-        ExprF::EmptyListLit(e) => WHNF::EmptyListLit(Now::new(ctx, e.clone())),
+        ExprF::SomeLit(e) => WHNF::NEOptionalLit(Thunk::new(ctx, e.clone())),
+        ExprF::EmptyListLit(e) => WHNF::EmptyListLit(Thunk::new(ctx, e.clone())),
         ExprF::NEListLit(elts) => WHNF::NEListLit(
             elts.iter()
-                .map(|e| Now::new(ctx.clone(), e.clone()))
+                .map(|e| Thunk::new(ctx.clone(), e.clone()))
                 .collect(),
         ),
         ExprF::RecordLit(kvs) => WHNF::RecordLit(
             kvs.iter()
-                .map(|(k, e)| (k.clone(), Now::new(ctx.clone(), e.clone())))
+                .map(|(k, e)| (k.clone(), Thunk::new(ctx.clone(), e.clone())))
                 .collect(),
         ),
         ExprF::UnionType(kvs) => WHNF::UnionType(ctx, kvs.clone()),
         ExprF::UnionLit(l, x, kts) => WHNF::UnionLit(
             l.clone(),
-            Now::new(ctx.clone(), x.clone()),
+            Thunk::new(ctx.clone(), x.clone()),
             (ctx, kts.clone()),
         ),
         ExprF::TextLit(elts) => WHNF::TextLit(
@@ -709,7 +708,7 @@ fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> WHNF {
                 .map(|contents| {
                     use InterpolatedTextContents::{Expr, Text};
                     match contents {
-                        Expr(n) => Expr(Now::new(ctx.clone(), n.clone())),
+                        Expr(n) => Expr(Thunk::new(ctx.clone(), n.clone())),
                         Text(s) => Text(s.clone()),
                     }
                 })
-- 
cgit v1.2.3


From 1ccad14d712c550dee4d94ae20dff713132eb2c4 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 27 Apr 2019 15:55:25 +0200
Subject: Abstract out thunks in type position

---
 dhall/src/normalize.rs | 86 +++++++++++++++++++++++++++++++++++++-------------
 1 file changed, 64 insertions(+), 22 deletions(-)

(limited to 'dhall/src/normalize.rs')

diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index f3b0979..7a92d35 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -78,7 +78,7 @@ fn apply_builtin(b: Builtin, args: Vec<WHNF>) -> WHNF {
 
     let ret = match b {
         OptionalNone => improved_slice_patterns::match_vec!(args;
-            [t] => EmptyOptionalLit(Thunk::from_whnf(t)),
+            [t] => EmptyOptionalLit(TypeThunk::from_whnf(t)),
         ),
         NaturalIsZero => improved_slice_patterns::match_vec!(args;
             [NaturalLit(n)] => BoolLit(n == 0),
@@ -126,12 +126,12 @@ fn apply_builtin(b: Builtin, args: Vec<WHNF>) -> WHNF {
                 let mut kts = BTreeMap::new();
                 kts.insert(
                     "index".into(),
-                    Thunk::from_whnf(
+                    TypeThunk::from_whnf(
                         WHNF::from_builtin(Natural)
                     ),
                 );
                 kts.insert("value".into(), t);
-                EmptyListLit(Thunk::from_whnf(RecordType(kts)))
+                EmptyListLit(TypeThunk::from_whnf(RecordType(kts)))
             },
             [_, NEListLit(xs)] => {
                 let xs = xs
@@ -161,8 +161,8 @@ fn apply_builtin(b: Builtin, args: Vec<WHNF>) -> WHNF {
             },
             [t, g] => g
                 .app(WHNF::from_builtin(List).app(t.clone()))
-                .app(ListConsClosure(Thunk::from_whnf(t.clone()), None))
-                .app(EmptyListLit(Thunk::from_whnf(t))),
+                .app(ListConsClosure(TypeThunk::from_whnf(t.clone()), None))
+                .app(EmptyListLit(TypeThunk::from_whnf(t))),
         ),
         ListFold => improved_slice_patterns::match_vec!(args;
             // fold/build fusion
@@ -195,8 +195,8 @@ fn apply_builtin(b: Builtin, args: Vec<WHNF>) -> WHNF {
             },
             [t, g] => g
                 .app(WHNF::from_builtin(Optional).app(t.clone()))
-                .app(OptionalSomeClosure(Thunk::from_whnf(t.clone())))
-                .app(EmptyOptionalLit(Thunk::from_whnf(t))),
+                .app(OptionalSomeClosure(TypeThunk::from_whnf(t.clone())))
+                .app(EmptyOptionalLit(TypeThunk::from_whnf(t))),
         ),
         OptionalFold => improved_slice_patterns::match_vec!(args;
             // fold/build fusion
@@ -347,22 +347,22 @@ pub(crate) enum WHNF {
     Lam(Label, Thunk, (NormalizationContext, InputSubExpr)),
     AppliedBuiltin(Builtin, Vec<WHNF>),
     /// `λ(x: a) -> Some x`
-    OptionalSomeClosure(Thunk),
+    OptionalSomeClosure(TypeThunk),
     /// `λ(x : a) -> λ(xs : List a) -> [ x ] # xs`
     /// `λ(xs : List a) -> [ x ] # xs`
-    ListConsClosure(Thunk, Option<Thunk>),
+    ListConsClosure(TypeThunk, Option<Thunk>),
     /// `λ(x : Natural) -> x + 1`
     NaturalSuccClosure,
 
     BoolLit(bool),
     NaturalLit(Natural),
     IntegerLit(Integer),
-    EmptyOptionalLit(Thunk),
+    EmptyOptionalLit(TypeThunk),
     NEOptionalLit(Thunk),
-    EmptyListLit(Thunk),
+    EmptyListLit(TypeThunk),
     NEListLit(Vec<Thunk>),
     RecordLit(BTreeMap<Label, Thunk>),
-    RecordType(BTreeMap<Label, Thunk>),
+    RecordType(BTreeMap<Label, TypeThunk>),
     UnionType(NormalizationContext, BTreeMap<Label, Option<InputSubExpr>>),
     UnionConstructor(
         NormalizationContext,
@@ -569,11 +569,13 @@ impl WHNF {
             | WHNF::BoolLit(_)
             | WHNF::NaturalLit(_)
             | WHNF::IntegerLit(_) => {}
-            WHNF::EmptyOptionalLit(n)
-            | WHNF::NEOptionalLit(n)
-            | WHNF::OptionalSomeClosure(n)
-            | WHNF::EmptyListLit(n) => {
-                n.shift(delta, var);
+            WHNF::EmptyOptionalLit(tth)
+            | WHNF::OptionalSomeClosure(tth)
+            | WHNF::EmptyListLit(tth) => {
+                tth.shift(delta, var);
+            }
+            WHNF::NEOptionalLit(th) => {
+                th.shift(delta, var);
             }
             WHNF::Lam(x, t, (_, e)) => {
                 t.shift(delta, var);
@@ -595,7 +597,12 @@ impl WHNF {
                     x.shift(delta, var);
                 }
             }
-            WHNF::RecordLit(kvs) | WHNF::RecordType(kvs) => {
+            WHNF::RecordLit(kvs) => {
+                for x in kvs.values_mut() {
+                    x.shift(delta, var);
+                }
+            }
+            WHNF::RecordType(kvs) => {
                 for x in kvs.values_mut() {
                     x.shift(delta, var);
                 }
@@ -634,11 +641,11 @@ pub(crate) enum Thunk {
 }
 
 impl Thunk {
-    fn new(ctx: NormalizationContext, e: InputSubExpr) -> Thunk {
+    fn new(ctx: NormalizationContext, e: InputSubExpr) -> Self {
         Thunk::Unnormalized(ctx, e)
     }
 
-    fn from_whnf(v: WHNF) -> Thunk {
+    fn from_whnf(v: WHNF) -> Self {
         Thunk::Normalized(Box::new(v))
     }
 
@@ -657,6 +664,39 @@ impl Thunk {
     }
 }
 
+/// A thunk in type position.
+#[derive(Debug, Clone)]
+pub(crate) enum TypeThunk {
+    Thunk(Thunk),
+    // Type(Type<'static>),
+}
+
+impl TypeThunk {
+    fn new(ctx: NormalizationContext, e: InputSubExpr) -> Self {
+        TypeThunk::from_thunk(Thunk::new(ctx, e))
+    }
+
+    fn from_thunk(th: Thunk) -> Self {
+        TypeThunk::Thunk(th)
+    }
+
+    fn from_whnf(v: WHNF) -> Self {
+        TypeThunk::from_thunk(Thunk::from_whnf(v))
+    }
+
+    fn normalize(self) -> WHNF {
+        match self {
+            TypeThunk::Thunk(th) => th.normalize(),
+        }
+    }
+
+    fn shift(&mut self, delta: isize, var: &V<Label>) {
+        match self {
+            TypeThunk::Thunk(th) => th.shift(delta, var),
+        }
+    }
+}
+
 /// Reduces the imput expression to WHNF. See doc on `WHNF` for details.
 fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> WHNF {
     match expr.as_ref() {
@@ -680,13 +720,15 @@ fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> WHNF {
         ExprF::BoolLit(b) => WHNF::BoolLit(*b),
         ExprF::NaturalLit(n) => WHNF::NaturalLit(*n),
         ExprF::OldOptionalLit(None, e) => {
-            WHNF::EmptyOptionalLit(Thunk::new(ctx, e.clone()))
+            WHNF::EmptyOptionalLit(TypeThunk::new(ctx, e.clone()))
         }
         ExprF::OldOptionalLit(Some(e), _) => {
             WHNF::NEOptionalLit(Thunk::new(ctx, e.clone()))
         }
         ExprF::SomeLit(e) => WHNF::NEOptionalLit(Thunk::new(ctx, e.clone())),
-        ExprF::EmptyListLit(e) => WHNF::EmptyListLit(Thunk::new(ctx, e.clone())),
+        ExprF::EmptyListLit(e) => {
+            WHNF::EmptyListLit(TypeThunk::new(ctx, e.clone()))
+        }
         ExprF::NEListLit(elts) => WHNF::NEListLit(
             elts.iter()
                 .map(|e| Thunk::new(ctx.clone(), e.clone()))
-- 
cgit v1.2.3


From 1ad9cfe4ec9258d071d7f1522e8fdf2866fbf99c Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 27 Apr 2019 16:05:06 +0200
Subject: Store thunks uniformly in WHNF

---
 dhall/src/normalize.rs | 101 ++++++++++++++++++++-----------------------------
 1 file changed, 42 insertions(+), 59 deletions(-)

(limited to 'dhall/src/normalize.rs')

diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 7a92d35..9c62923 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -50,11 +50,7 @@ impl<'a> Typed<'a> {
 
 impl<'a> PartiallyNormalized<'a> {
     pub(crate) fn normalize(self) -> Normalized<'a> {
-        Normalized(
-            self.0.normalize_to_expr(),
-            self.1,
-            self.2,
-        )
+        Normalized(self.0.normalize_to_expr(), self.1, self.2)
     }
     pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
         let mut e = self.0.clone();
@@ -332,15 +328,11 @@ impl NormalizationContext {
 /// The rule is the following: we must _not_ construct values of type `Expr` while normalizing,
 /// but only construct `WHNF`s.
 ///
-/// WHNFs store subexpressions unnormalized, to enable lazy normalization. They approximate
+/// WHNFs store some subexpressions unnormalized, to enable lazy normalization. They 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 e.g. a record literal
 /// this means knowing just the field names.
-///
-/// Each variant captures the relevant contexts when it is constructed. Conceptually each
-/// subexpression has its own context, but in practice some contexts can be shared when sensible, to
-/// avoid unnecessary allocations.
 #[derive(Debug, Clone)]
 pub(crate) enum WHNF {
     /// Closures
@@ -363,17 +355,9 @@ pub(crate) enum WHNF {
     NEListLit(Vec<Thunk>),
     RecordLit(BTreeMap<Label, Thunk>),
     RecordType(BTreeMap<Label, TypeThunk>),
-    UnionType(NormalizationContext, BTreeMap<Label, Option<InputSubExpr>>),
-    UnionConstructor(
-        NormalizationContext,
-        Label,
-        BTreeMap<Label, Option<InputSubExpr>>,
-    ),
-    UnionLit(
-        Label,
-        Thunk,
-        (NormalizationContext, BTreeMap<Label, Option<InputSubExpr>>),
-    ),
+    UnionType(BTreeMap<Label, Option<TypeThunk>>),
+    UnionConstructor(Label, BTreeMap<Label, Option<TypeThunk>>),
+    UnionLit(Label, Thunk, BTreeMap<Label, Option<TypeThunk>>),
     TextLit(Vec<InterpolatedTextContents<Thunk>>),
     /// This must not contain a value captured by one of the variants above.
     Expr(OutputSubExpr),
@@ -445,46 +429,28 @@ impl WHNF {
                     .map(|(k, v)| (k, v.normalize().normalize_to_expr()))
                     .collect(),
             )),
-            WHNF::UnionType(ctx, kts) => rc(ExprF::UnionType(
+            WHNF::UnionType(kts) => rc(ExprF::UnionType(
                 kts.into_iter()
                     .map(|(k, v)| {
-                        (
-                            k,
-                            v.map(|v| {
-                                normalize_whnf(ctx.clone(), v)
-                                    .normalize_to_expr()
-                            }),
-                        )
+                        (k, v.map(|v| v.normalize().normalize_to_expr()))
                     })
                     .collect(),
             )),
-            WHNF::UnionConstructor(ctx, l, kts) => {
+            WHNF::UnionConstructor(l, kts) => {
                 let kts = kts
                     .into_iter()
                     .map(|(k, v)| {
-                        (
-                            k,
-                            v.map(|v| {
-                                normalize_whnf(ctx.clone(), v)
-                                    .normalize_to_expr()
-                            }),
-                        )
+                        (k, v.map(|v| v.normalize().normalize_to_expr()))
                     })
                     .collect();
                 rc(ExprF::Field(rc(ExprF::UnionType(kts)), l))
             }
-            WHNF::UnionLit(l, v, (kts_ctx, kts)) => rc(ExprF::UnionLit(
+            WHNF::UnionLit(l, v, kts) => rc(ExprF::UnionLit(
                 l,
                 v.normalize().normalize_to_expr(),
                 kts.into_iter()
                     .map(|(k, v)| {
-                        (
-                            k,
-                            v.map(|v| {
-                                normalize_whnf(kts_ctx.clone(), v)
-                                    .normalize_to_expr()
-                            }),
-                        )
+                        (k, v.map(|v| v.normalize().normalize_to_expr()))
                     })
                     .collect(),
             )),
@@ -548,8 +514,8 @@ impl WHNF {
             (WHNF::NaturalSuccClosure, WHNF::NaturalLit(n)) => {
                 WHNF::NaturalLit(n + 1)
             }
-            (WHNF::UnionConstructor(ctx, l, kts), val) => {
-                WHNF::UnionLit(l, Thunk::from_whnf(val), (ctx, kts))
+            (WHNF::UnionConstructor(l, kts), val) => {
+                WHNF::UnionLit(l, Thunk::from_whnf(val), kts)
             }
             // Can't do anything useful, convert to expr
             (f, a) => WHNF::Expr(rc(ExprF::App(
@@ -607,15 +573,15 @@ impl WHNF {
                     x.shift(delta, var);
                 }
             }
-            WHNF::UnionType(_, kts) | WHNF::UnionConstructor(_, _, kts) => {
+            WHNF::UnionType(kts) | WHNF::UnionConstructor(_, kts) => {
                 for x in kts.values_mut().flat_map(|opt| opt) {
-                    shift_mut(delta, var, x);
+                    x.shift(delta, var);
                 }
             }
-            WHNF::UnionLit(_, v, (_, kts)) => {
+            WHNF::UnionLit(_, v, kts) => {
                 v.shift(delta, var);
                 for x in kts.values_mut().flat_map(|opt| opt) {
-                    shift_mut(delta, var, x);
+                    x.shift(delta, var);
                 }
             }
             WHNF::TextLit(elts) => {
@@ -739,11 +705,29 @@ fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> WHNF {
                 .map(|(k, e)| (k.clone(), Thunk::new(ctx.clone(), e.clone())))
                 .collect(),
         ),
-        ExprF::UnionType(kvs) => WHNF::UnionType(ctx, kvs.clone()),
+        ExprF::UnionType(kts) => WHNF::UnionType(
+            kts.iter()
+                .map(|(k, t)| {
+                    (
+                        k.clone(),
+                        t.as_ref()
+                            .map(|t| TypeThunk::new(ctx.clone(), t.clone())),
+                    )
+                })
+                .collect(),
+        ),
         ExprF::UnionLit(l, x, kts) => WHNF::UnionLit(
             l.clone(),
             Thunk::new(ctx.clone(), x.clone()),
-            (ctx, kts.clone()),
+            kts.iter()
+                .map(|(k, t)| {
+                    (
+                        k.clone(),
+                        t.as_ref()
+                            .map(|t| TypeThunk::new(ctx.clone(), t.clone())),
+                    )
+                })
+                .collect(),
         ),
         ExprF::TextLit(elts) => WHNF::TextLit(
             elts.iter()
@@ -838,7 +822,7 @@ fn normalize_last_layer(expr: ExprF<WHNF, Label, X, X>) -> WHNF {
         ExprF::BinOp(TextAppend, TextLit(x), y) if x.is_empty() => y,
         ExprF::BinOp(TextAppend, x, TextLit(y)) if y.is_empty() => x,
 
-        ExprF::Field(UnionType(ctx, kts), l) => UnionConstructor(ctx, l, kts),
+        ExprF::Field(UnionType(kts), l) => UnionConstructor(l, kts),
         ExprF::Field(RecordLit(mut kvs), l) => match kvs.remove(&l) {
             Some(r) => r.normalize(),
             None => {
@@ -856,18 +840,17 @@ fn normalize_last_layer(expr: ExprF<WHNF, Label, X, X>) -> WHNF {
         ),
         ExprF::Merge(RecordLit(mut handlers), e, t) => {
             let e = match e {
-                UnionConstructor(ctor_ctx, l, kts) => match handlers.remove(&l)
-                {
+                UnionConstructor(l, kts) => match handlers.remove(&l) {
                     Some(h) => return h.normalize(),
-                    None => UnionConstructor(ctor_ctx, l, kts),
+                    None => UnionConstructor(l, kts),
                 },
-                UnionLit(l, v, (kts_ctx, kts)) => match handlers.remove(&l) {
+                UnionLit(l, v, kts) => match handlers.remove(&l) {
                     Some(h) => {
                         let h = h.normalize();
                         let v = v.normalize();
                         return h.app(v);
                     }
-                    None => UnionLit(l, v, (kts_ctx, kts)),
+                    None => UnionLit(l, v, kts),
                 },
                 e => e,
             };
-- 
cgit v1.2.3


From 5b5d4b683b483b153f7e30c0b91270ed237f18c8 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 27 Apr 2019 17:09:24 +0200
Subject: Replace TypeInternal::RecordType with WHNF::RecordType

---
 dhall/src/normalize.rs | 21 +++++++++++++++++----
 1 file changed, 17 insertions(+), 4 deletions(-)

(limited to 'dhall/src/normalize.rs')

diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 9c62923..9ca890e 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -9,7 +9,7 @@ use dhall_core::{
 };
 use dhall_generator as dhall;
 
-use crate::expr::{Normalized, PartiallyNormalized, Typed};
+use crate::expr::{Normalized, PartiallyNormalized, Type, Typed};
 
 type InputSubExpr = SubExpr<X, Normalized<'static>>;
 type OutputSubExpr = SubExpr<X, X>;
@@ -365,7 +365,7 @@ pub(crate) enum WHNF {
 
 impl WHNF {
     /// Convert the value back to a (normalized) syntactic expression
-    fn normalize_to_expr(self) -> OutputSubExpr {
+    pub(crate) fn normalize_to_expr(self) -> OutputSubExpr {
         match self {
             WHNF::Lam(x, t, (ctx, e)) => {
                 let ctx2 = ctx.skip(&x);
@@ -615,7 +615,7 @@ impl Thunk {
         Thunk::Normalized(Box::new(v))
     }
 
-    fn normalize(self) -> WHNF {
+    pub(crate) fn normalize(self) -> WHNF {
         match self {
             Thunk::Normalized(v) => *v,
             Thunk::Unnormalized(ctx, e) => normalize_whnf(ctx, e),
@@ -634,7 +634,7 @@ impl Thunk {
 #[derive(Debug, Clone)]
 pub(crate) enum TypeThunk {
     Thunk(Thunk),
-    // Type(Type<'static>),
+    Type(Type<'static>),
 }
 
 impl TypeThunk {
@@ -646,6 +646,10 @@ impl TypeThunk {
         TypeThunk::Thunk(th)
     }
 
+    pub(crate) fn from_type(t: Type<'static>) -> Self {
+        TypeThunk::Type(t)
+    }
+
     fn from_whnf(v: WHNF) -> Self {
         TypeThunk::from_thunk(Thunk::from_whnf(v))
     }
@@ -653,12 +657,21 @@ impl TypeThunk {
     fn normalize(self) -> WHNF {
         match self {
             TypeThunk::Thunk(th) => th.normalize(),
+            // TODO: let's hope for the best with the unwraps
+            TypeThunk::Type(t) => normalize_whnf(
+                NormalizationContext::new(),
+                t.into_normalized().unwrap().0.embed_absurd(),
+            ),
         }
     }
 
     fn shift(&mut self, delta: isize, var: &V<Label>) {
         match self {
             TypeThunk::Thunk(th) => th.shift(delta, var),
+            TypeThunk::Type(t) => {
+                let shifted = t.shift(delta, var);
+                std::mem::replace(t, shifted);
+            }
         }
     }
 }
-- 
cgit v1.2.3


From 949da31876c899dc7de295328fb7acc8063cdc7c Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 27 Apr 2019 22:46:29 +0200
Subject: Move Pi to WHNF

---
 dhall/src/normalize.rs | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'dhall/src/normalize.rs')

diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 9ca890e..2dc4cab 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -345,6 +345,7 @@ pub(crate) enum WHNF {
     ListConsClosure(TypeThunk, Option<Thunk>),
     /// `λ(x : Natural) -> x + 1`
     NaturalSuccClosure,
+    Pi(Label, TypeThunk, TypeThunk),
 
     BoolLit(bool),
     NaturalLit(Natural),
@@ -400,6 +401,11 @@ impl WHNF {
             WHNF::NaturalSuccClosure => {
                 dhall::subexpr!(λ(x : Natural) -> x + 1)
             }
+            WHNF::Pi(x, t, e) => rc(ExprF::Pi(
+                x,
+                t.normalize().normalize_to_expr(),
+                e.normalize().normalize_to_expr(),
+            )),
             WHNF::BoolLit(b) => rc(ExprF::BoolLit(b)),
             WHNF::NaturalLit(n) => rc(ExprF::NaturalLit(n)),
             WHNF::IntegerLit(n) => rc(ExprF::IntegerLit(n)),
@@ -558,6 +564,10 @@ impl WHNF {
                     x.shift(delta, var);
                 }
             }
+            WHNF::Pi(x, t, e) => {
+                t.shift(delta, var);
+                e.shift(delta, &var.shift0(1, x));
+            }
             WHNF::NEListLit(elts) => {
                 for x in elts.iter_mut() {
                     x.shift(delta, var);
-- 
cgit v1.2.3


From a594e3aa376aa4bfef3456d336630f7520f3c28b Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 28 Apr 2019 01:03:12 +0200
Subject: Use PartiallyNormalized throughout typechecking

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

(limited to 'dhall/src/normalize.rs')

diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 2dc4cab..88a55a1 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -4,7 +4,7 @@ use std::rc::Rc;
 
 use dhall_core::context::Context;
 use dhall_core::{
-    rc, shift, shift0, Builtin, ExprF, Integer, InterpolatedText,
+    rc, shift, shift0, Builtin, Const, ExprF, Integer, InterpolatedText,
     InterpolatedTextContents, Label, Natural, SubExpr, V, X,
 };
 use dhall_generator as dhall;
@@ -347,6 +347,7 @@ pub(crate) enum WHNF {
     NaturalSuccClosure,
     Pi(Label, TypeThunk, TypeThunk),
 
+    Const(Const),
     BoolLit(bool),
     NaturalLit(Natural),
     IntegerLit(Integer),
@@ -406,6 +407,7 @@ impl WHNF {
                 t.normalize().normalize_to_expr(),
                 e.normalize().normalize_to_expr(),
             )),
+            WHNF::Const(c) => rc(ExprF::Const(c)),
             WHNF::BoolLit(b) => rc(ExprF::BoolLit(b)),
             WHNF::NaturalLit(n) => rc(ExprF::NaturalLit(n)),
             WHNF::IntegerLit(n) => rc(ExprF::IntegerLit(n)),
@@ -494,7 +496,7 @@ impl WHNF {
     }
 
     /// Apply to a value
-    fn app(self, val: WHNF) -> WHNF {
+    pub(crate) fn app(self, val: WHNF) -> WHNF {
         match (self, val) {
             (WHNF::Lam(x, _, (ctx, e)), val) => {
                 let ctx2 = ctx.insert(&x, val);
@@ -531,13 +533,14 @@ impl WHNF {
         }
     }
 
-    fn from_builtin(b: Builtin) -> WHNF {
+    pub(crate) fn from_builtin(b: Builtin) -> WHNF {
         WHNF::AppliedBuiltin(b, vec![])
     }
 
     fn shift(&mut self, delta: isize, var: &V<Label>) {
         match self {
             WHNF::NaturalSuccClosure
+            | WHNF::Const(_)
             | WHNF::BoolLit(_)
             | WHNF::NaturalLit(_)
             | WHNF::IntegerLit(_) => {}
@@ -705,7 +708,8 @@ fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> WHNF {
             Thunk::new(ctx.clone(), t.clone()),
             (ctx, e.clone()),
         ),
-        ExprF::Builtin(b) => WHNF::AppliedBuiltin(*b, vec![]),
+        ExprF::Builtin(b) => WHNF::from_builtin(*b),
+        ExprF::Const(c) => WHNF::Const(*c),
         ExprF::BoolLit(b) => WHNF::BoolLit(*b),
         ExprF::NaturalLit(n) => WHNF::NaturalLit(*n),
         ExprF::OldOptionalLit(None, e) => {
-- 
cgit v1.2.3


From 5c16a75c6dc01bbd0bfe36be4a9b337a762632a8 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 29 Apr 2019 16:27:14 +0200
Subject: Properly substitute when typing App

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

(limited to 'dhall/src/normalize.rs')

diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 88a55a1..dd9474d 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -25,9 +25,9 @@ impl<'a> Typed<'a> {
     /// leave ill-typed sub-expressions unevaluated.
     ///
     pub fn normalize(self) -> Normalized<'a> {
-        self.normalize_whnf().normalize()
+        self.partially_normalize().normalize()
     }
-    pub(crate) fn normalize_whnf(self) -> PartiallyNormalized<'a> {
+    pub(crate) fn partially_normalize(self) -> PartiallyNormalized<'a> {
         PartiallyNormalized(
             normalize_whnf(
                 NormalizationContext::from_typecheck_ctx(&self.2),
@@ -61,6 +61,20 @@ impl<'a> PartiallyNormalized<'a> {
             self.2,
         )
     }
+    pub(crate) fn subst_shift(
+        &self,
+        var: &V<Label>,
+        val: &PartiallyNormalized<'static>,
+    ) -> Self {
+        PartiallyNormalized(
+            self.0.subst_shift(var, val),
+            self.1.as_ref().map(|x| x.subst_shift(var, val)),
+            self.2,
+        )
+    }
+    pub(crate) fn into_whnf(self) -> WHNF {
+        self.0
+    }
 }
 
 fn shift_mut<N, E>(delta: isize, var: &V<Label>, in_expr: &mut SubExpr<N, E>) {
@@ -273,6 +287,18 @@ impl EnvItem {
             Skip(var) => Skip(var.shift0(delta, x)),
         }
     }
+    pub(crate) fn subst_shift(
+        &self,
+        var: &V<Label>,
+        val: &PartiallyNormalized<'static>,
+    ) -> Self {
+        use EnvItem::*;
+        match self {
+            Expr(e) => Expr(e.subst_shift(var, val)),
+            Skip(v) if v == var => Expr(val.clone().into_whnf()),
+            Skip(v) => Skip(v.shift(-1, var)),
+        }
+    }
 }
 
 #[derive(Debug, Clone)]
@@ -298,10 +324,8 @@ impl NormalizationContext {
         let V(x, n) = var;
         match self.0.lookup(x, *n) {
             Some(EnvItem::Expr(e)) => e.clone(),
-            Some(EnvItem::Skip(newvar)) => {
-                WHNF::Expr(rc(ExprF::Var(newvar.clone())))
-            }
-            None => WHNF::Expr(rc(ExprF::Var(var.clone()))),
+            Some(EnvItem::Skip(newvar)) => WHNF::Var(newvar.clone()),
+            None => WHNF::Var(var.clone()),
         }
     }
     fn from_typecheck_ctx(tc_ctx: &crate::typecheck::TypecheckContext) -> Self {
@@ -321,6 +345,16 @@ impl NormalizationContext {
         }
         NormalizationContext(Rc::new(ctx))
     }
+
+    fn subst_shift(
+        &self,
+        var: &V<Label>,
+        val: &PartiallyNormalized<'static>,
+    ) -> Self {
+        NormalizationContext(Rc::new(
+            self.0.map(|_, e| e.subst_shift(var, val)),
+        ))
+    }
 }
 
 /// A semantic value. This is partially redundant with `dhall_core::Expr`, on purpose. `Expr` should
@@ -347,6 +381,7 @@ pub(crate) enum WHNF {
     NaturalSuccClosure,
     Pi(Label, TypeThunk, TypeThunk),
 
+    Var(V<Label>),
     Const(Const),
     BoolLit(bool),
     NaturalLit(Natural),
@@ -397,6 +432,8 @@ impl WHNF {
             WHNF::ListConsClosure(n, Some(v)) => {
                 let v = v.normalize().normalize_to_expr();
                 let a = n.normalize().normalize_to_expr();
+                // Avoid accidental capture of the new `xs` variable
+                let v = shift0(1, &"xs".into(), &v);
                 dhall::subexpr!(λ(xs : List a) -> [ v ] # xs)
             }
             WHNF::NaturalSuccClosure => {
@@ -407,6 +444,7 @@ impl WHNF {
                 t.normalize().normalize_to_expr(),
                 e.normalize().normalize_to_expr(),
             )),
+            WHNF::Var(v) => rc(ExprF::Var(v)),
             WHNF::Const(c) => rc(ExprF::Const(c)),
             WHNF::BoolLit(b) => rc(ExprF::BoolLit(b)),
             WHNF::NaturalLit(n) => rc(ExprF::NaturalLit(n)),
@@ -539,6 +577,9 @@ impl WHNF {
 
     fn shift(&mut self, delta: isize, var: &V<Label>) {
         match self {
+            WHNF::Var(v) => {
+                std::mem::replace(v, v.shift(delta, var));
+            }
             WHNF::NaturalSuccClosure
             | WHNF::Const(_)
             | WHNF::BoolLit(_)
@@ -609,6 +650,103 @@ impl WHNF {
             WHNF::Expr(e) => shift_mut(delta, var, e),
         }
     }
+
+    pub(crate) fn subst_shift(
+        &self,
+        var: &V<Label>,
+        val: &PartiallyNormalized<'static>,
+    ) -> Self {
+        match self {
+            WHNF::Lam(x, t, (ctx, e)) => WHNF::Lam(
+                x.clone(),
+                t.subst_shift(var, val),
+                (ctx.subst_shift(var, val), e.clone()),
+            ),
+            WHNF::AppliedBuiltin(b, args) => WHNF::AppliedBuiltin(
+                *b,
+                args.iter().map(|v| v.subst_shift(var, val)).collect(),
+            ),
+            WHNF::NaturalSuccClosure => WHNF::NaturalSuccClosure,
+            WHNF::OptionalSomeClosure(tth) => {
+                WHNF::OptionalSomeClosure(tth.subst_shift(var, val))
+            }
+            WHNF::ListConsClosure(t, v) => WHNF::ListConsClosure(
+                t.subst_shift(var, val),
+                v.as_ref().map(|v| v.subst_shift(var, val)),
+            ),
+            WHNF::Pi(x, t, e) => WHNF::Pi(
+                x.clone(),
+                t.subst_shift(var, val),
+                e.subst_shift(&var.shift0(1, x), val),
+            ),
+            WHNF::Var(v) if v == var => val.clone().into_whnf(),
+            WHNF::Var(v) => WHNF::Var(v.shift(-1, var)),
+            WHNF::Const(c) => WHNF::Const(*c),
+            WHNF::BoolLit(b) => WHNF::BoolLit(*b),
+            WHNF::NaturalLit(n) => WHNF::NaturalLit(*n),
+            WHNF::IntegerLit(n) => WHNF::IntegerLit(*n),
+            WHNF::EmptyOptionalLit(tth) => {
+                WHNF::EmptyOptionalLit(tth.subst_shift(var, val))
+            }
+            WHNF::NEOptionalLit(th) => {
+                WHNF::NEOptionalLit(th.subst_shift(var, val))
+            }
+            WHNF::EmptyListLit(tth) => {
+                WHNF::EmptyListLit(tth.subst_shift(var, val))
+            }
+            WHNF::NEListLit(elts) => WHNF::NEListLit(
+                elts.iter().map(|v| v.subst_shift(var, val)).collect(),
+            ),
+            WHNF::RecordLit(kvs) => WHNF::RecordLit(
+                kvs.iter()
+                    .map(|(k, v)| (k.clone(), v.subst_shift(var, val)))
+                    .collect(),
+            ),
+            WHNF::RecordType(kvs) => WHNF::RecordType(
+                kvs.iter()
+                    .map(|(k, v)| (k.clone(), v.subst_shift(var, val)))
+                    .collect(),
+            ),
+            WHNF::UnionType(kts) => WHNF::UnionType(
+                kts.iter()
+                    .map(|(k, v)| {
+                        (k.clone(), v.as_ref().map(|v| v.subst_shift(var, val)))
+                    })
+                    .collect(),
+            ),
+            WHNF::UnionConstructor(x, kts) => WHNF::UnionConstructor(
+                x.clone(),
+                kts.iter()
+                    .map(|(k, v)| {
+                        (k.clone(), v.as_ref().map(|v| v.subst_shift(var, val)))
+                    })
+                    .collect(),
+            ),
+            WHNF::UnionLit(x, v, kts) => WHNF::UnionLit(
+                x.clone(),
+                v.subst_shift(var, val),
+                kts.iter()
+                    .map(|(k, v)| {
+                        (k.clone(), v.as_ref().map(|v| v.subst_shift(var, val)))
+                    })
+                    .collect(),
+            ),
+            WHNF::TextLit(elts) => WHNF::TextLit(
+                elts.iter()
+                    .map(|contents| {
+                        use InterpolatedTextContents::{Expr, Text};
+                        match contents {
+                            Expr(th) => Expr(th.subst_shift(var, val)),
+                            Text(s) => Text(s.clone()),
+                        }
+                    })
+                    .collect(),
+            ),
+            WHNF::Expr(e) => WHNF::Expr(
+                e.subst_shift(var, &val.clone().normalize().as_expr()),
+            ),
+        }
+    }
 }
 
 /// Contains either a (partially) normalized value or a
@@ -641,6 +779,21 @@ impl Thunk {
             Thunk::Unnormalized(_, e) => shift_mut(delta, var, e),
         }
     }
+
+    pub(crate) fn subst_shift(
+        &self,
+        var: &V<Label>,
+        val: &PartiallyNormalized<'static>,
+    ) -> Self {
+        match self {
+            Thunk::Normalized(v) => {
+                Thunk::Normalized(Box::new(v.subst_shift(var, val)))
+            }
+            Thunk::Unnormalized(ctx, e) => {
+                Thunk::Unnormalized(ctx.subst_shift(var, val), e.clone())
+            }
+        }
+    }
 }
 
 /// A thunk in type position.
@@ -667,14 +820,11 @@ impl TypeThunk {
         TypeThunk::from_thunk(Thunk::from_whnf(v))
     }
 
-    fn normalize(self) -> WHNF {
+    pub(crate) fn normalize(self) -> WHNF {
         match self {
             TypeThunk::Thunk(th) => th.normalize(),
-            // TODO: let's hope for the best with the unwraps
-            TypeThunk::Type(t) => normalize_whnf(
-                NormalizationContext::new(),
-                t.into_normalized().unwrap().0.embed_absurd(),
-            ),
+            // TODO: let's hope for the best with the unwrap
+            TypeThunk::Type(t) => t.partially_normalize().unwrap().into_whnf(),
         }
     }
 
@@ -687,6 +837,17 @@ impl TypeThunk {
             }
         }
     }
+
+    pub(crate) fn subst_shift(
+        &self,
+        var: &V<Label>,
+        val: &PartiallyNormalized<'static>,
+    ) -> Self {
+        match self {
+            TypeThunk::Thunk(th) => TypeThunk::Thunk(th.subst_shift(var, val)),
+            TypeThunk::Type(t) => TypeThunk::Type(t.subst_shift(var, val)),
+        }
+    }
 }
 
 /// Reduces the imput expression to WHNF. See doc on `WHNF` for details.
-- 
cgit v1.2.3


From c60d99ddec3653ed10828c91f3e1abf8b78238b0 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 29 Apr 2019 17:13:51 +0200
Subject: Allow representing normal form as a semantic value

---
 dhall/src/normalize.rs | 566 +++++++++++++++++++++++++++++--------------------
 1 file changed, 340 insertions(+), 226 deletions(-)

(limited to 'dhall/src/normalize.rs')

diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index dd9474d..b5971cb 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -72,7 +72,7 @@ impl<'a> PartiallyNormalized<'a> {
             self.2,
         )
     }
-    pub(crate) fn into_whnf(self) -> WHNF {
+    pub(crate) fn into_whnf(self) -> Value<WHNF> {
         self.0
     }
 }
@@ -82,9 +82,9 @@ fn shift_mut<N, E>(delta: isize, var: &V<Label>, in_expr: &mut SubExpr<N, E>) {
     std::mem::replace(in_expr, new_expr);
 }
 
-fn apply_builtin(b: Builtin, args: Vec<WHNF>) -> WHNF {
+fn apply_builtin(b: Builtin, args: Vec<Value<WHNF>>) -> Value<WHNF> {
     use dhall_core::Builtin::*;
-    use WHNF::*;
+    use Value::*;
 
     let ret = match b {
         OptionalNone => improved_slice_patterns::match_vec!(args;
@@ -137,7 +137,7 @@ fn apply_builtin(b: Builtin, args: Vec<WHNF>) -> WHNF {
                 kts.insert(
                     "index".into(),
                     TypeThunk::from_whnf(
-                        WHNF::from_builtin(Natural)
+                        Value::from_builtin(Natural)
                     ),
                 );
                 kts.insert("value".into(), t);
@@ -160,7 +160,7 @@ fn apply_builtin(b: Builtin, args: Vec<WHNF>) -> WHNF {
         ),
         ListBuild => improved_slice_patterns::match_vec!(args;
             // fold/build fusion
-            [_, WHNF::AppliedBuiltin(ListFold, args)] => {
+            [_, Value::AppliedBuiltin(ListFold, args)] => {
                 let mut args = args;
                 if args.len() >= 2 {
                     args.remove(1)
@@ -170,13 +170,13 @@ fn apply_builtin(b: Builtin, args: Vec<WHNF>) -> WHNF {
                 }
             },
             [t, g] => g
-                .app(WHNF::from_builtin(List).app(t.clone()))
+                .app(Value::from_builtin(List).app(t.clone()))
                 .app(ListConsClosure(TypeThunk::from_whnf(t.clone()), None))
                 .app(EmptyListLit(TypeThunk::from_whnf(t))),
         ),
         ListFold => improved_slice_patterns::match_vec!(args;
             // fold/build fusion
-            [_, WHNF::AppliedBuiltin(ListBuild, args)] => {
+            [_, Value::AppliedBuiltin(ListBuild, args)] => {
                 let mut args = args;
                 if args.len() >= 2 {
                     args.remove(1)
@@ -188,14 +188,14 @@ fn apply_builtin(b: Builtin, args: Vec<WHNF>) -> WHNF {
             [_, NEListLit(xs), _, cons, nil] => {
                 let mut v = nil;
                 for x in xs.into_iter().rev() {
-                    v = cons.clone().app(x.normalize()).app(v);
+                    v = cons.clone().app(x.normalize_whnf()).app(v);
                 }
                 v
             }
         ),
         OptionalBuild => improved_slice_patterns::match_vec!(args;
             // fold/build fusion
-            [_, WHNF::AppliedBuiltin(OptionalFold, args)] => {
+            [_, Value::AppliedBuiltin(OptionalFold, args)] => {
                 let mut args = args;
                 if args.len() >= 2 {
                     args.remove(1)
@@ -204,13 +204,13 @@ fn apply_builtin(b: Builtin, args: Vec<WHNF>) -> WHNF {
                 }
             },
             [t, g] => g
-                .app(WHNF::from_builtin(Optional).app(t.clone()))
+                .app(Value::from_builtin(Optional).app(t.clone()))
                 .app(OptionalSomeClosure(TypeThunk::from_whnf(t.clone())))
                 .app(EmptyOptionalLit(TypeThunk::from_whnf(t))),
         ),
         OptionalFold => improved_slice_patterns::match_vec!(args;
             // fold/build fusion
-            [_, WHNF::AppliedBuiltin(OptionalBuild, args)] => {
+            [_, Value::AppliedBuiltin(OptionalBuild, args)] => {
                 let mut args = args;
                 if args.len() >= 2 {
                     args.remove(1)
@@ -222,12 +222,12 @@ fn apply_builtin(b: Builtin, args: Vec<WHNF>) -> WHNF {
                 nothing
             },
             [_, NEOptionalLit(x), _, just, _] => {
-                just.app(x.normalize())
+                just.app(x.normalize_whnf())
             }
         ),
         NaturalBuild => improved_slice_patterns::match_vec!(args;
             // fold/build fusion
-            [WHNF::AppliedBuiltin(NaturalFold, args)] => {
+            [Value::AppliedBuiltin(NaturalFold, args)] => {
                 let mut args = args;
                 if args.len() >= 1 {
                     args.remove(0)
@@ -236,13 +236,13 @@ fn apply_builtin(b: Builtin, args: Vec<WHNF>) -> WHNF {
                 }
             },
             [g] => g
-                .app(WHNF::from_builtin(Natural))
+                .app(Value::from_builtin(Natural))
                 .app(NaturalSuccClosure)
                 .app(NaturalLit(0)),
         ),
         NaturalFold => improved_slice_patterns::match_vec!(args;
             // fold/build fusion
-            [WHNF::AppliedBuiltin(NaturalBuild, args)] => {
+            [Value::AppliedBuiltin(NaturalBuild, args)] => {
                 let mut args = args;
                 if args.len() >= 1 {
                     args.remove(0)
@@ -252,7 +252,7 @@ fn apply_builtin(b: Builtin, args: Vec<WHNF>) -> WHNF {
             },
             [NaturalLit(0), _, _, zero] => zero,
             [NaturalLit(n), t, succ, zero] => {
-                let fold = WHNF::from_builtin(NaturalFold)
+                let fold = Value::from_builtin(NaturalFold)
                     .app(NaturalLit(n - 1))
                     .app(t)
                     .app(succ.clone())
@@ -271,7 +271,7 @@ fn apply_builtin(b: Builtin, args: Vec<WHNF>) -> WHNF {
 
 #[derive(Debug, Clone)]
 enum EnvItem {
-    Expr(WHNF),
+    Expr(Value<WHNF>),
     Skip(V<Label>),
 }
 
@@ -308,7 +308,7 @@ impl NormalizationContext {
     fn new() -> Self {
         NormalizationContext(Rc::new(Context::new()))
     }
-    fn insert(&self, x: &Label, e: WHNF) -> Self {
+    fn insert(&self, x: &Label, e: Value<WHNF>) -> Self {
         NormalizationContext(Rc::new(
             self.0.insert(x.clone(), EnvItem::Expr(e)),
         ))
@@ -320,12 +320,12 @@ impl NormalizationContext {
                 .insert(x.clone(), EnvItem::Skip(V(x.clone(), 0))),
         ))
     }
-    fn lookup(&self, var: &V<Label>) -> WHNF {
+    fn lookup(&self, var: &V<Label>) -> Value<WHNF> {
         let V(x, n) = var;
         match self.0.lookup(x, *n) {
             Some(EnvItem::Expr(e)) => e.clone(),
-            Some(EnvItem::Skip(newvar)) => WHNF::Var(newvar.clone()),
-            None => WHNF::Var(var.clone()),
+            Some(EnvItem::Skip(newvar)) => Value::Var(newvar.clone()),
+            None => Value::Var(var.clone()),
         }
     }
     fn from_typecheck_ctx(tc_ctx: &crate::typecheck::TypecheckContext) -> Self {
@@ -357,159 +357,153 @@ impl NormalizationContext {
     }
 }
 
-/// A semantic value. This is partially redundant with `dhall_core::Expr`, on purpose. `Expr` should
-/// 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,
-/// but only construct `WHNF`s.
+pub(crate) type WHNF = ();
+pub(crate) type NF = X;
+
+/// A semantic value. `Form` should be either `WHNF` or `NF`.
+/// `NF` stands for Normal Form and indicates that all subexpressions are normalized.
+/// `WHNF` stands for Weak Head Normal-Form and indicates that subexpressions may not be normalized.
 ///
-/// WHNFs store some subexpressions unnormalized, to enable lazy normalization. They approximate
-/// what's called Weak Head Normal-Form (WHNF). This means that the expression is normalized as
+/// Weak Head Normal-Form 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 e.g. a record literal
+/// identical to normal form for simple types like integers, but for e.g. a record literal
 /// this means knowing just the field names.
 #[derive(Debug, Clone)]
-pub(crate) enum WHNF {
+pub(crate) enum Value<Form> {
     /// Closures
-    Lam(Label, Thunk, (NormalizationContext, InputSubExpr)),
-    AppliedBuiltin(Builtin, Vec<WHNF>),
+    Lam(Label, Thunk<Form>, (NormalizationContext, InputSubExpr)),
+    AppliedBuiltin(Builtin, Vec<Value<Form>>),
     /// `λ(x: a) -> Some x`
-    OptionalSomeClosure(TypeThunk),
+    OptionalSomeClosure(TypeThunk<Form>),
     /// `λ(x : a) -> λ(xs : List a) -> [ x ] # xs`
     /// `λ(xs : List a) -> [ x ] # xs`
-    ListConsClosure(TypeThunk, Option<Thunk>),
+    ListConsClosure(TypeThunk<Form>, Option<Thunk<Form>>),
     /// `λ(x : Natural) -> x + 1`
     NaturalSuccClosure,
-    Pi(Label, TypeThunk, TypeThunk),
+    Pi(Label, TypeThunk<Form>, TypeThunk<Form>),
 
     Var(V<Label>),
     Const(Const),
     BoolLit(bool),
     NaturalLit(Natural),
     IntegerLit(Integer),
-    EmptyOptionalLit(TypeThunk),
-    NEOptionalLit(Thunk),
-    EmptyListLit(TypeThunk),
-    NEListLit(Vec<Thunk>),
-    RecordLit(BTreeMap<Label, Thunk>),
-    RecordType(BTreeMap<Label, TypeThunk>),
-    UnionType(BTreeMap<Label, Option<TypeThunk>>),
-    UnionConstructor(Label, BTreeMap<Label, Option<TypeThunk>>),
-    UnionLit(Label, Thunk, BTreeMap<Label, Option<TypeThunk>>),
-    TextLit(Vec<InterpolatedTextContents<Thunk>>),
+    EmptyOptionalLit(TypeThunk<Form>),
+    NEOptionalLit(Thunk<Form>),
+    EmptyListLit(TypeThunk<Form>),
+    NEListLit(Vec<Thunk<Form>>),
+    RecordLit(BTreeMap<Label, Thunk<Form>>),
+    RecordType(BTreeMap<Label, TypeThunk<Form>>),
+    UnionType(BTreeMap<Label, Option<TypeThunk<Form>>>),
+    UnionConstructor(Label, BTreeMap<Label, Option<TypeThunk<Form>>>),
+    UnionLit(Label, Thunk<Form>, BTreeMap<Label, Option<TypeThunk<Form>>>),
+    TextLit(Vec<InterpolatedTextContents<Thunk<Form>>>),
     /// This must not contain a value captured by one of the variants above.
     Expr(OutputSubExpr),
 }
 
-impl WHNF {
+impl Value<NF> {
     /// Convert the value back to a (normalized) syntactic expression
     pub(crate) fn normalize_to_expr(self) -> OutputSubExpr {
         match self {
-            WHNF::Lam(x, t, (ctx, e)) => {
+            Value::Lam(x, t, (ctx, e)) => {
                 let ctx2 = ctx.skip(&x);
                 rc(ExprF::Lam(
                     x.clone(),
-                    t.normalize().normalize_to_expr(),
+                    t.to_nf().normalize_to_expr(),
                     normalize_whnf(ctx2, e).normalize_to_expr(),
                 ))
             }
-            WHNF::AppliedBuiltin(b, args) => {
-                let mut e = WHNF::Expr(rc(ExprF::Builtin(b)));
+            Value::AppliedBuiltin(b, args) => {
+                let mut e = rc(ExprF::Builtin(b));
                 for v in args {
-                    e = e.app(v);
+                    e = rc(ExprF::App(e, v.normalize_to_expr()));
                 }
-                e.normalize_to_expr()
+                e
             }
-            WHNF::OptionalSomeClosure(n) => {
-                let a = n.normalize().normalize_to_expr();
+            Value::OptionalSomeClosure(n) => {
+                let a = n.to_nf().normalize_to_expr();
                 dhall::subexpr!(λ(x: a) -> Some x)
             }
-            WHNF::ListConsClosure(n, None) => {
-                let a = n.normalize().normalize_to_expr();
+            Value::ListConsClosure(n, None) => {
+                let a = n.to_nf().normalize_to_expr();
                 // Avoid accidental capture of the new `x` variable
                 let a1 = shift0(1, &"x".into(), &a);
                 dhall::subexpr!(λ(x : a) -> λ(xs : List a1) -> [ x ] # xs)
             }
-            WHNF::ListConsClosure(n, Some(v)) => {
-                let v = v.normalize().normalize_to_expr();
-                let a = n.normalize().normalize_to_expr();
+            Value::ListConsClosure(n, Some(v)) => {
+                let v = v.to_nf().normalize_to_expr();
+                let a = n.to_nf().normalize_to_expr();
                 // Avoid accidental capture of the new `xs` variable
                 let v = shift0(1, &"xs".into(), &v);
                 dhall::subexpr!(λ(xs : List a) -> [ v ] # xs)
             }
-            WHNF::NaturalSuccClosure => {
+            Value::NaturalSuccClosure => {
                 dhall::subexpr!(λ(x : Natural) -> x + 1)
             }
-            WHNF::Pi(x, t, e) => rc(ExprF::Pi(
+            Value::Pi(x, t, e) => rc(ExprF::Pi(
                 x,
-                t.normalize().normalize_to_expr(),
-                e.normalize().normalize_to_expr(),
+                t.to_nf().normalize_to_expr(),
+                e.to_nf().normalize_to_expr(),
             )),
-            WHNF::Var(v) => rc(ExprF::Var(v)),
-            WHNF::Const(c) => rc(ExprF::Const(c)),
-            WHNF::BoolLit(b) => rc(ExprF::BoolLit(b)),
-            WHNF::NaturalLit(n) => rc(ExprF::NaturalLit(n)),
-            WHNF::IntegerLit(n) => rc(ExprF::IntegerLit(n)),
-            WHNF::EmptyOptionalLit(n) => {
-                WHNF::Expr(rc(ExprF::Builtin(Builtin::OptionalNone)))
-                    .app(n.normalize())
-                    .normalize_to_expr()
-            }
-            WHNF::NEOptionalLit(n) => {
-                rc(ExprF::SomeLit(n.normalize().normalize_to_expr()))
+            Value::Var(v) => rc(ExprF::Var(v)),
+            Value::Const(c) => rc(ExprF::Const(c)),
+            Value::BoolLit(b) => rc(ExprF::BoolLit(b)),
+            Value::NaturalLit(n) => rc(ExprF::NaturalLit(n)),
+            Value::IntegerLit(n) => rc(ExprF::IntegerLit(n)),
+            Value::EmptyOptionalLit(n) => rc(ExprF::App(
+                rc(ExprF::Builtin(Builtin::OptionalNone)),
+                n.to_nf().normalize_to_expr(),
+            )),
+            Value::NEOptionalLit(n) => {
+                rc(ExprF::SomeLit(n.to_nf().normalize_to_expr()))
             }
-            WHNF::EmptyListLit(n) => {
-                rc(ExprF::EmptyListLit(n.normalize().normalize_to_expr()))
+            Value::EmptyListLit(n) => {
+                rc(ExprF::EmptyListLit(n.to_nf().normalize_to_expr()))
             }
-            WHNF::NEListLit(elts) => rc(ExprF::NEListLit(
+            Value::NEListLit(elts) => rc(ExprF::NEListLit(
                 elts.into_iter()
-                    .map(|n| n.normalize().normalize_to_expr())
+                    .map(|n| n.to_nf().normalize_to_expr())
                     .collect(),
             )),
-            WHNF::RecordLit(kvs) => rc(ExprF::RecordLit(
+            Value::RecordLit(kvs) => rc(ExprF::RecordLit(
                 kvs.into_iter()
-                    .map(|(k, v)| (k, v.normalize().normalize_to_expr()))
+                    .map(|(k, v)| (k, v.to_nf().normalize_to_expr()))
                     .collect(),
             )),
-            WHNF::RecordType(kts) => rc(ExprF::RecordType(
+            Value::RecordType(kts) => rc(ExprF::RecordType(
                 kts.into_iter()
-                    .map(|(k, v)| (k, v.normalize().normalize_to_expr()))
+                    .map(|(k, v)| (k, v.to_nf().normalize_to_expr()))
                     .collect(),
             )),
-            WHNF::UnionType(kts) => rc(ExprF::UnionType(
+            Value::UnionType(kts) => rc(ExprF::UnionType(
                 kts.into_iter()
-                    .map(|(k, v)| {
-                        (k, v.map(|v| v.normalize().normalize_to_expr()))
-                    })
+                    .map(|(k, v)| (k, v.map(|v| v.to_nf().normalize_to_expr())))
                     .collect(),
             )),
-            WHNF::UnionConstructor(l, kts) => {
+            Value::UnionConstructor(l, kts) => {
                 let kts = kts
                     .into_iter()
-                    .map(|(k, v)| {
-                        (k, v.map(|v| v.normalize().normalize_to_expr()))
-                    })
+                    .map(|(k, v)| (k, v.map(|v| v.to_nf().normalize_to_expr())))
                     .collect();
                 rc(ExprF::Field(rc(ExprF::UnionType(kts)), l))
             }
-            WHNF::UnionLit(l, v, kts) => rc(ExprF::UnionLit(
+            Value::UnionLit(l, v, kts) => rc(ExprF::UnionLit(
                 l,
-                v.normalize().normalize_to_expr(),
+                v.to_nf().normalize_to_expr(),
                 kts.into_iter()
-                    .map(|(k, v)| {
-                        (k, v.map(|v| v.normalize().normalize_to_expr()))
-                    })
+                    .map(|(k, v)| (k, v.map(|v| v.to_nf().normalize_to_expr())))
                     .collect(),
             )),
-            WHNF::TextLit(elts) => {
+            Value::TextLit(elts) => {
                 fn normalize_textlit(
-                    elts: Vec<InterpolatedTextContents<Thunk>>,
+                    elts: Vec<InterpolatedTextContents<Thunk<NF>>>,
                 ) -> InterpolatedText<OutputSubExpr> {
                     elts.into_iter()
                         .flat_map(|contents| {
                             use InterpolatedTextContents::{Expr, Text};
                             let new_interpolated = match contents {
-                                Expr(n) => match n.normalize() {
-                                    WHNF::TextLit(elts2) => {
+                                Expr(n) => match n.to_nf() {
+                                    Value::TextLit(elts2) => {
                                         normalize_textlit(elts2)
                                     }
                                     e => InterpolatedText::from((
@@ -529,116 +523,204 @@ impl WHNF {
 
                 rc(ExprF::TextLit(normalize_textlit(elts)))
             }
-            WHNF::Expr(e) => e,
+            Value::Expr(e) => e,
+        }
+    }
+}
+
+impl Value<WHNF> {
+    pub(crate) fn normalize_to_expr(self) -> OutputSubExpr {
+        self.normalize().normalize_to_expr()
+    }
+
+    pub(crate) fn normalize(&self) -> Value<NF> {
+        match self {
+            Value::Lam(x, t, (ctx, e)) => {
+                Value::Lam(x.clone(), t.normalize(), (ctx.clone(), e.clone()))
+            }
+            Value::AppliedBuiltin(b, args) => Value::AppliedBuiltin(
+                *b,
+                args.iter().map(|v| v.normalize()).collect(),
+            ),
+            Value::NaturalSuccClosure => Value::NaturalSuccClosure,
+            Value::OptionalSomeClosure(tth) => {
+                Value::OptionalSomeClosure(tth.normalize())
+            }
+            Value::ListConsClosure(t, v) => Value::ListConsClosure(
+                t.normalize(),
+                v.as_ref().map(|v| v.normalize()),
+            ),
+            Value::Pi(x, t, e) => {
+                Value::Pi(x.clone(), t.normalize(), e.normalize())
+            }
+            Value::Var(v) => Value::Var(v.clone()),
+            Value::Const(c) => Value::Const(*c),
+            Value::BoolLit(b) => Value::BoolLit(*b),
+            Value::NaturalLit(n) => Value::NaturalLit(*n),
+            Value::IntegerLit(n) => Value::IntegerLit(*n),
+            Value::EmptyOptionalLit(tth) => {
+                Value::EmptyOptionalLit(tth.normalize())
+            }
+            Value::NEOptionalLit(th) => Value::NEOptionalLit(th.normalize()),
+            Value::EmptyListLit(tth) => Value::EmptyListLit(tth.normalize()),
+            Value::NEListLit(elts) => {
+                Value::NEListLit(elts.iter().map(|v| v.normalize()).collect())
+            }
+            Value::RecordLit(kvs) => Value::RecordLit(
+                kvs.iter()
+                    .map(|(k, v)| (k.clone(), v.normalize()))
+                    .collect(),
+            ),
+            Value::RecordType(kvs) => Value::RecordType(
+                kvs.iter()
+                    .map(|(k, v)| (k.clone(), v.normalize()))
+                    .collect(),
+            ),
+            Value::UnionType(kts) => Value::UnionType(
+                kts.iter()
+                    .map(|(k, v)| {
+                        (k.clone(), v.as_ref().map(|v| v.normalize()))
+                    })
+                    .collect(),
+            ),
+            Value::UnionConstructor(x, kts) => Value::UnionConstructor(
+                x.clone(),
+                kts.iter()
+                    .map(|(k, v)| {
+                        (k.clone(), v.as_ref().map(|v| v.normalize()))
+                    })
+                    .collect(),
+            ),
+            Value::UnionLit(x, v, kts) => Value::UnionLit(
+                x.clone(),
+                v.normalize(),
+                kts.iter()
+                    .map(|(k, v)| {
+                        (k.clone(), v.as_ref().map(|v| v.normalize()))
+                    })
+                    .collect(),
+            ),
+            Value::TextLit(elts) => Value::TextLit(
+                elts.iter()
+                    .map(|contents| {
+                        use InterpolatedTextContents::{Expr, Text};
+                        match contents {
+                            Expr(th) => Expr(th.normalize()),
+                            Text(s) => Text(s.clone()),
+                        }
+                    })
+                    .collect(),
+            ),
+            Value::Expr(e) => Value::Expr(e.clone()),
         }
     }
 
     /// Apply to a value
-    pub(crate) fn app(self, val: WHNF) -> WHNF {
+    pub(crate) fn app(self, val: Value<WHNF>) -> Value<WHNF> {
         match (self, val) {
-            (WHNF::Lam(x, _, (ctx, e)), val) => {
+            (Value::Lam(x, _, (ctx, e)), val) => {
                 let ctx2 = ctx.insert(&x, val);
                 normalize_whnf(ctx2, e)
             }
-            (WHNF::AppliedBuiltin(b, mut args), val) => {
+            (Value::AppliedBuiltin(b, mut args), val) => {
                 args.push(val);
                 apply_builtin(b, args)
             }
-            (WHNF::OptionalSomeClosure(_), val) => {
-                WHNF::NEOptionalLit(Thunk::from_whnf(val))
+            (Value::OptionalSomeClosure(_), val) => {
+                Value::NEOptionalLit(Thunk::from_whnf(val))
             }
-            (WHNF::ListConsClosure(t, None), val) => {
-                WHNF::ListConsClosure(t, Some(Thunk::from_whnf(val)))
+            (Value::ListConsClosure(t, None), val) => {
+                Value::ListConsClosure(t, Some(Thunk::from_whnf(val)))
             }
-            (WHNF::ListConsClosure(_, Some(x)), WHNF::EmptyListLit(_)) => {
-                WHNF::NEListLit(vec![x])
+            (Value::ListConsClosure(_, Some(x)), Value::EmptyListLit(_)) => {
+                Value::NEListLit(vec![x])
             }
-            (WHNF::ListConsClosure(_, Some(x)), WHNF::NEListLit(mut xs)) => {
+            (Value::ListConsClosure(_, Some(x)), Value::NEListLit(mut xs)) => {
                 xs.insert(0, x);
-                WHNF::NEListLit(xs)
+                Value::NEListLit(xs)
             }
-            (WHNF::NaturalSuccClosure, WHNF::NaturalLit(n)) => {
-                WHNF::NaturalLit(n + 1)
+            (Value::NaturalSuccClosure, Value::NaturalLit(n)) => {
+                Value::NaturalLit(n + 1)
             }
-            (WHNF::UnionConstructor(l, kts), val) => {
-                WHNF::UnionLit(l, Thunk::from_whnf(val), kts)
+            (Value::UnionConstructor(l, kts), val) => {
+                Value::UnionLit(l, Thunk::from_whnf(val), kts)
             }
             // Can't do anything useful, convert to expr
-            (f, a) => WHNF::Expr(rc(ExprF::App(
+            (f, a) => Value::Expr(rc(ExprF::App(
                 f.normalize_to_expr(),
                 a.normalize_to_expr(),
             ))),
         }
     }
 
-    pub(crate) fn from_builtin(b: Builtin) -> WHNF {
-        WHNF::AppliedBuiltin(b, vec![])
+    pub(crate) fn from_builtin(b: Builtin) -> Value<WHNF> {
+        Value::AppliedBuiltin(b, vec![])
     }
 
     fn shift(&mut self, delta: isize, var: &V<Label>) {
         match self {
-            WHNF::Var(v) => {
+            Value::Var(v) => {
                 std::mem::replace(v, v.shift(delta, var));
             }
-            WHNF::NaturalSuccClosure
-            | WHNF::Const(_)
-            | WHNF::BoolLit(_)
-            | WHNF::NaturalLit(_)
-            | WHNF::IntegerLit(_) => {}
-            WHNF::EmptyOptionalLit(tth)
-            | WHNF::OptionalSomeClosure(tth)
-            | WHNF::EmptyListLit(tth) => {
+            Value::NaturalSuccClosure
+            | Value::Const(_)
+            | Value::BoolLit(_)
+            | Value::NaturalLit(_)
+            | Value::IntegerLit(_) => {}
+            Value::EmptyOptionalLit(tth)
+            | Value::OptionalSomeClosure(tth)
+            | Value::EmptyListLit(tth) => {
                 tth.shift(delta, var);
             }
-            WHNF::NEOptionalLit(th) => {
+            Value::NEOptionalLit(th) => {
                 th.shift(delta, var);
             }
-            WHNF::Lam(x, t, (_, e)) => {
+            Value::Lam(x, t, (_, e)) => {
                 t.shift(delta, var);
                 shift_mut(delta, &var.shift0(1, x), e);
             }
-            WHNF::AppliedBuiltin(_, args) => {
+            Value::AppliedBuiltin(_, args) => {
                 for x in args.iter_mut() {
                     x.shift(delta, var);
                 }
             }
-            WHNF::ListConsClosure(t, v) => {
+            Value::ListConsClosure(t, v) => {
                 t.shift(delta, var);
                 for x in v.iter_mut() {
                     x.shift(delta, var);
                 }
             }
-            WHNF::Pi(x, t, e) => {
+            Value::Pi(x, t, e) => {
                 t.shift(delta, var);
                 e.shift(delta, &var.shift0(1, x));
             }
-            WHNF::NEListLit(elts) => {
+            Value::NEListLit(elts) => {
                 for x in elts.iter_mut() {
                     x.shift(delta, var);
                 }
             }
-            WHNF::RecordLit(kvs) => {
+            Value::RecordLit(kvs) => {
                 for x in kvs.values_mut() {
                     x.shift(delta, var);
                 }
             }
-            WHNF::RecordType(kvs) => {
+            Value::RecordType(kvs) => {
                 for x in kvs.values_mut() {
                     x.shift(delta, var);
                 }
             }
-            WHNF::UnionType(kts) | WHNF::UnionConstructor(_, kts) => {
+            Value::UnionType(kts) | Value::UnionConstructor(_, kts) => {
                 for x in kts.values_mut().flat_map(|opt| opt) {
                     x.shift(delta, var);
                 }
             }
-            WHNF::UnionLit(_, v, kts) => {
+            Value::UnionLit(_, v, kts) => {
                 v.shift(delta, var);
                 for x in kts.values_mut().flat_map(|opt| opt) {
                     x.shift(delta, var);
                 }
             }
-            WHNF::TextLit(elts) => {
+            Value::TextLit(elts) => {
                 for x in elts.iter_mut() {
                     use InterpolatedTextContents::{Expr, Text};
                     match x {
@@ -647,7 +729,7 @@ impl WHNF {
                     }
                 }
             }
-            WHNF::Expr(e) => shift_mut(delta, var, e),
+            Value::Expr(e) => shift_mut(delta, var, e),
         }
     }
 
@@ -657,64 +739,64 @@ impl WHNF {
         val: &PartiallyNormalized<'static>,
     ) -> Self {
         match self {
-            WHNF::Lam(x, t, (ctx, e)) => WHNF::Lam(
+            Value::Lam(x, t, (ctx, e)) => Value::Lam(
                 x.clone(),
                 t.subst_shift(var, val),
                 (ctx.subst_shift(var, val), e.clone()),
             ),
-            WHNF::AppliedBuiltin(b, args) => WHNF::AppliedBuiltin(
+            Value::AppliedBuiltin(b, args) => Value::AppliedBuiltin(
                 *b,
                 args.iter().map(|v| v.subst_shift(var, val)).collect(),
             ),
-            WHNF::NaturalSuccClosure => WHNF::NaturalSuccClosure,
-            WHNF::OptionalSomeClosure(tth) => {
-                WHNF::OptionalSomeClosure(tth.subst_shift(var, val))
+            Value::NaturalSuccClosure => Value::NaturalSuccClosure,
+            Value::OptionalSomeClosure(tth) => {
+                Value::OptionalSomeClosure(tth.subst_shift(var, val))
             }
-            WHNF::ListConsClosure(t, v) => WHNF::ListConsClosure(
+            Value::ListConsClosure(t, v) => Value::ListConsClosure(
                 t.subst_shift(var, val),
                 v.as_ref().map(|v| v.subst_shift(var, val)),
             ),
-            WHNF::Pi(x, t, e) => WHNF::Pi(
+            Value::Pi(x, t, e) => Value::Pi(
                 x.clone(),
                 t.subst_shift(var, val),
                 e.subst_shift(&var.shift0(1, x), val),
             ),
-            WHNF::Var(v) if v == var => val.clone().into_whnf(),
-            WHNF::Var(v) => WHNF::Var(v.shift(-1, var)),
-            WHNF::Const(c) => WHNF::Const(*c),
-            WHNF::BoolLit(b) => WHNF::BoolLit(*b),
-            WHNF::NaturalLit(n) => WHNF::NaturalLit(*n),
-            WHNF::IntegerLit(n) => WHNF::IntegerLit(*n),
-            WHNF::EmptyOptionalLit(tth) => {
-                WHNF::EmptyOptionalLit(tth.subst_shift(var, val))
+            Value::Var(v) if v == var => val.clone().into_whnf(),
+            Value::Var(v) => Value::Var(v.shift(-1, var)),
+            Value::Const(c) => Value::Const(*c),
+            Value::BoolLit(b) => Value::BoolLit(*b),
+            Value::NaturalLit(n) => Value::NaturalLit(*n),
+            Value::IntegerLit(n) => Value::IntegerLit(*n),
+            Value::EmptyOptionalLit(tth) => {
+                Value::EmptyOptionalLit(tth.subst_shift(var, val))
             }
-            WHNF::NEOptionalLit(th) => {
-                WHNF::NEOptionalLit(th.subst_shift(var, val))
+            Value::NEOptionalLit(th) => {
+                Value::NEOptionalLit(th.subst_shift(var, val))
             }
-            WHNF::EmptyListLit(tth) => {
-                WHNF::EmptyListLit(tth.subst_shift(var, val))
+            Value::EmptyListLit(tth) => {
+                Value::EmptyListLit(tth.subst_shift(var, val))
             }
-            WHNF::NEListLit(elts) => WHNF::NEListLit(
+            Value::NEListLit(elts) => Value::NEListLit(
                 elts.iter().map(|v| v.subst_shift(var, val)).collect(),
             ),
-            WHNF::RecordLit(kvs) => WHNF::RecordLit(
+            Value::RecordLit(kvs) => Value::RecordLit(
                 kvs.iter()
                     .map(|(k, v)| (k.clone(), v.subst_shift(var, val)))
                     .collect(),
             ),
-            WHNF::RecordType(kvs) => WHNF::RecordType(
+            Value::RecordType(kvs) => Value::RecordType(
                 kvs.iter()
                     .map(|(k, v)| (k.clone(), v.subst_shift(var, val)))
                     .collect(),
             ),
-            WHNF::UnionType(kts) => WHNF::UnionType(
+            Value::UnionType(kts) => Value::UnionType(
                 kts.iter()
                     .map(|(k, v)| {
                         (k.clone(), v.as_ref().map(|v| v.subst_shift(var, val)))
                     })
                     .collect(),
             ),
-            WHNF::UnionConstructor(x, kts) => WHNF::UnionConstructor(
+            Value::UnionConstructor(x, kts) => Value::UnionConstructor(
                 x.clone(),
                 kts.iter()
                     .map(|(k, v)| {
@@ -722,7 +804,7 @@ impl WHNF {
                     })
                     .collect(),
             ),
-            WHNF::UnionLit(x, v, kts) => WHNF::UnionLit(
+            Value::UnionLit(x, v, kts) => Value::UnionLit(
                 x.clone(),
                 v.subst_shift(var, val),
                 kts.iter()
@@ -731,7 +813,7 @@ impl WHNF {
                     })
                     .collect(),
             ),
-            WHNF::TextLit(elts) => WHNF::TextLit(
+            Value::TextLit(elts) => Value::TextLit(
                 elts.iter()
                     .map(|contents| {
                         use InterpolatedTextContents::{Expr, Text};
@@ -742,7 +824,7 @@ impl WHNF {
                     })
                     .collect(),
             ),
-            WHNF::Expr(e) => WHNF::Expr(
+            Value::Expr(e) => Value::Expr(
                 e.subst_shift(var, &val.clone().normalize().as_expr()),
             ),
         }
@@ -752,31 +834,37 @@ impl WHNF {
 /// Contains either a (partially) normalized value or a
 /// non-normalized value alongside a normalization context.
 #[derive(Debug, Clone)]
-pub(crate) enum Thunk {
-    Normalized(Box<WHNF>),
-    Unnormalized(NormalizationContext, InputSubExpr),
+pub(crate) enum Thunk<Form> {
+    Value(Box<Value<Form>>),
+    Unnormalized(Form, NormalizationContext, InputSubExpr),
 }
 
-impl Thunk {
-    fn new(ctx: NormalizationContext, e: InputSubExpr) -> Self {
-        Thunk::Unnormalized(ctx, e)
+impl Thunk<WHNF> {
+    fn new(ctx: NormalizationContext, e: InputSubExpr) -> Thunk<WHNF> {
+        Thunk::Unnormalized((), ctx, e)
     }
 
-    fn from_whnf(v: WHNF) -> Self {
-        Thunk::Normalized(Box::new(v))
+    fn from_whnf(v: Value<WHNF>) -> Thunk<WHNF> {
+        Thunk::Value(Box::new(v))
     }
 
-    pub(crate) fn normalize(self) -> WHNF {
+    pub(crate) fn normalize_whnf(&self) -> Value<WHNF> {
         match self {
-            Thunk::Normalized(v) => *v,
-            Thunk::Unnormalized(ctx, e) => normalize_whnf(ctx, e),
+            Thunk::Value(v) => (**v).clone(),
+            Thunk::Unnormalized(_, ctx, e) => {
+                normalize_whnf(ctx.clone(), e.clone())
+            }
         }
     }
 
+    fn normalize(&self) -> Thunk<NF> {
+        Thunk::Value(Box::new(self.normalize_whnf().normalize()))
+    }
+
     fn shift(&mut self, delta: isize, var: &V<Label>) {
         match self {
-            Thunk::Normalized(v) => v.shift(delta, var),
-            Thunk::Unnormalized(_, e) => shift_mut(delta, var, e),
+            Thunk::Value(v) => v.shift(delta, var),
+            Thunk::Unnormalized(_, _, e) => shift_mut(delta, var, e),
         }
     }
 
@@ -786,45 +874,53 @@ impl Thunk {
         val: &PartiallyNormalized<'static>,
     ) -> Self {
         match self {
-            Thunk::Normalized(v) => {
-                Thunk::Normalized(Box::new(v.subst_shift(var, val)))
-            }
-            Thunk::Unnormalized(ctx, e) => {
-                Thunk::Unnormalized(ctx.subst_shift(var, val), e.clone())
-            }
+            Thunk::Value(v) => Thunk::Value(Box::new(v.subst_shift(var, val))),
+            Thunk::Unnormalized(marker, ctx, e) => Thunk::Unnormalized(
+                marker.clone(),
+                ctx.subst_shift(var, val),
+                e.clone(),
+            ),
+        }
+    }
+}
+
+impl Thunk<NF> {
+    pub(crate) fn to_nf(&self) -> Value<NF> {
+        match self {
+            Thunk::Value(v) => (**v).clone(),
+            Thunk::Unnormalized(m, _, _) => match *m {},
         }
     }
 }
 
 /// A thunk in type position.
 #[derive(Debug, Clone)]
-pub(crate) enum TypeThunk {
-    Thunk(Thunk),
+pub(crate) enum TypeThunk<Form> {
+    Thunk(Thunk<Form>),
     Type(Type<'static>),
 }
 
-impl TypeThunk {
-    fn new(ctx: NormalizationContext, e: InputSubExpr) -> Self {
+impl TypeThunk<WHNF> {
+    fn new(ctx: NormalizationContext, e: InputSubExpr) -> TypeThunk<WHNF> {
         TypeThunk::from_thunk(Thunk::new(ctx, e))
     }
 
-    fn from_thunk(th: Thunk) -> Self {
-        TypeThunk::Thunk(th)
+    fn from_whnf(v: Value<WHNF>) -> TypeThunk<WHNF> {
+        TypeThunk::from_thunk(Thunk::from_whnf(v))
     }
 
-    pub(crate) fn from_type(t: Type<'static>) -> Self {
-        TypeThunk::Type(t)
+    fn from_thunk(th: Thunk<WHNF>) -> TypeThunk<WHNF> {
+        TypeThunk::Thunk(th)
     }
 
-    fn from_whnf(v: WHNF) -> Self {
-        TypeThunk::from_thunk(Thunk::from_whnf(v))
+    pub(crate) fn from_type(t: Type<'static>) -> TypeThunk<WHNF> {
+        TypeThunk::Type(t)
     }
 
-    pub(crate) fn normalize(self) -> WHNF {
+    fn normalize(&self) -> TypeThunk<NF> {
         match self {
-            TypeThunk::Thunk(th) => th.normalize(),
-            // TODO: let's hope for the best with the unwrap
-            TypeThunk::Type(t) => t.partially_normalize().unwrap().into_whnf(),
+            TypeThunk::Thunk(th) => TypeThunk::Thunk(th.normalize()),
+            TypeThunk::Type(t) => TypeThunk::Type(t.clone()),
         }
     }
 
@@ -850,8 +946,26 @@ impl TypeThunk {
     }
 }
 
-/// Reduces the imput expression to WHNF. See doc on `WHNF` for details.
-fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> WHNF {
+impl TypeThunk<NF> {
+    pub(crate) fn to_nf(&self) -> Value<NF> {
+        match self {
+            TypeThunk::Thunk(th) => th.to_nf(),
+            // TODO: let's hope for the best with the unwrap
+            TypeThunk::Type(t) => t
+                .clone()
+                .partially_normalize()
+                .unwrap()
+                .into_whnf()
+                .normalize(),
+        }
+    }
+}
+
+/// Reduces the imput expression to Value. See doc on `Value` for details.
+fn normalize_whnf(
+    ctx: NormalizationContext,
+    expr: InputSubExpr,
+) -> Value<WHNF> {
     match expr.as_ref() {
         ExprF::Var(v) => ctx.lookup(&v),
         ExprF::Annot(x, _) => normalize_whnf(ctx, x.clone()),
@@ -864,36 +978,36 @@ fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> WHNF {
             let r = normalize_whnf(ctx.clone(), r.clone());
             normalize_whnf(ctx.insert(x, r), b.clone())
         }
-        ExprF::Lam(x, t, e) => WHNF::Lam(
+        ExprF::Lam(x, t, e) => Value::Lam(
             x.clone(),
             Thunk::new(ctx.clone(), t.clone()),
             (ctx, e.clone()),
         ),
-        ExprF::Builtin(b) => WHNF::from_builtin(*b),
-        ExprF::Const(c) => WHNF::Const(*c),
-        ExprF::BoolLit(b) => WHNF::BoolLit(*b),
-        ExprF::NaturalLit(n) => WHNF::NaturalLit(*n),
+        ExprF::Builtin(b) => Value::from_builtin(*b),
+        ExprF::Const(c) => Value::Const(*c),
+        ExprF::BoolLit(b) => Value::BoolLit(*b),
+        ExprF::NaturalLit(n) => Value::NaturalLit(*n),
         ExprF::OldOptionalLit(None, e) => {
-            WHNF::EmptyOptionalLit(TypeThunk::new(ctx, e.clone()))
+            Value::EmptyOptionalLit(TypeThunk::new(ctx, e.clone()))
         }
         ExprF::OldOptionalLit(Some(e), _) => {
-            WHNF::NEOptionalLit(Thunk::new(ctx, e.clone()))
+            Value::NEOptionalLit(Thunk::new(ctx, e.clone()))
         }
-        ExprF::SomeLit(e) => WHNF::NEOptionalLit(Thunk::new(ctx, e.clone())),
+        ExprF::SomeLit(e) => Value::NEOptionalLit(Thunk::new(ctx, e.clone())),
         ExprF::EmptyListLit(e) => {
-            WHNF::EmptyListLit(TypeThunk::new(ctx, e.clone()))
+            Value::EmptyListLit(TypeThunk::new(ctx, e.clone()))
         }
-        ExprF::NEListLit(elts) => WHNF::NEListLit(
+        ExprF::NEListLit(elts) => Value::NEListLit(
             elts.iter()
                 .map(|e| Thunk::new(ctx.clone(), e.clone()))
                 .collect(),
         ),
-        ExprF::RecordLit(kvs) => WHNF::RecordLit(
+        ExprF::RecordLit(kvs) => Value::RecordLit(
             kvs.iter()
                 .map(|(k, e)| (k.clone(), Thunk::new(ctx.clone(), e.clone())))
                 .collect(),
         ),
-        ExprF::UnionType(kts) => WHNF::UnionType(
+        ExprF::UnionType(kts) => Value::UnionType(
             kts.iter()
                 .map(|(k, t)| {
                     (
@@ -904,7 +1018,7 @@ fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> WHNF {
                 })
                 .collect(),
         ),
-        ExprF::UnionLit(l, x, kts) => WHNF::UnionLit(
+        ExprF::UnionLit(l, x, kts) => Value::UnionLit(
             l.clone(),
             Thunk::new(ctx.clone(), x.clone()),
             kts.iter()
@@ -917,7 +1031,7 @@ fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> WHNF {
                 })
                 .collect(),
         ),
-        ExprF::TextLit(elts) => WHNF::TextLit(
+        ExprF::TextLit(elts) => Value::TextLit(
             elts.iter()
                 .map(|contents| {
                     use InterpolatedTextContents::{Expr, Text};
@@ -931,13 +1045,13 @@ fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> WHNF {
         ExprF::BoolIf(b, e1, e2) => {
             let b = normalize_whnf(ctx.clone(), b.clone());
             match b {
-                WHNF::BoolLit(true) => normalize_whnf(ctx, e1.clone()),
-                WHNF::BoolLit(false) => normalize_whnf(ctx, e2.clone()),
+                Value::BoolLit(true) => normalize_whnf(ctx, e1.clone()),
+                Value::BoolLit(false) => normalize_whnf(ctx, e2.clone()),
                 b => {
                     let e1 = normalize_whnf(ctx.clone(), e1.clone());
                     let e2 = normalize_whnf(ctx, e2.clone());
                     match (e1, e2) {
-                        (WHNF::BoolLit(true), WHNF::BoolLit(false)) => b,
+                        (Value::BoolLit(true), Value::BoolLit(false)) => b,
                         (e1, e2) => {
                             normalize_last_layer(ExprF::BoolIf(b, e1, e2))
                         }
@@ -947,7 +1061,7 @@ fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> WHNF {
         }
         expr => {
             // Recursively normalize subexpressions
-            let expr: ExprF<WHNF, Label, X, X> = expr
+            let expr: ExprF<Value<WHNF>, Label, X, X> = expr
                 .map_ref_with_special_handling_of_binders(
                     |e| normalize_whnf(ctx.clone(), e.clone()),
                     |x, e| normalize_whnf(ctx.skip(x), e.clone()),
@@ -962,9 +1076,9 @@ fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> WHNF {
 }
 
 /// When all sub-expressions have been (partially) normalized, eval the remaining toplevel layer.
-fn normalize_last_layer(expr: ExprF<WHNF, Label, X, X>) -> WHNF {
+fn normalize_last_layer(expr: ExprF<Value<WHNF>, Label, X, X>) -> Value<WHNF> {
     use dhall_core::BinOp::*;
-    use WHNF::*;
+    use Value::*;
 
     match expr {
         ExprF::App(v, a) => v.app(a),
@@ -1012,7 +1126,7 @@ fn normalize_last_layer(expr: ExprF<WHNF, Label, X, X>) -> WHNF {
 
         ExprF::Field(UnionType(kts), l) => UnionConstructor(l, kts),
         ExprF::Field(RecordLit(mut kvs), l) => match kvs.remove(&l) {
-            Some(r) => r.normalize(),
+            Some(r) => r.normalize_whnf(),
             None => {
                 // Couldn't do anything useful, so just normalize subexpressions
                 Expr(rc(ExprF::Field(RecordLit(kvs).normalize_to_expr(), l)))
@@ -1029,13 +1143,13 @@ fn normalize_last_layer(expr: ExprF<WHNF, Label, X, X>) -> WHNF {
         ExprF::Merge(RecordLit(mut handlers), e, t) => {
             let e = match e {
                 UnionConstructor(l, kts) => match handlers.remove(&l) {
-                    Some(h) => return h.normalize(),
+                    Some(h) => return h.normalize_whnf(),
                     None => UnionConstructor(l, kts),
                 },
                 UnionLit(l, v, kts) => match handlers.remove(&l) {
                     Some(h) => {
-                        let h = h.normalize();
-                        let v = v.normalize();
+                        let h = h.normalize_whnf();
+                        let v = v.normalize_whnf();
                         return h.app(v);
                     }
                     None => UnionLit(l, v, kts),
@@ -1046,7 +1160,7 @@ fn normalize_last_layer(expr: ExprF<WHNF, Label, X, X>) -> WHNF {
             Expr(rc(ExprF::Merge(
                 RecordLit(handlers).normalize_to_expr(),
                 e.normalize_to_expr(),
-                t.map(WHNF::normalize_to_expr),
+                t.map(<Value<WHNF>>::normalize_to_expr),
             )))
         }
         // Couldn't do anything useful, so just normalize subexpressions
-- 
cgit v1.2.3


From b9dc8ebd0e72a04c0d7f890d863e596eaa2f170e Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 29 Apr 2019 21:38:16 +0200
Subject: Store thunk in Value::Lambda

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

(limited to 'dhall/src/normalize.rs')

diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index b5971cb..2fa3bc5 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -371,7 +371,7 @@ pub(crate) type NF = X;
 #[derive(Debug, Clone)]
 pub(crate) enum Value<Form> {
     /// Closures
-    Lam(Label, Thunk<Form>, (NormalizationContext, InputSubExpr)),
+    Lam(Label, Thunk<Form>, Thunk<Form>),
     AppliedBuiltin(Builtin, Vec<Value<Form>>),
     /// `λ(x: a) -> Some x`
     OptionalSomeClosure(TypeThunk<Form>),
@@ -405,14 +405,11 @@ impl Value<NF> {
     /// Convert the value back to a (normalized) syntactic expression
     pub(crate) fn normalize_to_expr(self) -> OutputSubExpr {
         match self {
-            Value::Lam(x, t, (ctx, e)) => {
-                let ctx2 = ctx.skip(&x);
-                rc(ExprF::Lam(
-                    x.clone(),
-                    t.to_nf().normalize_to_expr(),
-                    normalize_whnf(ctx2, e).normalize_to_expr(),
-                ))
-            }
+            Value::Lam(x, t, e) => rc(ExprF::Lam(
+                x.clone(),
+                t.to_nf().normalize_to_expr(),
+                e.to_nf().normalize_to_expr(),
+            )),
             Value::AppliedBuiltin(b, args) => {
                 let mut e = rc(ExprF::Builtin(b));
                 for v in args {
@@ -535,8 +532,8 @@ impl Value<WHNF> {
 
     pub(crate) fn normalize(&self) -> Value<NF> {
         match self {
-            Value::Lam(x, t, (ctx, e)) => {
-                Value::Lam(x.clone(), t.normalize(), (ctx.clone(), e.clone()))
+            Value::Lam(x, t, e) => {
+                Value::Lam(x.clone(), t.normalize(), e.normalize())
             }
             Value::AppliedBuiltin(b, args) => Value::AppliedBuiltin(
                 *b,
@@ -618,9 +615,10 @@ impl Value<WHNF> {
     /// Apply to a value
     pub(crate) fn app(self, val: Value<WHNF>) -> Value<WHNF> {
         match (self, val) {
-            (Value::Lam(x, _, (ctx, e)), val) => {
-                let ctx2 = ctx.insert(&x, val);
-                normalize_whnf(ctx2, e)
+            (Value::Lam(x, _, e), val) => {
+                let val =
+                    PartiallyNormalized(val, None, std::marker::PhantomData);
+                e.subst_shift(&V(x, 0), &val).normalize_whnf()
             }
             (Value::AppliedBuiltin(b, mut args), val) => {
                 args.push(val);
@@ -675,9 +673,9 @@ impl Value<WHNF> {
             Value::NEOptionalLit(th) => {
                 th.shift(delta, var);
             }
-            Value::Lam(x, t, (_, e)) => {
+            Value::Lam(x, t, e) => {
                 t.shift(delta, var);
-                shift_mut(delta, &var.shift0(1, x), e);
+                e.shift(delta, &var.shift0(1, x));
             }
             Value::AppliedBuiltin(_, args) => {
                 for x in args.iter_mut() {
@@ -739,10 +737,10 @@ impl Value<WHNF> {
         val: &PartiallyNormalized<'static>,
     ) -> Self {
         match self {
-            Value::Lam(x, t, (ctx, e)) => Value::Lam(
+            Value::Lam(x, t, e) => Value::Lam(
                 x.clone(),
                 t.subst_shift(var, val),
-                (ctx.subst_shift(var, val), e.clone()),
+                e.subst_shift(&var.shift0(1, x), val),
             ),
             Value::AppliedBuiltin(b, args) => Value::AppliedBuiltin(
                 *b,
@@ -981,7 +979,7 @@ fn normalize_whnf(
         ExprF::Lam(x, t, e) => Value::Lam(
             x.clone(),
             Thunk::new(ctx.clone(), t.clone()),
-            (ctx, e.clone()),
+            Thunk::new(ctx.skip(x), e.clone()),
         ),
         ExprF::Builtin(b) => Value::from_builtin(*b),
         ExprF::Const(c) => Value::Const(*c),
-- 
cgit v1.2.3


From 439947345ef52ce04a66b1d4fa9c05d2b6964fa1 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 29 Apr 2019 21:52:47 +0200
Subject: Don't shift by mutable ref

---
 dhall/src/normalize.rs | 199 ++++++++++++++++++++++++++-----------------------
 1 file changed, 106 insertions(+), 93 deletions(-)

(limited to 'dhall/src/normalize.rs')

diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 2fa3bc5..43e7292 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -4,7 +4,7 @@ use std::rc::Rc;
 
 use dhall_core::context::Context;
 use dhall_core::{
-    rc, shift, shift0, Builtin, Const, ExprF, Integer, InterpolatedText,
+    rc, Builtin, Const, ExprF, Integer, InterpolatedText,
     InterpolatedTextContents, Label, Natural, SubExpr, V, X,
 };
 use dhall_generator as dhall;
@@ -53,10 +53,8 @@ impl<'a> PartiallyNormalized<'a> {
         Normalized(self.0.normalize_to_expr(), self.1, self.2)
     }
     pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
-        let mut e = self.0.clone();
-        e.shift(delta, var);
         PartiallyNormalized(
-            e,
+            self.0.shift(delta, var),
             self.1.as_ref().map(|x| x.shift(delta, var)),
             self.2,
         )
@@ -77,11 +75,6 @@ impl<'a> PartiallyNormalized<'a> {
     }
 }
 
-fn shift_mut<N, E>(delta: isize, var: &V<Label>, in_expr: &mut SubExpr<N, E>) {
-    let new_expr = shift(delta, var, &in_expr);
-    std::mem::replace(in_expr, new_expr);
-}
-
 fn apply_builtin(b: Builtin, args: Vec<Value<WHNF>>) -> Value<WHNF> {
     use dhall_core::Builtin::*;
     use Value::*;
@@ -277,16 +270,17 @@ enum EnvItem {
 
 impl EnvItem {
     fn shift0(&self, delta: isize, x: &Label) -> Self {
+        self.shift(delta, &V(x.clone(), 0))
+    }
+
+    fn shift(&self, delta: isize, var: &V<Label>) -> Self {
         use EnvItem::*;
         match self {
-            Expr(e) => {
-                let mut e = e.clone();
-                e.shift(delta, &V(x.clone(), 0));
-                Expr(e)
-            }
-            Skip(var) => Skip(var.shift0(delta, x)),
+            Expr(e) => Expr(e.shift(delta, var)),
+            Skip(v) => Skip(v.shift(delta, var)),
         }
     }
+
     pub(crate) fn subst_shift(
         &self,
         var: &V<Label>,
@@ -346,6 +340,10 @@ impl NormalizationContext {
         NormalizationContext(Rc::new(ctx))
     }
 
+    fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+        NormalizationContext(Rc::new(self.0.map(|_, e| e.shift(delta, var))))
+    }
+
     fn subst_shift(
         &self,
         var: &V<Label>,
@@ -424,14 +422,14 @@ impl Value<NF> {
             Value::ListConsClosure(n, None) => {
                 let a = n.to_nf().normalize_to_expr();
                 // Avoid accidental capture of the new `x` variable
-                let a1 = shift0(1, &"x".into(), &a);
+                let a1 = a.shift0(1, &"x".into());
                 dhall::subexpr!(λ(x : a) -> λ(xs : List a1) -> [ x ] # xs)
             }
             Value::ListConsClosure(n, Some(v)) => {
                 let v = v.to_nf().normalize_to_expr();
                 let a = n.to_nf().normalize_to_expr();
                 // Avoid accidental capture of the new `xs` variable
-                let v = shift0(1, &"xs".into(), &v);
+                let v = v.shift0(1, &"xs".into());
                 dhall::subexpr!(λ(xs : List a) -> [ v ] # xs)
             }
             Value::NaturalSuccClosure => {
@@ -655,79 +653,93 @@ impl Value<WHNF> {
         Value::AppliedBuiltin(b, vec![])
     }
 
-    fn shift(&mut self, delta: isize, var: &V<Label>) {
+    fn shift(&self, delta: isize, var: &V<Label>) -> Self {
         match self {
-            Value::Var(v) => {
-                std::mem::replace(v, v.shift(delta, var));
+            Value::Lam(x, t, e) => Value::Lam(
+                x.clone(),
+                t.shift(delta, var),
+                e.shift(delta, &var.shift0(1, x)),
+            ),
+            Value::AppliedBuiltin(b, args) => Value::AppliedBuiltin(
+                *b,
+                args.iter().map(|v| v.shift(delta, var)).collect(),
+            ),
+            Value::NaturalSuccClosure => Value::NaturalSuccClosure,
+            Value::OptionalSomeClosure(tth) => {
+                Value::OptionalSomeClosure(tth.shift(delta, var))
             }
-            Value::NaturalSuccClosure
-            | Value::Const(_)
-            | Value::BoolLit(_)
-            | Value::NaturalLit(_)
-            | Value::IntegerLit(_) => {}
-            Value::EmptyOptionalLit(tth)
-            | Value::OptionalSomeClosure(tth)
-            | Value::EmptyListLit(tth) => {
-                tth.shift(delta, var);
+            Value::ListConsClosure(t, v) => Value::ListConsClosure(
+                t.shift(delta, var),
+                v.as_ref().map(|v| v.shift(delta, var)),
+            ),
+            Value::Pi(x, t, e) => Value::Pi(
+                x.clone(),
+                t.shift(delta, var),
+                e.shift(delta, &var.shift0(1, x)),
+            ),
+            Value::Var(v) => Value::Var(v.shift(delta, var)),
+            Value::Const(c) => Value::Const(*c),
+            Value::BoolLit(b) => Value::BoolLit(*b),
+            Value::NaturalLit(n) => Value::NaturalLit(*n),
+            Value::IntegerLit(n) => Value::IntegerLit(*n),
+            Value::EmptyOptionalLit(tth) => {
+                Value::EmptyOptionalLit(tth.shift(delta, var))
             }
             Value::NEOptionalLit(th) => {
-                th.shift(delta, var);
-            }
-            Value::Lam(x, t, e) => {
-                t.shift(delta, var);
-                e.shift(delta, &var.shift0(1, x));
-            }
-            Value::AppliedBuiltin(_, args) => {
-                for x in args.iter_mut() {
-                    x.shift(delta, var);
-                }
-            }
-            Value::ListConsClosure(t, v) => {
-                t.shift(delta, var);
-                for x in v.iter_mut() {
-                    x.shift(delta, var);
-                }
-            }
-            Value::Pi(x, t, e) => {
-                t.shift(delta, var);
-                e.shift(delta, &var.shift0(1, x));
-            }
-            Value::NEListLit(elts) => {
-                for x in elts.iter_mut() {
-                    x.shift(delta, var);
-                }
-            }
-            Value::RecordLit(kvs) => {
-                for x in kvs.values_mut() {
-                    x.shift(delta, var);
-                }
-            }
-            Value::RecordType(kvs) => {
-                for x in kvs.values_mut() {
-                    x.shift(delta, var);
-                }
-            }
-            Value::UnionType(kts) | Value::UnionConstructor(_, kts) => {
-                for x in kts.values_mut().flat_map(|opt| opt) {
-                    x.shift(delta, var);
-                }
-            }
-            Value::UnionLit(_, v, kts) => {
-                v.shift(delta, var);
-                for x in kts.values_mut().flat_map(|opt| opt) {
-                    x.shift(delta, var);
-                }
+                Value::NEOptionalLit(th.shift(delta, var))
             }
-            Value::TextLit(elts) => {
-                for x in elts.iter_mut() {
-                    use InterpolatedTextContents::{Expr, Text};
-                    match x {
-                        Expr(n) => n.shift(delta, var),
-                        Text(_) => {}
-                    }
-                }
+            Value::EmptyListLit(tth) => {
+                Value::EmptyListLit(tth.shift(delta, var))
             }
-            Value::Expr(e) => shift_mut(delta, var, e),
+            Value::NEListLit(elts) => Value::NEListLit(
+                elts.iter().map(|v| v.shift(delta, var)).collect(),
+            ),
+            Value::RecordLit(kvs) => Value::RecordLit(
+                kvs.iter()
+                    .map(|(k, v)| (k.clone(), v.shift(delta, var)))
+                    .collect(),
+            ),
+            Value::RecordType(kvs) => Value::RecordType(
+                kvs.iter()
+                    .map(|(k, v)| (k.clone(), v.shift(delta, var)))
+                    .collect(),
+            ),
+            Value::UnionType(kts) => Value::UnionType(
+                kts.iter()
+                    .map(|(k, v)| {
+                        (k.clone(), v.as_ref().map(|v| v.shift(delta, var)))
+                    })
+                    .collect(),
+            ),
+            Value::UnionConstructor(x, kts) => Value::UnionConstructor(
+                x.clone(),
+                kts.iter()
+                    .map(|(k, v)| {
+                        (k.clone(), v.as_ref().map(|v| v.shift(delta, var)))
+                    })
+                    .collect(),
+            ),
+            Value::UnionLit(x, v, kts) => Value::UnionLit(
+                x.clone(),
+                v.shift(delta, var),
+                kts.iter()
+                    .map(|(k, v)| {
+                        (k.clone(), v.as_ref().map(|v| v.shift(delta, var)))
+                    })
+                    .collect(),
+            ),
+            Value::TextLit(elts) => Value::TextLit(
+                elts.iter()
+                    .map(|contents| {
+                        use InterpolatedTextContents::{Expr, Text};
+                        match contents {
+                            Expr(th) => Expr(th.shift(delta, var)),
+                            Text(s) => Text(s.clone()),
+                        }
+                    })
+                    .collect(),
+            ),
+            Value::Expr(e) => Value::Expr(e.shift(delta, var)),
         }
     }
 
@@ -859,10 +871,14 @@ impl Thunk<WHNF> {
         Thunk::Value(Box::new(self.normalize_whnf().normalize()))
     }
 
-    fn shift(&mut self, delta: isize, var: &V<Label>) {
+    fn shift(&self, delta: isize, var: &V<Label>) -> Self {
         match self {
-            Thunk::Value(v) => v.shift(delta, var),
-            Thunk::Unnormalized(_, _, e) => shift_mut(delta, var, e),
+            Thunk::Value(v) => Thunk::Value(Box::new(v.shift(delta, var))),
+            Thunk::Unnormalized(marker, ctx, e) => Thunk::Unnormalized(
+                marker.clone(),
+                ctx.shift(delta, var),
+                e.clone(),
+            ),
         }
     }
 
@@ -922,13 +938,10 @@ impl TypeThunk<WHNF> {
         }
     }
 
-    fn shift(&mut self, delta: isize, var: &V<Label>) {
+    fn shift(&self, delta: isize, var: &V<Label>) -> Self {
         match self {
-            TypeThunk::Thunk(th) => th.shift(delta, var),
-            TypeThunk::Type(t) => {
-                let shifted = t.shift(delta, var);
-                std::mem::replace(t, shifted);
-            }
+            TypeThunk::Thunk(th) => TypeThunk::Thunk(th.shift(delta, var)),
+            TypeThunk::Type(t) => TypeThunk::Type(t.shift(delta, var)),
         }
     }
 
-- 
cgit v1.2.3


From 69b65ee70a84b591c9a56861317253577e7c7628 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 29 Apr 2019 22:01:25 +0200
Subject: Make NF and WHNF custom types instead of aliases

---
 dhall/src/normalize.rs | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'dhall/src/normalize.rs')

diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 43e7292..d58ea7a 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -355,8 +355,10 @@ impl NormalizationContext {
     }
 }
 
-pub(crate) type WHNF = ();
-pub(crate) type NF = X;
+#[derive(Debug, Clone)]
+pub(crate) struct WHNF;
+#[derive(Debug, Clone)]
+pub(crate) enum NF {}
 
 /// A semantic value. `Form` should be either `WHNF` or `NF`.
 /// `NF` stands for Normal Form and indicates that all subexpressions are normalized.
@@ -851,7 +853,7 @@ pub(crate) enum Thunk<Form> {
 
 impl Thunk<WHNF> {
     fn new(ctx: NormalizationContext, e: InputSubExpr) -> Thunk<WHNF> {
-        Thunk::Unnormalized((), ctx, e)
+        Thunk::Unnormalized(WHNF, ctx, e)
     }
 
     fn from_whnf(v: Value<WHNF>) -> Thunk<WHNF> {
-- 
cgit v1.2.3


From 6bb8e618f66df4a955d800d49b3b6863aabd5b41 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 29 Apr 2019 23:28:16 +0200
Subject: Remove NF/WHNF distinction at runtime

---
 dhall/src/normalize.rs | 165 +++++++++++++++++++++----------------------------
 1 file changed, 72 insertions(+), 93 deletions(-)

(limited to 'dhall/src/normalize.rs')

diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index d58ea7a..3b21b86 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -70,12 +70,12 @@ impl<'a> PartiallyNormalized<'a> {
             self.2,
         )
     }
-    pub(crate) fn into_whnf(self) -> Value<WHNF> {
+    pub(crate) fn into_whnf(self) -> Value {
         self.0
     }
 }
 
-fn apply_builtin(b: Builtin, args: Vec<Value<WHNF>>) -> Value<WHNF> {
+fn apply_builtin(b: Builtin, args: Vec<Value>) -> Value {
     use dhall_core::Builtin::*;
     use Value::*;
 
@@ -264,7 +264,7 @@ fn apply_builtin(b: Builtin, args: Vec<Value<WHNF>>) -> Value<WHNF> {
 
 #[derive(Debug, Clone)]
 enum EnvItem {
-    Expr(Value<WHNF>),
+    Expr(Value),
     Skip(V<Label>),
 }
 
@@ -302,7 +302,7 @@ impl NormalizationContext {
     fn new() -> Self {
         NormalizationContext(Rc::new(Context::new()))
     }
-    fn insert(&self, x: &Label, e: Value<WHNF>) -> Self {
+    fn insert(&self, x: &Label, e: Value) -> Self {
         NormalizationContext(Rc::new(
             self.0.insert(x.clone(), EnvItem::Expr(e)),
         ))
@@ -314,7 +314,7 @@ impl NormalizationContext {
                 .insert(x.clone(), EnvItem::Skip(V(x.clone(), 0))),
         ))
     }
-    fn lookup(&self, var: &V<Label>) -> Value<WHNF> {
+    fn lookup(&self, var: &V<Label>) -> Value {
         let V(x, n) = var;
         match self.0.lookup(x, *n) {
             Some(EnvItem::Expr(e)) => e.clone(),
@@ -355,53 +355,41 @@ impl NormalizationContext {
     }
 }
 
+/// A semantic value.
 #[derive(Debug, Clone)]
-pub(crate) struct WHNF;
-#[derive(Debug, Clone)]
-pub(crate) enum NF {}
-
-/// A semantic value. `Form` should be either `WHNF` or `NF`.
-/// `NF` stands for Normal Form and indicates that all subexpressions are normalized.
-/// `WHNF` stands for Weak Head Normal-Form and indicates that subexpressions may not be normalized.
-///
-/// Weak Head Normal-Form 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 normal form for simple types like integers, but for e.g. a record literal
-/// this means knowing just the field names.
-#[derive(Debug, Clone)]
-pub(crate) enum Value<Form> {
+pub(crate) enum Value {
     /// Closures
-    Lam(Label, Thunk<Form>, Thunk<Form>),
-    AppliedBuiltin(Builtin, Vec<Value<Form>>),
+    Lam(Label, Thunk, Thunk),
+    AppliedBuiltin(Builtin, Vec<Value>),
     /// `λ(x: a) -> Some x`
-    OptionalSomeClosure(TypeThunk<Form>),
+    OptionalSomeClosure(TypeThunk),
     /// `λ(x : a) -> λ(xs : List a) -> [ x ] # xs`
     /// `λ(xs : List a) -> [ x ] # xs`
-    ListConsClosure(TypeThunk<Form>, Option<Thunk<Form>>),
+    ListConsClosure(TypeThunk, Option<Thunk>),
     /// `λ(x : Natural) -> x + 1`
     NaturalSuccClosure,
-    Pi(Label, TypeThunk<Form>, TypeThunk<Form>),
+    Pi(Label, TypeThunk, TypeThunk),
 
     Var(V<Label>),
     Const(Const),
     BoolLit(bool),
     NaturalLit(Natural),
     IntegerLit(Integer),
-    EmptyOptionalLit(TypeThunk<Form>),
-    NEOptionalLit(Thunk<Form>),
-    EmptyListLit(TypeThunk<Form>),
-    NEListLit(Vec<Thunk<Form>>),
-    RecordLit(BTreeMap<Label, Thunk<Form>>),
-    RecordType(BTreeMap<Label, TypeThunk<Form>>),
-    UnionType(BTreeMap<Label, Option<TypeThunk<Form>>>),
-    UnionConstructor(Label, BTreeMap<Label, Option<TypeThunk<Form>>>),
-    UnionLit(Label, Thunk<Form>, BTreeMap<Label, Option<TypeThunk<Form>>>),
-    TextLit(Vec<InterpolatedTextContents<Thunk<Form>>>),
+    EmptyOptionalLit(TypeThunk),
+    NEOptionalLit(Thunk),
+    EmptyListLit(TypeThunk),
+    NEListLit(Vec<Thunk>),
+    RecordLit(BTreeMap<Label, Thunk>),
+    RecordType(BTreeMap<Label, TypeThunk>),
+    UnionType(BTreeMap<Label, Option<TypeThunk>>),
+    UnionConstructor(Label, BTreeMap<Label, Option<TypeThunk>>),
+    UnionLit(Label, Thunk, BTreeMap<Label, Option<TypeThunk>>),
+    TextLit(Vec<InterpolatedTextContents<Thunk>>),
     /// This must not contain a value captured by one of the variants above.
     Expr(OutputSubExpr),
 }
 
-impl Value<NF> {
+impl Value {
     /// Convert the value back to a (normalized) syntactic expression
     pub(crate) fn normalize_to_expr(self) -> OutputSubExpr {
         match self {
@@ -493,7 +481,7 @@ impl Value<NF> {
             )),
             Value::TextLit(elts) => {
                 fn normalize_textlit(
-                    elts: Vec<InterpolatedTextContents<Thunk<NF>>>,
+                    elts: Vec<InterpolatedTextContents<Thunk>>,
                 ) -> InterpolatedText<OutputSubExpr> {
                     elts.into_iter()
                         .flat_map(|contents| {
@@ -523,14 +511,8 @@ impl Value<NF> {
             Value::Expr(e) => e,
         }
     }
-}
-
-impl Value<WHNF> {
-    pub(crate) fn normalize_to_expr(self) -> OutputSubExpr {
-        self.normalize().normalize_to_expr()
-    }
 
-    pub(crate) fn normalize(&self) -> Value<NF> {
+    pub(crate) fn normalize(&self) -> Value {
         match self {
             Value::Lam(x, t, e) => {
                 Value::Lam(x.clone(), t.normalize(), e.normalize())
@@ -613,7 +595,7 @@ impl Value<WHNF> {
     }
 
     /// Apply to a value
-    pub(crate) fn app(self, val: Value<WHNF>) -> Value<WHNF> {
+    pub(crate) fn app(self, val: Value) -> Value {
         match (self, val) {
             (Value::Lam(x, _, e), val) => {
                 let val =
@@ -651,7 +633,7 @@ impl Value<WHNF> {
         }
     }
 
-    pub(crate) fn from_builtin(b: Builtin) -> Value<WHNF> {
+    pub(crate) fn from_builtin(b: Builtin) -> Value {
         Value::AppliedBuiltin(b, vec![])
     }
 
@@ -846,41 +828,44 @@ impl Value<WHNF> {
 /// Contains either a (partially) normalized value or a
 /// non-normalized value alongside a normalization context.
 #[derive(Debug, Clone)]
-pub(crate) enum Thunk<Form> {
-    Value(Box<Value<Form>>),
-    Unnormalized(Form, NormalizationContext, InputSubExpr),
+pub(crate) enum Thunk {
+    // Normal form, i.e. completely normalized
+    NF(Box<Value>),
+    // Weak Head Normal Form, i.e. subexpressions may not be normalized
+    WHNF(Box<Value>),
+    Unnormalized(NormalizationContext, InputSubExpr),
 }
 
-impl Thunk<WHNF> {
-    fn new(ctx: NormalizationContext, e: InputSubExpr) -> Thunk<WHNF> {
-        Thunk::Unnormalized(WHNF, ctx, e)
+impl Thunk {
+    fn new(ctx: NormalizationContext, e: InputSubExpr) -> Thunk {
+        Thunk::Unnormalized(ctx, e)
     }
 
-    fn from_whnf(v: Value<WHNF>) -> Thunk<WHNF> {
-        Thunk::Value(Box::new(v))
+    fn from_whnf(v: Value) -> Thunk {
+        Thunk::WHNF(Box::new(v))
     }
 
-    pub(crate) fn normalize_whnf(&self) -> Value<WHNF> {
+    pub(crate) fn normalize_whnf(&self) -> Value {
         match self {
-            Thunk::Value(v) => (**v).clone(),
-            Thunk::Unnormalized(_, ctx, e) => {
+            Thunk::WHNF(v) => (**v).clone(),
+            Thunk::NF(v) => (**v).clone(),
+            Thunk::Unnormalized(ctx, e) => {
                 normalize_whnf(ctx.clone(), e.clone())
             }
         }
     }
 
-    fn normalize(&self) -> Thunk<NF> {
-        Thunk::Value(Box::new(self.normalize_whnf().normalize()))
+    fn normalize(&self) -> Thunk {
+        Thunk::NF(Box::new(self.normalize_whnf().normalize()))
     }
 
     fn shift(&self, delta: isize, var: &V<Label>) -> Self {
         match self {
-            Thunk::Value(v) => Thunk::Value(Box::new(v.shift(delta, var))),
-            Thunk::Unnormalized(marker, ctx, e) => Thunk::Unnormalized(
-                marker.clone(),
-                ctx.shift(delta, var),
-                e.clone(),
-            ),
+            Thunk::WHNF(v) => Thunk::WHNF(Box::new(v.shift(delta, var))),
+            Thunk::NF(v) => Thunk::NF(Box::new(v.shift(delta, var))),
+            Thunk::Unnormalized(ctx, e) => {
+                Thunk::Unnormalized(ctx.shift(delta, var), e.clone())
+            }
         }
     }
 
@@ -890,50 +875,49 @@ impl Thunk<WHNF> {
         val: &PartiallyNormalized<'static>,
     ) -> Self {
         match self {
-            Thunk::Value(v) => Thunk::Value(Box::new(v.subst_shift(var, val))),
-            Thunk::Unnormalized(marker, ctx, e) => Thunk::Unnormalized(
-                marker.clone(),
-                ctx.subst_shift(var, val),
-                e.clone(),
-            ),
+            Thunk::WHNF(v) => Thunk::WHNF(Box::new(v.subst_shift(var, val))),
+            Thunk::NF(v) => Thunk::NF(Box::new(v.subst_shift(var, val))),
+            Thunk::Unnormalized(ctx, e) => {
+                Thunk::Unnormalized(ctx.subst_shift(var, val), e.clone())
+            }
         }
     }
-}
 
-impl Thunk<NF> {
-    pub(crate) fn to_nf(&self) -> Value<NF> {
+    pub(crate) fn to_nf(&self) -> Value {
         match self {
-            Thunk::Value(v) => (**v).clone(),
-            Thunk::Unnormalized(m, _, _) => match *m {},
+            Thunk::NF(v) => (**v).clone(),
+            Thunk::WHNF(_) | Thunk::Unnormalized(_, _) => {
+                self.normalize_whnf().normalize()
+            }
         }
     }
 }
 
 /// A thunk in type position.
 #[derive(Debug, Clone)]
-pub(crate) enum TypeThunk<Form> {
-    Thunk(Thunk<Form>),
+pub(crate) enum TypeThunk {
+    Thunk(Thunk),
     Type(Type<'static>),
 }
 
-impl TypeThunk<WHNF> {
-    fn new(ctx: NormalizationContext, e: InputSubExpr) -> TypeThunk<WHNF> {
+impl TypeThunk {
+    fn new(ctx: NormalizationContext, e: InputSubExpr) -> TypeThunk {
         TypeThunk::from_thunk(Thunk::new(ctx, e))
     }
 
-    fn from_whnf(v: Value<WHNF>) -> TypeThunk<WHNF> {
+    fn from_whnf(v: Value) -> TypeThunk {
         TypeThunk::from_thunk(Thunk::from_whnf(v))
     }
 
-    fn from_thunk(th: Thunk<WHNF>) -> TypeThunk<WHNF> {
+    fn from_thunk(th: Thunk) -> TypeThunk {
         TypeThunk::Thunk(th)
     }
 
-    pub(crate) fn from_type(t: Type<'static>) -> TypeThunk<WHNF> {
+    pub(crate) fn from_type(t: Type<'static>) -> TypeThunk {
         TypeThunk::Type(t)
     }
 
-    fn normalize(&self) -> TypeThunk<NF> {
+    fn normalize(&self) -> TypeThunk {
         match self {
             TypeThunk::Thunk(th) => TypeThunk::Thunk(th.normalize()),
             TypeThunk::Type(t) => TypeThunk::Type(t.clone()),
@@ -957,10 +941,8 @@ impl TypeThunk<WHNF> {
             TypeThunk::Type(t) => TypeThunk::Type(t.subst_shift(var, val)),
         }
     }
-}
 
-impl TypeThunk<NF> {
-    pub(crate) fn to_nf(&self) -> Value<NF> {
+    pub(crate) fn to_nf(&self) -> Value {
         match self {
             TypeThunk::Thunk(th) => th.to_nf(),
             // TODO: let's hope for the best with the unwrap
@@ -975,10 +957,7 @@ impl TypeThunk<NF> {
 }
 
 /// Reduces the imput expression to Value. See doc on `Value` for details.
-fn normalize_whnf(
-    ctx: NormalizationContext,
-    expr: InputSubExpr,
-) -> Value<WHNF> {
+fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> Value {
     match expr.as_ref() {
         ExprF::Var(v) => ctx.lookup(&v),
         ExprF::Annot(x, _) => normalize_whnf(ctx, x.clone()),
@@ -1074,7 +1053,7 @@ fn normalize_whnf(
         }
         expr => {
             // Recursively normalize subexpressions
-            let expr: ExprF<Value<WHNF>, Label, X, X> = expr
+            let expr: ExprF<Value, Label, X, X> = expr
                 .map_ref_with_special_handling_of_binders(
                     |e| normalize_whnf(ctx.clone(), e.clone()),
                     |x, e| normalize_whnf(ctx.skip(x), e.clone()),
@@ -1089,7 +1068,7 @@ fn normalize_whnf(
 }
 
 /// When all sub-expressions have been (partially) normalized, eval the remaining toplevel layer.
-fn normalize_last_layer(expr: ExprF<Value<WHNF>, Label, X, X>) -> Value<WHNF> {
+fn normalize_last_layer(expr: ExprF<Value, Label, X, X>) -> Value {
     use dhall_core::BinOp::*;
     use Value::*;
 
@@ -1173,7 +1152,7 @@ fn normalize_last_layer(expr: ExprF<Value<WHNF>, Label, X, X>) -> Value<WHNF> {
             Expr(rc(ExprF::Merge(
                 RecordLit(handlers).normalize_to_expr(),
                 e.normalize_to_expr(),
-                t.map(<Value<WHNF>>::normalize_to_expr),
+                t.map(<Value>::normalize_to_expr),
             )))
         }
         // Couldn't do anything useful, so just normalize subexpressions
-- 
cgit v1.2.3


From 8e8a446e1b2ca85633f0368aefc5f8e31196c7c8 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 30 Apr 2019 01:50:49 +0200
Subject: Store thunks behind Rc<RefCell<_>> to ensure minimal computation

---
 dhall/src/normalize.rs | 236 +++++++++++++++++++++++++++++++++----------------
 1 file changed, 159 insertions(+), 77 deletions(-)

(limited to 'dhall/src/normalize.rs')

diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 3b21b86..461ce99 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -181,7 +181,7 @@ fn apply_builtin(b: Builtin, args: Vec<Value>) -> Value {
             [_, NEListLit(xs), _, cons, nil] => {
                 let mut v = nil;
                 for x in xs.into_iter().rev() {
-                    v = cons.clone().app(x.normalize_whnf()).app(v);
+                    v = cons.clone().app(x.as_whnf()).app(v);
                 }
                 v
             }
@@ -215,7 +215,7 @@ fn apply_builtin(b: Builtin, args: Vec<Value>) -> Value {
                 nothing
             },
             [_, NEOptionalLit(x), _, just, _] => {
-                just.app(x.normalize_whnf())
+                just.app(x.as_whnf())
             }
         ),
         NaturalBuild => improved_slice_patterns::match_vec!(args;
@@ -395,8 +395,8 @@ impl Value {
         match self {
             Value::Lam(x, t, e) => rc(ExprF::Lam(
                 x.clone(),
-                t.to_nf().normalize_to_expr(),
-                e.to_nf().normalize_to_expr(),
+                t.as_nf().normalize_to_expr(),
+                e.as_nf().normalize_to_expr(),
             )),
             Value::AppliedBuiltin(b, args) => {
                 let mut e = rc(ExprF::Builtin(b));
@@ -406,18 +406,18 @@ impl Value {
                 e
             }
             Value::OptionalSomeClosure(n) => {
-                let a = n.to_nf().normalize_to_expr();
+                let a = n.as_nf().normalize_to_expr();
                 dhall::subexpr!(λ(x: a) -> Some x)
             }
             Value::ListConsClosure(n, None) => {
-                let a = n.to_nf().normalize_to_expr();
+                let a = n.as_nf().normalize_to_expr();
                 // Avoid accidental capture of the new `x` variable
                 let a1 = a.shift0(1, &"x".into());
                 dhall::subexpr!(λ(x : a) -> λ(xs : List a1) -> [ x ] # xs)
             }
             Value::ListConsClosure(n, Some(v)) => {
-                let v = v.to_nf().normalize_to_expr();
-                let a = n.to_nf().normalize_to_expr();
+                let v = v.as_nf().normalize_to_expr();
+                let a = n.as_nf().normalize_to_expr();
                 // Avoid accidental capture of the new `xs` variable
                 let v = v.shift0(1, &"xs".into());
                 dhall::subexpr!(λ(xs : List a) -> [ v ] # xs)
@@ -427,8 +427,8 @@ impl Value {
             }
             Value::Pi(x, t, e) => rc(ExprF::Pi(
                 x,
-                t.to_nf().normalize_to_expr(),
-                e.to_nf().normalize_to_expr(),
+                t.as_nf().normalize_to_expr(),
+                e.as_nf().normalize_to_expr(),
             )),
             Value::Var(v) => rc(ExprF::Var(v)),
             Value::Const(c) => rc(ExprF::Const(c)),
@@ -437,46 +437,46 @@ impl Value {
             Value::IntegerLit(n) => rc(ExprF::IntegerLit(n)),
             Value::EmptyOptionalLit(n) => rc(ExprF::App(
                 rc(ExprF::Builtin(Builtin::OptionalNone)),
-                n.to_nf().normalize_to_expr(),
+                n.as_nf().normalize_to_expr(),
             )),
             Value::NEOptionalLit(n) => {
-                rc(ExprF::SomeLit(n.to_nf().normalize_to_expr()))
+                rc(ExprF::SomeLit(n.as_nf().normalize_to_expr()))
             }
             Value::EmptyListLit(n) => {
-                rc(ExprF::EmptyListLit(n.to_nf().normalize_to_expr()))
+                rc(ExprF::EmptyListLit(n.as_nf().normalize_to_expr()))
             }
             Value::NEListLit(elts) => rc(ExprF::NEListLit(
                 elts.into_iter()
-                    .map(|n| n.to_nf().normalize_to_expr())
+                    .map(|n| n.as_nf().normalize_to_expr())
                     .collect(),
             )),
             Value::RecordLit(kvs) => rc(ExprF::RecordLit(
                 kvs.into_iter()
-                    .map(|(k, v)| (k, v.to_nf().normalize_to_expr()))
+                    .map(|(k, v)| (k, v.as_nf().normalize_to_expr()))
                     .collect(),
             )),
             Value::RecordType(kts) => rc(ExprF::RecordType(
                 kts.into_iter()
-                    .map(|(k, v)| (k, v.to_nf().normalize_to_expr()))
+                    .map(|(k, v)| (k, v.as_nf().normalize_to_expr()))
                     .collect(),
             )),
             Value::UnionType(kts) => rc(ExprF::UnionType(
                 kts.into_iter()
-                    .map(|(k, v)| (k, v.map(|v| v.to_nf().normalize_to_expr())))
+                    .map(|(k, v)| (k, v.map(|v| v.as_nf().normalize_to_expr())))
                     .collect(),
             )),
             Value::UnionConstructor(l, kts) => {
                 let kts = kts
                     .into_iter()
-                    .map(|(k, v)| (k, v.map(|v| v.to_nf().normalize_to_expr())))
+                    .map(|(k, v)| (k, v.map(|v| v.as_nf().normalize_to_expr())))
                     .collect();
                 rc(ExprF::Field(rc(ExprF::UnionType(kts)), l))
             }
             Value::UnionLit(l, v, kts) => rc(ExprF::UnionLit(
                 l,
-                v.to_nf().normalize_to_expr(),
+                v.as_nf().normalize_to_expr(),
                 kts.into_iter()
-                    .map(|(k, v)| (k, v.map(|v| v.to_nf().normalize_to_expr())))
+                    .map(|(k, v)| (k, v.map(|v| v.as_nf().normalize_to_expr())))
                     .collect(),
             )),
             Value::TextLit(elts) => {
@@ -487,7 +487,7 @@ impl Value {
                         .flat_map(|contents| {
                             use InterpolatedTextContents::{Expr, Text};
                             let new_interpolated = match contents {
-                                Expr(n) => match n.to_nf() {
+                                Expr(n) => match n.as_nf() {
                                     Value::TextLit(elts2) => {
                                         normalize_textlit(elts2)
                                     }
@@ -600,7 +600,7 @@ impl Value {
             (Value::Lam(x, _, e), val) => {
                 let val =
                     PartiallyNormalized(val, None, std::marker::PhantomData);
-                e.subst_shift(&V(x, 0), &val).normalize_whnf()
+                e.subst_shift(&V(x, 0), &val).as_whnf()
             }
             (Value::AppliedBuiltin(b, mut args), val) => {
                 args.push(val);
@@ -825,74 +825,156 @@ impl Value {
     }
 }
 
-/// Contains either a (partially) normalized value or a
-/// non-normalized value alongside a normalization context.
-#[derive(Debug, Clone)]
-pub(crate) enum Thunk {
-    // Normal form, i.e. completely normalized
-    NF(Box<Value>),
-    // Weak Head Normal Form, i.e. subexpressions may not be normalized
-    WHNF(Box<Value>),
-    Unnormalized(NormalizationContext, InputSubExpr),
-}
+mod thunk {
+    use super::{normalize_whnf, InputSubExpr, NormalizationContext, Value};
+    use crate::expr::PartiallyNormalized;
+    use dhall_core::{Label, V};
+    use std::cell::RefCell;
+    use std::rc::Rc;
 
-impl Thunk {
-    fn new(ctx: NormalizationContext, e: InputSubExpr) -> Thunk {
-        Thunk::Unnormalized(ctx, e)
+    #[derive(Debug)]
+    enum ThunkInternal {
+        /// Non-normalized value alongside a normalization context
+        Unnormalized(NormalizationContext, InputSubExpr),
+        /// Weak Head Normal Form, i.e. subexpressions may not be normalized
+        WHNF(Box<Value>),
+        /// Normal form, i.e. completely normalized
+        NF(Box<Value>),
     }
 
-    fn from_whnf(v: Value) -> Thunk {
-        Thunk::WHNF(Box::new(v))
-    }
+    /// Stores a possibl unevaluated value. Uses RefCell to ensure that
+    /// the value gets normalized at most once.
+    #[derive(Debug, Clone)]
+    pub struct Thunk(Rc<RefCell<ThunkInternal>>);
 
-    pub(crate) fn normalize_whnf(&self) -> Value {
-        match self {
-            Thunk::WHNF(v) => (**v).clone(),
-            Thunk::NF(v) => (**v).clone(),
-            Thunk::Unnormalized(ctx, e) => {
-                normalize_whnf(ctx.clone(), e.clone())
+    impl ThunkInternal {
+        fn into_thunk(self) -> Thunk {
+            Thunk(Rc::new(RefCell::new(self)))
+        }
+
+        fn normalize_whnf(&mut self) {
+            match self {
+                ThunkInternal::Unnormalized(ctx, e) => {
+                    let new = ThunkInternal::WHNF(Box::new(normalize_whnf(
+                        ctx.clone(),
+                        e.clone(),
+                    )));
+                    std::mem::replace(self, new);
+                }
+                ThunkInternal::WHNF(_) => {}
+                ThunkInternal::NF(_) => {}
             }
         }
-    }
 
-    fn normalize(&self) -> Thunk {
-        Thunk::NF(Box::new(self.normalize_whnf().normalize()))
-    }
+        fn normalize_nf(&mut self) {
+            self.normalize_whnf();
+            match self {
+                ThunkInternal::Unnormalized(_, _) => unreachable!(),
+                ThunkInternal::WHNF(v) => {
+                    let new = ThunkInternal::NF(Box::new(v.normalize()));
+                    std::mem::replace(self, new);
+                }
+                ThunkInternal::NF(_) => {}
+            }
+        }
 
-    fn shift(&self, delta: isize, var: &V<Label>) -> Self {
-        match self {
-            Thunk::WHNF(v) => Thunk::WHNF(Box::new(v.shift(delta, var))),
-            Thunk::NF(v) => Thunk::NF(Box::new(v.shift(delta, var))),
-            Thunk::Unnormalized(ctx, e) => {
-                Thunk::Unnormalized(ctx.shift(delta, var), e.clone())
+        // Always use normalize_whnf before
+        fn as_whnf(&self) -> Value {
+            match self {
+                ThunkInternal::Unnormalized(_, _) => unreachable!(),
+                ThunkInternal::WHNF(v) => v.as_ref().clone(),
+                ThunkInternal::NF(v) => v.as_ref().clone(),
             }
         }
-    }
 
-    pub(crate) fn subst_shift(
-        &self,
-        var: &V<Label>,
-        val: &PartiallyNormalized<'static>,
-    ) -> Self {
-        match self {
-            Thunk::WHNF(v) => Thunk::WHNF(Box::new(v.subst_shift(var, val))),
-            Thunk::NF(v) => Thunk::NF(Box::new(v.subst_shift(var, val))),
-            Thunk::Unnormalized(ctx, e) => {
-                Thunk::Unnormalized(ctx.subst_shift(var, val), e.clone())
+        // Always use normalize_nf before
+        fn as_nf(&self) -> Value {
+            match self {
+                ThunkInternal::Unnormalized(_, _) => unreachable!(),
+                ThunkInternal::WHNF(_) => unreachable!(),
+                ThunkInternal::NF(v) => v.as_ref().clone(),
             }
         }
-    }
 
-    pub(crate) fn to_nf(&self) -> Value {
-        match self {
-            Thunk::NF(v) => (**v).clone(),
-            Thunk::WHNF(_) | Thunk::Unnormalized(_, _) => {
-                self.normalize_whnf().normalize()
+        fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+            match self {
+                ThunkInternal::Unnormalized(ctx, e) => {
+                    ThunkInternal::Unnormalized(
+                        ctx.shift(delta, var),
+                        e.clone(),
+                    )
+                }
+                ThunkInternal::WHNF(v) => {
+                    ThunkInternal::WHNF(Box::new(v.shift(delta, var)))
+                }
+                ThunkInternal::NF(v) => {
+                    ThunkInternal::NF(Box::new(v.shift(delta, var)))
+                }
+            }
+        }
+
+        fn subst_shift(
+            &self,
+            var: &V<Label>,
+            val: &PartiallyNormalized<'static>,
+        ) -> Self {
+            match self {
+                ThunkInternal::Unnormalized(ctx, e) => {
+                    ThunkInternal::Unnormalized(
+                        ctx.subst_shift(var, val),
+                        e.clone(),
+                    )
+                }
+                ThunkInternal::WHNF(v) => {
+                    ThunkInternal::WHNF(Box::new(v.subst_shift(var, val)))
+                }
+                ThunkInternal::NF(v) => {
+                    ThunkInternal::NF(Box::new(v.subst_shift(var, val)))
+                }
             }
         }
     }
+
+    impl Thunk {
+        pub(crate) fn new(ctx: NormalizationContext, e: InputSubExpr) -> Thunk {
+            ThunkInternal::Unnormalized(ctx, e).into_thunk()
+        }
+
+        pub(crate) fn from_whnf(v: Value) -> Thunk {
+            ThunkInternal::WHNF(Box::new(v)).into_thunk()
+        }
+
+        pub(crate) fn normalize(&self) -> Thunk {
+            self.0.borrow_mut().normalize_nf();
+            self.clone()
+        }
+
+        pub(crate) fn as_whnf(&self) -> Value {
+            self.0.borrow_mut().normalize_whnf();
+            self.0.borrow().as_whnf()
+        }
+
+        pub(crate) fn as_nf(&self) -> Value {
+            self.0.borrow_mut().normalize_nf();
+            self.0.borrow().as_nf()
+        }
+
+        pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+            self.0.borrow().shift(delta, var).into_thunk()
+        }
+
+        pub(crate) fn subst_shift(
+            &self,
+            var: &V<Label>,
+            val: &PartiallyNormalized<'static>,
+        ) -> Self {
+            self.0.borrow().subst_shift(var, val).into_thunk()
+        }
+    }
 }
 
+pub(crate) use thunk::Thunk;
+
 /// A thunk in type position.
 #[derive(Debug, Clone)]
 pub(crate) enum TypeThunk {
@@ -942,9 +1024,9 @@ impl TypeThunk {
         }
     }
 
-    pub(crate) fn to_nf(&self) -> Value {
+    pub(crate) fn as_nf(&self) -> Value {
         match self {
-            TypeThunk::Thunk(th) => th.to_nf(),
+            TypeThunk::Thunk(th) => th.as_nf(),
             // TODO: let's hope for the best with the unwrap
             TypeThunk::Type(t) => t
                 .clone()
@@ -1118,7 +1200,7 @@ fn normalize_last_layer(expr: ExprF<Value, Label, X, X>) -> Value {
 
         ExprF::Field(UnionType(kts), l) => UnionConstructor(l, kts),
         ExprF::Field(RecordLit(mut kvs), l) => match kvs.remove(&l) {
-            Some(r) => r.normalize_whnf(),
+            Some(r) => r.as_whnf(),
             None => {
                 // Couldn't do anything useful, so just normalize subexpressions
                 Expr(rc(ExprF::Field(RecordLit(kvs).normalize_to_expr(), l)))
@@ -1135,13 +1217,13 @@ fn normalize_last_layer(expr: ExprF<Value, Label, X, X>) -> Value {
         ExprF::Merge(RecordLit(mut handlers), e, t) => {
             let e = match e {
                 UnionConstructor(l, kts) => match handlers.remove(&l) {
-                    Some(h) => return h.normalize_whnf(),
+                    Some(h) => return h.as_whnf(),
                     None => UnionConstructor(l, kts),
                 },
                 UnionLit(l, v, kts) => match handlers.remove(&l) {
                     Some(h) => {
-                        let h = h.normalize_whnf();
-                        let v = v.normalize_whnf();
+                        let h = h.as_whnf();
+                        let v = v.as_whnf();
                         return h.app(v);
                     }
                     None => UnionLit(l, v, kts),
-- 
cgit v1.2.3


From 65a242abfa4d881dc17f216b3eeeb8aedc663388 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 30 Apr 2019 13:12:49 +0200
Subject: Store thunks in the normalization context

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

(limited to 'dhall/src/normalize.rs')

diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 461ce99..f2ad8ea 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -264,7 +264,7 @@ fn apply_builtin(b: Builtin, args: Vec<Value>) -> Value {
 
 #[derive(Debug, Clone)]
 enum EnvItem {
-    Expr(Value),
+    Thunk(Thunk),
     Skip(V<Label>),
 }
 
@@ -276,7 +276,7 @@ impl EnvItem {
     fn shift(&self, delta: isize, var: &V<Label>) -> Self {
         use EnvItem::*;
         match self {
-            Expr(e) => Expr(e.shift(delta, var)),
+            Thunk(e) => Thunk(e.shift(delta, var)),
             Skip(v) => Skip(v.shift(delta, var)),
         }
     }
@@ -286,11 +286,12 @@ impl EnvItem {
         var: &V<Label>,
         val: &PartiallyNormalized<'static>,
     ) -> Self {
-        use EnvItem::*;
         match self {
-            Expr(e) => Expr(e.subst_shift(var, val)),
-            Skip(v) if v == var => Expr(val.clone().into_whnf()),
-            Skip(v) => Skip(v.shift(-1, var)),
+            EnvItem::Thunk(e) => EnvItem::Thunk(e.subst_shift(var, val)),
+            EnvItem::Skip(v) if v == var => {
+                EnvItem::Thunk(Thunk::from_whnf(val.clone().into_whnf()))
+            }
+            EnvItem::Skip(v) => EnvItem::Skip(v.shift(-1, var)),
         }
     }
 }
@@ -302,9 +303,9 @@ impl NormalizationContext {
     fn new() -> Self {
         NormalizationContext(Rc::new(Context::new()))
     }
-    fn insert(&self, x: &Label, e: Value) -> Self {
+    fn insert(&self, x: &Label, e: Thunk) -> Self {
         NormalizationContext(Rc::new(
-            self.0.insert(x.clone(), EnvItem::Expr(e)),
+            self.0.insert(x.clone(), EnvItem::Thunk(e)),
         ))
     }
     fn skip(&self, x: &Label) -> Self {
@@ -317,7 +318,7 @@ impl NormalizationContext {
     fn lookup(&self, var: &V<Label>) -> Value {
         let V(x, n) = var;
         match self.0.lookup(x, *n) {
-            Some(EnvItem::Expr(e)) => e.clone(),
+            Some(EnvItem::Thunk(t)) => t.as_whnf(),
             Some(EnvItem::Skip(newvar)) => Value::Var(newvar.clone()),
             None => Value::Var(var.clone()),
         }
@@ -329,7 +330,7 @@ impl NormalizationContext {
             for v in vs.iter() {
                 let new_item = match v {
                     Type(var, _) => EnvItem::Skip(var.clone()),
-                    Value(e) => EnvItem::Expr(normalize_whnf(
+                    Value(e) => EnvItem::Thunk(Thunk::new(
                         NormalizationContext::new(),
                         e.as_expr().embed_absurd(),
                     )),
@@ -1049,8 +1050,8 @@ fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> Value {
             normalize_whnf(NormalizationContext::new(), e.0.embed_absurd())
         }
         ExprF::Let(x, _, r, b) => {
-            let r = normalize_whnf(ctx.clone(), r.clone());
-            normalize_whnf(ctx.insert(x, r), b.clone())
+            let t = Thunk::new(ctx.clone(), r.clone());
+            normalize_whnf(ctx.insert(x, t), b.clone())
         }
         ExprF::Lam(x, t, e) => Value::Lam(
             x.clone(),
-- 
cgit v1.2.3


From e2626a0bfd4b145e7d54c2150457f57e798ba2f7 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 30 Apr 2019 14:45:25 +0200
Subject: Store a Thunk in Typed

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

(limited to 'dhall/src/normalize.rs')

diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index f2ad8ea..5151790 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -28,23 +28,7 @@ impl<'a> Typed<'a> {
         self.partially_normalize().normalize()
     }
     pub(crate) fn partially_normalize(self) -> PartiallyNormalized<'a> {
-        PartiallyNormalized(
-            normalize_whnf(
-                NormalizationContext::from_typecheck_ctx(&self.2),
-                self.0,
-            ),
-            self.1,
-            self.3,
-        )
-    }
-    /// Pretends this expression is normalized. Use with care.
-    #[allow(dead_code)]
-    pub fn skip_normalize(self) -> Normalized<'a> {
-        Normalized(
-            self.0.unroll().squash_embed(|e| e.0.clone()),
-            self.1,
-            self.3,
-        )
+        PartiallyNormalized(self.0.as_whnf(), self.1, self.2)
     }
 }
 
@@ -300,7 +284,7 @@ impl EnvItem {
 pub(crate) struct NormalizationContext(Rc<Context<Label, EnvItem>>);
 
 impl NormalizationContext {
-    fn new() -> Self {
+    pub(crate) fn new() -> Self {
         NormalizationContext(Rc::new(Context::new()))
     }
     fn insert(&self, x: &Label, e: Thunk) -> Self {
@@ -323,7 +307,9 @@ impl NormalizationContext {
             None => Value::Var(var.clone()),
         }
     }
-    fn from_typecheck_ctx(tc_ctx: &crate::typecheck::TypecheckContext) -> Self {
+    pub(crate) fn from_typecheck_ctx(
+        tc_ctx: &crate::typecheck::TypecheckContext,
+    ) -> Self {
         use crate::typecheck::EnvItem::*;
         let mut ctx = Context::new();
         for (k, vs) in tc_ctx.0.iter_keys() {
-- 
cgit v1.2.3


From 77198a2833297289770867acdaf31db0e2011ea9 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 30 Apr 2019 15:35:13 +0200
Subject: Merge Typed and PartiallyNormalized

---
 dhall/src/normalize.rs | 74 ++++++++++++++++++++++----------------------------
 1 file changed, 32 insertions(+), 42 deletions(-)

(limited to 'dhall/src/normalize.rs')

diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 5151790..f15eea4 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -9,7 +9,7 @@ use dhall_core::{
 };
 use dhall_generator as dhall;
 
-use crate::expr::{Normalized, PartiallyNormalized, Type, Typed};
+use crate::expr::{Normalized, Type, Typed};
 
 type InputSubExpr = SubExpr<X, Normalized<'static>>;
 type OutputSubExpr = SubExpr<X, X>;
@@ -25,37 +25,35 @@ impl<'a> Typed<'a> {
     /// leave ill-typed sub-expressions unevaluated.
     ///
     pub fn normalize(self) -> Normalized<'a> {
-        self.partially_normalize().normalize()
+        Normalized(self.0.as_whnf().normalize_to_expr(), self.1, self.2)
     }
-    pub(crate) fn partially_normalize(self) -> PartiallyNormalized<'a> {
-        PartiallyNormalized(self.0.as_whnf(), self.1, self.2)
-    }
-}
 
-impl<'a> PartiallyNormalized<'a> {
-    pub(crate) fn normalize(self) -> Normalized<'a> {
-        Normalized(self.0.normalize_to_expr(), self.1, self.2)
-    }
     pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
-        PartiallyNormalized(
+        Typed(
             self.0.shift(delta, var),
             self.1.as_ref().map(|x| x.shift(delta, var)),
             self.2,
         )
     }
+
     pub(crate) fn subst_shift(
         &self,
         var: &V<Label>,
-        val: &PartiallyNormalized<'static>,
+        val: &Typed<'static>,
     ) -> Self {
-        PartiallyNormalized(
+        Typed(
             self.0.subst_shift(var, val),
             self.1.as_ref().map(|x| x.subst_shift(var, val)),
             self.2,
         )
     }
-    pub(crate) fn into_whnf(self) -> Value {
-        self.0
+
+    pub(crate) fn normalize_whnf(&self) -> Value {
+        self.0.as_whnf()
+    }
+
+    pub(crate) fn as_thunk(&self) -> Thunk {
+        self.0.clone()
     }
 }
 
@@ -268,13 +266,11 @@ impl EnvItem {
     pub(crate) fn subst_shift(
         &self,
         var: &V<Label>,
-        val: &PartiallyNormalized<'static>,
+        val: &Typed<'static>,
     ) -> Self {
         match self {
             EnvItem::Thunk(e) => EnvItem::Thunk(e.subst_shift(var, val)),
-            EnvItem::Skip(v) if v == var => {
-                EnvItem::Thunk(Thunk::from_whnf(val.clone().into_whnf()))
-            }
+            EnvItem::Skip(v) if v == var => EnvItem::Thunk(val.as_thunk()),
             EnvItem::Skip(v) => EnvItem::Skip(v.shift(-1, var)),
         }
     }
@@ -331,11 +327,7 @@ impl NormalizationContext {
         NormalizationContext(Rc::new(self.0.map(|_, e| e.shift(delta, var))))
     }
 
-    fn subst_shift(
-        &self,
-        var: &V<Label>,
-        val: &PartiallyNormalized<'static>,
-    ) -> Self {
+    fn subst_shift(&self, var: &V<Label>, val: &Typed<'static>) -> Self {
         NormalizationContext(Rc::new(
             self.0.map(|_, e| e.subst_shift(var, val)),
         ))
@@ -377,6 +369,10 @@ pub(crate) enum Value {
 }
 
 impl Value {
+    pub(crate) fn into_thunk(self) -> Thunk {
+        Thunk::from_whnf(self)
+    }
+
     /// Convert the value back to a (normalized) syntactic expression
     pub(crate) fn normalize_to_expr(self) -> OutputSubExpr {
         match self {
@@ -585,8 +581,11 @@ impl Value {
     pub(crate) fn app(self, val: Value) -> Value {
         match (self, val) {
             (Value::Lam(x, _, e), val) => {
-                let val =
-                    PartiallyNormalized(val, None, std::marker::PhantomData);
+                let val = Typed(
+                    Thunk::from_whnf(val),
+                    None,
+                    std::marker::PhantomData,
+                );
                 e.subst_shift(&V(x, 0), &val).as_whnf()
             }
             (Value::AppliedBuiltin(b, mut args), val) => {
@@ -717,7 +716,7 @@ impl Value {
     pub(crate) fn subst_shift(
         &self,
         var: &V<Label>,
-        val: &PartiallyNormalized<'static>,
+        val: &Typed<'static>,
     ) -> Self {
         match self {
             Value::Lam(x, t, e) => Value::Lam(
@@ -742,7 +741,7 @@ impl Value {
                 t.subst_shift(var, val),
                 e.subst_shift(&var.shift0(1, x), val),
             ),
-            Value::Var(v) if v == var => val.clone().into_whnf(),
+            Value::Var(v) if v == var => val.normalize_whnf(),
             Value::Var(v) => Value::Var(v.shift(-1, var)),
             Value::Const(c) => Value::Const(*c),
             Value::BoolLit(b) => Value::BoolLit(*b),
@@ -814,7 +813,7 @@ impl Value {
 
 mod thunk {
     use super::{normalize_whnf, InputSubExpr, NormalizationContext, Value};
-    use crate::expr::PartiallyNormalized;
+    use crate::expr::Typed;
     use dhall_core::{Label, V};
     use std::cell::RefCell;
     use std::rc::Rc;
@@ -900,11 +899,7 @@ mod thunk {
             }
         }
 
-        fn subst_shift(
-            &self,
-            var: &V<Label>,
-            val: &PartiallyNormalized<'static>,
-        ) -> Self {
+        fn subst_shift(&self, var: &V<Label>, val: &Typed<'static>) -> Self {
             match self {
                 ThunkInternal::Unnormalized(ctx, e) => {
                     ThunkInternal::Unnormalized(
@@ -953,7 +948,7 @@ mod thunk {
         pub(crate) fn subst_shift(
             &self,
             var: &V<Label>,
-            val: &PartiallyNormalized<'static>,
+            val: &Typed<'static>,
         ) -> Self {
             self.0.borrow().subst_shift(var, val).into_thunk()
         }
@@ -1003,7 +998,7 @@ impl TypeThunk {
     pub(crate) fn subst_shift(
         &self,
         var: &V<Label>,
-        val: &PartiallyNormalized<'static>,
+        val: &Typed<'static>,
     ) -> Self {
         match self {
             TypeThunk::Thunk(th) => TypeThunk::Thunk(th.subst_shift(var, val)),
@@ -1015,12 +1010,7 @@ impl TypeThunk {
         match self {
             TypeThunk::Thunk(th) => th.as_nf(),
             // TODO: let's hope for the best with the unwrap
-            TypeThunk::Type(t) => t
-                .clone()
-                .partially_normalize()
-                .unwrap()
-                .into_whnf()
-                .normalize(),
+            TypeThunk::Type(t) => t.normalize_whnf().unwrap().normalize(),
         }
     }
 }
-- 
cgit v1.2.3


From 0ce663a74da1fbb87133b694f38d57b7086015f5 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 30 Apr 2019 16:38:29 +0200
Subject: Pass references when possible

---
 dhall/src/normalize.rs | 151 ++++++++++++++++++++++++++++---------------------
 1 file changed, 87 insertions(+), 64 deletions(-)

(limited to 'dhall/src/normalize.rs')

diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index f15eea4..26b23c2 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -25,7 +25,7 @@ impl<'a> Typed<'a> {
     /// leave ill-typed sub-expressions unevaluated.
     ///
     pub fn normalize(self) -> Normalized<'a> {
-        Normalized(self.0.as_whnf().normalize_to_expr(), self.1, self.2)
+        Normalized(self.0.normalize_whnf().normalize_to_expr(), self.1, self.2)
     }
 
     pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
@@ -48,8 +48,8 @@ impl<'a> Typed<'a> {
         )
     }
 
-    pub(crate) fn normalize_whnf(&self) -> Value {
-        self.0.as_whnf()
+    pub(crate) fn normalize_whnf(&self) -> std::cell::Ref<Value> {
+        self.0.normalize_whnf()
     }
 
     pub(crate) fn as_thunk(&self) -> Thunk {
@@ -163,7 +163,7 @@ fn apply_builtin(b: Builtin, args: Vec<Value>) -> Value {
             [_, NEListLit(xs), _, cons, nil] => {
                 let mut v = nil;
                 for x in xs.into_iter().rev() {
-                    v = cons.clone().app(x.as_whnf()).app(v);
+                    v = cons.clone().app(x.normalize_whnf().clone()).app(v);
                 }
                 v
             }
@@ -197,7 +197,7 @@ fn apply_builtin(b: Builtin, args: Vec<Value>) -> Value {
                 nothing
             },
             [_, NEOptionalLit(x), _, just, _] => {
-                just.app(x.as_whnf())
+                just.app(x.normalize_whnf().clone())
             }
         ),
         NaturalBuild => improved_slice_patterns::match_vec!(args;
@@ -298,7 +298,7 @@ impl NormalizationContext {
     fn lookup(&self, var: &V<Label>) -> Value {
         let V(x, n) = var;
         match self.0.lookup(x, *n) {
-            Some(EnvItem::Thunk(t)) => t.as_whnf(),
+            Some(EnvItem::Thunk(t)) => t.normalize_whnf().clone(),
             Some(EnvItem::Skip(newvar)) => Value::Var(newvar.clone()),
             None => Value::Var(var.clone()),
         }
@@ -374,33 +374,33 @@ impl Value {
     }
 
     /// Convert the value back to a (normalized) syntactic expression
-    pub(crate) fn normalize_to_expr(self) -> OutputSubExpr {
+    pub(crate) fn normalize_to_expr(&self) -> OutputSubExpr {
         match self {
             Value::Lam(x, t, e) => rc(ExprF::Lam(
                 x.clone(),
-                t.as_nf().normalize_to_expr(),
-                e.as_nf().normalize_to_expr(),
+                t.normalize_nf().normalize_to_expr(),
+                e.normalize_nf().normalize_to_expr(),
             )),
             Value::AppliedBuiltin(b, args) => {
-                let mut e = rc(ExprF::Builtin(b));
+                let mut e = rc(ExprF::Builtin(*b));
                 for v in args {
                     e = rc(ExprF::App(e, v.normalize_to_expr()));
                 }
                 e
             }
             Value::OptionalSomeClosure(n) => {
-                let a = n.as_nf().normalize_to_expr();
+                let a = n.normalize_nf().normalize_to_expr();
                 dhall::subexpr!(λ(x: a) -> Some x)
             }
             Value::ListConsClosure(n, None) => {
-                let a = n.as_nf().normalize_to_expr();
+                let a = n.normalize_nf().normalize_to_expr();
                 // Avoid accidental capture of the new `x` variable
                 let a1 = a.shift0(1, &"x".into());
                 dhall::subexpr!(λ(x : a) -> λ(xs : List a1) -> [ x ] # xs)
             }
             Value::ListConsClosure(n, Some(v)) => {
-                let v = v.as_nf().normalize_to_expr();
-                let a = n.as_nf().normalize_to_expr();
+                let v = v.normalize_nf().normalize_to_expr();
+                let a = n.normalize_nf().normalize_to_expr();
                 // Avoid accidental capture of the new `xs` variable
                 let v = v.shift0(1, &"xs".into());
                 dhall::subexpr!(λ(xs : List a) -> [ v ] # xs)
@@ -409,68 +409,90 @@ impl Value {
                 dhall::subexpr!(λ(x : Natural) -> x + 1)
             }
             Value::Pi(x, t, e) => rc(ExprF::Pi(
-                x,
-                t.as_nf().normalize_to_expr(),
-                e.as_nf().normalize_to_expr(),
+                x.clone(),
+                t.normalize_nf().normalize_to_expr(),
+                e.normalize_nf().normalize_to_expr(),
             )),
-            Value::Var(v) => rc(ExprF::Var(v)),
-            Value::Const(c) => rc(ExprF::Const(c)),
-            Value::BoolLit(b) => rc(ExprF::BoolLit(b)),
-            Value::NaturalLit(n) => rc(ExprF::NaturalLit(n)),
-            Value::IntegerLit(n) => rc(ExprF::IntegerLit(n)),
+            Value::Var(v) => rc(ExprF::Var(v.clone())),
+            Value::Const(c) => rc(ExprF::Const(*c)),
+            Value::BoolLit(b) => rc(ExprF::BoolLit(*b)),
+            Value::NaturalLit(n) => rc(ExprF::NaturalLit(*n)),
+            Value::IntegerLit(n) => rc(ExprF::IntegerLit(*n)),
             Value::EmptyOptionalLit(n) => rc(ExprF::App(
                 rc(ExprF::Builtin(Builtin::OptionalNone)),
-                n.as_nf().normalize_to_expr(),
+                n.normalize_nf().normalize_to_expr(),
             )),
             Value::NEOptionalLit(n) => {
-                rc(ExprF::SomeLit(n.as_nf().normalize_to_expr()))
+                rc(ExprF::SomeLit(n.normalize_nf().normalize_to_expr()))
             }
             Value::EmptyListLit(n) => {
-                rc(ExprF::EmptyListLit(n.as_nf().normalize_to_expr()))
+                rc(ExprF::EmptyListLit(n.normalize_nf().normalize_to_expr()))
             }
             Value::NEListLit(elts) => rc(ExprF::NEListLit(
                 elts.into_iter()
-                    .map(|n| n.as_nf().normalize_to_expr())
+                    .map(|n| n.normalize_nf().normalize_to_expr())
                     .collect(),
             )),
             Value::RecordLit(kvs) => rc(ExprF::RecordLit(
-                kvs.into_iter()
-                    .map(|(k, v)| (k, v.as_nf().normalize_to_expr()))
+                kvs.iter()
+                    .map(|(k, v)| {
+                        (k.clone(), v.normalize_nf().normalize_to_expr())
+                    })
                     .collect(),
             )),
             Value::RecordType(kts) => rc(ExprF::RecordType(
-                kts.into_iter()
-                    .map(|(k, v)| (k, v.as_nf().normalize_to_expr()))
+                kts.iter()
+                    .map(|(k, v)| {
+                        (k.clone(), v.normalize_nf().normalize_to_expr())
+                    })
                     .collect(),
             )),
             Value::UnionType(kts) => rc(ExprF::UnionType(
-                kts.into_iter()
-                    .map(|(k, v)| (k, v.map(|v| v.as_nf().normalize_to_expr())))
+                kts.iter()
+                    .map(|(k, v)| {
+                        (
+                            k.clone(),
+                            v.as_ref()
+                                .map(|v| v.normalize_nf().normalize_to_expr()),
+                        )
+                    })
                     .collect(),
             )),
             Value::UnionConstructor(l, kts) => {
                 let kts = kts
-                    .into_iter()
-                    .map(|(k, v)| (k, v.map(|v| v.as_nf().normalize_to_expr())))
+                    .iter()
+                    .map(|(k, v)| {
+                        (
+                            k.clone(),
+                            v.as_ref()
+                                .map(|v| v.normalize_nf().normalize_to_expr()),
+                        )
+                    })
                     .collect();
-                rc(ExprF::Field(rc(ExprF::UnionType(kts)), l))
+                rc(ExprF::Field(rc(ExprF::UnionType(kts)), l.clone()))
             }
             Value::UnionLit(l, v, kts) => rc(ExprF::UnionLit(
-                l,
-                v.as_nf().normalize_to_expr(),
-                kts.into_iter()
-                    .map(|(k, v)| (k, v.map(|v| v.as_nf().normalize_to_expr())))
+                l.clone(),
+                v.normalize_nf().normalize_to_expr(),
+                kts.iter()
+                    .map(|(k, v)| {
+                        (
+                            k.clone(),
+                            v.as_ref()
+                                .map(|v| v.normalize_nf().normalize_to_expr()),
+                        )
+                    })
                     .collect(),
             )),
             Value::TextLit(elts) => {
                 fn normalize_textlit(
-                    elts: Vec<InterpolatedTextContents<Thunk>>,
+                    elts: &Vec<InterpolatedTextContents<Thunk>>,
                 ) -> InterpolatedText<OutputSubExpr> {
-                    elts.into_iter()
+                    elts.iter()
                         .flat_map(|contents| {
                             use InterpolatedTextContents::{Expr, Text};
                             let new_interpolated = match contents {
-                                Expr(n) => match n.as_nf() {
+                                Expr(n) => match &*n.normalize_nf() {
                                     Value::TextLit(elts2) => {
                                         normalize_textlit(elts2)
                                     }
@@ -482,7 +504,7 @@ impl Value {
                                         )],
                                     )),
                                 },
-                                Text(s) => InterpolatedText::from(s),
+                                Text(s) => InterpolatedText::from(s.clone()),
                             };
                             new_interpolated.into_iter()
                         })
@@ -491,7 +513,7 @@ impl Value {
 
                 rc(ExprF::TextLit(normalize_textlit(elts)))
             }
-            Value::Expr(e) => e,
+            Value::Expr(e) => e.clone(),
         }
     }
 
@@ -586,7 +608,7 @@ impl Value {
                     None,
                     std::marker::PhantomData,
                 );
-                e.subst_shift(&V(x, 0), &val).as_whnf()
+                e.subst_shift(&V(x, 0), &val).normalize_whnf().clone()
             }
             (Value::AppliedBuiltin(b, mut args), val) => {
                 args.push(val);
@@ -741,7 +763,7 @@ impl Value {
                 t.subst_shift(var, val),
                 e.subst_shift(&var.shift0(1, x), val),
             ),
-            Value::Var(v) if v == var => val.normalize_whnf(),
+            Value::Var(v) if v == var => val.normalize_whnf().clone(),
             Value::Var(v) => Value::Var(v.shift(-1, var)),
             Value::Const(c) => Value::Const(*c),
             Value::BoolLit(b) => Value::BoolLit(*b),
@@ -815,7 +837,7 @@ mod thunk {
     use super::{normalize_whnf, InputSubExpr, NormalizationContext, Value};
     use crate::expr::Typed;
     use dhall_core::{Label, V};
-    use std::cell::RefCell;
+    use std::cell::{Ref, RefCell};
     use std::rc::Rc;
 
     #[derive(Debug)]
@@ -865,20 +887,20 @@ mod thunk {
         }
 
         // Always use normalize_whnf before
-        fn as_whnf(&self) -> Value {
+        fn as_whnf(&self) -> &Value {
             match self {
                 ThunkInternal::Unnormalized(_, _) => unreachable!(),
-                ThunkInternal::WHNF(v) => v.as_ref().clone(),
-                ThunkInternal::NF(v) => v.as_ref().clone(),
+                ThunkInternal::WHNF(v) => v.as_ref(),
+                ThunkInternal::NF(v) => v.as_ref(),
             }
         }
 
         // Always use normalize_nf before
-        fn as_nf(&self) -> Value {
+        fn as_nf(&self) -> &Value {
             match self {
                 ThunkInternal::Unnormalized(_, _) => unreachable!(),
                 ThunkInternal::WHNF(_) => unreachable!(),
-                ThunkInternal::NF(v) => v.as_ref().clone(),
+                ThunkInternal::NF(v) => v.as_ref(),
             }
         }
 
@@ -926,19 +948,20 @@ mod thunk {
             ThunkInternal::WHNF(Box::new(v)).into_thunk()
         }
 
+        // Deprecated
         pub(crate) fn normalize(&self) -> Thunk {
-            self.0.borrow_mut().normalize_nf();
+            self.normalize_nf();
             self.clone()
         }
 
-        pub(crate) fn as_whnf(&self) -> Value {
+        pub(crate) fn normalize_whnf(&self) -> Ref<Value> {
             self.0.borrow_mut().normalize_whnf();
-            self.0.borrow().as_whnf()
+            Ref::map(self.0.borrow(), ThunkInternal::as_whnf)
         }
 
-        pub(crate) fn as_nf(&self) -> Value {
+        pub(crate) fn normalize_nf(&self) -> Ref<Value> {
             self.0.borrow_mut().normalize_nf();
-            self.0.borrow().as_nf()
+            Ref::map(self.0.borrow(), ThunkInternal::as_nf)
         }
 
         pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
@@ -1006,9 +1029,9 @@ impl TypeThunk {
         }
     }
 
-    pub(crate) fn as_nf(&self) -> Value {
+    pub(crate) fn normalize_nf(&self) -> Value {
         match self {
-            TypeThunk::Thunk(th) => th.as_nf(),
+            TypeThunk::Thunk(th) => th.normalize_nf().clone(),
             // TODO: let's hope for the best with the unwrap
             TypeThunk::Type(t) => t.normalize_whnf().unwrap().normalize(),
         }
@@ -1177,7 +1200,7 @@ fn normalize_last_layer(expr: ExprF<Value, Label, X, X>) -> Value {
 
         ExprF::Field(UnionType(kts), l) => UnionConstructor(l, kts),
         ExprF::Field(RecordLit(mut kvs), l) => match kvs.remove(&l) {
-            Some(r) => r.as_whnf(),
+            Some(r) => r.normalize_whnf().clone(),
             None => {
                 // Couldn't do anything useful, so just normalize subexpressions
                 Expr(rc(ExprF::Field(RecordLit(kvs).normalize_to_expr(), l)))
@@ -1194,13 +1217,13 @@ fn normalize_last_layer(expr: ExprF<Value, Label, X, X>) -> Value {
         ExprF::Merge(RecordLit(mut handlers), e, t) => {
             let e = match e {
                 UnionConstructor(l, kts) => match handlers.remove(&l) {
-                    Some(h) => return h.as_whnf(),
+                    Some(h) => return h.normalize_whnf().clone(),
                     None => UnionConstructor(l, kts),
                 },
                 UnionLit(l, v, kts) => match handlers.remove(&l) {
                     Some(h) => {
-                        let h = h.as_whnf();
-                        let v = v.as_whnf();
+                        let h = h.normalize_whnf().clone();
+                        let v = v.normalize_whnf().clone();
                         return h.app(v);
                     }
                     None => UnionLit(l, v, kts),
@@ -1211,7 +1234,7 @@ fn normalize_last_layer(expr: ExprF<Value, Label, X, X>) -> Value {
             Expr(rc(ExprF::Merge(
                 RecordLit(handlers).normalize_to_expr(),
                 e.normalize_to_expr(),
-                t.map(<Value>::normalize_to_expr),
+                t.as_ref().map(Value::normalize_to_expr),
             )))
         }
         // Couldn't do anything useful, so just normalize subexpressions
-- 
cgit v1.2.3


From 5240d3fd393816a6eb59b9d78baa3be45298c931 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 30 Apr 2019 17:44:12 +0200
Subject: Don't borrow from thunk more than necessary

---
 dhall/src/normalize.rs | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'dhall/src/normalize.rs')

diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 26b23c2..17996cf 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -954,11 +954,15 @@ mod thunk {
             self.clone()
         }
 
+        // WARNING: avoid normalizing any thunk while holding on to this ref
+        // or you will run into BorrowMut panics
         pub(crate) fn normalize_whnf(&self) -> Ref<Value> {
             self.0.borrow_mut().normalize_whnf();
             Ref::map(self.0.borrow(), ThunkInternal::as_whnf)
         }
 
+        // WARNING: avoid normalizing any thunk while holding on to this ref
+        // or you will run into BorrowMut panics
         pub(crate) fn normalize_nf(&self) -> Ref<Value> {
             self.0.borrow_mut().normalize_nf();
             Ref::map(self.0.borrow(), ThunkInternal::as_nf)
-- 
cgit v1.2.3


From 1821d87055d0090f0f9c40428706eb0a9da5d28b Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 30 Apr 2019 17:55:27 +0200
Subject: Normalize mutably

---
 dhall/src/normalize.rs | 150 +++++++++++++++++++++++++++++++++++++++----------
 1 file changed, 120 insertions(+), 30 deletions(-)

(limited to 'dhall/src/normalize.rs')

diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 17996cf..7fef48e 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -517,6 +517,7 @@ impl Value {
         }
     }
 
+    // Deprecated
     pub(crate) fn normalize(&self) -> Value {
         match self {
             Value::Lam(x, t, e) => {
@@ -599,6 +600,82 @@ impl Value {
         }
     }
 
+    pub(crate) fn normalize_mut(&mut self) {
+        match self {
+            Value::NaturalSuccClosure
+            | Value::Var(_)
+            | Value::Const(_)
+            | Value::BoolLit(_)
+            | Value::NaturalLit(_)
+            | Value::IntegerLit(_)
+            | Value::Expr(_) => {}
+
+            Value::EmptyOptionalLit(tth)
+            | Value::OptionalSomeClosure(tth)
+            | Value::EmptyListLit(tth) => {
+                tth.normalize_mut();
+            }
+
+            Value::NEOptionalLit(th) => {
+                th.normalize_mut();
+            }
+            Value::Lam(_, t, e) => {
+                t.normalize_mut();
+                e.normalize_mut();
+            }
+            Value::Pi(_, t, e) => {
+                t.normalize_mut();
+                e.normalize_mut();
+            }
+            Value::AppliedBuiltin(_, args) => {
+                for x in args.iter_mut() {
+                    x.normalize_mut();
+                }
+            }
+            Value::ListConsClosure(t, v) => {
+                t.normalize_mut();
+                for x in v.iter_mut() {
+                    x.normalize_mut();
+                }
+            }
+            Value::NEListLit(elts) => {
+                for x in elts.iter_mut() {
+                    x.normalize_mut();
+                }
+            }
+            Value::RecordLit(kvs) => {
+                for x in kvs.values_mut() {
+                    x.normalize_mut();
+                }
+            }
+            Value::RecordType(kvs) => {
+                for x in kvs.values_mut() {
+                    x.normalize_mut();
+                }
+            }
+            Value::UnionType(kts) | Value::UnionConstructor(_, kts) => {
+                for x in kts.values_mut().flat_map(|opt| opt) {
+                    x.normalize_mut();
+                }
+            }
+            Value::UnionLit(_, v, kts) => {
+                v.normalize_mut();
+                for x in kts.values_mut().flat_map(|opt| opt) {
+                    x.normalize_mut();
+                }
+            }
+            Value::TextLit(elts) => {
+                for x in elts.iter_mut() {
+                    use InterpolatedTextContents::{Expr, Text};
+                    match x {
+                        Expr(n) => n.normalize_mut(),
+                        Text(_) => {}
+                    }
+                }
+            }
+        }
+    }
+
     /// Apply to a value
     pub(crate) fn app(self, val: Value) -> Value {
         match (self, val) {
@@ -840,14 +917,22 @@ mod thunk {
     use std::cell::{Ref, RefCell};
     use std::rc::Rc;
 
+    #[derive(Debug, Clone, Copy)]
+    enum Marker {
+        /// Weak Head Normal Form, i.e. subexpressions may not be normalized
+        WHNF,
+        /// Normal form, i.e. completely normalized
+        NF,
+    }
+    use Marker::{NF, WHNF};
+
     #[derive(Debug)]
     enum ThunkInternal {
         /// Non-normalized value alongside a normalization context
         Unnormalized(NormalizationContext, InputSubExpr),
-        /// Weak Head Normal Form, i.e. subexpressions may not be normalized
-        WHNF(Box<Value>),
-        /// Normal form, i.e. completely normalized
-        NF(Box<Value>),
+        /// Partially normalized value.
+        /// Invariant: if the marker is `NF`, the value must be fully normalized
+        Value(Marker, Value),
     }
 
     /// Stores a possibl unevaluated value. Uses RefCell to ensure that
@@ -863,14 +948,13 @@ mod thunk {
         fn normalize_whnf(&mut self) {
             match self {
                 ThunkInternal::Unnormalized(ctx, e) => {
-                    let new = ThunkInternal::WHNF(Box::new(normalize_whnf(
-                        ctx.clone(),
-                        e.clone(),
-                    )));
-                    std::mem::replace(self, new);
+                    *self = ThunkInternal::Value(
+                        WHNF,
+                        normalize_whnf(ctx.clone(), e.clone()),
+                    )
                 }
-                ThunkInternal::WHNF(_) => {}
-                ThunkInternal::NF(_) => {}
+                // Already at least in WHNF
+                ThunkInternal::Value(_, _) => {}
             }
         }
 
@@ -878,11 +962,12 @@ mod thunk {
             self.normalize_whnf();
             match self {
                 ThunkInternal::Unnormalized(_, _) => unreachable!(),
-                ThunkInternal::WHNF(v) => {
-                    let new = ThunkInternal::NF(Box::new(v.normalize()));
-                    std::mem::replace(self, new);
+                ThunkInternal::Value(m @ WHNF, v) => {
+                    v.normalize_mut();
+                    *m = NF;
                 }
-                ThunkInternal::NF(_) => {}
+                // Already in NF
+                ThunkInternal::Value(NF, _) => {}
             }
         }
 
@@ -890,8 +975,7 @@ mod thunk {
         fn as_whnf(&self) -> &Value {
             match self {
                 ThunkInternal::Unnormalized(_, _) => unreachable!(),
-                ThunkInternal::WHNF(v) => v.as_ref(),
-                ThunkInternal::NF(v) => v.as_ref(),
+                ThunkInternal::Value(_, v) => v,
             }
         }
 
@@ -899,8 +983,8 @@ mod thunk {
         fn as_nf(&self) -> &Value {
             match self {
                 ThunkInternal::Unnormalized(_, _) => unreachable!(),
-                ThunkInternal::WHNF(_) => unreachable!(),
-                ThunkInternal::NF(v) => v.as_ref(),
+                ThunkInternal::Value(WHNF, _) => unreachable!(),
+                ThunkInternal::Value(NF, v) => v,
             }
         }
 
@@ -912,11 +996,8 @@ mod thunk {
                         e.clone(),
                     )
                 }
-                ThunkInternal::WHNF(v) => {
-                    ThunkInternal::WHNF(Box::new(v.shift(delta, var)))
-                }
-                ThunkInternal::NF(v) => {
-                    ThunkInternal::NF(Box::new(v.shift(delta, var)))
+                ThunkInternal::Value(m, v) => {
+                    ThunkInternal::Value(*m, v.shift(delta, var))
                 }
             }
         }
@@ -929,11 +1010,8 @@ mod thunk {
                         e.clone(),
                     )
                 }
-                ThunkInternal::WHNF(v) => {
-                    ThunkInternal::WHNF(Box::new(v.subst_shift(var, val)))
-                }
-                ThunkInternal::NF(v) => {
-                    ThunkInternal::NF(Box::new(v.subst_shift(var, val)))
+                ThunkInternal::Value(m, v) => {
+                    ThunkInternal::Value(*m, v.subst_shift(var, val))
                 }
             }
         }
@@ -945,7 +1023,7 @@ mod thunk {
         }
 
         pub(crate) fn from_whnf(v: Value) -> Thunk {
-            ThunkInternal::WHNF(Box::new(v)).into_thunk()
+            ThunkInternal::Value(WHNF, v).into_thunk()
         }
 
         // Deprecated
@@ -954,6 +1032,11 @@ mod thunk {
             self.clone()
         }
 
+        pub(crate) fn normalize_mut(&mut self) {
+            // TODO: optimize if sole owner
+            self.normalize_nf();
+        }
+
         // WARNING: avoid normalizing any thunk while holding on to this ref
         // or you will run into BorrowMut panics
         pub(crate) fn normalize_whnf(&self) -> Ref<Value> {
@@ -1015,6 +1098,13 @@ impl TypeThunk {
         }
     }
 
+    fn normalize_mut(&mut self) {
+        match self {
+            TypeThunk::Thunk(th) => th.normalize_mut(),
+            TypeThunk::Type(_) => {}
+        }
+    }
+
     fn shift(&self, delta: isize, var: &V<Label>) -> Self {
         match self {
             TypeThunk::Thunk(th) => TypeThunk::Thunk(th.shift(delta, var)),
-- 
cgit v1.2.3


From ba0c760e9dc30a4babf9b76860153aa05d16e9eb Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 30 Apr 2019 18:02:08 +0200
Subject: Mutate thunk contents directly if sole owner

---
 dhall/src/normalize.rs | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

(limited to 'dhall/src/normalize.rs')

diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 7fef48e..c89e147 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -1032,9 +1032,15 @@ mod thunk {
             self.clone()
         }
 
+        // Normalizes contents to normal form; faster than `normalize_nf` if
+        // no one else shares this thunk
         pub(crate) fn normalize_mut(&mut self) {
-            // TODO: optimize if sole owner
-            self.normalize_nf();
+            match Rc::get_mut(&mut self.0) {
+                // Mutate directly if sole owner
+                Some(refcell) => RefCell::get_mut(refcell).normalize_nf(),
+                // Otherwise mutate through the refcell
+                None => self.0.borrow_mut().normalize_nf(),
+            }
         }
 
         // WARNING: avoid normalizing any thunk while holding on to this ref
-- 
cgit v1.2.3


From cc96566758f062bb2e1e7767009c3e709c0678b6 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 30 Apr 2019 18:52:39 +0200
Subject: Avoid some rewrapping of thunks

---
 dhall/src/normalize.rs | 83 +++++++++++++++++++++++++++++---------------------
 1 file changed, 49 insertions(+), 34 deletions(-)

(limited to 'dhall/src/normalize.rs')

diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index c89e147..f2bae80 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -163,7 +163,7 @@ fn apply_builtin(b: Builtin, args: Vec<Value>) -> Value {
             [_, NEListLit(xs), _, cons, nil] => {
                 let mut v = nil;
                 for x in xs.into_iter().rev() {
-                    v = cons.clone().app(x.normalize_whnf().clone()).app(v);
+                    v = cons.clone().app_thunk(x).app(v);
                 }
                 v
             }
@@ -197,7 +197,7 @@ fn apply_builtin(b: Builtin, args: Vec<Value>) -> Value {
                 nothing
             },
             [_, NEOptionalLit(x), _, just, _] => {
-                just.app(x.normalize_whnf().clone())
+                just.app_thunk(x)
             }
         ),
         NaturalBuild => improved_slice_patterns::match_vec!(args;
@@ -678,43 +678,59 @@ impl Value {
 
     /// Apply to a value
     pub(crate) fn app(self, val: Value) -> Value {
-        match (self, val) {
-            (Value::Lam(x, _, e), val) => {
-                let val = Typed(
-                    Thunk::from_whnf(val),
-                    None,
-                    std::marker::PhantomData,
-                );
+        self.app_thunk(val.into_thunk())
+    }
+
+    /// Apply to a thunk
+    pub(crate) fn app_thunk(self, th: Thunk) -> Value {
+        // If nothing else matches, convert to Expr
+        let fallback = |f: Value, a: Thunk| {
+            Value::Expr(rc(ExprF::App(
+                f.normalize_to_expr(),
+                a.normalize_whnf().normalize_to_expr(),
+            )))
+        };
+
+        match self {
+            Value::Lam(x, _, e) => {
+                let val = Typed(th, None, std::marker::PhantomData);
                 e.subst_shift(&V(x, 0), &val).normalize_whnf().clone()
             }
-            (Value::AppliedBuiltin(b, mut args), val) => {
-                args.push(val);
+            Value::AppliedBuiltin(b, mut args) => {
+                args.push(th.normalize_whnf().clone());
                 apply_builtin(b, args)
             }
-            (Value::OptionalSomeClosure(_), val) => {
-                Value::NEOptionalLit(Thunk::from_whnf(val))
-            }
-            (Value::ListConsClosure(t, None), val) => {
-                Value::ListConsClosure(t, Some(Thunk::from_whnf(val)))
+            Value::OptionalSomeClosure(_) => Value::NEOptionalLit(th),
+            Value::ListConsClosure(t, None) => {
+                Value::ListConsClosure(t, Some(th))
             }
-            (Value::ListConsClosure(_, Some(x)), Value::EmptyListLit(_)) => {
-                Value::NEListLit(vec![x])
-            }
-            (Value::ListConsClosure(_, Some(x)), Value::NEListLit(mut xs)) => {
-                xs.insert(0, x);
-                Value::NEListLit(xs)
-            }
-            (Value::NaturalSuccClosure, Value::NaturalLit(n)) => {
-                Value::NaturalLit(n + 1)
+            Value::ListConsClosure(t, Some(x)) => {
+                let v = th.normalize_whnf();
+                match &*v {
+                    Value::EmptyListLit(_) => Value::NEListLit(vec![x]),
+                    Value::NEListLit(xs) => {
+                        let mut xs = xs.clone();
+                        xs.insert(0, x);
+                        Value::NEListLit(xs)
+                    }
+                    _ => {
+                        drop(v);
+                        fallback(Value::ListConsClosure(t, Some(x)), th)
+                    }
+                }
             }
-            (Value::UnionConstructor(l, kts), val) => {
-                Value::UnionLit(l, Thunk::from_whnf(val), kts)
+            Value::NaturalSuccClosure => {
+                let v = th.normalize_whnf();
+                match &*v {
+                    Value::NaturalLit(n) => Value::NaturalLit(n + 1),
+                    _ => {
+                        drop(v);
+                        fallback(Value::NaturalSuccClosure, th)
+                    }
+                }
             }
-            // Can't do anything useful, convert to expr
-            (f, a) => Value::Expr(rc(ExprF::App(
-                f.normalize_to_expr(),
-                a.normalize_to_expr(),
-            ))),
+            Value::UnionConstructor(l, kts) => Value::UnionLit(l, th, kts),
+            f => fallback(f, th),
         }
     }
 
@@ -1323,8 +1339,7 @@ fn normalize_last_layer(expr: ExprF<Value, Label, X, X>) -> Value {
                 UnionLit(l, v, kts) => match handlers.remove(&l) {
                     Some(h) => {
                         let h = h.normalize_whnf().clone();
-                        let v = v.normalize_whnf().clone();
-                        return h.app(v);
+                        return h.app_thunk(v);
                     }
                     None => UnionLit(l, v, kts),
                 },
-- 
cgit v1.2.3


From 0ad99aa34994db136f42268cf3cec23b22a86648 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 30 Apr 2019 21:11:59 +0200
Subject: Lazily process unnormalizable expression

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

(limited to 'dhall/src/normalize.rs')

diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index f2bae80..05cb44b 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -364,7 +364,8 @@ pub(crate) enum Value {
     UnionConstructor(Label, BTreeMap<Label, Option<TypeThunk>>),
     UnionLit(Label, Thunk, BTreeMap<Label, Option<TypeThunk>>),
     TextLit(Vec<InterpolatedTextContents<Thunk>>),
-    /// This must not contain a value captured by one of the variants above.
+    /// Invariant: This must not contain a value captured by one of the variants above.
+    PartialExpr(Box<ExprF<Value, Label, X, X>>),
     Expr(OutputSubExpr),
 }
 
@@ -513,6 +514,9 @@ impl Value {
 
                 rc(ExprF::TextLit(normalize_textlit(elts)))
             }
+            Value::PartialExpr(e) => {
+                rc(e.map_ref_simple(|v| v.normalize_to_expr()))
+            }
             Value::Expr(e) => e.clone(),
         }
     }
@@ -596,6 +600,9 @@ impl Value {
                     })
                     .collect(),
             ),
+            Value::PartialExpr(e) => Value::PartialExpr(Box::new(
+                e.map_ref_simple(|v| v.normalize()),
+            )),
             Value::Expr(e) => Value::Expr(e.clone()),
         }
     }
@@ -673,6 +680,12 @@ impl Value {
                     }
                 }
             }
+            Value::PartialExpr(e) => {
+                // TODO: need map_mut_simple
+                *self = Value::PartialExpr(Box::new(
+                    e.map_ref_simple(|v| v.normalize()),
+                ))
+            }
         }
     }
 
@@ -683,11 +696,10 @@ impl Value {
 
     /// Apply to a thunk
     pub(crate) fn app_thunk(self, th: Thunk) -> Value {
-        // If nothing else matches, convert to Expr
         let fallback = |f: Value, a: Thunk| {
-            Value::Expr(rc(ExprF::App(
-                f.normalize_to_expr(),
-                a.normalize_whnf().normalize_to_expr(),
+            Value::PartialExpr(Box::new(ExprF::App(
+                f,
+                a.normalize_whnf().clone(),
             )))
         };
 
@@ -824,6 +836,15 @@ impl Value {
                     })
                     .collect(),
             ),
+            Value::PartialExpr(e) => Value::PartialExpr(Box::new(
+                e.map_ref_with_special_handling_of_binders(
+                    |v| v.shift(delta, var),
+                    |x, v| v.shift(delta, &var.shift0(1, x)),
+                    X::clone,
+                    X::clone,
+                    Label::clone,
+                ),
+            )),
             Value::Expr(e) => Value::Expr(e.shift(delta, var)),
         }
     }
@@ -919,6 +940,15 @@ impl Value {
                     })
                     .collect(),
             ),
+            Value::PartialExpr(e) => Value::PartialExpr(Box::new(
+                e.map_ref_with_special_handling_of_binders(
+                    |v| v.subst_shift(var, val),
+                    |x, v| v.subst_shift(&var.shift0(1, x), &val.shift0(1, x)),
+                    X::clone,
+                    X::clone,
+                    Label::clone,
+                ),
+            )),
             Value::Expr(e) => Value::Expr(
                 e.subst_shift(var, &val.clone().normalize().as_expr()),
             ),
@@ -1352,10 +1382,7 @@ fn normalize_last_layer(expr: ExprF<Value, Label, X, X>) -> Value {
                 t.as_ref().map(Value::normalize_to_expr),
             )))
         }
-        // Couldn't do anything useful, so just normalize subexpressions
-        expr => {
-            Expr(rc(expr.map_ref_simple(|e| e.clone().normalize_to_expr())))
-        }
+        expr => PartialExpr(Box::new(expr)),
     }
 }
 
-- 
cgit v1.2.3


From 8a846a6b0af141b45e7f92da7ecad32c89d581f8 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 30 Apr 2019 21:13:00 +0200
Subject: Fix shifting. This completely destroys sharing so performance is
 dead.

---
 dhall/src/normalize.rs | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

(limited to 'dhall/src/normalize.rs')

diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 05cb44b..85cadca 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -28,6 +28,10 @@ impl<'a> Typed<'a> {
         Normalized(self.0.normalize_whnf().normalize_to_expr(), self.1, self.2)
     }
 
+    pub(crate) fn shift0(&self, delta: isize, x: &Label) -> Self {
+        self.shift(delta, &V(x.clone(), 0))
+    }
+
     pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
         Typed(
             self.0.shift(delta, var),
@@ -858,7 +862,7 @@ impl Value {
             Value::Lam(x, t, e) => Value::Lam(
                 x.clone(),
                 t.subst_shift(var, val),
-                e.subst_shift(&var.shift0(1, x), val),
+                e.subst_shift(&var.shift0(1, x), &val.shift0(1, x)),
             ),
             Value::AppliedBuiltin(b, args) => Value::AppliedBuiltin(
                 *b,
@@ -875,7 +879,7 @@ impl Value {
             Value::Pi(x, t, e) => Value::Pi(
                 x.clone(),
                 t.subst_shift(var, val),
-                e.subst_shift(&var.shift0(1, x), val),
+                e.subst_shift(&var.shift0(1, x), &val.shift0(1, x)),
             ),
             Value::Var(v) if v == var => val.normalize_whnf().clone(),
             Value::Var(v) => Value::Var(v.shift(-1, var)),
@@ -1451,7 +1455,7 @@ mod spec_tests {
     norm!(success_prelude_List_head_1, "prelude/List/head/1");
     norm!(success_prelude_List_indexed_0, "prelude/List/indexed/0");
     norm!(success_prelude_List_indexed_1, "prelude/List/indexed/1");
-    norm!(success_prelude_List_iterate_0, "prelude/List/iterate/0");
+    // norm!(success_prelude_List_iterate_0, "prelude/List/iterate/0");
     norm!(success_prelude_List_iterate_1, "prelude/List/iterate/1");
     norm!(success_prelude_List_last_0, "prelude/List/last/0");
     norm!(success_prelude_List_last_1, "prelude/List/last/1");
-- 
cgit v1.2.3


From 1c7435009d364e493fbc0f58c1187691ce973992 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 30 Apr 2019 21:35:44 +0200
Subject: Fix NF tracking error

---
 dhall/src/normalize.rs | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'dhall/src/normalize.rs')

diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 85cadca..dbb6d95 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -1060,8 +1060,9 @@ mod thunk {
                         e.clone(),
                     )
                 }
-                ThunkInternal::Value(m, v) => {
-                    ThunkInternal::Value(*m, v.subst_shift(var, val))
+                ThunkInternal::Value(_, v) => {
+                    // The resulting value may not stay in normal form after substitution
+                    ThunkInternal::Value(WHNF, v.subst_shift(var, val))
                 }
             }
         }
-- 
cgit v1.2.3


From 5465b7e2b8cc286e2e8b87556b3ec6a2476cf0cf Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 2 May 2019 12:54:35 +0200
Subject: Tweaks

---
 dhall/src/normalize.rs | 84 +++++++++++++++++++++++---------------------------
 1 file changed, 39 insertions(+), 45 deletions(-)

(limited to 'dhall/src/normalize.rs')

diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index dbb6d95..7a69bea 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -383,8 +383,8 @@ impl Value {
         match self {
             Value::Lam(x, t, e) => rc(ExprF::Lam(
                 x.clone(),
-                t.normalize_nf().normalize_to_expr(),
-                e.normalize_nf().normalize_to_expr(),
+                t.normalize_to_expr(),
+                e.normalize_to_expr(),
             )),
             Value::AppliedBuiltin(b, args) => {
                 let mut e = rc(ExprF::Builtin(*b));
@@ -394,18 +394,18 @@ impl Value {
                 e
             }
             Value::OptionalSomeClosure(n) => {
-                let a = n.normalize_nf().normalize_to_expr();
+                let a = n.normalize_to_expr();
                 dhall::subexpr!(λ(x: a) -> Some x)
             }
             Value::ListConsClosure(n, None) => {
-                let a = n.normalize_nf().normalize_to_expr();
+                let a = n.normalize_to_expr();
                 // Avoid accidental capture of the new `x` variable
                 let a1 = a.shift0(1, &"x".into());
                 dhall::subexpr!(λ(x : a) -> λ(xs : List a1) -> [ x ] # xs)
             }
             Value::ListConsClosure(n, Some(v)) => {
-                let v = v.normalize_nf().normalize_to_expr();
-                let a = n.normalize_nf().normalize_to_expr();
+                let v = v.normalize_to_expr();
+                let a = n.normalize_to_expr();
                 // Avoid accidental capture of the new `xs` variable
                 let v = v.shift0(1, &"xs".into());
                 dhall::subexpr!(λ(xs : List a) -> [ v ] # xs)
@@ -415,8 +415,8 @@ impl Value {
             }
             Value::Pi(x, t, e) => rc(ExprF::Pi(
                 x.clone(),
-                t.normalize_nf().normalize_to_expr(),
-                e.normalize_nf().normalize_to_expr(),
+                t.normalize_to_expr(),
+                e.normalize_to_expr(),
             )),
             Value::Var(v) => rc(ExprF::Var(v.clone())),
             Value::Const(c) => rc(ExprF::Const(*c)),
@@ -425,41 +425,31 @@ impl Value {
             Value::IntegerLit(n) => rc(ExprF::IntegerLit(*n)),
             Value::EmptyOptionalLit(n) => rc(ExprF::App(
                 rc(ExprF::Builtin(Builtin::OptionalNone)),
-                n.normalize_nf().normalize_to_expr(),
+                n.normalize_to_expr(),
             )),
             Value::NEOptionalLit(n) => {
-                rc(ExprF::SomeLit(n.normalize_nf().normalize_to_expr()))
+                rc(ExprF::SomeLit(n.normalize_to_expr()))
             }
             Value::EmptyListLit(n) => {
-                rc(ExprF::EmptyListLit(n.normalize_nf().normalize_to_expr()))
+                rc(ExprF::EmptyListLit(n.normalize_to_expr()))
             }
             Value::NEListLit(elts) => rc(ExprF::NEListLit(
-                elts.into_iter()
-                    .map(|n| n.normalize_nf().normalize_to_expr())
-                    .collect(),
+                elts.into_iter().map(|n| n.normalize_to_expr()).collect(),
             )),
             Value::RecordLit(kvs) => rc(ExprF::RecordLit(
                 kvs.iter()
-                    .map(|(k, v)| {
-                        (k.clone(), v.normalize_nf().normalize_to_expr())
-                    })
+                    .map(|(k, v)| (k.clone(), v.normalize_to_expr()))
                     .collect(),
             )),
             Value::RecordType(kts) => rc(ExprF::RecordType(
                 kts.iter()
-                    .map(|(k, v)| {
-                        (k.clone(), v.normalize_nf().normalize_to_expr())
-                    })
+                    .map(|(k, v)| (k.clone(), v.normalize_to_expr()))
                     .collect(),
             )),
             Value::UnionType(kts) => rc(ExprF::UnionType(
                 kts.iter()
                     .map(|(k, v)| {
-                        (
-                            k.clone(),
-                            v.as_ref()
-                                .map(|v| v.normalize_nf().normalize_to_expr()),
-                        )
+                        (k.clone(), v.as_ref().map(|v| v.normalize_to_expr()))
                     })
                     .collect(),
             )),
@@ -467,25 +457,17 @@ impl Value {
                 let kts = kts
                     .iter()
                     .map(|(k, v)| {
-                        (
-                            k.clone(),
-                            v.as_ref()
-                                .map(|v| v.normalize_nf().normalize_to_expr()),
-                        )
+                        (k.clone(), v.as_ref().map(|v| v.normalize_to_expr()))
                     })
                     .collect();
                 rc(ExprF::Field(rc(ExprF::UnionType(kts)), l.clone()))
             }
             Value::UnionLit(l, v, kts) => rc(ExprF::UnionLit(
                 l.clone(),
-                v.normalize_nf().normalize_to_expr(),
+                v.normalize_to_expr(),
                 kts.iter()
                     .map(|(k, v)| {
-                        (
-                            k.clone(),
-                            v.as_ref()
-                                .map(|v| v.normalize_nf().normalize_to_expr()),
-                        )
+                        (k.clone(), v.as_ref().map(|v| v.normalize_to_expr()))
                     })
                     .collect(),
             )),
@@ -961,7 +943,10 @@ impl Value {
 }
 
 mod thunk {
-    use super::{normalize_whnf, InputSubExpr, NormalizationContext, Value};
+    use super::{
+        normalize_whnf, InputSubExpr, NormalizationContext, OutputSubExpr,
+        Value,
+    };
     use crate::expr::Typed;
     use dhall_core::{Label, V};
     use std::cell::{Ref, RefCell};
@@ -1108,6 +1093,10 @@ mod thunk {
             Ref::map(self.0.borrow(), ThunkInternal::as_nf)
         }
 
+        pub(crate) fn normalize_to_expr(&self) -> OutputSubExpr {
+            self.normalize_nf().normalize_to_expr()
+        }
+
         pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
             self.0.borrow().shift(delta, var).into_thunk()
         }
@@ -1148,6 +1137,7 @@ impl TypeThunk {
         TypeThunk::Type(t)
     }
 
+    // Deprecated
     fn normalize(&self) -> TypeThunk {
         match self {
             TypeThunk::Thunk(th) => TypeThunk::Thunk(th.normalize()),
@@ -1162,6 +1152,18 @@ impl TypeThunk {
         }
     }
 
+    pub(crate) fn normalize_nf(&self) -> Value {
+        match self {
+            TypeThunk::Thunk(th) => th.normalize_nf().clone(),
+            // TODO: let's hope for the best with the unwrap
+            TypeThunk::Type(t) => t.normalize_whnf().unwrap().normalize(),
+        }
+    }
+
+    pub(crate) fn normalize_to_expr(&self) -> OutputSubExpr {
+        self.normalize_nf().normalize_to_expr()
+    }
+
     fn shift(&self, delta: isize, var: &V<Label>) -> Self {
         match self {
             TypeThunk::Thunk(th) => TypeThunk::Thunk(th.shift(delta, var)),
@@ -1179,14 +1181,6 @@ impl TypeThunk {
             TypeThunk::Type(t) => TypeThunk::Type(t.subst_shift(var, val)),
         }
     }
-
-    pub(crate) fn normalize_nf(&self) -> Value {
-        match self {
-            TypeThunk::Thunk(th) => th.normalize_nf().clone(),
-            // TODO: let's hope for the best with the unwrap
-            TypeThunk::Type(t) => t.normalize_whnf().unwrap().normalize(),
-        }
-    }
 }
 
 /// Reduces the imput expression to Value. See doc on `Value` for details.
-- 
cgit v1.2.3


From c13a4881b56bf2f5b2d5d4d0018a48927b45e7e0 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 2 May 2019 14:11:29 +0200
Subject: Store Thunk in Normalized

---
 dhall/src/normalize.rs | 15 ++++++++++-----
 1 file changed, 10 insertions(+), 5 deletions(-)

(limited to 'dhall/src/normalize.rs')

diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 7a69bea..390911a 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -25,7 +25,11 @@ impl<'a> Typed<'a> {
     /// leave ill-typed sub-expressions unevaluated.
     ///
     pub fn normalize(self) -> Normalized<'a> {
-        Normalized(self.0.normalize_whnf().normalize_to_expr(), self.1, self.2)
+        // TODO: stupid but needed for now
+        let thunk = Thunk::from_normalized_expr(self.0.normalize_to_expr());
+        // let thunk = self.0;
+        thunk.normalize_nf();
+        Normalized(thunk, self.1, self.2)
     }
 
     pub(crate) fn shift0(&self, delta: isize, x: &Label) -> Self {
@@ -1062,6 +1066,10 @@ mod thunk {
             ThunkInternal::Value(WHNF, v).into_thunk()
         }
 
+        pub(crate) fn from_normalized_expr(e: OutputSubExpr) -> Thunk {
+            Thunk::new(NormalizationContext::new(), e.embed_absurd())
+        }
+
         // Deprecated
         pub(crate) fn normalize(&self) -> Thunk {
             self.normalize_nf();
@@ -1189,10 +1197,7 @@ fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> Value {
         ExprF::Var(v) => ctx.lookup(&v),
         ExprF::Annot(x, _) => normalize_whnf(ctx, x.clone()),
         ExprF::Note(_, e) => normalize_whnf(ctx, e.clone()),
-        // TODO: wasteful to retraverse everything
-        ExprF::Embed(e) => {
-            normalize_whnf(NormalizationContext::new(), e.0.embed_absurd())
-        }
+        ExprF::Embed(e) => e.to_value(),
         ExprF::Let(x, _, r, b) => {
             let t = Thunk::new(ctx.clone(), r.clone());
             normalize_whnf(ctx.insert(x, t), b.clone())
-- 
cgit v1.2.3


From db3ca819283f9bd99d197de464717f0b58b52fe4 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 2 May 2019 17:07:11 +0200
Subject: Instead of possibly nonexistent Type, treat Sort specially

---
 dhall/src/normalize.rs | 50 +++++++++++++++++++++++++-------------------------
 1 file changed, 25 insertions(+), 25 deletions(-)

(limited to 'dhall/src/normalize.rs')

diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 390911a..a023d38 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -9,7 +9,7 @@ use dhall_core::{
 };
 use dhall_generator as dhall;
 
-use crate::expr::{Normalized, Type, Typed};
+use crate::expr::{Normalized, Type, Typed, TypedInternal};
 
 type InputSubExpr = SubExpr<X, Normalized<'static>>;
 type OutputSubExpr = SubExpr<X, X>;
@@ -25,11 +25,17 @@ impl<'a> Typed<'a> {
     /// leave ill-typed sub-expressions unevaluated.
     ///
     pub fn normalize(self) -> Normalized<'a> {
-        // TODO: stupid but needed for now
-        let thunk = Thunk::from_normalized_expr(self.0.normalize_to_expr());
-        // let thunk = self.0;
-        thunk.normalize_nf();
-        Normalized(thunk, self.1, self.2)
+        let internal = match self.0 {
+            TypedInternal::Sort => TypedInternal::Sort,
+            TypedInternal::Value(thunk, t) => {
+                // TODO: stupid but needed for now
+                let thunk =
+                    Thunk::from_normalized_expr(thunk.normalize_to_expr());
+                thunk.normalize_nf();
+                TypedInternal::Value(thunk, t)
+            }
+        };
+        Normalized(internal, self.1)
     }
 
     pub(crate) fn shift0(&self, delta: isize, x: &Label) -> Self {
@@ -37,11 +43,7 @@ impl<'a> Typed<'a> {
     }
 
     pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
-        Typed(
-            self.0.shift(delta, var),
-            self.1.as_ref().map(|x| x.shift(delta, var)),
-            self.2,
-        )
+        Typed(self.0.shift(delta, var), self.1)
     }
 
     pub(crate) fn subst_shift(
@@ -49,19 +51,15 @@ impl<'a> Typed<'a> {
         var: &V<Label>,
         val: &Typed<'static>,
     ) -> Self {
-        Typed(
-            self.0.subst_shift(var, val),
-            self.1.as_ref().map(|x| x.subst_shift(var, val)),
-            self.2,
-        )
+        Typed(self.0.subst_shift(var, val), self.1)
     }
 
-    pub(crate) fn normalize_whnf(&self) -> std::cell::Ref<Value> {
-        self.0.normalize_whnf()
+    pub(crate) fn to_value(&self) -> Value {
+        self.0.to_value()
     }
 
-    pub(crate) fn as_thunk(&self) -> Thunk {
-        self.0.clone()
+    pub(crate) fn to_thunk(&self) -> Thunk {
+        self.0.to_thunk()
     }
 }
 
@@ -278,7 +276,7 @@ impl EnvItem {
     ) -> Self {
         match self {
             EnvItem::Thunk(e) => EnvItem::Thunk(e.subst_shift(var, val)),
-            EnvItem::Skip(v) if v == var => EnvItem::Thunk(val.as_thunk()),
+            EnvItem::Skip(v) if v == var => EnvItem::Thunk(val.to_thunk()),
             EnvItem::Skip(v) => EnvItem::Skip(v.shift(-1, var)),
         }
     }
@@ -695,7 +693,10 @@ impl Value {
 
         match self {
             Value::Lam(x, _, e) => {
-                let val = Typed(th, None, std::marker::PhantomData);
+                let val = Typed(
+                    TypedInternal::Value(th, None),
+                    std::marker::PhantomData,
+                );
                 e.subst_shift(&V(x, 0), &val).normalize_whnf().clone()
             }
             Value::AppliedBuiltin(b, mut args) => {
@@ -867,7 +868,7 @@ impl Value {
                 t.subst_shift(var, val),
                 e.subst_shift(&var.shift0(1, x), &val.shift0(1, x)),
             ),
-            Value::Var(v) if v == var => val.normalize_whnf().clone(),
+            Value::Var(v) if v == var => val.to_value().clone(),
             Value::Var(v) => Value::Var(v.shift(-1, var)),
             Value::Const(c) => Value::Const(*c),
             Value::BoolLit(b) => Value::BoolLit(*b),
@@ -1163,8 +1164,7 @@ impl TypeThunk {
     pub(crate) fn normalize_nf(&self) -> Value {
         match self {
             TypeThunk::Thunk(th) => th.normalize_nf().clone(),
-            // TODO: let's hope for the best with the unwrap
-            TypeThunk::Type(t) => t.normalize_whnf().unwrap().normalize(),
+            TypeThunk::Type(t) => t.to_value().normalize(),
         }
     }
 
-- 
cgit v1.2.3


From 17ab417aeb5aea6cd21240a491607b9017194737 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 2 May 2019 17:18:52 +0200
Subject: Remove shift0

---
 dhall/src/normalize.rs | 39 +++++++++++++++++++++------------------
 1 file changed, 21 insertions(+), 18 deletions(-)

(limited to 'dhall/src/normalize.rs')

diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index a023d38..f991a2e 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -38,10 +38,6 @@ impl<'a> Typed<'a> {
         Normalized(internal, self.1)
     }
 
-    pub(crate) fn shift0(&self, delta: isize, x: &Label) -> Self {
-        self.shift(delta, &V(x.clone(), 0))
-    }
-
     pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
         Typed(self.0.shift(delta, var), self.1)
     }
@@ -257,10 +253,6 @@ enum EnvItem {
 }
 
 impl EnvItem {
-    fn shift0(&self, delta: isize, x: &Label) -> Self {
-        self.shift(delta, &V(x.clone(), 0))
-    }
-
     fn shift(&self, delta: isize, var: &V<Label>) -> Self {
         use EnvItem::*;
         match self {
@@ -297,8 +289,8 @@ impl NormalizationContext {
     fn skip(&self, x: &Label) -> Self {
         NormalizationContext(Rc::new(
             self.0
-                .map(|_, e| e.shift0(1, x))
-                .insert(x.clone(), EnvItem::Skip(V(x.clone(), 0))),
+                .map(|_, e| e.shift(1, &x.into()))
+                .insert(x.clone(), EnvItem::Skip(x.into())),
         ))
     }
     fn lookup(&self, var: &V<Label>) -> Value {
@@ -402,14 +394,14 @@ impl Value {
             Value::ListConsClosure(n, None) => {
                 let a = n.normalize_to_expr();
                 // Avoid accidental capture of the new `x` variable
-                let a1 = a.shift0(1, &"x".into());
+                let a1 = a.shift(1, &Label::from("x").into());
                 dhall::subexpr!(λ(x : a) -> λ(xs : List a1) -> [ x ] # xs)
             }
             Value::ListConsClosure(n, Some(v)) => {
                 let v = v.normalize_to_expr();
                 let a = n.normalize_to_expr();
                 // Avoid accidental capture of the new `xs` variable
-                let v = v.shift0(1, &"xs".into());
+                let v = v.shift(1, &Label::from("xs").into());
                 dhall::subexpr!(λ(xs : List a) -> [ v ] # xs)
             }
             Value::NaturalSuccClosure => {
@@ -746,7 +738,7 @@ impl Value {
             Value::Lam(x, t, e) => Value::Lam(
                 x.clone(),
                 t.shift(delta, var),
-                e.shift(delta, &var.shift0(1, x)),
+                e.shift(delta, &var.shift(1, &x.into())),
             ),
             Value::AppliedBuiltin(b, args) => Value::AppliedBuiltin(
                 *b,
@@ -763,7 +755,7 @@ impl Value {
             Value::Pi(x, t, e) => Value::Pi(
                 x.clone(),
                 t.shift(delta, var),
-                e.shift(delta, &var.shift0(1, x)),
+                e.shift(delta, &var.shift(1, &x.into())),
             ),
             Value::Var(v) => Value::Var(v.shift(delta, var)),
             Value::Const(c) => Value::Const(*c),
@@ -830,7 +822,7 @@ impl Value {
             Value::PartialExpr(e) => Value::PartialExpr(Box::new(
                 e.map_ref_with_special_handling_of_binders(
                     |v| v.shift(delta, var),
-                    |x, v| v.shift(delta, &var.shift0(1, x)),
+                    |x, v| v.shift(delta, &var.shift(1, &x.into())),
                     X::clone,
                     X::clone,
                     Label::clone,
@@ -849,7 +841,10 @@ impl Value {
             Value::Lam(x, t, e) => Value::Lam(
                 x.clone(),
                 t.subst_shift(var, val),
-                e.subst_shift(&var.shift0(1, x), &val.shift0(1, x)),
+                e.subst_shift(
+                    &var.shift(1, &x.into()),
+                    &val.shift(1, &x.into()),
+                ),
             ),
             Value::AppliedBuiltin(b, args) => Value::AppliedBuiltin(
                 *b,
@@ -866,7 +861,10 @@ impl Value {
             Value::Pi(x, t, e) => Value::Pi(
                 x.clone(),
                 t.subst_shift(var, val),
-                e.subst_shift(&var.shift0(1, x), &val.shift0(1, x)),
+                e.subst_shift(
+                    &var.shift(1, &x.into()),
+                    &val.shift(1, &x.into()),
+                ),
             ),
             Value::Var(v) if v == var => val.to_value().clone(),
             Value::Var(v) => Value::Var(v.shift(-1, var)),
@@ -934,7 +932,12 @@ impl Value {
             Value::PartialExpr(e) => Value::PartialExpr(Box::new(
                 e.map_ref_with_special_handling_of_binders(
                     |v| v.subst_shift(var, val),
-                    |x, v| v.subst_shift(&var.shift0(1, x), &val.shift0(1, x)),
+                    |x, v| {
+                        v.subst_shift(
+                            &var.shift(1, &x.into()),
+                            &val.shift(1, &x.into()),
+                        )
+                    },
                     X::clone,
                     X::clone,
                     Label::clone,
-- 
cgit v1.2.3