summaryrefslogtreecommitdiff
path: root/dhall/src
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src')
-rw-r--r--dhall/src/semantics/core/context.rs12
-rw-r--r--dhall/src/semantics/core/value.rs26
-rw-r--r--dhall/src/semantics/core/var.rs21
-rw-r--r--dhall/src/semantics/phase/normalize.rs9
-rw-r--r--dhall/src/semantics/phase/typecheck.rs22
5 files changed, 34 insertions, 56 deletions
diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs
index 47d2d2d..8c64c26 100644
--- a/dhall/src/semantics/core/context.rs
+++ b/dhall/src/semantics/core/context.rs
@@ -6,7 +6,9 @@ use crate::syntax::{Label, V};
#[derive(Debug, Clone)]
enum CtxItem {
- Kept(AlphaVar, Value),
+ // Variable is bound with given type
+ Kept(Value),
+ // Variable has been replaced by corresponding value
Replaced(Value),
}
@@ -24,7 +26,7 @@ impl TyCtx {
}
pub fn insert_type(&self, x: &Binder, t: Value) -> Self {
let mut vec = self.ctx.clone();
- vec.push((x.clone(), CtxItem::Kept(x.into(), t.under_binder(x))));
+ vec.push((x.clone(), CtxItem::Kept(t.under_binder())));
self.with_vec(vec)
}
pub fn insert_value(
@@ -47,7 +49,7 @@ impl TyCtx {
Some(newvar) => newvar,
None => break item,
};
- if let CtxItem::Kept(_, _) = item {
+ if let CtxItem::Kept(_) = item {
shift_delta += 1;
}
} else {
@@ -57,8 +59,8 @@ impl TyCtx {
};
let v = match found_item {
- CtxItem::Kept(newvar, t) => Value::from_kind_and_type(
- ValueKind::Var(newvar.clone()),
+ CtxItem::Kept(t) => Value::from_kind_and_type(
+ ValueKind::Var(AlphaVar::default()),
t.clone(),
),
CtxItem::Replaced(v) => v.clone(),
diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs
index 6ae0a90..8b3ada1 100644
--- a/dhall/src/semantics/core/value.rs
+++ b/dhall/src/semantics/core/value.rs
@@ -209,9 +209,9 @@ impl Value {
pub(crate) fn app(&self, v: Value) -> Value {
let body_t = match &*self.get_type_not_sort().as_whnf() {
- ValueKind::Pi(x, t, e) => {
+ ValueKind::Pi(_, t, e) => {
v.check_type(t);
- e.subst_shift(&x.into(), &v)
+ e.subst_shift(&AlphaVar::default(), &v)
}
_ => unreachable!("Internal type error"),
};
@@ -242,18 +242,12 @@ impl Value {
pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
Some(self.as_internal().shift(delta, var)?.into_value())
}
- pub(crate) fn over_binder<T>(&self, x: T) -> Option<Self>
- where
- T: Into<AlphaVar>,
- {
- self.shift(-1, &x.into())
+ pub(crate) fn over_binder(&self) -> Option<Self> {
+ self.shift(-1, &AlphaVar::default())
}
- pub(crate) fn under_binder<T>(&self, x: T) -> Self
- where
- T: Into<AlphaVar>,
- {
+ pub(crate) fn under_binder(&self) -> Self {
// Can't fail since delta is positive
- self.shift(1, &x.into()).unwrap()
+ self.shift(1, &AlphaVar::default()).unwrap()
}
pub(crate) fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
match &*self.as_kind() {
@@ -456,18 +450,18 @@ impl ValueKind<Value> {
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))?),
+ |_, _, x| Ok(x.shift(delta, &var.under_binder())?),
)?,
})
}
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.over_binder(var).unwrap()),
+ 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))
+ |_, _, x| {
+ x.subst_shift(&var.under_binder(), &val.under_binder())
},
),
}
diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs
index 93776bf..b336c66 100644
--- a/dhall/src/semantics/core/var.rs
+++ b/dhall/src/semantics/core/var.rs
@@ -26,15 +26,9 @@ impl AlphaVar {
alpha: self.alpha.shift(delta, &var.alpha)?,
})
}
- pub(crate) fn under_binder<T>(&self, x: T) -> Self
- where
- T: Into<AlphaVar>,
- {
+ pub(crate) fn under_binder(&self) -> Self {
// Can't fail since delta is positive
- self.shift(1, &x.into()).unwrap()
- }
- pub(crate) fn over_binder(&self, x: &AlphaVar) -> Option<Self> {
- self.shift(-1, x)
+ self.shift(1, &AlphaVar::default()).unwrap()
}
}
@@ -82,17 +76,6 @@ impl std::fmt::Debug for Binder {
}
}
-impl From<Binder> for AlphaVar {
- fn from(x: Binder) -> AlphaVar {
- AlphaVar { alpha: V((), 0) }
- }
-}
-impl<'a> From<&'a Binder> for AlphaVar {
- fn from(x: &'a Binder) -> AlphaVar {
- AlphaVar { alpha: V((), 0) }
- }
-}
-
impl From<Binder> for Label {
fn from(x: Binder) -> Label {
x.name
diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs
index 8f9a58a..541a196 100644
--- a/dhall/src/semantics/phase/normalize.rs
+++ b/dhall/src/semantics/phase/normalize.rs
@@ -1,10 +1,9 @@
use std::collections::HashMap;
use std::convert::TryInto;
-use crate::semantics::core::value::Value;
-use crate::semantics::core::value::ValueKind;
use crate::semantics::phase::typecheck::{rc, typecheck};
use crate::semantics::phase::Normalized;
+use crate::semantics::{AlphaVar, Value, ValueKind};
use crate::syntax;
use crate::syntax::Const::Type;
use crate::syntax::{
@@ -367,9 +366,9 @@ pub(crate) fn apply_builtin(
pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind<Value> {
let f_borrow = f.as_whnf();
match &*f_borrow {
- ValueKind::Lam(x, _, e) => {
- e.subst_shift(&x.into(), &a).to_whnf_check_type(ty)
- }
+ ValueKind::Lam(_, _, e) => e
+ .subst_shift(&AlphaVar::default(), &a)
+ .to_whnf_check_type(ty),
ValueKind::AppliedBuiltin(b, args) => {
use std::iter::once;
let args = args.iter().cloned().chain(once(a.clone())).collect();
diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs
index 852f41b..15025c1 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, Value, ValueKind};
+use crate::semantics::{AlphaVar, Binder, Value, ValueKind};
use crate::syntax;
use crate::syntax::{
Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label, Span,
@@ -385,15 +385,15 @@ fn type_last_layer(
App(f, a) => {
let tf = f.get_type()?;
let tf_borrow = tf.as_whnf();
- let (x, tx, tb) = match &*tf_borrow {
- ValueKind::Pi(x, tx, tb) => (x, tx, tb),
+ let (tx, tb) = match &*tf_borrow {
+ ValueKind::Pi(_, tx, tb) => (tx, tb),
_ => return mkerr(NotAFunction(f.clone())),
};
if &a.get_type()? != tx {
return mkerr(TypeMismatch(f.clone(), tx.clone(), a.clone()));
}
- let ret = tb.subst_shift(&x.into(), a);
+ let ret = tb.subst_shift(&AlphaVar::default(), a);
ret.normalize_nf();
RetTypeOnly(ret)
}
@@ -500,13 +500,12 @@ fn type_last_layer(
ValueKind::UnionType(kts) => match kts.get(&x) {
// Constructor has type T -> < x: T, ... >
Some(Some(t)) => {
- let x = ctx.new_binder(x);
RetTypeOnly(
tck_pi_type(
ctx,
- x.clone(),
+ ctx.new_binder(x),
t.clone(),
- r.under_binder(x),
+ r.under_binder(),
)?
)
},
@@ -719,8 +718,8 @@ fn type_last_layer(
// Union alternative with type
Some(Some(variant_type)) => {
let handler_type_borrow = handler_type.as_whnf();
- let (x, tx, tb) = match &*handler_type_borrow {
- ValueKind::Pi(x, tx, tb) => (x, tx, tb),
+ let (tx, tb) = match &*handler_type_borrow {
+ ValueKind::Pi(_, tx, tb) => (tx, tb),
_ => {
return mkerr(NotAFunction(
handler_type.clone(),
@@ -736,8 +735,9 @@ fn type_last_layer(
));
}
- // Extract `tb` from under the `x` binder. Fails is `x` was free in `tb`.
- match tb.over_binder(x) {
+ // Extract `tb` from under the binder. Fails if the variable was used
+ // in `tb`.
+ match tb.over_binder() {
Some(x) => x,
None => return mkerr(
MergeHandlerReturnTypeMustNotBeDependent,
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 17:52:30 +0000