Cleanup conversion of `Value` to `Expr`

3 files changed, 66 insertions, 102 deletions

diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index 49e30cd..3cccb1d 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -44,6 +44,15 @@ struct ValueInternal {
 #[derive(Clone)]
 pub(crate) struct Value(Rc<RefCell<ValueInternal>>);
 
+#[derive(Copy, Clone)]
+/// Controls conversion from `Value` to `Expr`
+pub(crate) struct ToExprOptions {
+    /// Whether to convert all variables to `_`
+    pub(crate) alpha: bool,
+    /// Whether to normalize before converting
+    pub(crate) normalize: bool,
+}
+
 impl ValueInternal {
     fn into_value(self) -> Value {
         Value(Rc::new(RefCell::new(self)))
@@ -158,20 +167,12 @@ impl Value {
         self.normalize_whnf();
         self.as_valuef()
     }
-    /// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut
-    /// panics.
-    pub(crate) fn as_nf(&self) -> Ref<ValueF> {
-        self.normalize_nf();
-        self.as_valuef()
-    }
 
-    // TODO: rename `normalize_to_expr`
-    pub(crate) fn to_expr(&self) -> NormalizedExpr {
-        self.as_whnf().normalize_to_expr()
-    }
-    // TODO: rename `normalize_to_expr_maybe_alpha`
-    pub(crate) fn to_expr_alpha(&self) -> NormalizedExpr {
-        self.as_whnf().normalize_to_expr_maybe_alpha(true)
+    pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
+        if opts.normalize {
+            self.normalize_whnf();
+        }
+        self.as_valuef().to_expr(opts)
     }
     pub(crate) fn to_whnf_ignore_type(&self) -> ValueF {
         self.as_whnf().clone()
@@ -223,13 +224,6 @@ impl Value {
         }
     }
 
-    pub(crate) fn normalize_to_expr_maybe_alpha(
-        &self,
-        alpha: bool,
-    ) -> NormalizedExpr {
-        self.as_nf().normalize_to_expr_maybe_alpha(alpha)
-    }
-
     pub(crate) fn app(&self, v: Value) -> Value {
         let body_t = match &*self.get_type_not_sort().as_whnf() {
             ValueF::Pi(x, t, e) => {
diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs
index 959f299..7ecec86 100644
--- a/dhall/src/core/valuef.rs
+++ b/dhall/src/core/valuef.rs
@@ -5,7 +5,7 @@ use dhall_syntax::{
     NaiveDouble, Natural,
 };
 
-use crate::core::value::Value;
+use crate::core::value::{ToExprOptions, Value};
 use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
 use crate::phase::{Normalized, NormalizedExpr};
 
@@ -51,38 +51,23 @@ impl ValueF {
         Value::from_valuef_and_type(self, t)
     }
 
-    /// Convert the value to a fully normalized syntactic expression
-    pub(crate) fn normalize_to_expr(&self) -> NormalizedExpr {
-        self.normalize_to_expr_maybe_alpha(false)
-    }
-    /// Convert the value to a fully normalized syntactic expression. Also alpha-normalize
-    /// if alpha is `true`
-    pub(crate) fn normalize_to_expr_maybe_alpha(
-        &self,
-        alpha: bool,
-    ) -> NormalizedExpr {
+    pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
         match self {
             ValueF::Lam(x, t, e) => rc(ExprF::Lam(
-                x.to_label_maybe_alpha(alpha),
-                t.normalize_to_expr_maybe_alpha(alpha),
-                e.normalize_to_expr_maybe_alpha(alpha),
+                x.to_label_maybe_alpha(opts.alpha),
+                t.to_expr(opts),
+                e.to_expr(opts),
             )),
-            ValueF::AppliedBuiltin(b, args) => {
-                let mut e = rc(ExprF::Builtin(*b));
-                for v in args {
-                    e = rc(ExprF::App(
-                        e,
-                        v.normalize_to_expr_maybe_alpha(alpha),
-                    ));
-                }
-                e
-            }
+            ValueF::AppliedBuiltin(b, args) => args
+                .iter()
+                .map(|v| v.to_expr(opts))
+                .fold(rc(ExprF::Builtin(*b)), |acc, v| rc(ExprF::App(acc, v))),
             ValueF::Pi(x, t, e) => rc(ExprF::Pi(
-                x.to_label_maybe_alpha(alpha),
-                t.normalize_to_expr_maybe_alpha(alpha),
-                e.normalize_to_expr_maybe_alpha(alpha),
+                x.to_label_maybe_alpha(opts.alpha),
+                t.to_expr(opts),
+                e.to_expr(opts),
             )),
-            ValueF::Var(v) => rc(ExprF::Var(v.to_var(alpha))),
+            ValueF::Var(v) => rc(ExprF::Var(v.to_var(opts.alpha))),
             ValueF::Const(c) => rc(ExprF::Const(*c)),
             ValueF::BoolLit(b) => rc(ExprF::BoolLit(*b)),
             ValueF::NaturalLit(n) => rc(ExprF::NaturalLit(*n)),
@@ -90,73 +75,47 @@ impl ValueF {
             ValueF::DoubleLit(n) => rc(ExprF::DoubleLit(*n)),
             ValueF::EmptyOptionalLit(n) => rc(ExprF::App(
                 rc(ExprF::Builtin(Builtin::OptionalNone)),
-                n.normalize_to_expr_maybe_alpha(alpha),
+                n.to_expr(opts),
             )),
-            ValueF::NEOptionalLit(n) => {
-                rc(ExprF::SomeLit(n.normalize_to_expr_maybe_alpha(alpha)))
-            }
+            ValueF::NEOptionalLit(n) => rc(ExprF::SomeLit(n.to_expr(opts))),
             ValueF::EmptyListLit(n) => rc(ExprF::EmptyListLit(rc(ExprF::App(
                 rc(ExprF::Builtin(Builtin::List)),
-                n.normalize_to_expr_maybe_alpha(alpha),
+                n.to_expr(opts),
             )))),
             ValueF::NEListLit(elts) => rc(ExprF::NEListLit(
-                elts.iter()
-                    .map(|n| n.normalize_to_expr_maybe_alpha(alpha))
-                    .collect(),
+                elts.iter().map(|n| n.to_expr(opts)).collect(),
             )),
             ValueF::RecordLit(kvs) => rc(ExprF::RecordLit(
                 kvs.iter()
-                    .map(|(k, v)| {
-                        (k.clone(), v.normalize_to_expr_maybe_alpha(alpha))
-                    })
+                    .map(|(k, v)| (k.clone(), v.to_expr(opts)))
                     .collect(),
             )),
             ValueF::RecordType(kts) => rc(ExprF::RecordType(
                 kts.iter()
-                    .map(|(k, v)| {
-                        (k.clone(), v.normalize_to_expr_maybe_alpha(alpha))
-                    })
+                    .map(|(k, v)| (k.clone(), v.to_expr(opts)))
                     .collect(),
             )),
             ValueF::UnionType(kts) => rc(ExprF::UnionType(
                 kts.iter()
                     .map(|(k, v)| {
-                        (
-                            k.clone(),
-                            v.as_ref().map(|v| {
-                                v.normalize_to_expr_maybe_alpha(alpha)
-                            }),
-                        )
+                        (k.clone(), v.as_ref().map(|v| v.to_expr(opts)))
                     })
                     .collect(),
             )),
-            ValueF::UnionConstructor(l, kts) => {
-                let kts = kts
-                    .iter()
-                    .map(|(k, v)| {
-                        (
-                            k.clone(),
-                            v.as_ref().map(|v| {
-                                v.normalize_to_expr_maybe_alpha(alpha)
-                            }),
-                        )
-                    })
-                    .collect();
-                rc(ExprF::Field(rc(ExprF::UnionType(kts)), l.clone()))
-            }
+            ValueF::UnionConstructor(l, kts) => rc(ExprF::Field(
+                ValueF::UnionType(kts.clone()).to_expr(opts),
+                l.clone(),
+            )),
             ValueF::UnionLit(l, v, kts) => rc(ExprF::App(
-                ValueF::UnionConstructor(l.clone(), kts.clone())
-                    .normalize_to_expr_maybe_alpha(alpha),
-                v.normalize_to_expr_maybe_alpha(alpha),
+                ValueF::UnionConstructor(l.clone(), kts.clone()).to_expr(opts),
+                v.to_expr(opts),
             )),
             ValueF::TextLit(elts) => {
                 use InterpolatedTextContents::{Expr, Text};
                 rc(ExprF::TextLit(
                     elts.iter()
                         .map(|contents| match contents {
-                            Expr(e) => {
-                                Expr(e.normalize_to_expr_maybe_alpha(alpha))
-                            }
+                            Expr(e) => Expr(e.to_expr(opts)),
                             Text(s) => Text(s.clone()),
                         })
                         .collect(),
@@ -164,12 +123,10 @@ impl ValueF {
             }
             ValueF::Equivalence(x, y) => rc(ExprF::BinOp(
                 dhall_syntax::BinOp::Equivalence,
-                x.normalize_to_expr_maybe_alpha(alpha),
-                y.normalize_to_expr_maybe_alpha(alpha),
+                x.to_expr(opts),
+                y.to_expr(opts),
             )),
-            ValueF::PartialExpr(e) => {
-                rc(e.map_ref(|v| v.normalize_to_expr_maybe_alpha(alpha)))
-            }
+            ValueF::PartialExpr(e) => rc(e.map_ref(|v| v.to_expr(opts))),
         }
     }
 
diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs
index ecc9213..2c5505c 100644
--- a/dhall/src/phase/mod.rs
+++ b/dhall/src/phase/mod.rs
@@ -3,7 +3,7 @@ use std::path::Path;
 
 use dhall_syntax::{Builtin, Const, Expr};
 
-use crate::core::value::Value;
+use crate::core::value::{ToExprOptions, Value};
 use crate::core::valuef::ValueF;
 use crate::core::var::{AlphaVar, Shift, Subst};
 use crate::error::{EncodeError, Error, ImportError, TypeError};
@@ -71,7 +71,8 @@ impl Resolved {
         Ok(typecheck::typecheck(self.0)?.into_typed())
     }
     pub fn typecheck_with(self, ty: &Typed) -> Result<Typed, TypeError> {
-        Ok(typecheck::typecheck_with(self.0, ty.to_expr())?.into_typed())
+        Ok(typecheck::typecheck_with(self.0, ty.normalize_to_expr())?
+            .into_typed())
     }
 }
 
@@ -102,11 +103,23 @@ impl Typed {
         Typed::from_const(Const::Type)
     }
 
-    pub fn to_expr(&self) -> NormalizedExpr {
-        self.0.to_expr()
-    }
-    pub(crate) fn to_expr_alpha(&self) -> NormalizedExpr {
-        self.0.to_expr_alpha()
+    pub(crate) fn to_expr(&self) -> NormalizedExpr {
+        self.0.to_expr(ToExprOptions {
+            alpha: false,
+            normalize: false,
+        })
+    }
+    pub fn normalize_to_expr(&self) -> NormalizedExpr {
+        self.0.to_expr(ToExprOptions {
+            alpha: false,
+            normalize: true,
+        })
+    }
+    pub(crate) fn normalize_to_expr_alpha(&self) -> NormalizedExpr {
+        self.0.to_expr(ToExprOptions {
+            alpha: true,
+            normalize: true,
+        })
     }
     pub(crate) fn to_value(&self) -> Value {
         self.0.clone()
@@ -163,10 +176,10 @@ impl Normalized {
     }
 
     pub(crate) fn to_expr(&self) -> NormalizedExpr {
-        self.0.to_expr()
+        self.0.normalize_to_expr()
     }
     pub(crate) fn to_expr_alpha(&self) -> NormalizedExpr {
-        self.0.to_expr_alpha()
+        self.0.normalize_to_expr_alpha()
     }
     pub(crate) fn into_typed(self) -> Typed {
         self.0