summaryrefslogtreecommitdiff
path: root/dhall/src
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src')
-rw-r--r--dhall/src/semantics/core/context.rs15
-rw-r--r--dhall/src/semantics/core/value.rs45
-rw-r--r--dhall/src/semantics/core/var.rs20
-rw-r--r--dhall/src/syntax/ast/expr.rs26
4 files changed, 8 insertions, 98 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) }
}
}
diff --git a/dhall/src/syntax/ast/expr.rs b/dhall/src/syntax/ast/expr.rs
index 2372b0a..170cbe7 100644
--- a/dhall/src/syntax/ast/expr.rs
+++ b/dhall/src/syntax/ast/expr.rs
@@ -1,5 +1,3 @@
-use std::collections::HashMap;
-
use crate::syntax::map::{DupTreeMap, DupTreeSet};
use crate::syntax::visitor::{self, ExprKindMutVisitor, ExprKindVisitor};
use crate::syntax::*;
@@ -319,30 +317,6 @@ impl<Label: PartialEq + Clone> V<Label> {
}
}
-impl V<Label> {
- pub(crate) fn under_multiple_binders(
- &self,
- shift_map: &HashMap<Label, usize>,
- ) -> Self {
- let name = &self.0;
- let idx = self.1 + shift_map.get(name).unwrap_or(&0);
- V(name.clone(), idx)
- }
-}
-
-impl V<()> {
- pub(crate) fn under_multiple_binders(
- &self,
- shift_map: &HashMap<Label, usize>,
- ) -> Self {
- let mut idx = self.1;
- for (_, n) in shift_map {
- idx += n;
- }
- V((), idx)
- }
-}
-
pub fn trivial_result<T>(x: Result<T, !>) -> T {
match x {
Ok(x) => x,
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 18:49:21 +0000