summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/normalize.rs39
-rw-r--r--dhall/src/typecheck.rs19
-rw-r--r--dhall_core/src/core.rs40
3 files changed, 43 insertions, 55 deletions
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index a023d38..f991a2e 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -38,10 +38,6 @@ impl<'a> Typed<'a> {
Normalized(internal, self.1)
}
- pub(crate) fn shift0(&self, delta: isize, x: &Label) -> Self {
- self.shift(delta, &V(x.clone(), 0))
- }
-
pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
Typed(self.0.shift(delta, var), self.1)
}
@@ -257,10 +253,6 @@ enum EnvItem {
}
impl EnvItem {
- fn shift0(&self, delta: isize, x: &Label) -> Self {
- self.shift(delta, &V(x.clone(), 0))
- }
-
fn shift(&self, delta: isize, var: &V<Label>) -> Self {
use EnvItem::*;
match self {
@@ -297,8 +289,8 @@ impl NormalizationContext {
fn skip(&self, x: &Label) -> Self {
NormalizationContext(Rc::new(
self.0
- .map(|_, e| e.shift0(1, x))
- .insert(x.clone(), EnvItem::Skip(V(x.clone(), 0))),
+ .map(|_, e| e.shift(1, &x.into()))
+ .insert(x.clone(), EnvItem::Skip(x.into())),
))
}
fn lookup(&self, var: &V<Label>) -> Value {
@@ -402,14 +394,14 @@ impl Value {
Value::ListConsClosure(n, None) => {
let a = n.normalize_to_expr();
// Avoid accidental capture of the new `x` variable
- let a1 = a.shift0(1, &"x".into());
+ let a1 = a.shift(1, &Label::from("x").into());
dhall::subexpr!(λ(x : a) -> λ(xs : List a1) -> [ x ] # xs)
}
Value::ListConsClosure(n, Some(v)) => {
let v = v.normalize_to_expr();
let a = n.normalize_to_expr();
// Avoid accidental capture of the new `xs` variable
- let v = v.shift0(1, &"xs".into());
+ let v = v.shift(1, &Label::from("xs").into());
dhall::subexpr!(λ(xs : List a) -> [ v ] # xs)
}
Value::NaturalSuccClosure => {
@@ -746,7 +738,7 @@ impl Value {
Value::Lam(x, t, e) => Value::Lam(
x.clone(),
t.shift(delta, var),
- e.shift(delta, &var.shift0(1, x)),
+ e.shift(delta, &var.shift(1, &x.into())),
),
Value::AppliedBuiltin(b, args) => Value::AppliedBuiltin(
*b,
@@ -763,7 +755,7 @@ impl Value {
Value::Pi(x, t, e) => Value::Pi(
x.clone(),
t.shift(delta, var),
- e.shift(delta, &var.shift0(1, x)),
+ e.shift(delta, &var.shift(1, &x.into())),
),
Value::Var(v) => Value::Var(v.shift(delta, var)),
Value::Const(c) => Value::Const(*c),
@@ -830,7 +822,7 @@ impl Value {
Value::PartialExpr(e) => Value::PartialExpr(Box::new(
e.map_ref_with_special_handling_of_binders(
|v| v.shift(delta, var),
- |x, v| v.shift(delta, &var.shift0(1, x)),
+ |x, v| v.shift(delta, &var.shift(1, &x.into())),
X::clone,
X::clone,
Label::clone,
@@ -849,7 +841,10 @@ impl Value {
Value::Lam(x, t, e) => Value::Lam(
x.clone(),
t.subst_shift(var, val),
- e.subst_shift(&var.shift0(1, x), &val.shift0(1, x)),
+ e.subst_shift(
+ &var.shift(1, &x.into()),
+ &val.shift(1, &x.into()),
+ ),
),
Value::AppliedBuiltin(b, args) => Value::AppliedBuiltin(
*b,
@@ -866,7 +861,10 @@ impl Value {
Value::Pi(x, t, e) => Value::Pi(
x.clone(),
t.subst_shift(var, val),
- e.subst_shift(&var.shift0(1, x), &val.shift0(1, x)),
+ e.subst_shift(
+ &var.shift(1, &x.into()),
+ &val.shift(1, &x.into()),
+ ),
),
Value::Var(v) if v == var => val.to_value().clone(),
Value::Var(v) => Value::Var(v.shift(-1, var)),
@@ -934,7 +932,12 @@ impl Value {
Value::PartialExpr(e) => Value::PartialExpr(Box::new(
e.map_ref_with_special_handling_of_binders(
|v| v.subst_shift(var, val),
- |x, v| v.subst_shift(&var.shift0(1, x), &val.shift0(1, x)),
+ |x, v| {
+ v.subst_shift(
+ &var.shift(1, &x.into()),
+ &val.shift(1, &x.into()),
+ )
+ },
X::clone,
X::clone,
Label::clone,
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 582930b..78538aa 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -46,9 +46,6 @@ impl<'a> Typed<'a> {
}
impl<'a> Normalized<'a> {
- fn shift0(&self, delta: isize, label: &Label) -> Self {
- self.shift(delta, &V(label.clone(), 0))
- }
fn shift(&self, delta: isize, var: &V<Label>) -> Self {
Normalized(self.0.shift(delta, var), self.1)
}
@@ -79,9 +76,6 @@ impl<'a> Type<'a> {
fn internal_whnf(&self) -> Option<Value> {
self.0.whnf()
}
- pub(crate) fn shift0(&self, delta: isize, label: &Label) -> Self {
- Type(self.0.shift0(delta, label))
- }
pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
Type(self.0.shift(delta, var))
}
@@ -164,9 +158,6 @@ impl<'a> TypeInternal<'a> {
_ => None,
}
}
- fn shift0(&self, delta: isize, label: &Label) -> Self {
- self.shift(delta, &V(label.clone(), 0))
- }
fn shift(&self, delta: isize, var: &V<Label>) -> Self {
use TypeInternal::*;
match self {
@@ -197,11 +188,11 @@ pub(crate) enum EnvItem {
}
impl EnvItem {
- fn shift0(&self, delta: isize, x: &Label) -> Self {
+ fn shift(&self, delta: isize, var: &V<Label>) -> Self {
use EnvItem::*;
match self {
- Type(v, e) => Type(v.shift0(delta, x), e.shift0(delta, x)),
- Value(e) => Value(e.shift0(delta, x)),
+ Type(v, e) => Type(v.shift(delta, var), e.shift(delta, var)),
+ Value(e) => Value(e.shift(delta, var)),
}
}
}
@@ -215,9 +206,9 @@ impl TypecheckContext {
}
pub(crate) fn insert_type(&self, x: &Label, t: Type<'static>) -> Self {
TypecheckContext(
- self.0.map(|_, e| e.shift0(1, x)).insert(
+ self.0.map(|_, e| e.shift(1, &x.into())).insert(
x.clone(),
- EnvItem::Type(V(x.clone(), 0), t.shift0(1, x)),
+ EnvItem::Type(x.into(), t.shift(1, &x.into())),
),
)
}
diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs
index ebd95e7..3db07dd 100644
--- a/dhall_core/src/core.rs
+++ b/dhall_core/src/core.rs
@@ -62,6 +62,18 @@ pub enum Const {
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct V<Label>(pub Label, pub usize);
+// This is only for the specific `Label` type, not generic
+impl From<Label> for V<Label> {
+ fn from(x: Label) -> V<Label> {
+ V(x, 0)
+ }
+}
+impl<'a> From<&'a Label> for V<Label> {
+ fn from(x: &'a Label) -> V<Label> {
+ V(x.clone(), 0)
+ }
+}
+
// Definition order must match precedence order for
// pretty-printing to work correctly
#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord)]
@@ -443,15 +455,11 @@ impl<N, E> SubExpr<N, E> {
ExprF::Var(v) => rc(ExprF::Var(v.shift(delta, var))),
_ => self.map_subexprs_with_special_handling_of_binders(
|e| e.shift(delta, var),
- |x: &Label, e| e.shift(delta, &var.shift0(1, x)),
+ |x: &Label, e| e.shift(delta, &var.shift(1, &x.into())),
),
}
}
- pub fn shift0(&self, delta: isize, label: &Label) -> Self {
- self.shift(delta, &V(label.clone(), 0))
- }
-
pub fn subst_shift(&self, var: &V<Label>, val: &Self) -> Self {
match self.as_ref() {
ExprF::Var(v) if v == var => val.clone(),
@@ -459,7 +467,10 @@ impl<N, E> SubExpr<N, E> {
_ => self.map_subexprs_with_special_handling_of_binders(
|e| e.subst_shift(var, val),
|x: &Label, e| {
- e.subst_shift(&var.shift0(1, x), &val.shift0(1, x))
+ e.subst_shift(
+ &var.shift(1, &x.into()),
+ &val.shift(1, &x.into()),
+ )
},
),
}
@@ -509,15 +520,6 @@ impl<Label: PartialEq + Clone> V<Label> {
V(y.clone(), *m)
}
}
-
- pub fn shift0(&self, delta: isize, x: &Label) -> Self {
- let V(y, m) = self;
- if x == y {
- V(y.clone(), add_ui(*m, delta))
- } else {
- V(y.clone(), *m)
- }
- }
}
/// `shift` is used by both normalization and type-checking to avoid variable
@@ -533,14 +535,6 @@ pub fn shift<N, E>(
in_expr.shift(delta, var)
}
-pub fn shift0<N, E>(
- delta: isize,
- label: &Label,
- in_expr: &SubExpr<N, E>,
-) -> SubExpr<N, E> {
- shift(delta, &V(label.clone(), 0), in_expr)
-}
-
pub fn shift0_multiple<N, E>(
deltas: &HashMap<Label, isize>,
in_expr: &SubExpr<N, E>,
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 08:36:02 +0000