diff options
author | Nadrieril | 2020-01-30 14:52:35 +0000 |
---|---|---|
committer | Nadrieril | 2020-01-30 14:52:35 +0000 |
commit | 4c4ec8614b84d72fee4d765857325b73dad16183 (patch) | |
tree | d9bb55e9692eecaaa565a8fec9ec6b425b35059c /dhall/src/semantics | |
parent | 837298f26e07bb264a6b6f0286cbb811553b0477 (diff) |
Remove NF marker; it was premature optimization
Diffstat (limited to 'dhall/src/semantics')
-rw-r--r-- | dhall/src/semantics/core/value.rs | 33 |
1 files changed, 11 insertions, 22 deletions
diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index bf75710..4c844ee 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -13,7 +13,7 @@ use crate::syntax::{ NaiveDouble, Natural, Span, }; -use self::Form::{Unevaled, NF, WHNF}; +use self::Form::{Unevaled, WHNF}; /// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, sharing computation /// automatically. Uses a RefCell to share computation. @@ -25,7 +25,6 @@ use self::Form::{Unevaled, NF, WHNF}; pub(crate) struct Value(Rc<RefCell<ValueInternal>>); /// Invariant: if `form` is `WHNF`, `value` must be in Weak Head Normal Form -/// Invariant: if `form` is `NF`, `value` must be fully normalized #[derive(Debug)] struct ValueInternal { form: Form, @@ -42,12 +41,10 @@ pub(crate) enum Form { /// 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). - WHNF, - /// Normal Form, i.e. completely normalized. - /// When all the Values in a ValueKind are at least in WHNF, and recursively so, then the + /// 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. - NF, + WHNF, } #[derive(Debug, Clone)] @@ -116,7 +113,7 @@ impl Value { } pub(crate) fn const_sort() -> Value { ValueInternal { - form: NF, + form: WHNF, kind: ValueKind::Const(Const::Sort), ty: None, span: Span::Artificial, @@ -219,8 +216,8 @@ impl Value { drop(borrow); self.as_internal_mut().normalize_whnf(); } - // Already at least in WHNF - WHNF | NF => {} + // Already in WHNF + WHNF => {} } } pub(crate) fn normalize_nf(&self) { @@ -415,28 +412,20 @@ impl ValueInternal { }, // `value` is `Sort` (Unevaled, None) => ValueInternal { - form: NF, + form: WHNF, kind: ValueKind::Const(Const::Sort), ty: None, span: vint.span, }, // Already in WHNF - (WHNF, _) | (NF, _) => vint, + (WHNF, _) => vint, } } fn normalize_nf(&mut self) { - match self.form { - Unevaled => { - self.normalize_whnf(); - self.normalize_nf(); - } - WHNF => { - self.kind.normalize_mut(); - self.form = NF; - } - // Already in NF - NF => {} + if let Unevaled = self.form { + self.normalize_whnf(); } + self.kind.normalize_mut(); } fn get_type(&self) -> Result<&Value, TypeError> { |