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 | |
parent | 8cb3046e0920bf24d66c578b1a2b184c741b73fe (diff) |
Promote shift and subst_shift to traits
-rw-r--r-- | dhall/src/core/context.rs | 84 | ||||
-rw-r--r-- | dhall/src/core/thunk.rs | 82 | ||||
-rw-r--r-- | dhall/src/core/value.rs | 10 | ||||
-rw-r--r-- | dhall/src/core/var.rs | 29 | ||||
-rw-r--r-- | dhall/src/phase/mod.rs | 69 | ||||
-rw-r--r-- | dhall/src/phase/normalize.rs | 1 | ||||
-rw-r--r-- | dhall/src/phase/typecheck.rs | 1 |
7 files changed, 161 insertions, 115 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 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)), diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 4c71778..412fe11 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -7,7 +7,7 @@ use dhall_syntax::{ }; use crate::core::thunk::{Thunk, TypeThunk}; -use crate::core::var::{AlphaLabel, AlphaVar}; +use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; use crate::phase::normalize::{ apply_builtin, normalize_one_layer, squash_textlit, OutputSubExpr, }; @@ -316,8 +316,10 @@ impl Value { pub(crate) fn from_builtin(b: Builtin) -> Value { Value::AppliedBuiltin(b, vec![]) } +} - pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Self { +impl Shift for Value { + fn shift(&self, delta: isize, var: &AlphaVar) -> Self { match self { Value::Lam(x, t, e) => Value::Lam( x.clone(), @@ -413,8 +415,10 @@ impl Value { } } } +} - pub(crate) fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { +impl Subst<Typed> for Value { + fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { match self { // Retry normalizing since substituting may allow progress Value::AppliedBuiltin(b, args) => apply_builtin( diff --git a/dhall/src/core/var.rs b/dhall/src/core/var.rs index e431fc2..21bc06b 100644 --- a/dhall/src/core/var.rs +++ b/dhall/src/core/var.rs @@ -14,6 +14,14 @@ pub(crate) struct AlphaVar { #[derive(Debug, Clone, Eq)] pub(crate) struct AlphaLabel(Label); +pub(crate) trait Shift { + fn shift(&self, delta: isize, var: &AlphaVar) -> Self; +} + +pub(crate) trait Subst<T>: Shift { + fn subst_shift(&self, var: &AlphaVar, val: &T) -> Self; +} + impl AlphaVar { pub(crate) fn to_var(&self, alpha: bool) -> V<Label> { match (alpha, &self.alpha) { @@ -27,15 +35,6 @@ impl AlphaVar { alpha: None, } } - pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Self { - AlphaVar { - normal: self.normal.shift(delta, &var.normal), - alpha: match (&self.alpha, &var.alpha) { - (Some(x), Some(v)) => Some(x.shift(delta, v)), - _ => None, - }, - } - } } impl AlphaLabel { @@ -51,6 +50,18 @@ impl AlphaLabel { } } +impl Shift for AlphaVar { + fn shift(&self, delta: isize, var: &AlphaVar) -> Self { + AlphaVar { + normal: self.normal.shift(delta, &var.normal), + alpha: match (&self.alpha, &var.alpha) { + (Some(x), Some(v)) => Some(x.shift(delta, v)), + _ => None, + }, + } + } +} + impl std::cmp::PartialEq for AlphaVar { fn eq(&self, other: &Self) -> bool { match (&self.alpha, &other.alpha) { diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs index 97b8083..5c910bc 100644 --- a/dhall/src/phase/mod.rs +++ b/dhall/src/phase/mod.rs @@ -7,7 +7,7 @@ use dhall_syntax::{Const, Import, Span, SubExpr, X}; use crate::core::context::TypecheckContext; use crate::core::thunk::Thunk; use crate::core::value::Value; -use crate::core::var::AlphaVar; +use crate::core::var::{AlphaVar, Shift, Subst}; use crate::error::{Error, ImportError, TypeError, TypeMessage}; use resolve::ImportRoot; @@ -168,26 +168,6 @@ impl Typed { Typed::Const(c) => Ok(Cow::Owned(type_of_const(*c)?)), } } - - pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Self { - match self { - Typed::Value(th, t) => Typed::Value( - th.shift(delta, var), - t.as_ref().map(|x| x.shift(delta, var)), - ), - Typed::Const(c) => Typed::Const(*c), - } - } - - pub(crate) fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { - match self { - Typed::Value(th, t) => Typed::Value( - th.subst_shift(var, val), - t.as_ref().map(|x| x.subst_shift(var, val)), - ), - Typed::Const(c) => Typed::Const(*c), - } - } } impl Type { @@ -226,13 +206,6 @@ impl Type { pub(crate) fn from_const(c: Const) -> Self { Type(Box::new(Typed::from_const(c))) } - - pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Self { - Type(Box::new(self.0.shift(delta, var))) - } - pub(crate) fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { - Type(Box::new(self.0.subst_shift(var, val))) - } } impl Normalized { @@ -259,12 +232,50 @@ impl Normalized { pub(crate) fn get_type(&self) -> Result<Cow<'_, Type>, TypeError> { self.0.get_type() } +} + +impl Shift for Typed { + fn shift(&self, delta: isize, var: &AlphaVar) -> Self { + match self { + Typed::Value(th, t) => Typed::Value( + th.shift(delta, var), + t.as_ref().map(|x| x.shift(delta, var)), + ), + Typed::Const(c) => Typed::Const(*c), + } + } +} + +impl Shift for Type { + fn shift(&self, delta: isize, var: &AlphaVar) -> Self { + Type(Box::new(self.0.shift(delta, var))) + } +} - pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Self { +impl Shift for Normalized { + fn shift(&self, delta: isize, var: &AlphaVar) -> Self { Normalized(self.0.shift(delta, var)) } } +impl Subst<Typed> for Typed { + fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { + match self { + Typed::Value(th, t) => Typed::Value( + th.subst_shift(var, val), + t.as_ref().map(|x| x.subst_shift(var, val)), + ), + Typed::Const(c) => Typed::Const(*c), + } + } +} + +impl Subst<Typed> for Type { + fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { + Type(Box::new(self.0.subst_shift(var, val))) + } +} + macro_rules! derive_traits_for_wrapper_struct { ($ty:ident) => { impl std::cmp::PartialEq for $ty { diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs index 5dfcfb6..e9fc570 100644 --- a/dhall/src/phase/normalize.rs +++ b/dhall/src/phase/normalize.rs @@ -5,6 +5,7 @@ use dhall_syntax::{BinOp, Builtin, ExprF, InterpolatedTextContents, Label, X}; use crate::core::context::NormalizationContext; use crate::core::thunk::{Thunk, TypeThunk}; use crate::core::value::Value; +use crate::core::var::Subst; use crate::phase::{NormalizedSubExpr, ResolvedSubExpr, Typed}; pub(crate) type InputSubExpr = ResolvedSubExpr; diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index 32c1531..f8ee559 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -11,6 +11,7 @@ use dhall_syntax::{ use crate::core::context::{NormalizationContext, TypecheckContext}; use crate::core::thunk::{Thunk, TypeThunk}; use crate::core::value::Value; +use crate::core::var::Subst; use crate::error::{TypeError, TypeMessage}; use crate::phase::{Normalized, Resolved, Type, Typed}; |