diff options
author | Nadrieril | 2020-01-30 19:56:31 +0000 |
---|---|---|
committer | Nadrieril | 2020-01-30 19:56:31 +0000 |
commit | d8de45763037937b5c2dedbe5f7bb95a4e7bc7cd (patch) | |
tree | 0c73b8ec2df6e8f592136133f07957e3ae8e8931 | |
parent | 673a580e11d31356bec25d73213b283685fd6ea3 (diff) |
Avoid unnecessary allocations of `Value`s
-rw-r--r-- | dhall/src/semantics/nze/env.rs | 16 | ||||
-rw-r--r-- | dhall/src/semantics/nze/normalize.rs | 21 | ||||
-rw-r--r-- | dhall/src/semantics/nze/value.rs | 6 | ||||
-rw-r--r-- | dhall/src/semantics/tck/env.rs | 2 | ||||
-rw-r--r-- | dhall/src/semantics/tck/tyexpr.rs | 5 |
5 files changed, 25 insertions, 25 deletions
diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs index 073886e..0b22a8b 100644 --- a/dhall/src/semantics/nze/env.rs +++ b/dhall/src/semantics/nze/env.rs @@ -59,14 +59,18 @@ impl NzEnv { env.items.push(NzEnvItem::Replaced(e)); env } - pub fn lookup_val(&self, var: &AlphaVar) -> Value { + pub fn lookup_val(&self, var: &AlphaVar) -> ValueKind { let idx = self.items.len() - 1 - var.idx(); match &self.items[idx] { - NzEnvItem::Kept(ty) => Value::from_kind_and_type( - ValueKind::Var(NzVar::new(idx)), - ty.clone(), - ), - NzEnvItem::Replaced(x) => x.clone(), + NzEnvItem::Kept(_) => ValueKind::Var(NzVar::new(idx)), + NzEnvItem::Replaced(x) => x.kind().clone(), + } + } + pub fn lookup_ty(&self, var: &AlphaVar) -> Value { + let idx = self.items.len() - 1 - var.idx(); + match &self.items[idx] { + NzEnvItem::Kept(ty) => ty.clone(), + NzEnvItem::Replaced(x) => x.get_type().unwrap(), } } } diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index 7632d12..e677f78 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -445,14 +445,9 @@ pub(crate) fn normalize_one_layer( } /// Normalize a TyExpr into WHNF -pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value { - let ty = match tye.get_type() { - Ok(ty) => ty, - Err(_) => return Value::from_const(Const::Sort), - }; - - let kind = match tye.kind() { - TyExprKind::Var(var) => return env.lookup_val(var), +pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> ValueKind { + match tye.kind() { + TyExprKind::Var(var) => env.lookup_val(var), TyExprKind::Expr(ExprKind::Lam(binder, annot, body)) => { let annot = annot.eval(env); ValueKind::LamClosure { @@ -472,13 +467,15 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value { } TyExprKind::Expr(ExprKind::Let(_, None, val, body)) => { let val = val.eval(env); - return body.eval(&env.insert_value(val)); + body.eval(&env.insert_value(val)).kind().clone() } TyExprKind::Expr(e) => { + let ty = match tye.get_type() { + Ok(ty) => ty, + Err(_) => return ValueKind::Const(Const::Sort), + }; let e = e.map_ref(|tye| tye.eval(env)); normalize_one_layer(e, &ty, env) } - }; - - Value::from_kind_and_type(kind, ty) + } } diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index 108dc9c..ff0ca42 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -405,7 +405,7 @@ impl ValueInternal { use std::mem::replace; let dummy = Form::PartialExpr(ExprKind::Const(Const::Type)); self.form = match replace(&mut self.form, dummy) { - Form::Thunk(th) => Form::WHNF(th.eval().kind().clone()), + Form::Thunk(th) => Form::WHNF(th.eval()), Form::PartialExpr(e) => { Form::WHNF(match &self.ty { // TODO: env @@ -516,9 +516,7 @@ impl Thunk { body, } } - - // TODO: maybe return a ValueKind ? - pub fn eval(&self) -> Value { + pub fn eval(&self) -> ValueKind { normalize_tyexpr_whnf(&self.body, &self.env) } } diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs index d4cc37d..812ca7a 100644 --- a/dhall/src/semantics/tck/env.rs +++ b/dhall/src/semantics/tck/env.rs @@ -118,7 +118,7 @@ impl TyEnv { } pub fn lookup(&self, var: &V) -> Option<(TyExprKind, Type)> { let var = self.names.unlabel_var(var)?; - let ty = self.items.lookup_val(&var).get_type().unwrap(); + let ty = self.items.lookup_ty(&var); Some((TyExprKind::Var(var), ty)) } } diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs index 4b88048..1a048f9 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -1,5 +1,4 @@ use crate::error::{TypeError, TypeMessage}; -use crate::semantics::normalize_tyexpr_whnf; use crate::semantics::{rc, NameEnv, NzEnv, TyEnv, Value}; use crate::syntax::{ExprKind, Span, V}; use crate::Normalized; @@ -83,7 +82,9 @@ impl TyExpr { } /// Eval a closed TyExpr fully and recursively; pub fn rec_eval_closed_expr(&self) -> Value { - normalize_tyexpr_whnf(self, &NzEnv::new()) + let mut val = self.eval_closed_expr(); + val.normalize_mut(); + val } } |