Merge pull request #48 from Nadrieril/exprf

Move recursion out of Expr for enhanced genericity

8 files changed, 269 insertions, 316 deletions

diff --git a/dhall/compare.fish b/dhall/compare.fish
deleted file mode 100755
index 154f06a..0000000
--- a/dhall/compare.fish
+++ /dev/null
@@ -1,9 +0,0 @@
-#!/usr/bin/env fish
-
-set dhall_hs_path ../dhall
-set dhall_hs $dhall_hs_path/.stack-work/install/**/bin/dhall
-set dhall_rs target/debug/dhall
-set input_file $argv[1]
-diff -u \
-    --label "dhall-hs < $input_file" (eval $dhall_hs < $input_file ^&1 | psub) \
-    --label "dhall-rs < $input_file" (eval $dhall_rs < $input_file ^&1 | psub)
diff --git a/dhall/src/binary.rs b/dhall/src/binary.rs
index 235a55b..1ba1873 100644
--- a/dhall/src/binary.rs
+++ b/dhall/src/binary.rs
@@ -1,9 +1,8 @@
 use dhall_core::*;
 use itertools::*;
 use serde_cbor::value::value as cbor;
-use std::rc::Rc;
 
-type ParsedExpr = Rc<Expr<X, Import>>;
+type ParsedExpr = SubExpr<X, Import>;
 
 #[derive(Debug)]
 pub enum DecodeError {
@@ -21,10 +20,10 @@ pub fn decode(data: &[u8]) -> Result<ParsedExpr, DecodeError> {
 fn cbor_value_to_dhall(data: &cbor::Value) -> Result<ParsedExpr, DecodeError> {
     use cbor::Value::*;
     use dhall_core::{BinOp, Builtin, Const};
-    use Expr::*;
+    use ExprF::*;
     Ok(rc(match data {
         String(s) => match Builtin::parse(s) {
-            Some(b) => Expr::Builtin(b),
+            Some(b) => ExprF::Builtin(b),
             None => match s.as_str() {
                 "True" => BoolLit(true),
                 "False" => BoolLit(false),
diff --git a/dhall/src/imports.rs b/dhall/src/imports.rs
index 8df4e97..96268ca 100644
--- a/dhall/src/imports.rs
+++ b/dhall/src/imports.rs
@@ -79,9 +79,9 @@ pub fn load_dhall_file(
         let resolve = |import: &Import| -> Expr<X, X> {
             resolve_import(import, &root).unwrap()
         };
-        expr.map_embed(&resolve).squash_embed()
+        expr.as_ref().map_embed(&resolve).squash_embed()
     } else {
-        panic_imports(&expr)
+        panic_imports(expr.as_ref())
     };
     Ok(expr)
 }
diff --git a/dhall/src/main.rs b/dhall/src/main.rs
index 1a2e309..77f558c 100644
--- a/dhall/src/main.rs
+++ b/dhall/src/main.rs
@@ -1,6 +1,5 @@
 use std::error::Error;
 use std::io::{self, Read};
-use std::rc::Rc;
 use term_painter::ToStyle;
 
 use dhall::*;
@@ -66,7 +65,7 @@ fn main() {
         }
     };
 
-    let expr: Rc<Expr<_, _>> = rc(imports::panic_imports(&expr));
+    let expr: SubExpr<_, _> = rc(imports::panic_imports(expr.as_ref()));
 
     let type_expr = match typecheck::type_of(expr.clone()) {
         Err(e) => {
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index d9bd08a..7574c2f 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -2,84 +2,61 @@
 use dhall_core::*;
 use dhall_generator::dhall_expr;
 use std::fmt;
-use std::rc::Rc;
 
-fn apply_builtin<S, A>(
-    b: Builtin,
-    mut args: Vec<SubExpr<S, A>>,
-) -> SubExpr<S, A>
+fn apply_builtin<S, A>(b: Builtin, args: &Vec<Expr<S, A>>) -> WhatNext<S, A>
 where
-    S: fmt::Debug,
-    A: fmt::Debug,
+    S: fmt::Debug + Clone,
+    A: fmt::Debug + Clone,
 {
     use dhall_core::Builtin::*;
-    use dhall_core::Expr::*;
-    let f = rc(Builtin(b));
-    // How many arguments a builtin needs, and which argument
-    // should be normalized and pattern-matched
-    let (len_consumption, arg_to_eval) = match b {
-        OptionalSome => (1, None),
-        OptionalNone => (1, None),
-        NaturalIsZero => (1, Some(0)),
-        NaturalEven => (1, Some(0)),
-        NaturalOdd => (1, Some(0)),
-        NaturalToInteger => (1, Some(0)),
-        NaturalShow => (1, Some(0)),
-        ListLength => (2, Some(1)),
-        ListHead => (2, Some(1)),
-        ListLast => (2, Some(1)),
-        ListReverse => (2, Some(1)),
-        ListIndexed => (2, Some(1)),
-        ListBuild => (2, Some(1)),
-        OptionalBuild => (2, Some(1)),
-        ListFold => (5, Some(1)),
-        OptionalFold => (5, Some(1)),
-        NaturalBuild => (1, Some(0)),
-        NaturalFold => (4, Some(0)),
-        _ => (0, None),
-    };
-    // Abort if not enough arguments present
-    if len_consumption > args.len() {
-        return rc(App(f, args));
-    }
-    // Normalize the important argument
-    if let Some(i) = arg_to_eval {
-        args[i] = Rc::clone(&normalize_whnf(&args[i]));
-    }
-    let evaled_arg = arg_to_eval.map(|i| args[i].as_ref());
-
-    let ret = match (b, evaled_arg, args.as_slice()) {
-        (OptionalSome, _, [x, ..]) => rc(NEOptionalLit(Rc::clone(x))),
-        (OptionalNone, _, [t, ..]) => rc(EmptyOptionalLit(Rc::clone(t))),
-        (NaturalIsZero, Some(NaturalLit(n)), _) => rc(BoolLit(*n == 0)),
-        (NaturalEven, Some(NaturalLit(n)), _) => rc(BoolLit(*n % 2 == 0)),
-        (NaturalOdd, Some(NaturalLit(n)), _) => rc(BoolLit(*n % 2 != 0)),
-        (NaturalToInteger, Some(NaturalLit(n)), _) => {
-            rc(IntegerLit(*n as isize))
+    use dhall_core::ExprF::*;
+    use WhatNext::*;
+    let (ret, rest) = match (b, args.as_slice()) {
+        (OptionalSome, [x, rest..]) => (rc(NEOptionalLit(x.roll())), rest),
+        (OptionalNone, [t, rest..]) => (rc(EmptyOptionalLit(t.roll())), rest),
+        (NaturalIsZero, [NaturalLit(n), rest..]) => {
+            (rc(BoolLit(*n == 0)), rest)
         }
-        (NaturalShow, Some(NaturalLit(n)), _) => {
-            rc(TextLit(n.to_string().into()))
+        (NaturalEven, [NaturalLit(n), rest..]) => {
+            (rc(BoolLit(*n % 2 == 0)), rest)
         }
-        (ListLength, Some(EmptyListLit(_)), _) => rc(NaturalLit(0)),
-        (ListLength, Some(NEListLit(ys)), _) => rc(NaturalLit(ys.len())),
-        (ListHead, Some(EmptyListLit(t)), _) => rc(EmptyOptionalLit(t.clone())),
-        (ListHead, Some(NEListLit(ys)), _) => {
-            rc(NEOptionalLit(ys.first().unwrap().clone()))
+        (NaturalOdd, [NaturalLit(n), rest..]) => {
+            (rc(BoolLit(*n % 2 != 0)), rest)
         }
-        (ListLast, Some(EmptyListLit(t)), _) => rc(EmptyOptionalLit(t.clone())),
-        (ListLast, Some(NEListLit(ys)), _) => {
-            rc(NEOptionalLit(ys.last().unwrap().clone()))
+        (NaturalToInteger, [NaturalLit(n), rest..]) => {
+            (rc(IntegerLit(*n as isize)), rest)
         }
-        (ListReverse, Some(EmptyListLit(t)), _) => rc(EmptyListLit(t.clone())),
-        (ListReverse, Some(NEListLit(ys)), _) => {
-            let ys = ys.iter().rev().cloned().collect();
-            rc(NEListLit(ys))
+        (NaturalShow, [NaturalLit(n), rest..]) => {
+            (rc(TextLit(n.to_string().into())), rest)
+        }
+        (ListLength, [_, EmptyListLit(_), rest..]) => (rc(NaturalLit(0)), rest),
+        (ListLength, [_, NEListLit(ys), rest..]) => {
+            (rc(NaturalLit(ys.len())), rest)
+        }
+        (ListHead, [_, EmptyListLit(t), rest..]) => {
+            (rc(EmptyOptionalLit(t.clone())), rest)
+        }
+        (ListHead, [_, NEListLit(ys), rest..]) => {
+            (rc(NEOptionalLit(ys.first().unwrap().clone())), rest)
         }
-        (ListIndexed, Some(EmptyListLit(t)), _) => {
-            let t = Rc::clone(t);
-            dhall_expr!([] : List ({ index : Natural, value : t }))
+        (ListLast, [_, EmptyListLit(t), rest..]) => {
+            (rc(EmptyOptionalLit(t.clone())), rest)
         }
-        (ListIndexed, Some(NEListLit(xs)), _) => {
+        (ListLast, [_, NEListLit(ys), rest..]) => {
+            (rc(NEOptionalLit(ys.last().unwrap().clone())), rest)
+        }
+        (ListReverse, [_, EmptyListLit(t), rest..]) => {
+            (rc(EmptyListLit(t.clone())), rest)
+        }
+        (ListReverse, [_, NEListLit(ys), rest..]) => {
+            let ys = ys.iter().rev().cloned().collect();
+            (rc(NEListLit(ys)), rest)
+        }
+        (ListIndexed, [_, EmptyListLit(t), rest..]) => (
+            dhall_expr!([] : List ({ index : Natural, value : t })),
+            rest,
+        ),
+        (ListIndexed, [_, NEListLit(xs), rest..]) => {
             let xs = xs
                 .iter()
                 .cloned()
@@ -89,100 +66,110 @@ where
                     dhall_expr!({ index = i, value = e })
                 })
                 .collect();
-            rc(NEListLit(xs))
+            (rc(NEListLit(xs)), rest)
         }
-        (ListBuild, _, [a0, g, ..]) => {
+        (ListBuild, [a0, g, rest..]) => {
             loop {
-                if let App(f2, args2) = g.as_ref() {
-                    if let (Builtin(ListFold), [_, x, rest..]) =
+                if let App(f2, args2) = g {
+                    if let (Builtin(ListFold), [_, x, rest_inner..]) =
                         (f2.as_ref(), args2.as_slice())
                     {
                         // fold/build fusion
-                        break rc(App(x.clone(), rest.to_vec()));
+                        break (rc(App(x.clone(), rest_inner.to_vec())), rest);
                     }
                 };
-                let a0 = Rc::clone(a0);
+                let a0 = a0.roll();
                 let a1 = shift(1, &V("a".into(), 0), &a0);
-                // TODO: use Embed to avoid reevaluating g
-                break dhall_expr!(
-                    g
-                    (List a0)
-                    (λ(x : a0) -> λ(xs : List a1) -> [ x ] # xs)
-                    ([] : List a0)
+                let g = g.roll();
+                break (
+                    dhall_expr!(
+                        g
+                        (List a0)
+                        (λ(x : a0) -> λ(xs : List a1) -> [ x ] # xs)
+                        ([] : List a0)
+                    ),
+                    rest,
                 );
             }
         }
-        (OptionalBuild, _, [a0, g, ..]) => {
+        (OptionalBuild, [a0, g, rest..]) => {
             loop {
-                if let App(f2, args2) = g.as_ref() {
-                    if let (Builtin(OptionalFold), [_, x, rest..]) =
+                if let App(f2, args2) = g {
+                    if let (Builtin(OptionalFold), [_, x, rest_inner..]) =
                         (f2.as_ref(), args2.as_slice())
                     {
                         // fold/build fusion
-                        break rc(App(x.clone(), rest.to_vec()));
+                        break (rc(App(x.clone(), rest_inner.to_vec())), rest);
                     }
                 };
-                let a0 = Rc::clone(a0);
-                // TODO: use Embed to avoid reevaluating g
-                break dhall_expr!(
-                    g
-                    (Optional a0)
-                    (λ(x: a0) -> Some x)
-                    (None a0)
+                let a0 = a0.roll();
+                let g = g.roll();
+                break (
+                    dhall_expr!(
+                        g
+                        (Optional a0)
+                        (λ(x: a0) -> Some x)
+                        (None a0)
+                    ),
+                    rest,
                 );
             }
         }
-        (ListFold, Some(EmptyListLit(_)), [_, _, _, _, nil, ..]) => {
-            Rc::clone(nil)
+        (ListFold, [_, EmptyListLit(_), _, _, nil, rest..]) => {
+            (nil.roll(), rest)
         }
-        (ListFold, Some(NEListLit(xs)), [_, _, _, cons, nil, ..]) => {
-            xs.iter().rev().fold(Rc::clone(nil), |acc, x| {
+        (ListFold, [_, NEListLit(xs), _, cons, nil, rest..]) => (
+            xs.iter().rev().fold(nil.roll(), |acc, x| {
                 let x = x.clone();
                 let acc = acc.clone();
-                let cons = Rc::clone(cons);
+                let cons = cons.roll();
                 dhall_expr!(cons x acc)
-            })
-        }
+            }),
+            rest,
+        ),
         // // fold/build fusion
         // (ListFold, [_, App(box Builtin(ListBuild), [_, x, rest..]), rest..]) => {
-        //     normalize_whnf(&App(bx(x.clone()), rest.to_vec()))
+        //     normalize_ref(&App(bx(x.clone()), rest.to_vec()))
         // }
-        (OptionalFold, Some(NEOptionalLit(x)), [_, _, _, just, _, ..]) => {
+        (OptionalFold, [_, NEOptionalLit(x), _, just, _, rest..]) => {
             let x = x.clone();
-            let just = Rc::clone(just);
-            dhall_expr!(just x)
+            let just = just.roll();
+            (dhall_expr!(just x), rest)
+        }
+        (OptionalFold, [_, EmptyOptionalLit(_), _, _, nothing, rest..]) => {
+            (nothing.roll(), rest)
         }
-        (
-            OptionalFold,
-            Some(EmptyOptionalLit(_)),
-            [_, _, _, _, nothing, ..],
-        ) => Rc::clone(nothing),
         // // fold/build fusion
         // (OptionalFold, [_, App(box Builtin(OptionalBuild), [_, x, rest..]), rest..]) => {
-        //     normalize_whnf(&App(bx(x.clone()), rest.to_vec()))
+        //     normalize_ref(&App(bx(x.clone()), rest.to_vec()))
         // }
-        (NaturalBuild, _, [g, ..]) => {
+        (NaturalBuild, [g, rest..]) => {
             loop {
-                if let App(f2, args2) = g.as_ref() {
-                    if let (Builtin(NaturalFold), [x, rest..]) =
+                if let App(f2, args2) = g {
+                    if let (Builtin(NaturalFold), [x, rest_inner..]) =
                         (f2.as_ref(), args2.as_slice())
                     {
                         // fold/build fusion
-                        break rc(App(x.clone(), rest.to_vec()));
+                        break (rc(App(x.clone(), rest_inner.to_vec())), rest);
                     }
                 };
-                // TODO: use Embed to avoid reevaluating g
-                break dhall_expr!(g Natural (λ(x : Natural) -> x + 1) 0);
+                let g = g.roll();
+                break (
+                    dhall_expr!(g Natural (λ(x : Natural) -> x + 1) 0),
+                    rest,
+                );
             }
         }
-        (NaturalFold, Some(NaturalLit(0)), [_, _, _, zero]) => Rc::clone(zero),
-        (NaturalFold, Some(NaturalLit(n)), [_, t, succ, zero]) => {
+        (NaturalFold, [NaturalLit(0), _, _, zero, rest..]) => {
+            (zero.roll(), rest)
+        }
+        (NaturalFold, [NaturalLit(n), t, succ, zero, rest..]) => {
             let fold = rc(Builtin(NaturalFold));
             let n = rc(NaturalLit(n - 1));
-            let t = Rc::clone(t);
-            let succ = Rc::clone(succ);
-            let zero = Rc::clone(zero);
-            dhall_expr!(succ (fold n t succ zero))
+            let t = t.roll();
+            let succ = succ.roll();
+            let zero = zero.roll();
+            (dhall_expr!(succ (fold n t succ zero)), rest)
         }
         // (NaturalFold, Some(App(f2, args2)), _) => {
         //     match (f2.as_ref(), args2.as_slice()) {
@@ -193,140 +180,127 @@ where
         //         _ => return rc(App(f, args)),
         //     }
         // }
-        _ => return rc(App(f, args)),
+        _ => return DoneAsIs,
     };
     // Put the remaining arguments back and eval again. In most cases
     // ret will not be of a form that can be applied, so this won't go very deep.
     // In lots of cases, there are no remaining args so this cann will just return ret.
-    normalize_whnf(&rc(Expr::App(ret, args.split_off(len_consumption))))
+    let rest: Vec<SubExpr<S, A>> = rest.iter().map(ExprF::roll).collect();
+    Continue(ExprF::App(ret, rest))
 }
 
-/// Reduce an expression to its weak head normal form, i.e. normalize
-/// just enough to get the first constructor of the final expression
-/// Is identical to normalize on primitive types, but not on more complex
-/// types like functions and records.
-/// This allows normalization to be lazy.
-pub fn normalize_whnf<S, A>(e: &SubExpr<S, A>) -> SubExpr<S, A>
+// Small enum to help with being DRY
+enum WhatNext<'a, S, A> {
+    // Recurse on this expression
+    Continue(Expr<S, A>),
+    ContinueSub(SubExpr<S, A>),
+    // The following expression is the normal form
+    Done(Expr<S, A>),
+    DoneRef(&'a Expr<S, A>),
+    DoneRefSub(&'a SubExpr<S, A>),
+    // The current expression is already in normal form
+    DoneAsIs,
+}
+
+pub fn normalize_ref<S, A>(expr: &Expr<S, A>) -> Expr<S, A>
 where
-    S: fmt::Debug,
-    A: fmt::Debug,
+    S: fmt::Debug + Clone,
+    A: fmt::Debug + Clone,
 {
     use dhall_core::BinOp::*;
-    use dhall_core::Expr::*;
-    match e.as_ref() {
+    use dhall_core::ExprF::*;
+    // Recursively normalize all subexpressions
+    let expr: ExprF<Expr<S, A>, Label, S, A> =
+        expr.map_ref_simple(|e| normalize_ref(e.as_ref()));
+
+    use WhatNext::*;
+    let what_next = match &expr {
         Let(f, _, r, b) => {
             let vf0 = &V(f.clone(), 0);
-            let r2 = shift(1, vf0, r);
+            let r2 = shift(1, vf0, &r.roll());
             // TODO: use a context
-            let b2 = subst(vf0, &r2, b);
+            let b2 = subst(vf0, &r2, &b.roll());
             // TODO: add tests sensitive to shift errors before
             // trying anything
             let b3 = shift(-1, vf0, &b2);
-            normalize_whnf(&b3)
-        }
-        Annot(x, _) => normalize_whnf(x),
-        Note(_, e) => normalize_whnf(e),
-        App(f, args) => {
-            let f = normalize_whnf(f);
-            match (f.as_ref(), args.as_slice()) {
-                (_, []) => f,
-                // TODO: use Embed to avoid reevaluating f
-                (App(f, args1), args2) => normalize_whnf(&rc(App(
-                    f.clone(),
-                    args1.iter().chain(args2.iter()).cloned().collect(),
-                ))),
-                (Lam(ref x, _, ref b), [a, rest..]) => {
-                    // Beta reduce
-                    let vx0 = &V(x.clone(), 0);
-                    let a2 = shift(1, vx0, a);
-                    let b2 = subst(vx0, &a2, &b);
-                    let b3 = shift(-1, vx0, &b2);
-                    normalize_whnf(&rc(App(b3, rest.to_vec())))
-                }
-                (Builtin(b), _) => apply_builtin(*b, args.to_vec()),
-                _ => rc(App(f, args.to_vec())),
-            }
+            ContinueSub(b3)
         }
-        BoolIf(b, t, f) => {
-            let b = normalize_whnf(b);
-            match b.as_ref() {
-                BoolLit(true) => normalize_whnf(t),
-                BoolLit(false) => normalize_whnf(f),
-                _ => rc(BoolIf(b, t.clone(), f.clone())),
-            }
+        Annot(x, _) => DoneRef(x),
+        Note(_, e) => DoneRef(e),
+        App(f, args) if args.is_empty() => DoneRef(f),
+        App(App(f, args1), args2) => Continue(App(
+            f.clone(),
+            args1
+                .iter()
+                .cloned()
+                .chain(args2.iter().map(ExprF::roll))
+                .collect(),
+        )),
+        App(Builtin(b), args) => apply_builtin(*b, args),
+        App(Lam(x, _, b), args) => {
+            let mut iter = args.iter();
+            // We know args is nonempty
+            let a = iter.next().unwrap();
+            // Beta reduce
+            let vx0 = &V(x.clone(), 0);
+            let a2 = shift(1, vx0, &a.roll());
+            let b2 = subst(vx0, &a2, &b);
+            let b3 = shift(-1, vx0, &b2);
+            Continue(App(b3, iter.map(ExprF::roll).collect()))
         }
+        BoolIf(BoolLit(true), t, _) => DoneRef(t),
+        BoolIf(BoolLit(false), _, f) => DoneRef(f),
         // TODO: interpolation
         // TextLit(t) =>
-        BinOp(o, x, y) => {
-            let x = normalize_whnf(x);
-            let y = normalize_whnf(y);
-            rc(match (o, x.as_ref(), y.as_ref()) {
-                (BoolAnd, BoolLit(x), BoolLit(y)) => BoolLit(*x && *y),
-                (BoolOr, BoolLit(x), BoolLit(y)) => BoolLit(*x || *y),
-                (BoolEQ, BoolLit(x), BoolLit(y)) => BoolLit(x == y),
-                (BoolNE, BoolLit(x), BoolLit(y)) => BoolLit(x != y),
-                (NaturalPlus, NaturalLit(x), NaturalLit(y)) => {
-                    NaturalLit(x + y)
-                }
-                (NaturalTimes, NaturalLit(x), NaturalLit(y)) => {
-                    NaturalLit(x * y)
-                }
-                (TextAppend, TextLit(x), TextLit(y)) => TextLit(x + y),
-                (ListAppend, EmptyListLit(t), EmptyListLit(_)) => {
-                    EmptyListLit(Rc::clone(t))
-                }
-                (ListAppend, EmptyListLit(_), _) => return y,
-                (ListAppend, _, EmptyListLit(_)) => return x,
-                (ListAppend, NEListLit(xs), NEListLit(ys)) => {
-                    let xs = xs.into_iter().cloned();
-                    let ys = ys.into_iter().cloned();
-                    NEListLit(xs.chain(ys).collect())
-                }
-                (o, _, _) => BinOp(*o, x, y),
-            })
+        BinOp(BoolAnd, BoolLit(x), BoolLit(y)) => Done(BoolLit(*x && *y)),
+        BinOp(BoolOr, BoolLit(x), BoolLit(y)) => Done(BoolLit(*x || *y)),
+        BinOp(BoolEQ, BoolLit(x), BoolLit(y)) => Done(BoolLit(x == y)),
+        BinOp(BoolNE, BoolLit(x), BoolLit(y)) => Done(BoolLit(x != y)),
+        BinOp(NaturalPlus, NaturalLit(x), NaturalLit(y)) => {
+            Done(NaturalLit(x + y))
         }
-        Merge(x, y, t) => {
-            let x = normalize_whnf(x);
-            let y = normalize_whnf(y);
-            match (x.as_ref(), y.as_ref()) {
-                (RecordLit(handlers), UnionLit(k, v, _)) => {
-                    match handlers.get(&k) {
-                        Some(h) => {
-                            normalize_whnf(&rc(App(h.clone(), vec![v.clone()])))
-                        }
-                        None => rc(Merge(x, y, t.clone())),
-                    }
-                }
-                _ => rc(Merge(x, y, t.clone())),
-            }
+        BinOp(NaturalTimes, NaturalLit(x), NaturalLit(y)) => {
+            Done(NaturalLit(x * y))
         }
-        Field(e, l) => {
-            let e = normalize_whnf(e);
-            match e.as_ref() {
-                RecordLit(kvs) => match kvs.get(&l) {
-                    Some(r) => normalize_whnf(r),
-                    None => rc(Field(e, l.clone())),
-                },
-                _ => rc(Field(e, l.clone())),
-            }
+        BinOp(TextAppend, TextLit(x), TextLit(y)) => Done(TextLit(x + y)),
+        BinOp(ListAppend, EmptyListLit(t), EmptyListLit(_)) => {
+            Done(EmptyListLit(SubExpr::clone(t)))
         }
-        Projection(_, ls) if ls.is_empty() => {
-            rc(RecordLit(std::collections::BTreeMap::new()))
+        BinOp(ListAppend, EmptyListLit(_), y) => DoneRef(y),
+        BinOp(ListAppend, x, EmptyListLit(_)) => DoneRef(x),
+        BinOp(ListAppend, NEListLit(xs), NEListLit(ys)) => {
+            let xs = xs.into_iter().cloned();
+            let ys = ys.into_iter().cloned();
+            Done(NEListLit(xs.chain(ys).collect()))
         }
-        Projection(e, ls) => {
-            let e = normalize_whnf(e);
-            match e.as_ref() {
-                RecordLit(kvs) => rc(RecordLit(
-                    ls.iter()
-                        .filter_map(|l| {
-                            kvs.get(l).map(|x| (l.clone(), x.clone()))
-                        })
-                        .collect(),
-                )),
-                _ => rc(Projection(e, ls.clone())),
+        Merge(RecordLit(handlers), UnionLit(k, v, _), _) => {
+            match handlers.get(&k) {
+                Some(h) => Continue(App(h.clone(), vec![v.clone()])),
+                None => DoneAsIs,
             }
         }
-        _ => Rc::clone(e),
+        Field(RecordLit(kvs), l) => match kvs.get(&l) {
+            Some(r) => DoneRefSub(r),
+            None => DoneAsIs,
+        },
+        Projection(_, ls) if ls.is_empty() => {
+            Done(RecordLit(std::collections::BTreeMap::new()))
+        }
+        Projection(RecordLit(kvs), ls) => Done(RecordLit(
+            ls.iter()
+                .filter_map(|l| kvs.get(l).map(|x| (l.clone(), x.clone())))
+                .collect(),
+        )),
+        _ => DoneAsIs,
+    };
+
+    match what_next {
+        Continue(e) => normalize_ref(&e),
+        ContinueSub(e) => normalize_ref(e.as_ref()),
+        Done(e) => e,
+        DoneRef(e) => e.clone(),
+        DoneRefSub(e) => e.unroll(),
+        DoneAsIs => expr.map_ref_simple(ExprF::roll),
     }
 }
 
@@ -341,8 +315,8 @@ where
 ///
 pub fn normalize<S, A>(e: SubExpr<S, A>) -> SubExpr<S, A>
 where
-    S: fmt::Debug,
-    A: fmt::Debug,
+    S: fmt::Debug + Clone,
+    A: fmt::Debug + Clone,
 {
-    map_subexpr_rc(&normalize_whnf(&e), |x| normalize(Rc::clone(x)))
+    normalize_ref(e.as_ref()).roll()
 }
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index f21721d..75e6e1d 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -1,7 +1,6 @@
 #![allow(non_snake_case)]
 use std::collections::HashSet;
 use std::fmt;
-use std::rc::Rc;
 
 use crate::normalize::normalize;
 use dhall_core;
@@ -13,7 +12,7 @@ use self::TypeMessage::*;
 
 fn axiom<S>(c: Const) -> Result<Const, TypeError<S>> {
     use dhall_core::Const::*;
-    use dhall_core::Expr::*;
+    use dhall_core::ExprF::*;
     match c {
         Type => Ok(Kind),
         Kind => Err(TypeError::new(&Context::new(), rc(Const(Kind)), Untyped)),
@@ -29,7 +28,7 @@ fn rule(a: Const, b: Const) -> Result<Const, ()> {
     }
 }
 
-fn match_vars(vl: &V, vr: &V, ctx: &[(Label, Label)]) -> bool {
+fn match_vars(vl: &V<Label>, vr: &V<Label>, ctx: &[(Label, Label)]) -> bool {
     let mut vl = vl.clone();
     let mut vr = vr.clone();
     let mut ctx = ctx.to_vec();
@@ -54,7 +53,7 @@ where
     S: ::std::fmt::Debug,
     T: ::std::fmt::Debug,
 {
-    use dhall_core::Expr::*;
+    use dhall_core::ExprF::*;
     fn go<S, T>(
         ctx: &mut Vec<(Label, Label)>,
         el: &Expr<S, X>,
@@ -113,7 +112,7 @@ where
     go::<S, T>(&mut ctx, eL0, eR0)
 }
 
-fn type_of_builtin<S>(b: Builtin) -> Rc<Expr<S, X>> {
+fn type_of_builtin<S>(b: Builtin) -> SubExpr<S, X> {
     use dhall_core::Builtin::*;
     match b {
         Bool | Natural | Integer | Double | Text => dhall_expr!(Type),
@@ -184,17 +183,16 @@ fn type_of_builtin<S>(b: Builtin) -> Rc<Expr<S, X>> {
 /// is not necessary for just type-checking.  If you actually care about the
 /// returned type then you may want to `normalize` it afterwards.
 pub fn type_with<S>(
-    ctx: &Context<Label, Rc<Expr<S, X>>>,
-    e: Rc<Expr<S, X>>,
-) -> Result<Rc<Expr<S, X>>, TypeError<S>>
+    ctx: &Context<Label, SubExpr<S, X>>,
+    e: SubExpr<S, X>,
+) -> Result<SubExpr<S, X>, TypeError<S>>
 where
-    S: ::std::fmt::Debug,
+    S: ::std::fmt::Debug + Clone,
 {
     use dhall_core::BinOp::*;
     use dhall_core::Builtin::*;
     use dhall_core::Const::*;
-    use dhall_core::Expr;
-    use dhall_core::Expr::*;
+    use dhall_core::ExprF::*;
     let mkerr = |msg: TypeMessage<_>| TypeError::new(ctx, e.clone(), msg);
     let ensure_const = |x: &SubExpr<_, _>, msg: TypeMessage<_>| match x.as_ref()
     {
@@ -266,7 +264,7 @@ where
                     return Err(mkerr(NotAFunction(f.clone(), tf)));
                 }
             };
-            let tA = normalize(Rc::clone(tA));
+            let tA = normalize(SubExpr::clone(tA));
             let tA2 = normalized_type_with(ctx, a.clone())?;
             if prop_equal(tA.as_ref(), tA2.as_ref()) {
                 let vx0 = &V(x.clone(), 0);
@@ -280,9 +278,9 @@ where
         }
         Let(f, mt, r, b) => {
             let r = if let Some(t) = mt {
-                rc(Annot(Rc::clone(r), Rc::clone(t)))
+                rc(Annot(SubExpr::clone(r), SubExpr::clone(t)))
             } else {
-                Rc::clone(r)
+                SubExpr::clone(r)
             };
 
             let tR = type_with(ctx, r)?;
@@ -351,7 +349,7 @@ where
         EmptyListLit(t) => {
             let s = normalized_type_with(ctx, t.clone())?;
             ensure_is_type(s, InvalidListType(t.clone()))?;
-            let t = normalize(Rc::clone(t));
+            let t = normalize(SubExpr::clone(t));
             return Ok(dhall_expr!(List t));
         }
         NEListLit(xs) => {
@@ -377,7 +375,7 @@ where
             return Ok(dhall_expr!(Optional t));
         }
         NEOptionalLit(x) => {
-            let t: Rc<Expr<_, _>> = type_with(ctx, x.clone())?;
+            let t: SubExpr<_, _> = type_with(ctx, x.clone())?;
             let s = normalized_type_with(ctx, t.clone())?;
             ensure_is_type(s, InvalidOptionalType(t.clone()))?;
             let t = normalize(t);
@@ -451,11 +449,11 @@ where
 }
 
 pub fn normalized_type_with<S>(
-    ctx: &Context<Label, Rc<Expr<S, X>>>,
-    e: Rc<Expr<S, X>>,
-) -> Result<Rc<Expr<S, X>>, TypeError<S>>
+    ctx: &Context<Label, SubExpr<S, X>>,
+    e: SubExpr<S, X>,
+) -> Result<SubExpr<S, X>, TypeError<S>>
 where
-    S: ::std::fmt::Debug,
+    S: ::std::fmt::Debug + Clone,
 {
     Ok(normalize(type_with(ctx, e)?))
 }
@@ -463,9 +461,9 @@ where
 /// `typeOf` is the same as `type_with` with an empty context, meaning that the
 /// expression must be closed (i.e. no free variables), otherwise type-checking
 /// will fail.
-pub fn type_of<S: ::std::fmt::Debug>(
-    e: Rc<Expr<S, X>>,
-) -> Result<Rc<Expr<S, X>>, TypeError<S>> {
+pub fn type_of<S: ::std::fmt::Debug + Clone>(
+    e: SubExpr<S, X>,
+) -> Result<SubExpr<S, X>, TypeError<S>> {
     let ctx = Context::new();
     type_with(&ctx, e) //.map(|e| e.into_owned())
 }
@@ -474,63 +472,58 @@ pub fn type_of<S: ::std::fmt::Debug>(
 #[derive(Debug)]
 pub enum TypeMessage<S> {
     UnboundVariable,
-    InvalidInputType(Rc<Expr<S, X>>),
-    InvalidOutputType(Rc<Expr<S, X>>),
-    NotAFunction(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
-    TypeMismatch(
-        Rc<Expr<S, X>>,
-        Rc<Expr<S, X>>,
-        Rc<Expr<S, X>>,
-        Rc<Expr<S, X>>,
-    ),
-    AnnotMismatch(Rc<Expr<S, X>>, Rc<Expr<S, X>>, Rc<Expr<S, X>>),
+    InvalidInputType(SubExpr<S, X>),
+    InvalidOutputType(SubExpr<S, X>),
+    NotAFunction(SubExpr<S, X>, SubExpr<S, X>),
+    TypeMismatch(SubExpr<S, X>, SubExpr<S, X>, SubExpr<S, X>, SubExpr<S, X>),
+    AnnotMismatch(SubExpr<S, X>, SubExpr<S, X>, SubExpr<S, X>),
     Untyped,
-    InvalidListElement(usize, Rc<Expr<S, X>>, Rc<Expr<S, X>>, Rc<Expr<S, X>>),
-    InvalidListType(Rc<Expr<S, X>>),
-    InvalidOptionalElement(Rc<Expr<S, X>>, Rc<Expr<S, X>>, Rc<Expr<S, X>>),
+    InvalidListElement(usize, SubExpr<S, X>, SubExpr<S, X>, SubExpr<S, X>),
+    InvalidListType(SubExpr<S, X>),
+    InvalidOptionalElement(SubExpr<S, X>, SubExpr<S, X>, SubExpr<S, X>),
     InvalidOptionalLiteral(usize),
-    InvalidOptionalType(Rc<Expr<S, X>>),
-    InvalidPredicate(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
+    InvalidOptionalType(SubExpr<S, X>),
+    InvalidPredicate(SubExpr<S, X>, SubExpr<S, X>),
     IfBranchMismatch(
-        Rc<Expr<S, X>>,
-        Rc<Expr<S, X>>,
-        Rc<Expr<S, X>>,
-        Rc<Expr<S, X>>,
+        SubExpr<S, X>,
+        SubExpr<S, X>,
+        SubExpr<S, X>,
+        SubExpr<S, X>,
     ),
-    IfBranchMustBeTerm(bool, Rc<Expr<S, X>>, Rc<Expr<S, X>>, Rc<Expr<S, X>>),
-    InvalidField(Label, Rc<Expr<S, X>>),
-    InvalidFieldType(Label, Rc<Expr<S, X>>),
-    InvalidAlternative(Label, Rc<Expr<S, X>>),
-    InvalidAlternativeType(Label, Rc<Expr<S, X>>),
+    IfBranchMustBeTerm(bool, SubExpr<S, X>, SubExpr<S, X>, SubExpr<S, X>),
+    InvalidField(Label, SubExpr<S, X>),
+    InvalidFieldType(Label, SubExpr<S, X>),
+    InvalidAlternative(Label, SubExpr<S, X>),
+    InvalidAlternativeType(Label, SubExpr<S, X>),
     DuplicateAlternative(Label),
-    MustCombineARecord(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
+    MustCombineARecord(SubExpr<S, X>, SubExpr<S, X>),
     FieldCollision(Label),
-    MustMergeARecord(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
-    MustMergeUnion(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
+    MustMergeARecord(SubExpr<S, X>, SubExpr<S, X>),
+    MustMergeUnion(SubExpr<S, X>, SubExpr<S, X>),
     UnusedHandler(HashSet<Label>),
     MissingHandler(HashSet<Label>),
-    HandlerInputTypeMismatch(Label, Rc<Expr<S, X>>, Rc<Expr<S, X>>),
-    HandlerOutputTypeMismatch(Label, Rc<Expr<S, X>>, Rc<Expr<S, X>>),
-    HandlerNotAFunction(Label, Rc<Expr<S, X>>),
-    NotARecord(Label, Rc<Expr<S, X>>, Rc<Expr<S, X>>),
-    MissingField(Label, Rc<Expr<S, X>>),
-    BinOpTypeMismatch(BinOp, Rc<Expr<S, X>>, Rc<Expr<S, X>>),
-    NoDependentLet(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
-    NoDependentTypes(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
+    HandlerInputTypeMismatch(Label, SubExpr<S, X>, SubExpr<S, X>),
+    HandlerOutputTypeMismatch(Label, SubExpr<S, X>, SubExpr<S, X>),
+    HandlerNotAFunction(Label, SubExpr<S, X>),
+    NotARecord(Label, SubExpr<S, X>, SubExpr<S, X>),
+    MissingField(Label, SubExpr<S, X>),
+    BinOpTypeMismatch(BinOp, SubExpr<S, X>, SubExpr<S, X>),
+    NoDependentLet(SubExpr<S, X>, SubExpr<S, X>),
+    NoDependentTypes(SubExpr<S, X>, SubExpr<S, X>),
 }
 
 /// A structured type error that includes context
 #[derive(Debug)]
 pub struct TypeError<S> {
-    pub context: Context<Label, Rc<Expr<S, X>>>,
-    pub current: Rc<Expr<S, X>>,
+    pub context: Context<Label, SubExpr<S, X>>,
+    pub current: SubExpr<S, X>,
     pub type_message: TypeMessage<S>,
 }
 
 impl<S> TypeError<S> {
     pub fn new(
-        context: &Context<Label, Rc<Expr<S, X>>>,
-        current: Rc<Expr<S, X>>,
+        context: &Context<Label, SubExpr<S, X>>,
+        current: SubExpr<S, X>,
         type_message: TypeMessage<S>,
     ) -> Self {
         TypeError {
diff --git a/dhall/tests/common/mod.rs b/dhall/tests/common/mod.rs
index 6b893e0..325b80f 100644
--- a/dhall/tests/common/mod.rs
+++ b/dhall/tests/common/mod.rs
@@ -111,7 +111,7 @@ pub fn run_test(base_path: &str, feature: Feature) {
             let expected_file_path = base_path + "B.dhall";
             let expr = rc(read_dhall_file(&expr_file_path).unwrap());
             let expected = rc(read_dhall_file(&expected_file_path).unwrap());
-            typecheck::type_of(rc(Expr::Annot(expr, expected))).unwrap();
+            typecheck::type_of(rc(ExprF::Annot(expr, expected))).unwrap();
         }
     }
 }
diff --git a/dhall/tests/dhall_type.rs b/dhall/tests/dhall_type.rs
index faece20..941e3a4 100644
--- a/dhall/tests/dhall_type.rs
+++ b/dhall/tests/dhall_type.rs
@@ -33,10 +33,7 @@ fn test_dhall_type() {
     #[derive(Type)]
     #[allow(dead_code)]
     struct C<T>(T, Option<String>);
-    assert_eq!(
-        <C<bool>>::get_type(),
-        <(bool, Option<String>)>::get_type()
-    );
+    assert_eq!(<C<bool>>::get_type(), <(bool, Option<String>)>::get_type());
 
     #[derive(Type)]
     #[allow(dead_code)]