summaryrefslogtreecommitdiff
path: root/dhall/src/core/thunk.rs
diff options
context:
space:
mode:
authorNadrieril2019-05-07 18:38:54 +0200
committerNadrieril2019-05-07 18:38:54 +0200
commitb3f00a827bcdd0fe406ccf8913cc5fb7cd6e0f2f (patch)
tree18d8326069fe94bcb03177c3375fcf453a370759 /dhall/src/core/thunk.rs
parent8cb3046e0920bf24d66c578b1a2b184c741b73fe (diff)
Promote shift and subst_shift to traits
Diffstat (limited to 'dhall/src/core/thunk.rs')
-rw-r--r--dhall/src/core/thunk.rs82
1 files changed, 47 insertions, 35 deletions
diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs
index 14ef710..b3817dc 100644
--- a/dhall/src/core/thunk.rs
+++ b/dhall/src/core/thunk.rs
@@ -4,7 +4,7 @@ use std::rc::Rc;
use crate::core::context::NormalizationContext;
use crate::core::context::TypecheckContext;
use crate::core::value::Value;
-use crate::core::var::AlphaVar;
+use crate::core::var::{AlphaVar, Shift, Subst};
use crate::error::TypeError;
use crate::phase::normalize::{
apply_any, normalize_whnf, InputSubExpr, OutputSubExpr,
@@ -93,30 +93,6 @@ impl ThunkInternal {
ThunkInternal::Value(NF, v) => v,
}
}
-
- fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
- match self {
- ThunkInternal::Unnormalized(ctx, e) => {
- ThunkInternal::Unnormalized(ctx.shift(delta, var), e.clone())
- }
- ThunkInternal::Value(m, v) => {
- ThunkInternal::Value(*m, v.shift(delta, var))
- }
- }
- }
-
- fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
- match self {
- ThunkInternal::Unnormalized(ctx, e) => ThunkInternal::Unnormalized(
- ctx.subst_shift(var, val),
- e.clone(),
- ),
- ThunkInternal::Value(_, v) => {
- // The resulting value may not stay in normal form after substitution
- ThunkInternal::Value(WHNF, v.subst_shift(var, val))
- }
- }
- }
}
impl Thunk {
@@ -204,14 +180,6 @@ impl Thunk {
pub(crate) fn app_thunk(&self, th: Thunk) -> Value {
apply_any(self.clone(), th)
}
-
- pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
- self.0.borrow().shift(delta, var).into_thunk()
- }
-
- pub(crate) fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
- self.0.borrow().subst_shift(var, val).into_thunk()
- }
}
impl TypeThunk {
@@ -267,15 +235,59 @@ impl TypeThunk {
) -> OutputSubExpr {
self.normalize_nf().normalize_to_expr_maybe_alpha(alpha)
}
+}
+
+impl Shift for Thunk {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
+ self.0.borrow().shift(delta, var).into_thunk()
+ }
+}
+
+impl Shift for ThunkInternal {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
+ match self {
+ ThunkInternal::Unnormalized(ctx, e) => {
+ ThunkInternal::Unnormalized(ctx.shift(delta, var), e.clone())
+ }
+ ThunkInternal::Value(m, v) => {
+ ThunkInternal::Value(*m, v.shift(delta, var))
+ }
+ }
+ }
+}
- pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
+impl Shift for TypeThunk {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
match self {
TypeThunk::Thunk(th) => TypeThunk::Thunk(th.shift(delta, var)),
TypeThunk::Type(t) => TypeThunk::Type(t.shift(delta, var)),
}
}
+}
- pub(crate) fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
+impl Subst<Typed> for Thunk {
+ fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
+ self.0.borrow().subst_shift(var, val).into_thunk()
+ }
+}
+
+impl Subst<Typed> for ThunkInternal {
+ fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
+ match self {
+ ThunkInternal::Unnormalized(ctx, e) => ThunkInternal::Unnormalized(
+ ctx.subst_shift(var, val),
+ e.clone(),
+ ),
+ ThunkInternal::Value(_, v) => {
+ // The resulting value may not stay in normal form after substitution
+ ThunkInternal::Value(WHNF, v.subst_shift(var, val))
+ }
+ }
+ }
+}
+
+impl Subst<Typed> for TypeThunk {
+ fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
match self {
TypeThunk::Thunk(th) => TypeThunk::Thunk(th.subst_shift(var, val)),
TypeThunk::Type(t) => TypeThunk::Type(t.subst_shift(var, val)),