Start separating normalized values from syntactic expressions

2 files changed, 179 insertions, 121 deletions

diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs
index 544df6e..c85b962 100644
--- a/dhall/src/lib.rs
+++ b/dhall/src/lib.rs
@@ -3,6 +3,7 @@
 #![feature(slice_patterns)]
 #![feature(label_break_value)]
 #![feature(non_exhaustive)]
+#![feature(bind_by_move_pattern_guards)]
 #![cfg_attr(test, feature(custom_inner_attributes))]
 #![allow(
     clippy::type_complexity,
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 7a9ca2f..90c6841 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -216,6 +216,39 @@ where
     Continue(ExprF::App(ret, rest))
 }
 
+#[derive(Debug, Clone, PartialEq, Eq)]
+enum Value {
+    Expr(SubExpr<X, X>),
+    Lam(
+        Label,
+        SubExpr<X, Normalized<'static>>,
+        SubExpr<X, Normalized<'static>>,
+    ),
+    // App(
+    //     SubExpr<X, Normalized<'static>>,
+    //     Vec<SubExpr<X, Normalized<'static>>>,
+    // ),
+}
+
+impl Value {
+    fn into_expr(self, ctx: &NormalizationContext) -> SubExpr<X, X> {
+        match self {
+            Value::Expr(e) => e,
+            Value::Lam(x, t, e) => rc(ExprF::Lam(
+                x.clone(),
+                normalize_value(ctx, t).into_expr(ctx),
+                normalize_value(&ctx.skip(&x), e).into_expr(&ctx.skip(&x)),
+            )),
+            // Value::App(f, args) => rc(ExprF::App(
+            //     normalize_value(ctx, f).into_expr(ctx),
+            //     args.into_iter()
+            //         .map(|e| normalize_value(ctx, e).into_expr(ctx))
+            //         .collect(),
+            // )),
+        }
+    }
+}
+
 #[derive(Debug, Clone)]
 enum EnvItem {
     Expr(SubExpr<X, X>),
@@ -268,138 +301,161 @@ enum WhatNext<'a, N, E> {
     DoneAsIs,
 }
 
+fn reval(expr: SubExpr<X, X>) -> Value {
+    match expr.as_ref() {
+        ExprF::Lam(x, t, e) => {
+            Value::Lam(x.clone(), t.embed_absurd(), e.embed_absurd())
+        }
+        _ => Value::Expr(expr),
+    }
+}
+
 fn normalize_value(
     ctx: &NormalizationContext,
     expr: SubExpr<X, Normalized<'static>>,
-) -> SubExpr<X, X> {
+) -> Value {
     use dhall_core::BinOp::*;
     use dhall_core::ExprF::*;
 
-    match expr.as_ref() {
+    let e = match expr.as_ref() {
         Let(x, _, r, b) => {
-            let r = normalize_value(ctx, r.clone());
-            normalize_value(&ctx.insert(x, r.clone()), b.clone())
-        }
-        e => {
-            // Recursively normalize all subexpressions
-            let expr: ExprF<Expr<X, X>, Label, X, Normalized<'static>> = e
-                .map_ref_with_special_handling_of_binders(
-                    |e| normalize_value(ctx, e.clone()).unroll(),
-                    |x, e| normalize_value(&ctx.skip(x), e.clone()).unroll(),
-                    X::clone,
-                    Normalized::clone,
-                    Label::clone,
-                );
+            let r = normalize_value(ctx, r.clone()).into_expr(ctx);
+            return normalize_value(&ctx.insert(x, r.clone()), b.clone());
+        }
+        Lam(x, t, e) => return Value::Lam(x.clone(), t.clone(), e.clone()),
+        e => e,
+    };
 
-            use WhatNext::*;
-            let what_next = match &expr {
-                Let(_, _, _, _) => unreachable!(),
-                Embed(e) => DoneRefSub(&e.0),
-                Var(v) => DoneSub(ctx.lookup(v)),
-                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 b2 = subst_shift(vx0, &a.roll(), &b);
-                    Continue(App(b2, iter.map(ExprF::roll).collect()))
-                }
-                App(UnionConstructor(l, kts), args) => {
-                    let mut iter = args.iter();
-                    // We know args is nonempty
-                    let a = iter.next().unwrap();
-                    let e = rc(UnionLit(l.clone(), rc(a.clone()), kts.clone()));
-                    Continue(App(e, iter.map(ExprF::roll).collect()))
-                }
-                BoolIf(BoolLit(true), t, _) => DoneRef(t),
-                BoolIf(BoolLit(false), _, f) => DoneRef(f),
-                // TODO: interpolation
-                // TextLit(t) =>
-                OldOptionalLit(None, t) => Done(EmptyOptionalLit(t.roll())),
-                OldOptionalLit(Some(x), _) => Done(NEOptionalLit(x.roll())),
-                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))
-                }
-                BinOp(NaturalTimes, NaturalLit(x), NaturalLit(y)) => {
-                    Done(NaturalLit(x * y))
-                }
-                BinOp(TextAppend, TextLit(x), TextLit(y)) => {
-                    Done(TextLit(x + y))
-                }
-                BinOp(ListAppend, EmptyListLit(_), y) => DoneRef(y),
-                BinOp(ListAppend, x, EmptyListLit(_)) => DoneRef(x),
-                BinOp(ListAppend, NEListLit(xs), NEListLit(ys)) => {
-                    let xs = xs.iter().cloned();
-                    let ys = ys.iter().cloned();
-                    Done(NEListLit(xs.chain(ys).collect()))
-                }
-                Merge(RecordLit(handlers), UnionLit(l, v, _), _) => {
-                    match handlers.get(&l) {
-                        Some(h) => Continue(App(h.clone(), vec![v.clone()])),
-                        None => DoneAsIs,
-                    }
-                }
-                Merge(RecordLit(handlers), UnionConstructor(l, _), _) => {
-                    match handlers.get(&l) {
-                        Some(h) => DoneRefSub(h),
-                        None => DoneAsIs,
-                    }
-                }
-                Field(RecordLit(kvs), l) => match kvs.get(&l) {
-                    Some(r) => DoneRefSub(r),
-                    None => DoneAsIs,
-                },
-                Field(UnionType(kts), l) => {
-                    Done(UnionConstructor(l.clone(), kts.clone()))
-                }
-                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,
-            };
+    // Recursively normalize all subexpressions
+    let expr: ExprF<Value, Label, X, Normalized<'static>> = e
+        .map_ref_with_special_handling_of_binders(
+            |e| normalize_value(ctx, e.clone()),
+            |x, e| normalize_value(&ctx.skip(x), e.clone()),
+            X::clone,
+            Normalized::clone,
+            Label::clone,
+        );
 
-            match what_next {
-                Continue(e) => normalize_value(ctx, e.embed_absurd().roll()),
-                Done(e) => e.roll(),
-                DoneRef(e) => e.roll(),
-                DoneSub(e) => e,
-                DoneRefSub(e) => e.clone(),
-                DoneAsIs => rc(expr.map_ref_simple(ExprF::roll).map_ref(
-                    SubExpr::clone,
-                    X::clone,
-                    |_| unreachable!(),
-                    Label::clone,
-                )),
+    let expr = match expr {
+        App(v, args) if args.is_empty() => return v,
+        App(Value::Lam(x, _, b), args) => {
+            let mut iter = args.into_iter();
+            // We know args is nonempty
+            let a = iter.next().unwrap();
+            // Beta reduce
+            let ctx2 = ctx.insert(&x, a.into_expr(ctx));
+            let b2 = normalize_value(&ctx2, b).into_expr(&ctx2);
+            return normalize_value(
+                ctx,
+                App(b2, iter.map(|val| val.into_expr(ctx)).collect())
+                    .embed_absurd()
+                    .roll(),
+            );
+        }
+        expr => expr,
+    };
+
+    let expr: ExprF<Expr<X, X>, Label, X, Normalized<'static>> = expr
+        .map_ref_with_special_handling_of_binders(
+            |e| e.clone().into_expr(ctx).unroll(),
+            |x, e| e.clone().into_expr(&ctx.skip(x)).unroll(),
+            X::clone,
+            Normalized::clone,
+            Label::clone,
+        );
+
+    use WhatNext::*;
+    let what_next = match &expr {
+        Embed(e) => DoneRefSub(&e.0),
+        Var(v) => DoneSub(ctx.lookup(v)),
+        Annot(x, _) => DoneRef(x),
+        Note(_, e) => DoneRef(e),
+        App(_, args) if args.is_empty() => unreachable!(),
+        Let(_, _, _, _) => unreachable!(),
+        Lam(_, _, _) => unreachable!(),
+        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(_, _, _), _) => unreachable!(),
+        App(UnionConstructor(l, kts), args) => {
+            let mut iter = args.iter();
+            // We know args is nonempty
+            let a = iter.next().unwrap();
+            let e = rc(UnionLit(l.clone(), rc(a.clone()), kts.clone()));
+            Continue(App(e, iter.map(ExprF::roll).collect()))
+        }
+        BoolIf(BoolLit(true), t, _) => DoneRef(t),
+        BoolIf(BoolLit(false), _, f) => DoneRef(f),
+        // TODO: interpolation
+        // TextLit(t) =>
+        OldOptionalLit(None, t) => Done(EmptyOptionalLit(t.roll())),
+        OldOptionalLit(Some(x), _) => Done(NEOptionalLit(x.roll())),
+        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))
+        }
+        BinOp(NaturalTimes, NaturalLit(x), NaturalLit(y)) => {
+            Done(NaturalLit(x * y))
+        }
+        BinOp(TextAppend, TextLit(x), TextLit(y)) => Done(TextLit(x + y)),
+        BinOp(ListAppend, EmptyListLit(_), y) => DoneRef(y),
+        BinOp(ListAppend, x, EmptyListLit(_)) => DoneRef(x),
+        BinOp(ListAppend, NEListLit(xs), NEListLit(ys)) => {
+            let xs = xs.iter().cloned();
+            let ys = ys.iter().cloned();
+            Done(NEListLit(xs.chain(ys).collect()))
+        }
+        Merge(RecordLit(handlers), UnionLit(l, v, _), _) => {
+            match handlers.get(&l) {
+                Some(h) => Continue(App(h.clone(), vec![v.clone()])),
+                None => DoneAsIs,
+            }
+        }
+        Merge(RecordLit(handlers), UnionConstructor(l, _), _) => {
+            match handlers.get(&l) {
+                Some(h) => DoneRefSub(h),
+                None => DoneAsIs,
             }
         }
+        Field(RecordLit(kvs), l) => match kvs.get(&l) {
+            Some(r) => DoneRefSub(r),
+            None => DoneAsIs,
+        },
+        Field(UnionType(kts), l) => {
+            Done(UnionConstructor(l.clone(), kts.clone()))
+        }
+        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_value(ctx, e.embed_absurd().roll()),
+        Done(e) => reval(e.roll()),
+        DoneRef(e) => reval(e.roll()),
+        DoneSub(e) => reval(e),
+        DoneRefSub(e) => reval(e.clone()),
+        DoneAsIs => reval(rc(expr.map_ref_simple(ExprF::roll).map_ref(
+            SubExpr::clone,
+            X::clone,
+            |_| unreachable!(),
+            Label::clone,
+        ))),
     }
 }
 
@@ -414,6 +470,7 @@ fn normalize_value(
 ///
 fn normalize(e: SubExpr<X, Normalized<'static>>) -> SubExpr<X, X> {
     normalize_value(&NormalizationContext::new(), e)
+        .into_expr(&NormalizationContext::new())
 }
 
 #[cfg(test)]