summaryrefslogtreecommitdiff
path: root/dhall/src/core/context.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/context.rs
parent8cb3046e0920bf24d66c578b1a2b184c741b73fe (diff)
Promote shift and subst_shift to traits
Diffstat (limited to 'dhall/src/core/context.rs')
-rw-r--r--dhall/src/core/context.rs84
1 files changed, 45 insertions, 39 deletions
diff --git a/dhall/src/core/context.rs b/dhall/src/core/context.rs
index 0466058..e693317 100644
--- a/dhall/src/core/context.rs
+++ b/dhall/src/core/context.rs
@@ -6,7 +6,7 @@ use dhall_syntax::{Label, V};
use crate::core::thunk::Thunk;
use crate::core::value::Value;
-use crate::core::var::AlphaVar;
+use crate::core::var::{AlphaVar, Shift, Subst};
use crate::phase::{Normalized, Type, Typed};
#[derive(Debug, Clone)]
@@ -27,24 +27,6 @@ pub(crate) enum TyEnvItem {
#[derive(Debug, Clone)]
pub(crate) struct TypecheckContext(pub(crate) Context<Label, TyEnvItem>);
-impl NzEnvItem {
- pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
- use NzEnvItem::*;
- match self {
- Thunk(e) => Thunk(e.shift(delta, var)),
- Skip(v) => Skip(v.shift(delta, var)),
- }
- }
-
- pub(crate) fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
- match self {
- NzEnvItem::Thunk(e) => NzEnvItem::Thunk(e.subst_shift(var, val)),
- NzEnvItem::Skip(v) if v == var => NzEnvItem::Thunk(val.to_thunk()),
- NzEnvItem::Skip(v) => NzEnvItem::Skip(v.shift(-1, var)),
- }
- }
-}
-
impl NormalizationContext {
pub(crate) fn new() -> Self {
NormalizationContext(Rc::new(Context::new()))
@@ -79,26 +61,6 @@ impl NormalizationContext {
}
NormalizationContext(Rc::new(ctx))
}
-
- pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
- NormalizationContext(Rc::new(self.0.map(|_, e| e.shift(delta, var))))
- }
-
- pub(crate) fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
- NormalizationContext(Rc::new(
- self.0.map(|_, e| e.subst_shift(var, val)),
- ))
- }
-}
-
-impl TyEnvItem {
- fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
- use TyEnvItem::*;
- match self {
- Type(v, e) => Type(v.shift(delta, var), e.shift(delta, var)),
- Value(e) => Value(e.shift(delta, var)),
- }
- }
}
impl TypecheckContext {
@@ -127,6 +89,50 @@ impl TypecheckContext {
}
}
+impl Shift for NzEnvItem {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
+ use NzEnvItem::*;
+ match self {
+ Thunk(e) => Thunk(e.shift(delta, var)),
+ Skip(v) => Skip(v.shift(delta, var)),
+ }
+ }
+}
+
+impl Shift for NormalizationContext {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
+ NormalizationContext(Rc::new(self.0.map(|_, e| e.shift(delta, var))))
+ }
+}
+
+impl Shift for TyEnvItem {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
+ use TyEnvItem::*;
+ match self {
+ Type(v, e) => Type(v.shift(delta, var), e.shift(delta, var)),
+ Value(e) => Value(e.shift(delta, var)),
+ }
+ }
+}
+
+impl Subst<Typed> for NzEnvItem {
+ fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
+ match self {
+ NzEnvItem::Thunk(e) => NzEnvItem::Thunk(e.subst_shift(var, val)),
+ NzEnvItem::Skip(v) if v == var => NzEnvItem::Thunk(val.to_thunk()),
+ NzEnvItem::Skip(v) => NzEnvItem::Skip(v.shift(-1, var)),
+ }
+ }
+}
+
+impl Subst<Typed> for NormalizationContext {
+ fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
+ NormalizationContext(Rc::new(
+ self.0.map(|_, e| e.subst_shift(var, val)),
+ ))
+ }
+}
+
impl PartialEq for TypecheckContext {
fn eq(&self, _: &Self) -> bool {
// don't count contexts when comparing stuff