summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/expr.rs30
-rw-r--r--dhall/src/normalize.rs352
-rw-r--r--dhall/src/tests.rs9
-rw-r--r--dhall/src/typecheck.rs109
4 files changed, 312 insertions, 188 deletions
diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs
index 5bde68f..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
}
}
@@ -58,11 +58,11 @@ impl std::fmt::Display for Normalized {
mod typed {
use super::{Type, Typed};
- use crate::normalize::{Thunk, Value};
+ use crate::normalize::{DoubleVar, Thunk, Value};
use crate::typecheck::{
TypeError, TypeInternal, TypeMessage, TypecheckContext,
};
- use dhall_syntax::{Const, Label, SubExpr, V, X};
+ use dhall_syntax::{Const, SubExpr, X};
use std::borrow::Cow;
#[derive(Debug, Clone)]
@@ -94,6 +94,10 @@ mod typed {
self.to_value().normalize_to_expr()
}
+ pub(crate) fn to_expr_alpha(&self) -> SubExpr<X, X> {
+ self.to_value().normalize_to_expr_maybe_alpha(true)
+ }
+
pub(crate) fn to_thunk(&self) -> Thunk {
match self {
TypedInternal::Value(th, _) => th.clone(),
@@ -129,7 +133,7 @@ mod typed {
}
}
- pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+ pub(crate) fn shift(&self, delta: isize, var: &DoubleVar) -> Self {
match self {
TypedInternal::Value(th, t) => TypedInternal::Value(
th.shift(delta, var),
@@ -139,7 +143,7 @@ mod typed {
}
}
- pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
+ pub(crate) fn subst_shift(&self, var: &DoubleVar, val: &Typed) -> Self {
match self {
TypedInternal::Value(th, t) => TypedInternal::Value(
th.subst_shift(var, val),
@@ -149,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.
@@ -207,16 +219,16 @@ impl Normalized {
pub(crate) fn to_expr(&self) -> SubExpr<X, X> {
self.0.to_expr()
}
+ #[allow(dead_code)]
+ pub(crate) fn to_expr_alpha(&self) -> SubExpr<X, X> {
+ self.0.to_expr_alpha()
+ }
pub(crate) fn to_value(&self) -> Value {
self.0.to_value()
}
pub(crate) fn to_thunk(&self) -> Thunk {
self.0.to_thunk()
}
- #[allow(dead_code)]
- pub(crate) fn unnote(self) -> Normalized {
- Normalized(self.0)
- }
}
impl Typed {
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 8ae746d..c11dd82 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -25,24 +25,20 @@ impl Typed {
/// leave ill-typed sub-expressions unevaluated.
///
pub fn normalize(self) -> Normalized {
- let internal = match self.0 {
- TypedInternal::Sort => TypedInternal::Sort,
- TypedInternal::Value(thunk, t) => {
- // TODO: stupid but needed for now
- let thunk =
- Thunk::from_normalized_expr(thunk.normalize_to_expr());
+ match &self.0 {
+ TypedInternal::Sort => {}
+ TypedInternal::Value(thunk, _) => {
thunk.normalize_nf();
- TypedInternal::Value(thunk, t)
}
- };
- Normalized(internal)
+ }
+ Normalized(self.0)
}
- pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+ pub(crate) fn shift(&self, delta: isize, var: &DoubleVar) -> Self {
Typed(self.0.shift(delta, var))
}
- pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
+ pub(crate) fn subst_shift(&self, var: &DoubleVar, val: &Typed) -> Self {
Typed(self.0.subst_shift(var, val))
}
@@ -55,14 +51,117 @@ 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, Eq)]
+pub(crate) struct DoubleVar {
+ normal: V<Label>,
+ alpha: Option<V<()>>,
+}
+
+impl DoubleVar {
+ pub(crate) fn to_var(&self, alpha: bool) -> V<Label> {
+ match (alpha, &self.alpha) {
+ (true, Some(x)) => V("_".into(), x.1),
+ _ => self.normal.clone(),
+ }
+ }
+ pub(crate) fn from_var(normal: V<Label>) -> Self {
+ DoubleVar {
+ normal,
+ alpha: None,
+ }
+ }
+ pub(crate) fn shift(&self, delta: isize, var: &DoubleVar) -> Self {
+ DoubleVar {
+ normal: self.normal.shift(delta, &var.normal),
+ alpha: match (&self.alpha, &var.alpha) {
+ (Some(x), Some(v)) => Some(x.shift(delta, v)),
+ _ => None,
+ },
+ }
+ }
+}
+
+/// Equality is up to alpha-equivalence.
+impl std::cmp::PartialEq for DoubleVar {
+ fn eq(&self, other: &Self) -> bool {
+ match (&self.alpha, &other.alpha) {
+ (Some(x), Some(y)) => x == y,
+ (None, None) => self.normal == other.normal,
+ _ => false,
+ }
+ }
+}
+
+impl From<Label> for DoubleVar {
+ fn from(x: Label) -> DoubleVar {
+ DoubleVar {
+ normal: V(x, 0),
+ alpha: Some(V((), 0)),
+ }
+ }
+}
+impl<'a> From<&'a Label> for DoubleVar {
+ fn from(x: &'a Label) -> 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 {
Thunk(Thunk),
- Skip(V<Label>),
+ Skip(DoubleVar),
}
impl EnvItem {
- fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+ fn shift(&self, delta: isize, var: &DoubleVar) -> Self {
use EnvItem::*;
match self {
Thunk(e) => Thunk(e.shift(delta, var)),
@@ -70,7 +169,7 @@ impl EnvItem {
}
}
- pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
+ pub(crate) fn subst_shift(&self, var: &DoubleVar, val: &Typed) -> Self {
match self {
EnvItem::Thunk(e) => EnvItem::Thunk(e.subst_shift(var, val)),
EnvItem::Skip(v) if v == var => EnvItem::Thunk(val.to_thunk()),
@@ -98,7 +197,8 @@ impl NormalizationContext {
match self.0.lookup(x, *n) {
Some(EnvItem::Thunk(t)) => t.to_value(),
Some(EnvItem::Skip(newvar)) => Value::Var(newvar.clone()),
- None => Value::Var(var.clone()),
+ // Free variable
+ None => Value::Var(DoubleVar::from_var(var.clone())),
}
}
pub(crate) fn from_typecheck_ctx(
@@ -118,11 +218,11 @@ impl NormalizationContext {
NormalizationContext(Rc::new(ctx))
}
- fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+ fn shift(&self, delta: isize, var: &DoubleVar) -> Self {
NormalizationContext(Rc::new(self.0.map(|_, e| e.shift(delta, var))))
}
- fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
+ fn subst_shift(&self, var: &DoubleVar, val: &Typed) -> Self {
NormalizationContext(Rc::new(
self.0.map(|_, e| e.subst_shift(var, val)),
))
@@ -130,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),
@@ -142,9 +243,9 @@ pub(crate) enum Value {
ListConsClosure(TypeThunk, Option<Thunk>),
/// `λ(x : Natural) -> x + 1`
NaturalSuccClosure,
- Pi(Label, TypeThunk, TypeThunk),
+ Pi(AlphaLabel, TypeThunk, TypeThunk),
- Var(V<Label>),
+ Var(DoubleVar),
Const(Const),
BoolLit(bool),
NaturalLit(Natural),
@@ -170,76 +271,99 @@ impl Value {
/// Convert the value to a fully normalized syntactic expression
pub(crate) fn normalize_to_expr(&self) -> OutputSubExpr {
+ self.normalize_to_expr_maybe_alpha(false)
+ }
+ /// Convert the value to a fully normalized syntactic expression. Also alpha-normalize
+ /// if alpha is `true`
+ pub(crate) fn normalize_to_expr_maybe_alpha(
+ &self,
+ alpha: bool,
+ ) -> OutputSubExpr {
match self {
Value::Lam(x, t, e) => rc(ExprF::Lam(
- x.clone(),
- t.normalize_to_expr(),
- e.normalize_to_expr(),
+ x.to_label_maybe_alpha(alpha),
+ t.normalize_to_expr_maybe_alpha(alpha),
+ e.normalize_to_expr_maybe_alpha(alpha),
)),
Value::AppliedBuiltin(b, args) => {
let mut e = rc(ExprF::Builtin(*b));
for v in args {
- e = rc(ExprF::App(e, v.normalize_to_expr()));
+ e = rc(ExprF::App(
+ e,
+ v.normalize_to_expr_maybe_alpha(alpha),
+ ));
}
e
}
Value::OptionalSomeClosure(n) => {
- let a = n.normalize_to_expr();
+ let a = n.normalize_to_expr_maybe_alpha(alpha);
dhall::subexpr!(λ(x: a) -> Some x)
}
- Value::ListConsClosure(n, None) => {
- let a = n.normalize_to_expr();
+ Value::ListConsClosure(a, None) => {
// Avoid accidental capture of the new `x` variable
let a1 = a.shift(1, &Label::from("x").into());
+ let a1 = a1.normalize_to_expr_maybe_alpha(alpha);
+ let a = a.normalize_to_expr_maybe_alpha(alpha);
dhall::subexpr!(λ(x : a) -> λ(xs : List a1) -> [ x ] # xs)
}
Value::ListConsClosure(n, Some(v)) => {
- let v = v.normalize_to_expr();
- let a = n.normalize_to_expr();
// Avoid accidental capture of the new `xs` variable
let v = v.shift(1, &Label::from("xs").into());
+ let v = v.normalize_to_expr_maybe_alpha(alpha);
+ let a = n.normalize_to_expr_maybe_alpha(alpha);
dhall::subexpr!(λ(xs : List a) -> [ v ] # xs)
}
Value::NaturalSuccClosure => {
dhall::subexpr!(λ(x : Natural) -> x + 1)
}
Value::Pi(x, t, e) => rc(ExprF::Pi(
- x.clone(),
- t.normalize_to_expr(),
- e.normalize_to_expr(),
+ x.to_label_maybe_alpha(alpha),
+ t.normalize_to_expr_maybe_alpha(alpha),
+ e.normalize_to_expr_maybe_alpha(alpha),
)),
- Value::Var(v) => rc(ExprF::Var(v.clone())),
+ Value::Var(v) => rc(ExprF::Var(v.to_var(alpha))),
Value::Const(c) => rc(ExprF::Const(*c)),
Value::BoolLit(b) => rc(ExprF::BoolLit(*b)),
Value::NaturalLit(n) => rc(ExprF::NaturalLit(*n)),
Value::IntegerLit(n) => rc(ExprF::IntegerLit(*n)),
Value::EmptyOptionalLit(n) => rc(ExprF::App(
rc(ExprF::Builtin(Builtin::OptionalNone)),
- n.normalize_to_expr(),
+ n.normalize_to_expr_maybe_alpha(alpha),
)),
Value::NEOptionalLit(n) => {
- rc(ExprF::SomeLit(n.normalize_to_expr()))
+ rc(ExprF::SomeLit(n.normalize_to_expr_maybe_alpha(alpha)))
}
Value::EmptyListLit(n) => {
- rc(ExprF::EmptyListLit(n.normalize_to_expr()))
+ rc(ExprF::EmptyListLit(n.normalize_to_expr_maybe_alpha(alpha)))
}
Value::NEListLit(elts) => rc(ExprF::NEListLit(
- elts.into_iter().map(|n| n.normalize_to_expr()).collect(),
+ elts.into_iter()
+ .map(|n| n.normalize_to_expr_maybe_alpha(alpha))
+ .collect(),
)),
Value::RecordLit(kvs) => rc(ExprF::RecordLit(
kvs.iter()
- .map(|(k, v)| (k.clone(), v.normalize_to_expr()))
+ .map(|(k, v)| {
+ (k.clone(), v.normalize_to_expr_maybe_alpha(alpha))
+ })
.collect(),
)),
Value::RecordType(kts) => rc(ExprF::RecordType(
kts.iter()
- .map(|(k, v)| (k.clone(), v.normalize_to_expr()))
+ .map(|(k, v)| {
+ (k.clone(), v.normalize_to_expr_maybe_alpha(alpha))
+ })
.collect(),
)),
Value::UnionType(kts) => rc(ExprF::UnionType(
kts.iter()
.map(|(k, v)| {
- (k.clone(), v.as_ref().map(|v| v.normalize_to_expr()))
+ (
+ k.clone(),
+ v.as_ref().map(|v| {
+ v.normalize_to_expr_maybe_alpha(alpha)
+ }),
+ )
})
.collect(),
)),
@@ -247,23 +371,34 @@ impl Value {
let kts = kts
.iter()
.map(|(k, v)| {
- (k.clone(), v.as_ref().map(|v| v.normalize_to_expr()))
+ (
+ k.clone(),
+ v.as_ref().map(|v| {
+ v.normalize_to_expr_maybe_alpha(alpha)
+ }),
+ )
})
.collect();
rc(ExprF::Field(rc(ExprF::UnionType(kts)), l.clone()))
}
Value::UnionLit(l, v, kts) => rc(ExprF::UnionLit(
l.clone(),
- v.normalize_to_expr(),
+ v.normalize_to_expr_maybe_alpha(alpha),
kts.iter()
.map(|(k, v)| {
- (k.clone(), v.as_ref().map(|v| v.normalize_to_expr()))
+ (
+ k.clone(),
+ v.as_ref().map(|v| {
+ v.normalize_to_expr_maybe_alpha(alpha)
+ }),
+ )
})
.collect(),
)),
Value::TextLit(elts) => {
fn normalize_textlit(
elts: &Vec<InterpolatedTextContents<Thunk>>,
+ alpha: bool,
) -> InterpolatedText<OutputSubExpr> {
elts.iter()
.flat_map(|contents| {
@@ -271,12 +406,14 @@ impl Value {
let new_interpolated = match contents {
Expr(n) => match &*n.normalize_nf() {
Value::TextLit(elts2) => {
- normalize_textlit(elts2)
+ normalize_textlit(elts2, alpha)
}
e => InterpolatedText::from((
String::new(),
vec![(
- e.normalize_to_expr(),
+ e.normalize_to_expr_maybe_alpha(
+ alpha,
+ ),
String::new(),
)],
)),
@@ -288,10 +425,10 @@ impl Value {
.collect()
}
- rc(ExprF::TextLit(normalize_textlit(elts)))
+ rc(ExprF::TextLit(normalize_textlit(elts, alpha)))
}
Value::PartialExpr(e) => {
- rc(e.map_ref_simple(|v| v.normalize_to_expr()))
+ rc(e.map_ref_simple(|v| v.normalize_to_expr_maybe_alpha(alpha)))
}
}
}
@@ -403,7 +540,7 @@ impl Value {
Value::AppliedBuiltin(b, vec![])
}
- fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+ fn shift(&self, delta: isize, var: &DoubleVar) -> Self {
match self {
Value::Lam(x, t, e) => Value::Lam(
x.clone(),
@@ -500,8 +637,27 @@ impl Value {
}
}
- pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
+ pub(crate) fn subst_shift(&self, var: &DoubleVar, val: &Typed) -> Self {
match self {
+ // Retry normalizing since substituting may allow progress
+ Value::AppliedBuiltin(b, args) => apply_builtin(
+ *b,
+ args.iter().map(|v| v.subst_shift(var, val)).collect(),
+ ),
+ // Retry normalizing since substituting may allow progress
+ Value::PartialExpr(e) => {
+ normalize_one_layer(e.map_ref_with_special_handling_of_binders(
+ |v| v.subst_shift(var, val),
+ |x, v| {
+ v.subst_shift(
+ &var.shift(1, &x.into()),
+ &val.shift(1, &x.into()),
+ )
+ },
+ X::clone,
+ Label::clone,
+ ))
+ }
Value::Lam(x, t, e) => Value::Lam(
x.clone(),
t.subst_shift(var, val),
@@ -510,10 +666,6 @@ impl Value {
&val.shift(1, &x.into()),
),
),
- Value::AppliedBuiltin(b, args) => Value::AppliedBuiltin(
- *b,
- args.iter().map(|v| v.subst_shift(var, val)).collect(),
- ),
Value::NaturalSuccClosure => Value::NaturalSuccClosure,
Value::OptionalSomeClosure(tth) => {
Value::OptionalSomeClosure(tth.subst_shift(var, val))
@@ -593,30 +745,16 @@ impl Value {
})
.collect(),
),
- Value::PartialExpr(e) => {
- Value::PartialExpr(e.map_ref_with_special_handling_of_binders(
- |v| v.subst_shift(var, val),
- |x, v| {
- v.subst_shift(
- &var.shift(1, &x.into()),
- &val.shift(1, &x.into()),
- )
- },
- X::clone,
- Label::clone,
- ))
- }
}
}
}
mod thunk {
use super::{
- apply_any, normalize_whnf, InputSubExpr, NormalizationContext,
- OutputSubExpr, Value,
+ apply_any, normalize_whnf, DoubleVar, InputSubExpr,
+ NormalizationContext, OutputSubExpr, Value,
};
use crate::expr::Typed;
- use dhall_syntax::{Label, V};
use std::cell::{Ref, RefCell};
use std::rc::Rc;
@@ -693,7 +831,7 @@ mod thunk {
}
}
- fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+ fn shift(&self, delta: isize, var: &DoubleVar) -> Self {
match self {
ThunkInternal::Unnormalized(ctx, e) => {
ThunkInternal::Unnormalized(
@@ -707,7 +845,7 @@ mod thunk {
}
}
- fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
+ fn subst_shift(&self, var: &DoubleVar, val: &Typed) -> Self {
match self {
ThunkInternal::Unnormalized(ctx, e) => {
ThunkInternal::Unnormalized(
@@ -794,7 +932,14 @@ mod thunk {
}
pub(crate) fn normalize_to_expr(&self) -> OutputSubExpr {
- self.normalize_nf().normalize_to_expr()
+ self.normalize_to_expr_maybe_alpha(false)
+ }
+
+ pub(crate) fn normalize_to_expr_maybe_alpha(
+ &self,
+ alpha: bool,
+ ) -> OutputSubExpr {
+ self.normalize_nf().normalize_to_expr_maybe_alpha(alpha)
}
pub(crate) fn app_val(&self, val: Value) -> Value {
@@ -805,14 +950,21 @@ mod thunk {
apply_any(self.clone(), th)
}
- pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+ pub(crate) fn shift(&self, delta: isize, var: &DoubleVar) -> Self {
self.0.borrow().shift(delta, var).into_thunk()
}
- pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
+ pub(crate) fn subst_shift(&self, var: &DoubleVar, val: &Typed) -> Self {
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;
@@ -851,18 +1003,28 @@ impl TypeThunk {
}
}
- pub(crate) fn normalize_to_expr(&self) -> OutputSubExpr {
- self.normalize_nf().normalize_to_expr()
+ 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,
+ ) -> OutputSubExpr {
+ self.normalize_nf().normalize_to_expr_maybe_alpha(alpha)
}
- fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+ fn shift(&self, delta: isize, var: &DoubleVar) -> 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: &V<Label>, val: &Typed) -> Self {
+ pub(crate) fn subst_shift(&self, var: &DoubleVar, 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)),
@@ -870,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::*;
@@ -1118,7 +1287,7 @@ fn apply_any(f: Thunk, a: Thunk) -> Value {
fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> Value {
match expr.as_ref() {
ExprF::Embed(e) => return e.to_value(),
- ExprF::Var(v) => return ctx.lookup(&v),
+ ExprF::Var(v) => return ctx.lookup(v),
_ => {}
}
@@ -1154,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))
@@ -1384,6 +1555,12 @@ mod spec_tests {
};
}
+ macro_rules! alpha_norm {
+ ($name:ident, $path:expr) => {
+ make_spec_test!(AlphaNormalization, Success, $name, $path);
+ };
+ }
+
norm!(success_haskell_tutorial_access_0, "haskell-tutorial/access/0");
norm!(success_haskell_tutorial_access_1, "haskell-tutorial/access/1");
// norm!(success_haskell_tutorial_combineTypes_0, "haskell-tutorial/combineTypes/0");
@@ -1710,4 +1887,11 @@ mod spec_tests {
norm!(success_unit_UnionTypeEmpty, "unit/UnionTypeEmpty");
norm!(success_unit_UnionTypeNormalizeArguments, "unit/UnionTypeNormalizeArguments");
norm!(success_unit_Variable, "unit/Variable");
+
+ alpha_norm!(alpha_success_unit_FunctionBindingUnderscore, "unit/FunctionBindingUnderscore");
+ alpha_norm!(alpha_success_unit_FunctionBindingX, "unit/FunctionBindingX");
+ alpha_norm!(alpha_success_unit_FunctionNestedBindingX, "unit/FunctionNestedBindingX");
+ alpha_norm!(alpha_success_unit_FunctionTypeBindingUnderscore, "unit/FunctionTypeBindingUnderscore");
+ alpha_norm!(alpha_success_unit_FunctionTypeBindingX, "unit/FunctionTypeBindingX");
+ alpha_norm!(alpha_success_unit_FunctionTypeNestedBindingX, "unit/FunctionTypeNestedBindingX");
}
diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs
index ce74606..6b2ab60 100644
--- a/dhall/src/tests.rs
+++ b/dhall/src/tests.rs
@@ -43,6 +43,7 @@ pub enum Feature {
Parser,
Import,
Normalization,
+ AlphaNormalization,
Typecheck,
TypeInference,
}
@@ -83,6 +84,7 @@ pub fn run_test(
Parser => "parser/",
Import => "import/",
Normalization => "normalization/",
+ AlphaNormalization => "alpha-normalization/",
Typecheck => "typecheck/",
TypeInference => "type-inference/",
};
@@ -139,6 +141,11 @@ pub fn run_test(
let expr = expr.skip_typecheck().normalize();
assert_eq_display!(expr, expected);
}
+ AlphaNormalization => {
+ let expr =
+ expr.skip_typecheck().normalize().to_expr_alpha();
+ assert_eq_display!(expr, expected.to_expr());
+ }
}
}
Failure => {
@@ -154,7 +161,7 @@ pub fn run_test(
Import => {
parse_file_str(&file_path)?.resolve().unwrap_err();
}
- Normalization => unreachable!(),
+ Normalization | AlphaNormalization => unreachable!(),
Typecheck | TypeInference => {
parse_file_str(&file_path)?
.skip_resolve()?
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 8b7f011..2b87bd2 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -5,7 +5,9 @@ use std::collections::BTreeMap;
use std::fmt;
use crate::expr::*;
-use crate::normalize::{NormalizationContext, Thunk, TypeThunk, Value};
+use crate::normalize::{
+ DoubleVar, NormalizationContext, Thunk, TypeThunk, Value,
+};
use crate::traits::DynamicType;
use dhall_proc_macros as dhall;
use dhall_syntax;
@@ -43,7 +45,7 @@ impl Typed {
}
impl Normalized {
- fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+ fn shift(&self, delta: isize, var: &DoubleVar) -> Self {
Normalized(self.0.shift(delta, var))
}
pub(crate) fn to_type(self) -> Type {
@@ -67,16 +69,13 @@ impl Type {
fn as_const(&self) -> Option<Const> {
self.0.as_const()
}
- fn internal(&self) -> &TypeInternal {
- &self.0
- }
fn internal_whnf(&self) -> Option<Value> {
self.0.whnf()
}
- pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+ pub(crate) fn shift(&self, delta: isize, var: &DoubleVar) -> Self {
Type(self.0.shift(delta, var))
}
- pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
+ pub(crate) fn subst_shift(&self, var: &DoubleVar, val: &Typed) -> Self {
Type(self.0.subst_shift(var, val))
}
@@ -148,14 +147,14 @@ impl TypeInternal {
_ => None,
}
}
- fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+ fn shift(&self, delta: isize, var: &DoubleVar) -> Self {
use TypeInternal::*;
match self {
Typed(e) => Typed(Box::new(e.shift(delta, var))),
Const(c) => Const(*c),
}
}
- fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
+ fn subst_shift(&self, var: &DoubleVar, val: &Typed) -> Self {
use TypeInternal::*;
match self {
Typed(e) => Typed(Box::new(e.subst_shift(var, val))),
@@ -173,12 +172,12 @@ impl PartialEq for TypeInternal {
#[derive(Debug, Clone)]
pub(crate) enum EnvItem {
- Type(V<Label>, Type),
+ Type(DoubleVar, Type),
Value(Normalized),
}
impl EnvItem {
- fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+ fn shift(&self, delta: isize, var: &DoubleVar) -> Self {
use EnvItem::*;
match self {
Type(v, e) => Type(v.shift(delta, var), e.shift(delta, var)),
@@ -238,89 +237,13 @@ fn function_check(a: Const, b: Const) -> Result<Const, ()> {
}
}
-fn match_vars(vl: &V<Label>, vr: &V<Label>, ctx: &[(&Label, &Label)]) -> bool {
- let (V(xL, mut nL), V(xR, mut nR)) = (vl, vr);
- for &(xL2, xR2) in ctx {
- match (nL, nR) {
- (0, 0) if xL == xL2 && xR == xR2 => return true,
- (_, _) => {
- if xL == xL2 {
- nL -= 1;
- }
- if xR == xR2 {
- nR -= 1;
- }
- }
- }
- }
- xL == xR && nL == nR
-}
-
// Equality up to alpha-equivalence (renaming of bound variables)
fn prop_equal<T, U>(eL0: T, eR0: U) -> bool
where
T: Borrow<Type>,
U: Borrow<Type>,
{
- use dhall_syntax::ExprF::*;
- fn go<'a, S, T>(
- ctx: &mut Vec<(&'a Label, &'a Label)>,
- el: &'a SubExpr<S, X>,
- er: &'a SubExpr<T, X>,
- ) -> bool
- where
- S: ::std::fmt::Debug,
- T: ::std::fmt::Debug,
- {
- match (el.as_ref(), er.as_ref()) {
- (Const(a), Const(b)) => a == b,
- (Builtin(a), Builtin(b)) => a == b,
- (Var(vL), Var(vR)) => match_vars(vL, vR, ctx),
- (Pi(xL, tL, bL), Pi(xR, tR, bR)) => {
- go(ctx, tL, tR) && {
- ctx.push((xL, xR));
- let eq2 = go(ctx, bL, bR);
- ctx.pop();
- eq2
- }
- }
- (App(fL, aL), App(fR, aR)) => go(ctx, fL, fR) && go(ctx, aL, aR),
- (RecordType(ktsL0), RecordType(ktsR0)) => {
- ktsL0.len() == ktsR0.len()
- && ktsL0
- .iter()
- .zip(ktsR0.iter())
- .all(|((kL, tL), (kR, tR))| kL == kR && go(ctx, tL, tR))
- }
- (UnionType(ktsL0), UnionType(ktsR0)) => {
- ktsL0.len() == ktsR0.len()
- && ktsL0.iter().zip(ktsR0.iter()).all(
- |((kL, tL), (kR, tR))| {
- kL == kR
- && match (tL, tR) {
- (None, None) => true,
- (Some(tL), Some(tR)) => go(ctx, tL, tR),
- _ => false,
- }
- },
- )
- }
- (_, _) => false,
- }
- }
- match (eL0.borrow().internal(), eR0.borrow().internal()) {
- // (TypeInternal::Const(cl), TypeInternal::Const(cr)) => cl == cr,
- // (TypeInternal::Expr(l), TypeInternal::Expr(r)) => {
- _ => {
- let mut ctx = vec![];
- go(
- &mut ctx,
- &eL0.borrow().to_expr(),
- &eR0.borrow().to_expr(),
- )
- }
- // _ => false,
- }
+ eL0.borrow().to_value() == eR0.borrow().to_value()
}
fn const_to_typed(c: Const) -> Typed {
@@ -428,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
),
}
}
@@ -512,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()),
)
@@ -756,7 +678,7 @@ fn type_last_layer(
mkerr(TypeMismatch(f.clone(), tx.clone().to_normalized(), a))
});
- Ok(RetType(tb.subst_shift(&V(x.clone(), 0), &a)))
+ Ok(RetType(tb.subst_shift(&x.into(), &a)))
}
Annot(x, t) => {
let t = t.to_type();
@@ -899,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-25 17:07:24 +0000