Rewrite normalization and typechecking with environments (#126)

Rewrite normalization and typechecking with environments

6 files changed, 1262 insertions, 0 deletions

diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs
new file mode 100644
index 0000000..0b22a8b
--- /dev/null
+++ b/dhall/src/semantics/nze/env.rs
@@ -0,0 +1,76 @@
+use crate::semantics::{AlphaVar, Value, ValueKind};
+
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+pub(crate) enum NzVar {
+    /// Reverse-debruijn index: counts number of binders from the bottom of the stack.
+    Bound(usize),
+    /// Fake fresh variable generated for expression equality checking.
+    Fresh(usize),
+}
+
+#[derive(Debug, Clone)]
+enum NzEnvItem {
+    // Variable is bound with given type
+    Kept(Value),
+    // Variable has been replaced by corresponding value
+    Replaced(Value),
+}
+
+#[derive(Debug, Clone)]
+pub(crate) struct NzEnv {
+    items: Vec<NzEnvItem>,
+}
+
+impl NzVar {
+    pub fn new(idx: usize) -> Self {
+        NzVar::Bound(idx)
+    }
+    pub fn fresh() -> Self {
+        use std::sync::atomic::{AtomicUsize, Ordering};
+        // Global counter to ensure uniqueness of the generated id.
+        static FRESH_VAR_COUNTER: AtomicUsize = AtomicUsize::new(0);
+        let id = FRESH_VAR_COUNTER.fetch_add(1, Ordering::SeqCst);
+        NzVar::Fresh(id)
+    }
+    /// Get index of bound variable.
+    /// Panics on a fresh variable.
+    pub fn idx(&self) -> usize {
+        match self {
+            NzVar::Bound(i) => *i,
+            NzVar::Fresh(_) => panic!(
+                "Trying to use a fresh variable outside of equality checking"
+            ),
+        }
+    }
+}
+
+impl NzEnv {
+    pub fn new() -> Self {
+        NzEnv { items: Vec::new() }
+    }
+
+    pub fn insert_type(&self, t: Value) -> Self {
+        let mut env = self.clone();
+        env.items.push(NzEnvItem::Kept(t));
+        env
+    }
+    pub fn insert_value(&self, e: Value) -> Self {
+        let mut env = self.clone();
+        env.items.push(NzEnvItem::Replaced(e));
+        env
+    }
+    pub fn lookup_val(&self, var: &AlphaVar) -> ValueKind {
+        let idx = self.items.len() - 1 - var.idx();
+        match &self.items[idx] {
+            NzEnvItem::Kept(_) => ValueKind::Var(NzVar::new(idx)),
+            NzEnvItem::Replaced(x) => x.kind().clone(),
+        }
+    }
+    pub fn lookup_ty(&self, var: &AlphaVar) -> Value {
+        let idx = self.items.len() - 1 - var.idx();
+        match &self.items[idx] {
+            NzEnvItem::Kept(ty) => ty.clone(),
+            NzEnvItem::Replaced(x) => x.get_type().unwrap(),
+        }
+    }
+}
diff --git a/dhall/src/semantics/nze/lazy.rs b/dhall/src/semantics/nze/lazy.rs
new file mode 100644
index 0000000..d361313
--- /dev/null
+++ b/dhall/src/semantics/nze/lazy.rs
@@ -0,0 +1,64 @@
+use once_cell::unsync::OnceCell;
+use std::cell::Cell;
+use std::fmt::Debug;
+use std::ops::Deref;
+
+pub trait Eval<Tgt> {
+    fn eval(self) -> Tgt;
+}
+
+/// A value which is initialized from a `Src` on the first access.
+pub struct Lazy<Src, Tgt> {
+    /// Exactly one of `src` of `tgt` must be set at a given time.
+    /// Once `src` is unset and `tgt` is set, we never go back.
+    src: Cell<Option<Src>>,
+    tgt: OnceCell<Tgt>,
+}
+
+impl<Src, Tgt> Lazy<Src, Tgt>
+where
+    Src: Eval<Tgt>,
+{
+    /// Creates a new lazy value with the given initializing value.
+    pub fn new(src: Src) -> Self {
+        Lazy {
+            src: Cell::new(Some(src)),
+            tgt: OnceCell::new(),
+        }
+    }
+    /// Creates a new lazy value with the given already-initialized value.
+    pub fn new_completed(tgt: Tgt) -> Self {
+        let lazy = Lazy {
+            src: Cell::new(None),
+            tgt: OnceCell::new(),
+        };
+        let _ = lazy.tgt.set(tgt);
+        lazy
+    }
+}
+
+impl<Src, Tgt> Deref for Lazy<Src, Tgt>
+where
+    Src: Eval<Tgt>,
+{
+    type Target = Tgt;
+    fn deref(&self) -> &Self::Target {
+        self.tgt.get_or_init(|| {
+            let src = self.src.take().unwrap();
+            src.eval()
+        })
+    }
+}
+
+impl<Src, Tgt> Debug for Lazy<Src, Tgt>
+where
+    Tgt: Debug,
+{
+    fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        if let Some(tgt) = self.tgt.get() {
+            fmt.debug_tuple("Lazy@Init").field(tgt).finish()
+        } else {
+            fmt.debug_tuple("Lazy@Uninit").finish()
+        }
+    }
+}
diff --git a/dhall/src/semantics/nze/mod.rs b/dhall/src/semantics/nze/mod.rs
new file mode 100644
index 0000000..2c8d907
--- /dev/null
+++ b/dhall/src/semantics/nze/mod.rs
@@ -0,0 +1,9 @@
+pub mod env;
+pub mod lazy;
+pub mod normalize;
+pub mod value;
+pub mod var;
+pub(crate) use env::*;
+pub(crate) use normalize::*;
+pub(crate) use value::*;
+pub(crate) use var::*;
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
new file mode 100644
index 0000000..e9d140b
--- /dev/null
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -0,0 +1,421 @@
+use std::collections::HashMap;
+
+use crate::semantics::NzEnv;
+use crate::semantics::{
+    Binder, BuiltinClosure, Closure, TextLit, TyExpr, TyExprKind, Value,
+    ValueKind,
+};
+use crate::syntax::{
+    BinOp, Builtin, Const, ExprKind, InterpolatedTextContents,
+};
+use crate::Normalized;
+
+pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind {
+    match f.kind() {
+        ValueKind::LamClosure { closure, .. } => {
+            closure.apply(a).to_whnf_check_type(ty)
+        }
+        ValueKind::AppliedBuiltin(closure) => {
+            closure.apply(a, f.get_type().unwrap(), ty)
+        }
+        ValueKind::UnionConstructor(l, kts, uniont) => ValueKind::UnionLit(
+            l.clone(),
+            a,
+            kts.clone(),
+            uniont.clone(),
+            f.get_type().unwrap(),
+        ),
+        _ => ValueKind::PartialExpr(ExprKind::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) => match e.kind() {
+                    ValueKind::TextLit(elts2) => {
+                        inner(elts2.iter().cloned(), crnt_str, ret)
+                    }
+                    _ => {
+                        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> {
+    ValueKind(ValueKind),
+    Value(Value),
+    ValueRef(&'a Value),
+    Expr(ExprKind<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 ValueKind::{
+        BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType,
+    };
+    Some(match (o, x.kind(), y.kind()) {
+        (BoolAnd, BoolLit(true), _) => Ret::ValueRef(y),
+        (BoolAnd, _, BoolLit(true)) => Ret::ValueRef(x),
+        (BoolAnd, BoolLit(false), _) => Ret::ValueKind(BoolLit(false)),
+        (BoolAnd, _, BoolLit(false)) => Ret::ValueKind(BoolLit(false)),
+        (BoolAnd, _, _) if x == y => Ret::ValueRef(x),
+        (BoolOr, BoolLit(true), _) => Ret::ValueKind(BoolLit(true)),
+        (BoolOr, _, BoolLit(true)) => Ret::ValueKind(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::ValueKind(BoolLit(x == y)),
+        (BoolEQ, _, _) if x == y => Ret::ValueKind(BoolLit(true)),
+        (BoolNE, BoolLit(false), _) => Ret::ValueRef(y),
+        (BoolNE, _, BoolLit(false)) => Ret::ValueRef(x),
+        (BoolNE, BoolLit(x), BoolLit(y)) => Ret::ValueKind(BoolLit(x != y)),
+        (BoolNE, _, _) if x == y => Ret::ValueKind(BoolLit(false)),
+
+        (NaturalPlus, NaturalLit(0), _) => Ret::ValueRef(y),
+        (NaturalPlus, _, NaturalLit(0)) => Ret::ValueRef(x),
+        (NaturalPlus, NaturalLit(x), NaturalLit(y)) => {
+            Ret::ValueKind(NaturalLit(x + y))
+        }
+        (NaturalTimes, NaturalLit(0), _) => Ret::ValueKind(NaturalLit(0)),
+        (NaturalTimes, _, NaturalLit(0)) => Ret::ValueKind(NaturalLit(0)),
+        (NaturalTimes, NaturalLit(1), _) => Ret::ValueRef(y),
+        (NaturalTimes, _, NaturalLit(1)) => Ret::ValueRef(x),
+        (NaturalTimes, NaturalLit(x), NaturalLit(y)) => {
+            Ret::ValueKind(NaturalLit(x * y))
+        }
+
+        (ListAppend, EmptyListLit(_), _) => Ret::ValueRef(y),
+        (ListAppend, _, EmptyListLit(_)) => Ret::ValueRef(x),
+        (ListAppend, NEListLit(xs), NEListLit(ys)) => Ret::ValueKind(
+            NEListLit(xs.iter().chain(ys.iter()).cloned().collect()),
+        ),
+
+        (TextAppend, ValueKind::TextLit(x), _) if x.is_empty() => {
+            Ret::ValueRef(y)
+        }
+        (TextAppend, _, ValueKind::TextLit(y)) if y.is_empty() => {
+            Ret::ValueRef(x)
+        }
+        (TextAppend, ValueKind::TextLit(x), ValueKind::TextLit(y)) => {
+            Ret::ValueKind(ValueKind::TextLit(x.concat(y)))
+        }
+        (TextAppend, ValueKind::TextLit(x), _) => Ret::ValueKind(
+            ValueKind::TextLit(x.concat(&TextLit::interpolate(y.clone()))),
+        ),
+        (TextAppend, _, ValueKind::TextLit(y)) => Ret::ValueKind(
+            ValueKind::TextLit(TextLit::interpolate(x.clone()).concat(y)),
+        ),
+
+        (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::ValueKind(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 kts = match ty.kind() {
+                RecordType(kts) => kts,
+                _ => unreachable!("Internal type error"),
+            };
+            let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |k, v1, v2| {
+                Ok(Value::from_partial_expr(
+                    ExprKind::BinOp(
+                        RecursiveRecordMerge,
+                        v1.clone(),
+                        v2.clone(),
+                    ),
+                    kts.get(k).expect("Internal type error").clone(),
+                ))
+            })?;
+            Ret::ValueKind(RecordLit(kvs))
+        }
+
+        (RecursiveRecordTypeMerge, RecordType(kts_x), RecordType(kts_y)) => {
+            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| {
+                    Ok(Value::from_partial_expr(
+                        ExprKind::BinOp(
+                            RecursiveRecordTypeMerge,
+                            l.clone(),
+                            r.clone(),
+                        ),
+                        ty.clone(),
+                    ))
+                },
+            )?;
+            Ret::ValueKind(RecordType(kts))
+        }
+
+        (Equivalence, _, _) => {
+            Ret::ValueKind(ValueKind::Equivalence(x.clone(), y.clone()))
+        }
+
+        _ => return None,
+    })
+}
+
+pub(crate) fn normalize_one_layer(
+    expr: ExprKind<Value, Normalized>,
+    ty: &Value,
+    env: &NzEnv,
+) -> ValueKind {
+    use ValueKind::{
+        BoolLit, DoubleLit, EmptyOptionalLit, IntegerLit, NEListLit,
+        NEOptionalLit, NaturalLit, RecordLit, RecordType, UnionConstructor,
+        UnionLit, UnionType,
+    };
+
+    let ret = match expr {
+        ExprKind::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.
+        ExprKind::Lam(..)
+        | ExprKind::Pi(..)
+        | ExprKind::Let(..)
+        | ExprKind::Embed(_)
+        | ExprKind::Var(_) => {
+            unreachable!("This case should have been handled in typecheck")
+        }
+        ExprKind::Annot(x, _) => Ret::Value(x),
+        ExprKind::Const(c) => Ret::Value(Value::from_const(c)),
+        ExprKind::Builtin(b) => Ret::Value(Value::from_builtin_env(b, env)),
+        ExprKind::Assert(_) => Ret::Expr(expr),
+        ExprKind::App(v, a) => Ret::Value(v.app(a)),
+        ExprKind::BoolLit(b) => Ret::ValueKind(BoolLit(b)),
+        ExprKind::NaturalLit(n) => Ret::ValueKind(NaturalLit(n)),
+        ExprKind::IntegerLit(n) => Ret::ValueKind(IntegerLit(n)),
+        ExprKind::DoubleLit(n) => Ret::ValueKind(DoubleLit(n)),
+        ExprKind::SomeLit(e) => Ret::ValueKind(NEOptionalLit(e)),
+        ExprKind::EmptyListLit(t) => {
+            let arg = match &*t.kind() {
+                ValueKind::AppliedBuiltin(BuiltinClosure {
+                    b: Builtin::List,
+                    args,
+                    ..
+                }) if args.len() == 1 => args[0].clone(),
+                _ => panic!("internal type error"),
+            };
+            Ret::ValueKind(ValueKind::EmptyListLit(arg))
+        }
+        ExprKind::NEListLit(elts) => {
+            Ret::ValueKind(NEListLit(elts.into_iter().collect()))
+        }
+        ExprKind::RecordLit(kvs) => {
+            Ret::ValueKind(RecordLit(kvs.into_iter().collect()))
+        }
+        ExprKind::RecordType(kvs) => {
+            Ret::ValueKind(RecordType(kvs.into_iter().collect()))
+        }
+        ExprKind::UnionType(kvs) => {
+            Ret::ValueKind(UnionType(kvs.into_iter().collect()))
+        }
+        ExprKind::TextLit(elts) => {
+            let tlit = TextLit::new(elts.into_iter());
+            // Simplify bare interpolation
+            if let Some(v) = tlit.as_single_expr() {
+                Ret::Value(v.clone())
+            } else {
+                Ret::ValueKind(ValueKind::TextLit(tlit))
+            }
+        }
+        ExprKind::BoolIf(ref b, ref e1, ref e2) => {
+            match b.kind() {
+                BoolLit(true) => Ret::ValueRef(e1),
+                BoolLit(false) => Ret::ValueRef(e2),
+                _ => {
+                    match (e1.kind(), e2.kind()) {
+                        // Simplify `if b then True else False`
+                        (BoolLit(true), BoolLit(false)) => Ret::ValueRef(b),
+                        _ if e1 == e2 => Ret::ValueRef(e1),
+                        _ => Ret::Expr(expr),
+                    }
+                }
+            }
+        }
+        ExprKind::BinOp(o, ref x, ref y) => match apply_binop(o, x, y, ty) {
+            Some(ret) => ret,
+            None => Ret::Expr(expr),
+        },
+
+        ExprKind::Projection(_, ref ls) if ls.is_empty() => {
+            Ret::ValueKind(RecordLit(HashMap::new()))
+        }
+        ExprKind::Projection(ref v, ref ls) => match v.kind() {
+            RecordLit(kvs) => Ret::ValueKind(RecordLit(
+                ls.iter()
+                    .filter_map(|l| kvs.get(l).map(|x| (l.clone(), x.clone())))
+                    .collect(),
+            )),
+            _ => Ret::Expr(expr),
+        },
+        ExprKind::Field(ref v, ref l) => match v.kind() {
+            RecordLit(kvs) => match kvs.get(l) {
+                Some(r) => Ret::Value(r.clone()),
+                None => Ret::Expr(expr),
+            },
+            UnionType(kts) => Ret::ValueKind(UnionConstructor(
+                l.clone(),
+                kts.clone(),
+                v.get_type().unwrap(),
+            )),
+            _ => Ret::Expr(expr),
+        },
+        ExprKind::ProjectionByExpr(_, _) => {
+            unimplemented!("selection by expression")
+        }
+        ExprKind::Completion(_, _) => unimplemented!("record completion"),
+
+        ExprKind::Merge(ref handlers, ref variant, _) => {
+            match handlers.kind() {
+                RecordLit(kvs) => match variant.kind() {
+                    UnionConstructor(l, _, _) => match kvs.get(l) {
+                        Some(h) => Ret::Value(h.clone()),
+                        None => Ret::Expr(expr),
+                    },
+                    UnionLit(l, v, _, _, _) => match kvs.get(l) {
+                        Some(h) => Ret::Value(h.app(v.clone())),
+                        None => Ret::Expr(expr),
+                    },
+                    EmptyOptionalLit(_) => match kvs.get(&"None".into()) {
+                        Some(h) => Ret::Value(h.clone()),
+                        None => Ret::Expr(expr),
+                    },
+                    NEOptionalLit(v) => match kvs.get(&"Some".into()) {
+                        Some(h) => Ret::Value(h.app(v.clone())),
+                        None => Ret::Expr(expr),
+                    },
+                    _ => Ret::Expr(expr),
+                },
+                _ => Ret::Expr(expr),
+            }
+        }
+        ExprKind::ToMap(_, _) => unimplemented!("toMap"),
+    };
+
+    match ret {
+        Ret::ValueKind(v) => v,
+        Ret::Value(v) => v.to_whnf_check_type(ty),
+        Ret::ValueRef(v) => v.to_whnf_check_type(ty),
+        Ret::Expr(expr) => ValueKind::PartialExpr(expr),
+    }
+}
+
+/// Normalize a TyExpr into WHNF
+pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> ValueKind {
+    match tye.kind() {
+        TyExprKind::Var(var) => env.lookup_val(var),
+        TyExprKind::Expr(ExprKind::Lam(binder, annot, body)) => {
+            let annot = annot.eval(env);
+            ValueKind::LamClosure {
+                binder: Binder::new(binder.clone()),
+                annot: annot.clone(),
+                closure: Closure::new(annot, env, body.clone()),
+            }
+        }
+        TyExprKind::Expr(ExprKind::Pi(binder, annot, body)) => {
+            let annot = annot.eval(env);
+            let closure = Closure::new(annot.clone(), env, body.clone());
+            ValueKind::PiClosure {
+                binder: Binder::new(binder.clone()),
+                annot,
+                closure,
+            }
+        }
+        TyExprKind::Expr(ExprKind::Let(_, None, val, body)) => {
+            let val = val.eval(env);
+            body.eval(&env.insert_value(val)).kind().clone()
+        }
+        TyExprKind::Expr(e) => {
+            let ty = match tye.get_type() {
+                Ok(ty) => ty,
+                Err(_) => return ValueKind::Const(Const::Sort),
+            };
+            let e = e.map_ref(|tye| tye.eval(env));
+            normalize_one_layer(e, &ty, env)
+        }
+    }
+}
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
new file mode 100644
index 0000000..ae06942
--- /dev/null
+++ b/dhall/src/semantics/nze/value.rs
@@ -0,0 +1,656 @@
+use std::collections::HashMap;
+use std::rc::Rc;
+
+use crate::error::{TypeError, TypeMessage};
+use crate::semantics::nze::lazy;
+use crate::semantics::Binder;
+use crate::semantics::{
+    apply_any, normalize_one_layer, normalize_tyexpr_whnf, squash_textlit,
+};
+use crate::semantics::{type_of_builtin, typecheck, TyExpr, TyExprKind};
+use crate::semantics::{BuiltinClosure, NzEnv, NzVar, VarEnv};
+use crate::syntax::{
+    BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label,
+    NaiveDouble, Natural, Span,
+};
+use crate::{Normalized, NormalizedExpr, ToExprOptions};
+
+/// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, sharing computation
+/// automatically. Uses a Rc<RefCell> to share computation.
+/// If you compare for equality two `Value`s, then equality will be up to alpha-equivalence
+/// (renaming of bound variables) and beta-equivalence (normalization). It will recursively
+/// normalize as needed.
+#[derive(Clone)]
+pub(crate) struct Value(Rc<ValueInternal>);
+
+#[derive(Debug)]
+struct ValueInternal {
+    kind: lazy::Lazy<Thunk, ValueKind>,
+    /// This is None if and only if `form` is `Sort` (which doesn't have a type)
+    ty: Option<Value>,
+    span: Span,
+}
+
+/// An unevaluated subexpression
+#[derive(Debug, Clone)]
+pub(crate) enum Thunk {
+    /// A completely unnormalized expression.
+    Thunk { env: NzEnv, body: TyExpr },
+    /// A partially normalized expression that may need to go through `normalize_one_layer`.
+    PartialExpr {
+        env: NzEnv,
+        expr: ExprKind<Value, Normalized>,
+        ty: Value,
+    },
+}
+
+/// An unevaluated subexpression that takes an argument.
+#[derive(Debug, Clone)]
+pub(crate) enum Closure {
+    /// Normal closure
+    Closure {
+        arg_ty: Value,
+        env: NzEnv,
+        body: TyExpr,
+    },
+    /// Closure that ignores the argument passed
+    ConstantClosure { body: Value },
+}
+
+/// A text literal with interpolations.
+// Invariant: this must not contain interpolations that are themselves TextLits, and contiguous
+// text values must be merged.
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub(crate) struct TextLit(Vec<InterpolatedTextContents<Value>>);
+
+/// This represents a value in Weak Head Normal Form (WHNF). This means that the value is
+/// normalized up to the first constructor, but subexpressions may not be fully normalized.
+/// When all the Values in a ValueKind are in WHNF, and recursively so, then the ValueKind is in
+/// Normal Form (NF). This is because WHNF ensures that we have the first constructor of the NF; so
+/// if we have the first constructor of the NF at all levels, we actually have the NF.
+/// In particular, this means that once we get a `ValueKind`, it can be considered immutable, and
+/// we only need to recursively normalize its sub-`Value`s to get to the NF.
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub(crate) enum ValueKind {
+    /// Closures
+    LamClosure {
+        binder: Binder,
+        annot: Value,
+        closure: Closure,
+    },
+    PiClosure {
+        binder: Binder,
+        annot: Value,
+        closure: Closure,
+    },
+    AppliedBuiltin(BuiltinClosure<Value>),
+
+    Var(NzVar),
+    Const(Const),
+    BoolLit(bool),
+    NaturalLit(Natural),
+    IntegerLit(Integer),
+    DoubleLit(NaiveDouble),
+    EmptyOptionalLit(Value),
+    NEOptionalLit(Value),
+    // EmptyListLit(t) means `[] : List t`, not `[] : t`
+    EmptyListLit(Value),
+    NEListLit(Vec<Value>),
+    RecordType(HashMap<Label, Value>),
+    RecordLit(HashMap<Label, Value>),
+    UnionType(HashMap<Label, Option<Value>>),
+    // Also keep the type of the uniontype around
+    UnionConstructor(Label, HashMap<Label, Option<Value>>, Value),
+    // Also keep the type of the uniontype and the constructor around
+    UnionLit(Label, Value, HashMap<Label, Option<Value>>, Value, Value),
+    TextLit(TextLit),
+    Equivalence(Value, Value),
+    /// Invariant: evaluation must not be able to progress with `normalize_one_layer`?
+    PartialExpr(ExprKind<Value, Normalized>),
+}
+
+impl Value {
+    pub(crate) fn const_sort() -> Value {
+        ValueInternal::from_whnf(
+            ValueKind::Const(Const::Sort),
+            None,
+            Span::Artificial,
+        )
+        .into_value()
+    }
+    /// Construct a Value from a completely unnormalized expression.
+    pub(crate) fn new_thunk(env: &NzEnv, tye: TyExpr) -> Value {
+        ValueInternal::from_thunk(
+            Thunk::new(env, tye.clone()),
+            tye.get_type().ok(),
+            tye.span().clone(),
+        )
+        .into_value()
+    }
+    /// Construct a Value from a partially normalized expression that's not in WHNF.
+    pub(crate) fn from_partial_expr(
+        e: ExprKind<Value, Normalized>,
+        ty: Value,
+    ) -> Value {
+        // TODO: env
+        let env = NzEnv::new();
+        ValueInternal::from_thunk(
+            Thunk::from_partial_expr(env, e, ty.clone()),
+            Some(ty),
+            Span::Artificial,
+        )
+        .into_value()
+    }
+    /// Make a Value from a ValueKind
+    pub(crate) fn from_kind_and_type(v: ValueKind, t: Value) -> Value {
+        ValueInternal::from_whnf(v, Some(t), Span::Artificial).into_value()
+    }
+    pub(crate) fn from_const(c: Const) -> Self {
+        let v = ValueKind::Const(c);
+        match c {
+            Const::Type => {
+                Value::from_kind_and_type(v, Value::from_const(Const::Kind))
+            }
+            Const::Kind => {
+                Value::from_kind_and_type(v, Value::from_const(Const::Sort))
+            }
+            Const::Sort => Value::const_sort(),
+        }
+    }
+    pub(crate) fn from_builtin(b: Builtin) -> Self {
+        Self::from_builtin_env(b, &NzEnv::new())
+    }
+    pub(crate) fn from_builtin_env(b: Builtin, env: &NzEnv) -> Self {
+        Value::from_kind_and_type(
+            ValueKind::from_builtin_env(b, env.clone()),
+            typecheck(&type_of_builtin(b)).unwrap().eval_closed_expr(),
+        )
+    }
+
+    pub(crate) fn as_const(&self) -> Option<Const> {
+        match &*self.kind() {
+            ValueKind::Const(c) => Some(*c),
+            _ => None,
+        }
+    }
+    pub(crate) fn span(&self) -> Span {
+        self.0.span.clone()
+    }
+
+    /// This is what you want if you want to pattern-match on the value.
+    /// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut
+    /// panics.
+    pub(crate) fn kind(&self) -> &ValueKind {
+        self.0.kind()
+    }
+
+    /// Converts a value back to the corresponding AST expression.
+    pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
+        if opts.normalize {
+            self.normalize();
+        }
+
+        self.to_tyexpr_noenv().to_expr(opts)
+    }
+    pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind {
+        self.kind().clone()
+    }
+    /// Before discarding type information, check that it matches the expected return type.
+    pub(crate) fn to_whnf_check_type(&self, ty: &Value) -> ValueKind {
+        self.check_type(ty);
+        self.to_whnf_ignore_type()
+    }
+
+    /// Normalizes contents to normal form; faster than `normalize` if
+    /// no one else shares this.
+    pub(crate) fn normalize_mut(&mut self) {
+        match Rc::get_mut(&mut self.0) {
+            // Mutate directly if sole owner
+            Some(vint) => vint.normalize_mut(),
+            // Otherwise mutate through the refcell
+            None => self.normalize(),
+        }
+    }
+    pub(crate) fn normalize(&self) {
+        self.0.normalize()
+    }
+
+    pub(crate) fn app(&self, v: Value) -> Value {
+        let body_t = match &*self.get_type_not_sort().kind() {
+            ValueKind::PiClosure { annot, closure, .. } => {
+                v.check_type(annot);
+                closure.apply(v.clone())
+            }
+            _ => unreachable!("Internal type error"),
+        };
+        Value::from_kind_and_type(apply_any(self.clone(), v, &body_t), body_t)
+    }
+
+    /// In debug mode, panic if the provided type doesn't match the value's type.
+    /// Otherwise does nothing.
+    pub(crate) fn check_type(&self, _ty: &Value) {
+        // TODO: reenable
+        // debug_assert_eq!(
+        //     Some(ty),
+        //     self.get_type().ok().as_ref(),
+        //     "Internal type error"
+        // );
+    }
+    pub(crate) fn get_type(&self) -> Result<Value, TypeError> {
+        Ok(self.0.get_type()?.clone())
+    }
+    /// When we know the value isn't `Sort`, this gets the type directly
+    pub(crate) fn get_type_not_sort(&self) -> Value {
+        self.get_type()
+            .expect("Internal type error: value is `Sort` but shouldn't be")
+    }
+
+    pub fn to_tyexpr(&self, venv: VarEnv) -> TyExpr {
+        let map_uniontype = |kts: &HashMap<Label, Option<Value>>| {
+            ExprKind::UnionType(
+                kts.iter()
+                    .map(|(k, v)| {
+                        (k.clone(), v.as_ref().map(|v| v.to_tyexpr(venv)))
+                    })
+                    .collect(),
+            )
+        };
+
+        let tye = match &*self.kind() {
+            ValueKind::Var(v) => TyExprKind::Var(venv.lookup(v)),
+            ValueKind::AppliedBuiltin(closure) => closure.to_tyexprkind(venv),
+            self_kind => TyExprKind::Expr(match self_kind {
+                ValueKind::Var(..) | ValueKind::AppliedBuiltin(..) => {
+                    unreachable!()
+                }
+                ValueKind::LamClosure {
+                    binder,
+                    annot,
+                    closure,
+                } => ExprKind::Lam(
+                    binder.to_label(),
+                    annot.to_tyexpr(venv),
+                    closure.to_tyexpr(venv),
+                ),
+                ValueKind::PiClosure {
+                    binder,
+                    annot,
+                    closure,
+                } => ExprKind::Pi(
+                    binder.to_label(),
+                    annot.to_tyexpr(venv),
+                    closure.to_tyexpr(venv),
+                ),
+                ValueKind::Const(c) => ExprKind::Const(*c),
+                ValueKind::BoolLit(b) => ExprKind::BoolLit(*b),
+                ValueKind::NaturalLit(n) => ExprKind::NaturalLit(*n),
+                ValueKind::IntegerLit(n) => ExprKind::IntegerLit(*n),
+                ValueKind::DoubleLit(n) => ExprKind::DoubleLit(*n),
+                ValueKind::EmptyOptionalLit(n) => ExprKind::App(
+                    Value::from_builtin(Builtin::OptionalNone).to_tyexpr(venv),
+                    n.to_tyexpr(venv),
+                ),
+                ValueKind::NEOptionalLit(n) => {
+                    ExprKind::SomeLit(n.to_tyexpr(venv))
+                }
+                ValueKind::EmptyListLit(n) => {
+                    ExprKind::EmptyListLit(TyExpr::new(
+                        TyExprKind::Expr(ExprKind::App(
+                            Value::from_builtin(Builtin::List).to_tyexpr(venv),
+                            n.to_tyexpr(venv),
+                        )),
+                        Some(Value::from_const(Const::Type)),
+                        Span::Artificial,
+                    ))
+                }
+                ValueKind::NEListLit(elts) => ExprKind::NEListLit(
+                    elts.iter().map(|v| v.to_tyexpr(venv)).collect(),
+                ),
+                ValueKind::TextLit(elts) => ExprKind::TextLit(
+                    elts.iter()
+                        .map(|t| t.map_ref(|v| v.to_tyexpr(venv)))
+                        .collect(),
+                ),
+                ValueKind::RecordLit(kvs) => ExprKind::RecordLit(
+                    kvs.iter()
+                        .map(|(k, v)| (k.clone(), v.to_tyexpr(venv)))
+                        .collect(),
+                ),
+                ValueKind::RecordType(kts) => ExprKind::RecordType(
+                    kts.iter()
+                        .map(|(k, v)| (k.clone(), v.to_tyexpr(venv)))
+                        .collect(),
+                ),
+                ValueKind::UnionType(kts) => map_uniontype(kts),
+                ValueKind::UnionConstructor(l, kts, t) => ExprKind::Field(
+                    TyExpr::new(
+                        TyExprKind::Expr(map_uniontype(kts)),
+                        Some(t.clone()),
+                        Span::Artificial,
+                    ),
+                    l.clone(),
+                ),
+                ValueKind::UnionLit(l, v, kts, uniont, ctort) => ExprKind::App(
+                    TyExpr::new(
+                        TyExprKind::Expr(ExprKind::Field(
+                            TyExpr::new(
+                                TyExprKind::Expr(map_uniontype(kts)),
+                                Some(uniont.clone()),
+                                Span::Artificial,
+                            ),
+                            l.clone(),
+                        )),
+                        Some(ctort.clone()),
+                        Span::Artificial,
+                    ),
+                    v.to_tyexpr(venv),
+                ),
+                ValueKind::Equivalence(x, y) => ExprKind::BinOp(
+                    BinOp::Equivalence,
+                    x.to_tyexpr(venv),
+                    y.to_tyexpr(venv),
+                ),
+                ValueKind::PartialExpr(e) => e.map_ref(|v| v.to_tyexpr(venv)),
+            }),
+        };
+
+        TyExpr::new(tye, self.0.ty.clone(), self.0.span.clone())
+    }
+    pub fn to_tyexpr_noenv(&self) -> TyExpr {
+        self.to_tyexpr(VarEnv::new())
+    }
+}
+
+impl ValueInternal {
+    fn from_whnf(k: ValueKind, ty: Option<Value>, span: Span) -> Self {
+        ValueInternal {
+            kind: lazy::Lazy::new_completed(k),
+            ty,
+            span,
+        }
+    }
+    fn from_thunk(th: Thunk, ty: Option<Value>, span: Span) -> Self {
+        ValueInternal {
+            kind: lazy::Lazy::new(th),
+            ty,
+            span,
+        }
+    }
+    fn into_value(self) -> Value {
+        Value(Rc::new(self))
+    }
+
+    fn kind(&self) -> &ValueKind {
+        &self.kind
+    }
+    fn normalize(&self) {
+        self.kind().normalize();
+    }
+    // TODO: deprecated
+    fn normalize_mut(&mut self) {
+        self.normalize();
+    }
+
+    fn get_type(&self) -> Result<&Value, TypeError> {
+        match &self.ty {
+            Some(t) => Ok(t),
+            None => Err(TypeError::new(TypeMessage::Sort)),
+        }
+    }
+}
+
+impl ValueKind {
+    pub(crate) fn into_value_with_type(self, t: Value) -> Value {
+        Value::from_kind_and_type(self, t)
+    }
+
+    pub(crate) fn normalize(&self) {
+        match self {
+            ValueKind::Var(..)
+            | ValueKind::Const(_)
+            | ValueKind::BoolLit(_)
+            | ValueKind::NaturalLit(_)
+            | ValueKind::IntegerLit(_)
+            | ValueKind::DoubleLit(_) => {}
+
+            ValueKind::EmptyOptionalLit(tth) | ValueKind::EmptyListLit(tth) => {
+                tth.normalize();
+            }
+
+            ValueKind::NEOptionalLit(th) => {
+                th.normalize();
+            }
+            ValueKind::LamClosure { annot, closure, .. }
+            | ValueKind::PiClosure { annot, closure, .. } => {
+                annot.normalize();
+                closure.normalize();
+            }
+            ValueKind::AppliedBuiltin(closure) => closure.normalize(),
+            ValueKind::NEListLit(elts) => {
+                for x in elts.iter() {
+                    x.normalize();
+                }
+            }
+            ValueKind::RecordLit(kvs) => {
+                for x in kvs.values() {
+                    x.normalize();
+                }
+            }
+            ValueKind::RecordType(kvs) => {
+                for x in kvs.values() {
+                    x.normalize();
+                }
+            }
+            ValueKind::UnionType(kts)
+            | ValueKind::UnionConstructor(_, kts, _) => {
+                for x in kts.values().flat_map(|opt| opt) {
+                    x.normalize();
+                }
+            }
+            ValueKind::UnionLit(_, v, kts, _, _) => {
+                v.normalize();
+                for x in kts.values().flat_map(|opt| opt) {
+                    x.normalize();
+                }
+            }
+            ValueKind::TextLit(tlit) => tlit.normalize(),
+            ValueKind::Equivalence(x, y) => {
+                x.normalize();
+                y.normalize();
+            }
+            ValueKind::PartialExpr(e) => {
+                e.map_ref(Value::normalize);
+            }
+        }
+    }
+
+    pub(crate) fn from_builtin(b: Builtin) -> ValueKind {
+        ValueKind::from_builtin_env(b, NzEnv::new())
+    }
+    pub(crate) fn from_builtin_env(b: Builtin, env: NzEnv) -> ValueKind {
+        ValueKind::AppliedBuiltin(BuiltinClosure::new(b, env))
+    }
+}
+
+impl Thunk {
+    pub fn new(env: &NzEnv, body: TyExpr) -> Self {
+        Thunk::Thunk {
+            env: env.clone(),
+            body,
+        }
+    }
+    pub fn from_partial_expr(
+        env: NzEnv,
+        expr: ExprKind<Value, Normalized>,
+        ty: Value,
+    ) -> Self {
+        Thunk::PartialExpr { env, expr, ty }
+    }
+    pub fn eval(self) -> ValueKind {
+        match self {
+            Thunk::Thunk { env, body } => normalize_tyexpr_whnf(&body, &env),
+            Thunk::PartialExpr { env, expr, ty } => {
+                normalize_one_layer(expr, &ty, &env)
+            }
+        }
+    }
+}
+
+impl Closure {
+    pub fn new(arg_ty: Value, env: &NzEnv, body: TyExpr) -> Self {
+        Closure::Closure {
+            arg_ty,
+            env: env.clone(),
+            body,
+        }
+    }
+    /// New closure that ignores its argument
+    pub fn new_constant(body: Value) -> Self {
+        Closure::ConstantClosure { body }
+    }
+
+    pub fn apply(&self, val: Value) -> Value {
+        match self {
+            Closure::Closure { env, body, .. } => {
+                body.eval(&env.insert_value(val))
+            }
+            Closure::ConstantClosure { body, .. } => body.clone(),
+        }
+    }
+    fn apply_var(&self, var: NzVar) -> Value {
+        match self {
+            Closure::Closure { arg_ty, .. } => {
+                let val = Value::from_kind_and_type(
+                    ValueKind::Var(var),
+                    arg_ty.clone(),
+                );
+                self.apply(val)
+            }
+            Closure::ConstantClosure { body, .. } => body.clone(),
+        }
+    }
+
+    // TODO: somehow normalize the body. Might require to pass an env.
+    pub fn normalize(&self) {}
+    /// Convert this closure to a TyExpr
+    pub fn to_tyexpr(&self, venv: VarEnv) -> TyExpr {
+        self.apply_var(NzVar::new(venv.size()))
+            .to_tyexpr(venv.insert())
+    }
+    /// If the closure variable is free in the closure, return Err. Otherwise, return the value
+    /// with that free variable remove.
+    pub fn remove_binder(&self) -> Result<Value, ()> {
+        match self {
+            Closure::Closure { .. } => {
+                let v = NzVar::fresh();
+                // TODO: handle case where variable is used in closure
+                // TODO: return information about where the variable is used
+                Ok(self.apply_var(v))
+            }
+            Closure::ConstantClosure { body, .. } => Ok(body.clone()),
+        }
+    }
+}
+
+impl TextLit {
+    pub fn new(
+        elts: impl Iterator<Item = InterpolatedTextContents<Value>>,
+    ) -> Self {
+        TextLit(squash_textlit(elts))
+    }
+    pub fn interpolate(v: Value) -> TextLit {
+        TextLit(vec![InterpolatedTextContents::Expr(v)])
+    }
+    pub fn from_text(s: String) -> TextLit {
+        TextLit(vec![InterpolatedTextContents::Text(s)])
+    }
+
+    pub fn concat(&self, other: &TextLit) -> TextLit {
+        TextLit::new(self.iter().chain(other.iter()).cloned())
+    }
+    pub fn is_empty(&self) -> bool {
+        self.0.is_empty()
+    }
+    /// If the literal consists of only one interpolation and not text, return the interpolated
+    /// value.
+    pub fn as_single_expr(&self) -> Option<&Value> {
+        use InterpolatedTextContents::Expr;
+        if let [Expr(v)] = self.0.as_slice() {
+            Some(v)
+        } else {
+            None
+        }
+    }
+    /// If there are no interpolations, return the corresponding text value.
+    pub fn as_text(&self) -> Option<String> {
+        use InterpolatedTextContents::Text;
+        if self.is_empty() {
+            Some(String::new())
+        } else if let [Text(s)] = self.0.as_slice() {
+            Some(s.clone())
+        } else {
+            None
+        }
+    }
+    pub fn iter(
+        &self,
+    ) -> impl Iterator<Item = &InterpolatedTextContents<Value>> {
+        self.0.iter()
+    }
+    /// Normalize the contained values. This does not break the invariant because we have already
+    /// ensured that no contained values normalize to a TextLit.
+    pub fn normalize(&self) {
+        for x in self.0.iter() {
+            x.map_ref(Value::normalize);
+        }
+    }
+}
+
+impl lazy::Eval<ValueKind> for Thunk {
+    fn eval(self) -> ValueKind {
+        self.eval()
+    }
+}
+
+/// Compare two values for equality modulo alpha/beta-equivalence.
+impl std::cmp::PartialEq for Value {
+    fn eq(&self, other: &Self) -> bool {
+        Rc::ptr_eq(&self.0, &other.0) || self.kind() == other.kind()
+    }
+}
+impl std::cmp::Eq for Value {}
+
+impl std::cmp::PartialEq for Thunk {
+    fn eq(&self, _other: &Self) -> bool {
+        unreachable!(
+            "Trying to compare thunks but we should only compare WHNFs"
+        )
+    }
+}
+impl std::cmp::Eq for Thunk {}
+
+impl std::cmp::PartialEq for Closure {
+    fn eq(&self, other: &Self) -> bool {
+        let v = NzVar::fresh();
+        self.apply_var(v) == other.apply_var(v)
+    }
+}
+impl std::cmp::Eq for Closure {}
+
+impl std::fmt::Debug for Value {
+    fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        let vint: &ValueInternal = &self.0;
+        let kind = vint.kind();
+        if let ValueKind::Const(c) = kind {
+            return write!(fmt, "{:?}", c);
+        }
+        let mut x = fmt.debug_struct(&format!("Value@WHNF"));
+        x.field("kind", kind);
+        if let Some(ty) = vint.ty.as_ref() {
+            x.field("type", &ty);
+        } else {
+            x.field("type", &None::<()>);
+        }
+        x.finish()
+    }
+}
diff --git a/dhall/src/semantics/nze/var.rs b/dhall/src/semantics/nze/var.rs
new file mode 100644
index 0000000..264b81d
--- /dev/null
+++ b/dhall/src/semantics/nze/var.rs
@@ -0,0 +1,36 @@
+use crate::syntax::Label;
+
+// Exactly like a Label, but equality returns always true.
+// This is so that ValueKind equality is exactly alpha-equivalence.
+#[derive(Clone, Eq)]
+pub struct Binder {
+    name: Label,
+}
+
+impl Binder {
+    pub(crate) fn new(name: Label) -> Self {
+        Binder { name }
+    }
+    pub(crate) fn to_label(&self) -> Label {
+        self.clone().into()
+    }
+}
+
+/// Equality up to alpha-equivalence
+impl std::cmp::PartialEq for Binder {
+    fn eq(&self, _other: &Self) -> bool {
+        true
+    }
+}
+
+impl std::fmt::Debug for Binder {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        write!(f, "Binder({})", &self.name)
+    }
+}
+
+impl From<Binder> for Label {
+    fn from(x: Binder) -> Label {
+        x.name
+    }
+}