From 3b9dac7fccf5faea61703177cafe476f72518585 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 4 May 2019 20:42:05 +0200 Subject: subst_shift now correctly preserves WHNF --- dhall/src/normalize.rs | 50 ++++++++++++++++++++++++-------------------------- 1 file changed, 24 insertions(+), 26 deletions(-) diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs index d84c2d5..904c0a2 100644 --- a/dhall/src/normalize.rs +++ b/dhall/src/normalize.rs @@ -25,17 +25,13 @@ impl Typed { /// leave ill-typed sub-expressions unevaluated. /// pub fn normalize(self) -> Normalized { - let internal = match self.0 { - TypedInternal::Sort => TypedInternal::Sort, - TypedInternal::Value(thunk, t) => { - // TODO: stupid but needed for now - let thunk = - Thunk::from_normalized_expr(thunk.normalize_to_expr()); + match &self.0 { + TypedInternal::Sort => {} + TypedInternal::Value(thunk, _) => { thunk.normalize_nf(); - TypedInternal::Value(thunk, t) } - }; - Normalized(internal) + } + Normalized(self.0) } pub(crate) fn shift(&self, delta: isize, var: &V