diff options
author | Nadrieril | 2019-08-16 22:33:16 +0200 |
---|---|---|
committer | Nadrieril | 2019-08-16 22:33:16 +0200 |
commit | cc0c6cc420ca8019665e745797758c997cc35358 (patch) | |
tree | 38afd8786d959d4cc244ca048b94c3f069e3d97e | |
parent | 961dbc0e9d52691de590568c01a22d28c04fe2f5 (diff) |
Use generic Shift/Subst impls
Diffstat (limited to '')
-rw-r--r-- | dhall/src/core/thunk.rs | 35 | ||||
-rw-r--r-- | dhall/src/core/value.rs | 168 | ||||
-rw-r--r-- | dhall/src/core/var.rs | 175 |
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() + } +} |