From c7d9a8659214a228963ea40d76e361bbc08129bb Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 18 Aug 2019 15:24:13 +0200 Subject: Rework ValueInternal and clarify invariants around ValueF --- Cargo.lock | 1 + dhall/Cargo.toml | 1 + dhall/src/core/value.rs | 103 +++++++++++++++++++++++-------------------- dhall/src/core/valuef.rs | 30 ++++--------- dhall/src/phase/normalize.rs | 29 ++++++++---- 5 files changed, 86 insertions(+), 78 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index ccd8520..c073fad 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -75,6 +75,7 @@ dependencies = [ "pretty_assertions 0.6.1 (registry+https://github.com/rust-lang/crates.io-index)", "serde 1.0.90 (registry+https://github.com/rust-lang/crates.io-index)", "serde_cbor 0.9.0 (registry+https://github.com/rust-lang/crates.io-index)", + "take_mut 0.2.2 (registry+https://github.com/rust-lang/crates.io-index)", "term-painter 0.2.4 (registry+https://github.com/rust-lang/crates.io-index)", "walkdir 2.2.7 (registry+https://github.com/rust-lang/crates.io-index)", ] diff --git a/dhall/Cargo.toml b/dhall/Cargo.toml index 0a257e4..16c1c78 100644 --- a/dhall/Cargo.toml +++ b/dhall/Cargo.toml @@ -9,6 +9,7 @@ build = "build.rs" [dependencies] bytecount = "0.5.1" itertools = "0.8.0" +take_mut = "0.2.2" term-painter = "0.2.3" serde = { version = "1.0" } serde_cbor = "0.9.0" diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 5c29bf0..19976af 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -8,28 +8,32 @@ use crate::core::context::TypecheckContext; use crate::core::valuef::ValueF; use crate::core::var::{AlphaVar, Shift, Subst}; use crate::error::{TypeError, TypeMessage}; -use crate::phase::normalize::{apply_any, normalize_one_layer, OutputSubExpr}; +use crate::phase::normalize::{apply_any, normalize_whnf, OutputSubExpr}; use crate::phase::typecheck::type_of_const; use crate::phase::{Normalized, NormalizedSubExpr, Type, Typed}; #[derive(Debug, Clone, Copy)] -enum Marker { - /// Weak Head Normal Form, i.e. subexpressions may not be normalized +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 ValueF is the first + /// constructor of the final Normal Form (NF). WHNF, - /// Normal form, i.e. completely normalized + /// Normal Form, i.e. completely normalized. + /// When all the Values in a ValueF are at least in WHNF, and recursively so, then the + /// ValueF 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. NF, } -use Marker::{NF, WHNF}; +use Form::{Unevaled, NF, WHNF}; #[derive(Debug, Clone)] enum ValueInternal { - /// Partially normalized value whose subexpressions have been thunked (this is returned from - /// typechecking). Note that this is different from `ValueF::PartialExpr` because there is no - /// requirement of WHNF here. - PartialExpr(ExprF), /// Partially normalized value. + /// Invariant: if the marker is `WHNF`, the value must be in Weak Head Normal Form /// Invariant: if the marker is `NF`, the value must be fully normalized - ValueF(Marker, ValueF), + ValueF(Form, ValueF), } #[derive(Debug)] @@ -45,6 +49,8 @@ struct TypedValueInternal { #[derive(Clone)] pub struct Value(Rc>); +/// A value that needs to carry a type for typechecking to work. +/// TODO: actually enforce this. #[derive(Debug, Clone)] pub struct TypedValue(Value); @@ -58,25 +64,25 @@ impl ValueInternal { } fn normalize_whnf(&mut self) { - match self { - ValueInternal::PartialExpr(e) => { - *self = - ValueInternal::ValueF(WHNF, normalize_one_layer(e.clone())) + take_mut::take(self, |vint| match vint { + ValueInternal::ValueF(Unevaled, v) => { + ValueInternal::ValueF(WHNF, normalize_whnf(v)) } - // Already at least in WHNF - ValueInternal::ValueF(_, _) => {} - } + // Already in WHNF + vint @ ValueInternal::ValueF(WHNF, _) + | vint @ ValueInternal::ValueF(NF, _) => vint, + }) } fn normalize_nf(&mut self) { match self { - ValueInternal::PartialExpr(_) => { + ValueInternal::ValueF(Unevaled, _) => { self.normalize_whnf(); self.normalize_nf(); } - ValueInternal::ValueF(m @ WHNF, v) => { + ValueInternal::ValueF(f @ WHNF, v) => { v.normalize_mut(); - *m = NF; + *f = NF; } // Already in NF ValueInternal::ValueF(NF, _) => {} @@ -86,7 +92,7 @@ impl ValueInternal { // Always use normalize_whnf before fn as_whnf(&self) -> &ValueF { match self { - ValueInternal::PartialExpr(_) => unreachable!(), + ValueInternal::ValueF(Unevaled, _) => unreachable!(), ValueInternal::ValueF(_, v) => v, } } @@ -94,9 +100,8 @@ impl ValueInternal { // Always use normalize_nf before fn as_nf(&self) -> &ValueF { match self { - ValueInternal::PartialExpr(_) | ValueInternal::ValueF(WHNF, _) => { - unreachable!() - } + ValueInternal::ValueF(Unevaled, _) + | ValueInternal::ValueF(WHNF, _) => unreachable!(), ValueInternal::ValueF(NF, v) => v, } } @@ -126,13 +131,13 @@ impl TypedValueInternal { impl Value { pub(crate) fn from_valuef(v: ValueF) -> Value { - ValueInternal::ValueF(WHNF, v).into_value(None) + ValueInternal::ValueF(Unevaled, v).into_value(None) } pub(crate) fn from_valuef_and_type(v: ValueF, t: Type) -> Value { - ValueInternal::ValueF(WHNF, v).into_value(Some(t)) + ValueInternal::ValueF(Unevaled, v).into_value(Some(t)) } pub(crate) fn from_partial_expr(e: ExprF) -> Value { - ValueInternal::PartialExpr(e).into_value(None) + Value::from_valuef(ValueF::PartialExpr(e)) } pub(crate) fn with_type(self, t: Type) -> Value { self.as_internal().clone().into_value(Some(t)) @@ -150,7 +155,7 @@ impl Value { } /// Normalizes contents to normal form; faster than `normalize_nf` if - /// no one else shares this thunk + /// no one else shares this thunk. pub(crate) fn normalize_mut(&mut self) { self.mutate_internal(|i| i.as_internal_mut().normalize_nf()) } @@ -171,19 +176,20 @@ impl Value { fn do_normalize_whnf(&self) { let borrow = self.as_internal(); match &*borrow { - ValueInternal::PartialExpr(_) => { + ValueInternal::ValueF(Unevaled, _) => { drop(borrow); self.as_internal_mut().normalize_whnf(); } // Already at least in WHNF - ValueInternal::ValueF(_, _) => {} + ValueInternal::ValueF(WHNF, _) | ValueInternal::ValueF(NF, _) => {} } } fn do_normalize_nf(&self) { let borrow = self.as_internal(); match &*borrow { - ValueInternal::PartialExpr(_) | ValueInternal::ValueF(WHNF, _) => { + ValueInternal::ValueF(Unevaled, _) + | ValueInternal::ValueF(WHNF, _) => { drop(borrow); self.as_internal_mut().normalize_nf(); } @@ -199,13 +205,21 @@ impl Value { Ref::map(self.as_internal(), ValueInternal::as_nf) } - // WARNING: avoid normalizing any thunk while holding on to this ref - // or you could run into BorrowMut panics + /// WARNING: avoid normalizing any thunk while holding on to this ref + /// or you could run into BorrowMut panics + /// TODO: deprecated because of misleading name pub(crate) fn as_valuef(&self) -> Ref { + self.as_whnf() + } + + /// WARNING: avoid normalizing any thunk while holding on to this ref + /// or you could run into BorrowMut panics + pub(crate) fn as_whnf(&self) -> Ref { self.do_normalize_whnf(); Ref::map(self.as_internal(), ValueInternal::as_whnf) } + /// TODO: deprecated because of misleading name pub(crate) fn to_valuef(&self) -> ValueF { self.as_valuef().clone() } @@ -317,11 +331,8 @@ impl Shift for Value { impl Shift for ValueInternal { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { Some(match self { - ValueInternal::PartialExpr(e) => { - ValueInternal::PartialExpr(e.shift(delta, var)?) - } - ValueInternal::ValueF(m, v) => { - ValueInternal::ValueF(*m, v.shift(delta, var)?) + ValueInternal::ValueF(f, v) => { + ValueInternal::ValueF(*f, v.shift(delta, var)?) } }) } @@ -351,12 +362,9 @@ impl Subst for Value { impl Subst for ValueInternal { fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { match self { - ValueInternal::PartialExpr(e) => { - ValueInternal::PartialExpr(e.subst_shift(var, val)) - } ValueInternal::ValueF(_, v) => { - // The resulting value may not stay in normal form after substitution - ValueInternal::ValueF(WHNF, v.subst_shift(var, val)) + // The resulting value may not stay in wnhf after substitution + ValueInternal::ValueF(Unevaled, v.subst_shift(var, val)) } } } @@ -392,14 +400,11 @@ impl std::cmp::PartialEq for TypedValue { impl std::cmp::Eq for TypedValue {} impl std::fmt::Debug for Value { - fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { let b: &ValueInternal = &self.as_internal(); match b { - ValueInternal::ValueF(m, v) => { - f.debug_tuple(&format!("Value@{:?}", m)).field(v).finish() - } - ValueInternal::PartialExpr(e) => { - f.debug_tuple("Value@PartialExpr").field(e).finish() + ValueInternal::ValueF(f, v) => { + fmt.debug_tuple(&format!("Value@{:?}", f)).field(v).finish() } } } diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs index bea2e2e..9e6e8c8 100644 --- a/dhall/src/core/valuef.rs +++ b/dhall/src/core/valuef.rs @@ -7,22 +7,13 @@ use dhall_syntax::{ use crate::core::value::{TypedValue, Value}; use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; -use crate::phase::normalize::{ - apply_builtin, normalize_one_layer, squash_textlit, OutputSubExpr, -}; +use crate::phase::normalize::OutputSubExpr; use crate::phase::{Normalized, Typed}; -/// A semantic value. The invariants ensure this value represents a Weak-Head -/// Normal Form (WHNF). This means that this first constructor is the first constructor of the -/// final Normal Form (NF). -/// This WHNF must be preserved by operations on `ValueF`s. In particular, `subst_shift` could break -/// the invariants so need to be careful to reevaluate as needed. -/// Subexpressions are Values, which are partially evaluated expressions that are normalized -/// on-demand. When all the Values in a ValueF are at least in WHNF, and recursively so, then the -/// ValueF 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 semantic value. Subexpressions are Values, which are partially evaluated expressions that are +/// normalized on-demand. /// Equality is up to alpha-equivalence (renaming of bound variables) and beta-equivalence -/// (normalization). Equality will normalize only as needed. +/// (normalization). Equality will normalize as needed. #[derive(Debug, Clone, PartialEq, Eq)] pub enum ValueF { /// Closures @@ -338,18 +329,15 @@ impl Shift for ValueF { impl Subst for ValueF { fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { match self { - // Retry normalizing since substituting may allow progress ValueF::AppliedBuiltin(b, args) => { - apply_builtin(*b, args.subst_shift(var, val)) + ValueF::AppliedBuiltin(*b, args.subst_shift(var, val)) } - // Retry normalizing since substituting may allow progress ValueF::PartialExpr(e) => { - normalize_one_layer(e.subst_shift(var, val)) + ValueF::PartialExpr(e.subst_shift(var, val)) + } + ValueF::TextLit(elts) => { + ValueF::TextLit(elts.subst_shift(var, val)) } - // Retry normalizing since substituting may allow progress - ValueF::TextLit(elts) => ValueF::TextLit(squash_textlit( - elts.iter().map(|contents| contents.subst_shift(var, val)), - )), ValueF::Lam(x, t, e) => ValueF::Lam( x.clone(), t.subst_shift(var, val), diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs index 93f2528..6c65e43 100644 --- a/dhall/src/phase/normalize.rs +++ b/dhall/src/phase/normalize.rs @@ -389,14 +389,6 @@ pub(crate) fn squash_textlit( ret } -// Small helper enum to avoid repetition -enum Ret<'a> { - ValueF(ValueF), - Value(Value), - ValueRef(&'a Value), - Expr(ExprF), -} - /// Performs an intersection of two HashMaps. /// /// # Arguments @@ -510,6 +502,14 @@ where kvs } +// Small helper enum to avoid repetition +enum Ret<'a> { + ValueF(ValueF), + Value(Value), + ValueRef(&'a Value), + Expr(ExprF), +} + fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option> { use BinOp::{ BoolAnd, BoolEQ, BoolNE, BoolOr, Equivalence, ListAppend, NaturalPlus, @@ -819,3 +819,16 @@ pub(crate) fn normalize_one_layer(expr: ExprF) -> ValueF { Ret::Expr(expr) => ValueF::PartialExpr(expr), } } + +/// Normalize a ValueF into WHNF +pub(crate) fn normalize_whnf(v: ValueF) -> ValueF { + match v { + ValueF::AppliedBuiltin(b, args) => apply_builtin(b, args), + ValueF::PartialExpr(e) => normalize_one_layer(e), + ValueF::TextLit(elts) => { + ValueF::TextLit(squash_textlit(elts.into_iter())) + } + // All other cases are already in WHNF + v => v, + } +} -- cgit v1.2.3