diff options
author | Nadrieril | 2020-01-17 18:42:13 +0000 |
---|---|---|
committer | Nadrieril | 2020-01-17 18:42:13 +0000 |
commit | 0f4a4801ed67826dc82015d39ce8fd05e7950035 (patch) | |
tree | f8393bb9e8abaccc8db0e1c17ae1d1a39b88ff7b /dhall/src/semantics | |
parent | ab672506fd45e33f60b1b962c4757f912b6e27be (diff) |
Replace all bulk shifting by a single shift
Diffstat (limited to 'dhall/src/semantics')
-rw-r--r-- | dhall/src/semantics/core/context.rs | 15 | ||||
-rw-r--r-- | dhall/src/semantics/core/value.rs | 45 | ||||
-rw-r--r-- | dhall/src/semantics/core/var.rs | 20 |
3 files changed, 8 insertions, 72 deletions
diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs index f8d6ff0..47d2d2d 100644 --- a/dhall/src/semantics/core/context.rs +++ b/dhall/src/semantics/core/context.rs @@ -1,5 +1,3 @@ -use std::collections::HashMap; - use crate::error::TypeError; use crate::semantics::core::value::Value; use crate::semantics::core::value::ValueKind; @@ -40,7 +38,7 @@ impl TyCtx { } pub fn lookup(&self, var: &V<Label>) -> Option<Value> { let mut var = var.clone(); - let mut shift_map: HashMap<Label, usize> = HashMap::new(); + let mut shift_delta: isize = 0; let mut rev_ctx = self.ctx.iter().rev().map(|(b, i)| (b.to_label(), i)); let found_item = loop { @@ -50,7 +48,7 @@ impl TyCtx { None => break item, }; if let CtxItem::Kept(_, _) = item { - *shift_map.entry(label).or_insert(0) += 1; + shift_delta += 1; } } else { // Unbound variable @@ -65,13 +63,8 @@ impl TyCtx { ), CtxItem::Replaced(v) => v.clone(), }; - - let v = v.under_multiple_binders(&shift_map); - // for (x, n) in shift_map { - // let x: AlphaVar = (&x).into(); - // // Can't fail since delta is positive - // v = v.shift(n as isize, &x).unwrap(); - // } + // Can't fail because delta is positive + let v = v.shift(shift_delta, &AlphaVar::default()).unwrap(); return Some(v); } // pub fn lookup_alpha(&self, var: &AlphaVar) -> Option<Value> { diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index d843a1b..6ae0a90 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -255,14 +255,6 @@ impl Value { // Can't fail since delta is positive self.shift(1, &x.into()).unwrap() } - pub(crate) fn under_multiple_binders( - &self, - shift_map: &HashMap<Label, usize>, - ) -> Self { - self.as_internal() - .under_multiple_binders(shift_map) - .into_value() - } 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. @@ -369,20 +361,6 @@ impl ValueInternal { span: self.span.clone(), }) } - fn under_multiple_binders( - &self, - shift_map: &HashMap<Label, usize>, - ) -> Self { - ValueInternal { - form: self.form, - kind: self.kind.under_multiple_binders(shift_map), - ty: match &self.ty { - None => None, - Some(ty) => Some(ty.under_multiple_binders(shift_map)), - }, - span: self.span.clone(), - } - } fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { ValueInternal { // The resulting value may not stay in wnhf after substitution @@ -482,29 +460,6 @@ impl ValueKind<Value> { )?, }) } - #[allow(dead_code)] - fn under_multiple_binders( - &self, - shift_map: &HashMap<Label, usize>, - ) -> Self { - match self { - ValueKind::Var(v) => { - ValueKind::Var(v.under_multiple_binders(shift_map)) - } - _ => self.map_ref_with_special_handling_of_binders( - |v| v.under_multiple_binders(shift_map), - |b, _, v| { - let mut v = v.clone(); - for (x, n) in shift_map { - let x: AlphaVar = x.into(); - // Can't fail since delta is positive - v = v.shift(*n as isize, &x.under_binder(b)).unwrap(); - } - v - }, - ), - } - } fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { match self { ValueKind::Var(v) if v == var => val.to_whnf_ignore_type(), diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs index f3475e7..93776bf 100644 --- a/dhall/src/semantics/core/var.rs +++ b/dhall/src/semantics/core/var.rs @@ -1,5 +1,3 @@ -use std::collections::HashMap; - use crate::syntax::{Label, V}; /// Stores an alpha-normalized variable. @@ -16,6 +14,9 @@ pub struct Binder { } impl AlphaVar { + pub(crate) fn default() -> Self { + AlphaVar { alpha: V((), 0) } + } pub(crate) fn idx(&self) -> usize { self.alpha.idx() } @@ -35,14 +36,6 @@ impl AlphaVar { pub(crate) fn over_binder(&self, x: &AlphaVar) -> Option<Self> { self.shift(-1, x) } - pub(crate) fn under_multiple_binders( - &self, - shift_map: &HashMap<Label, usize>, - ) -> Self { - AlphaVar { - alpha: self.alpha.under_multiple_binders(shift_map), - } - } } impl Binder { @@ -89,11 +82,6 @@ impl std::fmt::Debug for Binder { } } -impl<'a> From<&'a Label> for AlphaVar { - fn from(x: &'a Label) -> AlphaVar { - AlphaVar { alpha: V((), 0) } - } -} impl From<Binder> for AlphaVar { fn from(x: Binder) -> AlphaVar { AlphaVar { alpha: V((), 0) } @@ -101,7 +89,7 @@ impl From<Binder> for AlphaVar { } impl<'a> From<&'a Binder> for AlphaVar { fn from(x: &'a Binder) -> AlphaVar { - x.clone().into() + AlphaVar { alpha: V((), 0) } } } |