From 72d1e3c339cf550fa5af9981af6078a813feb80a Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 17 Jan 2020 11:03:40 +0000 Subject: Remove Shift/Subst traits --- dhall/src/semantics/core/value.rs | 158 +++++++++++++++++++------------------- 1 file changed, 78 insertions(+), 80 deletions(-) (limited to 'dhall/src/semantics/core/value.rs') diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index 28f8e37..ad03187 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -4,7 +4,7 @@ use std::rc::Rc; use crate::error::{TypeError, TypeMessage}; use crate::semantics::core::context::TyCtx; -use crate::semantics::core::var::{AlphaVar, Binder, Shift, Subst}; +use crate::semantics::core::var::{AlphaVar, Binder}; use crate::semantics::phase::normalize::{apply_any, normalize_whnf}; use crate::semantics::phase::typecheck::{builtin_to_value, const_to_value}; use crate::semantics::phase::{Normalized, NormalizedExpr, Typed}; @@ -238,6 +238,40 @@ impl Value { self.get_type() .expect("Internal type error: value is `Sort` but shouldn't be") } + + pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Option { + Some(Value(Rc::new(RefCell::new( + self.0.borrow().shift(delta, var)?, + )))) + } + pub(crate) fn over_binder(&self, x: T) -> Option + where + T: Into, + { + self.shift(-1, &x.into()) + } + pub(crate) fn under_binder(&self, x: T) -> Self + where + T: Into, + { + // Can't fail since delta is positive + self.shift(1, &x.into()).unwrap() + } + pub(crate) fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { + match &*self.as_kind() { + // If the var matches, we can just reuse the provided value instead of copying it. + // We also check that the types match, if in debug mode. + ValueKind::Var(v) if v == var => { + if let Ok(self_ty) = self.get_type() { + val.check_type(&self_ty.subst_shift(var, val)); + } + val.clone() + } + _ => Value(Rc::new(RefCell::new( + self.0.borrow().subst_shift(var, val), + ))), + } + } } impl ValueInternal { @@ -298,6 +332,27 @@ impl ValueInternal { None => Err(TypeError::new(&TyCtx::new(), TypeMessage::Sort)), } } + + pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Option { + Some(ValueInternal { + form: self.form, + kind: self.kind.shift(delta, var)?, + ty: match &self.ty { + None => None, + Some(ty) => Some(ty.shift(delta, var)?), + }, + span: self.span.clone(), + }) + } + pub(crate) fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { + ValueInternal { + // The resulting value may not stay in wnhf after substitution + form: Unevaled, + kind: self.kind.subst_shift(var, val), + ty: self.ty.as_ref().map(|x| x.subst_shift(var, val)), + span: self.span.clone(), + } + } } impl ValueKind { @@ -378,6 +433,28 @@ impl ValueKind { pub(crate) fn from_builtin(b: Builtin) -> ValueKind { ValueKind::AppliedBuiltin(b, vec![]) } + + pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Option { + Some(match self { + ValueKind::Var(v) => ValueKind::Var(v.shift(delta, var)?), + _ => self.traverse_ref_with_special_handling_of_binders( + |x| Ok(x.shift(delta, var)?), + |b, x| Ok(x.shift(delta, &var.under_binder(b))?), + )?, + }) + } + pub(crate) fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { + match self { + ValueKind::Var(v) if v == var => val.to_whnf_ignore_type(), + ValueKind::Var(v) => ValueKind::Var(v.shift(-1, var).unwrap()), + _ => self.map_ref_with_special_handling_of_binders( + |x| x.subst_shift(var, val), + |b, x| { + x.subst_shift(&var.under_binder(b), &val.under_binder(b)) + }, + ), + } + } } impl ValueKind { @@ -418,85 +495,6 @@ impl ValueKind { } } -impl Shift for Value { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option { - Some(Value(Rc::new(RefCell::new( - self.0.borrow().shift(delta, var)?, - )))) - } -} - -impl Shift for ValueInternal { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option { - Some(ValueInternal { - form: self.form, - kind: self.kind.shift(delta, var)?, - ty: match &self.ty { - None => None, - Some(ty) => Some(ty.shift(delta, var)?), - }, - span: self.span.clone(), - }) - } -} - -impl Shift for ValueKind { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option { - Some(match self { - ValueKind::Var(v) => ValueKind::Var(v.shift(delta, var)?), - _ => self.traverse_ref_with_special_handling_of_binders( - |x| Ok(x.shift(delta, var)?), - |b, x| Ok(x.shift(delta, &var.under_binder(b))?), - )?, - }) - } -} - -impl Subst for Value { - fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { - match &*self.as_kind() { - // If the var matches, we can just reuse the provided value instead of copying it. - // We also check that the types match, if in debug mode. - ValueKind::Var(v) if v == var => { - if let Ok(self_ty) = self.get_type() { - val.check_type(&self_ty.subst_shift(var, val)); - } - val.clone() - } - _ => Value(Rc::new(RefCell::new( - self.0.borrow().subst_shift(var, val), - ))), - } - } -} - -impl Subst for ValueInternal { - fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { - ValueInternal { - // The resulting value may not stay in wnhf after substitution - form: Unevaled, - kind: self.kind.subst_shift(var, val), - ty: self.ty.as_ref().map(|x| x.subst_shift(var, val)), - span: self.span.clone(), - } - } -} - -impl Subst for ValueKind { - fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { - match self { - ValueKind::Var(v) if v == var => val.to_whnf_ignore_type(), - ValueKind::Var(v) => ValueKind::Var(v.shift(-1, var).unwrap()), - _ => self.map_ref_with_special_handling_of_binders( - |x| x.subst_shift(var, val), - |b, x| { - x.subst_shift(&var.under_binder(b), &val.under_binder(b)) - }, - ), - } - } -} - // TODO: use Rc comparison to shortcut on identical pointers impl std::cmp::PartialEq for Value { fn eq(&self, other: &Self) -> bool { -- cgit v1.2.3