Cleanup

1 files changed, 144 insertions, 166 deletions

diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 26d062b..6d071f2 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -123,7 +123,7 @@ fn apply_builtin(
         (OptionalBuild, [t, g]) => g
             .clone()
             .app(AppliedBuiltin(ctx.clone(), Optional, vec![]).app(t.clone()))
-            .app(SomeConstructorClosure(Now::from_whnf(t.clone())))
+            .app(OptionalSomeClosure(Now::from_whnf(t.clone())))
             .app(EmptyOptionalLit(Now::from_whnf(t.clone()))),
         (OptionalFold, [_, EmptyOptionalLit(_), _, _, nothing]) => {
             nothing.clone()
@@ -225,9 +225,9 @@ enum WHNF {
     Lam(Label, Now, (NormalizationContext, InputSubExpr)),
     AppliedBuiltin(NormalizationContext, Builtin, Vec<WHNF>),
     /// `λ(x: a) -> Some x`
-    SomeConstructorClosure(Now),
-    /// `λ(x : a) -> λ(xs : List a) -> [ x ] # xs
-    /// `λ(xs : List a) -> [ x ] # xs
+    OptionalSomeClosure(Now),
+    /// `λ(x : a) -> λ(xs : List a) -> [ x ] # xs`
+    /// `λ(xs : List a) -> [ x ] # xs`
     ListConsClosure(Now, Option<Now>),
     /// `λ(x : Natural) -> x + 1`
     NaturalSuccClosure,
@@ -275,7 +275,7 @@ impl WHNF {
                 }
                 e.normalize_to_expr()
             }
-            WHNF::SomeConstructorClosure(n) => {
+            WHNF::OptionalSomeClosure(n) => {
                 let a = n.normalize().normalize_to_expr();
                 dhall::subexpr!(λ(x: a) -> Some x)
             }
@@ -410,7 +410,7 @@ impl WHNF {
                     None => WHNF::AppliedBuiltin(ctx, b, args),
                 }
             }
-            (WHNF::SomeConstructorClosure(_), val) => {
+            (WHNF::OptionalSomeClosure(_), val) => {
                 WHNF::NEOptionalLit(Now::from_whnf(val))
             }
             (WHNF::ListConsClosure(t, None), val) => {
@@ -448,8 +448,8 @@ impl WHNF {
                 b,
                 args.into_iter().map(|e| e.shift0(delta, label)).collect(),
             ),
-            WHNF::SomeConstructorClosure(n) => {
-                WHNF::SomeConstructorClosure(n.shift0(delta, label))
+            WHNF::OptionalSomeClosure(n) => {
+                WHNF::OptionalSomeClosure(n.shift0(delta, label))
             }
             WHNF::ListConsClosure(t, v) => WHNF::ListConsClosure(
                 t.shift0(delta, label),
@@ -557,206 +557,184 @@ impl Now {
 
 /// Reduces the imput expression to WHNF. See doc on `WHNF` for details.
 fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> WHNF {
-    let expr = match expr.as_ref() {
-        ExprF::Var(v) => return ctx.lookup(&v),
-        ExprF::Annot(x, _) => return normalize_whnf(ctx, x.clone()),
-        ExprF::Note(_, e) => return normalize_whnf(ctx, e.clone()),
+    match expr.as_ref() {
+        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) => return normalize_whnf(ctx, e.0.embed_absurd()),
+        ExprF::Embed(e) => normalize_whnf(ctx, e.0.embed_absurd()),
         ExprF::Let(x, _, r, b) => {
             let r = normalize_whnf(ctx.clone(), r.clone());
-            return normalize_whnf(ctx.insert(x, r), b.clone());
+            normalize_whnf(ctx.insert(x, r), b.clone())
         }
-        ExprF::Lam(x, t, e) => {
-            return WHNF::Lam(
-                x.clone(),
-                Now::new(ctx.clone(), t.clone()),
-                (ctx, e.clone()),
-            )
-        }
-        ExprF::Builtin(b) => return WHNF::AppliedBuiltin(ctx, *b, vec![]),
-        ExprF::BoolLit(b) => return WHNF::BoolLit(*b),
-        ExprF::NaturalLit(n) => return WHNF::NaturalLit(*n),
+        ExprF::Lam(x, t, e) => WHNF::Lam(
+            x.clone(),
+            Now::new(ctx.clone(), t.clone()),
+            (ctx, e.clone()),
+        ),
+        ExprF::Builtin(b) => WHNF::AppliedBuiltin(ctx, *b, vec![]),
+        ExprF::BoolLit(b) => WHNF::BoolLit(*b),
+        ExprF::NaturalLit(n) => WHNF::NaturalLit(*n),
         ExprF::OldOptionalLit(None, e) => {
-            return WHNF::EmptyOptionalLit(Now::new(ctx, e.clone()))
+            WHNF::EmptyOptionalLit(Now::new(ctx, e.clone()))
         }
         ExprF::OldOptionalLit(Some(e), _) => {
-            return WHNF::NEOptionalLit(Now::new(ctx, e.clone()))
+            WHNF::NEOptionalLit(Now::new(ctx, e.clone()))
         }
         ExprF::EmptyOptionalLit(e) => {
-            return WHNF::EmptyOptionalLit(Now::new(ctx, e.clone()))
+            WHNF::EmptyOptionalLit(Now::new(ctx, e.clone()))
         }
         ExprF::NEOptionalLit(e) => {
-            return WHNF::NEOptionalLit(Now::new(ctx, e.clone()))
-        }
-        ExprF::EmptyListLit(e) => {
-            return WHNF::EmptyListLit(Now::new(ctx, e.clone()))
-        }
-        ExprF::NEListLit(elts) => {
-            return WHNF::NEListLit(
-                elts.iter()
-                    .map(|e| Now::new(ctx.clone(), e.clone()))
-                    .collect(),
-            )
-        }
-        ExprF::RecordLit(kvs) => {
-            return WHNF::RecordLit(
-                kvs.iter()
-                    .map(|(k, e)| (k.clone(), Now::new(ctx.clone(), e.clone())))
-                    .collect(),
-            )
-        }
-        ExprF::UnionType(kvs) => return WHNF::UnionType(ctx, kvs.clone()),
-        ExprF::UnionLit(l, x, kts) => {
-            return WHNF::UnionLit(
-                l.clone(),
-                Now::new(ctx.clone(), x.clone()),
-                (ctx, kts.clone()),
-            )
-        }
-        ExprF::TextLit(elts) => {
-            return WHNF::TextLit(
-                elts.iter()
-                    .map(|contents| {
-                        use InterpolatedTextContents::{Expr, Text};
-                        match contents {
-                            Expr(n) => Expr(Now::new(ctx.clone(), n.clone())),
-                            Text(s) => Text(s.clone()),
-                        }
-                    })
-                    .collect(),
-            )
+            WHNF::NEOptionalLit(Now::new(ctx, e.clone()))
         }
+        ExprF::EmptyListLit(e) => WHNF::EmptyListLit(Now::new(ctx, e.clone())),
+        ExprF::NEListLit(elts) => WHNF::NEListLit(
+            elts.iter()
+                .map(|e| Now::new(ctx.clone(), e.clone()))
+                .collect(),
+        ),
+        ExprF::RecordLit(kvs) => WHNF::RecordLit(
+            kvs.iter()
+                .map(|(k, e)| (k.clone(), Now::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()),
+            (ctx, kts.clone()),
+        ),
+        ExprF::TextLit(elts) => WHNF::TextLit(
+            elts.iter()
+                .map(|contents| {
+                    use InterpolatedTextContents::{Expr, Text};
+                    match contents {
+                        Expr(n) => Expr(Now::new(ctx.clone(), n.clone())),
+                        Text(s) => Text(s.clone()),
+                    }
+                })
+                .collect(),
+        ),
         ExprF::BoolIf(b, e1, e2) => {
             let b = normalize_whnf(ctx.clone(), b.clone());
             match b {
-                WHNF::BoolLit(true) => return normalize_whnf(ctx, e1.clone()),
-                WHNF::BoolLit(false) => return normalize_whnf(ctx, e2.clone()),
-                _ => expr,
+                WHNF::BoolLit(true) => normalize_whnf(ctx, e1.clone()),
+                WHNF::BoolLit(false) => normalize_whnf(ctx, e2.clone()),
+                _ => normalize_last_layer(ExprF::BoolIf(
+                    b,
+                    normalize_whnf(ctx.clone(), e1.clone()),
+                    normalize_whnf(ctx, e2.clone()),
+                )),
             }
         }
-        _ => expr,
-    };
-
-    // Recursively normalize all subexpressions
-    let expr: ExprF<WHNF, Label, X, X> =
-        expr.as_ref().map_ref_with_special_handling_of_binders(
-            |e| normalize_whnf(ctx.clone(), e.clone()),
-            |x, e| normalize_whnf(ctx.skip(x), e.clone()),
-            X::clone,
-            |_| unreachable!(),
-            Label::clone,
-        );
+        expr => {
+            // Recursively normalize subexpressions
+            let expr: ExprF<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()),
+                    X::clone,
+                    |_| unreachable!(),
+                    Label::clone,
+                );
 
-    normalize_last_layer(ctx, expr)
+            normalize_last_layer(expr)
+        }
+    }
 }
 
 /// When all sub-expressions have been (partially) normalized, eval the remaining toplevel layer.
-fn normalize_last_layer(
-    ctx: NormalizationContext,
-    expr: ExprF<WHNF, Label, X, X>,
-) -> WHNF {
+fn normalize_last_layer(expr: ExprF<WHNF, Label, X, X>) -> WHNF {
     use dhall_core::BinOp::*;
     use WHNF::*;
 
-    let expr = match expr {
-        ExprF::App(v, a) => return v.app(a),
+    match expr {
+        ExprF::App(v, a) => v.app(a),
 
-        ExprF::BinOp(BoolAnd, BoolLit(true), y) => return y,
-        ExprF::BinOp(BoolAnd, x, BoolLit(true)) => return x,
-        ExprF::BinOp(BoolAnd, BoolLit(false), _) => return BoolLit(false),
-        ExprF::BinOp(BoolAnd, _, BoolLit(false)) => return BoolLit(false),
-        ExprF::BinOp(BoolOr, BoolLit(true), _) => return BoolLit(true),
-        ExprF::BinOp(BoolOr, _, BoolLit(true)) => return BoolLit(true),
-        ExprF::BinOp(BoolOr, BoolLit(false), y) => return y,
-        ExprF::BinOp(BoolOr, x, BoolLit(false)) => return x,
-        ExprF::BinOp(BoolEQ, BoolLit(true), y) => return y,
-        ExprF::BinOp(BoolEQ, x, BoolLit(true)) => return x,
-        ExprF::BinOp(BoolNE, BoolLit(false), y) => return y,
-        ExprF::BinOp(BoolNE, x, BoolLit(false)) => return x,
-        ExprF::BinOp(BoolEQ, BoolLit(x), BoolLit(y)) => return BoolLit(x == y),
-        ExprF::BinOp(BoolNE, BoolLit(x), BoolLit(y)) => return BoolLit(x != y),
+        ExprF::BinOp(BoolAnd, BoolLit(true), y) => y,
+        ExprF::BinOp(BoolAnd, x, BoolLit(true)) => x,
+        ExprF::BinOp(BoolAnd, BoolLit(false), _) => BoolLit(false),
+        ExprF::BinOp(BoolAnd, _, BoolLit(false)) => BoolLit(false),
+        ExprF::BinOp(BoolOr, BoolLit(true), _) => BoolLit(true),
+        ExprF::BinOp(BoolOr, _, BoolLit(true)) => BoolLit(true),
+        ExprF::BinOp(BoolOr, BoolLit(false), y) => y,
+        ExprF::BinOp(BoolOr, x, BoolLit(false)) => x,
+        ExprF::BinOp(BoolEQ, BoolLit(true), y) => y,
+        ExprF::BinOp(BoolEQ, x, BoolLit(true)) => x,
+        ExprF::BinOp(BoolNE, BoolLit(false), y) => y,
+        ExprF::BinOp(BoolNE, x, BoolLit(false)) => x,
+        ExprF::BinOp(BoolEQ, BoolLit(x), BoolLit(y)) => BoolLit(x == y),
+        ExprF::BinOp(BoolNE, BoolLit(x), BoolLit(y)) => BoolLit(x != y),
 
-        ExprF::BinOp(NaturalPlus, NaturalLit(0), y) => return y,
-        ExprF::BinOp(NaturalPlus, x, NaturalLit(0)) => return x,
-        ExprF::BinOp(NaturalTimes, NaturalLit(0), _) => return NaturalLit(0),
-        ExprF::BinOp(NaturalTimes, _, NaturalLit(0)) => return NaturalLit(0),
-        ExprF::BinOp(NaturalTimes, NaturalLit(1), y) => return y,
-        ExprF::BinOp(NaturalTimes, x, NaturalLit(1)) => return x,
+        ExprF::BinOp(NaturalPlus, NaturalLit(0), y) => y,
+        ExprF::BinOp(NaturalPlus, x, NaturalLit(0)) => x,
+        ExprF::BinOp(NaturalTimes, NaturalLit(0), _) => NaturalLit(0),
+        ExprF::BinOp(NaturalTimes, _, NaturalLit(0)) => NaturalLit(0),
+        ExprF::BinOp(NaturalTimes, NaturalLit(1), y) => y,
+        ExprF::BinOp(NaturalTimes, x, NaturalLit(1)) => x,
         ExprF::BinOp(NaturalPlus, NaturalLit(x), NaturalLit(y)) => {
-            return NaturalLit(x + y)
+            NaturalLit(x + y)
         }
         ExprF::BinOp(NaturalTimes, NaturalLit(x), NaturalLit(y)) => {
-            return NaturalLit(x * y)
+            NaturalLit(x * y)
         }
 
-        ExprF::BinOp(ListAppend, EmptyListLit(_), y) => return y,
-        ExprF::BinOp(ListAppend, x, EmptyListLit(_)) => return x,
+        ExprF::BinOp(ListAppend, EmptyListLit(_), y) => y,
+        ExprF::BinOp(ListAppend, x, EmptyListLit(_)) => x,
         ExprF::BinOp(ListAppend, NEListLit(mut xs), NEListLit(mut ys)) => {
             xs.append(&mut ys);
-            return NEListLit(xs);
+            NEListLit(xs)
         }
         ExprF::BinOp(TextAppend, TextLit(mut x), TextLit(mut y)) => {
             x.append(&mut y);
-            return TextLit(x);
+            TextLit(x)
         }
 
-        ExprF::Field(UnionType(ctx, kts), l) => {
-            return UnionConstructor(ctx, l, kts)
-        }
-        ExprF::Field(RecordLit(mut kvs), l) => {
-            match kvs.remove(&l) {
-                Some(r) => return r.normalize(),
-                // Return ownership
-                None => ExprF::Field(RecordLit(kvs), l),
+        ExprF::Field(UnionType(ctx, kts), l) => UnionConstructor(ctx, l, kts),
+        ExprF::Field(RecordLit(mut kvs), l) => match kvs.remove(&l) {
+            Some(r) => r.normalize(),
+            None => {
+                // Couldn't do anything useful, so just normalize subexpressions
+                Expr(rc(ExprF::Field(RecordLit(kvs).normalize_to_expr(), l)))
             }
-        }
-        // Always simplify `x.{}` to `{}`
+        },
         ExprF::Projection(_, ls) if ls.is_empty() => {
-            return RecordLit(std::collections::BTreeMap::new())
+            RecordLit(std::collections::BTreeMap::new())
         }
-        ExprF::Projection(RecordLit(mut kvs), ls) => {
-            return RecordLit(
-                ls.into_iter()
-                    .filter_map(|l| kvs.remove(&l).map(|x| (l, x)))
-                    .collect(),
-            )
+        ExprF::Projection(RecordLit(mut kvs), ls) => RecordLit(
+            ls.into_iter()
+                .filter_map(|l| kvs.remove(&l).map(|x| (l, x)))
+                .collect(),
+        ),
+        ExprF::Merge(RecordLit(mut handlers), e, t) => {
+            let e = match e {
+                UnionConstructor(ctor_ctx, l, kts) => match handlers.remove(&l)
+                {
+                    Some(h) => return h.normalize(),
+                    None => UnionConstructor(ctor_ctx, l, kts),
+                },
+                UnionLit(l, v, (kts_ctx, 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)),
+                },
+                e => e,
+            };
+            // Couldn't do anything useful, so just normalize subexpressions
+            Expr(rc(ExprF::Merge(
+                RecordLit(handlers).normalize_to_expr(),
+                e.normalize_to_expr(),
+                t.map(WHNF::normalize_to_expr),
+            )))
         }
-        ExprF::Merge(
-            RecordLit(mut handlers),
-            UnionConstructor(ctor_ctx, l, kts),
-            t,
-        ) => match handlers.remove(&l) {
-            Some(h) => return h.normalize(),
-            // Return ownership
-            None => ExprF::Merge(
-                RecordLit(handlers),
-                UnionConstructor(ctor_ctx, l, kts),
-                t,
-            ),
-        },
-        ExprF::Merge(
-            RecordLit(mut handlers),
-            UnionLit(l, v, (kts_ctx, kts)),
-            t,
-        ) => match handlers.remove(&l) {
-            Some(h) => {
-                let h = h.normalize();
-                let v = v.normalize();
-                return normalize_last_layer(ctx, ExprF::App(h, v));
-            }
-            // Return ownership
-            None => ExprF::Merge(
-                RecordLit(handlers),
-                UnionLit(l, v, (kts_ctx, kts)),
-                t,
-            ),
-        },
-        expr => expr,
-    };
-
-    // Couldn't do anything useful, so just normalize subexpressions
-    Expr(rc(expr.map_ref_simple(|e| e.clone().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())))
+        }
+    }
 }
 
 /// Reduce an expression to its normal form, performing beta reduction