From 29016b78736dca857e4e7f7c4dc68ed5e30c28bb Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 19 Aug 2019 12:25:09 +0200 Subject: s/to_valuef/to_whnf/ and avoid cloning ValueFs when possible --- dhall/src/core/valuef.rs | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'dhall/src/core/valuef.rs') diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs index 9e6e8c8..0ba1d59 100644 --- a/dhall/src/core/valuef.rs +++ b/dhall/src/core/valuef.rs @@ -12,8 +12,9 @@ use crate::phase::{Normalized, Typed}; /// 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 as needed. +/// If you compare for equality two `ValueF`s in WHNF, then equality will be up to +/// alpha-equivalence (renaming of bound variables) and beta-equivalence (normalization). It will +/// recursively normalize as needed. #[derive(Debug, Clone, PartialEq, Eq)] pub enum ValueF { /// Closures @@ -348,7 +349,7 @@ impl Subst for ValueF { t.subst_shift(var, val), e.subst_shift(&var.under_binder(x), &val.under_binder(x)), ), - ValueF::Var(v) if v == var => val.to_valuef(), + ValueF::Var(v) if v == var => val.to_whnf(), ValueF::Var(v) => ValueF::Var(v.shift(-1, var).unwrap()), ValueF::Const(c) => ValueF::Const(*c), ValueF::BoolLit(b) => ValueF::BoolLit(*b), -- cgit v1.2.3