summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/core/thunk.rs35
-rw-r--r--dhall/src/core/value.rs168
-rw-r--r--dhall/src/core/var.rs175
3 files changed, 186 insertions, 192 deletions
diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs
index e315a90..b6358ef 100644
--- a/dhall/src/core/thunk.rs
+++ b/dhall/src/core/thunk.rs
@@ -266,24 +266,16 @@ impl TypedThunk {
impl Shift for Thunk {
fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
- Some(
- self.0
- .borrow()
- .shift(delta, var)?
- .into_thunk(self.1.shift(delta, var)?),
- )
+ Some(Thunk(self.0.shift(delta, var)?, self.1.shift(delta, var)?))
}
}
impl Shift for ThunkInternal {
fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
Some(match self {
- ThunkInternal::PartialExpr(e) => ThunkInternal::PartialExpr(
- e.traverse_ref_with_special_handling_of_binders(
- |v| Ok(v.shift(delta, var)?),
- |x, v| Ok(v.shift(delta, &var.under_binder(x))?),
- )?,
- ),
+ ThunkInternal::PartialExpr(e) => {
+ ThunkInternal::PartialExpr(e.shift(delta, var)?)
+ }
ThunkInternal::ValueF(m, v) => {
ThunkInternal::ValueF(*m, v.shift(delta, var)?)
}
@@ -301,27 +293,16 @@ impl Shift for TypedThunk {
impl Subst<Typed> for Thunk {
fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
- self.0
- .borrow()
- .subst_shift(var, val)
- .into_thunk(self.1.subst_shift(var, val))
+ Thunk(self.0.subst_shift(var, val), self.1.subst_shift(var, val))
}
}
impl Subst<Typed> for ThunkInternal {
fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
match self {
- ThunkInternal::PartialExpr(e) => ThunkInternal::PartialExpr(
- e.map_ref_with_special_handling_of_binders(
- |v| v.subst_shift(var, val),
- |x, v| {
- v.subst_shift(
- &var.under_binder(x),
- &val.under_binder(x),
- )
- },
- ),
- ),
+ ThunkInternal::PartialExpr(e) => {
+ ThunkInternal::PartialExpr(e.subst_shift(var, val))
+ }
ThunkInternal::ValueF(_, v) => {
// The resulting value may not stay in normal form after substitution
ThunkInternal::ValueF(WHNF, v.subst_shift(var, val))
diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index 0f2ef00..da70118 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -287,12 +287,9 @@ impl Shift for ValueF {
t.shift(delta, var)?,
e.shift(delta, &var.under_binder(x))?,
),
- ValueF::AppliedBuiltin(b, args) => ValueF::AppliedBuiltin(
- *b,
- args.iter()
- .map(|v| Ok(v.shift(delta, var)?))
- .collect::<Result<_, _>>()?,
- ),
+ ValueF::AppliedBuiltin(b, args) => {
+ ValueF::AppliedBuiltin(*b, args.shift(delta, var)?)
+ }
ValueF::Pi(x, t, e) => ValueF::Pi(
x.clone(),
t.shift(delta, var)?,
@@ -313,80 +310,27 @@ impl Shift for ValueF {
ValueF::EmptyListLit(tth) => {
ValueF::EmptyListLit(tth.shift(delta, var)?)
}
- ValueF::NEListLit(elts) => ValueF::NEListLit(
- elts.iter()
- .map(|v| Ok(v.shift(delta, var)?))
- .collect::<Result<_, _>>()?,
- ),
- ValueF::RecordLit(kvs) => ValueF::RecordLit(
- kvs.iter()
- .map(|(k, v)| Ok((k.clone(), v.shift(delta, var)?)))
- .collect::<Result<_, _>>()?,
- ),
- ValueF::RecordType(kvs) => ValueF::RecordType(
- kvs.iter()
- .map(|(k, v)| Ok((k.clone(), v.shift(delta, var)?)))
- .collect::<Result<_, _>>()?,
- ),
- ValueF::UnionType(kts) => ValueF::UnionType(
- kts.iter()
- .map(|(k, v)| {
- Ok((
- k.clone(),
- v.as_ref()
- .map(|v| Ok(v.shift(delta, var)?))
- .transpose()?,
- ))
- })
- .collect::<Result<_, _>>()?,
- ),
- ValueF::UnionConstructor(x, kts) => ValueF::UnionConstructor(
- x.clone(),
- kts.iter()
- .map(|(k, v)| {
- Ok((
- k.clone(),
- v.as_ref()
- .map(|v| Ok(v.shift(delta, var)?))
- .transpose()?,
- ))
- })
- .collect::<Result<_, _>>()?,
- ),
+ ValueF::NEListLit(elts) => {
+ ValueF::NEListLit(elts.shift(delta, var)?)
+ }
+ ValueF::RecordLit(kvs) => ValueF::RecordLit(kvs.shift(delta, var)?),
+ ValueF::RecordType(kvs) => {
+ ValueF::RecordType(kvs.shift(delta, var)?)
+ }
+ ValueF::UnionType(kts) => ValueF::UnionType(kts.shift(delta, var)?),
+ ValueF::UnionConstructor(x, kts) => {
+ ValueF::UnionConstructor(x.clone(), kts.shift(delta, var)?)
+ }
ValueF::UnionLit(x, v, kts) => ValueF::UnionLit(
x.clone(),
v.shift(delta, var)?,
- kts.iter()
- .map(|(k, v)| {
- Ok((
- k.clone(),
- v.as_ref()
- .map(|v| Ok(v.shift(delta, var)?))
- .transpose()?,
- ))
- })
- .collect::<Result<_, _>>()?,
- ),
- ValueF::TextLit(elts) => ValueF::TextLit(
- elts.iter()
- .map(|contents| {
- use InterpolatedTextContents::{Expr, Text};
- Ok(match contents {
- Expr(th) => Expr(th.shift(delta, var)?),
- Text(s) => Text(s.clone()),
- })
- })
- .collect::<Result<_, _>>()?,
+ kts.shift(delta, var)?,
),
+ ValueF::TextLit(elts) => ValueF::TextLit(elts.shift(delta, var)?),
ValueF::Equivalence(x, y) => {
ValueF::Equivalence(x.shift(delta, var)?, y.shift(delta, var)?)
}
- ValueF::PartialExpr(e) => ValueF::PartialExpr(
- e.traverse_ref_with_special_handling_of_binders(
- |v| Ok(v.shift(delta, var)?),
- |x, v| Ok(v.shift(delta, &var.under_binder(x))?),
- )?,
- ),
+ ValueF::PartialExpr(e) => ValueF::PartialExpr(e.shift(delta, var)?),
})
}
}
@@ -395,32 +339,17 @@ impl Subst<Typed> for ValueF {
fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
match self {
// Retry normalizing since substituting may allow progress
- ValueF::AppliedBuiltin(b, args) => apply_builtin(
- *b,
- args.iter().map(|v| v.subst_shift(var, val)).collect(),
- ),
+ ValueF::AppliedBuiltin(b, args) => {
+ apply_builtin(*b, args.subst_shift(var, val))
+ }
// Retry normalizing since substituting may allow progress
ValueF::PartialExpr(e) => {
- normalize_one_layer(e.map_ref_with_special_handling_of_binders(
- |v| v.subst_shift(var, val),
- |x, v| {
- v.subst_shift(
- &var.under_binder(x),
- &val.under_binder(x),
- )
- },
- ))
+ normalize_one_layer(e.subst_shift(var, val))
}
// Retry normalizing since substituting may allow progress
- ValueF::TextLit(elts) => {
- ValueF::TextLit(squash_textlit(elts.iter().map(|contents| {
- use InterpolatedTextContents::{Expr, Text};
- match contents {
- Expr(th) => Expr(th.subst_shift(var, val)),
- Text(s) => Text(s.clone()),
- }
- })))
- }
+ ValueF::TextLit(elts) => ValueF::TextLit(squash_textlit(
+ elts.iter().map(|contents| contents.subst_shift(var, val)),
+ )),
ValueF::Lam(x, t, e) => ValueF::Lam(
x.clone(),
t.subst_shift(var, val),
@@ -447,42 +376,25 @@ impl Subst<Typed> for ValueF {
ValueF::EmptyListLit(tth) => {
ValueF::EmptyListLit(tth.subst_shift(var, val))
}
- ValueF::NEListLit(elts) => ValueF::NEListLit(
- elts.iter().map(|v| v.subst_shift(var, val)).collect(),
- ),
- ValueF::RecordLit(kvs) => ValueF::RecordLit(
- kvs.iter()
- .map(|(k, v)| (k.clone(), v.subst_shift(var, val)))
- .collect(),
- ),
- ValueF::RecordType(kvs) => ValueF::RecordType(
- kvs.iter()
- .map(|(k, v)| (k.clone(), v.subst_shift(var, val)))
- .collect(),
- ),
- ValueF::UnionType(kts) => ValueF::UnionType(
- kts.iter()
- .map(|(k, v)| {
- (k.clone(), v.as_ref().map(|v| v.subst_shift(var, val)))
- })
- .collect(),
- ),
- ValueF::UnionConstructor(x, kts) => ValueF::UnionConstructor(
- x.clone(),
- kts.iter()
- .map(|(k, v)| {
- (k.clone(), v.as_ref().map(|v| v.subst_shift(var, val)))
- })
- .collect(),
- ),
+ ValueF::NEListLit(elts) => {
+ ValueF::NEListLit(elts.subst_shift(var, val))
+ }
+ ValueF::RecordLit(kvs) => {
+ ValueF::RecordLit(kvs.subst_shift(var, val))
+ }
+ ValueF::RecordType(kvs) => {
+ ValueF::RecordType(kvs.subst_shift(var, val))
+ }
+ ValueF::UnionType(kts) => {
+ ValueF::UnionType(kts.subst_shift(var, val))
+ }
+ ValueF::UnionConstructor(x, kts) => {
+ ValueF::UnionConstructor(x.clone(), kts.subst_shift(var, val))
+ }
ValueF::UnionLit(x, v, kts) => ValueF::UnionLit(
x.clone(),
v.subst_shift(var, val),
- kts.iter()
- .map(|(k, v)| {
- (k.clone(), v.as_ref().map(|v| v.subst_shift(var, val)))
- })
- .collect(),
+ kts.subst_shift(var, val),
),
ValueF::Equivalence(x, y) => ValueF::Equivalence(
x.subst_shift(var, val),
diff --git a/dhall/src/core/var.rs b/dhall/src/core/var.rs
index 3af12ec..8d02171 100644
--- a/dhall/src/core/var.rs
+++ b/dhall/src/core/var.rs
@@ -92,43 +92,6 @@ impl Shift for AlphaVar {
}
}
-impl Shift for () {
- fn shift(&self, _delta: isize, _var: &AlphaVar) -> Option<Self> {
- Some(())
- }
-}
-
-impl<T: Shift> Shift for Option<T> {
- fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
- Some(match self {
- None => None,
- Some(x) => Some(x.shift(delta, var)?),
- })
- }
-}
-
-impl<T: Shift> Shift for Box<T> {
- fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
- Some(Box::new(self.as_ref().shift(delta, var)?))
- }
-}
-
-impl<S> Subst<S> for () {
- fn subst_shift(&self, _var: &AlphaVar, _val: &S) -> Self {}
-}
-
-impl<S, T: Subst<S>> Subst<S> for Option<T> {
- fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self {
- self.as_ref().map(|x| x.subst_shift(var, val))
- }
-}
-
-impl<S, T: Subst<S>> Subst<S> for Box<T> {
- fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self {
- Box::new(self.as_ref().subst_shift(var, val))
- }
-}
-
/// Equality up to alpha-equivalence
impl std::cmp::PartialEq for AlphaVar {
fn eq(&self, other: &Self) -> bool {
@@ -188,3 +151,141 @@ impl From<AlphaLabel> for Label {
x.0
}
}
+impl Shift for () {
+ fn shift(&self, _delta: isize, _var: &AlphaVar) -> Option<Self> {
+ Some(())
+ }
+}
+
+impl<T: Shift> Shift for Option<T> {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ Some(match self {
+ None => None,
+ Some(x) => Some(x.shift(delta, var)?),
+ })
+ }
+}
+
+impl<T: Shift> Shift for Box<T> {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ Some(Box::new(self.as_ref().shift(delta, var)?))
+ }
+}
+
+impl<T: Shift> Shift for std::rc::Rc<T> {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ Some(std::rc::Rc::new(self.as_ref().shift(delta, var)?))
+ }
+}
+
+impl<T: Shift> Shift for std::cell::RefCell<T> {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ Some(std::cell::RefCell::new(self.borrow().shift(delta, var)?))
+ }
+}
+
+impl<T: Shift, E: Clone> Shift for dhall_syntax::ExprF<T, E> {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ Some(self.traverse_ref_with_special_handling_of_binders(
+ |v| Ok(v.shift(delta, var)?),
+ |x, v| Ok(v.shift(delta, &var.under_binder(x))?),
+ )?)
+ }
+}
+
+impl<T: Shift> Shift for Vec<T> {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ Some(
+ self.iter()
+ .map(|v| Ok(v.shift(delta, var)?))
+ .collect::<Result<_, _>>()?,
+ )
+ }
+}
+
+impl<K, T: Shift> Shift for HashMap<K, T>
+where
+ K: Clone + std::hash::Hash + Eq,
+{
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ Some(
+ self.iter()
+ .map(|(k, v)| Ok((k.clone(), v.shift(delta, var)?)))
+ .collect::<Result<_, _>>()?,
+ )
+ }
+}
+
+impl<T: Shift> Shift for dhall_syntax::InterpolatedTextContents<T> {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ use dhall_syntax::InterpolatedTextContents::{Expr, Text};
+ Some(match self {
+ Expr(x) => Expr(x.shift(delta, var)?),
+ Text(s) => Text(s.clone()),
+ })
+ }
+}
+
+impl<S> Subst<S> for () {
+ fn subst_shift(&self, _var: &AlphaVar, _val: &S) -> Self {}
+}
+
+impl<S, T: Subst<S>> Subst<S> for Option<T> {
+ fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self {
+ self.as_ref().map(|x| x.subst_shift(var, val))
+ }
+}
+
+impl<S, T: Subst<S>> Subst<S> for Box<T> {
+ fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self {
+ Box::new(self.as_ref().subst_shift(var, val))
+ }
+}
+
+impl<S, T: Subst<S>> Subst<S> for std::rc::Rc<T> {
+ fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self {
+ std::rc::Rc::new(self.as_ref().subst_shift(var, val))
+ }
+}
+
+impl<S, T: Subst<S>> Subst<S> for std::cell::RefCell<T> {
+ fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self {
+ std::cell::RefCell::new(self.borrow().subst_shift(var, val))
+ }
+}
+
+impl<S: Shift, T: Subst<S>, E: Clone> Subst<S> for dhall_syntax::ExprF<T, E> {
+ fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self {
+ self.map_ref_with_special_handling_of_binders(
+ |v| v.subst_shift(var, val),
+ |x, v| v.subst_shift(&var.under_binder(x), &val.under_binder(x)),
+ )
+ }
+}
+
+impl<S, T: Subst<S>> Subst<S> for Vec<T> {
+ fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self {
+ self.iter().map(|v| v.subst_shift(var, val)).collect()
+ }
+}
+
+impl<S, T: Subst<S>> Subst<S> for dhall_syntax::InterpolatedTextContents<T> {
+ fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self {
+ use dhall_syntax::InterpolatedTextContents::{Expr, Text};
+ match self {
+ Expr(x) => Expr(x.subst_shift(var, val)),
+ Text(s) => Text(s.clone()),
+ }
+ }
+}
+
+impl<S, K, T: Subst<S>> Subst<S> for HashMap<K, T>
+where
+ K: Clone + std::hash::Hash + Eq,
+{
+ fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self {
+ self.iter()
+ .map(|(k, v)| (k.clone(), v.subst_shift(var, val)))
+ .collect()
+ }
+}
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-28 16:05:50 +0000