diff options
| -rw-r--r-- | dhall/src/semantics/nze/normalize.rs | 1 | ||||
| -rw-r--r-- | dhall/src/semantics/nze/value.rs | 66 |
2 files changed, 32 insertions, 35 deletions
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index 89424e9..16c886e 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -449,7 +449,6 @@ pub(crate) fn normalize_whnf(v: ValueKind, ty: &Value) -> ValueKind { match v { ValueKind::AppliedBuiltin(closure) => closure.ensure_whnf(ty), ValueKind::PartialExpr(e) => normalize_one_layer(e, ty, &NzEnv::new()), - ValueKind::Thunk(th) => th.eval().kind().clone(), // All other cases are already in WHNF v => v, } 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<Value, Normalized>), - // 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<ValueKind> { 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); |