Split-off normalization into its own crate

9 files changed, 328 insertions, 287 deletions

diff --git a/Cargo.lock b/Cargo.lock
index 58fdd1c..57ad661 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -136,6 +136,7 @@ version = "0.1.0"
 dependencies = [
  "bytecount 0.5.1 (registry+https://github.com/rust-lang/crates.io-index)",
  "dhall_core 0.1.0",
+ "dhall_normalize 0.1.0",
  "itertools 0.8.0 (registry+https://github.com/rust-lang/crates.io-index)",
  "lalrpop-util 0.16.3 (registry+https://github.com/rust-lang/crates.io-index)",
  "term-painter 0.2.4 (registry+https://github.com/rust-lang/crates.io-index)",
@@ -156,6 +157,19 @@ dependencies = [
 ]
 
 [[package]]
+name = "dhall_normalize"
+version = "0.1.0"
+dependencies = [
+ "bytecount 0.5.1 (registry+https://github.com/rust-lang/crates.io-index)",
+ "dhall_core 0.1.0",
+ "itertools 0.8.0 (registry+https://github.com/rust-lang/crates.io-index)",
+ "lalrpop-util 0.16.3 (registry+https://github.com/rust-lang/crates.io-index)",
+ "nom 3.2.1 (registry+https://github.com/rust-lang/crates.io-index)",
+ "pest 2.1.0 (git+https://github.com/pest-parser/pest)",
+ "term-painter 0.2.4 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
 name = "dhall_parser"
 version = "0.1.0"
 dependencies = [
diff --git a/dhall/Cargo.toml b/dhall/Cargo.toml
index db62d5b..80df0c3 100644
--- a/dhall/Cargo.toml
+++ b/dhall/Cargo.toml
@@ -10,3 +10,4 @@ itertools = "0.8.0"
 lalrpop-util = "0.16.3"
 term-painter = "0.2.3"
 dhall_core = { path = "../dhall_core" }
+dhall_normalize = { path = "../dhall_normalize" }
diff --git a/dhall/src/main.rs b/dhall/src/main.rs
index 3e8aca4..182f4a7 100644
--- a/dhall/src/main.rs
+++ b/dhall/src/main.rs
@@ -4,6 +4,7 @@ use term_painter::ToStyle;
 
 use dhall::*;
 use dhall_core::*;
+use dhall_normalize::*;
 
 const ERROR_STYLE: term_painter::Color = term_painter::Color::Red;
 const BOLD: term_painter::Attr = term_painter::Attr::Bold;
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 61a83e7..26192d2 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -9,7 +9,8 @@ use dhall_core::core::Builtin::*;
 use dhall_core::core::Const::*;
 use dhall_core::core::Expr::*;
 use dhall_core::core::{app, pi};
-use dhall_core::core::{bx, normalize, shift, subst, Expr, V, X};
+use dhall_core::core::{bx, shift, subst, Expr, V, X};
+use dhall_normalize::{normalize};
 
 use self::TypeMessage::*;
 
diff --git a/dhall/tests/macros.rs b/dhall/tests/macros.rs
index 777a2f6..7c9d458 100644
--- a/dhall/tests/macros.rs
+++ b/dhall/tests/macros.rs
@@ -92,6 +92,7 @@ macro_rules! make_spec_test {
         fn $name() {
             use dhall::*;
             use dhall_core::*;
+            use dhall_normalize::*;
             use std::thread;
 
             thread::Builder::new()
diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs
index 340cb04..0787862 100644
--- a/dhall_core/src/core.rs
+++ b/dhall_core/src/core.rs
@@ -233,21 +233,21 @@ impl<'i, S, A> From<Builtin> for Expr<'i, S, A> {
 }
 
 impl<'i, S, A> Expr<'i, S, A> {
-    fn bool_lit(&self) -> Option<bool> {
+    pub fn bool_lit(&self) -> Option<bool> {
         match *self {
             Expr::BoolLit(v) => Some(v),
             _ => None,
         }
     }
 
-    fn natural_lit(&self) -> Option<usize> {
+    pub fn natural_lit(&self) -> Option<usize> {
         match *self {
             Expr::NaturalLit(v) => Some(v),
             _ => None,
         }
     }
 
-    fn text_lit(&self) -> Option<String> {
+    pub fn text_lit(&self) -> Option<String> {
         match *self {
             Expr::TextLit(ref t) => Some(t.clone()), // FIXME?
             _ => None,
@@ -630,7 +630,7 @@ fn add_ui(u: usize, i: isize) -> usize {
     }
 }
 
-fn map_record_value<'a, I, K, V, U, F>(it: I, f: F) -> BTreeMap<K, U>
+pub fn map_record_value<'a, I, K, V, U, F>(it: I, f: F) -> BTreeMap<K, U>
 where
     I: IntoIterator<Item = (&'a K, &'a V)>,
     K: Eq + Ord + Copy + 'a,
@@ -921,285 +921,3 @@ where
     map_op2(f, |x| bx(subst(v, e, x)), a, b)
 }
 
-/// 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<'i, S, T, A>(e: &Expr<'i, S, A>) -> Expr<'i, T, A>
-where
-    S: Clone + fmt::Debug,
-    T: Clone + fmt::Debug,
-    A: Clone + fmt::Debug,
-{
-    use crate::BinOp::*;
-    use crate::Builtin::*;
-    use crate::Expr::*;
-    match *e {
-        Const(k) => Const(k),
-        Var(v) => Var(v),
-        Lam(x, ref tA, ref b) => {
-            let tA2 = normalize(tA);
-            let b2 = normalize(b);
-            Lam(x, bx(tA2), bx(b2))
-        }
-        Pi(x, ref tA, ref tB) => {
-            let tA2 = normalize(tA);
-            let tB2 = normalize(tB);
-            pi(x, tA2, tB2)
-        }
-        App(ref f, ref a) => match normalize::<S, T, A>(f) {
-            Lam(x, _A, b) => {
-                // Beta reduce
-                let vx0 = V(x, 0);
-                let a2 = shift::<S, S, A>(1, vx0, a);
-                let b2 = subst::<S, T, A>(vx0, &a2, &b);
-                let b3 = shift::<S, T, A>(-1, vx0, &b2);
-                normalize(&b3)
-            }
-            f2 => match (f2, normalize::<S, T, A>(a)) {
-                // fold/build fusion for `List`
-                (App(box Builtin(ListBuild), _), App(box App(box Builtin(ListFold), _), box e2)) |
-                (App(box Builtin(ListFold), _), App(box App(box Builtin(ListBuild), _), box e2)) |
-
-                // fold/build fusion for `Natural`
-                (Builtin(NaturalBuild), App(box Builtin(NaturalFold), box e2)) |
-                (Builtin(NaturalFold), App(box Builtin(NaturalBuild), box e2)) => normalize(&e2),
-
-            /*
-                App (App (App (App NaturalFold (NaturalLit n0)) _) succ') zero ->
-                    normalize (go n0)
-                  where
-                    go !0 = zero
-                    go !n = App succ' (go (n - 1))
-                App NaturalBuild k
-                    | check     -> NaturalLit n
-                    | otherwise -> App f' a'
-                  where
-                    labeled =
-                        normalize (App (App (App k Natural) "Succ") "Zero")
-
-                    n = go 0 labeled
-                      where
-                        go !m (App (Var "Succ") e') = go (m + 1) e'
-                        go !m (Var "Zero")          = m
-                        go !_  _                    = internalError text
-                    check = go labeled
-                      where
-                        go (App (Var "Succ") e') = go e'
-                        go (Var "Zero")          = True
-                        go  _                    = False
-                        */
-                (Builtin(NaturalIsZero), NaturalLit(n)) => BoolLit(n == 0),
-                (Builtin(NaturalEven), NaturalLit(n)) => BoolLit(n % 2 == 0),
-                (Builtin(NaturalOdd), NaturalLit(n)) => BoolLit(n % 2 != 0),
-                (Builtin(NaturalToInteger), NaturalLit(n)) => IntegerLit(n as isize),
-                (Builtin(NaturalShow), NaturalLit(n)) => TextLit(n.to_string()),
-                (App(f@box Builtin(ListBuild), box t), k) => {
-                        let labeled =
-                            normalize::<_, T, _>(&app(app(app(k.clone(), app(
-                                Builtin(self::Builtin::List), t.clone())), "Cons"), "Nil"));
-
-                        fn list_to_vector<'i, S, A>(v: &mut Vec<Expr<'i, S, A>>, e: Expr<'i, S, A>)
-                            where S: Clone, A: Clone
-                        {
-                            match e {
-                                App(box App(box Var(V("Cons", _)), box x), box e2) => {
-                                    v.push(x);
-                                    list_to_vector(v, e2)
-                                }
-                                Var(V("Nil", _)) => {}
-                                _ => panic!("internalError list_to_vector"),
-                            }
-                        }
-                        fn check<S, A>(e: &Expr<S, A>) -> bool {
-                            match *e {
-                                App(box App(box Var(V("Cons", _)), _), ref e2) => check(e2),
-                                Var(V("Nil", _)) => true,
-                                _ => false,
-                            }
-                        }
-
-                        if check(&labeled) {
-                            let mut v = vec![];
-                            list_to_vector(&mut v, labeled);
-                            ListLit(Some(bx(t)), v)
-                        } else {
-                            app(App(f, bx(t)), k)
-                        }
-                    }
-                (App(box App(box App(box App(box Builtin(ListFold), _), box ListLit(_, xs)), _), cons), nil) => {
-                    let e2: Expr<_, _> = xs.into_iter().rev().fold(nil, |y, ys| // foldr
-                        App(bx(App(cons.clone(), bx(y))), bx(ys))
-                    );
-                    normalize(&e2)
-                }
-                (App(f, x_), ListLit(t, ys)) => match *f {
-                    Builtin(ListLength) =>
-                        NaturalLit(ys.len()),
-                    Builtin(ListHead) =>
-                        normalize(&OptionalLit(t, ys.into_iter().take(1).collect())),
-                    Builtin(ListLast) =>
-                        normalize(&OptionalLit(t, ys.into_iter().last().into_iter().collect())),
-                    Builtin(ListReverse) => {
-                        let mut xs = ys;
-                        xs.reverse();
-                        normalize(&ListLit(t, xs))
-                    }
-                    _ => app(App(f, x_), ListLit(t, ys)),
-                },
-                /*
-                App (App ListIndexed _) (ListLit t xs) ->
-                    normalize (ListLit t' (fmap adapt (Data.Vector.indexed xs)))
-                  where
-                    t' = Record (Data.Map.fromList kts)
-                      where
-                        kts = [ ("index", Natural)
-                              , ("value", t)
-                              ]
-                    adapt (n, x) = RecordLit (Data.Map.fromList kvs)
-                      where
-                        kvs = [ ("index", NaturalLit (fromIntegral n))
-                              , ("value", x)
-                              ]
-            */
-                (App(box App(box App(box App(box Builtin(OptionalFold), _), box OptionalLit(_, xs)), _), just), nothing) => {
-                    let e2: Expr<_, _> = xs.into_iter().fold(nothing, |y, _|
-                        App(just.clone(), bx(y))
-                    );
-                    normalize(&e2)
-                }
-                (App(box Builtin(OptionalBuild), _), App(box App(box Builtin(OptionalFold), _), b)) => {
-                    normalize(&b)
-                }
-                (App(box Builtin(OptionalBuild), a0), g) => {
-                    let e2: Expr<_, _> = app(app(app(g,
-                        App(bx(Builtin(Optional)), a0.clone())),
-                            Lam("x", a0.clone(),
-                                bx(OptionalLit(Some(a0.clone()), vec![Var(V("x", 0))])))),
-                            OptionalLit(Some(a0), vec![]));
-                    normalize(&e2)
-                }
-                (f2, a2) => app(f2, a2),
-            },
-        },
-        Let(f, _, ref r, ref b) => {
-            let r2 = shift::<_, S, _>(1, V(f, 0), r);
-            let b2 = subst(V(f, 0), &r2, b);
-            let b3 = shift::<_, T, _>(-1, V(f, 0), &b2);
-            normalize(&b3)
-        }
-        Annot(ref x, _) => normalize(x),
-        Builtin(v) => Builtin(v),
-        BoolLit(b) => BoolLit(b),
-        BinOp(BoolAnd, ref x, ref y) => with_binop(
-            BoolAnd,
-            Expr::bool_lit,
-            |xn, yn| BoolLit(xn && yn),
-            normalize(x),
-            normalize(y),
-        ),
-        BinOp(BoolOr, ref x, ref y) => with_binop(
-            BoolOr,
-            Expr::bool_lit,
-            |xn, yn| BoolLit(xn || yn),
-            normalize(x),
-            normalize(y),
-        ),
-        BinOp(BoolEQ, ref x, ref y) => with_binop(
-            BoolEQ,
-            Expr::bool_lit,
-            |xn, yn| BoolLit(xn == yn),
-            normalize(x),
-            normalize(y),
-        ),
-        BinOp(BoolNE, ref x, ref y) => with_binop(
-            BoolNE,
-            Expr::bool_lit,
-            |xn, yn| BoolLit(xn != yn),
-            normalize(x),
-            normalize(y),
-        ),
-        BoolIf(ref b, ref t, ref f) => match normalize(b) {
-            BoolLit(true) => normalize(t),
-            BoolLit(false) => normalize(f),
-            b2 => BoolIf(bx(b2), bx(normalize(t)), bx(normalize(f))),
-        },
-        NaturalLit(n) => NaturalLit(n),
-        BinOp(NaturalPlus, ref x, ref y) => with_binop(
-            NaturalPlus,
-            Expr::natural_lit,
-            |xn, yn| NaturalLit(xn + yn),
-            normalize(x),
-            normalize(y),
-        ),
-        BinOp(NaturalTimes, ref x, ref y) => with_binop(
-            NaturalTimes,
-            Expr::natural_lit,
-            |xn, yn| NaturalLit(xn * yn),
-            normalize(x),
-            normalize(y),
-        ),
-        IntegerLit(n) => IntegerLit(n),
-        DoubleLit(n) => DoubleLit(n),
-        TextLit(ref t) => TextLit(t.clone()),
-        BinOp(TextAppend, ref x, ref y) => with_binop(
-            TextAppend,
-            Expr::text_lit,
-            |xt, yt| TextLit(xt + &yt),
-            normalize(x),
-            normalize(y),
-        ),
-        ListLit(ref t, ref es) => {
-            let t2 = t.as_ref().map(|x| x.as_ref()).map(normalize).map(bx);
-            let es2 = es.iter().map(normalize).collect();
-            ListLit(t2, es2)
-        }
-        OptionalLit(ref t, ref es) => {
-            let t2 = t.as_ref().map(|x| x.as_ref()).map(normalize).map(bx);
-            let es2 = es.iter().map(normalize).collect();
-            OptionalLit(t2, es2)
-        }
-        Record(ref kts) => Record(map_record_value(kts, normalize)),
-        RecordLit(ref kvs) => RecordLit(map_record_value(kvs, normalize)),
-        Union(ref kts) => Union(map_record_value(kts, normalize)),
-        UnionLit(k, ref v, ref kvs) => {
-            UnionLit(k, bx(normalize(v)), map_record_value(kvs, normalize))
-        }
-        Merge(ref _x, ref _y, ref _t) => unimplemented!(),
-        Field(ref r, x) => match normalize(r) {
-            RecordLit(kvs) => match kvs.get(x) {
-                Some(r2) => normalize(r2),
-                None => {
-                    Field(bx(RecordLit(map_record_value(&kvs, normalize))), x)
-                }
-            },
-            r2 => Field(bx(r2), x),
-        },
-        Note(_, ref e) => normalize(e),
-        Embed(ref a) => Embed(a.clone()),
-        _ => unimplemented!(),
-    }
-}
-
-fn with_binop<'a, S, A, U, Get, Set>(
-    op: BinOp,
-    get: Get,
-    set: Set,
-    x: Expr<'a, S, A>,
-    y: Expr<'a, S, A>,
-) -> Expr<'a, S, A>
-where
-    Get: Fn(&Expr<'a, S, A>) -> Option<U>,
-    Set: FnOnce(U, U) -> Expr<'a, S, A>,
-{
-    if let (Some(xv), Some(yv)) = (get(&x), get(&y)) {
-        set(xv, yv)
-    } else {
-        Expr::BinOp(op, bx(x), bx(y))
-    }
-}
diff --git a/dhall_normalize/Cargo.toml b/dhall_normalize/Cargo.toml
new file mode 100644
index 0000000..65524ed
--- /dev/null
+++ b/dhall_normalize/Cargo.toml
@@ -0,0 +1,14 @@
+[package]
+name = "dhall_normalize"
+version = "0.1.0"
+authors = ["NanoTech <nanotech@nanotechcorp.net>", "Nadrieril <nadrieril@users.noreply.github.com>"]
+edition = "2018"
+
+[dependencies]
+bytecount = "0.5.1"
+itertools = "0.8.0"
+lalrpop-util = "0.16.3"
+nom = "3.0.0"
+term-painter = "0.2.3"
+pest = { git = "https://github.com/pest-parser/pest" }
+dhall_core = { path = "../dhall_core" }
diff --git a/dhall_normalize/src/lib.rs b/dhall_normalize/src/lib.rs
new file mode 100644
index 0000000..a2f7041
--- /dev/null
+++ b/dhall_normalize/src/lib.rs
@@ -0,0 +1,5 @@
+#![feature(box_patterns)]
+#![feature(trace_macros)]
+
+mod normalize;
+pub use crate::normalize::*;
diff --git a/dhall_normalize/src/normalize.rs b/dhall_normalize/src/normalize.rs
new file mode 100644
index 0000000..1fa5524
--- /dev/null
+++ b/dhall_normalize/src/normalize.rs
@@ -0,0 +1,286 @@
+#![allow(non_snake_case)]
+use std::fmt;
+use dhall_core::core::*;
+
+/// 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<'i, S, T, A>(e: &Expr<'i, S, A>) -> Expr<'i, T, A>
+where
+    S: Clone + fmt::Debug,
+    T: Clone + fmt::Debug,
+    A: Clone + fmt::Debug,
+{
+    use dhall_core::BinOp::*;
+    use dhall_core::Builtin::*;
+    use dhall_core::Expr::*;
+    match *e {
+        Const(k) => Const(k),
+        Var(v) => Var(v),
+        Lam(x, ref tA, ref b) => {
+            let tA2 = normalize(tA);
+            let b2 = normalize(b);
+            Lam(x, bx(tA2), bx(b2))
+        }
+        Pi(x, ref tA, ref tB) => {
+            let tA2 = normalize(tA);
+            let tB2 = normalize(tB);
+            pi(x, tA2, tB2)
+        }
+        App(ref f, ref a) => match normalize::<S, T, A>(f) {
+            Lam(x, _A, b) => {
+                // Beta reduce
+                let vx0 = V(x, 0);
+                let a2 = shift::<S, S, A>(1, vx0, a);
+                let b2 = subst::<S, T, A>(vx0, &a2, &b);
+                let b3 = shift::<S, T, A>(-1, vx0, &b2);
+                normalize(&b3)
+            }
+            f2 => match (f2, normalize::<S, T, A>(a)) {
+                // fold/build fusion for `List`
+                (App(box Builtin(ListBuild), _), App(box App(box Builtin(ListFold), _), box e2)) |
+                (App(box Builtin(ListFold), _), App(box App(box Builtin(ListBuild), _), box e2)) |
+
+                // fold/build fusion for `Natural`
+                (Builtin(NaturalBuild), App(box Builtin(NaturalFold), box e2)) |
+                (Builtin(NaturalFold), App(box Builtin(NaturalBuild), box e2)) => normalize(&e2),
+
+            /*
+                App (App (App (App NaturalFold (NaturalLit n0)) _) succ') zero ->
+                    normalize (go n0)
+                  where
+                    go !0 = zero
+                    go !n = App succ' (go (n - 1))
+                App NaturalBuild k
+                    | check     -> NaturalLit n
+                    | otherwise -> App f' a'
+                  where
+                    labeled =
+                        normalize (App (App (App k Natural) "Succ") "Zero")
+
+                    n = go 0 labeled
+                      where
+                        go !m (App (Var "Succ") e') = go (m + 1) e'
+                        go !m (Var "Zero")          = m
+                        go !_  _                    = internalError text
+                    check = go labeled
+                      where
+                        go (App (Var "Succ") e') = go e'
+                        go (Var "Zero")          = True
+                        go  _                    = False
+                        */
+                (Builtin(NaturalIsZero), NaturalLit(n)) => BoolLit(n == 0),
+                (Builtin(NaturalEven), NaturalLit(n)) => BoolLit(n % 2 == 0),
+                (Builtin(NaturalOdd), NaturalLit(n)) => BoolLit(n % 2 != 0),
+                (Builtin(NaturalToInteger), NaturalLit(n)) => IntegerLit(n as isize),
+                (Builtin(NaturalShow), NaturalLit(n)) => TextLit(n.to_string()),
+                (App(f@box Builtin(ListBuild), box t), k) => {
+                        let labeled =
+                            normalize::<_, T, _>(&app(app(app(k.clone(), app(
+                                Builtin(self::Builtin::List), t.clone())), "Cons"), "Nil"));
+
+                        fn list_to_vector<'i, S, A>(v: &mut Vec<Expr<'i, S, A>>, e: Expr<'i, S, A>)
+                            where S: Clone, A: Clone
+                        {
+                            match e {
+                                App(box App(box Var(V("Cons", _)), box x), box e2) => {
+                                    v.push(x);
+                                    list_to_vector(v, e2)
+                                }
+                                Var(V("Nil", _)) => {}
+                                _ => panic!("internalError list_to_vector"),
+                            }
+                        }
+                        fn check<S, A>(e: &Expr<S, A>) -> bool {
+                            match *e {
+                                App(box App(box Var(V("Cons", _)), _), ref e2) => check(e2),
+                                Var(V("Nil", _)) => true,
+                                _ => false,
+                            }
+                        }
+
+                        if check(&labeled) {
+                            let mut v = vec![];
+                            list_to_vector(&mut v, labeled);
+                            ListLit(Some(bx(t)), v)
+                        } else {
+                            app(App(f, bx(t)), k)
+                        }
+                    }
+                (App(box App(box App(box App(box Builtin(ListFold), _), box ListLit(_, xs)), _), cons), nil) => {
+                    let e2: Expr<_, _> = xs.into_iter().rev().fold(nil, |y, ys| // foldr
+                        App(bx(App(cons.clone(), bx(y))), bx(ys))
+                    );
+                    normalize(&e2)
+                }
+                (App(f, x_), ListLit(t, ys)) => match *f {
+                    Builtin(ListLength) =>
+                        NaturalLit(ys.len()),
+                    Builtin(ListHead) =>
+                        normalize(&OptionalLit(t, ys.into_iter().take(1).collect())),
+                    Builtin(ListLast) =>
+                        normalize(&OptionalLit(t, ys.into_iter().last().into_iter().collect())),
+                    Builtin(ListReverse) => {
+                        let mut xs = ys;
+                        xs.reverse();
+                        normalize(&ListLit(t, xs))
+                    }
+                    _ => app(App(f, x_), ListLit(t, ys)),
+                },
+                /*
+                App (App ListIndexed _) (ListLit t xs) ->
+                    normalize (ListLit t' (fmap adapt (Data.Vector.indexed xs)))
+                  where
+                    t' = Record (Data.Map.fromList kts)
+                      where
+                        kts = [ ("index", Natural)
+                              , ("value", t)
+                              ]
+                    adapt (n, x) = RecordLit (Data.Map.fromList kvs)
+                      where
+                        kvs = [ ("index", NaturalLit (fromIntegral n))
+                              , ("value", x)
+                              ]
+            */
+                (App(box App(box App(box App(box Builtin(OptionalFold), _), box OptionalLit(_, xs)), _), just), nothing) => {
+                    let e2: Expr<_, _> = xs.into_iter().fold(nothing, |y, _|
+                        App(just.clone(), bx(y))
+                    );
+                    normalize(&e2)
+                }
+                (App(box Builtin(OptionalBuild), _), App(box App(box Builtin(OptionalFold), _), b)) => {
+                    normalize(&b)
+                }
+                (App(box Builtin(OptionalBuild), a0), g) => {
+                    let e2: Expr<_, _> = app(app(app(g,
+                        App(bx(Builtin(Optional)), a0.clone())),
+                            Lam("x", a0.clone(),
+                                bx(OptionalLit(Some(a0.clone()), vec![Var(V("x", 0))])))),
+                            OptionalLit(Some(a0), vec![]));
+                    normalize(&e2)
+                }
+                (f2, a2) => app(f2, a2),
+            },
+        },
+        Let(f, _, ref r, ref b) => {
+            let r2 = shift::<_, S, _>(1, V(f, 0), r);
+            let b2 = subst(V(f, 0), &r2, b);
+            let b3 = shift::<_, T, _>(-1, V(f, 0), &b2);
+            normalize(&b3)
+        }
+        Annot(ref x, _) => normalize(x),
+        Builtin(v) => Builtin(v),
+        BoolLit(b) => BoolLit(b),
+        BinOp(BoolAnd, ref x, ref y) => with_binop(
+            BoolAnd,
+            Expr::bool_lit,
+            |xn, yn| BoolLit(xn && yn),
+            normalize(x),
+            normalize(y),
+        ),
+        BinOp(BoolOr, ref x, ref y) => with_binop(
+            BoolOr,
+            Expr::bool_lit,
+            |xn, yn| BoolLit(xn || yn),
+            normalize(x),
+            normalize(y),
+        ),
+        BinOp(BoolEQ, ref x, ref y) => with_binop(
+            BoolEQ,
+            Expr::bool_lit,
+            |xn, yn| BoolLit(xn == yn),
+            normalize(x),
+            normalize(y),
+        ),
+        BinOp(BoolNE, ref x, ref y) => with_binop(
+            BoolNE,
+            Expr::bool_lit,
+            |xn, yn| BoolLit(xn != yn),
+            normalize(x),
+            normalize(y),
+        ),
+        BoolIf(ref b, ref t, ref f) => match normalize(b) {
+            BoolLit(true) => normalize(t),
+            BoolLit(false) => normalize(f),
+            b2 => BoolIf(bx(b2), bx(normalize(t)), bx(normalize(f))),
+        },
+        NaturalLit(n) => NaturalLit(n),
+        BinOp(NaturalPlus, ref x, ref y) => with_binop(
+            NaturalPlus,
+            Expr::natural_lit,
+            |xn, yn| NaturalLit(xn + yn),
+            normalize(x),
+            normalize(y),
+        ),
+        BinOp(NaturalTimes, ref x, ref y) => with_binop(
+            NaturalTimes,
+            Expr::natural_lit,
+            |xn, yn| NaturalLit(xn * yn),
+            normalize(x),
+            normalize(y),
+        ),
+        IntegerLit(n) => IntegerLit(n),
+        DoubleLit(n) => DoubleLit(n),
+        TextLit(ref t) => TextLit(t.clone()),
+        BinOp(TextAppend, ref x, ref y) => with_binop(
+            TextAppend,
+            Expr::text_lit,
+            |xt, yt| TextLit(xt + &yt),
+            normalize(x),
+            normalize(y),
+        ),
+        ListLit(ref t, ref es) => {
+            let t2 = t.as_ref().map(|x| x.as_ref()).map(normalize).map(bx);
+            let es2 = es.iter().map(normalize).collect();
+            ListLit(t2, es2)
+        }
+        OptionalLit(ref t, ref es) => {
+            let t2 = t.as_ref().map(|x| x.as_ref()).map(normalize).map(bx);
+            let es2 = es.iter().map(normalize).collect();
+            OptionalLit(t2, es2)
+        }
+        Record(ref kts) => Record(map_record_value(kts, normalize)),
+        RecordLit(ref kvs) => RecordLit(map_record_value(kvs, normalize)),
+        Union(ref kts) => Union(map_record_value(kts, normalize)),
+        UnionLit(k, ref v, ref kvs) => {
+            UnionLit(k, bx(normalize(v)), map_record_value(kvs, normalize))
+        }
+        Merge(ref _x, ref _y, ref _t) => unimplemented!(),
+        Field(ref r, x) => match normalize(r) {
+            RecordLit(kvs) => match kvs.get(x) {
+                Some(r2) => normalize(r2),
+                None => {
+                    Field(bx(RecordLit(map_record_value(&kvs, normalize))), x)
+                }
+            },
+            r2 => Field(bx(r2), x),
+        },
+        Note(_, ref e) => normalize(e),
+        Embed(ref a) => Embed(a.clone()),
+        _ => unimplemented!(),
+    }
+}
+
+fn with_binop<'a, S, A, U, Get, Set>(
+    op: BinOp,
+    get: Get,
+    set: Set,
+    x: Expr<'a, S, A>,
+    y: Expr<'a, S, A>,
+) -> Expr<'a, S, A>
+where
+    Get: Fn(&Expr<'a, S, A>) -> Option<U>,
+    Set: FnOnce(U, U) -> Expr<'a, S, A>,
+{
+    if let (Some(xv), Some(yv)) = (get(&x), get(&y)) {
+        set(xv, yv)
+    } else {
+        Expr::BinOp(op, bx(x), bx(y))
+    }
+}