From 72d1e3c339cf550fa5af9981af6078a813feb80a Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 17 Jan 2020 11:03:40 +0000 Subject: Remove Shift/Subst traits --- dhall/src/semantics/core/context.rs | 105 +++++----------------- dhall/src/semantics/core/value.rs | 158 ++++++++++++++++----------------- dhall/src/semantics/core/var.rs | 63 +++---------- dhall/src/semantics/phase/mod.rs | 13 --- dhall/src/semantics/phase/normalize.rs | 1 - dhall/src/semantics/phase/typecheck.rs | 2 +- 6 files changed, 115 insertions(+), 227 deletions(-) (limited to 'dhall/src') 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 { + 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) -> 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( - &self, - var: &AlphaVar, - mut f: impl FnMut(&AlphaVar, &CtxItem) -> Result, - ) -> Result { - 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 { - 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::>()?, - ), - ) - } - } - 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 { - 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.shift(delta, var) - } -} - -impl Subst 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 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 { + Some(Value(Rc::new(RefCell::new( + self.0.borrow().shift(delta, var)?, + )))) + } + pub(crate) fn over_binder(&self, x: T) -> Option + where + T: Into, + { + self.shift(-1, &x.into()) + } + pub(crate) fn under_binder(&self, x: T) -> Self + where + T: Into, + { + // 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 { + 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 { @@ -378,6 +433,28 @@ impl ValueKind { pub(crate) fn from_builtin(b: Builtin) -> ValueKind { ValueKind::AppliedBuiltin(b, vec![]) } + + pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Option { + 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 ValueKind { @@ -418,85 +495,6 @@ impl ValueKind { } } -impl Shift for Value { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option { - Some(Value(Rc::new(RefCell::new( - self.0.borrow().shift(delta, var)?, - )))) - } -} - -impl Shift for ValueInternal { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option { - 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 { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option { - 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 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 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 for ValueKind { - 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; - - fn over_binder(&self, x: T) -> Option - where - T: Into, - { - self.shift(-1, &x.into()) - } - - fn under_binder(&self, x: T) -> Self - where - T: Into, - { - // Can't fail since delta is positive - self.shift(1, &x.into()).unwrap() - } - - fn under_multiple_binders(&self, shift_map: &HashMap) -> 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 { - fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self; -} - impl AlphaVar { pub(crate) fn to_var_maybe_alpha(&self, alpha: bool) -> V