diff options
author | Nadrieril | 2020-01-17 11:03:40 +0000 |
---|---|---|
committer | Nadrieril | 2020-01-17 11:18:57 +0000 |
commit | 72d1e3c339cf550fa5af9981af6078a813feb80a (patch) | |
tree | b6dc162bf0af9ce8e2cd7dbe0443b302ef071f0e | |
parent | f7a8d967b02bc20c093d501746ed3de53cc7da13 (diff) |
Remove Shift/Subst traits
Diffstat (limited to '')
-rw-r--r-- | dhall/src/semantics/core/context.rs | 105 | ||||
-rw-r--r-- | dhall/src/semantics/core/value.rs | 158 | ||||
-rw-r--r-- | dhall/src/semantics/core/var.rs | 63 | ||||
-rw-r--r-- | dhall/src/semantics/phase/mod.rs | 13 | ||||
-rw-r--r-- | dhall/src/semantics/phase/normalize.rs | 1 | ||||
-rw-r--r-- | dhall/src/semantics/phase/typecheck.rs | 2 |
6 files changed, 115 insertions, 227 deletions
diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs index 3a7930e..16ea48f 100644 --- a/dhall/src/semantics/core/context.rs +++ b/dhall/src/semantics/core/context.rs @@ -3,7 +3,7 @@ use std::collections::HashMap; use crate::error::TypeError; use crate::semantics::core::value::Value; use crate::semantics::core::value::ValueKind; -use crate::semantics::core::var::{AlphaVar, Binder, Shift, Subst}; +use crate::semantics::core::var::{AlphaVar, Binder}; use crate::syntax::{Label, V}; #[derive(Debug, Clone)] @@ -17,6 +17,27 @@ pub(crate) struct TyCtx { ctx: Vec<(Binder, CtxItem)>, } +impl CtxItem { + fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { + Some(match self { + CtxItem::Kept(v, t) => { + CtxItem::Kept(v.shift(delta, var)?, t.shift(delta, var)?) + } + CtxItem::Replaced(e) => CtxItem::Replaced(e.shift(delta, var)?), + }) + } + fn under_multiple_binders(&self, shift_map: &HashMap<Label, usize>) -> Self + where + Self: Clone, + { + let mut v = self.clone(); + for (x, n) in shift_map { + v = v.shift(*n as isize, &x.into()).unwrap(); + } + v + } +} + impl TyCtx { pub fn new() -> Self { TyCtx { ctx: Vec::new() } @@ -65,86 +86,4 @@ impl TyCtx { pub fn new_binder(&self, l: &Label) -> Binder { Binder::new(l.clone()) } - - /// Given a var that makes sense in the current context, map the given function in such a way - /// that the passed variable always makes sense in the context of the passed item. - /// Once we pass the variable definition, the variable doesn't make sense anymore so we just - /// copy the remaining items. - fn do_with_var<E>( - &self, - var: &AlphaVar, - mut f: impl FnMut(&AlphaVar, &CtxItem) -> Result<CtxItem, E>, - ) -> Result<Self, E> { - let mut vec = Vec::new(); - vec.reserve(self.ctx.len()); - let mut var = var.clone(); - let mut iter = self.ctx.iter().rev(); - for (l, i) in iter.by_ref() { - vec.push((l.clone(), f(&var, i)?)); - if let CtxItem::Kept(_, _) = i { - match var.over_binder(l) { - None => break, - Some(newvar) => var = newvar, - }; - } - } - for (l, i) in iter { - vec.push((l.clone(), (*i).clone())); - } - vec.reverse(); - Ok(self.with_vec(vec)) - } - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - if delta < 0 { - Some(self.do_with_var(var, |var, i| Ok(i.shift(delta, &var)?))?) - } else { - Some( - self.with_vec( - self.ctx - .iter() - .map(|(l, i)| Ok((l.clone(), i.shift(delta, &var)?))) - .collect::<Result<_, _>>()?, - ), - ) - } - } - fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { - self.do_with_var(var, |var, i| Ok::<_, !>(i.subst_shift(&var, val))) - .unwrap() - } -} - -impl Shift for CtxItem { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some(match self { - CtxItem::Kept(v, t) => { - CtxItem::Kept(v.shift(delta, var)?, t.shift(delta, var)?) - } - CtxItem::Replaced(e) => CtxItem::Replaced(e.shift(delta, var)?), - }) - } -} - -impl Shift for TyCtx { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - self.shift(delta, var) - } -} - -impl Subst<Value> for CtxItem { - fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { - match self { - CtxItem::Replaced(e) => CtxItem::Replaced(e.subst_shift(var, val)), - CtxItem::Kept(v, t) => match v.shift(-1, var) { - None => CtxItem::Replaced(val.clone()), - Some(newvar) => CtxItem::Kept(newvar, t.subst_shift(var, val)), - }, - } - } -} - -impl Subst<Value> for TyCtx { - fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { - self.subst_shift(var, val) - } } diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index 28f8e37..ad03187 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -4,7 +4,7 @@ use std::rc::Rc; use crate::error::{TypeError, TypeMessage}; use crate::semantics::core::context::TyCtx; -use crate::semantics::core::var::{AlphaVar, Binder, Shift, Subst}; +use crate::semantics::core::var::{AlphaVar, Binder}; use crate::semantics::phase::normalize::{apply_any, normalize_whnf}; use crate::semantics::phase::typecheck::{builtin_to_value, const_to_value}; use crate::semantics::phase::{Normalized, NormalizedExpr, Typed}; @@ -238,6 +238,40 @@ impl Value { self.get_type() .expect("Internal type error: value is `Sort` but shouldn't be") } + + pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { + Some(Value(Rc::new(RefCell::new( + self.0.borrow().shift(delta, var)?, + )))) + } + pub(crate) fn over_binder<T>(&self, x: T) -> Option<Self> + where + T: Into<AlphaVar>, + { + self.shift(-1, &x.into()) + } + pub(crate) fn under_binder<T>(&self, x: T) -> Self + where + T: Into<AlphaVar>, + { + // Can't fail since delta is positive + self.shift(1, &x.into()).unwrap() + } + pub(crate) fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { + match &*self.as_kind() { + // If the var matches, we can just reuse the provided value instead of copying it. + // We also check that the types match, if in debug mode. + ValueKind::Var(v) if v == var => { + if let Ok(self_ty) = self.get_type() { + val.check_type(&self_ty.subst_shift(var, val)); + } + val.clone() + } + _ => Value(Rc::new(RefCell::new( + self.0.borrow().subst_shift(var, val), + ))), + } + } } impl ValueInternal { @@ -298,6 +332,27 @@ impl ValueInternal { None => Err(TypeError::new(&TyCtx::new(), TypeMessage::Sort)), } } + + pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { + Some(ValueInternal { + form: self.form, + kind: self.kind.shift(delta, var)?, + ty: match &self.ty { + None => None, + Some(ty) => Some(ty.shift(delta, var)?), + }, + span: self.span.clone(), + }) + } + pub(crate) fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { + ValueInternal { + // The resulting value may not stay in wnhf after substitution + form: Unevaled, + kind: self.kind.subst_shift(var, val), + ty: self.ty.as_ref().map(|x| x.subst_shift(var, val)), + span: self.span.clone(), + } + } } impl ValueKind<Value> { @@ -378,6 +433,28 @@ impl ValueKind<Value> { pub(crate) fn from_builtin(b: Builtin) -> ValueKind<Value> { ValueKind::AppliedBuiltin(b, vec![]) } + + pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { + Some(match self { + ValueKind::Var(v) => ValueKind::Var(v.shift(delta, var)?), + _ => self.traverse_ref_with_special_handling_of_binders( + |x| Ok(x.shift(delta, var)?), + |b, x| Ok(x.shift(delta, &var.under_binder(b))?), + )?, + }) + } + pub(crate) fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { + match self { + ValueKind::Var(v) if v == var => val.to_whnf_ignore_type(), + ValueKind::Var(v) => ValueKind::Var(v.shift(-1, var).unwrap()), + _ => self.map_ref_with_special_handling_of_binders( + |x| x.subst_shift(var, val), + |b, x| { + x.subst_shift(&var.under_binder(b), &val.under_binder(b)) + }, + ), + } + } } impl<V> ValueKind<V> { @@ -418,85 +495,6 @@ impl<V> ValueKind<V> { } } -impl Shift for Value { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some(Value(Rc::new(RefCell::new( - self.0.borrow().shift(delta, var)?, - )))) - } -} - -impl Shift for ValueInternal { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some(ValueInternal { - form: self.form, - kind: self.kind.shift(delta, var)?, - ty: match &self.ty { - None => None, - Some(ty) => Some(ty.shift(delta, var)?), - }, - span: self.span.clone(), - }) - } -} - -impl Shift for ValueKind<Value> { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some(match self { - ValueKind::Var(v) => ValueKind::Var(v.shift(delta, var)?), - _ => self.traverse_ref_with_special_handling_of_binders( - |x| Ok(x.shift(delta, var)?), - |b, x| Ok(x.shift(delta, &var.under_binder(b))?), - )?, - }) - } -} - -impl Subst<Value> for Value { - fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { - match &*self.as_kind() { - // If the var matches, we can just reuse the provided value instead of copying it. - // We also check that the types match, if in debug mode. - ValueKind::Var(v) if v == var => { - if let Ok(self_ty) = self.get_type() { - val.check_type(&self_ty.subst_shift(var, val)); - } - val.clone() - } - _ => Value(Rc::new(RefCell::new( - self.0.borrow().subst_shift(var, val), - ))), - } - } -} - -impl Subst<Value> for ValueInternal { - fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { - ValueInternal { - // The resulting value may not stay in wnhf after substitution - form: Unevaled, - kind: self.kind.subst_shift(var, val), - ty: self.ty.as_ref().map(|x| x.subst_shift(var, val)), - span: self.span.clone(), - } - } -} - -impl Subst<Value> for ValueKind<Value> { - fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { - match self { - ValueKind::Var(v) if v == var => val.to_whnf_ignore_type(), - ValueKind::Var(v) => ValueKind::Var(v.shift(-1, var).unwrap()), - _ => self.map_ref_with_special_handling_of_binders( - |x| x.subst_shift(var, val), - |b, x| { - x.subst_shift(&var.under_binder(b), &val.under_binder(b)) - }, - ), - } - } -} - // TODO: use Rc comparison to shortcut on identical pointers impl std::cmp::PartialEq for Value { fn eq(&self, other: &Self) -> bool { diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs index c21e53e..a110632 100644 --- a/dhall/src/semantics/core/var.rs +++ b/dhall/src/semantics/core/var.rs @@ -1,5 +1,3 @@ -use std::collections::HashMap; - use crate::syntax::{Label, V}; /// Stores a pair of variables: a normal one and one @@ -18,44 +16,6 @@ pub struct Binder { name: Label, } -pub(crate) trait Shift: Sized { - // Shift an expression to move it around binders without changing the meaning of its free - // variables. Shift by 1 to move an expression under a binder. Shift by -1 to extract an - // expression from under a binder, if the expression does not refer to that bound variable. - // Returns None if delta was negative and the variable was free in the expression. - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self>; - - fn over_binder<T>(&self, x: T) -> Option<Self> - where - T: Into<AlphaVar>, - { - self.shift(-1, &x.into()) - } - - fn under_binder<T>(&self, x: T) -> Self - where - T: Into<AlphaVar>, - { - // Can't fail since delta is positive - self.shift(1, &x.into()).unwrap() - } - - fn under_multiple_binders(&self, shift_map: &HashMap<Label, usize>) -> Self - where - Self: Clone, - { - let mut v = self.clone(); - for (x, n) in shift_map { - v = v.shift(*n as isize, &x.into()).unwrap(); - } - v - } -} - -pub(crate) trait Subst<S> { - fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self; -} - impl AlphaVar { pub(crate) fn to_var_maybe_alpha(&self, alpha: bool) -> V<Label> { if alpha { @@ -64,6 +24,20 @@ impl AlphaVar { self.normal.clone() } } + + pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { + Some(AlphaVar { + normal: self.normal.shift(delta, &var.normal)?, + alpha: self.alpha.shift(delta, &var.alpha)?, + }) + } + pub(crate) fn under_binder<T>(&self, x: T) -> Self + where + T: Into<AlphaVar>, + { + // Can't fail since delta is positive + self.shift(1, &x.into()).unwrap() + } } impl Binder { @@ -82,15 +56,6 @@ impl Binder { } } -impl Shift for AlphaVar { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some(AlphaVar { - normal: self.normal.shift(delta, &var.normal)?, - alpha: self.alpha.shift(delta, &var.alpha)?, - }) - } -} - /// Equality up to alpha-equivalence impl std::cmp::PartialEq for AlphaVar { fn eq(&self, other: &Self) -> bool { diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs index 5d17338..6afed88 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -4,7 +4,6 @@ use std::path::Path; use crate::error::{EncodeError, Error, ImportError, TypeError}; use crate::semantics::core::value::Value; use crate::semantics::core::value::ValueKind; -use crate::semantics::core::var::{AlphaVar, Shift}; use crate::semantics::to_expr::ToExprOptions; use crate::syntax::binary; use crate::syntax::{Builtin, Const, Expr}; @@ -191,18 +190,6 @@ impl Normalized { } } -impl Shift for Typed { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some(Typed(self.0.shift(delta, var)?)) - } -} - -impl Shift for Normalized { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some(Normalized(self.0.shift(delta, var)?)) - } -} - macro_rules! derive_traits_for_wrapper_struct { ($ty:ident) => { impl std::cmp::PartialEq for $ty { diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 7b4b37f..615b2ff 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -3,7 +3,6 @@ use std::convert::TryInto; use crate::semantics::core::value::Value; use crate::semantics::core::value::ValueKind; -use crate::semantics::core::var::Subst; use crate::semantics::phase::typecheck::{rc, typecheck}; use crate::semantics::phase::Normalized; use crate::syntax; diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index 7e408eb..c77d9c4 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -6,7 +6,7 @@ use crate::error::{TypeError, TypeMessage}; use crate::semantics::core::context::TyCtx; use crate::semantics::phase::normalize::merge_maps; use crate::semantics::phase::Normalized; -use crate::semantics::{Binder, Shift, Subst, Value, ValueKind}; +use crate::semantics::{Binder, Value, ValueKind}; use crate::syntax; use crate::syntax::{ Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label, Span, |