summaryrefslogtreecommitdiff
path: root/dhall/src/core
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/core')
-rw-r--r--dhall/src/core/context.rs84
-rw-r--r--dhall/src/core/thunk.rs82
-rw-r--r--dhall/src/core/value.rs10
-rw-r--r--dhall/src/core/var.rs29
4 files changed, 119 insertions, 86 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) {
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 05:36:20 +0000