Move contents of dhall under a semantics submodule

6 files changed, 0 insertions, 2828 deletions

diff --git a/dhall/src/phase/binary.rs b/dhall/src/phase/binary.rs
deleted file mode 100644
index b1e7638..0000000
--- a/dhall/src/phase/binary.rs
+++ /dev/null
@@ -1,748 +0,0 @@
-use itertools::Itertools;
-use serde_cbor::value::value as cbor;
-use std::iter::FromIterator;
-use std::vec;
-
-use crate::syntax::map::DupTreeMap;
-use crate::syntax::{
-    Expr, ExprF, FilePath, FilePrefix, Hash, Import, ImportLocation,
-    ImportMode, Integer, InterpolatedText, Label, Natural, RawExpr, Scheme,
-    Span, URL, V,
-};
-
-use crate::error::{DecodeError, EncodeError};
-use crate::phase::DecodedExpr;
-
-pub(crate) fn decode(data: &[u8]) -> Result<DecodedExpr, DecodeError> {
-    match serde_cbor::de::from_slice(data) {
-        Ok(v) => cbor_value_to_dhall(&v),
-        Err(e) => Err(DecodeError::CBORError(e)),
-    }
-}
-
-pub(crate) fn encode<E>(expr: &Expr<E>) -> Result<Vec<u8>, EncodeError> {
-    serde_cbor::ser::to_vec(&Serialize::Expr(expr))
-        .map_err(|e| EncodeError::CBORError(e))
-}
-
-// Should probably rename this
-pub fn rc<E>(x: RawExpr<E>) -> Expr<E> {
-    Expr::new(x, Span::Decoded)
-}
-
-fn cbor_value_to_dhall(data: &cbor::Value) -> Result<DecodedExpr, DecodeError> {
-    use cbor::Value::*;
-    use crate::syntax::{BinOp, Builtin, Const};
-    use ExprF::*;
-    Ok(rc(match data {
-        String(s) => match Builtin::parse(s) {
-            Some(b) => ExprF::Builtin(b),
-            None => match s.as_str() {
-                "True" => BoolLit(true),
-                "False" => BoolLit(false),
-                "Type" => Const(Const::Type),
-                "Kind" => Const(Const::Kind),
-                "Sort" => Const(Const::Sort),
-                _ => Err(DecodeError::WrongFormatError("builtin".to_owned()))?,
-            },
-        },
-        U64(n) => Var(V(Label::from("_"), *n as usize)),
-        F64(x) => DoubleLit((*x).into()),
-        Bool(b) => BoolLit(*b),
-        Array(vec) => match vec.as_slice() {
-            [String(l), U64(n)] => {
-                if l.as_str() == "_" {
-                    Err(DecodeError::WrongFormatError(
-                        "`_` variable was encoded incorrectly".to_owned(),
-                    ))?
-                }
-                let l = Label::from(l.as_str());
-                Var(V(l, *n as usize))
-            }
-            [U64(0), f, args @ ..] => {
-                if args.is_empty() {
-                    Err(DecodeError::WrongFormatError(
-                        "Function application must have at least one argument"
-                            .to_owned(),
-                    ))?
-                }
-                let mut f = cbor_value_to_dhall(&f)?;
-                for a in args {
-                    let a = cbor_value_to_dhall(&a)?;
-                    f = rc(App(f, a))
-                }
-                return Ok(f);
-            }
-            [U64(1), x, y] => {
-                let x = cbor_value_to_dhall(&x)?;
-                let y = cbor_value_to_dhall(&y)?;
-                Lam(Label::from("_"), x, y)
-            }
-            [U64(1), String(l), x, y] => {
-                if l.as_str() == "_" {
-                    Err(DecodeError::WrongFormatError(
-                        "`_` variable was encoded incorrectly".to_owned(),
-                    ))?
-                }
-                let x = cbor_value_to_dhall(&x)?;
-                let y = cbor_value_to_dhall(&y)?;
-                let l = Label::from(l.as_str());
-                Lam(l, x, y)
-            }
-            [U64(2), x, y] => {
-                let x = cbor_value_to_dhall(&x)?;
-                let y = cbor_value_to_dhall(&y)?;
-                Pi(Label::from("_"), x, y)
-            }
-            [U64(2), String(l), x, y] => {
-                if l.as_str() == "_" {
-                    Err(DecodeError::WrongFormatError(
-                        "`_` variable was encoded incorrectly".to_owned(),
-                    ))?
-                }
-                let x = cbor_value_to_dhall(&x)?;
-                let y = cbor_value_to_dhall(&y)?;
-                let l = Label::from(l.as_str());
-                Pi(l, x, y)
-            }
-            [U64(3), U64(n), x, y] => {
-                let x = cbor_value_to_dhall(&x)?;
-                let y = cbor_value_to_dhall(&y)?;
-                use BinOp::*;
-                let op = match n {
-                    0 => BoolOr,
-                    1 => BoolAnd,
-                    2 => BoolEQ,
-                    3 => BoolNE,
-                    4 => NaturalPlus,
-                    5 => NaturalTimes,
-                    6 => TextAppend,
-                    7 => ListAppend,
-                    8 => RecursiveRecordMerge,
-                    9 => RightBiasedRecordMerge,
-                    10 => RecursiveRecordTypeMerge,
-                    11 => ImportAlt,
-                    12 => Equivalence,
-                    _ => {
-                        Err(DecodeError::WrongFormatError("binop".to_owned()))?
-                    }
-                };
-                BinOp(op, x, y)
-            }
-            [U64(4), t] => {
-                let t = cbor_value_to_dhall(&t)?;
-                EmptyListLit(rc(App(rc(ExprF::Builtin(Builtin::List)), t)))
-            }
-            [U64(4), Null, rest @ ..] => {
-                let rest = rest
-                    .iter()
-                    .map(cbor_value_to_dhall)
-                    .collect::<Result<Vec<_>, _>>()?;
-                NEListLit(rest)
-            }
-            [U64(5), Null, x] => {
-                let x = cbor_value_to_dhall(&x)?;
-                SomeLit(x)
-            }
-            // Old-style optional literals
-            [U64(5), t] => {
-                let t = cbor_value_to_dhall(&t)?;
-                App(rc(ExprF::Builtin(Builtin::OptionalNone)), t)
-            }
-            [U64(5), t, x] => {
-                let x = cbor_value_to_dhall(&x)?;
-                let t = cbor_value_to_dhall(&t)?;
-                Annot(
-                    rc(SomeLit(x)),
-                    rc(App(rc(ExprF::Builtin(Builtin::Optional)), t)),
-                )
-            }
-            [U64(6), x, y] => {
-                let x = cbor_value_to_dhall(&x)?;
-                let y = cbor_value_to_dhall(&y)?;
-                Merge(x, y, None)
-            }
-            [U64(6), x, y, z] => {
-                let x = cbor_value_to_dhall(&x)?;
-                let y = cbor_value_to_dhall(&y)?;
-                let z = cbor_value_to_dhall(&z)?;
-                Merge(x, y, Some(z))
-            }
-            [U64(7), Object(map)] => {
-                let map = cbor_map_to_dhall_map(map)?;
-                RecordType(map)
-            }
-            [U64(8), Object(map)] => {
-                let map = cbor_map_to_dhall_map(map)?;
-                RecordLit(map)
-            }
-            [U64(9), x, String(l)] => {
-                let x = cbor_value_to_dhall(&x)?;
-                let l = Label::from(l.as_str());
-                Field(x, l)
-            }
-            [U64(10), x, Array(arr)] => {
-                let x = cbor_value_to_dhall(&x)?;
-                if let [y] = arr.as_slice() {
-                    let y = cbor_value_to_dhall(&y)?;
-                    ProjectionByExpr(x, y)
-                } else {
-                    Err(DecodeError::WrongFormatError(
-                        "projection-by-expr".to_owned(),
-                    ))?
-                }
-            }
-            [U64(10), x, rest @ ..] => {
-                let x = cbor_value_to_dhall(&x)?;
-                let labels = rest
-                    .iter()
-                    .map(|s| match s {
-                        String(s) => Ok(Label::from(s.as_str())),
-                        _ => Err(DecodeError::WrongFormatError(
-                            "projection".to_owned(),
-                        )),
-                    })
-                    .collect::<Result<_, _>>()?;
-                Projection(x, labels)
-            }
-            [U64(11), Object(map)] => {
-                let map = cbor_map_to_dhall_opt_map(map)?;
-                UnionType(map)
-            }
-            [U64(12), ..] => Err(DecodeError::WrongFormatError(
-                "Union literals are not supported anymore".to_owned(),
-            ))?,
-            [U64(14), x, y, z] => {
-                let x = cbor_value_to_dhall(&x)?;
-                let y = cbor_value_to_dhall(&y)?;
-                let z = cbor_value_to_dhall(&z)?;
-                BoolIf(x, y, z)
-            }
-            [U64(15), U64(x)] => NaturalLit(*x as Natural),
-            [U64(16), U64(x)] => IntegerLit(*x as Integer),
-            [U64(16), I64(x)] => IntegerLit(*x as Integer),
-            [U64(18), String(first), rest @ ..] => {
-                TextLit(InterpolatedText::from((
-                    first.clone(),
-                    rest.iter()
-                        .tuples()
-                        .map(|(x, y)| {
-                            let x = cbor_value_to_dhall(&x)?;
-                            let y = match y {
-                                String(s) => s.clone(),
-                                _ => Err(DecodeError::WrongFormatError(
-                                    "text".to_owned(),
-                                ))?,
-                            };
-                            Ok((x, y))
-                        })
-                        .collect::<Result<_, _>>()?,
-                )))
-            }
-            [U64(19), t] => {
-                let t = cbor_value_to_dhall(&t)?;
-                Assert(t)
-            }
-            [U64(24), hash, U64(mode), U64(scheme), rest @ ..] => {
-                let mode = match mode {
-                    0 => ImportMode::Code,
-                    1 => ImportMode::RawText,
-                    2 => ImportMode::Location,
-                    _ => Err(DecodeError::WrongFormatError(format!(
-                        "import/mode/unknown_mode: {:?}",
-                        mode
-                    )))?,
-                };
-                let hash = match hash {
-                    Null => None,
-                    Bytes(bytes) => match bytes.as_slice() {
-                        [18, 32, rest @ ..] => {
-                            Some(Hash::SHA256(rest.to_vec()))
-                        }
-                        _ => Err(DecodeError::WrongFormatError(format!(
-                            "import/hash/unknown_multihash: {:?}",
-                            bytes
-                        )))?,
-                    },
-                    _ => Err(DecodeError::WrongFormatError(
-                        "import/hash/should_be_bytes".to_owned(),
-                    ))?,
-                };
-                let mut rest = rest.iter();
-                let location = match scheme {
-                    0 | 1 => {
-                        let scheme = match scheme {
-                            0 => Scheme::HTTP,
-                            _ => Scheme::HTTPS,
-                        };
-                        let headers = match rest.next() {
-                            Some(Null) => None,
-                            Some(x) => {
-                                let x = cbor_value_to_dhall(&x)?;
-                                Some(x)
-                            }
-                            _ => Err(DecodeError::WrongFormatError(
-                                "import/remote/headers".to_owned(),
-                            ))?,
-                        };
-                        let authority = match rest.next() {
-                            Some(String(s)) => s.to_owned(),
-                            _ => Err(DecodeError::WrongFormatError(
-                                "import/remote/authority".to_owned(),
-                            ))?,
-                        };
-                        let query = match rest.next_back() {
-                            Some(Null) => None,
-                            Some(String(s)) => Some(s.to_owned()),
-                            _ => Err(DecodeError::WrongFormatError(
-                                "import/remote/query".to_owned(),
-                            ))?,
-                        };
-                        let file_path = rest
-                            .map(|s| match s.as_string() {
-                                Some(s) => Ok(s.clone()),
-                                None => Err(DecodeError::WrongFormatError(
-                                    "import/remote/path".to_owned(),
-                                )),
-                            })
-                            .collect::<Result<_, _>>()?;
-                        let path = FilePath { file_path };
-                        ImportLocation::Remote(URL {
-                            scheme,
-                            authority,
-                            path,
-                            query,
-                            headers,
-                        })
-                    }
-                    2 | 3 | 4 | 5 => {
-                        let prefix = match scheme {
-                            2 => FilePrefix::Absolute,
-                            3 => FilePrefix::Here,
-                            4 => FilePrefix::Parent,
-                            5 => FilePrefix::Home,
-                            _ => Err(DecodeError::WrongFormatError(
-                                "import/local/prefix".to_owned(),
-                            ))?,
-                        };
-                        let file_path = rest
-                            .map(|s| match s.as_string() {
-                                Some(s) => Ok(s.clone()),
-                                None => Err(DecodeError::WrongFormatError(
-                                    "import/local/path".to_owned(),
-                                )),
-                            })
-                            .collect::<Result<_, _>>()?;
-                        let path = FilePath { file_path };
-                        ImportLocation::Local(prefix, path)
-                    }
-                    6 => {
-                        let env = match rest.next() {
-                            Some(String(s)) => s.to_owned(),
-                            _ => Err(DecodeError::WrongFormatError(
-                                "import/env".to_owned(),
-                            ))?,
-                        };
-                        ImportLocation::Env(env)
-                    }
-                    7 => ImportLocation::Missing,
-                    _ => Err(DecodeError::WrongFormatError(
-                        "import/type".to_owned(),
-                    ))?,
-                };
-                Import(crate::syntax::Import {
-                    mode,
-                    hash,
-                    location,
-                })
-            }
-            [U64(25), bindings @ ..] => {
-                let mut tuples = bindings.iter().tuples();
-                let bindings = (&mut tuples)
-                    .map(|(x, t, v)| {
-                        let x = x.as_string().ok_or_else(|| {
-                            DecodeError::WrongFormatError(
-                                "let/label".to_owned(),
-                            )
-                        })?;
-                        let x = Label::from(x.as_str());
-                        let t = match t {
-                            Null => None,
-                            t => Some(cbor_value_to_dhall(&t)?),
-                        };
-                        let v = cbor_value_to_dhall(&v)?;
-                        Ok((x, t, v))
-                    })
-                    .collect::<Result<Vec<_>, _>>()?;
-                let expr = tuples.into_buffer().next().ok_or_else(|| {
-                    DecodeError::WrongFormatError("let/expr".to_owned())
-                })?;
-                let expr = cbor_value_to_dhall(expr)?;
-                return Ok(bindings
-                    .into_iter()
-                    .rev()
-                    .fold(expr, |acc, (x, t, v)| rc(Let(x, t, v, acc))));
-            }
-            [U64(26), x, y] => {
-                let x = cbor_value_to_dhall(&x)?;
-                let y = cbor_value_to_dhall(&y)?;
-                Annot(x, y)
-            }
-            [U64(27), x] => {
-                let x = cbor_value_to_dhall(&x)?;
-                ToMap(x, None)
-            }
-            [U64(27), x, y] => {
-                let x = cbor_value_to_dhall(&x)?;
-                let y = cbor_value_to_dhall(&y)?;
-                ToMap(x, Some(y))
-            }
-            [U64(28), x] => {
-                let x = cbor_value_to_dhall(&x)?;
-                EmptyListLit(x)
-            }
-            _ => Err(DecodeError::WrongFormatError(format!("{:?}", data)))?,
-        },
-        _ => Err(DecodeError::WrongFormatError(format!("{:?}", data)))?,
-    }))
-}
-
-fn cbor_map_to_dhall_map<'a, T>(
-    map: impl IntoIterator<Item = (&'a cbor::ObjectKey, &'a cbor::Value)>,
-) -> Result<T, DecodeError>
-where
-    T: FromIterator<(Label, DecodedExpr)>,
-{
-    map.into_iter()
-        .map(|(k, v)| -> Result<(_, _), _> {
-            let k = k.as_string().ok_or_else(|| {
-                DecodeError::WrongFormatError("map/key".to_owned())
-            })?;
-            let v = cbor_value_to_dhall(v)?;
-            Ok((Label::from(k.as_ref()), v))
-        })
-        .collect::<Result<_, _>>()
-}
-
-fn cbor_map_to_dhall_opt_map<'a, T>(
-    map: impl IntoIterator<Item = (&'a cbor::ObjectKey, &'a cbor::Value)>,
-) -> Result<T, DecodeError>
-where
-    T: FromIterator<(Label, Option<DecodedExpr>)>,
-{
-    map.into_iter()
-        .map(|(k, v)| -> Result<(_, _), _> {
-            let k = k.as_string().ok_or_else(|| {
-                DecodeError::WrongFormatError("map/key".to_owned())
-            })?;
-            let v = match v {
-                cbor::Value::Null => None,
-                _ => Some(cbor_value_to_dhall(v)?),
-            };
-            Ok((Label::from(k.as_ref()), v))
-        })
-        .collect::<Result<_, _>>()
-}
-
-enum Serialize<'a, E> {
-    Expr(&'a Expr<E>),
-    CBOR(cbor::Value),
-    RecordMap(&'a DupTreeMap<Label, Expr<E>>),
-    UnionMap(&'a DupTreeMap<Label, Option<Expr<E>>>),
-}
-
-macro_rules! count {
-    (@replace_with $_t:tt $sub:expr) => { $sub };
-    ($($tts:tt)*) => {0usize $(+ count!(@replace_with $tts 1usize))*};
-}
-
-macro_rules! ser_seq {
-    ($ser:expr; $($elt:expr),* $(,)?) => {{
-        use serde::ser::SerializeSeq;
-        let count = count!($($elt)*);
-        let mut ser_seq = $ser.serialize_seq(Some(count))?;
-        $(
-            ser_seq.serialize_element(&$elt)?;
-        )*
-        ser_seq.end()
-    }};
-}
-
-fn serialize_subexpr<S, E>(ser: S, e: &Expr<E>) -> Result<S::Ok, S::Error>
-where
-    S: serde::ser::Serializer,
-{
-    use cbor::Value::{String, I64, U64};
-    use crate::syntax::Builtin;
-    use crate::syntax::ExprF::*;
-    use std::iter::once;
-
-    use self::Serialize::{RecordMap, UnionMap};
-    fn expr<E>(x: &Expr<E>) -> self::Serialize<'_, E> {
-        self::Serialize::Expr(x)
-    }
-    let cbor =
-        |v: cbor::Value| -> self::Serialize<'_, E> { self::Serialize::CBOR(v) };
-    let tag = |x: u64| cbor(U64(x));
-    let null = || cbor(cbor::Value::Null);
-    let label = |l: &Label| cbor(cbor::Value::String(l.into()));
-
-    match e.as_ref() {
-        Const(c) => ser.serialize_str(&c.to_string()),
-        Builtin(b) => ser.serialize_str(&b.to_string()),
-        BoolLit(b) => ser.serialize_bool(*b),
-        NaturalLit(n) => ser_seq!(ser; tag(15), U64(*n as u64)),
-        IntegerLit(n) => ser_seq!(ser; tag(16), I64(*n as i64)),
-        DoubleLit(n) => {
-            let n: f64 = (*n).into();
-            ser.serialize_f64(n)
-        }
-        BoolIf(x, y, z) => ser_seq!(ser; tag(14), expr(x), expr(y), expr(z)),
-        Var(V(l, n)) if l == &"_".into() => ser.serialize_u64(*n as u64),
-        Var(V(l, n)) => ser_seq!(ser; label(l), U64(*n as u64)),
-        Lam(l, x, y) if l == &"_".into() => {
-            ser_seq!(ser; tag(1), expr(x), expr(y))
-        }
-        Lam(l, x, y) => ser_seq!(ser; tag(1), label(l), expr(x), expr(y)),
-        Pi(l, x, y) if l == &"_".into() => {
-            ser_seq!(ser; tag(2), expr(x), expr(y))
-        }
-        Pi(l, x, y) => ser_seq!(ser; tag(2), label(l), expr(x), expr(y)),
-        Let(_, _, _, _) => {
-            let (bound_e, bindings) = collect_nested_lets(e);
-            let count = 1 + 3 * bindings.len() + 1;
-
-            use serde::ser::SerializeSeq;
-            let mut ser_seq = ser.serialize_seq(Some(count))?;
-            ser_seq.serialize_element(&tag(25))?;
-            for (l, t, v) in bindings {
-                ser_seq.serialize_element(&label(l))?;
-                match t {
-                    Some(t) => ser_seq.serialize_element(&expr(t))?,
-                    None => ser_seq.serialize_element(&null())?,
-                }
-                ser_seq.serialize_element(&expr(v))?;
-            }
-            ser_seq.serialize_element(&expr(bound_e))?;
-            ser_seq.end()
-        }
-        App(_, _) => {
-            let (f, args) = collect_nested_applications(e);
-            ser.collect_seq(
-                once(tag(0))
-                    .chain(once(expr(f)))
-                    .chain(args.into_iter().rev().map(expr)),
-            )
-        }
-        Annot(x, y) => ser_seq!(ser; tag(26), expr(x), expr(y)),
-        Assert(x) => ser_seq!(ser; tag(19), expr(x)),
-        SomeLit(x) => ser_seq!(ser; tag(5), null(), expr(x)),
-        EmptyListLit(x) => match x.as_ref() {
-            App(f, a) => match f.as_ref() {
-                ExprF::Builtin(Builtin::List) => ser_seq!(ser; tag(4), expr(a)),
-                _ => ser_seq!(ser; tag(28), expr(x)),
-            },
-            _ => ser_seq!(ser; tag(28), expr(x)),
-        },
-        NEListLit(xs) => ser.collect_seq(
-            once(tag(4)).chain(once(null())).chain(xs.iter().map(expr)),
-        ),
-        TextLit(xs) => {
-            use crate::syntax::InterpolatedTextContents::{Expr, Text};
-            ser.collect_seq(once(tag(18)).chain(xs.iter().map(|x| match x {
-                Expr(x) => expr(x),
-                Text(x) => cbor(String(x.clone())),
-            })))
-        }
-        RecordType(map) => ser_seq!(ser; tag(7), RecordMap(map)),
-        RecordLit(map) => ser_seq!(ser; tag(8), RecordMap(map)),
-        UnionType(map) => ser_seq!(ser; tag(11), UnionMap(map)),
-        Field(x, l) => ser_seq!(ser; tag(9), expr(x), label(l)),
-        BinOp(op, x, y) => {
-            use crate::syntax::BinOp::*;
-            let op = match op {
-                BoolOr => 0,
-                BoolAnd => 1,
-                BoolEQ => 2,
-                BoolNE => 3,
-                NaturalPlus => 4,
-                NaturalTimes => 5,
-                TextAppend => 6,
-                ListAppend => 7,
-                RecursiveRecordMerge => 8,
-                RightBiasedRecordMerge => 9,
-                RecursiveRecordTypeMerge => 10,
-                ImportAlt => 11,
-                Equivalence => 12,
-            };
-            ser_seq!(ser; tag(3), U64(op), expr(x), expr(y))
-        }
-        Merge(x, y, None) => ser_seq!(ser; tag(6), expr(x), expr(y)),
-        Merge(x, y, Some(z)) => {
-            ser_seq!(ser; tag(6), expr(x), expr(y), expr(z))
-        }
-        ToMap(x, None) => ser_seq!(ser; tag(27), expr(x)),
-        ToMap(x, Some(y)) => ser_seq!(ser; tag(27), expr(x), expr(y)),
-        Projection(x, ls) => ser.collect_seq(
-            once(tag(10))
-                .chain(once(expr(x)))
-                .chain(ls.iter().map(label)),
-        ),
-        ProjectionByExpr(x, y) => {
-            ser_seq!(ser; tag(10), expr(x), vec![expr(y)])
-        }
-        Import(import) => serialize_import(ser, import),
-        Embed(_) => unimplemented!(
-            "An expression with resolved imports cannot be binary-encoded"
-        ),
-    }
-}
-
-fn serialize_import<S, E>(
-    ser: S,
-    import: &Import<Expr<E>>,
-) -> Result<S::Ok, S::Error>
-where
-    S: serde::ser::Serializer,
-{
-    use cbor::Value::{Bytes, Null, U64};
-    use serde::ser::SerializeSeq;
-
-    let count = 4 + match &import.location {
-        ImportLocation::Remote(url) => 3 + url.path.file_path.len(),
-        ImportLocation::Local(_, path) => path.file_path.len(),
-        ImportLocation::Env(_) => 1,
-        ImportLocation::Missing => 0,
-    };
-    let mut ser_seq = ser.serialize_seq(Some(count))?;
-
-    ser_seq.serialize_element(&U64(24))?;
-
-    let hash = match &import.hash {
-        None => Null,
-        Some(Hash::SHA256(h)) => {
-            let mut bytes = vec![18, 32];
-            bytes.extend_from_slice(h);
-            Bytes(bytes)
-        }
-    };
-    ser_seq.serialize_element(&hash)?;
-
-    let mode = match import.mode {
-        ImportMode::Code => 0,
-        ImportMode::RawText => 1,
-        ImportMode::Location => 2,
-    };
-    ser_seq.serialize_element(&U64(mode))?;
-
-    let scheme = match &import.location {
-        ImportLocation::Remote(url) => match url.scheme {
-            Scheme::HTTP => 0,
-            Scheme::HTTPS => 1,
-        },
-        ImportLocation::Local(prefix, _) => match prefix {
-            FilePrefix::Absolute => 2,
-            FilePrefix::Here => 3,
-            FilePrefix::Parent => 4,
-            FilePrefix::Home => 5,
-        },
-        ImportLocation::Env(_) => 6,
-        ImportLocation::Missing => 7,
-    };
-    ser_seq.serialize_element(&U64(scheme))?;
-
-    match &import.location {
-        ImportLocation::Remote(url) => {
-            match &url.headers {
-                None => ser_seq.serialize_element(&Null)?,
-                Some(e) => {
-                    ser_seq.serialize_element(&self::Serialize::Expr(e))?
-                }
-            };
-            ser_seq.serialize_element(&url.authority)?;
-            for p in url.path.file_path.iter() {
-                ser_seq.serialize_element(&p)?;
-            }
-            match &url.query {
-                None => ser_seq.serialize_element(&Null)?,
-                Some(x) => ser_seq.serialize_element(x)?,
-            };
-        }
-        ImportLocation::Local(_, path) => {
-            for p in path.file_path.iter() {
-                ser_seq.serialize_element(&p)?;
-            }
-        }
-        ImportLocation::Env(env) => {
-            ser_seq.serialize_element(env)?;
-        }
-        ImportLocation::Missing => {}
-    }
-
-    ser_seq.end()
-}
-
-impl<'a, E> serde::ser::Serialize for Serialize<'a, E> {
-    fn serialize<S>(&self, ser: S) -> Result<S::Ok, S::Error>
-    where
-        S: serde::ser::Serializer,
-    {
-        match self {
-            Serialize::Expr(e) => serialize_subexpr(ser, e),
-            Serialize::CBOR(v) => v.serialize(ser),
-            Serialize::RecordMap(map) => {
-                ser.collect_map(map.iter().map(|(k, v)| {
-                    (cbor::Value::String(k.into()), Serialize::Expr(v))
-                }))
-            }
-            Serialize::UnionMap(map) => {
-                ser.collect_map(map.iter().map(|(k, v)| {
-                    let v = match v {
-                        Some(x) => Serialize::Expr(x),
-                        None => Serialize::CBOR(cbor::Value::Null),
-                    };
-                    (cbor::Value::String(k.into()), v)
-                }))
-            }
-        }
-    }
-}
-
-fn collect_nested_applications<'a, E>(
-    e: &'a Expr<E>,
-) -> (&'a Expr<E>, Vec<&'a Expr<E>>) {
-    fn go<'a, E>(e: &'a Expr<E>, vec: &mut Vec<&'a Expr<E>>) -> &'a Expr<E> {
-        match e.as_ref() {
-            ExprF::App(f, a) => {
-                vec.push(a);
-                go(f, vec)
-            }
-            _ => e,
-        }
-    }
-    let mut vec = vec![];
-    let e = go(e, &mut vec);
-    (e, vec)
-}
-
-type LetBinding<'a, E> = (&'a Label, &'a Option<Expr<E>>, &'a Expr<E>);
-
-fn collect_nested_lets<'a, E>(
-    e: &'a Expr<E>,
-) -> (&'a Expr<E>, Vec<LetBinding<'a, E>>) {
-    fn go<'a, E>(
-        e: &'a Expr<E>,
-        vec: &mut Vec<LetBinding<'a, E>>,
-    ) -> &'a Expr<E> {
-        match e.as_ref() {
-            ExprF::Let(l, t, v, e) => {
-                vec.push((l, t, v));
-                go(e, vec)
-            }
-            _ => e,
-        }
-    }
-    let mut vec = vec![];
-    let e = go(e, &mut vec);
-    (e, vec)
-}
diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs
deleted file mode 100644
index 918c4d0..0000000
--- a/dhall/src/phase/mod.rs
+++ /dev/null
@@ -1,254 +0,0 @@
-use std::fmt::Display;
-use std::path::Path;
-
-use crate::syntax::{Builtin, Const, Expr};
-
-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};
-
-use resolve::ImportRoot;
-
-pub(crate) mod binary;
-pub(crate) mod normalize;
-pub(crate) mod parse;
-pub(crate) mod resolve;
-pub(crate) mod typecheck;
-
-pub type ParsedExpr = Expr<Normalized>;
-pub type DecodedExpr = Expr<Normalized>;
-pub type ResolvedExpr = Expr<Normalized>;
-pub type NormalizedExpr = Expr<Normalized>;
-
-#[derive(Debug, Clone)]
-pub struct Parsed(ParsedExpr, ImportRoot);
-
-/// An expression where all imports have been resolved
-///
-/// Invariant: there must be no `Import` nodes or `ImportAlt` operations left.
-#[derive(Debug, Clone)]
-pub struct Resolved(ResolvedExpr);
-
-/// A typed expression
-#[derive(Debug, Clone)]
-pub struct Typed(Value);
-
-/// A normalized expression.
-///
-/// Invariant: the contained Typed expression must be in normal form,
-#[derive(Debug, Clone)]
-pub struct Normalized(Typed);
-
-impl Parsed {
-    pub fn parse_file(f: &Path) -> Result<Parsed, Error> {
-        parse::parse_file(f)
-    }
-    pub fn parse_str(s: &str) -> Result<Parsed, Error> {
-        parse::parse_str(s)
-    }
-    pub fn parse_binary_file(f: &Path) -> Result<Parsed, Error> {
-        parse::parse_binary_file(f)
-    }
-    pub fn parse_binary(data: &[u8]) -> Result<Parsed, Error> {
-        parse::parse_binary(data)
-    }
-
-    pub fn resolve(self) -> Result<Resolved, ImportError> {
-        resolve::resolve(self)
-    }
-    pub fn skip_resolve(self) -> Result<Resolved, ImportError> {
-        resolve::skip_resolve_expr(self)
-    }
-
-    pub fn encode(&self) -> Result<Vec<u8>, EncodeError> {
-        crate::phase::binary::encode(&self.0)
-    }
-}
-
-impl Resolved {
-    pub fn typecheck(self) -> Result<Typed, TypeError> {
-        Ok(typecheck::typecheck(self.0)?.into_typed())
-    }
-    pub fn typecheck_with(self, ty: &Typed) -> Result<Typed, TypeError> {
-        Ok(typecheck::typecheck_with(self.0, ty.normalize_to_expr())?
-            .into_typed())
-    }
-}
-
-impl Typed {
-    /// 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(mut self) -> Normalized {
-        self.normalize_mut();
-        Normalized(self)
-    }
-
-    pub(crate) fn from_const(c: Const) -> Self {
-        Typed(Value::from_const(c))
-    }
-    pub(crate) fn from_valuef_and_type(v: ValueF, t: Typed) -> Self {
-        Typed(Value::from_valuef_and_type(v, t.into_value()))
-    }
-    pub(crate) fn from_value(th: Value) -> Self {
-        Typed(th)
-    }
-    pub(crate) fn const_type() -> Self {
-        Typed::from_const(Const::Type)
-    }
-
-    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()
-    }
-    pub(crate) fn into_value(self) -> Value {
-        self.0
-    }
-
-    pub(crate) fn normalize_mut(&mut self) {
-        self.0.normalize_mut()
-    }
-
-    pub(crate) fn get_type(&self) -> Result<Typed, TypeError> {
-        Ok(self.0.get_type()?.into_typed())
-    }
-
-    pub fn make_builtin_type(b: Builtin) -> Self {
-        Typed::from_value(Value::from_builtin(b))
-    }
-    pub fn make_optional_type(t: Typed) -> Self {
-        Typed::from_value(
-            Value::from_builtin(Builtin::Optional).app(t.to_value()),
-        )
-    }
-    pub fn make_list_type(t: Typed) -> Self {
-        Typed::from_value(Value::from_builtin(Builtin::List).app(t.to_value()))
-    }
-    pub fn make_record_type(
-        kts: impl Iterator<Item = (String, Typed)>,
-    ) -> Self {
-        Typed::from_valuef_and_type(
-            ValueF::RecordType(
-                kts.map(|(k, t)| (k.into(), t.into_value())).collect(),
-            ),
-            Typed::const_type(),
-        )
-    }
-    pub fn make_union_type(
-        kts: impl Iterator<Item = (String, Option<Typed>)>,
-    ) -> Self {
-        Typed::from_valuef_and_type(
-            ValueF::UnionType(
-                kts.map(|(k, t)| (k.into(), t.map(|t| t.into_value())))
-                    .collect(),
-            ),
-            Typed::const_type(),
-        )
-    }
-}
-
-impl Normalized {
-    pub fn encode(&self) -> Result<Vec<u8>, EncodeError> {
-        crate::phase::binary::encode(&self.to_expr())
-    }
-
-    pub(crate) fn to_expr(&self) -> NormalizedExpr {
-        self.0.normalize_to_expr()
-    }
-    pub(crate) fn to_expr_alpha(&self) -> NormalizedExpr {
-        self.0.normalize_to_expr_alpha()
-    }
-    pub(crate) fn into_typed(self) -> Typed {
-        self.0
-    }
-}
-
-impl Shift for Typed {
-    fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
-        Some(Typed(self.0.shift(delta, var)?))
-    }
-}
-
-impl Shift for Normalized {
-    fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
-        Some(Normalized(self.0.shift(delta, var)?))
-    }
-}
-
-impl Subst<Value> for Typed {
-    fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
-        Typed(self.0.subst_shift(var, val))
-    }
-}
-
-macro_rules! derive_traits_for_wrapper_struct {
-    ($ty:ident) => {
-        impl std::cmp::PartialEq for $ty {
-            fn eq(&self, other: &Self) -> bool {
-                self.0 == other.0
-            }
-        }
-
-        impl std::cmp::Eq for $ty {}
-
-        impl std::fmt::Display for $ty {
-            fn fmt(
-                &self,
-                f: &mut std::fmt::Formatter,
-            ) -> Result<(), std::fmt::Error> {
-                self.0.fmt(f)
-            }
-        }
-    };
-}
-
-derive_traits_for_wrapper_struct!(Parsed);
-derive_traits_for_wrapper_struct!(Resolved);
-derive_traits_for_wrapper_struct!(Normalized);
-
-impl std::hash::Hash for Normalized {
-    fn hash<H>(&self, state: &mut H)
-    where
-        H: std::hash::Hasher,
-    {
-        if let Ok(vec) = self.encode() {
-            vec.hash(state)
-        }
-    }
-}
-
-impl Eq for Typed {}
-impl PartialEq for Typed {
-    fn eq(&self, other: &Self) -> bool {
-        self.0 == other.0
-    }
-}
-
-impl Display for Typed {
-    fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> {
-        self.to_expr().fmt(f)
-    }
-}
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
deleted file mode 100644
index 3ed53f4..0000000
--- a/dhall/src/phase/normalize.rs
+++ /dev/null
@@ -1,794 +0,0 @@
-use std::collections::HashMap;
-
-use crate::syntax::Const::Type;
-use crate::syntax::{
-    BinOp, Builtin, ExprF, InterpolatedText, InterpolatedTextContents, Label,
-    NaiveDouble,
-};
-
-use crate::core::value::Value;
-use crate::core::valuef::ValueF;
-use crate::core::var::{AlphaLabel, Shift, Subst};
-use crate::phase::Normalized;
-
-// Ad-hoc macro to help construct closures
-macro_rules! make_closure {
-    (#$var:ident) => { $var.clone() };
-    (var($var:ident, $n:expr, $($ty:tt)*)) => {{
-        let var = crate::core::var::AlphaVar::from_var_and_alpha(
-            Label::from(stringify!($var)).into(),
-            $n
-        );
-        ValueF::Var(var)
-            .into_value_with_type(make_closure!($($ty)*))
-    }};
-    // Warning: assumes that $ty, as a dhall value, has type `Type`
-    (λ($var:ident : $($ty:tt)*) -> $($body:tt)*) => {{
-        let var: AlphaLabel = Label::from(stringify!($var)).into();
-        let ty = make_closure!($($ty)*);
-        let body = make_closure!($($body)*);
-        let body_ty = body.get_type_not_sort();
-        let lam_ty = ValueF::Pi(var.clone(), ty.clone(), body_ty)
-            .into_value_with_type(Value::from_const(Type));
-        ValueF::Lam(var, ty, body).into_value_with_type(lam_ty)
-    }};
-    (Natural) => {
-        Value::from_builtin(Builtin::Natural)
-    };
-    (List $($rest:tt)*) => {
-        Value::from_builtin(Builtin::List)
-            .app(make_closure!($($rest)*))
-    };
-    (Some($($rest:tt)*)) => {{
-        let v = make_closure!($($rest)*);
-        let v_type = v.get_type_not_sort();
-        let opt_v_type = Value::from_builtin(Builtin::Optional).app(v_type);
-        ValueF::NEOptionalLit(v).into_value_with_type(opt_v_type)
-    }};
-    (1 + $($rest:tt)*) => {
-        ValueF::PartialExpr(ExprF::BinOp(
-            crate::syntax::BinOp::NaturalPlus,
-            make_closure!($($rest)*),
-            Value::from_valuef_and_type(
-                ValueF::NaturalLit(1),
-                make_closure!(Natural)
-            ),
-        )).into_value_with_type(
-            make_closure!(Natural)
-        )
-    };
-    ([ $($head:tt)* ] # $($tail:tt)*) => {{
-        let head = make_closure!($($head)*);
-        let tail = make_closure!($($tail)*);
-        let list_type = tail.get_type_not_sort();
-        ValueF::PartialExpr(ExprF::BinOp(
-            crate::syntax::BinOp::ListAppend,
-            ValueF::NEListLit(vec![head])
-                .into_value_with_type(list_type.clone()),
-            tail,
-        )).into_value_with_type(list_type)
-    }};
-}
-
-#[allow(clippy::cognitive_complexity)]
-pub(crate) fn apply_builtin(
-    b: Builtin,
-    args: Vec<Value>,
-    ty: &Value,
-) -> ValueF {
-    use crate::syntax::Builtin::*;
-    use ValueF::*;
-
-    // Small helper enum
-    enum Ret<'a> {
-        ValueF(ValueF),
-        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 ret = match (b, args.as_slice()) {
-        (OptionalNone, [t]) => Ret::ValueF(EmptyOptionalLit(t.clone())),
-        (NaturalIsZero, [n]) => match &*n.as_whnf() {
-            NaturalLit(n) => Ret::ValueF(BoolLit(*n == 0)),
-            _ => Ret::DoneAsIs,
-        },
-        (NaturalEven, [n]) => match &*n.as_whnf() {
-            NaturalLit(n) => Ret::ValueF(BoolLit(*n % 2 == 0)),
-            _ => Ret::DoneAsIs,
-        },
-        (NaturalOdd, [n]) => match &*n.as_whnf() {
-            NaturalLit(n) => Ret::ValueF(BoolLit(*n % 2 != 0)),
-            _ => Ret::DoneAsIs,
-        },
-        (NaturalToInteger, [n]) => match &*n.as_whnf() {
-            NaturalLit(n) => Ret::ValueF(IntegerLit(*n as isize)),
-            _ => Ret::DoneAsIs,
-        },
-        (NaturalShow, [n]) => match &*n.as_whnf() {
-            NaturalLit(n) => {
-                Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text(
-                    n.to_string(),
-                )]))
-            }
-            _ => Ret::DoneAsIs,
-        },
-        (NaturalSubtract, [a, b]) => match (&*a.as_whnf(), &*b.as_whnf()) {
-            (NaturalLit(a), NaturalLit(b)) => {
-                Ret::ValueF(NaturalLit(if b > a { b - a } else { 0 }))
-            }
-            (NaturalLit(0), _) => Ret::Value(b.clone()),
-            (_, NaturalLit(0)) => Ret::ValueF(NaturalLit(0)),
-            _ if a == b => Ret::ValueF(NaturalLit(0)),
-            _ => Ret::DoneAsIs,
-        },
-        (IntegerShow, [n]) => match &*n.as_whnf() {
-            IntegerLit(n) => {
-                let s = if *n < 0 {
-                    n.to_string()
-                } else {
-                    format!("+{}", n)
-                };
-                Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text(s)]))
-            }
-            _ => Ret::DoneAsIs,
-        },
-        (IntegerToDouble, [n]) => match &*n.as_whnf() {
-            IntegerLit(n) => {
-                Ret::ValueF(DoubleLit(NaiveDouble::from(*n as f64)))
-            }
-            _ => Ret::DoneAsIs,
-        },
-        (DoubleShow, [n]) => match &*n.as_whnf() {
-            DoubleLit(n) => {
-                Ret::ValueF(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::ValueF(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::ValueF(TextLit(vec![
-                            InterpolatedTextContents::Text(s),
-                        ]))
-                    }
-                    _ => Ret::DoneAsIs,
-                }
-            }
-            _ => Ret::DoneAsIs,
-        },
-        (ListLength, [_, l]) => match &*l.as_whnf() {
-            EmptyListLit(_) => Ret::ValueF(NaturalLit(0)),
-            NEListLit(xs) => Ret::ValueF(NaturalLit(xs.len())),
-            _ => Ret::DoneAsIs,
-        },
-        (ListHead, [_, l]) => match &*l.as_whnf() {
-            EmptyListLit(n) => Ret::ValueF(EmptyOptionalLit(n.clone())),
-            NEListLit(xs) => {
-                Ret::ValueF(NEOptionalLit(xs.iter().next().unwrap().clone()))
-            }
-            _ => Ret::DoneAsIs,
-        },
-        (ListLast, [_, l]) => match &*l.as_whnf() {
-            EmptyListLit(n) => Ret::ValueF(EmptyOptionalLit(n.clone())),
-            NEListLit(xs) => Ret::ValueF(NEOptionalLit(
-                xs.iter().rev().next().unwrap().clone(),
-            )),
-            _ => Ret::DoneAsIs,
-        },
-        (ListReverse, [_, l]) => match &*l.as_whnf() {
-            EmptyListLit(n) => Ret::ValueF(EmptyListLit(n.clone())),
-            NEListLit(xs) => {
-                Ret::ValueF(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_valuef_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_valuef_and_type(
-                                            NaturalLit(i),
-                                            Value::from_builtin(
-                                                Builtin::Natural,
-                                            ),
-                                        ),
-                                    );
-                                    kvs.insert("value".into(), e.clone());
-                                    Value::from_valuef_and_type(
-                                        RecordLit(kvs),
-                                        t.clone(),
-                                    )
-                                })
-                                .collect(),
-                        ),
-                        _ => unreachable!(),
-                    };
-                    Ret::ValueF(list)
-                }
-                _ => Ret::DoneAsIs,
-            }
-        }
-        (ListBuild, [t, f]) => match &*f.as_whnf() {
-            // fold/build fusion
-            ValueF::AppliedBuiltin(ListFold, args) => {
-                if args.len() >= 2 {
-                    Ret::Value(args[1].clone())
-                } else {
-                    // Do we really need to handle this case ?
-                    unimplemented!()
-                }
-            }
-            _ => {
-                let list_t = Value::from_builtin(List).app(t.clone());
-                Ret::Value(
-                    f.app(list_t.clone())
-                        .app({
-                            // Move `t` under new variables
-                            let t1 = t.under_binder(Label::from("x"));
-                            let t2 = t1.under_binder(Label::from("xs"));
-                            make_closure!(
-                                λ(x : #t) ->
-                                λ(xs : List #t1) ->
-                                [ var(x, 1, #t2) ] # var(xs, 0, List #t2)
-                            )
-                        })
-                        .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]) => match &*f.as_whnf() {
-            // fold/build fusion
-            ValueF::AppliedBuiltin(OptionalFold, args) => {
-                if args.len() >= 2 {
-                    Ret::Value(args[1].clone())
-                } else {
-                    // Do we really need to handle this case ?
-                    unimplemented!()
-                }
-            }
-            _ => {
-                let optional_t = Value::from_builtin(Optional).app(t.clone());
-                Ret::Value(
-                    f.app(optional_t.clone())
-                        .app({
-                            let t1 = t.under_binder(Label::from("x"));
-                            make_closure!(λ(x: #t) -> Some(var(x, 0, #t1)))
-                        })
-                        .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]) => match &*f.as_whnf() {
-            // fold/build fusion
-            ValueF::AppliedBuiltin(NaturalFold, args) => {
-                if !args.is_empty() {
-                    Ret::Value(args[0].clone())
-                } else {
-                    // Do we really need to handle this case ?
-                    unimplemented!()
-                }
-            }
-            _ => Ret::Value(
-                f.app(Value::from_builtin(Natural))
-                    .app(make_closure!(
-                        λ(x : Natural) -> 1 + var(x, 0, Natural)
-                    ))
-                    .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::ValueF(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),
-    }
-}
-
-pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueF {
-    let f_borrow = f.as_whnf();
-    match &*f_borrow {
-        ValueF::Lam(x, _, e) => {
-            e.subst_shift(&x.into(), &a).to_whnf_check_type(ty)
-        }
-        ValueF::AppliedBuiltin(b, args) => {
-            use std::iter::once;
-            let args = args.iter().cloned().chain(once(a.clone())).collect();
-            apply_builtin(*b, args, ty)
-        }
-        ValueF::UnionConstructor(l, kts) => {
-            ValueF::UnionLit(l.clone(), a, kts.clone())
-        }
-        _ => {
-            drop(f_borrow);
-            ValueF::PartialExpr(ExprF::App(f, a))
-        }
-    }
-}
-
-pub(crate) fn squash_textlit(
-    elts: impl Iterator<Item = InterpolatedTextContents<Value>>,
-) -> Vec<InterpolatedTextContents<Value>> {
-    use std::mem::replace;
-    use InterpolatedTextContents::{Expr, Text};
-
-    fn inner(
-        elts: impl Iterator<Item = InterpolatedTextContents<Value>>,
-        crnt_str: &mut String,
-        ret: &mut Vec<InterpolatedTextContents<Value>>,
-    ) {
-        for contents in elts {
-            match contents {
-                Text(s) => crnt_str.push_str(&s),
-                Expr(e) => {
-                    let e_borrow = e.as_whnf();
-                    match &*e_borrow {
-                        ValueF::TextLit(elts2) => {
-                            inner(elts2.iter().cloned(), crnt_str, ret)
-                        }
-                        _ => {
-                            drop(e_borrow);
-                            if !crnt_str.is_empty() {
-                                ret.push(Text(replace(crnt_str, String::new())))
-                            }
-                            ret.push(Expr(e.clone()))
-                        }
-                    }
-                }
-            }
-        }
-    }
-
-    let mut crnt_str = String::new();
-    let mut ret = Vec::new();
-    inner(elts, &mut crnt_str, &mut ret);
-    if !crnt_str.is_empty() {
-        ret.push(Text(replace(&mut crnt_str, String::new())))
-    }
-    ret
-}
-
-pub(crate) fn merge_maps<K, V, F, Err>(
-    map1: &HashMap<K, V>,
-    map2: &HashMap<K, V>,
-    mut f: F,
-) -> Result<HashMap<K, V>, Err>
-where
-    F: FnMut(&K, &V, &V) -> Result<V, Err>,
-    K: std::hash::Hash + Eq + Clone,
-    V: Clone,
-{
-    let mut kvs = HashMap::new();
-    for (x, v2) in map2 {
-        let newv = if let Some(v1) = map1.get(x) {
-            f(x, v1, v2)?
-        } else {
-            v2.clone()
-        };
-        kvs.insert(x.clone(), newv);
-    }
-    for (x, v1) in map1 {
-        // Insert only if key not already present
-        kvs.entry(x.clone()).or_insert_with(|| v1.clone());
-    }
-    Ok(kvs)
-}
-
-// Small helper enum to avoid repetition
-enum Ret<'a> {
-    ValueF(ValueF),
-    Value(Value),
-    ValueRef(&'a Value),
-    Expr(ExprF<Value, Normalized>),
-}
-
-fn apply_binop<'a>(
-    o: BinOp,
-    x: &'a Value,
-    y: &'a Value,
-    ty: &Value,
-) -> Option<Ret<'a>> {
-    use BinOp::{
-        BoolAnd, BoolEQ, BoolNE, BoolOr, Equivalence, ListAppend, NaturalPlus,
-        NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge,
-        RightBiasedRecordMerge, TextAppend,
-    };
-    use ValueF::{
-        BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType,
-        TextLit,
-    };
-    let x_borrow = x.as_whnf();
-    let y_borrow = y.as_whnf();
-    Some(match (o, &*x_borrow, &*y_borrow) {
-        (BoolAnd, BoolLit(true), _) => Ret::ValueRef(y),
-        (BoolAnd, _, BoolLit(true)) => Ret::ValueRef(x),
-        (BoolAnd, BoolLit(false), _) => Ret::ValueF(BoolLit(false)),
-        (BoolAnd, _, BoolLit(false)) => Ret::ValueF(BoolLit(false)),
-        (BoolAnd, _, _) if x == y => Ret::ValueRef(x),
-        (BoolOr, BoolLit(true), _) => Ret::ValueF(BoolLit(true)),
-        (BoolOr, _, BoolLit(true)) => Ret::ValueF(BoolLit(true)),
-        (BoolOr, BoolLit(false), _) => Ret::ValueRef(y),
-        (BoolOr, _, BoolLit(false)) => Ret::ValueRef(x),
-        (BoolOr, _, _) if x == y => Ret::ValueRef(x),
-        (BoolEQ, BoolLit(true), _) => Ret::ValueRef(y),
-        (BoolEQ, _, BoolLit(true)) => Ret::ValueRef(x),
-        (BoolEQ, BoolLit(x), BoolLit(y)) => Ret::ValueF(BoolLit(x == y)),
-        (BoolEQ, _, _) if x == y => Ret::ValueF(BoolLit(true)),
-        (BoolNE, BoolLit(false), _) => Ret::ValueRef(y),
-        (BoolNE, _, BoolLit(false)) => Ret::ValueRef(x),
-        (BoolNE, BoolLit(x), BoolLit(y)) => Ret::ValueF(BoolLit(x != y)),
-        (BoolNE, _, _) if x == y => Ret::ValueF(BoolLit(false)),
-
-        (NaturalPlus, NaturalLit(0), _) => Ret::ValueRef(y),
-        (NaturalPlus, _, NaturalLit(0)) => Ret::ValueRef(x),
-        (NaturalPlus, NaturalLit(x), NaturalLit(y)) => {
-            Ret::ValueF(NaturalLit(x + y))
-        }
-        (NaturalTimes, NaturalLit(0), _) => Ret::ValueF(NaturalLit(0)),
-        (NaturalTimes, _, NaturalLit(0)) => Ret::ValueF(NaturalLit(0)),
-        (NaturalTimes, NaturalLit(1), _) => Ret::ValueRef(y),
-        (NaturalTimes, _, NaturalLit(1)) => Ret::ValueRef(x),
-        (NaturalTimes, NaturalLit(x), NaturalLit(y)) => {
-            Ret::ValueF(NaturalLit(x * y))
-        }
-
-        (ListAppend, EmptyListLit(_), _) => Ret::ValueRef(y),
-        (ListAppend, _, EmptyListLit(_)) => Ret::ValueRef(x),
-        (ListAppend, NEListLit(xs), NEListLit(ys)) => Ret::ValueF(NEListLit(
-            xs.iter().chain(ys.iter()).cloned().collect(),
-        )),
-
-        (TextAppend, TextLit(x), _) if x.is_empty() => Ret::ValueRef(y),
-        (TextAppend, _, TextLit(y)) if y.is_empty() => Ret::ValueRef(x),
-        (TextAppend, TextLit(x), TextLit(y)) => Ret::ValueF(TextLit(
-            squash_textlit(x.iter().chain(y.iter()).cloned()),
-        )),
-        (TextAppend, TextLit(x), _) => {
-            use std::iter::once;
-            let y = InterpolatedTextContents::Expr(y.clone());
-            Ret::ValueF(TextLit(squash_textlit(
-                x.iter().cloned().chain(once(y)),
-            )))
-        }
-        (TextAppend, _, TextLit(y)) => {
-            use std::iter::once;
-            let x = InterpolatedTextContents::Expr(x.clone());
-            Ret::ValueF(TextLit(squash_textlit(
-                once(x).chain(y.iter().cloned()),
-            )))
-        }
-
-        (RightBiasedRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => {
-            Ret::ValueRef(x)
-        }
-        (RightBiasedRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => {
-            Ret::ValueRef(y)
-        }
-        (RightBiasedRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
-            let mut kvs = kvs2.clone();
-            for (x, v) in kvs1 {
-                // Insert only if key not already present
-                kvs.entry(x.clone()).or_insert_with(|| v.clone());
-            }
-            Ret::ValueF(RecordLit(kvs))
-        }
-
-        (RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => {
-            Ret::ValueRef(x)
-        }
-        (RecursiveRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => {
-            Ret::ValueRef(y)
-        }
-        (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
-            let ty_borrow = ty.as_whnf();
-            let kts = match &*ty_borrow {
-                RecordType(kts) => kts,
-                _ => unreachable!("Internal type error"),
-            };
-            let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |k, v1, v2| {
-                Ok(Value::from_valuef_and_type(
-                    ValueF::PartialExpr(ExprF::BinOp(
-                        RecursiveRecordMerge,
-                        v1.clone(),
-                        v2.clone(),
-                    )),
-                    kts.get(k).expect("Internal type error").clone(),
-                ))
-            })?;
-            Ret::ValueF(RecordLit(kvs))
-        }
-
-        (RecursiveRecordTypeMerge, _, _) | (Equivalence, _, _) => {
-            unreachable!("This case should have been handled in typecheck")
-        }
-
-        _ => return None,
-    })
-}
-
-pub(crate) fn normalize_one_layer(
-    expr: ExprF<Value, Normalized>,
-    ty: &Value,
-) -> ValueF {
-    use ValueF::{
-        AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit,
-        NEListLit, NEOptionalLit, NaturalLit, RecordLit, TextLit,
-        UnionConstructor, UnionLit, UnionType,
-    };
-
-    let ret = match expr {
-        ExprF::Import(_) => unreachable!(
-            "There should remain no imports in a resolved expression"
-        ),
-        // Those cases have already been completely handled in the typechecking phase (using
-        // `RetWhole`), so they won't appear here.
-        ExprF::Lam(_, _, _)
-        | ExprF::Pi(_, _, _)
-        | ExprF::Let(_, _, _, _)
-        | ExprF::Embed(_)
-        | ExprF::Const(_)
-        | ExprF::Builtin(_)
-        | ExprF::Var(_)
-        | ExprF::Annot(_, _)
-        | ExprF::RecordType(_)
-        | ExprF::UnionType(_) => {
-            unreachable!("This case should have been handled in typecheck")
-        }
-        ExprF::Assert(_) => Ret::Expr(expr),
-        ExprF::App(v, a) => Ret::Value(v.app(a)),
-        ExprF::BoolLit(b) => Ret::ValueF(BoolLit(b)),
-        ExprF::NaturalLit(n) => Ret::ValueF(NaturalLit(n)),
-        ExprF::IntegerLit(n) => Ret::ValueF(IntegerLit(n)),
-        ExprF::DoubleLit(n) => Ret::ValueF(DoubleLit(n)),
-        ExprF::SomeLit(e) => Ret::ValueF(NEOptionalLit(e)),
-        ExprF::EmptyListLit(ref t) => {
-            // Check if the type is of the form `List x`
-            let t_borrow = t.as_whnf();
-            match &*t_borrow {
-                AppliedBuiltin(Builtin::List, args) if args.len() == 1 => {
-                    Ret::ValueF(EmptyListLit(args[0].clone()))
-                }
-                _ => {
-                    drop(t_borrow);
-                    Ret::Expr(expr)
-                }
-            }
-        }
-        ExprF::NEListLit(elts) => {
-            Ret::ValueF(NEListLit(elts.into_iter().collect()))
-        }
-        ExprF::RecordLit(kvs) => {
-            Ret::ValueF(RecordLit(kvs.into_iter().collect()))
-        }
-        ExprF::TextLit(elts) => {
-            use InterpolatedTextContents::Expr;
-            let elts: Vec<_> = squash_textlit(elts.into_iter());
-            // Simplify bare interpolation
-            if let [Expr(th)] = elts.as_slice() {
-                Ret::Value(th.clone())
-            } else {
-                Ret::ValueF(TextLit(elts))
-            }
-        }
-        ExprF::BoolIf(ref b, ref e1, ref e2) => {
-            let b_borrow = b.as_whnf();
-            match &*b_borrow {
-                BoolLit(true) => Ret::ValueRef(e1),
-                BoolLit(false) => Ret::ValueRef(e2),
-                _ => {
-                    let e1_borrow = e1.as_whnf();
-                    let e2_borrow = e2.as_whnf();
-                    match (&*e1_borrow, &*e2_borrow) {
-                        // Simplify `if b then True else False`
-                        (BoolLit(true), BoolLit(false)) => Ret::ValueRef(b),
-                        _ if e1 == e2 => Ret::ValueRef(e1),
-                        _ => {
-                            drop(b_borrow);
-                            drop(e1_borrow);
-                            drop(e2_borrow);
-                            Ret::Expr(expr)
-                        }
-                    }
-                }
-            }
-        }
-        ExprF::BinOp(o, ref x, ref y) => match apply_binop(o, x, y, ty) {
-            Some(ret) => ret,
-            None => Ret::Expr(expr),
-        },
-
-        ExprF::Projection(_, ref ls) if ls.is_empty() => {
-            Ret::ValueF(RecordLit(HashMap::new()))
-        }
-        ExprF::Projection(ref v, ref ls) => {
-            let v_borrow = v.as_whnf();
-            match &*v_borrow {
-                RecordLit(kvs) => Ret::ValueF(RecordLit(
-                    ls.iter()
-                        .filter_map(|l| {
-                            kvs.get(l).map(|x| (l.clone(), x.clone()))
-                        })
-                        .collect(),
-                )),
-                _ => {
-                    drop(v_borrow);
-                    Ret::Expr(expr)
-                }
-            }
-        }
-        ExprF::Field(ref v, ref l) => {
-            let v_borrow = v.as_whnf();
-            match &*v_borrow {
-                RecordLit(kvs) => match kvs.get(l) {
-                    Some(r) => Ret::Value(r.clone()),
-                    None => {
-                        drop(v_borrow);
-                        Ret::Expr(expr)
-                    }
-                },
-                UnionType(kts) => {
-                    Ret::ValueF(UnionConstructor(l.clone(), kts.clone()))
-                }
-                _ => {
-                    drop(v_borrow);
-                    Ret::Expr(expr)
-                }
-            }
-        }
-        ExprF::ProjectionByExpr(_, _) => {
-            unimplemented!("selection by expression")
-        }
-
-        ExprF::Merge(ref handlers, ref variant, _) => {
-            let handlers_borrow = handlers.as_whnf();
-            let variant_borrow = variant.as_whnf();
-            match (&*handlers_borrow, &*variant_borrow) {
-                (RecordLit(kvs), UnionConstructor(l, _)) => match kvs.get(l) {
-                    Some(h) => Ret::Value(h.clone()),
-                    None => {
-                        drop(handlers_borrow);
-                        drop(variant_borrow);
-                        Ret::Expr(expr)
-                    }
-                },
-                (RecordLit(kvs), UnionLit(l, v, _)) => match kvs.get(l) {
-                    Some(h) => Ret::Value(h.app(v.clone())),
-                    None => {
-                        drop(handlers_borrow);
-                        drop(variant_borrow);
-                        Ret::Expr(expr)
-                    }
-                },
-                _ => {
-                    drop(handlers_borrow);
-                    drop(variant_borrow);
-                    Ret::Expr(expr)
-                }
-            }
-        }
-        ExprF::ToMap(_, _) => unimplemented!("toMap"),
-    };
-
-    match ret {
-        Ret::ValueF(v) => v,
-        Ret::Value(v) => v.to_whnf_check_type(ty),
-        Ret::ValueRef(v) => v.to_whnf_check_type(ty),
-        Ret::Expr(expr) => ValueF::PartialExpr(expr),
-    }
-}
-
-/// Normalize a ValueF into WHNF
-pub(crate) fn normalize_whnf(v: ValueF, ty: &Value) -> ValueF {
-    match v {
-        ValueF::AppliedBuiltin(b, args) => apply_builtin(b, args, ty),
-        ValueF::PartialExpr(e) => normalize_one_layer(e, ty),
-        ValueF::TextLit(elts) => {
-            ValueF::TextLit(squash_textlit(elts.into_iter()))
-        }
-        // All other cases are already in WHNF
-        v => v,
-    }
-}
diff --git a/dhall/src/phase/parse.rs b/dhall/src/phase/parse.rs
deleted file mode 100644
index e277e54..0000000
--- a/dhall/src/phase/parse.rs
+++ /dev/null
@@ -1,37 +0,0 @@
-use std::fs::File;
-use std::io::Read;
-use std::path::Path;
-
-use crate::syntax::parse_expr;
-
-use crate::error::Error;
-use crate::phase::resolve::ImportRoot;
-use crate::phase::Parsed;
-
-pub(crate) fn parse_file(f: &Path) -> Result<Parsed, Error> {
-    let mut buffer = String::new();
-    File::open(f)?.read_to_string(&mut buffer)?;
-    let expr = parse_expr(&*buffer)?;
-    let root = ImportRoot::LocalDir(f.parent().unwrap().to_owned());
-    Ok(Parsed(expr, root))
-}
-
-pub(crate) fn parse_str(s: &str) -> Result<Parsed, Error> {
-    let expr = parse_expr(s)?;
-    let root = ImportRoot::LocalDir(std::env::current_dir()?);
-    Ok(Parsed(expr, root))
-}
-
-pub(crate) fn parse_binary(data: &[u8]) -> Result<Parsed, Error> {
-    let expr = crate::phase::binary::decode(data)?;
-    let root = ImportRoot::LocalDir(std::env::current_dir()?);
-    Ok(Parsed(expr, root))
-}
-
-pub(crate) fn parse_binary_file(f: &Path) -> Result<Parsed, Error> {
-    let mut buffer = Vec::new();
-    File::open(f)?.read_to_end(&mut buffer)?;
-    let expr = crate::phase::binary::decode(&buffer)?;
-    let root = ImportRoot::LocalDir(f.parent().unwrap().to_owned());
-    Ok(Parsed(expr, root))
-}
diff --git a/dhall/src/phase/resolve.rs b/dhall/src/phase/resolve.rs
deleted file mode 100644
index 5920f82..0000000
--- a/dhall/src/phase/resolve.rs
+++ /dev/null
@@ -1,180 +0,0 @@
-use std::collections::HashMap;
-use std::path::{Path, PathBuf};
-
-use crate::error::{Error, ImportError};
-use crate::phase::{Normalized, NormalizedExpr, Parsed, Resolved};
-use crate::syntax::{FilePath, ImportLocation, URL};
-
-type Import = crate::syntax::Import<NormalizedExpr>;
-
-/// A root from which to resolve relative imports.
-#[derive(Debug, Clone, PartialEq, Eq)]
-pub(crate) enum ImportRoot {
-    LocalDir(PathBuf),
-}
-
-type ImportCache = HashMap<Import, Normalized>;
-
-pub(crate) type ImportStack = Vec<Import>;
-
-fn resolve_import(
-    import: &Import,
-    root: &ImportRoot,
-    import_cache: &mut ImportCache,
-    import_stack: &ImportStack,
-) -> Result<Normalized, ImportError> {
-    use self::ImportRoot::*;
-    use crate::syntax::FilePrefix::*;
-    use crate::syntax::ImportLocation::*;
-    let cwd = match root {
-        LocalDir(cwd) => cwd,
-    };
-    match &import.location {
-        Local(prefix, path) => {
-            let path_buf: PathBuf = path.file_path.iter().collect();
-            let path_buf = match prefix {
-                // TODO: fail gracefully
-                Parent => cwd.parent().unwrap().join(path_buf),
-                Here => cwd.join(path_buf),
-                _ => unimplemented!("{:?}", import),
-            };
-            Ok(load_import(&path_buf, import_cache, import_stack).map_err(
-                |e| ImportError::Recursive(import.clone(), Box::new(e)),
-            )?)
-        }
-        _ => unimplemented!("{:?}", import),
-    }
-}
-
-fn load_import(
-    f: &Path,
-    import_cache: &mut ImportCache,
-    import_stack: &ImportStack,
-) -> Result<Normalized, Error> {
-    Ok(
-        do_resolve_expr(Parsed::parse_file(f)?, import_cache, import_stack)?
-            .typecheck()?
-            .normalize(),
-    )
-}
-
-fn do_resolve_expr(
-    parsed: Parsed,
-    import_cache: &mut ImportCache,
-    import_stack: &ImportStack,
-) -> Result<Resolved, ImportError> {
-    let Parsed(mut expr, root) = parsed;
-    let mut resolve = |import: Import| -> Result<Normalized, ImportError> {
-        if import_stack.contains(&import) {
-            return Err(ImportError::ImportCycle(import_stack.clone(), import));
-        }
-        match import_cache.get(&import) {
-            Some(expr) => Ok(expr.clone()),
-            None => {
-                // Copy the import stack and push the current import
-                let mut import_stack = import_stack.clone();
-                import_stack.push(import.clone());
-
-                // Resolve the import recursively
-                let expr = resolve_import(
-                    &import,
-                    &root,
-                    import_cache,
-                    &import_stack,
-                )?;
-
-                // Add the import to the cache
-                import_cache.insert(import, expr.clone());
-                Ok(expr)
-            }
-        }
-    };
-    expr.traverse_resolve_mut(&mut resolve)?;
-    Ok(Resolved(expr))
-}
-
-pub(crate) fn resolve(e: Parsed) -> Result<Resolved, ImportError> {
-    do_resolve_expr(e, &mut HashMap::new(), &Vec::new())
-}
-
-pub(crate) fn skip_resolve_expr(
-    parsed: Parsed,
-) -> Result<Resolved, ImportError> {
-    let mut expr = parsed.0;
-    let mut resolve = |import: Import| -> Result<Normalized, ImportError> {
-        Err(ImportError::UnexpectedImport(import))
-    };
-    expr.traverse_resolve_mut(&mut resolve)?;
-    Ok(Resolved(expr))
-}
-
-pub trait Canonicalize {
-    fn canonicalize(&self) -> Self;
-}
-
-impl Canonicalize for FilePath {
-    fn canonicalize(&self) -> FilePath {
-        let mut file_path = Vec::new();
-        let mut file_path_components = self.file_path.clone().into_iter();
-
-        loop {
-            let component = file_path_components.next();
-            match component.as_ref() {
-                // ───────────────────
-                // canonicalize(ε) = ε
-                None => break,
-
-                // canonicalize(directory₀) = directory₁
-                // ───────────────────────────────────────
-                // canonicalize(directory₀/.) = directory₁
-                Some(c) if c == "." => continue,
-
-                Some(c) if c == ".." => match file_path_components.next() {
-                    // canonicalize(directory₀) = ε
-                    // ────────────────────────────
-                    // canonicalize(directory₀/..) = /..
-                    None => file_path.push("..".to_string()),
-
-                    // canonicalize(directory₀) = directory₁/..
-                    // ──────────────────────────────────────────────
-                    // canonicalize(directory₀/..) = directory₁/../..
-                    Some(ref c) if c == ".." => {
-                        file_path.push("..".to_string());
-                        file_path.push("..".to_string());
-                    }
-
-                    // canonicalize(directory₀) = directory₁/component
-                    // ───────────────────────────────────────────────  ; If "component" is not
-                    // canonicalize(directory₀/..) = directory₁         ; ".."
-                    Some(_) => continue,
-                },
-
-                // canonicalize(directory₀) = directory₁
-                // ─────────────────────────────────────────────────────────  ; If no other
-                // canonicalize(directory₀/component) = directory₁/component  ; rule matches
-                Some(c) => file_path.push(c.clone()),
-            }
-        }
-
-        FilePath { file_path }
-    }
-}
-
-impl<SE: Copy> Canonicalize for ImportLocation<SE> {
-    fn canonicalize(&self) -> ImportLocation<SE> {
-        match self {
-            ImportLocation::Local(prefix, file) => {
-                ImportLocation::Local(*prefix, file.canonicalize())
-            }
-            ImportLocation::Remote(url) => ImportLocation::Remote(URL {
-                scheme: url.scheme,
-                authority: url.authority.clone(),
-                path: url.path.canonicalize(),
-                query: url.query.clone(),
-                headers: url.headers.clone(),
-            }),
-            ImportLocation::Env(name) => ImportLocation::Env(name.to_string()),
-            ImportLocation::Missing => ImportLocation::Missing,
-        }
-    }
-}
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
deleted file mode 100644
index 9a41be9..0000000
--- a/dhall/src/phase/typecheck.rs
+++ /dev/null
@@ -1,815 +0,0 @@
-use std::cmp::max;
-use std::collections::HashMap;
-
-use crate::syntax::{
-    Builtin, Const, Expr, ExprF, InterpolatedTextContents, Label, RawExpr, Span,
-};
-
-use crate::core::context::TypecheckContext;
-use crate::core::value::Value;
-use crate::core::valuef::ValueF;
-use crate::core::var::{Shift, Subst};
-use crate::error::{TypeError, TypeMessage};
-use crate::phase::Normalized;
-
-fn tck_pi_type(
-    ctx: &TypecheckContext,
-    x: Label,
-    tx: Value,
-    te: Value,
-) -> Result<Value, TypeError> {
-    use crate::error::TypeMessage::*;
-    let ctx2 = ctx.insert_type(&x, tx.clone());
-
-    let ka = match tx.get_type()?.as_const() {
-        Some(k) => k,
-        _ => return Err(TypeError::new(ctx, InvalidInputType(tx))),
-    };
-
-    let kb = match te.get_type()?.as_const() {
-        Some(k) => k,
-        _ => {
-            return Err(TypeError::new(
-                &ctx2,
-                InvalidOutputType(te.get_type()?),
-            ))
-        }
-    };
-
-    let k = function_check(ka, kb);
-
-    Ok(Value::from_valuef_and_type(
-        ValueF::Pi(x.into(), tx, te),
-        Value::from_const(k),
-    ))
-}
-
-fn tck_record_type(
-    ctx: &TypecheckContext,
-    kts: impl IntoIterator<Item = Result<(Label, Value), TypeError>>,
-) -> Result<Value, TypeError> {
-    use crate::error::TypeMessage::*;
-    use std::collections::hash_map::Entry;
-    let mut new_kts = HashMap::new();
-    // An empty record type has type Type
-    let mut k = Const::Type;
-    for e in kts {
-        let (x, t) = e?;
-        // Construct the union of the contained `Const`s
-        match t.get_type()?.as_const() {
-            Some(k2) => k = max(k, k2),
-            None => return Err(TypeError::new(ctx, InvalidFieldType(x, t))),
-        }
-        // Check for duplicated entries
-        let entry = new_kts.entry(x);
-        match &entry {
-            Entry::Occupied(_) => {
-                return Err(TypeError::new(ctx, RecordTypeDuplicateField))
-            }
-            Entry::Vacant(_) => entry.or_insert_with(|| t),
-        };
-    }
-
-    Ok(Value::from_valuef_and_type(
-        ValueF::RecordType(new_kts),
-        Value::from_const(k),
-    ))
-}
-
-fn tck_union_type<Iter>(
-    ctx: &TypecheckContext,
-    kts: Iter,
-) -> Result<Value, TypeError>
-where
-    Iter: IntoIterator<Item = Result<(Label, Option<Value>), TypeError>>,
-{
-    use crate::error::TypeMessage::*;
-    use std::collections::hash_map::Entry;
-    let mut new_kts = HashMap::new();
-    // Check that all types are the same const
-    let mut k = None;
-    for e in kts {
-        let (x, t) = e?;
-        if let Some(t) = &t {
-            match (k, t.get_type()?.as_const()) {
-                (None, Some(k2)) => k = Some(k2),
-                (Some(k1), Some(k2)) if k1 == k2 => {}
-                _ => {
-                    return Err(TypeError::new(
-                        ctx,
-                        InvalidFieldType(x, t.clone()),
-                    ))
-                }
-            }
-        }
-        let entry = new_kts.entry(x);
-        match &entry {
-            Entry::Occupied(_) => {
-                return Err(TypeError::new(ctx, UnionTypeDuplicateField))
-            }
-            Entry::Vacant(_) => entry.or_insert_with(|| t),
-        };
-    }
-
-    // An empty union type has type Type;
-    // an union type with only unary variants also has type Type
-    let k = k.unwrap_or(Const::Type);
-
-    Ok(Value::from_valuef_and_type(
-        ValueF::UnionType(new_kts),
-        Value::from_const(k),
-    ))
-}
-
-fn function_check(a: Const, b: Const) -> Const {
-    if b == Const::Type {
-        Const::Type
-    } else {
-        max(a, b)
-    }
-}
-
-pub(crate) fn const_to_value(c: Const) -> Value {
-    let v = ValueF::Const(c);
-    match c {
-        Const::Type => {
-            Value::from_valuef_and_type(v, const_to_value(Const::Kind))
-        }
-        Const::Kind => {
-            Value::from_valuef_and_type(v, const_to_value(Const::Sort))
-        }
-        Const::Sort => Value::const_sort(),
-    }
-}
-
-pub fn rc<E>(x: RawExpr<E>) -> Expr<E> {
-    Expr::new(x, Span::Artificial)
-}
-
-// Ad-hoc macro to help construct the types of builtins
-macro_rules! make_type {
-    (Type) => { ExprF::Const(Const::Type) };
-    (Bool) => { ExprF::Builtin(Builtin::Bool) };
-    (Natural) => { ExprF::Builtin(Builtin::Natural) };
-    (Integer) => { ExprF::Builtin(Builtin::Integer) };
-    (Double) => { ExprF::Builtin(Builtin::Double) };
-    (Text) => { ExprF::Builtin(Builtin::Text) };
-    ($var:ident) => {
-        ExprF::Var(crate::syntax::V(stringify!($var).into(), 0))
-    };
-    (Optional $ty:ident) => {
-        ExprF::App(
-            rc(ExprF::Builtin(Builtin::Optional)),
-            rc(make_type!($ty))
-        )
-    };
-    (List $($rest:tt)*) => {
-        ExprF::App(
-            rc(ExprF::Builtin(Builtin::List)),
-            rc(make_type!($($rest)*))
-        )
-    };
-    ({ $($label:ident : $ty:ident),* }) => {{
-        let mut kts = crate::syntax::map::DupTreeMap::new();
-        $(
-            kts.insert(
-                Label::from(stringify!($label)),
-                rc(make_type!($ty)),
-            );
-        )*
-        ExprF::RecordType(kts)
-    }};
-    ($ty:ident -> $($rest:tt)*) => {
-        ExprF::Pi(
-            "_".into(),
-            rc(make_type!($ty)),
-            rc(make_type!($($rest)*))
-        )
-    };
-    (($($arg:tt)*) -> $($rest:tt)*) => {
-        ExprF::Pi(
-            "_".into(),
-            rc(make_type!($($arg)*)),
-            rc(make_type!($($rest)*))
-        )
-    };
-    (forall ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => {
-        ExprF::Pi(
-            stringify!($var).into(),
-            rc(make_type!($($ty)*)),
-            rc(make_type!($($rest)*))
-        )
-    };
-}
-
-fn type_of_builtin<E>(b: Builtin) -> Expr<E> {
-    use crate::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),
-        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 {
-    let ctx = TypecheckContext::new();
-    Value::from_valuef_and_type(
-        ValueF::from_builtin(b),
-        type_with(&ctx, type_of_builtin(b)).unwrap(),
-    )
-}
-
-/// Type-check an expression and return the expression alongside its type if type-checking
-/// succeeded, or an error if type-checking failed.
-/// Some normalization is done while typechecking, so the returned expression might be partially
-/// normalized as well.
-fn type_with(
-    ctx: &TypecheckContext,
-    e: Expr<Normalized>,
-) -> Result<Value, TypeError> {
-    use crate::syntax::ExprF::{Annot, Embed, Lam, Let, Pi, Var};
-    let span = e.span();
-
-    Ok(match e.as_ref() {
-        Lam(var, annot, body) => {
-            let annot = type_with(ctx, annot.clone())?;
-            let ctx2 = ctx.insert_type(var, annot.clone());
-            let body = type_with(&ctx2, body.clone())?;
-            let body_type = body.get_type()?;
-            Value::from_valuef_and_type(
-                ValueF::Lam(var.clone().into(), annot.clone(), body),
-                tck_pi_type(ctx, var.clone(), annot, body_type)?,
-            )
-        }
-        Pi(x, ta, tb) => {
-            let ta = type_with(ctx, ta.clone())?;
-            let ctx2 = ctx.insert_type(x, ta.clone());
-            let tb = type_with(&ctx2, tb.clone())?;
-            return tck_pi_type(ctx, x.clone(), ta, tb);
-        }
-        Let(x, t, v, e) => {
-            let v = if let Some(t) = t {
-                t.rewrap(Annot(v.clone(), t.clone()))
-            } else {
-                v.clone()
-            };
-
-            let v = type_with(ctx, v)?;
-            return type_with(&ctx.insert_value(x, v.clone())?, e.clone());
-        }
-        Embed(p) => p.clone().into_typed().into_value(),
-        Var(var) => match ctx.lookup(&var) {
-            Some(typed) => typed.clone(),
-            None => {
-                return Err(TypeError::new(
-                    ctx,
-                    TypeMessage::UnboundVariable(span),
-                ))
-            }
-        },
-        e => {
-            // Typecheck recursively all subexpressions
-            let expr = e.traverse_ref_with_special_handling_of_binders(
-                |e| type_with(ctx, e.clone()),
-                |_, _| unreachable!(),
-            )?;
-            type_last_layer(ctx, expr, span)?
-        }
-    })
-}
-
-/// When all sub-expressions have been typed, check the remaining toplevel
-/// layer.
-fn type_last_layer(
-    ctx: &TypecheckContext,
-    e: ExprF<Value, Normalized>,
-    span: Span,
-) -> Result<Value, TypeError> {
-    use crate::error::TypeMessage::*;
-    use crate::syntax::BinOp::*;
-    use crate::syntax::Builtin::*;
-    use crate::syntax::Const::Type;
-    use crate::syntax::ExprF::*;
-    let mkerr = |msg: TypeMessage| Err(TypeError::new(ctx, msg));
-
-    /// Intermediary return type
-    enum Ret {
-        /// Returns the contained value as is
-        RetWhole(Value),
-        /// Returns the input expression `e` with the contained value as its type
-        RetTypeOnly(Value),
-    }
-    use Ret::*;
-
-    let ret = match &e {
-        Import(_) => unreachable!(
-            "There should remain no imports in a resolved expression"
-        ),
-        Lam(_, _, _) | Pi(_, _, _) | Let(_, _, _, _) | Embed(_) | Var(_) => {
-            unreachable!()
-        }
-        App(f, a) => {
-            let tf = f.get_type()?;
-            let tf_borrow = tf.as_whnf();
-            let (x, tx, tb) = match &*tf_borrow {
-                ValueF::Pi(x, tx, tb) => (x, tx, tb),
-                _ => return mkerr(NotAFunction(f.clone())),
-            };
-            if &a.get_type()? != tx {
-                return mkerr(TypeMismatch(f.clone(), tx.clone(), a.clone()));
-            }
-
-            RetTypeOnly(tb.subst_shift(&x.into(), a))
-        }
-        Annot(x, t) => {
-            if &x.get_type()? != t {
-                return mkerr(AnnotMismatch(x.clone(), t.clone()));
-            }
-            RetWhole(x.clone())
-        }
-        Assert(t) => {
-            match &*t.as_whnf() {
-                ValueF::Equivalence(x, y) if x == y => {}
-                ValueF::Equivalence(x, y) => {
-                    return mkerr(AssertMismatch(x.clone(), y.clone()))
-                }
-                _ => return mkerr(AssertMustTakeEquivalence),
-            }
-            RetTypeOnly(t.clone())
-        }
-        BoolIf(x, y, z) => {
-            if *x.get_type()?.as_whnf() != ValueF::from_builtin(Bool) {
-                return mkerr(InvalidPredicate(x.clone()));
-            }
-
-            if y.get_type()?.get_type()?.as_const() != Some(Type) {
-                return mkerr(IfBranchMustBeTerm(true, y.clone()));
-            }
-
-            if z.get_type()?.get_type()?.as_const() != Some(Type) {
-                return mkerr(IfBranchMustBeTerm(false, z.clone()));
-            }
-
-            if y.get_type()? != z.get_type()? {
-                return mkerr(IfBranchMismatch(y.clone(), z.clone()));
-            }
-
-            RetTypeOnly(y.get_type()?)
-        }
-        EmptyListLit(t) => {
-            match &*t.as_whnf() {
-                ValueF::AppliedBuiltin(crate::syntax::Builtin::List, args)
-                    if args.len() == 1 => {}
-                _ => return mkerr(InvalidListType(t.clone())),
-            }
-            RetTypeOnly(t.clone())
-        }
-        NEListLit(xs) => {
-            let mut iter = xs.iter().enumerate();
-            let (_, x) = iter.next().unwrap();
-            for (i, y) in iter {
-                if x.get_type()? != y.get_type()? {
-                    return mkerr(InvalidListElement(
-                        i,
-                        x.get_type()?,
-                        y.clone(),
-                    ));
-                }
-            }
-            let t = x.get_type()?;
-            if t.get_type()?.as_const() != Some(Type) {
-                return mkerr(InvalidListType(t));
-            }
-
-            RetTypeOnly(Value::from_builtin(crate::syntax::Builtin::List).app(t))
-        }
-        SomeLit(x) => {
-            let t = x.get_type()?;
-            if t.get_type()?.as_const() != Some(Type) {
-                return mkerr(InvalidOptionalType(t));
-            }
-
-            RetTypeOnly(
-                Value::from_builtin(crate::syntax::Builtin::Optional).app(t),
-            )
-        }
-        RecordType(kts) => RetWhole(tck_record_type(
-            ctx,
-            kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))),
-        )?),
-        UnionType(kts) => RetWhole(tck_union_type(
-            ctx,
-            kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))),
-        )?),
-        RecordLit(kvs) => RetTypeOnly(tck_record_type(
-            ctx,
-            kvs.iter().map(|(x, v)| Ok((x.clone(), v.get_type()?))),
-        )?),
-        Field(r, x) => {
-            match &*r.get_type()?.as_whnf() {
-                ValueF::RecordType(kts) => match kts.get(&x) {
-                    Some(tth) => {
-                        RetTypeOnly(tth.clone())
-                    },
-                    None => return mkerr(MissingRecordField(x.clone(),
-                                        r.clone())),
-                },
-                // TODO: branch here only when r.get_type() is a Const
-                _ => {
-                    match &*r.as_whnf() {
-                        ValueF::UnionType(kts) => match kts.get(&x) {
-                            // Constructor has type T -> < x: T, ... >
-                            Some(Some(t)) => {
-                                RetTypeOnly(
-                                    tck_pi_type(
-                                        ctx,
-                                        "_".into(),
-                                        t.clone(),
-                                        r.under_binder(Label::from("_")),
-                                    )?
-                                )
-                            },
-                            Some(None) => {
-                                RetTypeOnly(r.clone())
-                            },
-                            None => {
-                                return mkerr(MissingUnionField(
-                                    x.clone(),
-                                    r.clone(),
-                                ))
-                            },
-                        },
-                        _ => {
-                            return mkerr(NotARecord(
-                                x.clone(),
-                                r.clone()
-                            ))
-                        },
-                    }
-                }
-                // _ => mkerr(NotARecord(
-                //     x,
-                //     r?,
-                // )),
-            }
-        }
-        Const(c) => RetWhole(const_to_value(*c)),
-        Builtin(b) => RetWhole(builtin_to_value(*b)),
-        BoolLit(_) => RetTypeOnly(builtin_to_value(Bool)),
-        NaturalLit(_) => RetTypeOnly(builtin_to_value(Natural)),
-        IntegerLit(_) => RetTypeOnly(builtin_to_value(Integer)),
-        DoubleLit(_) => RetTypeOnly(builtin_to_value(Double)),
-        TextLit(interpolated) => {
-            let text_type = builtin_to_value(Text);
-            for contents in interpolated.iter() {
-                use InterpolatedTextContents::Expr;
-                if let Expr(x) = contents {
-                    if x.get_type()? != text_type {
-                        return mkerr(InvalidTextInterpolation(x.clone()));
-                    }
-                }
-            }
-            RetTypeOnly(text_type)
-        }
-        BinOp(RightBiasedRecordMerge, l, r) => {
-            use crate::phase::normalize::merge_maps;
-
-            let l_type = l.get_type()?;
-            let r_type = r.get_type()?;
-
-            // Extract the LHS record type
-            let l_type_borrow = l_type.as_whnf();
-            let kts_x = match &*l_type_borrow {
-                ValueF::RecordType(kts) => kts,
-                _ => return mkerr(MustCombineRecord(l.clone())),
-            };
-
-            // Extract the RHS record type
-            let r_type_borrow = r_type.as_whnf();
-            let kts_y = match &*r_type_borrow {
-                ValueF::RecordType(kts) => kts,
-                _ => return mkerr(MustCombineRecord(r.clone())),
-            };
-
-            // Union the two records, prefering
-            // the values found in the RHS.
-            let kts = merge_maps::<_, _, _, !>(kts_x, kts_y, |_, _, r_t| {
-                Ok(r_t.clone())
-            })?;
-
-            // Construct the final record type from the union
-            RetTypeOnly(tck_record_type(
-                ctx,
-                kts.into_iter().map(|(x, v)| Ok((x.clone(), v))),
-            )?)
-        }
-        BinOp(RecursiveRecordMerge, l, r) => RetTypeOnly(type_last_layer(
-            ctx,
-            ExprF::BinOp(
-                RecursiveRecordTypeMerge,
-                l.get_type()?,
-                r.get_type()?,
-            ),
-            Span::Artificial,
-        )?),
-        BinOp(RecursiveRecordTypeMerge, l, r) => {
-            use crate::phase::normalize::merge_maps;
-
-            // Extract the LHS record type
-            let borrow_l = l.as_whnf();
-            let kts_x = match &*borrow_l {
-                ValueF::RecordType(kts) => kts,
-                _ => {
-                    return mkerr(RecordTypeMergeRequiresRecordType(l.clone()))
-                }
-            };
-
-            // Extract the RHS record type
-            let borrow_r = r.as_whnf();
-            let kts_y = match &*borrow_r {
-                ValueF::RecordType(kts) => kts,
-                _ => {
-                    return mkerr(RecordTypeMergeRequiresRecordType(r.clone()))
-                }
-            };
-
-            // Ensure that the records combine without a type error
-            let kts = merge_maps(
-                kts_x,
-                kts_y,
-                // If the Label exists for both records, then we hit the recursive case.
-                |_, l: &Value, r: &Value| {
-                    type_last_layer(
-                        ctx,
-                        ExprF::BinOp(
-                            RecursiveRecordTypeMerge,
-                            l.clone(),
-                            r.clone(),
-                        ),
-                        Span::Artificial,
-                    )
-                },
-            )?;
-
-            RetWhole(tck_record_type(ctx, kts.into_iter().map(Ok))?)
-        }
-        BinOp(o @ ListAppend, l, r) => {
-            match &*l.get_type()?.as_whnf() {
-                ValueF::AppliedBuiltin(List, _) => {}
-                _ => return mkerr(BinOpTypeMismatch(*o, l.clone())),
-            }
-
-            if l.get_type()? != r.get_type()? {
-                return mkerr(BinOpTypeMismatch(*o, r.clone()));
-            }
-
-            RetTypeOnly(l.get_type()?)
-        }
-        BinOp(Equivalence, l, r) => {
-            if l.get_type()?.get_type()?.as_const() != Some(Type) {
-                return mkerr(EquivalenceArgumentMustBeTerm(true, l.clone()));
-            }
-            if r.get_type()?.get_type()?.as_const() != Some(Type) {
-                return mkerr(EquivalenceArgumentMustBeTerm(false, r.clone()));
-            }
-
-            if l.get_type()? != r.get_type()? {
-                return mkerr(EquivalenceTypeMismatch(r.clone(), l.clone()));
-            }
-
-            RetWhole(Value::from_valuef_and_type(
-                ValueF::Equivalence(l.clone(), r.clone()),
-                Value::from_const(Type),
-            ))
-        }
-        BinOp(o, l, r) => {
-            let t = builtin_to_value(match o {
-                BoolAnd => Bool,
-                BoolOr => Bool,
-                BoolEQ => Bool,
-                BoolNE => Bool,
-                NaturalPlus => Natural,
-                NaturalTimes => Natural,
-                TextAppend => Text,
-                ListAppend => unreachable!(),
-                RightBiasedRecordMerge => unreachable!(),
-                RecursiveRecordMerge => unreachable!(),
-                RecursiveRecordTypeMerge => unreachable!(),
-                ImportAlt => unreachable!("There should remain no import alternatives in a resolved expression"),
-                Equivalence => unreachable!(),
-            });
-
-            if l.get_type()? != t {
-                return mkerr(BinOpTypeMismatch(*o, l.clone()));
-            }
-
-            if r.get_type()? != t {
-                return mkerr(BinOpTypeMismatch(*o, r.clone()));
-            }
-
-            RetTypeOnly(t)
-        }
-        Merge(record, union, type_annot) => {
-            let record_type = record.get_type()?;
-            let record_borrow = record_type.as_whnf();
-            let handlers = match &*record_borrow {
-                ValueF::RecordType(kts) => kts,
-                _ => return mkerr(Merge1ArgMustBeRecord(record.clone())),
-            };
-
-            let union_type = union.get_type()?;
-            let union_borrow = union_type.as_whnf();
-            let variants = match &*union_borrow {
-                ValueF::UnionType(kts) => kts,
-                _ => return mkerr(Merge2ArgMustBeUnion(union.clone())),
-            };
-
-            let mut inferred_type = None;
-            for (x, handler_type) in handlers {
-                let handler_return_type =
-                    match variants.get(x) {
-                        // Union alternative with type
-                        Some(Some(variant_type)) => {
-                            let handler_type_borrow = handler_type.as_whnf();
-                            let (x, tx, tb) = match &*handler_type_borrow {
-                                ValueF::Pi(x, tx, tb) => (x, tx, tb),
-                                _ => {
-                                    return mkerr(NotAFunction(
-                                        handler_type.clone(),
-                                    ))
-                                }
-                            };
-
-                            if variant_type != tx {
-                                return mkerr(TypeMismatch(
-                                    handler_type.clone(),
-                                    tx.clone(),
-                                    variant_type.clone(),
-                                ));
-                            }
-
-                            // Extract `tb` from under the `x` binder. Fails is `x` was free in `tb`.
-                            match tb.over_binder(x) {
-                                Some(x) => x,
-                                None => return mkerr(
-                                    MergeHandlerReturnTypeMustNotBeDependent,
-                                ),
-                            }
-                        }
-                        // Union alternative without type
-                        Some(None) => handler_type.clone(),
-                        None => {
-                            return mkerr(MergeHandlerMissingVariant(x.clone()))
-                        }
-                    };
-                match &inferred_type {
-                    None => inferred_type = Some(handler_return_type),
-                    Some(t) => {
-                        if t != &handler_return_type {
-                            return mkerr(MergeHandlerTypeMismatch);
-                        }
-                    }
-                }
-            }
-            for x in variants.keys() {
-                if !handlers.contains_key(x) {
-                    return mkerr(MergeVariantMissingHandler(x.clone()));
-                }
-            }
-
-            match (inferred_type, type_annot) {
-                (Some(ref t1), Some(t2)) => {
-                    if t1 != t2 {
-                        return mkerr(MergeAnnotMismatch);
-                    }
-                    RetTypeOnly(t2.clone())
-                }
-                (Some(t), None) => RetTypeOnly(t),
-                (None, Some(t)) => RetTypeOnly(t.clone()),
-                (None, None) => return mkerr(MergeEmptyNeedsAnnotation),
-            }
-        }
-        ToMap(_, _) => unimplemented!("toMap"),
-        Projection(record, labels) => {
-            let record_type = record.get_type()?;
-            let record_type_borrow = record_type.as_whnf();
-            let kts = match &*record_type_borrow {
-                ValueF::RecordType(kts) => kts,
-                _ => return mkerr(ProjectionMustBeRecord),
-            };
-
-            let mut new_kts = HashMap::new();
-            for l in labels {
-                match kts.get(l) {
-                    None => return mkerr(ProjectionMissingEntry),
-                    Some(t) => new_kts.insert(l.clone(), t.clone()),
-                };
-            }
-
-            RetTypeOnly(Value::from_valuef_and_type(
-                ValueF::RecordType(new_kts),
-                record_type.get_type()?,
-            ))
-        }
-        ProjectionByExpr(_, _) => unimplemented!("selection by expression"),
-    };
-
-    Ok(match ret {
-        RetTypeOnly(typ) => Value::from_valuef_and_type_and_span(
-            ValueF::PartialExpr(e),
-            typ,
-            span,
-        ),
-        RetWhole(v) => v.with_span(span),
-    })
-}
-
-/// `type_of` is the same as `type_with` with an empty context, meaning that the
-/// expression must be closed (i.e. no free variables), otherwise type-checking
-/// will fail.
-pub(crate) fn typecheck(e: Expr<Normalized>) -> Result<Value, TypeError> {
-    type_with(&TypecheckContext::new(), e)
-}
-
-pub(crate) fn typecheck_with(
-    expr: Expr<Normalized>,
-    ty: Expr<Normalized>,
-) -> Result<Value, TypeError> {
-    typecheck(expr.rewrap(ExprF::Annot(expr.clone(), ty)))
-}