summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/semantics/core/value.rs72
-rw-r--r--dhall/src/semantics/core/var.rs10
-rw-r--r--dhall/src/semantics/nze/nzexpr.rs3
-rw-r--r--dhall/src/semantics/phase/normalize.rs8
-rw-r--r--dhall/src/syntax/ast/expr.rs22
5 files changed, 3 insertions, 112 deletions
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<Self> {
- 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<Self> {
- 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<Value> {
@@ -588,36 +546,6 @@ impl ValueKind<Value> {
pub(crate) fn from_builtin_env(b: Builtin, env: NzEnv) -> ValueKind<Value> {
ValueKind::AppliedBuiltin(b, vec![], vec![], env)
}
-
- fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
- 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<V> ValueKind<V> {
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<Self> {
- 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)),
diff --git a/dhall/src/syntax/ast/expr.rs b/dhall/src/syntax/ast/expr.rs
index 0da617b..424ac34 100644
--- a/dhall/src/syntax/ast/expr.rs
+++ b/dhall/src/syntax/ast/expr.rs
@@ -320,18 +320,6 @@ impl<E> Expr<E> {
}
}
-impl<Label: PartialEq + Clone> V<Label> {
- pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Option<Self> {
- let V(x, n) = var;
- let V(y, m) = self;
- Some(if x == y && n <= m {
- V(y.clone(), add_ui(*m, delta)?)
- } else {
- V(y.clone(), *m)
- })
- }
-}
-
pub fn trivial_result<T>(x: Result<T, !>) -> T {
match x {
Ok(x) => x,
@@ -339,16 +327,6 @@ pub fn trivial_result<T>(x: Result<T, !>) -> T {
}
}
-/// Add an isize to an usize
-/// Returns `None` on over/underflow
-fn add_ui(u: usize, i: isize) -> Option<usize> {
- Some(if i < 0 {
- u.checked_sub(i.checked_neg()? as usize)?
- } else {
- u.checked_add(i as usize)?
- })
-}
-
impl PartialEq for NaiveDouble {
fn eq(&self, other: &Self) -> bool {
self.0.to_bits() == other.0.to_bits()
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 17:49:15 +0000