Move builtins-related code to its own module

8 files changed, 553 insertions, 568 deletions

diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs
new file mode 100644
index 0000000..58cf0d6
--- /dev/null
+++ b/dhall/src/semantics/builtins.rs
@@ -0,0 +1,511 @@
+use crate::semantics::phase::Normalized;
+use crate::semantics::{type_with, NzEnv, Value, ValueKind};
+use crate::syntax::Const::Type;
+use crate::syntax::{
+    self, Builtin, Const, Expr, ExprKind, InterpolatedText,
+    InterpolatedTextContents, Label, NaiveDouble, Span, UnspannedExpr, V,
+};
+use std::collections::HashMap;
+use std::convert::TryInto;
+
+pub(crate) fn rc<E>(x: UnspannedExpr<E>) -> Expr<E> {
+    Expr::new(x, Span::Artificial)
+}
+
+// Ad-hoc macro to help construct the types of builtins
+macro_rules! make_type {
+    (Type) => { rc(ExprKind::Const(Const::Type)) };
+    (Bool) => { rc(ExprKind::Builtin(Builtin::Bool)) };
+    (Natural) => { rc(ExprKind::Builtin(Builtin::Natural)) };
+    (Integer) => { rc(ExprKind::Builtin(Builtin::Integer)) };
+    (Double) => { rc(ExprKind::Builtin(Builtin::Double)) };
+    (Text) => { rc(ExprKind::Builtin(Builtin::Text)) };
+    ($var:ident) => {
+        rc(ExprKind::Var(V(stringify!($var).into(), 0)))
+    };
+    (Optional $ty:ident) => {
+        rc(ExprKind::App(
+            rc(ExprKind::Builtin(Builtin::Optional)),
+            make_type!($ty)
+        ))
+    };
+    (List $($rest:tt)*) => {
+        rc(ExprKind::App(
+            rc(ExprKind::Builtin(Builtin::List)),
+            make_type!($($rest)*)
+        ))
+    };
+    ({ $($label:ident : $ty:ident),* }) => {{
+        let mut kts = syntax::map::DupTreeMap::new();
+        $(
+            kts.insert(
+                Label::from(stringify!($label)),
+                make_type!($ty),
+            );
+        )*
+        rc(ExprKind::RecordType(kts))
+    }};
+    ($ty:ident -> $($rest:tt)*) => {
+        rc(ExprKind::Pi(
+            "_".into(),
+            make_type!($ty),
+            make_type!($($rest)*)
+        ))
+    };
+    (($($arg:tt)*) -> $($rest:tt)*) => {
+        rc(ExprKind::Pi(
+            "_".into(),
+            make_type!($($arg)*),
+            make_type!($($rest)*)
+        ))
+    };
+    (forall ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => {
+        rc(ExprKind::Pi(
+            stringify!($var).into(),
+            make_type!($($ty)*),
+            make_type!($($rest)*)
+        ))
+    };
+}
+
+pub(crate) fn type_of_builtin<E>(b: Builtin) -> Expr<E> {
+    use Builtin::*;
+    match b {
+        Bool | Natural | Integer | Double | Text => make_type!(Type),
+        List | Optional => make_type!(
+            Type -> Type
+        ),
+
+        NaturalFold => make_type!(
+            Natural ->
+            forall (natural: Type) ->
+            forall (succ: natural -> natural) ->
+            forall (zero: natural) ->
+            natural
+        ),
+        NaturalBuild => make_type!(
+            (forall (natural: Type) ->
+                forall (succ: natural -> natural) ->
+                forall (zero: natural) ->
+                natural) ->
+            Natural
+        ),
+        NaturalIsZero | NaturalEven | NaturalOdd => make_type!(
+            Natural -> Bool
+        ),
+        NaturalToInteger => make_type!(Natural -> Integer),
+        NaturalShow => make_type!(Natural -> Text),
+        NaturalSubtract => make_type!(Natural -> Natural -> Natural),
+
+        IntegerToDouble => make_type!(Integer -> Double),
+        IntegerShow => make_type!(Integer -> Text),
+        IntegerNegate => make_type!(Integer -> Integer),
+        IntegerClamp => make_type!(Integer -> Natural),
+
+        DoubleShow => make_type!(Double -> Text),
+        TextShow => make_type!(Text -> Text),
+
+        ListBuild => make_type!(
+            forall (a: Type) ->
+            (forall (list: Type) ->
+                forall (cons: a -> list -> list) ->
+                forall (nil: list) ->
+                list) ->
+            List a
+        ),
+        ListFold => make_type!(
+            forall (a: Type) ->
+            (List a) ->
+            forall (list: Type) ->
+            forall (cons: a -> list -> list) ->
+            forall (nil: list) ->
+            list
+        ),
+        ListLength => make_type!(forall (a: Type) -> (List a) -> Natural),
+        ListHead | ListLast => {
+            make_type!(forall (a: Type) -> (List a) -> Optional a)
+        }
+        ListIndexed => make_type!(
+            forall (a: Type) ->
+            (List a) ->
+            List { index: Natural, value: a }
+        ),
+        ListReverse => make_type!(
+            forall (a: Type) -> (List a) -> List a
+        ),
+
+        OptionalBuild => make_type!(
+            forall (a: Type) ->
+            (forall (optional: Type) ->
+                forall (just: a -> optional) ->
+                forall (nothing: optional) ->
+                optional) ->
+            Optional a
+        ),
+        OptionalFold => make_type!(
+            forall (a: Type) ->
+            (Optional a) ->
+            forall (optional: Type) ->
+            forall (just: a -> optional) ->
+            forall (nothing: optional) ->
+            optional
+        ),
+        OptionalNone => make_type!(
+            forall (A: Type) -> Optional A
+        ),
+    }
+}
+
+// Ad-hoc macro to help construct closures
+macro_rules! make_closure {
+    (var($var:ident)) => {{
+        rc(ExprKind::Var(syntax::V(
+            Label::from(stringify!($var)).into(),
+            0
+        )))
+    }};
+    (λ($var:tt : $($ty:tt)*) -> $($body:tt)*) => {{
+        let var = Label::from(stringify!($var));
+        let ty = make_closure!($($ty)*);
+        let body = make_closure!($($body)*);
+        rc(ExprKind::Lam(var, ty, body))
+    }};
+    (Type) => {
+        rc(ExprKind::Const(Type))
+    };
+    (Natural) => {
+        rc(ExprKind::Builtin(Builtin::Natural))
+    };
+    (List $($ty:tt)*) => {{
+        let ty = make_closure!($($ty)*);
+        rc(ExprKind::App(
+            rc(ExprKind::Builtin(Builtin::List)),
+            ty
+        ))
+    }};
+    (Some($($v:tt)*)) => {
+        rc(ExprKind::SomeLit(
+            make_closure!($($v)*)
+        ))
+    };
+    (1 + $($v:tt)*) => {
+        rc(ExprKind::BinOp(
+            syntax::BinOp::NaturalPlus,
+            make_closure!($($v)*),
+            rc(ExprKind::NaturalLit(1))
+        ))
+    };
+    ([ $($head:tt)* ] # $($tail:tt)*) => {{
+        let head = make_closure!($($head)*);
+        let tail = make_closure!($($tail)*);
+        rc(ExprKind::BinOp(
+            syntax::BinOp::ListAppend,
+            rc(ExprKind::NEListLit(vec![head])),
+            tail,
+        ))
+    }};
+}
+
+#[allow(clippy::cognitive_complexity)]
+pub(crate) fn apply_builtin(
+    b: Builtin,
+    args: Vec<Value>,
+    ty: &Value,
+    types: Vec<Value>,
+    env: NzEnv,
+) -> ValueKind<Value> {
+    use syntax::Builtin::*;
+    use ValueKind::*;
+
+    // Small helper enum
+    enum Ret<'a> {
+        ValueKind(ValueKind<Value>),
+        Value(Value),
+        // For applications that can return a function, it's important to keep the remaining
+        // arguments to apply them to the resulting function.
+        ValueWithRemainingArgs(&'a [Value], Value),
+        DoneAsIs,
+    }
+    let make_closure = |e| {
+        type_with(&env.to_alpha_tyenv(), &e)
+            .unwrap()
+            .normalize_whnf(&env)
+    };
+
+    let ret = match (b, args.as_slice()) {
+        (OptionalNone, [t]) => Ret::ValueKind(EmptyOptionalLit(t.clone())),
+        (NaturalIsZero, [n]) => match &*n.as_whnf() {
+            NaturalLit(n) => Ret::ValueKind(BoolLit(*n == 0)),
+            _ => Ret::DoneAsIs,
+        },
+        (NaturalEven, [n]) => match &*n.as_whnf() {
+            NaturalLit(n) => Ret::ValueKind(BoolLit(*n % 2 == 0)),
+            _ => Ret::DoneAsIs,
+        },
+        (NaturalOdd, [n]) => match &*n.as_whnf() {
+            NaturalLit(n) => Ret::ValueKind(BoolLit(*n % 2 != 0)),
+            _ => Ret::DoneAsIs,
+        },
+        (NaturalToInteger, [n]) => match &*n.as_whnf() {
+            NaturalLit(n) => Ret::ValueKind(IntegerLit(*n as isize)),
+            _ => Ret::DoneAsIs,
+        },
+        (NaturalShow, [n]) => {
+            match &*n.as_whnf() {
+                NaturalLit(n) => Ret::ValueKind(TextLit(vec![
+                    InterpolatedTextContents::Text(n.to_string()),
+                ])),
+                _ => Ret::DoneAsIs,
+            }
+        }
+        (NaturalSubtract, [a, b]) => match (&*a.as_whnf(), &*b.as_whnf()) {
+            (NaturalLit(a), NaturalLit(b)) => {
+                Ret::ValueKind(NaturalLit(if b > a { b - a } else { 0 }))
+            }
+            (NaturalLit(0), _) => Ret::Value(b.clone()),
+            (_, NaturalLit(0)) => Ret::ValueKind(NaturalLit(0)),
+            _ if a == b => Ret::ValueKind(NaturalLit(0)),
+            _ => Ret::DoneAsIs,
+        },
+        (IntegerShow, [n]) => match &*n.as_whnf() {
+            IntegerLit(n) => {
+                let s = if *n < 0 {
+                    n.to_string()
+                } else {
+                    format!("+{}", n)
+                };
+                Ret::ValueKind(TextLit(vec![InterpolatedTextContents::Text(s)]))
+            }
+            _ => Ret::DoneAsIs,
+        },
+        (IntegerToDouble, [n]) => match &*n.as_whnf() {
+            IntegerLit(n) => {
+                Ret::ValueKind(DoubleLit(NaiveDouble::from(*n as f64)))
+            }
+            _ => Ret::DoneAsIs,
+        },
+        (IntegerNegate, [n]) => match &*n.as_whnf() {
+            IntegerLit(n) => Ret::ValueKind(IntegerLit(-n)),
+            _ => Ret::DoneAsIs,
+        },
+        (IntegerClamp, [n]) => match &*n.as_whnf() {
+            IntegerLit(n) => {
+                Ret::ValueKind(NaturalLit((*n).try_into().unwrap_or(0)))
+            }
+            _ => Ret::DoneAsIs,
+        },
+        (DoubleShow, [n]) => {
+            match &*n.as_whnf() {
+                DoubleLit(n) => Ret::ValueKind(TextLit(vec![
+                    InterpolatedTextContents::Text(n.to_string()),
+                ])),
+                _ => Ret::DoneAsIs,
+            }
+        }
+        (TextShow, [v]) => match &*v.as_whnf() {
+            TextLit(elts) => {
+                match elts.as_slice() {
+                    // Empty string literal.
+                    [] => {
+                        // Printing InterpolatedText takes care of all the escaping
+                        let txt: InterpolatedText<Normalized> =
+                            std::iter::empty().collect();
+                        let s = txt.to_string();
+                        Ret::ValueKind(TextLit(vec![
+                            InterpolatedTextContents::Text(s),
+                        ]))
+                    }
+                    // If there are no interpolations (invariants ensure that when there are no
+                    // interpolations, there is a single Text item) in the literal.
+                    [InterpolatedTextContents::Text(s)] => {
+                        // Printing InterpolatedText takes care of all the escaping
+                        let txt: InterpolatedText<Normalized> =
+                            std::iter::once(InterpolatedTextContents::Text(
+                                s.clone(),
+                            ))
+                            .collect();
+                        let s = txt.to_string();
+                        Ret::ValueKind(TextLit(vec![
+                            InterpolatedTextContents::Text(s),
+                        ]))
+                    }
+                    _ => Ret::DoneAsIs,
+                }
+            }
+            _ => Ret::DoneAsIs,
+        },
+        (ListLength, [_, l]) => match &*l.as_whnf() {
+            EmptyListLit(_) => Ret::ValueKind(NaturalLit(0)),
+            NEListLit(xs) => Ret::ValueKind(NaturalLit(xs.len())),
+            _ => Ret::DoneAsIs,
+        },
+        (ListHead, [_, l]) => match &*l.as_whnf() {
+            EmptyListLit(n) => Ret::ValueKind(EmptyOptionalLit(n.clone())),
+            NEListLit(xs) => {
+                Ret::ValueKind(NEOptionalLit(xs.iter().next().unwrap().clone()))
+            }
+            _ => Ret::DoneAsIs,
+        },
+        (ListLast, [_, l]) => match &*l.as_whnf() {
+            EmptyListLit(n) => Ret::ValueKind(EmptyOptionalLit(n.clone())),
+            NEListLit(xs) => Ret::ValueKind(NEOptionalLit(
+                xs.iter().rev().next().unwrap().clone(),
+            )),
+            _ => Ret::DoneAsIs,
+        },
+        (ListReverse, [_, l]) => match &*l.as_whnf() {
+            EmptyListLit(n) => Ret::ValueKind(EmptyListLit(n.clone())),
+            NEListLit(xs) => {
+                Ret::ValueKind(NEListLit(xs.iter().rev().cloned().collect()))
+            }
+            _ => Ret::DoneAsIs,
+        },
+        (ListIndexed, [_, l]) => {
+            let l_whnf = l.as_whnf();
+            match &*l_whnf {
+                EmptyListLit(_) | NEListLit(_) => {
+                    // Extract the type of the list elements
+                    let t = match &*l_whnf {
+                        EmptyListLit(t) => t.clone(),
+                        NEListLit(xs) => xs[0].get_type_not_sort(),
+                        _ => unreachable!(),
+                    };
+
+                    // Construct the returned record type: { index: Natural, value: t }
+                    let mut kts = HashMap::new();
+                    kts.insert("index".into(), Value::from_builtin(Natural));
+                    kts.insert("value".into(), t.clone());
+                    let t = Value::from_kind_and_type(
+                        RecordType(kts),
+                        Value::from_const(Type),
+                    );
+
+                    // Construct the new list, with added indices
+                    let list = match &*l_whnf {
+                        EmptyListLit(_) => EmptyListLit(t),
+                        NEListLit(xs) => NEListLit(
+                            xs.iter()
+                                .enumerate()
+                                .map(|(i, e)| {
+                                    let mut kvs = HashMap::new();
+                                    kvs.insert(
+                                        "index".into(),
+                                        Value::from_kind_and_type(
+                                            NaturalLit(i),
+                                            Value::from_builtin(
+                                                Builtin::Natural,
+                                            ),
+                                        ),
+                                    );
+                                    kvs.insert("value".into(), e.clone());
+                                    Value::from_kind_and_type(
+                                        RecordLit(kvs),
+                                        t.clone(),
+                                    )
+                                })
+                                .collect(),
+                        ),
+                        _ => unreachable!(),
+                    };
+                    Ret::ValueKind(list)
+                }
+                _ => Ret::DoneAsIs,
+            }
+        }
+        (ListBuild, [t, f]) => {
+            let list_t = Value::from_builtin(List).app(t.clone());
+            Ret::Value(
+                f.app(list_t.clone())
+                    .app(
+                        make_closure(make_closure!(
+                            λ(T : Type) ->
+                            λ(a : var(T)) ->
+                            λ(as : List var(T)) ->
+                            [ var(a) ] # var(as)
+                        ))
+                        .app(t.clone()),
+                    )
+                    .app(EmptyListLit(t.clone()).into_value_with_type(list_t)),
+            )
+        }
+        (ListFold, [_, l, _, cons, nil, r @ ..]) => match &*l.as_whnf() {
+            EmptyListLit(_) => Ret::ValueWithRemainingArgs(r, nil.clone()),
+            NEListLit(xs) => {
+                let mut v = nil.clone();
+                for x in xs.iter().cloned().rev() {
+                    v = cons.app(x).app(v);
+                }
+                Ret::ValueWithRemainingArgs(r, v)
+            }
+            _ => Ret::DoneAsIs,
+        },
+        (OptionalBuild, [t, f]) => {
+            let optional_t = Value::from_builtin(Optional).app(t.clone());
+            Ret::Value(
+                f.app(optional_t.clone())
+                    .app(
+                        make_closure(make_closure!(
+                            λ(T : Type) ->
+                            λ(a : var(T)) ->
+                            Some(var(a))
+                        ))
+                        .app(t.clone()),
+                    )
+                    .app(
+                        EmptyOptionalLit(t.clone())
+                            .into_value_with_type(optional_t),
+                    ),
+            )
+        }
+        (OptionalFold, [_, v, _, just, nothing, r @ ..]) => match &*v.as_whnf()
+        {
+            EmptyOptionalLit(_) => {
+                Ret::ValueWithRemainingArgs(r, nothing.clone())
+            }
+            NEOptionalLit(x) => {
+                Ret::ValueWithRemainingArgs(r, just.app(x.clone()))
+            }
+            _ => Ret::DoneAsIs,
+        },
+        (NaturalBuild, [f]) => Ret::Value(
+            f.app(Value::from_builtin(Natural))
+                .app(make_closure(make_closure!(
+                    λ(x : Natural) ->
+                    1 + var(x)
+                )))
+                .app(
+                    NaturalLit(0)
+                        .into_value_with_type(Value::from_builtin(Natural)),
+                ),
+        ),
+
+        (NaturalFold, [n, t, succ, zero, r @ ..]) => match &*n.as_whnf() {
+            NaturalLit(0) => Ret::ValueWithRemainingArgs(r, zero.clone()),
+            NaturalLit(n) => {
+                let fold = Value::from_builtin(NaturalFold)
+                    .app(
+                        NaturalLit(n - 1)
+                            .into_value_with_type(Value::from_builtin(Natural)),
+                    )
+                    .app(t.clone())
+                    .app(succ.clone())
+                    .app(zero.clone());
+                Ret::ValueWithRemainingArgs(r, succ.app(fold))
+            }
+            _ => Ret::DoneAsIs,
+        },
+        _ => Ret::DoneAsIs,
+    };
+    match ret {
+        Ret::ValueKind(v) => v,
+        Ret::Value(v) => v.to_whnf_check_type(ty),
+        Ret::ValueWithRemainingArgs(unconsumed_args, mut v) => {
+            let n_consumed_args = args.len() - unconsumed_args.len();
+            for x in args.into_iter().skip(n_consumed_args) {
+                v = v.app(x);
+            }
+            v.to_whnf_check_type(ty)
+        }
+        Ret::DoneAsIs => AppliedBuiltin(b, args, types, env),
+    }
+}
diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs
index 918826b..7ecb2bf 100644
--- a/dhall/src/semantics/core/value.rs
+++ b/dhall/src/semantics/core/value.rs
@@ -5,12 +5,9 @@ use std::rc::Rc;
 use crate::error::{TypeError, TypeMessage};
 use crate::semantics::core::var::Binder;
 use crate::semantics::phase::normalize::{apply_any, normalize_whnf};
-use crate::semantics::phase::typecheck::{
-    builtin_to_value, builtin_to_value_env, const_to_value,
-};
 use crate::semantics::phase::{Normalized, NormalizedExpr, ToExprOptions};
+use crate::semantics::{type_of_builtin, TyExpr, TyExprKind};
 use crate::semantics::{NzEnv, NzVar, VarEnv};
-use crate::semantics::{TyExpr, TyExprKind};
 use crate::syntax::{
     BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label,
     NaiveDouble, Natural, Span,
@@ -138,13 +135,27 @@ impl Value {
         Value::new(v, WHNF, t, Span::Artificial)
     }
     pub(crate) fn from_const(c: Const) -> Self {
-        const_to_value(c)
+        let v = ValueKind::Const(c);
+        match c {
+            Const::Type => {
+                Value::from_kind_and_type(v, Value::from_const(Const::Kind))
+            }
+            Const::Kind => {
+                Value::from_kind_and_type(v, Value::from_const(Const::Sort))
+            }
+            Const::Sort => Value::const_sort(),
+        }
     }
     pub(crate) fn from_builtin(b: Builtin) -> Self {
         Self::from_builtin_env(b, &NzEnv::new())
     }
     pub(crate) fn from_builtin_env(b: Builtin, env: &NzEnv) -> Self {
-        builtin_to_value_env(b, env)
+        Value::from_kind_and_type(
+            ValueKind::from_builtin_env(b, env.clone()),
+            crate::semantics::tck::typecheck::typecheck(&type_of_builtin(b))
+                .unwrap()
+                .normalize_whnf_noenv(),
+        )
     }
 
     pub(crate) fn as_const(&self) -> Option<Const> {
@@ -361,17 +372,19 @@ impl Value {
                     ValueKind::IntegerLit(n) => ExprKind::IntegerLit(n),
                     ValueKind::DoubleLit(n) => ExprKind::DoubleLit(n),
                     ValueKind::EmptyOptionalLit(n) => ExprKind::App(
-                        builtin_to_value(Builtin::OptionalNone).to_tyexpr(venv),
+                        Value::from_builtin(Builtin::OptionalNone)
+                            .to_tyexpr(venv),
                         n,
                     ),
                     ValueKind::NEOptionalLit(n) => ExprKind::SomeLit(n),
                     ValueKind::EmptyListLit(n) => {
                         ExprKind::EmptyListLit(TyExpr::new(
                             TyExprKind::Expr(ExprKind::App(
-                                builtin_to_value(Builtin::List).to_tyexpr(venv),
+                                Value::from_builtin(Builtin::List)
+                                    .to_tyexpr(venv),
                                 n,
                             )),
-                            Some(const_to_value(Const::Type)),
+                            Some(Value::from_const(Const::Type)),
                             Span::Artificial,
                         ))
                     }
diff --git a/dhall/src/semantics/mod.rs b/dhall/src/semantics/mod.rs
index ce08334..01bbd39 100644
--- a/dhall/src/semantics/mod.rs
+++ b/dhall/src/semantics/mod.rs
@@ -1,7 +1,9 @@
+pub mod builtins;
 pub mod core;
 pub mod nze;
 pub mod phase;
 pub mod tck;
+pub(crate) use self::builtins::*;
 pub(crate) use self::core::*;
 pub(crate) use self::nze::*;
 pub(crate) use self::tck::*;
diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs
index ce37993..2d4b4b3 100644
--- a/dhall/src/semantics/phase/normalize.rs
+++ b/dhall/src/semantics/phase/normalize.rs
@@ -1,373 +1,12 @@
 use std::collections::HashMap;
-use std::convert::TryInto;
 
-use crate::semantics::phase::typecheck::{
-    builtin_to_value_env, const_to_value, rc,
-};
 use crate::semantics::phase::Normalized;
-use crate::semantics::tck::typecheck::type_with;
 use crate::semantics::NzEnv;
-use crate::semantics::{Binder, Closure, TyExpr, TyExprKind, Value, ValueKind};
-use crate::syntax;
-use crate::syntax::Const::Type;
-use crate::syntax::{
-    BinOp, Builtin, Const, ExprKind, InterpolatedText,
-    InterpolatedTextContents, Label, NaiveDouble,
+use crate::semantics::{
+    apply_builtin, Binder, Closure, TyExpr, TyExprKind, Value, ValueKind,
 };
-
-// Ad-hoc macro to help construct closures
-macro_rules! make_closure {
-    (var($var:ident)) => {{
-        rc(ExprKind::Var(syntax::V(
-            Label::from(stringify!($var)).into(),
-            0
-        )))
-    }};
-    (λ($var:tt : $($ty:tt)*) -> $($body:tt)*) => {{
-        let var = Label::from(stringify!($var));
-        let ty = make_closure!($($ty)*);
-        let body = make_closure!($($body)*);
-        rc(ExprKind::Lam(var, ty, body))
-    }};
-    (Type) => {
-        rc(ExprKind::Const(Type))
-    };
-    (Natural) => {
-        rc(ExprKind::Builtin(Builtin::Natural))
-    };
-    (List $($ty:tt)*) => {{
-        let ty = make_closure!($($ty)*);
-        rc(ExprKind::App(
-            rc(ExprKind::Builtin(Builtin::List)),
-            ty
-        ))
-    }};
-    (Some($($v:tt)*)) => {
-        rc(ExprKind::SomeLit(
-            make_closure!($($v)*)
-        ))
-    };
-    (1 + $($v:tt)*) => {
-        rc(ExprKind::BinOp(
-            syntax::BinOp::NaturalPlus,
-            make_closure!($($v)*),
-            rc(ExprKind::NaturalLit(1))
-        ))
-    };
-    ([ $($head:tt)* ] # $($tail:tt)*) => {{
-        let head = make_closure!($($head)*);
-        let tail = make_closure!($($tail)*);
-        rc(ExprKind::BinOp(
-            syntax::BinOp::ListAppend,
-            rc(ExprKind::NEListLit(vec![head])),
-            tail,
-        ))
-    }};
-}
-
-#[allow(clippy::cognitive_complexity)]
-pub(crate) fn apply_builtin(
-    b: Builtin,
-    args: Vec<Value>,
-    ty: &Value,
-    types: Vec<Value>,
-    env: NzEnv,
-) -> ValueKind<Value> {
-    use syntax::Builtin::*;
-    use ValueKind::*;
-
-    // Small helper enum
-    enum Ret<'a> {
-        ValueKind(ValueKind<Value>),
-        Value(Value),
-        // For applications that can return a function, it's important to keep the remaining
-        // arguments to apply them to the resulting function.
-        ValueWithRemainingArgs(&'a [Value], Value),
-        DoneAsIs,
-    }
-    let make_closure = |e| {
-        type_with(&env.to_alpha_tyenv(), &e)
-            .unwrap()
-            .normalize_whnf(&env)
-    };
-
-    let ret = match (b, args.as_slice()) {
-        (OptionalNone, [t]) => Ret::ValueKind(EmptyOptionalLit(t.clone())),
-        (NaturalIsZero, [n]) => match &*n.as_whnf() {
-            NaturalLit(n) => Ret::ValueKind(BoolLit(*n == 0)),
-            _ => Ret::DoneAsIs,
-        },
-        (NaturalEven, [n]) => match &*n.as_whnf() {
-            NaturalLit(n) => Ret::ValueKind(BoolLit(*n % 2 == 0)),
-            _ => Ret::DoneAsIs,
-        },
-        (NaturalOdd, [n]) => match &*n.as_whnf() {
-            NaturalLit(n) => Ret::ValueKind(BoolLit(*n % 2 != 0)),
-            _ => Ret::DoneAsIs,
-        },
-        (NaturalToInteger, [n]) => match &*n.as_whnf() {
-            NaturalLit(n) => Ret::ValueKind(IntegerLit(*n as isize)),
-            _ => Ret::DoneAsIs,
-        },
-        (NaturalShow, [n]) => {
-            match &*n.as_whnf() {
-                NaturalLit(n) => Ret::ValueKind(TextLit(vec![
-                    InterpolatedTextContents::Text(n.to_string()),
-                ])),
-                _ => Ret::DoneAsIs,
-            }
-        }
-        (NaturalSubtract, [a, b]) => match (&*a.as_whnf(), &*b.as_whnf()) {
-            (NaturalLit(a), NaturalLit(b)) => {
-                Ret::ValueKind(NaturalLit(if b > a { b - a } else { 0 }))
-            }
-            (NaturalLit(0), _) => Ret::Value(b.clone()),
-            (_, NaturalLit(0)) => Ret::ValueKind(NaturalLit(0)),
-            _ if a == b => Ret::ValueKind(NaturalLit(0)),
-            _ => Ret::DoneAsIs,
-        },
-        (IntegerShow, [n]) => match &*n.as_whnf() {
-            IntegerLit(n) => {
-                let s = if *n < 0 {
-                    n.to_string()
-                } else {
-                    format!("+{}", n)
-                };
-                Ret::ValueKind(TextLit(vec![InterpolatedTextContents::Text(s)]))
-            }
-            _ => Ret::DoneAsIs,
-        },
-        (IntegerToDouble, [n]) => match &*n.as_whnf() {
-            IntegerLit(n) => {
-                Ret::ValueKind(DoubleLit(NaiveDouble::from(*n as f64)))
-            }
-            _ => Ret::DoneAsIs,
-        },
-        (IntegerNegate, [n]) => match &*n.as_whnf() {
-            IntegerLit(n) => Ret::ValueKind(IntegerLit(-n)),
-            _ => Ret::DoneAsIs,
-        },
-        (IntegerClamp, [n]) => match &*n.as_whnf() {
-            IntegerLit(n) => {
-                Ret::ValueKind(NaturalLit((*n).try_into().unwrap_or(0)))
-            }
-            _ => Ret::DoneAsIs,
-        },
-        (DoubleShow, [n]) => {
-            match &*n.as_whnf() {
-                DoubleLit(n) => Ret::ValueKind(TextLit(vec![
-                    InterpolatedTextContents::Text(n.to_string()),
-                ])),
-                _ => Ret::DoneAsIs,
-            }
-        }
-        (TextShow, [v]) => match &*v.as_whnf() {
-            TextLit(elts) => {
-                match elts.as_slice() {
-                    // Empty string literal.
-                    [] => {
-                        // Printing InterpolatedText takes care of all the escaping
-                        let txt: InterpolatedText<Normalized> =
-                            std::iter::empty().collect();
-                        let s = txt.to_string();
-                        Ret::ValueKind(TextLit(vec![
-                            InterpolatedTextContents::Text(s),
-                        ]))
-                    }
-                    // If there are no interpolations (invariants ensure that when there are no
-                    // interpolations, there is a single Text item) in the literal.
-                    [InterpolatedTextContents::Text(s)] => {
-                        // Printing InterpolatedText takes care of all the escaping
-                        let txt: InterpolatedText<Normalized> =
-                            std::iter::once(InterpolatedTextContents::Text(
-                                s.clone(),
-                            ))
-                            .collect();
-                        let s = txt.to_string();
-                        Ret::ValueKind(TextLit(vec![
-                            InterpolatedTextContents::Text(s),
-                        ]))
-                    }
-                    _ => Ret::DoneAsIs,
-                }
-            }
-            _ => Ret::DoneAsIs,
-        },
-        (ListLength, [_, l]) => match &*l.as_whnf() {
-            EmptyListLit(_) => Ret::ValueKind(NaturalLit(0)),
-            NEListLit(xs) => Ret::ValueKind(NaturalLit(xs.len())),
-            _ => Ret::DoneAsIs,
-        },
-        (ListHead, [_, l]) => match &*l.as_whnf() {
-            EmptyListLit(n) => Ret::ValueKind(EmptyOptionalLit(n.clone())),
-            NEListLit(xs) => {
-                Ret::ValueKind(NEOptionalLit(xs.iter().next().unwrap().clone()))
-            }
-            _ => Ret::DoneAsIs,
-        },
-        (ListLast, [_, l]) => match &*l.as_whnf() {
-            EmptyListLit(n) => Ret::ValueKind(EmptyOptionalLit(n.clone())),
-            NEListLit(xs) => Ret::ValueKind(NEOptionalLit(
-                xs.iter().rev().next().unwrap().clone(),
-            )),
-            _ => Ret::DoneAsIs,
-        },
-        (ListReverse, [_, l]) => match &*l.as_whnf() {
-            EmptyListLit(n) => Ret::ValueKind(EmptyListLit(n.clone())),
-            NEListLit(xs) => {
-                Ret::ValueKind(NEListLit(xs.iter().rev().cloned().collect()))
-            }
-            _ => Ret::DoneAsIs,
-        },
-        (ListIndexed, [_, l]) => {
-            let l_whnf = l.as_whnf();
-            match &*l_whnf {
-                EmptyListLit(_) | NEListLit(_) => {
-                    // Extract the type of the list elements
-                    let t = match &*l_whnf {
-                        EmptyListLit(t) => t.clone(),
-                        NEListLit(xs) => xs[0].get_type_not_sort(),
-                        _ => unreachable!(),
-                    };
-
-                    // Construct the returned record type: { index: Natural, value: t }
-                    let mut kts = HashMap::new();
-                    kts.insert("index".into(), Value::from_builtin(Natural));
-                    kts.insert("value".into(), t.clone());
-                    let t = Value::from_kind_and_type(
-                        RecordType(kts),
-                        Value::from_const(Type),
-                    );
-
-                    // Construct the new list, with added indices
-                    let list = match &*l_whnf {
-                        EmptyListLit(_) => EmptyListLit(t),
-                        NEListLit(xs) => NEListLit(
-                            xs.iter()
-                                .enumerate()
-                                .map(|(i, e)| {
-                                    let mut kvs = HashMap::new();
-                                    kvs.insert(
-                                        "index".into(),
-                                        Value::from_kind_and_type(
-                                            NaturalLit(i),
-                                            Value::from_builtin(
-                                                Builtin::Natural,
-                                            ),
-                                        ),
-                                    );
-                                    kvs.insert("value".into(), e.clone());
-                                    Value::from_kind_and_type(
-                                        RecordLit(kvs),
-                                        t.clone(),
-                                    )
-                                })
-                                .collect(),
-                        ),
-                        _ => unreachable!(),
-                    };
-                    Ret::ValueKind(list)
-                }
-                _ => Ret::DoneAsIs,
-            }
-        }
-        (ListBuild, [t, f]) => {
-            let list_t = Value::from_builtin(List).app(t.clone());
-            Ret::Value(
-                f.app(list_t.clone())
-                    .app(
-                        make_closure(make_closure!(
-                            λ(T : Type) ->
-                            λ(a : var(T)) ->
-                            λ(as : List var(T)) ->
-                            [ var(a) ] # var(as)
-                        ))
-                        .app(t.clone()),
-                    )
-                    .app(EmptyListLit(t.clone()).into_value_with_type(list_t)),
-            )
-        }
-        (ListFold, [_, l, _, cons, nil, r @ ..]) => match &*l.as_whnf() {
-            EmptyListLit(_) => Ret::ValueWithRemainingArgs(r, nil.clone()),
-            NEListLit(xs) => {
-                let mut v = nil.clone();
-                for x in xs.iter().cloned().rev() {
-                    v = cons.app(x).app(v);
-                }
-                Ret::ValueWithRemainingArgs(r, v)
-            }
-            _ => Ret::DoneAsIs,
-        },
-        (OptionalBuild, [t, f]) => {
-            let optional_t = Value::from_builtin(Optional).app(t.clone());
-            Ret::Value(
-                f.app(optional_t.clone())
-                    .app(
-                        make_closure(make_closure!(
-                            λ(T : Type) ->
-                            λ(a : var(T)) ->
-                            Some(var(a))
-                        ))
-                        .app(t.clone()),
-                    )
-                    .app(
-                        EmptyOptionalLit(t.clone())
-                            .into_value_with_type(optional_t),
-                    ),
-            )
-        }
-        (OptionalFold, [_, v, _, just, nothing, r @ ..]) => match &*v.as_whnf()
-        {
-            EmptyOptionalLit(_) => {
-                Ret::ValueWithRemainingArgs(r, nothing.clone())
-            }
-            NEOptionalLit(x) => {
-                Ret::ValueWithRemainingArgs(r, just.app(x.clone()))
-            }
-            _ => Ret::DoneAsIs,
-        },
-        (NaturalBuild, [f]) => Ret::Value(
-            f.app(Value::from_builtin(Natural))
-                .app(make_closure(make_closure!(
-                    λ(x : Natural) ->
-                    1 + var(x)
-                )))
-                .app(
-                    NaturalLit(0)
-                        .into_value_with_type(Value::from_builtin(Natural)),
-                ),
-        ),
-
-        (NaturalFold, [n, t, succ, zero, r @ ..]) => match &*n.as_whnf() {
-            NaturalLit(0) => Ret::ValueWithRemainingArgs(r, zero.clone()),
-            NaturalLit(n) => {
-                let fold = Value::from_builtin(NaturalFold)
-                    .app(
-                        NaturalLit(n - 1)
-                            .into_value_with_type(Value::from_builtin(Natural)),
-                    )
-                    .app(t.clone())
-                    .app(succ.clone())
-                    .app(zero.clone());
-                Ret::ValueWithRemainingArgs(r, succ.app(fold))
-            }
-            _ => Ret::DoneAsIs,
-        },
-        _ => Ret::DoneAsIs,
-    };
-    match ret {
-        Ret::ValueKind(v) => v,
-        Ret::Value(v) => v.to_whnf_check_type(ty),
-        Ret::ValueWithRemainingArgs(unconsumed_args, mut v) => {
-            let n_consumed_args = args.len() - unconsumed_args.len();
-            for x in args.into_iter().skip(n_consumed_args) {
-                v = v.app(x);
-            }
-            v.to_whnf_check_type(ty)
-        }
-        Ret::DoneAsIs => AppliedBuiltin(b, args, types, env),
-    }
-}
+use crate::syntax;
+use crate::syntax::{BinOp, Const, ExprKind, InterpolatedTextContents};
 
 pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind<Value> {
     let f_borrow = f.as_whnf();
@@ -643,8 +282,8 @@ pub(crate) fn normalize_one_layer(
             unreachable!("This case should have been handled in typecheck")
         }
         ExprKind::Annot(x, _) => Ret::Value(x),
-        ExprKind::Const(c) => Ret::Value(const_to_value(c)),
-        ExprKind::Builtin(b) => Ret::Value(builtin_to_value_env(b, env)),
+        ExprKind::Const(c) => Ret::Value(Value::from_const(c)),
+        ExprKind::Builtin(b) => Ret::Value(Value::from_builtin_env(b, env)),
         ExprKind::Assert(_) => Ret::Expr(expr),
         ExprKind::App(v, a) => Ret::Value(v.app(a)),
         ExprKind::BoolLit(b) => Ret::ValueKind(BoolLit(b)),
diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs
index 2e22ad2..8b13789 100644
--- a/dhall/src/semantics/phase/typecheck.rs
+++ b/dhall/src/semantics/phase/typecheck.rs
@@ -1,178 +1 @@
-use crate::semantics::{NzEnv, Value, ValueKind};
-use crate::syntax;
-use crate::syntax::{
-    Builtin, Const, Expr, ExprKind, Label, Span, UnspannedExpr,
-};
 
-pub(crate) fn const_to_value(c: Const) -> Value {
-    let v = ValueKind::Const(c);
-    match c {
-        Const::Type => {
-            Value::from_kind_and_type(v, const_to_value(Const::Kind))
-        }
-        Const::Kind => {
-            Value::from_kind_and_type(v, const_to_value(Const::Sort))
-        }
-        Const::Sort => Value::const_sort(),
-    }
-}
-
-pub fn rc<E>(x: UnspannedExpr<E>) -> Expr<E> {
-    Expr::new(x, Span::Artificial)
-}
-
-// Ad-hoc macro to help construct the types of builtins
-macro_rules! make_type {
-    (Type) => { ExprKind::Const(Const::Type) };
-    (Bool) => { ExprKind::Builtin(Builtin::Bool) };
-    (Natural) => { ExprKind::Builtin(Builtin::Natural) };
-    (Integer) => { ExprKind::Builtin(Builtin::Integer) };
-    (Double) => { ExprKind::Builtin(Builtin::Double) };
-    (Text) => { ExprKind::Builtin(Builtin::Text) };
-    ($var:ident) => {
-        ExprKind::Var(syntax::V(stringify!($var).into(), 0))
-    };
-    (Optional $ty:ident) => {
-        ExprKind::App(
-            rc(ExprKind::Builtin(Builtin::Optional)),
-            rc(make_type!($ty))
-        )
-    };
-    (List $($rest:tt)*) => {
-        ExprKind::App(
-            rc(ExprKind::Builtin(Builtin::List)),
-            rc(make_type!($($rest)*))
-        )
-    };
-    ({ $($label:ident : $ty:ident),* }) => {{
-        let mut kts = syntax::map::DupTreeMap::new();
-        $(
-            kts.insert(
-                Label::from(stringify!($label)),
-                rc(make_type!($ty)),
-            );
-        )*
-        ExprKind::RecordType(kts)
-    }};
-    ($ty:ident -> $($rest:tt)*) => {
-        ExprKind::Pi(
-            "_".into(),
-            rc(make_type!($ty)),
-            rc(make_type!($($rest)*))
-        )
-    };
-    (($($arg:tt)*) -> $($rest:tt)*) => {
-        ExprKind::Pi(
-            "_".into(),
-            rc(make_type!($($arg)*)),
-            rc(make_type!($($rest)*))
-        )
-    };
-    (forall ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => {
-        ExprKind::Pi(
-            stringify!($var).into(),
-            rc(make_type!($($ty)*)),
-            rc(make_type!($($rest)*))
-        )
-    };
-}
-
-pub(crate) fn type_of_builtin<E>(b: Builtin) -> Expr<E> {
-    use syntax::Builtin::*;
-    rc(match b {
-        Bool | Natural | Integer | Double | Text => make_type!(Type),
-        List | Optional => make_type!(
-            Type -> Type
-        ),
-
-        NaturalFold => make_type!(
-            Natural ->
-            forall (natural: Type) ->
-            forall (succ: natural -> natural) ->
-            forall (zero: natural) ->
-            natural
-        ),
-        NaturalBuild => make_type!(
-            (forall (natural: Type) ->
-                forall (succ: natural -> natural) ->
-                forall (zero: natural) ->
-                natural) ->
-            Natural
-        ),
-        NaturalIsZero | NaturalEven | NaturalOdd => make_type!(
-            Natural -> Bool
-        ),
-        NaturalToInteger => make_type!(Natural -> Integer),
-        NaturalShow => make_type!(Natural -> Text),
-        NaturalSubtract => make_type!(Natural -> Natural -> Natural),
-
-        IntegerToDouble => make_type!(Integer -> Double),
-        IntegerShow => make_type!(Integer -> Text),
-        IntegerNegate => make_type!(Integer -> Integer),
-        IntegerClamp => make_type!(Integer -> Natural),
-
-        DoubleShow => make_type!(Double -> Text),
-        TextShow => make_type!(Text -> Text),
-
-        ListBuild => make_type!(
-            forall (a: Type) ->
-            (forall (list: Type) ->
-                forall (cons: a -> list -> list) ->
-                forall (nil: list) ->
-                list) ->
-            List a
-        ),
-        ListFold => make_type!(
-            forall (a: Type) ->
-            (List a) ->
-            forall (list: Type) ->
-            forall (cons: a -> list -> list) ->
-            forall (nil: list) ->
-            list
-        ),
-        ListLength => make_type!(forall (a: Type) -> (List a) -> Natural),
-        ListHead | ListLast => {
-            make_type!(forall (a: Type) -> (List a) -> Optional a)
-        }
-        ListIndexed => make_type!(
-            forall (a: Type) ->
-            (List a) ->
-            List { index: Natural, value: a }
-        ),
-        ListReverse => make_type!(
-            forall (a: Type) -> (List a) -> List a
-        ),
-
-        OptionalBuild => make_type!(
-            forall (a: Type) ->
-            (forall (optional: Type) ->
-                forall (just: a -> optional) ->
-                forall (nothing: optional) ->
-                optional) ->
-            Optional a
-        ),
-        OptionalFold => make_type!(
-            forall (a: Type) ->
-            (Optional a) ->
-            forall (optional: Type) ->
-            forall (just: a -> optional) ->
-            forall (nothing: optional) ->
-            optional
-        ),
-        OptionalNone => make_type!(
-            forall (A: Type) -> Optional A
-        ),
-    })
-}
-
-pub(crate) fn builtin_to_value(b: Builtin) -> Value {
-    builtin_to_value_env(b, &NzEnv::new())
-}
-pub(crate) fn builtin_to_value_env(b: Builtin, env: &NzEnv) -> Value {
-    Value::from_kind_and_type(
-        ValueKind::from_builtin_env(b, env.clone()),
-        crate::semantics::tck::typecheck::typecheck(&type_of_builtin(b))
-            .unwrap()
-            .normalize_whnf_noenv(),
-    )
-}
diff --git a/dhall/src/semantics/tck/mod.rs b/dhall/src/semantics/tck/mod.rs
index 28974af..1df2a48 100644
--- a/dhall/src/semantics/tck/mod.rs
+++ b/dhall/src/semantics/tck/mod.rs
@@ -1,6 +1,6 @@
-pub mod context;
 pub mod env;
 pub mod tyexpr;
 pub mod typecheck;
 pub(crate) use env::*;
 pub(crate) use tyexpr::*;
+pub(crate) use typecheck::*;
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index 114bb14..bf7c130 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -1,9 +1,8 @@
 use crate::error::{TypeError, TypeMessage};
 use crate::semantics::phase::normalize::normalize_tyexpr_whnf;
-use crate::semantics::phase::typecheck::rc;
 use crate::semantics::phase::Normalized;
 use crate::semantics::phase::{NormalizedExpr, ToExprOptions};
-use crate::semantics::{NameEnv, NzEnv, TyEnv, Value};
+use crate::semantics::{rc, NameEnv, NzEnv, TyEnv, Value};
 use crate::syntax::{ExprKind, Span, V};
 
 pub(crate) type Type = Value;
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 789105f..22ba72d 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -4,12 +4,10 @@ use std::collections::HashMap;
 
 use crate::error::{TypeError, TypeMessage};
 use crate::semantics::phase::normalize::merge_maps;
-use crate::semantics::phase::typecheck::{
-    builtin_to_value, const_to_value, type_of_builtin,
-};
 use crate::semantics::phase::Normalized;
 use crate::semantics::{
-    Binder, Closure, NzVar, TyEnv, TyExpr, TyExprKind, Type, Value, ValueKind,
+    type_of_builtin, Binder, Closure, NzVar, TyEnv, TyExpr, TyExprKind, Type,
+    Value, ValueKind,
 };
 use crate::syntax;
 use crate::syntax::{
@@ -72,19 +70,19 @@ fn type_one_layer(
         | ExprKind::Const(Const::Sort)
         | ExprKind::Embed(..) => unreachable!(), // Handled in type_with
 
-        ExprKind::Const(Const::Type) => const_to_value(Const::Kind),
-        ExprKind::Const(Const::Kind) => const_to_value(Const::Sort),
+        ExprKind::Const(Const::Type) => Value::from_const(Const::Kind),
+        ExprKind::Const(Const::Kind) => Value::from_const(Const::Sort),
         ExprKind::Builtin(b) => {
             let t_expr = type_of_builtin(*b);
             let t_tyexpr = type_with(env, &t_expr)?;
             t_tyexpr.normalize_whnf(env.as_nzenv())
         }
-        ExprKind::BoolLit(_) => builtin_to_value(Builtin::Bool),
-        ExprKind::NaturalLit(_) => builtin_to_value(Builtin::Natural),
-        ExprKind::IntegerLit(_) => builtin_to_value(Builtin::Integer),
-        ExprKind::DoubleLit(_) => builtin_to_value(Builtin::Double),
+        ExprKind::BoolLit(_) => Value::from_builtin(Builtin::Bool),
+        ExprKind::NaturalLit(_) => Value::from_builtin(Builtin::Natural),
+        ExprKind::IntegerLit(_) => Value::from_builtin(Builtin::Integer),
+        ExprKind::DoubleLit(_) => Value::from_builtin(Builtin::Double),
         ExprKind::TextLit(interpolated) => {
-            let text_type = builtin_to_value(Builtin::Text);
+            let text_type = Value::from_builtin(Builtin::Text);
             for contents in interpolated.iter() {
                 use InterpolatedTextContents::Expr;
                 if let Expr(x) = contents {
@@ -388,7 +386,7 @@ fn type_one_layer(
             Value::from_const(Const::Type)
         }
         ExprKind::BinOp(o, l, r) => {
-            let t = builtin_to_value(match o {
+            let t = Value::from_builtin(match o {
                 BinOp::BoolAnd
                 | BinOp::BoolOr
                 | BinOp::BoolEQ