1 files changed, 8 insertions, 74 deletions

diff --git a/dhall/src/semantics/core/value_kind.rs b/dhall/src/semantics/core/value_kind.rs
index 36ba068..47df39d 100644
--- a/dhall/src/semantics/core/value_kind.rs
+++ b/dhall/src/semantics/core/value_kind.rs
@@ -1,10 +1,9 @@
 use std::collections::HashMap;
 
-use crate::semantics::core::value::{ToExprOptions, Value};
+use crate::semantics::core::value::Value;
 use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
-use crate::semantics::phase::typecheck::rc;
 use crate::semantics::phase::{Normalized, NormalizedExpr};
-use crate::syntax;
+use crate::semantics::to_expr;
 use crate::syntax::{
     Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label,
     NaiveDouble, Natural,
@@ -52,77 +51,12 @@ impl ValueKind {
         Value::from_kind_and_type(self, t)
     }
 
-    pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
-        match self {
-            ValueKind::Lam(x, t, e) => rc(ExprF::Lam(
-                x.to_label_maybe_alpha(opts.alpha),
-                t.to_expr(opts),
-                e.to_expr(opts),
-            )),
-            ValueKind::AppliedBuiltin(b, args) => args
-                .iter()
-                .map(|v| v.to_expr(opts))
-                .fold(rc(ExprF::Builtin(*b)), |acc, v| rc(ExprF::App(acc, v))),
-            ValueKind::Pi(x, t, e) => rc(ExprF::Pi(
-                x.to_label_maybe_alpha(opts.alpha),
-                t.to_expr(opts),
-                e.to_expr(opts),
-            )),
-            ValueKind::Var(v) => rc(ExprF::Var(v.to_var(opts.alpha))),
-            ValueKind::Const(c) => rc(ExprF::Const(*c)),
-            ValueKind::BoolLit(b) => rc(ExprF::BoolLit(*b)),
-            ValueKind::NaturalLit(n) => rc(ExprF::NaturalLit(*n)),
-            ValueKind::IntegerLit(n) => rc(ExprF::IntegerLit(*n)),
-            ValueKind::DoubleLit(n) => rc(ExprF::DoubleLit(*n)),
-            ValueKind::EmptyOptionalLit(n) => rc(ExprF::App(
-                rc(ExprF::Builtin(Builtin::OptionalNone)),
-                n.to_expr(opts),
-            )),
-            ValueKind::NEOptionalLit(n) => rc(ExprF::SomeLit(n.to_expr(opts))),
-            ValueKind::EmptyListLit(n) => rc(ExprF::EmptyListLit(rc(
-                ExprF::App(rc(ExprF::Builtin(Builtin::List)), n.to_expr(opts)),
-            ))),
-            ValueKind::NEListLit(elts) => rc(ExprF::NEListLit(
-                elts.iter().map(|n| n.to_expr(opts)).collect(),
-            )),
-            ValueKind::RecordLit(kvs) => rc(ExprF::RecordLit(
-                kvs.iter()
-                    .map(|(k, v)| (k.clone(), v.to_expr(opts)))
-                    .collect(),
-            )),
-            ValueKind::RecordType(kts) => rc(ExprF::RecordType(
-                kts.iter()
-                    .map(|(k, v)| (k.clone(), v.to_expr(opts)))
-                    .collect(),
-            )),
-            ValueKind::UnionType(kts) => rc(ExprF::UnionType(
-                kts.iter()
-                    .map(|(k, v)| {
-                        (k.clone(), v.as_ref().map(|v| v.to_expr(opts)))
-                    })
-                    .collect(),
-            )),
-            ValueKind::UnionConstructor(l, kts) => rc(ExprF::Field(
-                ValueKind::UnionType(kts.clone()).to_expr(opts),
-                l.clone(),
-            )),
-            ValueKind::UnionLit(l, v, kts) => rc(ExprF::App(
-                ValueKind::UnionConstructor(l.clone(), kts.clone())
-                    .to_expr(opts),
-                v.to_expr(opts),
-            )),
-            ValueKind::TextLit(elts) => rc(ExprF::TextLit(
-                elts.iter()
-                    .map(|contents| contents.map_ref(|e| e.to_expr(opts)))
-                    .collect(),
-            )),
-            ValueKind::Equivalence(x, y) => rc(ExprF::BinOp(
-                syntax::BinOp::Equivalence,
-                x.to_expr(opts),
-                y.to_expr(opts),
-            )),
-            ValueKind::PartialExpr(e) => rc(e.map_ref(|v| v.to_expr(opts))),
-        }
+    /// Converts a value back to the corresponding AST expression.
+    pub(crate) fn to_expr(
+        &self,
+        opts: to_expr::ToExprOptions,
+    ) -> NormalizedExpr {
+        to_expr::kind_to_expr(self, opts)
     }
 
     pub(crate) fn normalize_mut(&mut self) {