diff options
author | Nadrieril | 2019-05-07 18:38:54 +0200 |
---|---|---|
committer | Nadrieril | 2019-05-07 18:38:54 +0200 |
commit | b3f00a827bcdd0fe406ccf8913cc5fb7cd6e0f2f (patch) | |
tree | 18d8326069fe94bcb03177c3375fcf453a370759 /dhall/src/core/thunk.rs | |
parent | 8cb3046e0920bf24d66c578b1a2b184c741b73fe (diff) |
Promote shift and subst_shift to traits
Diffstat (limited to 'dhall/src/core/thunk.rs')
-rw-r--r-- | dhall/src/core/thunk.rs | 82 |
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)), |