From b3f00a827bcdd0fe406ccf8913cc5fb7cd6e0f2f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 7 May 2019 18:38:54 +0200 Subject: Promote shift and subst_shift to traits --- dhall/src/core/context.rs | 84 ++++++++++++++++++++++++-------------------- dhall/src/core/thunk.rs | 82 ++++++++++++++++++++++++------------------ dhall/src/core/value.rs | 10 ++++-- dhall/src/core/var.rs | 29 ++++++++++----- dhall/src/phase/mod.rs | 69 +++++++++++++++++++++--------------- dhall/src/phase/normalize.rs | 1 + 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); -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 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 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 for Thunk { + fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { + self.0.borrow().subst_shift(var, val).into_thunk() + } +} + +impl Subst 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 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 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: Shift { + fn subst_shift(&self, var: &AlphaVar, val: &T) -> Self; +} + impl AlphaVar { pub(crate) fn to_var(&self, alpha: bool) -> V