summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/semantics/core/context.rs105
-rw-r--r--dhall/src/semantics/core/value.rs158
-rw-r--r--dhall/src/semantics/core/var.rs63
-rw-r--r--dhall/src/semantics/phase/mod.rs13
-rw-r--r--dhall/src/semantics/phase/normalize.rs1
-rw-r--r--dhall/src/semantics/phase/typecheck.rs2
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,
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 19:18:32 +0000