From 0c95dd4f940e796865976dad594068ae0fff8f7c Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 17:01:36 +0000 Subject: Move Value-related stuff under semantics::nze --- dhall/src/error/mod.rs | 2 +- dhall/src/semantics/core/context.rs | 1 - dhall/src/semantics/core/mod.rs | 6 - dhall/src/semantics/core/value.rs | 698 ------------------------------------ dhall/src/semantics/core/var.rs | 36 -- dhall/src/semantics/core/visitor.rs | 167 --------- dhall/src/semantics/mod.rs | 2 - dhall/src/semantics/nze/mod.rs | 5 + dhall/src/semantics/nze/value.rs | 698 ++++++++++++++++++++++++++++++++++++ dhall/src/semantics/nze/var.rs | 36 ++ dhall/src/semantics/nze/visitor.rs | 167 +++++++++ 11 files changed, 907 insertions(+), 911 deletions(-) delete mode 100644 dhall/src/semantics/core/context.rs delete mode 100644 dhall/src/semantics/core/mod.rs delete mode 100644 dhall/src/semantics/core/value.rs delete mode 100644 dhall/src/semantics/core/var.rs delete mode 100644 dhall/src/semantics/core/visitor.rs create mode 100644 dhall/src/semantics/nze/value.rs create mode 100644 dhall/src/semantics/nze/var.rs create mode 100644 dhall/src/semantics/nze/visitor.rs (limited to 'dhall/src') diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs index 215a7bf..852e795 100644 --- a/dhall/src/error/mod.rs +++ b/dhall/src/error/mod.rs @@ -1,8 +1,8 @@ use std::io::Error as IOError; -use crate::semantics::core::value::Value; use crate::semantics::phase::resolve::ImportStack; use crate::semantics::phase::NormalizedExpr; +use crate::semantics::Value; use crate::syntax::{Import, ParseError}; pub type Result = std::result::Result; diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs deleted file mode 100644 index 8b13789..0000000 --- a/dhall/src/semantics/core/context.rs +++ /dev/null @@ -1 +0,0 @@ - diff --git a/dhall/src/semantics/core/mod.rs b/dhall/src/semantics/core/mod.rs deleted file mode 100644 index 6f577f0..0000000 --- a/dhall/src/semantics/core/mod.rs +++ /dev/null @@ -1,6 +0,0 @@ -pub mod context; -pub mod value; -pub mod var; -pub mod visitor; -pub(crate) use value::*; -pub(crate) use var::*; diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs deleted file mode 100644 index c881a9a..0000000 --- a/dhall/src/semantics/core/value.rs +++ /dev/null @@ -1,698 +0,0 @@ -use std::cell::{Ref, RefCell, RefMut}; -use std::collections::HashMap; -use std::rc::Rc; - -use crate::error::{TypeError, TypeMessage}; -use crate::semantics::core::var::Binder; -use crate::semantics::phase::normalize::{ - apply_any, normalize_tyexpr_whnf, normalize_whnf, -}; -use crate::semantics::phase::{Normalized, NormalizedExpr, ToExprOptions}; -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>); - -/// Invariant: if `form` is `WHNF`, `value` must be in Weak Head Normal Form -#[derive(Debug)] -struct ValueInternal { - form: Form, - kind: ValueKind, - /// This is None if and only if `value` is `Sort` (which doesn't have a type) - ty: Option, - 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 { - /// 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), - - 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), - RecordType(HashMap), - RecordLit(HashMap), - UnionType(HashMap>), - // Also keep the type of the uniontype around - UnionConstructor(Label, HashMap>, Value), - // Also keep the type of the uniontype and the constructor around - UnionLit(Label, Value, HashMap>, Value, Value), - // Invariant: in whnf, this must not contain interpolations that are themselves TextLits, and - // contiguous text values must be merged. - TextLit(Vec>), - Equivalence(Value, Value), - // Invariant: in whnf, this must not contain a value captured by one of the variants above. - PartialExpr(ExprKind), - // Invariant: absent in whnf - Thunk(Thunk), -} - -impl Value { - fn new(kind: ValueKind, 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, t: Value) -> Value { - Value::new(v, Unevaled, t, Span::Artificial) - } - pub(crate) fn from_kind_and_type_whnf( - v: ValueKind, - 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 { - 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 { - self.0.borrow() - } - fn as_internal_mut(&self) -> RefMut { - 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> { - 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 { - 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() - } - - /// 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 { - 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 { - &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 { - 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 { - 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 ValueKind { - fn traverse_ref_with_special_handling_of_binders<'a, V2, E>( - &'a self, - visit_val: impl FnMut(&'a V) -> Result, - visit_under_binder: impl for<'b> FnMut( - &'a Binder, - &'b V, - &'a V, - ) -> Result, - ) -> Result, E> { - use crate::semantics::visitor; - 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 { - 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 { - 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 { - 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/core/var.rs b/dhall/src/semantics/core/var.rs deleted file mode 100644 index 264b81d..0000000 --- a/dhall/src/semantics/core/var.rs +++ /dev/null @@ -1,36 +0,0 @@ -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 for Label { - fn from(x: Binder) -> Label { - x.name - } -} diff --git a/dhall/src/semantics/core/visitor.rs b/dhall/src/semantics/core/visitor.rs deleted file mode 100644 index d1a85d8..0000000 --- a/dhall/src/semantics/core/visitor.rs +++ /dev/null @@ -1,167 +0,0 @@ -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; - 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, Self::Error> { - x.iter().map(|e| self.visit_val(e)).collect() - } - fn visit_opt( - &mut self, - x: &'a Option, - ) -> Result, Self::Error> { - Ok(match x { - Some(x) => Some(self.visit_val(x)?), - None => None, - }) - } - fn visit_map( - &mut self, - x: impl IntoIterator, - ) -> Result - where - V1: 'a, - T: FromIterator<(Label, V2)>, - { - x.into_iter() - .map(|(k, x)| Ok((k.clone(), self.visit_val(x)?))) - .collect() - } - fn visit_optmap( - &mut self, - x: impl IntoIterator)>, - ) -> Result - where - V1: 'a, - T: FromIterator<(Label, Option)>, - { - x.into_iter() - .map(|(k, x)| Ok((k.clone(), self.visit_opt(x)?))) - .collect() - } - - fn visit( - self, - input: &'a ValueKind, - ) -> Result, Self::Error> { - visit_ref(self, input) - } -} - -fn visit_ref<'a, Visitor, V1, V2>( - mut v: Visitor, - input: &'a ValueKind, -) -> Result, 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::>()?, - ), - 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 { - pub visit_val: F1, - pub visit_under_binder: F2, -} - -impl<'a, V1, V2, Err, F1, F2> ValueKindVisitor<'a, V1, V2> - for TraverseRefWithBindersVisitor -where - V1: 'a, - F1: FnMut(&'a V1) -> Result, - F2: for<'b> FnOnce(&'a Binder, &'b V1, &'a V1) -> Result, -{ - type Error = Err; - - fn visit_val(&mut self, val: &'a V1) -> Result { - (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)) - } -} diff --git a/dhall/src/semantics/mod.rs b/dhall/src/semantics/mod.rs index 01bbd39..92e5912 100644 --- a/dhall/src/semantics/mod.rs +++ b/dhall/src/semantics/mod.rs @@ -1,9 +1,7 @@ pub mod builtins; -pub mod core; pub mod nze; pub mod phase; pub mod tck; pub(crate) use self::builtins::*; -pub(crate) use self::core::*; pub(crate) use self::nze::*; pub(crate) use self::tck::*; diff --git a/dhall/src/semantics/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>); + +/// Invariant: if `form` is `WHNF`, `value` must be in Weak Head Normal Form +#[derive(Debug)] +struct ValueInternal { + form: Form, + kind: ValueKind, + /// This is None if and only if `value` is `Sort` (which doesn't have a type) + ty: Option, + 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 { + /// 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), + + 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), + RecordType(HashMap), + RecordLit(HashMap), + UnionType(HashMap>), + // Also keep the type of the uniontype around + UnionConstructor(Label, HashMap>, Value), + // Also keep the type of the uniontype and the constructor around + UnionLit(Label, Value, HashMap>, Value, Value), + // Invariant: in whnf, this must not contain interpolations that are themselves TextLits, and + // contiguous text values must be merged. + TextLit(Vec>), + Equivalence(Value, Value), + // Invariant: in whnf, this must not contain a value captured by one of the variants above. + PartialExpr(ExprKind), + // Invariant: absent in whnf + Thunk(Thunk), +} + +impl Value { + fn new(kind: ValueKind, 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, t: Value) -> Value { + Value::new(v, Unevaled, t, Span::Artificial) + } + pub(crate) fn from_kind_and_type_whnf( + v: ValueKind, + 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 { + 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 { + self.0.borrow() + } + fn as_internal_mut(&self) -> RefMut { + 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> { + 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 { + 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() + } + + /// 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 { + 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 { + &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 { + 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 { + 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 ValueKind { + fn traverse_ref_with_special_handling_of_binders<'a, V2, E>( + &'a self, + visit_val: impl FnMut(&'a V) -> Result, + visit_under_binder: impl for<'b> FnMut( + &'a Binder, + &'b V, + &'a V, + ) -> Result, + ) -> Result, 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 { + 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 { + 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 { + 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 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; + 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, Self::Error> { + x.iter().map(|e| self.visit_val(e)).collect() + } + fn visit_opt( + &mut self, + x: &'a Option, + ) -> Result, Self::Error> { + Ok(match x { + Some(x) => Some(self.visit_val(x)?), + None => None, + }) + } + fn visit_map( + &mut self, + x: impl IntoIterator, + ) -> Result + where + V1: 'a, + T: FromIterator<(Label, V2)>, + { + x.into_iter() + .map(|(k, x)| Ok((k.clone(), self.visit_val(x)?))) + .collect() + } + fn visit_optmap( + &mut self, + x: impl IntoIterator)>, + ) -> Result + where + V1: 'a, + T: FromIterator<(Label, Option)>, + { + x.into_iter() + .map(|(k, x)| Ok((k.clone(), self.visit_opt(x)?))) + .collect() + } + + fn visit( + self, + input: &'a ValueKind, + ) -> Result, Self::Error> { + visit_ref(self, input) + } +} + +fn visit_ref<'a, Visitor, V1, V2>( + mut v: Visitor, + input: &'a ValueKind, +) -> Result, 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::>()?, + ), + 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 { + pub visit_val: F1, + pub visit_under_binder: F2, +} + +impl<'a, V1, V2, Err, F1, F2> ValueKindVisitor<'a, V1, V2> + for TraverseRefWithBindersVisitor +where + V1: 'a, + F1: FnMut(&'a V1) -> Result, + F2: for<'b> FnOnce(&'a Binder, &'b V1, &'a V1) -> Result, +{ + type Error = Err; + + fn visit_val(&mut self, val: &'a V1) -> Result { + (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)) + } +} -- cgit v1.2.3