summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/expr.rs10
-rw-r--r--dhall/src/normalize.rs99
-rw-r--r--dhall/src/typecheck.rs11
3 files changed, 99 insertions, 21 deletions
diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs
index 90efd39..071bb92 100644
--- a/dhall/src/expr.rs
+++ b/dhall/src/expr.rs
@@ -44,7 +44,7 @@ pub(crate) struct Normalized(pub(crate) TypedInternal);
impl std::cmp::PartialEq for Normalized {
fn eq(&self, other: &Self) -> bool {
- self.to_expr() == other.to_expr()
+ self.0 == other.0
}
}
@@ -153,6 +153,14 @@ mod typed {
}
}
}
+
+ impl std::cmp::PartialEq for TypedInternal {
+ fn eq(&self, other: &Self) -> bool {
+ self.to_value() == other.to_value()
+ }
+ }
+
+ impl std::cmp::Eq for TypedInternal {}
}
/// A Dhall expression representing a simple type.
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 3e13350..c11dd82 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -53,7 +53,7 @@ impl Typed {
/// Stores a pair of variables: a normal one and if relevant one
/// that corresponds to the alpha-normalized version of the first one.
-#[derive(Debug, Clone)]
+#[derive(Debug, Clone, Eq)]
pub(crate) struct DoubleVar {
normal: V<Label>,
alpha: Option<V<()>>,
@@ -83,14 +83,17 @@ impl DoubleVar {
}
}
+/// Equality is up to alpha-equivalence.
impl std::cmp::PartialEq for DoubleVar {
fn eq(&self, other: &Self) -> bool {
- self.normal == other.normal
+ match (&self.alpha, &other.alpha) {
+ (Some(x), Some(y)) => x == y,
+ (None, None) => self.normal == other.normal,
+ _ => false,
+ }
}
}
-impl std::cmp::Eq for DoubleVar {}
-
impl From<Label> for DoubleVar {
fn from(x: Label) -> DoubleVar {
DoubleVar {
@@ -104,6 +107,52 @@ impl<'a> From<&'a Label> for DoubleVar {
x.clone().into()
}
}
+impl From<AlphaLabel> for DoubleVar {
+ fn from(x: AlphaLabel) -> DoubleVar {
+ let l: Label = x.into();
+ l.into()
+ }
+}
+impl<'a> From<&'a AlphaLabel> for DoubleVar {
+ fn from(x: &'a AlphaLabel) -> DoubleVar {
+ x.clone().into()
+ }
+}
+
+// Exactly like a Label, but equality returns always true.
+// This is so that Value equality is exactly alpha-equivalence.
+#[derive(Debug, Clone, Eq)]
+pub(crate) struct AlphaLabel(Label);
+
+impl AlphaLabel {
+ fn to_label_maybe_alpha(&self, alpha: bool) -> Label {
+ if alpha {
+ "_".into()
+ } else {
+ self.to_label()
+ }
+ }
+ fn to_label(&self) -> Label {
+ self.clone().into()
+ }
+}
+
+impl std::cmp::PartialEq for AlphaLabel {
+ fn eq(&self, _other: &Self) -> bool {
+ true
+ }
+}
+
+impl From<Label> for AlphaLabel {
+ fn from(x: Label) -> AlphaLabel {
+ AlphaLabel(x)
+ }
+}
+impl From<AlphaLabel> for Label {
+ fn from(x: AlphaLabel) -> Label {
+ x.0
+ }
+}
#[derive(Debug, Clone)]
enum EnvItem {
@@ -181,10 +230,11 @@ impl NormalizationContext {
}
/// A semantic value.
-#[derive(Debug, Clone)]
+/// Equality is up to alpha-equivalence (renaming of bound variables).
+#[derive(Debug, Clone, PartialEq, Eq)]
pub(crate) enum Value {
/// Closures
- Lam(Label, Thunk, Thunk),
+ Lam(AlphaLabel, Thunk, Thunk),
AppliedBuiltin(Builtin, Vec<Thunk>),
/// `λ(x: a) -> Some x`
OptionalSomeClosure(TypeThunk),
@@ -193,7 +243,7 @@ pub(crate) enum Value {
ListConsClosure(TypeThunk, Option<Thunk>),
/// `λ(x : Natural) -> x + 1`
NaturalSuccClosure,
- Pi(Label, TypeThunk, TypeThunk),
+ Pi(AlphaLabel, TypeThunk, TypeThunk),
Var(DoubleVar),
Const(Const),
@@ -231,7 +281,7 @@ impl Value {
) -> OutputSubExpr {
match self {
Value::Lam(x, t, e) => rc(ExprF::Lam(
- if alpha { "_".into() } else { x.clone() },
+ x.to_label_maybe_alpha(alpha),
t.normalize_to_expr_maybe_alpha(alpha),
e.normalize_to_expr_maybe_alpha(alpha),
)),
@@ -267,7 +317,7 @@ impl Value {
dhall::subexpr!(λ(x : Natural) -> x + 1)
}
Value::Pi(x, t, e) => rc(ExprF::Pi(
- if alpha { "_".into() } else { x.clone() },
+ x.to_label_maybe_alpha(alpha),
t.normalize_to_expr_maybe_alpha(alpha),
e.normalize_to_expr_maybe_alpha(alpha),
)),
@@ -908,6 +958,13 @@ mod thunk {
self.0.borrow().subst_shift(var, val).into_thunk()
}
}
+
+ impl std::cmp::PartialEq for Thunk {
+ fn eq(&self, other: &Self) -> bool {
+ &*self.as_value() == &*other.as_value()
+ }
+ }
+ impl std::cmp::Eq for Thunk {}
}
pub(crate) use thunk::Thunk;
@@ -946,6 +1003,13 @@ impl TypeThunk {
}
}
+ pub(crate) fn to_value(&self) -> Value {
+ match self {
+ TypeThunk::Thunk(th) => th.to_value(),
+ TypeThunk::Type(t) => t.to_value(),
+ }
+ }
+
pub(crate) fn normalize_to_expr_maybe_alpha(
&self,
alpha: bool,
@@ -968,6 +1032,13 @@ impl TypeThunk {
}
}
+impl std::cmp::PartialEq for TypeThunk {
+ fn eq(&self, other: &Self) -> bool {
+ self.to_value() == other.to_value()
+ }
+}
+impl std::cmp::Eq for TypeThunk {}
+
fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
use dhall_syntax::Builtin::*;
use Value::*;
@@ -1252,10 +1323,12 @@ fn normalize_one_layer(expr: ExprF<Thunk, Label, X>) -> Value {
ExprF::Embed(_) => unreachable!(),
ExprF::Var(_) => unreachable!(),
ExprF::Annot(x, _) => RetThunk(x),
- ExprF::Lam(x, t, e) => RetValue(Lam(x, t, e)),
- ExprF::Pi(x, t, e) => {
- RetValue(Pi(x, TypeThunk::from_thunk(t), TypeThunk::from_thunk(e)))
- }
+ ExprF::Lam(x, t, e) => RetValue(Lam(x.into(), t, e)),
+ ExprF::Pi(x, t, e) => RetValue(Pi(
+ x.into(),
+ TypeThunk::from_thunk(t),
+ TypeThunk::from_thunk(e),
+ )),
ExprF::Let(x, _, v, b) => {
let v = Typed::from_thunk_untyped(v);
RetThunk(b.subst_shift(&x.into(), &v))
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 8137417..2b87bd2 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -243,8 +243,7 @@ where
T: Borrow<Type>,
U: Borrow<Type>,
{
- eL0.borrow().to_value().normalize_to_expr_maybe_alpha(true)
- == eR0.borrow().to_value().normalize_to_expr_maybe_alpha(true)
+ eL0.borrow().to_value() == eR0.borrow().to_value()
}
fn const_to_typed(c: Const) -> Typed {
@@ -352,9 +351,8 @@ fn type_of_builtin<E>(b: Builtin) -> Expr<X, E> {
forall (nothing: optional) ->
optional
),
- // TODO: alpha-equivalence in type-inference tests
OptionalNone => dhall::expr!(
- forall (A: Type) -> Optional A
+ forall (a: Type) -> Optional a
),
}
}
@@ -436,7 +434,7 @@ impl TypeIntermediate {
Typed::from_thunk_and_type(
Value::Pi(
- x.clone(),
+ x.clone().into(),
TypeThunk::from_type(ta.clone()),
TypeThunk::from_type(tb.clone()),
)
@@ -823,12 +821,11 @@ fn type_last_layer(
match &r.internal_whnf() {
Some(Value::UnionType(kts)) => match kts.get(&x) {
// Constructor has type T -> < x: T, ... >
- // TODO: use "_" instead of x (i.e. compare types using equivalence in tests)
Some(Some(t)) => {
Ok(RetType(
TypeIntermediate::Pi(
ctx.clone(),
- x.clone(),
+ "_".into(),
t.to_type(ctx)?,
r.clone(),
)
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 21:36:12 +0000