From 280b3174476ef8fe5a98f3614f4fe253fa243d8c Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 29 Jan 2020 21:35:28 +0000 Subject: Finally get rid of all of the shift/subst_shift ! --- dhall/src/semantics/core/value.rs | 72 ---------------------------------- dhall/src/semantics/core/var.rs | 10 ----- dhall/src/semantics/nze/nzexpr.rs | 3 -- dhall/src/semantics/phase/normalize.rs | 8 ++-- 4 files changed, 3 insertions(+), 90 deletions(-) (limited to 'dhall/src/semantics') diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index df1382b..90b30b4 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -256,27 +256,6 @@ impl Value { .expect("Internal type error: value is `Sort` but shouldn't be") } - pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Option { - Some(self.as_internal().shift(delta, var)?.into_value()) - } - pub(crate) fn under_binder(&self) -> Self { - // Can't fail since delta is positive - self.shift(1, &AlphaVar::default()).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() - } - _ => self.as_internal().subst_shift(var, val).into_value(), - } - } - pub fn to_tyexpr(&self, venv: VarEnv) -> TyExpr { let tye = match &*self.as_kind() { // ValueKind::Var(v, _w) => TyExprKind::Var(*v), @@ -487,27 +466,6 @@ impl ValueInternal { None => Err(TypeError::new(TypeMessage::Sort)), } } - - 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(), - }) - } - 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 { @@ -588,36 +546,6 @@ impl ValueKind { pub(crate) fn from_builtin_env(b: Builtin, env: NzEnv) -> ValueKind { ValueKind::AppliedBuiltin(b, vec![], vec![], env) } - - fn shift(&self, delta: isize, var: &AlphaVar) -> Option { - Some(match self { - ValueKind::Var(v, w) if var.idx() <= v.idx() => { - ValueKind::Var(v.shift(delta, var)?, *w) - } - ValueKind::Var(v, w) => { - ValueKind::Var(v.shift(delta, var)?, w.shift(delta)) - } - // ValueKind::Var(v, w) => ValueKind::Var(v.shift(delta, var)?, *w), - _ => self.traverse_ref_with_special_handling_of_binders( - |x| Ok(x.shift(delta, var)?), - |_, _, x| Ok(x.shift(delta, &var.under_binder())?), - )?, - }) - } - 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, w) => { - ValueKind::Var(v.shift(-1, var).unwrap(), *w) - } - _ => self.map_ref_with_special_handling_of_binders( - |x| x.subst_shift(var, val), - |_, _, x| { - x.subst_shift(&var.under_binder(), &val.under_binder()) - }, - ), - } - } } impl ValueKind { diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs index cf45d5e..3458489 100644 --- a/dhall/src/semantics/core/var.rs +++ b/dhall/src/semantics/core/var.rs @@ -29,16 +29,6 @@ impl AlphaVar { pub(crate) fn idx(&self) -> usize { self.alpha.idx() } - - pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Option { - Some(AlphaVar { - alpha: self.alpha.shift(delta, &var.alpha)?, - }) - } - pub(crate) fn under_binder(&self) -> Self { - // Can't fail since delta is positive - self.shift(1, &AlphaVar::default()).unwrap() - } } impl Binder { diff --git a/dhall/src/semantics/nze/nzexpr.rs b/dhall/src/semantics/nze/nzexpr.rs index 87d0269..c065a5b 100644 --- a/dhall/src/semantics/nze/nzexpr.rs +++ b/dhall/src/semantics/nze/nzexpr.rs @@ -104,9 +104,6 @@ impl NzVar { let id = FRESH_VAR_COUNTER.fetch_add(1, Ordering::SeqCst); NzVar::Fresh(id) } - pub fn shift(&self, delta: isize) -> Self { - NzVar::new((self.idx() as isize + delta) as usize) - } // Panics on a fresh variable. pub fn idx(&self) -> usize { match self { diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index d40456b..fa80b6e 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -638,15 +638,13 @@ pub(crate) fn normalize_one_layer( ), // Those cases have already been completely handled in the typechecking phase (using // `RetWhole`), so they won't appear here. - ExprKind::Lam(_, _, _) - | ExprKind::Pi(_, _, _) + ExprKind::Lam(..) + | ExprKind::Pi(..) + | ExprKind::Let(..) | ExprKind::Embed(_) | ExprKind::Var(_) => { unreachable!("This case should have been handled in typecheck") } - ExprKind::Let(_, _, val, body) => { - Ret::Value(body.subst_shift(&AlphaVar::default(), &val)) - } ExprKind::Annot(x, _) => Ret::Value(x), ExprKind::Const(c) => Ret::Value(const_to_value(c)), ExprKind::Builtin(b) => Ret::Value(builtin_to_value_env(b, env)), -- cgit v1.2.3