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/semantics/nze/value.rs | 698 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 698 insertions(+) create mode 100644 dhall/src/semantics/nze/value.rs (limited to 'dhall/src/semantics/nze/value.rs') 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() + } + } +} -- cgit v1.2.3 From 653cdb44cec4f54697d18f2c4ae9f67bbbc2fb3d Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 17:04:28 +0000 Subject: Move normalize under nze --- dhall/src/semantics/nze/value.rs | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) (limited to 'dhall/src/semantics/nze/value.rs') diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index 4960076..215c342 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -4,11 +4,9 @@ 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::{apply_any, normalize_tyexpr_whnf, normalize_whnf}; use crate::semantics::{type_of_builtin, typecheck, TyExpr, TyExprKind}; use crate::semantics::{BuiltinClosure, NzEnv, NzVar, VarEnv}; use crate::syntax::{ -- cgit v1.2.3 From 5197c26c23edd6c499f8e0f8a239fe4393b2e3d2 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 17:09:16 +0000 Subject: Move main API to lib.rs --- dhall/src/semantics/nze/value.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'dhall/src/semantics/nze/value.rs') diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index 215c342..0a9de6a 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -4,7 +4,6 @@ use std::rc::Rc; use crate::error::{TypeError, TypeMessage}; use crate::semantics::nze::visitor; -use crate::semantics::phase::{Normalized, NormalizedExpr, ToExprOptions}; use crate::semantics::Binder; use crate::semantics::{apply_any, normalize_tyexpr_whnf, normalize_whnf}; use crate::semantics::{type_of_builtin, typecheck, TyExpr, TyExprKind}; @@ -13,6 +12,7 @@ use crate::syntax::{ BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label, NaiveDouble, Natural, Span, }; +use crate::{Normalized, NormalizedExpr, ToExprOptions}; use self::Form::{Unevaled, WHNF}; -- cgit v1.2.3 From 7062de011eab7954f4bcf78fa1cf970ba91d6a5a Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 18:04:16 +0000 Subject: Remove Value visitor It's mostly useful when we can change types, but it's also too constraining if we can, because then we can't enforce complex invariants like the one for TextLit. --- dhall/src/semantics/nze/value.rs | 228 +++++++++++++++------------------------ 1 file changed, 87 insertions(+), 141 deletions(-) (limited to 'dhall/src/semantics/nze/value.rs') diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index 0a9de6a..6ab6fe3 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -3,7 +3,6 @@ use std::collections::HashMap; use std::rc::Rc; use crate::error::{TypeError, TypeMessage}; -use crate::semantics::nze::visitor; use crate::semantics::Binder; use crate::semantics::{apply_any, normalize_tyexpr_whnf, normalize_whnf}; use crate::semantics::{type_of_builtin, typecheck, TyExpr, TyExprKind}; @@ -276,62 +275,96 @@ impl Value { } pub fn to_tyexpr(&self, venv: VarEnv) -> TyExpr { + let map_uniontype = |kts: &HashMap>| { + 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::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(), + ValueKind::Thunk(th) => return th.to_tyexpr(venv), + self_kind => TyExprKind::Expr(match self_kind { + ValueKind::Var(..) + | ValueKind::AppliedBuiltin(..) + | ValueKind::Thunk(..) => 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) => { - TyExprKind::Expr(ExprKind::App( + ), + ValueKind::UnionLit(l, v, kts, uniont, ctort) => 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(), - )), + TyExprKind::Expr(map_uniontype(kts)), Some(uniont.clone()), Span::Artificial, ), @@ -341,61 +374,14 @@ impl Value { 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) - } + ), + 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)), + }), }; let self_ty = self.as_internal().ty.clone(); @@ -535,46 +521,6 @@ impl ValueKind { } } -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 { -- cgit v1.2.3 From 0749482ad2ab9340fb45a2fe2997d2ea04516d75 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 18:06:53 +0000 Subject: Remove type parameter from ValueKind --- dhall/src/semantics/nze/value.rs | 27 ++++++++++++--------------- 1 file changed, 12 insertions(+), 15 deletions(-) (limited to 'dhall/src/semantics/nze/value.rs') diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index 6ab6fe3..8fad911 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -28,7 +28,7 @@ pub(crate) struct Value(Rc>); #[derive(Debug)] struct ValueInternal { form: Form, - kind: ValueKind, + kind: ValueKind, /// This is None if and only if `value` is `Sort` (which doesn't have a type) ty: Option, span: Span, @@ -68,7 +68,7 @@ pub(crate) enum Closure { } #[derive(Debug, Clone, PartialEq, Eq)] -pub(crate) enum ValueKind { +pub(crate) enum ValueKind { /// Closures LamClosure { binder: Binder, @@ -112,7 +112,7 @@ pub(crate) enum ValueKind { } impl Value { - fn new(kind: ValueKind, form: Form, ty: Value, span: Span) -> Value { + fn new(kind: ValueKind, form: Form, ty: Value, span: Span) -> Value { ValueInternal { form, kind, @@ -139,13 +139,10 @@ impl Value { } .into_value() } - pub(crate) fn from_kind_and_type(v: ValueKind, t: Value) -> 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 { + 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 { @@ -189,7 +186,7 @@ impl Value { /// 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> { + pub(crate) fn kind(&self) -> Ref { self.normalize_whnf(); Ref::map(self.as_internal(), ValueInternal::as_kind) } @@ -202,11 +199,11 @@ impl Value { self.to_tyexpr_noenv().to_expr(opts) } - pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind { + 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 { + pub(crate) fn to_whnf_check_type(&self, ty: &Value) -> ValueKind { self.check_type(ty); self.to_whnf_ignore_type() } @@ -397,7 +394,7 @@ impl ValueInternal { fn into_value(self) -> Value { Value(Rc::new(RefCell::new(self))) } - fn as_kind(&self) -> &ValueKind { + fn as_kind(&self) -> &ValueKind { &self.kind } @@ -442,7 +439,7 @@ impl ValueInternal { } } -impl ValueKind { +impl ValueKind { pub(crate) fn into_value_with_type(self, t: Value) -> Value { Value::from_kind_and_type(self, t) } @@ -513,10 +510,10 @@ impl ValueKind { } } - pub(crate) fn from_builtin(b: Builtin) -> ValueKind { + 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 { + pub(crate) fn from_builtin_env(b: Builtin, env: NzEnv) -> ValueKind { ValueKind::AppliedBuiltin(BuiltinClosure::new(b, env)) } } -- cgit v1.2.3 From dc01ef2030e1177e4f247f4ddc0a3f69241d5cfc Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 18:32:22 +0000 Subject: Factor out text literals in Value This allows encapsulating invariants properly and reducing clutter --- dhall/src/semantics/nze/value.rs | 74 +++++++++++++++++++++++++++++++++++----- 1 file changed, 65 insertions(+), 9 deletions(-) (limited to 'dhall/src/semantics/nze/value.rs') diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index 8fad911..06d8df8 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -4,7 +4,9 @@ use std::rc::Rc; use crate::error::{TypeError, TypeMessage}; use crate::semantics::Binder; -use crate::semantics::{apply_any, normalize_tyexpr_whnf, normalize_whnf}; +use crate::semantics::{ + apply_any, normalize_tyexpr_whnf, normalize_whnf, squash_textlit, +}; use crate::semantics::{type_of_builtin, typecheck, TyExpr, TyExprKind}; use crate::semantics::{BuiltinClosure, NzEnv, NzVar, VarEnv}; use crate::syntax::{ @@ -67,6 +69,12 @@ pub(crate) enum Closure { ConstantClosure { env: NzEnv, body: TyExpr }, } +/// 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>); + #[derive(Debug, Clone, PartialEq, Eq)] pub(crate) enum ValueKind { /// Closures @@ -101,9 +109,7 @@ pub(crate) enum ValueKind { 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>), + TextLit(TextLit), Equivalence(Value, Value), // Invariant: in whnf, this must not contain a value captured by one of the variants above. PartialExpr(ExprKind), @@ -492,11 +498,7 @@ impl ValueKind { x.normalize_mut(); } } - ValueKind::TextLit(elts) => { - for x in elts.iter_mut() { - x.map_mut(Value::normalize_mut); - } - } + ValueKind::TextLit(tlit) => tlit.normalize_mut(), ValueKind::Equivalence(x, y) => { x.normalize_mut(); y.normalize_mut(); @@ -594,6 +596,60 @@ impl Closure { } } +impl TextLit { + pub fn new( + elts: impl Iterator>, + ) -> 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 { + 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> { + 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_mut(&mut self) { + for x in self.0.iter_mut() { + x.map_mut(Value::normalize_mut); + } + } +} + /// Compare two values for equality modulo alpha/beta-equivalence. // TODO: use Rc comparison to shortcut on identical pointers impl std::cmp::PartialEq for Value { -- cgit v1.2.3 From 3c4895a06a4910184203d8531e7ab318db71fb15 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 19:13:37 +0000 Subject: Prepare ValueInternal with new `Form`s --- dhall/src/semantics/nze/value.rs | 103 +++++++++++++++++++-------------------- 1 file changed, 50 insertions(+), 53 deletions(-) (limited to 'dhall/src/semantics/nze/value.rs') diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index 06d8df8..31acb11 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -30,23 +30,22 @@ pub(crate) struct Value(Rc>); #[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)] +#[derive(Debug, Clone)] pub(crate) enum Form { /// No constraints; expression may not be normalized at all. - Unevaled, + Unevaled(ValueKind), /// 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, + WHNF(ValueKind), } /// An unevaluated subexpression @@ -118,10 +117,9 @@ pub(crate) enum ValueKind { } impl Value { - fn new(kind: ValueKind, form: Form, ty: Value, span: Span) -> Value { + fn new(form: Form, ty: Value, span: Span) -> Value { ValueInternal { form, - kind, ty: Some(ty), span, } @@ -129,8 +127,7 @@ impl Value { } pub(crate) fn const_sort() -> Value { ValueInternal { - form: WHNF, - kind: ValueKind::Const(Const::Sort), + form: WHNF(ValueKind::Const(Const::Sort)), ty: None, span: Span::Artificial, } @@ -138,18 +135,17 @@ impl Value { } pub(crate) fn new_thunk(env: &NzEnv, tye: TyExpr) -> Value { ValueInternal { - form: Unevaled, - kind: ValueKind::Thunk(Thunk::new(env, tye.clone())), + form: Unevaled(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) + Value::new(Unevaled(v), t, Span::Artificial) } pub(crate) fn from_kind_and_type_whnf(v: ValueKind, t: Value) -> Value { - Value::new(v, WHNF, t, Span::Artificial) + Value::new(WHNF(v), t, Span::Artificial) } pub(crate) fn from_const(c: Const) -> Self { let v = ValueKind::Const(c); @@ -194,7 +190,10 @@ impl Value { /// panics. pub(crate) fn kind(&self) -> Ref { self.normalize_whnf(); - Ref::map(self.as_internal(), ValueInternal::as_kind) + Ref::map(self.as_internal(), |vint| match &vint.form { + Unevaled(..) => unreachable!(), + WHNF(k) => k, + }) } /// Converts a value back to the corresponding AST expression. @@ -232,12 +231,12 @@ impl Value { pub(crate) fn normalize_whnf(&self) { let borrow = self.as_internal(); match borrow.form { - Unevaled => { + Unevaled(_) => { drop(borrow); self.as_internal_mut().normalize_whnf(); } // Already in WHNF - WHNF => {} + WHNF(_) => {} } } pub(crate) fn normalize_nf(&self) { @@ -400,41 +399,29 @@ 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, - }, + use std::mem::replace; + let dummy = Unevaled(ValueKind::Const(Const::Type)); + self.form = match replace(&mut self.form, dummy) { + Unevaled(kind) => { + WHNF(match &self.ty { + Some(ty) => normalize_whnf(kind, &ty), + // `value` is `Sort` + None => ValueKind::Const(Const::Sort), + }) + } // Already in WHNF - (WHNF, _) => vint, - } + form @ WHNF(_) => form, + }; } fn normalize_nf(&mut self) { - if let Unevaled = self.form { + if let Unevaled(_) = self.form { self.normalize_whnf(); } - self.kind.normalize_mut(); + match &mut self.form { + Unevaled(k) | WHNF(k) => k.normalize_mut(), + } } fn get_type(&self) -> Result<&Value, TypeError> { @@ -679,17 +666,27 @@ 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::<()>); + let mut x = match &vint.form { + WHNF(kind) => { + if let ValueKind::Const(c) = kind { + return write!(fmt, "{:?}", c); + } else { + let mut x = fmt.debug_struct(&format!("Value@WHNF")); + x.field("kind", kind); + x + } } - x.finish() + Unevaled(kind) => { + let mut x = fmt.debug_struct(&format!("Value@Unevaled")); + x.field("kind", kind); + x + } + }; + if let Some(ty) = vint.ty.as_ref() { + x.field("type", &ty); + } else { + x.field("type", &None::<()>); } + x.finish() } } -- cgit v1.2.3 From 40336a928dfc3d1f96273d39ba564334b1719344 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 19:27:33 +0000 Subject: Move Thunk value into ValueInternal --- dhall/src/semantics/nze/value.rs | 66 +++++++++++++++++++--------------------- 1 file changed, 32 insertions(+), 34 deletions(-) (limited to 'dhall/src/semantics/nze/value.rs') diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index 31acb11..8ae0939 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -15,8 +15,6 @@ use crate::syntax::{ }; use crate::{Normalized, NormalizedExpr, ToExprOptions}; -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. @@ -37,6 +35,7 @@ struct ValueInternal { #[derive(Debug, Clone)] pub(crate) enum Form { + Thunk(Thunk), /// No constraints; expression may not be normalized at all. Unevaled(ValueKind), /// Weak Head Normal Form, i.e. normalized up to the first constructor, but subexpressions may @@ -112,8 +111,6 @@ pub(crate) enum ValueKind { 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 { @@ -127,7 +124,7 @@ impl Value { } pub(crate) fn const_sort() -> Value { ValueInternal { - form: WHNF(ValueKind::Const(Const::Sort)), + form: Form::WHNF(ValueKind::Const(Const::Sort)), ty: None, span: Span::Artificial, } @@ -135,17 +132,17 @@ impl Value { } pub(crate) fn new_thunk(env: &NzEnv, tye: TyExpr) -> Value { ValueInternal { - form: Unevaled(ValueKind::Thunk(Thunk::new(env, tye.clone()))), + form: Form::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(Unevaled(v), t, Span::Artificial) + Value::new(Form::Unevaled(v), t, Span::Artificial) } pub(crate) fn from_kind_and_type_whnf(v: ValueKind, t: Value) -> Value { - Value::new(WHNF(v), t, Span::Artificial) + Value::new(Form::WHNF(v), t, Span::Artificial) } pub(crate) fn from_const(c: Const) -> Self { let v = ValueKind::Const(c); @@ -191,8 +188,8 @@ impl Value { pub(crate) fn kind(&self) -> Ref { self.normalize_whnf(); Ref::map(self.as_internal(), |vint| match &vint.form { - Unevaled(..) => unreachable!(), - WHNF(k) => k, + Form::Thunk(..) | Form::Unevaled(..) => unreachable!(), + Form::WHNF(k) => k, }) } @@ -231,12 +228,12 @@ impl Value { pub(crate) fn normalize_whnf(&self) { let borrow = self.as_internal(); match borrow.form { - Unevaled(_) => { + Form::Thunk(..) | Form::Unevaled(_) => { drop(borrow); self.as_internal_mut().normalize_whnf(); } // Already in WHNF - WHNF(_) => {} + Form::WHNF(_) => {} } } pub(crate) fn normalize_nf(&self) { @@ -290,11 +287,10 @@ impl Value { let tye = match &*self.kind() { ValueKind::Var(v) => TyExprKind::Var(venv.lookup(v)), ValueKind::AppliedBuiltin(closure) => closure.to_tyexprkind(venv), - ValueKind::Thunk(th) => return th.to_tyexpr(venv), self_kind => TyExprKind::Expr(match self_kind { - ValueKind::Var(..) - | ValueKind::AppliedBuiltin(..) - | ValueKind::Thunk(..) => unreachable!(), + ValueKind::Var(..) | ValueKind::AppliedBuiltin(..) => { + unreachable!() + } ValueKind::LamClosure { binder, annot, @@ -402,25 +398,27 @@ impl ValueInternal { fn normalize_whnf(&mut self) { use std::mem::replace; - let dummy = Unevaled(ValueKind::Const(Const::Type)); + let dummy = Form::Unevaled(ValueKind::Const(Const::Type)); self.form = match replace(&mut self.form, dummy) { - Unevaled(kind) => { - WHNF(match &self.ty { + Form::Thunk(th) => Form::WHNF(th.eval().kind().clone()), + Form::Unevaled(kind) => { + Form::WHNF(match &self.ty { Some(ty) => normalize_whnf(kind, &ty), // `value` is `Sort` None => ValueKind::Const(Const::Sort), }) } // Already in WHNF - form @ WHNF(_) => form, + form @ Form::WHNF(_) => form, }; } fn normalize_nf(&mut self) { - if let Unevaled(_) = self.form { + if let Form::Thunk(..) | Form::Unevaled(_) = self.form { self.normalize_whnf(); } match &mut self.form { - Unevaled(k) | WHNF(k) => k.normalize_mut(), + Form::Thunk(..) | Form::Unevaled(_) => unreachable!(), + Form::WHNF(k) => k.normalize_mut(), } } @@ -493,9 +491,6 @@ impl ValueKind { ValueKind::PartialExpr(e) => { e.map_mut(Value::normalize_mut); } - ValueKind::Thunk(..) => { - unreachable!("Should only normalize_mut values in WHNF") - } } } @@ -515,12 +510,10 @@ impl Thunk { } } + // TODO: maybe return a ValueKind ? 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 { @@ -667,7 +660,17 @@ impl std::fmt::Debug for Value { fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { let vint: &ValueInternal = &self.as_internal(); let mut x = match &vint.form { - WHNF(kind) => { + Form::Thunk(th) => { + let mut x = fmt.debug_struct(&format!("Value@Thunk")); + x.field("thunk", th); + x + } + Form::Unevaled(kind) => { + let mut x = fmt.debug_struct(&format!("Value@Unevaled")); + x.field("kind", kind); + x + } + Form::WHNF(kind) => { if let ValueKind::Const(c) = kind { return write!(fmt, "{:?}", c); } else { @@ -676,11 +679,6 @@ impl std::fmt::Debug for Value { x } } - Unevaled(kind) => { - let mut x = fmt.debug_struct(&format!("Value@Unevaled")); - x.field("kind", kind); - x - } }; if let Some(ty) = vint.ty.as_ref() { x.field("type", &ty); -- cgit v1.2.3 From 673a580e11d31356bec25d73213b283685fd6ea3 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 19:49:03 +0000 Subject: Clarify normalization to ensure we only nze once --- dhall/src/semantics/nze/value.rs | 79 ++++++++++++++++++++++------------------ 1 file changed, 44 insertions(+), 35 deletions(-) (limited to 'dhall/src/semantics/nze/value.rs') diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index 8ae0939..108dc9c 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -5,7 +5,7 @@ use std::rc::Rc; use crate::error::{TypeError, TypeMessage}; use crate::semantics::Binder; use crate::semantics::{ - apply_any, normalize_tyexpr_whnf, normalize_whnf, squash_textlit, + 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}; @@ -16,34 +16,30 @@ use crate::syntax::{ use crate::{Normalized, NormalizedExpr, ToExprOptions}; /// 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 +/// automatically. Uses a Rc 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>); -/// Invariant: if `form` is `WHNF`, `value` must be in Weak Head Normal Form #[derive(Debug)] struct ValueInternal { form: Form, - /// This is None if and only if `value` is `Sort` (which doesn't have a type) + /// This is None if and only if `form` is `Sort` (which doesn't have a type) ty: Option, span: Span, } +/// A potentially un-evaluated expression. Once we get to WHNF we won't modify the form again, as +/// explained in the doc for `ValueKind`. #[derive(Debug, Clone)] pub(crate) enum Form { + /// A totally unnormalized value. Thunk(Thunk), - /// No constraints; expression may not be normalized at all. - Unevaled(ValueKind), - /// 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. + /// A partially normalized value that may need to go through `normalize_one_layer`. + PartialExpr(ExprKind), + /// A value in WHNF. WHNF(ValueKind), } @@ -73,6 +69,13 @@ pub(crate) enum Closure { #[derive(Debug, Clone, PartialEq, Eq)] pub(crate) struct TextLit(Vec>); +/// 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 @@ -86,7 +89,6 @@ pub(crate) enum ValueKind { annot: Value, closure: Closure, }, - // Invariant: in whnf, the evaluation must not be able to progress further. AppliedBuiltin(BuiltinClosure), Var(NzVar), @@ -109,7 +111,7 @@ pub(crate) enum ValueKind { UnionLit(Label, Value, HashMap>, Value, Value), TextLit(TextLit), Equivalence(Value, Value), - // Invariant: in whnf, this must not contain a value captured by one of the variants above. + /// Invariant: evaluation must not be able to progress with `normalize_one_layer`? PartialExpr(ExprKind), } @@ -130,6 +132,7 @@ impl Value { } .into_value() } + /// Construct a Value from a completely unnormalized expression. pub(crate) fn new_thunk(env: &NzEnv, tye: TyExpr) -> Value { ValueInternal { form: Form::Thunk(Thunk::new(env, tye.clone())), @@ -138,10 +141,15 @@ impl Value { } .into_value() } - pub(crate) fn from_kind_and_type(v: ValueKind, t: Value) -> Value { - Value::new(Form::Unevaled(v), t, Span::Artificial) + /// Construct a Value from a partially normalized expression that's not in WHNF. + pub(crate) fn from_partial_expr( + e: ExprKind, + t: Value, + ) -> Value { + Value::new(Form::PartialExpr(e), t, Span::Artificial) } - pub(crate) fn from_kind_and_type_whnf(v: ValueKind, t: Value) -> Value { + /// Make a Value from a ValueKind + pub(crate) fn from_kind_and_type(v: ValueKind, t: Value) -> Value { Value::new(Form::WHNF(v), t, Span::Artificial) } pub(crate) fn from_const(c: Const) -> Self { @@ -188,7 +196,7 @@ impl Value { pub(crate) fn kind(&self) -> Ref { self.normalize_whnf(); Ref::map(self.as_internal(), |vint| match &vint.form { - Form::Thunk(..) | Form::Unevaled(..) => unreachable!(), + Form::Thunk(..) | Form::PartialExpr(..) => unreachable!(), Form::WHNF(k) => k, }) } @@ -228,7 +236,7 @@ impl Value { pub(crate) fn normalize_whnf(&self) { let borrow = self.as_internal(); match borrow.form { - Form::Thunk(..) | Form::Unevaled(_) => { + Form::Thunk(..) | Form::PartialExpr(_) => { drop(borrow); self.as_internal_mut().normalize_whnf(); } @@ -248,10 +256,7 @@ impl Value { } _ => unreachable!("Internal type error"), }; - Value::from_kind_and_type_whnf( - apply_any(self.clone(), v, &body_t), - body_t, - ) + 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. @@ -398,12 +403,13 @@ impl ValueInternal { fn normalize_whnf(&mut self) { use std::mem::replace; - let dummy = Form::Unevaled(ValueKind::Const(Const::Type)); + let dummy = Form::PartialExpr(ExprKind::Const(Const::Type)); self.form = match replace(&mut self.form, dummy) { Form::Thunk(th) => Form::WHNF(th.eval().kind().clone()), - Form::Unevaled(kind) => { + Form::PartialExpr(e) => { Form::WHNF(match &self.ty { - Some(ty) => normalize_whnf(kind, &ty), + // TODO: env + Some(ty) => normalize_one_layer(e, &ty, &NzEnv::new()), // `value` is `Sort` None => ValueKind::Const(Const::Sort), }) @@ -413,11 +419,11 @@ impl ValueInternal { }; } fn normalize_nf(&mut self) { - if let Form::Thunk(..) | Form::Unevaled(_) = self.form { + if let Form::Thunk(..) | Form::PartialExpr(_) = self.form { self.normalize_whnf(); } match &mut self.form { - Form::Thunk(..) | Form::Unevaled(_) => unreachable!(), + Form::Thunk(..) | Form::PartialExpr(_) => unreachable!(), Form::WHNF(k) => k.normalize_mut(), } } @@ -451,9 +457,10 @@ impl ValueKind { ValueKind::NEOptionalLit(th) => { th.normalize_mut(); } - ValueKind::LamClosure { annot, .. } - | ValueKind::PiClosure { annot, .. } => { + ValueKind::LamClosure { annot, closure, .. } + | ValueKind::PiClosure { annot, closure, .. } => { annot.normalize_mut(); + closure.normalize_mut(); } ValueKind::AppliedBuiltin(closure) => closure.normalize_mut(), ValueKind::NEListLit(elts) => { @@ -553,6 +560,8 @@ impl Closure { } } + // TODO: somehow normalize the body. Might require to pass an env. + pub fn normalize_mut(&mut self) {} /// Convert this closure to a TyExpr pub fn to_tyexpr(&self, venv: VarEnv) -> TyExpr { self.apply_var(NzVar::new(venv.size())) @@ -665,9 +674,9 @@ impl std::fmt::Debug for Value { x.field("thunk", th); x } - Form::Unevaled(kind) => { - let mut x = fmt.debug_struct(&format!("Value@Unevaled")); - x.field("kind", kind); + Form::PartialExpr(e) => { + let mut x = fmt.debug_struct(&format!("Value@PartialExpr")); + x.field("expr", e); x } Form::WHNF(kind) => { -- cgit v1.2.3 From d8de45763037937b5c2dedbe5f7bb95a4e7bc7cd Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 19:56:31 +0000 Subject: Avoid unnecessary allocations of `Value`s --- dhall/src/semantics/nze/value.rs | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) (limited to 'dhall/src/semantics/nze/value.rs') diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index 108dc9c..ff0ca42 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -405,7 +405,7 @@ impl ValueInternal { use std::mem::replace; let dummy = Form::PartialExpr(ExprKind::Const(Const::Type)); self.form = match replace(&mut self.form, dummy) { - Form::Thunk(th) => Form::WHNF(th.eval().kind().clone()), + Form::Thunk(th) => Form::WHNF(th.eval()), Form::PartialExpr(e) => { Form::WHNF(match &self.ty { // TODO: env @@ -516,9 +516,7 @@ impl Thunk { body, } } - - // TODO: maybe return a ValueKind ? - pub fn eval(&self) -> Value { + pub fn eval(&self) -> ValueKind { normalize_tyexpr_whnf(&self.body, &self.env) } } -- cgit v1.2.3 From b79a9b81a803794a7a86d953ced24f0d3e2fd212 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 20:23:06 +0000 Subject: Only the Form must be in a RefCell --- dhall/src/semantics/nze/value.rs | 128 ++++++++++++++++++++------------------- 1 file changed, 67 insertions(+), 61 deletions(-) (limited to 'dhall/src/semantics/nze/value.rs') diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index ff0ca42..d737a0f 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -1,4 +1,4 @@ -use std::cell::{Ref, RefCell, RefMut}; +use std::cell::{Ref, RefCell}; use std::collections::HashMap; use std::rc::Rc; @@ -21,11 +21,11 @@ use crate::{Normalized, NormalizedExpr, ToExprOptions}; /// (renaming of bound variables) and beta-equivalence (normalization). It will recursively /// normalize as needed. #[derive(Clone)] -pub(crate) struct Value(Rc>); +pub(crate) struct Value(Rc); #[derive(Debug)] struct ValueInternal { - form: Form, + form: RefCell
, /// This is None if and only if `form` is `Sort` (which doesn't have a type) ty: Option, span: Span, @@ -117,28 +117,23 @@ pub(crate) enum ValueKind { impl Value { fn new(form: Form, ty: Value, span: Span) -> Value { - ValueInternal { - form, - ty: Some(ty), - span, - } - .into_value() + ValueInternal::new(form, Some(ty), span).into_value() } pub(crate) fn const_sort() -> Value { - ValueInternal { - form: Form::WHNF(ValueKind::Const(Const::Sort)), - ty: None, - span: Span::Artificial, - } + ValueInternal::new( + Form::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 { - form: Form::Thunk(Thunk::new(env, tye.clone())), - ty: tye.get_type().ok(), - span: tye.span().clone(), - } + ValueInternal::new( + Form::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. @@ -181,21 +176,18 @@ impl Value { } } pub(crate) fn span(&self) -> Span { - self.as_internal().span.clone() + self.0.span.clone() } - fn as_internal(&self) -> Ref { - self.0.borrow() - } - fn as_internal_mut(&self) -> RefMut { - self.0.borrow_mut() + fn as_form(&self) -> Ref { + self.0.form.borrow() } /// 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(), |vint| match &vint.form { + Ref::map(self.as_form(), |form| match form { Form::Thunk(..) | Form::PartialExpr(..) => unreachable!(), Form::WHNF(k) => k, }) @@ -219,33 +211,25 @@ impl Value { } /// Mutates the contents. If no one else shares this, this avoids a RefCell lock. - fn mutate_internal(&mut self, f: impl FnOnce(&mut ValueInternal)) { + fn mutate_form(&mut self, f: impl FnOnce(&mut Form, &Option)) { match Rc::get_mut(&mut self.0) { // Mutate directly if sole owner - Some(refcell) => f(RefCell::get_mut(refcell)), + Some(vint) => f(RefCell::get_mut(&mut vint.form), &vint.ty), // Otherwise mutate through the refcell - None => f(&mut self.as_internal_mut()), + None => f(&mut self.0.form.borrow_mut(), &self.0.ty), } } /// 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()) + self.mutate_form(|form, ty| form.normalize_nf(ty)) } pub(crate) fn normalize_whnf(&self) { - let borrow = self.as_internal(); - match borrow.form { - Form::Thunk(..) | Form::PartialExpr(_) => { - drop(borrow); - self.as_internal_mut().normalize_whnf(); - } - // Already in WHNF - Form::WHNF(_) => {} - } + self.0.normalize_whnf() } pub(crate) fn normalize_nf(&self) { - self.as_internal_mut().normalize_nf(); + self.0.normalize_nf() } pub(crate) fn app(&self, v: Value) -> Value { @@ -270,7 +254,7 @@ impl Value { // ); } pub(crate) fn get_type(&self) -> Result { - Ok(self.as_internal().get_type()?.clone()) + 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 { @@ -387,9 +371,7 @@ impl Value { }), }; - let self_ty = self.as_internal().ty.clone(); - let self_span = self.as_internal().span.clone(); - TyExpr::new(tye, self_ty, self_span) + TyExpr::new(tye, self.0.ty.clone(), self.0.span.clone()) } pub fn to_tyexpr_noenv(&self) -> TyExpr { self.to_tyexpr(VarEnv::new()) @@ -397,17 +379,48 @@ impl Value { } impl ValueInternal { + fn new(form: Form, ty: Option, span: Span) -> Self { + ValueInternal { + form: RefCell::new(form), + ty, + span, + } + } fn into_value(self) -> Value { - Value(Rc::new(RefCell::new(self))) + Value(Rc::new(self)) } - fn normalize_whnf(&mut self) { + fn normalize_whnf(&self) { + if !self.form.borrow().is_whnf() { + self.form.borrow_mut().normalize_whnf(&self.ty) + } + } + fn normalize_nf(&self) { + self.form.borrow_mut().normalize_nf(&self.ty) + } + + fn get_type(&self) -> Result<&Value, TypeError> { + match &self.ty { + Some(t) => Ok(t), + None => Err(TypeError::new(TypeMessage::Sort)), + } + } +} + +impl Form { + fn is_whnf(&self) -> bool { + match self { + Form::Thunk(..) | Form::PartialExpr(..) => false, + Form::WHNF(..) => true, + } + } + fn normalize_whnf(&mut self, ty: &Option) { use std::mem::replace; let dummy = Form::PartialExpr(ExprKind::Const(Const::Type)); - self.form = match replace(&mut self.form, dummy) { + *self = match replace(self, dummy) { Form::Thunk(th) => Form::WHNF(th.eval()), Form::PartialExpr(e) => { - Form::WHNF(match &self.ty { + Form::WHNF(match ty { // TODO: env Some(ty) => normalize_one_layer(e, &ty, &NzEnv::new()), // `value` is `Sort` @@ -418,22 +431,15 @@ impl ValueInternal { form @ Form::WHNF(_) => form, }; } - fn normalize_nf(&mut self) { - if let Form::Thunk(..) | Form::PartialExpr(_) = self.form { - self.normalize_whnf(); + fn normalize_nf(&mut self, ty: &Option) { + if !self.is_whnf() { + self.normalize_whnf(ty); } - match &mut self.form { + match self { Form::Thunk(..) | Form::PartialExpr(_) => unreachable!(), Form::WHNF(k) => k.normalize_mut(), } } - - fn get_type(&self) -> Result<&Value, TypeError> { - match &self.ty { - Some(t) => Ok(t), - None => Err(TypeError::new(TypeMessage::Sort)), - } - } } impl ValueKind { @@ -665,8 +671,8 @@ 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(); - let mut x = match &vint.form { + let vint: &ValueInternal = &self.0; + let mut x = match &*vint.form.borrow() { Form::Thunk(th) => { let mut x = fmt.debug_struct(&format!("Value@Thunk")); x.field("thunk", th); -- cgit v1.2.3 From a87b22da10aa20cef939d3c3c7b56710a1f78c2c Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 20:36:10 +0000 Subject: Move Form::PartialExpr into Thunk --- dhall/src/semantics/nze/value.rs | 82 ++++++++++++++++++++++------------------ 1 file changed, 46 insertions(+), 36 deletions(-) (limited to 'dhall/src/semantics/nze/value.rs') diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index d737a0f..87ebfcd 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -35,19 +35,23 @@ struct ValueInternal { /// explained in the doc for `ValueKind`. #[derive(Debug, Clone)] pub(crate) enum Form { - /// A totally unnormalized value. + /// An unevaluated value. Thunk(Thunk), - /// A partially normalized value that may need to go through `normalize_one_layer`. - PartialExpr(ExprKind), /// A value in WHNF. WHNF(ValueKind), } /// An unevaluated subexpression #[derive(Debug, Clone)] -pub(crate) struct Thunk { - env: NzEnv, - body: TyExpr, +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, + ty: Value, + }, } /// An unevaluated subexpression that takes an argument. @@ -139,9 +143,15 @@ impl Value { /// Construct a Value from a partially normalized expression that's not in WHNF. pub(crate) fn from_partial_expr( e: ExprKind, - t: Value, + ty: Value, ) -> Value { - Value::new(Form::PartialExpr(e), t, Span::Artificial) + // TODO: env + let env = NzEnv::new(); + Value::new( + Form::Thunk(Thunk::from_partial_expr(env, e, ty.clone())), + ty, + Span::Artificial, + ) } /// Make a Value from a ValueKind pub(crate) fn from_kind_and_type(v: ValueKind, t: Value) -> Value { @@ -188,7 +198,7 @@ impl Value { pub(crate) fn kind(&self) -> Ref { self.normalize_whnf(); Ref::map(self.as_form(), |form| match form { - Form::Thunk(..) | Form::PartialExpr(..) => unreachable!(), + Form::Thunk(..) => unreachable!(), Form::WHNF(k) => k, }) } @@ -211,18 +221,18 @@ impl Value { } /// Mutates the contents. If no one else shares this, this avoids a RefCell lock. - fn mutate_form(&mut self, f: impl FnOnce(&mut Form, &Option)) { + fn mutate_form(&mut self, f: impl FnOnce(&mut Form)) { match Rc::get_mut(&mut self.0) { // Mutate directly if sole owner - Some(vint) => f(RefCell::get_mut(&mut vint.form), &vint.ty), + Some(vint) => f(RefCell::get_mut(&mut vint.form)), // Otherwise mutate through the refcell - None => f(&mut self.0.form.borrow_mut(), &self.0.ty), + None => f(&mut self.0.form.borrow_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_form(|form, ty| form.normalize_nf(ty)) + self.mutate_form(|form| form.normalize_nf()) } pub(crate) fn normalize_whnf(&self) { @@ -392,11 +402,11 @@ impl ValueInternal { fn normalize_whnf(&self) { if !self.form.borrow().is_whnf() { - self.form.borrow_mut().normalize_whnf(&self.ty) + self.form.borrow_mut().normalize_whnf() } } fn normalize_nf(&self) { - self.form.borrow_mut().normalize_nf(&self.ty) + self.form.borrow_mut().normalize_nf() } fn get_type(&self) -> Result<&Value, TypeError> { @@ -410,33 +420,25 @@ impl ValueInternal { impl Form { fn is_whnf(&self) -> bool { match self { - Form::Thunk(..) | Form::PartialExpr(..) => false, + Form::Thunk(..) => false, Form::WHNF(..) => true, } } - fn normalize_whnf(&mut self, ty: &Option) { + fn normalize_whnf(&mut self) { use std::mem::replace; - let dummy = Form::PartialExpr(ExprKind::Const(Const::Type)); + let dummy = Form::WHNF(ValueKind::Const(Const::Type)); *self = match replace(self, dummy) { Form::Thunk(th) => Form::WHNF(th.eval()), - Form::PartialExpr(e) => { - Form::WHNF(match ty { - // TODO: env - Some(ty) => normalize_one_layer(e, &ty, &NzEnv::new()), - // `value` is `Sort` - None => ValueKind::Const(Const::Sort), - }) - } // Already in WHNF form @ Form::WHNF(_) => form, }; } - fn normalize_nf(&mut self, ty: &Option) { + fn normalize_nf(&mut self) { if !self.is_whnf() { - self.normalize_whnf(ty); + self.normalize_whnf(); } match self { - Form::Thunk(..) | Form::PartialExpr(_) => unreachable!(), + Form::Thunk(..) => unreachable!(), Form::WHNF(k) => k.normalize_mut(), } } @@ -517,13 +519,26 @@ impl ValueKind { impl Thunk { pub fn new(env: &NzEnv, body: TyExpr) -> Self { - Thunk { + Thunk::Thunk { env: env.clone(), body, } } + pub fn from_partial_expr( + env: NzEnv, + expr: ExprKind, + ty: Value, + ) -> Self { + Thunk::PartialExpr { env, expr, ty } + } + // TODO: take by value pub fn eval(&self) -> ValueKind { - normalize_tyexpr_whnf(&self.body, &self.env) + match self { + Thunk::Thunk { env, body } => normalize_tyexpr_whnf(body, env), + Thunk::PartialExpr { env, expr, ty } => { + normalize_one_layer(expr.clone(), ty, env) + } + } } } @@ -678,11 +693,6 @@ impl std::fmt::Debug for Value { x.field("thunk", th); x } - Form::PartialExpr(e) => { - let mut x = fmt.debug_struct(&format!("Value@PartialExpr")); - x.field("expr", e); - x - } Form::WHNF(kind) => { if let ValueKind::Const(c) = kind { return write!(fmt, "{:?}", c); -- cgit v1.2.3 From 884774dbf13fd0a0fb6936c4259527a30a285ff0 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 21:06:12 +0000 Subject: Replace Form with a pair of RefCells, in preparation for OnceCell --- dhall/src/semantics/nze/value.rs | 159 +++++++++++++++++---------------------- 1 file changed, 71 insertions(+), 88 deletions(-) (limited to 'dhall/src/semantics/nze/value.rs') diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index 87ebfcd..d25e8b5 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -25,22 +25,15 @@ pub(crate) struct Value(Rc); #[derive(Debug)] struct ValueInternal { - form: RefCell, + /// Exactly one of `thunk` of `kind` must be set at a given time. + /// Once `thunk` is unset and `kind` is set, we never go back. + thunk: RefCell>, + kind: RefCell>, /// This is None if and only if `form` is `Sort` (which doesn't have a type) ty: Option, span: Span, } -/// A potentially un-evaluated expression. Once we get to WHNF we won't modify the form again, as -/// explained in the doc for `ValueKind`. -#[derive(Debug, Clone)] -pub(crate) enum Form { - /// An unevaluated value. - Thunk(Thunk), - /// A value in WHNF. - WHNF(ValueKind), -} - /// An unevaluated subexpression #[derive(Debug, Clone)] pub(crate) enum Thunk { @@ -120,12 +113,9 @@ pub(crate) enum ValueKind { } impl Value { - fn new(form: Form, ty: Value, span: Span) -> Value { - ValueInternal::new(form, Some(ty), span).into_value() - } pub(crate) fn const_sort() -> Value { - ValueInternal::new( - Form::WHNF(ValueKind::Const(Const::Sort)), + ValueInternal::from_whnf( + ValueKind::Const(Const::Sort), None, Span::Artificial, ) @@ -133,8 +123,8 @@ impl Value { } /// Construct a Value from a completely unnormalized expression. pub(crate) fn new_thunk(env: &NzEnv, tye: TyExpr) -> Value { - ValueInternal::new( - Form::Thunk(Thunk::new(env, tye.clone())), + ValueInternal::from_thunk( + Thunk::new(env, tye.clone()), tye.get_type().ok(), tye.span().clone(), ) @@ -147,15 +137,16 @@ impl Value { ) -> Value { // TODO: env let env = NzEnv::new(); - Value::new( - Form::Thunk(Thunk::from_partial_expr(env, e, ty.clone())), - ty, + 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 { - Value::new(Form::WHNF(v), t, Span::Artificial) + ValueInternal::from_whnf(v, Some(t), Span::Artificial).into_value() } pub(crate) fn from_const(c: Const) -> Self { let v = ValueKind::Const(c); @@ -189,18 +180,11 @@ impl Value { self.0.span.clone() } - fn as_form(&self) -> Ref { - self.0.form.borrow() - } /// 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_form(), |form| match form { - Form::Thunk(..) => unreachable!(), - Form::WHNF(k) => k, - }) + self.0.kind() } /// Converts a value back to the corresponding AST expression. @@ -220,24 +204,16 @@ impl Value { self.to_whnf_ignore_type() } - /// Mutates the contents. If no one else shares this, this avoids a RefCell lock. - fn mutate_form(&mut self, f: impl FnOnce(&mut Form)) { + /// Normalizes contents to normal form; faster than `normalize_nf` 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) => f(RefCell::get_mut(&mut vint.form)), + Some(vint) => vint.normalize_nf_mut(), // Otherwise mutate through the refcell - None => f(&mut self.0.form.borrow_mut()), + None => self.0.normalize_nf(), } } - /// Normalizes contents to normal form; faster than `normalize_nf` if - /// no one else shares this. - pub(crate) fn normalize_mut(&mut self) { - self.mutate_form(|form| form.normalize_nf()) - } - - pub(crate) fn normalize_whnf(&self) { - self.0.normalize_whnf() - } pub(crate) fn normalize_nf(&self) { self.0.normalize_nf() } @@ -389,9 +365,18 @@ impl Value { } impl ValueInternal { - fn new(form: Form, ty: Option, span: Span) -> Self { + fn from_whnf(k: ValueKind, ty: Option, span: Span) -> Self { ValueInternal { - form: RefCell::new(form), + thunk: RefCell::new(None), + kind: RefCell::new(Some(k)), + ty, + span, + } + } + fn from_thunk(th: Thunk, ty: Option, span: Span) -> Self { + ValueInternal { + kind: RefCell::new(None), + thunk: RefCell::new(Some(th)), ty, span, } @@ -400,13 +385,38 @@ impl ValueInternal { Value(Rc::new(self)) } + fn kind(&self) -> Ref { + self.normalize_whnf(); + Ref::map(self.kind.borrow(), |kind| kind.as_ref().unwrap()) + } fn normalize_whnf(&self) { - if !self.form.borrow().is_whnf() { - self.form.borrow_mut().normalize_whnf() + if self.kind.borrow().is_none() { + let mut thunk_borrow = self.thunk.borrow_mut(); + let kind = thunk_borrow.as_ref().unwrap().eval(); + *thunk_borrow = None; + *self.kind.borrow_mut() = Some(kind); } } fn normalize_nf(&self) { - self.form.borrow_mut().normalize_nf() + self.normalize_whnf(); + self.kind.borrow_mut().as_mut().unwrap().normalize_mut() + } + // Avoids a RefCell lock + fn normalize_whnf_mut(&mut self) { + let self_thunk = RefCell::get_mut(&mut self.thunk); + if let Some(thunk) = &mut *self_thunk { + let self_kind = RefCell::get_mut(&mut self.kind); + let mut kind = thunk.eval(); + kind.normalize_mut(); + *self_kind = Some(kind); + *self_thunk = None; + } + } + // Avoids a RefCell lock + fn normalize_nf_mut(&mut self) { + self.normalize_whnf_mut(); + let self_kind = RefCell::get_mut(&mut self.kind); + self_kind.as_mut().unwrap().normalize_mut(); } fn get_type(&self) -> Result<&Value, TypeError> { @@ -417,33 +427,6 @@ impl ValueInternal { } } -impl Form { - fn is_whnf(&self) -> bool { - match self { - Form::Thunk(..) => false, - Form::WHNF(..) => true, - } - } - fn normalize_whnf(&mut self) { - use std::mem::replace; - let dummy = Form::WHNF(ValueKind::Const(Const::Type)); - *self = match replace(self, dummy) { - Form::Thunk(th) => Form::WHNF(th.eval()), - // Already in WHNF - form @ Form::WHNF(_) => form, - }; - } - fn normalize_nf(&mut self) { - if !self.is_whnf() { - self.normalize_whnf(); - } - match self { - Form::Thunk(..) => unreachable!(), - Form::WHNF(k) => k.normalize_mut(), - } - } -} - impl ValueKind { pub(crate) fn into_value_with_type(self, t: Value) -> Value { Value::from_kind_and_type(self, t) @@ -687,21 +670,21 @@ 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 mut x = match &*vint.form.borrow() { - Form::Thunk(th) => { - let mut x = fmt.debug_struct(&format!("Value@Thunk")); - x.field("thunk", th); + let kind_borrow = vint.kind.borrow(); + let mut x = if let Some(kind) = kind_borrow.as_ref() { + if let ValueKind::Const(c) = kind { + return write!(fmt, "{:?}", c); + } else { + let mut x = fmt.debug_struct(&format!("Value@WHNF")); + x.field("kind", kind); x } - Form::WHNF(kind) => { - if let ValueKind::Const(c) = kind { - return write!(fmt, "{:?}", c); - } else { - let mut x = fmt.debug_struct(&format!("Value@WHNF")); - x.field("kind", kind); - x - } - } + } else { + let thunk_borrow = vint.thunk.borrow(); + let th = thunk_borrow.as_ref().unwrap(); + let mut x = fmt.debug_struct(&format!("Value@Thunk")); + x.field("thunk", th); + x }; if let Some(ty) = vint.ty.as_ref() { x.field("type", &ty); -- cgit v1.2.3 From 2700af36adfac4390b9395ac2ed0e534b7eac887 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 21:43:50 +0000 Subject: Use OnceCell to enable returning &ValKind --- dhall/src/semantics/nze/value.rs | 121 +++++++++++++++++---------------------- 1 file changed, 53 insertions(+), 68 deletions(-) (limited to 'dhall/src/semantics/nze/value.rs') diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index d25e8b5..945ee6e 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -1,4 +1,5 @@ -use std::cell::{Ref, RefCell}; +use once_cell::unsync::OnceCell; +use std::cell::RefCell; use std::collections::HashMap; use std::rc::Rc; @@ -28,7 +29,7 @@ struct ValueInternal { /// Exactly one of `thunk` of `kind` must be set at a given time. /// Once `thunk` is unset and `kind` is set, we never go back. thunk: RefCell>, - kind: RefCell>, + kind: OnceCell, /// This is None if and only if `form` is `Sort` (which doesn't have a type) ty: Option, span: Span, @@ -183,14 +184,14 @@ impl Value { /// 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 { + 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_nf(); + self.normalize(); } self.to_tyexpr_noenv().to_expr(opts) @@ -204,18 +205,18 @@ impl Value { self.to_whnf_ignore_type() } - /// Normalizes contents to normal form; faster than `normalize_nf` if + /// 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_nf_mut(), + Some(vint) => vint.normalize_mut(), // Otherwise mutate through the refcell - None => self.0.normalize_nf(), + None => self.normalize(), } } - pub(crate) fn normalize_nf(&self) { - self.0.normalize_nf() + pub(crate) fn normalize(&self) { + self.0.normalize() } pub(crate) fn app(&self, v: Value) -> Value { @@ -366,17 +367,19 @@ impl Value { impl ValueInternal { fn from_whnf(k: ValueKind, ty: Option, span: Span) -> Self { + let kind = OnceCell::new(); + kind.set(k).unwrap(); ValueInternal { thunk: RefCell::new(None), - kind: RefCell::new(Some(k)), + kind, ty, span, } } fn from_thunk(th: Thunk, ty: Option, span: Span) -> Self { ValueInternal { - kind: RefCell::new(None), thunk: RefCell::new(Some(th)), + kind: OnceCell::new(), ty, span, } @@ -385,38 +388,23 @@ impl ValueInternal { Value(Rc::new(self)) } - fn kind(&self) -> Ref { - self.normalize_whnf(); - Ref::map(self.kind.borrow(), |kind| kind.as_ref().unwrap()) - } - fn normalize_whnf(&self) { - if self.kind.borrow().is_none() { - let mut thunk_borrow = self.thunk.borrow_mut(); - let kind = thunk_borrow.as_ref().unwrap().eval(); - *thunk_borrow = None; - *self.kind.borrow_mut() = Some(kind); + fn kind(&self) -> &ValueKind { + if self.kind.get().is_none() { + let thunk = self.thunk.borrow_mut().take().unwrap(); + self.kind.set(thunk.eval()).unwrap(); } + self.kind.get().unwrap() } - fn normalize_nf(&self) { - self.normalize_whnf(); - self.kind.borrow_mut().as_mut().unwrap().normalize_mut() + fn normalize(&self) { + self.kind().normalize(); } // Avoids a RefCell lock - fn normalize_whnf_mut(&mut self) { - let self_thunk = RefCell::get_mut(&mut self.thunk); - if let Some(thunk) = &mut *self_thunk { - let self_kind = RefCell::get_mut(&mut self.kind); - let mut kind = thunk.eval(); - kind.normalize_mut(); - *self_kind = Some(kind); - *self_thunk = None; + fn normalize_mut(&mut self) { + if self.kind.get().is_none() { + let thunk = RefCell::get_mut(&mut self.thunk).take().unwrap(); + self.kind.set(thunk.eval()).unwrap(); } - } - // Avoids a RefCell lock - fn normalize_nf_mut(&mut self) { - self.normalize_whnf_mut(); - let self_kind = RefCell::get_mut(&mut self.kind); - self_kind.as_mut().unwrap().normalize_mut(); + self.normalize(); } fn get_type(&self) -> Result<&Value, TypeError> { @@ -432,7 +420,7 @@ impl ValueKind { Value::from_kind_and_type(self, t) } - pub(crate) fn normalize_mut(&mut self) { + pub(crate) fn normalize(&self) { match self { ValueKind::Var(..) | ValueKind::Const(_) @@ -442,52 +430,52 @@ impl ValueKind { | ValueKind::DoubleLit(_) => {} ValueKind::EmptyOptionalLit(tth) | ValueKind::EmptyListLit(tth) => { - tth.normalize_mut(); + tth.normalize(); } ValueKind::NEOptionalLit(th) => { - th.normalize_mut(); + th.normalize(); } ValueKind::LamClosure { annot, closure, .. } | ValueKind::PiClosure { annot, closure, .. } => { - annot.normalize_mut(); - closure.normalize_mut(); + annot.normalize(); + closure.normalize(); } - ValueKind::AppliedBuiltin(closure) => closure.normalize_mut(), + ValueKind::AppliedBuiltin(closure) => closure.normalize(), ValueKind::NEListLit(elts) => { - for x in elts.iter_mut() { - x.normalize_mut(); + for x in elts.iter() { + x.normalize(); } } ValueKind::RecordLit(kvs) => { - for x in kvs.values_mut() { - x.normalize_mut(); + for x in kvs.values() { + x.normalize(); } } ValueKind::RecordType(kvs) => { - for x in kvs.values_mut() { - x.normalize_mut(); + for x in kvs.values() { + x.normalize(); } } ValueKind::UnionType(kts) | ValueKind::UnionConstructor(_, kts, _) => { - for x in kts.values_mut().flat_map(|opt| opt) { - x.normalize_mut(); + for x in kts.values().flat_map(|opt| opt) { + x.normalize(); } } ValueKind::UnionLit(_, v, kts, _, _) => { - v.normalize_mut(); - for x in kts.values_mut().flat_map(|opt| opt) { - x.normalize_mut(); + v.normalize(); + for x in kts.values().flat_map(|opt| opt) { + x.normalize(); } } - ValueKind::TextLit(tlit) => tlit.normalize_mut(), + ValueKind::TextLit(tlit) => tlit.normalize(), ValueKind::Equivalence(x, y) => { - x.normalize_mut(); - y.normalize_mut(); + x.normalize(); + y.normalize(); } ValueKind::PartialExpr(e) => { - e.map_mut(Value::normalize_mut); + e.map_ref(Value::normalize); } } } @@ -563,7 +551,7 @@ impl Closure { } // TODO: somehow normalize the body. Might require to pass an env. - pub fn normalize_mut(&mut self) {} + 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())) @@ -634,9 +622,9 @@ impl TextLit { } /// 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_mut(&mut self) { - for x in self.0.iter_mut() { - x.map_mut(Value::normalize_mut); + pub fn normalize(&self) { + for x in self.0.iter() { + x.map_ref(Value::normalize); } } } @@ -670,8 +658,7 @@ 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_borrow = vint.kind.borrow(); - let mut x = if let Some(kind) = kind_borrow.as_ref() { + let mut x = if let Some(kind) = vint.kind.get() { if let ValueKind::Const(c) = kind { return write!(fmt, "{:?}", c); } else { @@ -680,10 +667,8 @@ impl std::fmt::Debug for Value { x } } else { - let thunk_borrow = vint.thunk.borrow(); - let th = thunk_borrow.as_ref().unwrap(); let mut x = fmt.debug_struct(&format!("Value@Thunk")); - x.field("thunk", th); + x.field("thunk", vint.thunk.borrow().as_ref().unwrap()); x }; if let Some(ty) = vint.ty.as_ref() { -- cgit v1.2.3 From 4e2bb03bcf6355d49216c6886bf03e5aeaad16cc Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 22:01:54 +0000 Subject: Eval Thunk by move --- dhall/src/semantics/nze/value.rs | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) (limited to 'dhall/src/semantics/nze/value.rs') diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index 945ee6e..724e3e8 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -502,12 +502,11 @@ impl Thunk { ) -> Self { Thunk::PartialExpr { env, expr, ty } } - // TODO: take by value - pub fn eval(&self) -> ValueKind { + pub fn eval(self) -> ValueKind { match self { - Thunk::Thunk { env, body } => normalize_tyexpr_whnf(body, env), + Thunk::Thunk { env, body } => normalize_tyexpr_whnf(&body, &env), Thunk::PartialExpr { env, expr, ty } => { - normalize_one_layer(expr.clone(), ty, env) + normalize_one_layer(expr, &ty, &env) } } } -- cgit v1.2.3 From 70af1a47bce9e6c8282d6e53cf82aeda9aab10de Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 22:08:57 +0000 Subject: Tweak ConstantClosure --- dhall/src/semantics/nze/value.rs | 20 +++++++------------- 1 file changed, 7 insertions(+), 13 deletions(-) (limited to 'dhall/src/semantics/nze/value.rs') diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index 724e3e8..67ab90a 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -58,7 +58,7 @@ pub(crate) enum Closure { body: TyExpr, }, /// Closure that ignores the argument passed - ConstantClosure { env: NzEnv, body: TyExpr }, + ConstantClosure { body: Value }, } /// A text literal with interpolations. @@ -521,11 +521,8 @@ impl Closure { } } /// New closure that ignores its argument - pub fn new_constant(env: &NzEnv, body: TyExpr) -> Self { - Closure::ConstantClosure { - env: env.clone(), - body, - } + pub fn new_constant(body: Value) -> Self { + Closure::ConstantClosure { body } } pub fn apply(&self, val: Value) -> Value { @@ -533,7 +530,7 @@ impl Closure { Closure::Closure { env, body, .. } => { body.eval(&env.insert_value(val)) } - Closure::ConstantClosure { env, body, .. } => body.eval(env), + Closure::ConstantClosure { body, .. } => body.clone(), } } fn apply_var(&self, var: NzVar) -> Value { @@ -545,7 +542,7 @@ impl Closure { ); self.apply(val) } - Closure::ConstantClosure { env, body, .. } => body.eval(env), + Closure::ConstantClosure { body, .. } => body.clone(), } } @@ -559,17 +556,14 @@ impl Closure { /// 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 { .. } => { + 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 { .. } => { - // Ok: the variable is indeed ignored - Ok(self.apply_var(v)) - } + Closure::ConstantClosure { body, .. } => Ok(body.clone()), } } } -- cgit v1.2.3 From 4312ad935d881f269fa7e9cc3d880fa763db957d Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 22:10:40 +0000 Subject: Use Rc equality to shortcut Value equality --- dhall/src/semantics/nze/value.rs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'dhall/src/semantics/nze/value.rs') diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index 67ab90a..de40d53 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -623,10 +623,9 @@ impl TextLit { } /// 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() + Rc::ptr_eq(&self.0, &other.0) || self.kind() == other.kind() } } impl std::cmp::Eq for Value {} -- cgit v1.2.3 From aa93f18c8ef9ad13c6bb4ddef90b419b3ed546f4 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 31 Jan 2020 19:46:16 +0000 Subject: Factor out custom Lazy struct --- dhall/src/semantics/nze/value.rs | 53 ++++++++++++++-------------------------- 1 file changed, 18 insertions(+), 35 deletions(-) (limited to 'dhall/src/semantics/nze/value.rs') diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index de40d53..ae06942 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -1,9 +1,8 @@ -use once_cell::unsync::OnceCell; -use std::cell::RefCell; 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, @@ -26,10 +25,7 @@ pub(crate) struct Value(Rc); #[derive(Debug)] struct ValueInternal { - /// Exactly one of `thunk` of `kind` must be set at a given time. - /// Once `thunk` is unset and `kind` is set, we never go back. - thunk: RefCell>, - kind: OnceCell, + kind: lazy::Lazy, /// This is None if and only if `form` is `Sort` (which doesn't have a type) ty: Option, span: Span, @@ -367,19 +363,15 @@ impl Value { impl ValueInternal { fn from_whnf(k: ValueKind, ty: Option, span: Span) -> Self { - let kind = OnceCell::new(); - kind.set(k).unwrap(); ValueInternal { - thunk: RefCell::new(None), - kind, + kind: lazy::Lazy::new_completed(k), ty, span, } } fn from_thunk(th: Thunk, ty: Option, span: Span) -> Self { ValueInternal { - thunk: RefCell::new(Some(th)), - kind: OnceCell::new(), + kind: lazy::Lazy::new(th), ty, span, } @@ -389,21 +381,13 @@ impl ValueInternal { } fn kind(&self) -> &ValueKind { - if self.kind.get().is_none() { - let thunk = self.thunk.borrow_mut().take().unwrap(); - self.kind.set(thunk.eval()).unwrap(); - } - self.kind.get().unwrap() + &self.kind } fn normalize(&self) { self.kind().normalize(); } - // Avoids a RefCell lock + // TODO: deprecated fn normalize_mut(&mut self) { - if self.kind.get().is_none() { - let thunk = RefCell::get_mut(&mut self.thunk).take().unwrap(); - self.kind.set(thunk.eval()).unwrap(); - } self.normalize(); } @@ -622,6 +606,12 @@ impl TextLit { } } +impl lazy::Eval 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 { @@ -650,19 +640,12 @@ 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 mut x = if let Some(kind) = vint.kind.get() { - if let ValueKind::Const(c) = kind { - return write!(fmt, "{:?}", c); - } else { - let mut x = fmt.debug_struct(&format!("Value@WHNF")); - x.field("kind", kind); - x - } - } else { - let mut x = fmt.debug_struct(&format!("Value@Thunk")); - x.field("thunk", vint.thunk.borrow().as_ref().unwrap()); - x - }; + 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 { -- cgit v1.2.3