summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/nze
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/semantics/nze')
-rw-r--r--dhall/src/semantics/nze/mod.rs5
-rw-r--r--dhall/src/semantics/nze/value.rs698
-rw-r--r--dhall/src/semantics/nze/var.rs36
-rw-r--r--dhall/src/semantics/nze/visitor.rs167
4 files changed, 906 insertions, 0 deletions
diff --git a/dhall/src/semantics/nze/mod.rs b/dhall/src/semantics/nze/mod.rs
index 1cd2363..f367f8f 100644
--- a/dhall/src/semantics/nze/mod.rs
+++ b/dhall/src/semantics/nze/mod.rs
@@ -1,2 +1,7 @@
pub mod env;
+pub mod value;
+pub mod var;
+pub mod visitor;
pub(crate) use env::*;
+pub(crate) use value::*;
+pub(crate) use var::*;
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
new file mode 100644
index 0000000..4960076
--- /dev/null
+++ b/dhall/src/semantics/nze/value.rs
@@ -0,0 +1,698 @@
+use std::cell::{Ref, RefCell, RefMut};
+use std::collections::HashMap;
+use std::rc::Rc;
+
+use crate::error::{TypeError, TypeMessage};
+use crate::semantics::nze::visitor;
+use crate::semantics::phase::normalize::{
+ apply_any, normalize_tyexpr_whnf, normalize_whnf,
+};
+use crate::semantics::phase::{Normalized, NormalizedExpr, ToExprOptions};
+use crate::semantics::Binder;
+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 self::Form::{Unevaled, WHNF};
+
+/// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, sharing computation
+/// automatically. Uses a RefCell to share computation.
+/// Can optionally store a type from typechecking to preserve type information.
+/// If you compare for equality two `Value`s in WHNF, 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<RefCell<ValueInternal>>);
+
+/// Invariant: if `form` is `WHNF`, `value` must be in Weak Head Normal Form
+#[derive(Debug)]
+struct ValueInternal {
+ form: Form,
+ kind: ValueKind<Value>,
+ /// This is None if and only if `value` is `Sort` (which doesn't have a type)
+ ty: Option<Value>,
+ span: Span,
+}
+
+#[derive(Debug, Clone, Copy)]
+pub(crate) enum Form {
+ /// No constraints; expression may not be normalized at all.
+ Unevaled,
+ /// Weak Head Normal Form, i.e. normalized up to the first constructor, but subexpressions may
+ /// not be normalized. This means that the first constructor of the contained ValueKind is the first
+ /// constructor of the final Normal Form (NF).
+ /// When all the Values in a ValueKind are in WHNF, and recursively so, then the
+ /// ValueKind is in 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.
+ WHNF,
+}
+
+/// An unevaluated subexpression
+#[derive(Debug, Clone)]
+pub(crate) struct Thunk {
+ env: NzEnv,
+ body: TyExpr,
+}
+
+/// 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 { env: NzEnv, body: TyExpr },
+}
+
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub(crate) enum ValueKind<Value> {
+ /// Closures
+ LamClosure {
+ binder: Binder,
+ annot: Value,
+ closure: Closure,
+ },
+ PiClosure {
+ binder: Binder,
+ annot: Value,
+ closure: Closure,
+ },
+ // Invariant: in whnf, the evaluation must not be able to progress further.
+ 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),
+ // Invariant: in whnf, this must not contain interpolations that are themselves TextLits, and
+ // contiguous text values must be merged.
+ TextLit(Vec<InterpolatedTextContents<Value>>),
+ Equivalence(Value, Value),
+ // Invariant: in whnf, this must not contain a value captured by one of the variants above.
+ PartialExpr(ExprKind<Value, Normalized>),
+ // Invariant: absent in whnf
+ Thunk(Thunk),
+}
+
+impl Value {
+ fn new(kind: ValueKind<Value>, form: Form, ty: Value, span: Span) -> Value {
+ ValueInternal {
+ form,
+ kind,
+ ty: Some(ty),
+ span,
+ }
+ .into_value()
+ }
+ pub(crate) fn const_sort() -> Value {
+ ValueInternal {
+ form: WHNF,
+ kind: ValueKind::Const(Const::Sort),
+ ty: None,
+ span: Span::Artificial,
+ }
+ .into_value()
+ }
+ pub(crate) fn new_thunk(env: &NzEnv, tye: TyExpr) -> Value {
+ ValueInternal {
+ form: Unevaled,
+ kind: ValueKind::Thunk(Thunk::new(env, tye.clone())),
+ ty: tye.get_type().ok(),
+ span: tye.span().clone(),
+ }
+ .into_value()
+ }
+ pub(crate) fn from_kind_and_type(v: ValueKind<Value>, t: Value) -> Value {
+ Value::new(v, Unevaled, t, Span::Artificial)
+ }
+ pub(crate) fn from_kind_and_type_whnf(
+ v: ValueKind<Value>,
+ t: Value,
+ ) -> Value {
+ Value::new(v, WHNF, t, Span::Artificial)
+ }
+ 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.as_internal().span.clone()
+ }
+
+ fn as_internal(&self) -> Ref<ValueInternal> {
+ self.0.borrow()
+ }
+ fn as_internal_mut(&self) -> RefMut<ValueInternal> {
+ self.0.borrow_mut()
+ }
+ /// 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) -> Ref<ValueKind<Value>> {
+ self.normalize_whnf();
+ Ref::map(self.as_internal(), ValueInternal::as_kind)
+ }
+
+ /// Converts a value back to the corresponding AST expression.
+ pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
+ if opts.normalize {
+ self.normalize_nf();
+ }
+
+ self.to_tyexpr_noenv().to_expr(opts)
+ }
+ pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind<Value> {
+ 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<Value> {
+ self.check_type(ty);
+ self.to_whnf_ignore_type()
+ }
+
+ /// Mutates the contents. If no one else shares this, this avoids a RefCell lock.
+ fn mutate_internal(&mut self, f: impl FnOnce(&mut ValueInternal)) {
+ match Rc::get_mut(&mut self.0) {
+ // Mutate directly if sole owner
+ Some(refcell) => f(RefCell::get_mut(refcell)),
+ // Otherwise mutate through the refcell
+ None => f(&mut self.as_internal_mut()),
+ }
+ }
+ /// Normalizes contents to normal form; faster than `normalize_nf` if
+ /// no one else shares this.
+ pub(crate) fn normalize_mut(&mut self) {
+ self.mutate_internal(|vint| vint.normalize_nf())
+ }
+
+ pub(crate) fn normalize_whnf(&self) {
+ let borrow = self.as_internal();
+ match borrow.form {
+ Unevaled => {
+ drop(borrow);
+ self.as_internal_mut().normalize_whnf();
+ }
+ // Already in WHNF
+ WHNF => {}
+ }
+ }
+ pub(crate) fn normalize_nf(&self) {
+ self.as_internal_mut().normalize_nf();
+ }
+
+ 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_whnf(
+ 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.as_internal().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 tye = match &*self.kind() {
+ ValueKind::Var(v) => TyExprKind::Var(venv.lookup(v)),
+ ValueKind::LamClosure {
+ binder,
+ annot,
+ closure,
+ } => TyExprKind::Expr(ExprKind::Lam(
+ binder.to_label(),
+ annot.to_tyexpr(venv),
+ closure.to_tyexpr(venv),
+ )),
+ ValueKind::PiClosure {
+ binder,
+ annot,
+ closure,
+ } => TyExprKind::Expr(ExprKind::Pi(
+ binder.to_label(),
+ annot.to_tyexpr(venv),
+ closure.to_tyexpr(venv),
+ )),
+ ValueKind::AppliedBuiltin(closure) => closure.to_tyexprkind(venv),
+ ValueKind::UnionConstructor(l, kts, t) => {
+ TyExprKind::Expr(ExprKind::Field(
+ TyExpr::new(
+ TyExprKind::Expr(ExprKind::UnionType(
+ kts.into_iter()
+ .map(|(k, v)| {
+ (
+ k.clone(),
+ v.as_ref().map(|v| v.to_tyexpr(venv)),
+ )
+ })
+ .collect(),
+ )),
+ Some(t.clone()),
+ Span::Artificial,
+ ),
+ l.clone(),
+ ))
+ }
+ ValueKind::UnionLit(l, v, kts, uniont, ctort) => {
+ TyExprKind::Expr(ExprKind::App(
+ TyExpr::new(
+ TyExprKind::Expr(ExprKind::Field(
+ TyExpr::new(
+ TyExprKind::Expr(ExprKind::UnionType(
+ kts.into_iter()
+ .map(|(k, v)| {
+ (
+ k.clone(),
+ v.as_ref()
+ .map(|v| v.to_tyexpr(venv)),
+ )
+ })
+ .collect(),
+ )),
+ Some(uniont.clone()),
+ Span::Artificial,
+ ),
+ l.clone(),
+ )),
+ Some(ctort.clone()),
+ Span::Artificial,
+ ),
+ v.to_tyexpr(venv),
+ ))
+ }
+ ValueKind::Thunk(th) => return th.to_tyexpr(venv),
+ self_kind => {
+ let self_kind = self_kind.map_ref(|v| v.to_tyexpr(venv));
+ let expr = match self_kind {
+ ValueKind::Var(..)
+ | ValueKind::LamClosure { .. }
+ | ValueKind::PiClosure { .. }
+ | ValueKind::AppliedBuiltin(..)
+ | ValueKind::UnionConstructor(..)
+ | ValueKind::UnionLit(..)
+ | ValueKind::Thunk(..) => unreachable!(),
+ 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,
+ ),
+ ValueKind::NEOptionalLit(n) => ExprKind::SomeLit(n),
+ ValueKind::EmptyListLit(n) => {
+ ExprKind::EmptyListLit(TyExpr::new(
+ TyExprKind::Expr(ExprKind::App(
+ Value::from_builtin(Builtin::List)
+ .to_tyexpr(venv),
+ n,
+ )),
+ Some(Value::from_const(Const::Type)),
+ Span::Artificial,
+ ))
+ }
+ ValueKind::NEListLit(elts) => ExprKind::NEListLit(elts),
+ ValueKind::RecordLit(kvs) => {
+ ExprKind::RecordLit(kvs.into_iter().collect())
+ }
+ ValueKind::RecordType(kts) => {
+ ExprKind::RecordType(kts.into_iter().collect())
+ }
+ ValueKind::UnionType(kts) => {
+ ExprKind::UnionType(kts.into_iter().collect())
+ }
+ ValueKind::TextLit(elts) => {
+ ExprKind::TextLit(elts.into_iter().collect())
+ }
+ ValueKind::Equivalence(x, y) => {
+ ExprKind::BinOp(BinOp::Equivalence, x, y)
+ }
+ ValueKind::PartialExpr(e) => e,
+ };
+ TyExprKind::Expr(expr)
+ }
+ };
+
+ let self_ty = self.as_internal().ty.clone();
+ let self_span = self.as_internal().span.clone();
+ TyExpr::new(tye, self_ty, self_span)
+ }
+ pub fn to_tyexpr_noenv(&self) -> TyExpr {
+ self.to_tyexpr(VarEnv::new())
+ }
+}
+
+impl ValueInternal {
+ fn into_value(self) -> Value {
+ Value(Rc::new(RefCell::new(self)))
+ }
+ fn as_kind(&self) -> &ValueKind<Value> {
+ &self.kind
+ }
+
+ fn normalize_whnf(&mut self) {
+ let dummy = ValueInternal {
+ form: Unevaled,
+ kind: ValueKind::Const(Const::Type),
+ ty: None,
+ span: Span::Artificial,
+ };
+ let vint = std::mem::replace(self, dummy);
+ *self = match (&vint.form, &vint.ty) {
+ (Unevaled, Some(ty)) => ValueInternal {
+ form: WHNF,
+ kind: normalize_whnf(vint.kind, &ty),
+ ty: vint.ty,
+ span: vint.span,
+ },
+ // `value` is `Sort`
+ (Unevaled, None) => ValueInternal {
+ form: WHNF,
+ kind: ValueKind::Const(Const::Sort),
+ ty: None,
+ span: vint.span,
+ },
+ // Already in WHNF
+ (WHNF, _) => vint,
+ }
+ }
+ fn normalize_nf(&mut self) {
+ if let Unevaled = self.form {
+ self.normalize_whnf();
+ }
+ self.kind.normalize_mut();
+ }
+
+ fn get_type(&self) -> Result<&Value, TypeError> {
+ match &self.ty {
+ Some(t) => Ok(t),
+ None => Err(TypeError::new(TypeMessage::Sort)),
+ }
+ }
+}
+
+impl ValueKind<Value> {
+ pub(crate) fn into_value_with_type(self, t: Value) -> Value {
+ Value::from_kind_and_type(self, t)
+ }
+
+ pub(crate) fn normalize_mut(&mut self) {
+ match self {
+ ValueKind::Var(..)
+ | ValueKind::Const(_)
+ | ValueKind::BoolLit(_)
+ | ValueKind::NaturalLit(_)
+ | ValueKind::IntegerLit(_)
+ | ValueKind::DoubleLit(_) => {}
+
+ ValueKind::EmptyOptionalLit(tth) | ValueKind::EmptyListLit(tth) => {
+ tth.normalize_mut();
+ }
+
+ ValueKind::NEOptionalLit(th) => {
+ th.normalize_mut();
+ }
+ ValueKind::LamClosure { annot, .. }
+ | ValueKind::PiClosure { annot, .. } => {
+ annot.normalize_mut();
+ }
+ ValueKind::AppliedBuiltin(closure) => closure.normalize_mut(),
+ ValueKind::NEListLit(elts) => {
+ for x in elts.iter_mut() {
+ x.normalize_mut();
+ }
+ }
+ ValueKind::RecordLit(kvs) => {
+ for x in kvs.values_mut() {
+ x.normalize_mut();
+ }
+ }
+ ValueKind::RecordType(kvs) => {
+ for x in kvs.values_mut() {
+ x.normalize_mut();
+ }
+ }
+ ValueKind::UnionType(kts)
+ | ValueKind::UnionConstructor(_, kts, _) => {
+ for x in kts.values_mut().flat_map(|opt| opt) {
+ x.normalize_mut();
+ }
+ }
+ ValueKind::UnionLit(_, v, kts, _, _) => {
+ v.normalize_mut();
+ for x in kts.values_mut().flat_map(|opt| opt) {
+ x.normalize_mut();
+ }
+ }
+ ValueKind::TextLit(elts) => {
+ for x in elts.iter_mut() {
+ x.map_mut(Value::normalize_mut);
+ }
+ }
+ ValueKind::Equivalence(x, y) => {
+ x.normalize_mut();
+ y.normalize_mut();
+ }
+ ValueKind::PartialExpr(e) => {
+ e.map_mut(Value::normalize_mut);
+ }
+ ValueKind::Thunk(..) => {
+ unreachable!("Should only normalize_mut values in WHNF")
+ }
+ }
+ }
+
+ pub(crate) fn from_builtin(b: Builtin) -> ValueKind<Value> {
+ ValueKind::from_builtin_env(b, NzEnv::new())
+ }
+ pub(crate) fn from_builtin_env(b: Builtin, env: NzEnv) -> ValueKind<Value> {
+ ValueKind::AppliedBuiltin(BuiltinClosure::new(b, env))
+ }
+}
+
+impl<V> ValueKind<V> {
+ fn traverse_ref_with_special_handling_of_binders<'a, V2, E>(
+ &'a self,
+ visit_val: impl FnMut(&'a V) -> Result<V2, E>,
+ visit_under_binder: impl for<'b> FnMut(
+ &'a Binder,
+ &'b V,
+ &'a V,
+ ) -> Result<V2, E>,
+ ) -> Result<ValueKind<V2>, E> {
+ use visitor::ValueKindVisitor;
+ visitor::TraverseRefWithBindersVisitor {
+ visit_val,
+ visit_under_binder,
+ }
+ .visit(self)
+ }
+
+ fn map_ref_with_special_handling_of_binders<'a, V2>(
+ &'a self,
+ mut map_val: impl FnMut(&'a V) -> V2,
+ mut map_under_binder: impl for<'b> FnMut(&'a Binder, &'b V, &'a V) -> V2,
+ ) -> ValueKind<V2> {
+ use crate::syntax::trivial_result;
+ trivial_result(self.traverse_ref_with_special_handling_of_binders(
+ |x| Ok(map_val(x)),
+ |l, t, x| Ok(map_under_binder(l, t, x)),
+ ))
+ }
+
+ fn map_ref<'a, V2>(
+ &'a self,
+ map_val: impl Fn(&'a V) -> V2,
+ ) -> ValueKind<V2> {
+ self.map_ref_with_special_handling_of_binders(&map_val, |_, _, x| {
+ map_val(x)
+ })
+ }
+}
+
+impl Thunk {
+ pub fn new(env: &NzEnv, body: TyExpr) -> Self {
+ Thunk {
+ env: env.clone(),
+ body,
+ }
+ }
+
+ pub fn eval(&self) -> Value {
+ normalize_tyexpr_whnf(&self.body, &self.env)
+ }
+ pub fn to_tyexpr(&self, venv: VarEnv) -> TyExpr {
+ self.eval().to_tyexpr(venv)
+ }
+}
+
+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(env: &NzEnv, body: TyExpr) -> Self {
+ Closure::ConstantClosure {
+ env: env.clone(),
+ body,
+ }
+ }
+
+ pub fn apply(&self, val: Value) -> Value {
+ match self {
+ Closure::Closure { env, body, .. } => {
+ body.eval(&env.insert_value(val))
+ }
+ Closure::ConstantClosure { env, body, .. } => body.eval(env),
+ }
+ }
+ 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 { env, body, .. } => body.eval(env),
+ }
+ }
+
+ /// 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, ()> {
+ let v = NzVar::fresh();
+ match self {
+ Closure::Closure { .. } => {
+ // 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 { .. } => {
+ // Ok: the variable is indeed ignored
+ Ok(self.apply_var(v))
+ }
+ }
+ }
+}
+
+/// Compare two values for equality modulo alpha/beta-equivalence.
+// TODO: use Rc comparison to shortcut on identical pointers
+impl std::cmp::PartialEq for Value {
+ fn eq(&self, other: &Self) -> bool {
+ *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.as_internal();
+ if let ValueKind::Const(c) = &vint.kind {
+ write!(fmt, "{:?}", c)
+ } else {
+ let mut x = fmt.debug_struct(&format!("Value@{:?}", &vint.form));
+ x.field("value", &vint.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
+ }
+}
diff --git a/dhall/src/semantics/nze/visitor.rs b/dhall/src/semantics/nze/visitor.rs
new file mode 100644
index 0000000..d1a85d8
--- /dev/null
+++ b/dhall/src/semantics/nze/visitor.rs
@@ -0,0 +1,167 @@
+use std::iter::FromIterator;
+
+use crate::semantics::{Binder, BuiltinClosure, ValueKind};
+use crate::syntax::Label;
+
+/// A visitor trait that can be used to traverse `ValueKind`s. We need this pattern so that Rust lets
+/// us have as much mutability as we can. See the equivalent file in `crate::syntax` for more
+/// details.
+pub(crate) trait ValueKindVisitor<'a, V1, V2>: Sized {
+ type Error;
+
+ fn visit_val(&mut self, val: &'a V1) -> Result<V2, Self::Error>;
+ fn visit_binder(
+ mut self,
+ _label: &'a Binder,
+ ty: &'a V1,
+ val: &'a V1,
+ ) -> Result<(V2, V2), Self::Error> {
+ Ok((self.visit_val(ty)?, self.visit_val(val)?))
+ }
+ fn visit_vec(&mut self, x: &'a [V1]) -> Result<Vec<V2>, Self::Error> {
+ x.iter().map(|e| self.visit_val(e)).collect()
+ }
+ fn visit_opt(
+ &mut self,
+ x: &'a Option<V1>,
+ ) -> Result<Option<V2>, Self::Error> {
+ Ok(match x {
+ Some(x) => Some(self.visit_val(x)?),
+ None => None,
+ })
+ }
+ fn visit_map<T>(
+ &mut self,
+ x: impl IntoIterator<Item = (&'a Label, &'a V1)>,
+ ) -> Result<T, Self::Error>
+ where
+ V1: 'a,
+ T: FromIterator<(Label, V2)>,
+ {
+ x.into_iter()
+ .map(|(k, x)| Ok((k.clone(), self.visit_val(x)?)))
+ .collect()
+ }
+ fn visit_optmap<T>(
+ &mut self,
+ x: impl IntoIterator<Item = (&'a Label, &'a Option<V1>)>,
+ ) -> Result<T, Self::Error>
+ where
+ V1: 'a,
+ T: FromIterator<(Label, Option<V2>)>,
+ {
+ x.into_iter()
+ .map(|(k, x)| Ok((k.clone(), self.visit_opt(x)?)))
+ .collect()
+ }
+
+ fn visit(
+ self,
+ input: &'a ValueKind<V1>,
+ ) -> Result<ValueKind<V2>, Self::Error> {
+ visit_ref(self, input)
+ }
+}
+
+fn visit_ref<'a, Visitor, V1, V2>(
+ mut v: Visitor,
+ input: &'a ValueKind<V1>,
+) -> Result<ValueKind<V2>, Visitor::Error>
+where
+ Visitor: ValueKindVisitor<'a, V1, V2>,
+{
+ use ValueKind::*;
+ Ok(match input {
+ LamClosure {
+ binder,
+ annot,
+ closure,
+ } => LamClosure {
+ binder: binder.clone(),
+ annot: v.visit_val(annot)?,
+ closure: closure.clone(),
+ },
+ PiClosure {
+ binder,
+ annot,
+ closure,
+ } => PiClosure {
+ binder: binder.clone(),
+ annot: v.visit_val(annot)?,
+ closure: closure.clone(),
+ },
+ AppliedBuiltin(BuiltinClosure {
+ b,
+ args,
+ types,
+ env,
+ }) => AppliedBuiltin(BuiltinClosure {
+ b: *b,
+ args: v.visit_vec(args)?,
+ types: v.visit_vec(types)?,
+ env: env.clone(),
+ }),
+ Var(v) => Var(*v),
+ Const(k) => Const(*k),
+ BoolLit(b) => BoolLit(*b),
+ NaturalLit(n) => NaturalLit(*n),
+ IntegerLit(n) => IntegerLit(*n),
+ DoubleLit(n) => DoubleLit(*n),
+ EmptyOptionalLit(t) => EmptyOptionalLit(v.visit_val(t)?),
+ NEOptionalLit(x) => NEOptionalLit(v.visit_val(x)?),
+ EmptyListLit(t) => EmptyListLit(v.visit_val(t)?),
+ NEListLit(xs) => NEListLit(v.visit_vec(xs)?),
+ RecordType(kts) => RecordType(v.visit_map(kts)?),
+ RecordLit(kvs) => RecordLit(v.visit_map(kvs)?),
+ UnionType(kts) => UnionType(v.visit_optmap(kts)?),
+ UnionConstructor(l, kts, uniont) => UnionConstructor(
+ l.clone(),
+ v.visit_optmap(kts)?,
+ v.visit_val(uniont)?,
+ ),
+ UnionLit(l, x, kts, uniont, ctort) => UnionLit(
+ l.clone(),
+ v.visit_val(x)?,
+ v.visit_optmap(kts)?,
+ v.visit_val(uniont)?,
+ v.visit_val(ctort)?,
+ ),
+ TextLit(ts) => TextLit(
+ ts.iter()
+ .map(|t| t.traverse_ref(|e| v.visit_val(e)))
+ .collect::<Result<_, _>>()?,
+ ),
+ Equivalence(x, y) => Equivalence(v.visit_val(x)?, v.visit_val(y)?),
+ PartialExpr(e) => PartialExpr(e.traverse_ref(|e| v.visit_val(e))?),
+ Thunk(th) => Thunk(th.clone()),
+ })
+}
+
+pub struct TraverseRefWithBindersVisitor<F1, F2> {
+ pub visit_val: F1,
+ pub visit_under_binder: F2,
+}
+
+impl<'a, V1, V2, Err, F1, F2> ValueKindVisitor<'a, V1, V2>
+ for TraverseRefWithBindersVisitor<F1, F2>
+where
+ V1: 'a,
+ F1: FnMut(&'a V1) -> Result<V2, Err>,
+ F2: for<'b> FnOnce(&'a Binder, &'b V1, &'a V1) -> Result<V2, Err>,
+{
+ type Error = Err;
+
+ fn visit_val(&mut self, val: &'a V1) -> Result<V2, Self::Error> {
+ (self.visit_val)(val)
+ }
+ fn visit_binder<'b>(
+ mut self,
+ label: &'a Binder,
+ ty: &'a V1,
+ val: &'a V1,
+ ) -> Result<(V2, V2), Self::Error> {
+ let val = (self.visit_under_binder)(label, ty, val)?;
+ let ty = (self.visit_val)(ty)?;
+ Ok((ty, val))
+ }
+}