From 67bbbafbc9730d74e20e5ac082ae9a87bdf2234e Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 16:39:25 +0000 Subject: Introduce Thunks and normalize lazily --- dhall/src/semantics/phase/mod.rs | 2 +- dhall/src/semantics/phase/normalize.rs | 11 ++++++----- 2 files changed, 7 insertions(+), 6 deletions(-) (limited to 'dhall/src/semantics/phase') diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs index f24a668..a25f096 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -91,7 +91,7 @@ impl Resolved { impl Typed { /// Reduce an expression to its normal form, performing beta reduction pub fn normalize(&self) -> Normalized { - Normalized(self.0.normalize_nf_noenv()) + Normalized(self.0.rec_eval_closed_expr()) } /// Converts a value back to the corresponding AST expression. diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index f36ec4a..ea1a25b 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -457,6 +457,7 @@ pub(crate) fn normalize_whnf( 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(), ValueKind::TextLit(elts) => { ValueKind::TextLit(squash_textlit(elts.into_iter())) } @@ -475,7 +476,7 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value { let kind = match tye.kind() { TyExprKind::Var(var) => return env.lookup_val(var), TyExprKind::Expr(ExprKind::Lam(binder, annot, body)) => { - let annot = annot.normalize_whnf(env); + let annot = annot.eval(env); ValueKind::LamClosure { binder: Binder::new(binder.clone()), annot: annot.clone(), @@ -483,7 +484,7 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value { } } TyExprKind::Expr(ExprKind::Pi(binder, annot, body)) => { - let annot = annot.normalize_whnf(env); + let annot = annot.eval(env); let closure = Closure::new(annot.clone(), env, body.clone()); ValueKind::PiClosure { binder: Binder::new(binder.clone()), @@ -492,11 +493,11 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value { } } TyExprKind::Expr(ExprKind::Let(_, None, val, body)) => { - let val = val.normalize_whnf(env); - return body.normalize_whnf(&env.insert_value(val)); + let val = val.eval(env); + return body.eval(&env.insert_value(val)); } TyExprKind::Expr(e) => { - let e = e.map_ref(|tye| tye.normalize_whnf(env)); + let e = e.map_ref(|tye| tye.eval(env)); normalize_one_layer(e, &ty, env) } }; -- cgit v1.2.3