summaryrefslogtreecommitdiff
path: root/dhall/src/normalize.rs
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/normalize.rs214
1 files changed, 163 insertions, 51 deletions
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 904c0a2..3e13350 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -34,11 +34,11 @@ impl Typed {
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))
}
@@ -51,14 +51,68 @@ 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)]
+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,
+ },
+ }
+ }
+}
+
+impl std::cmp::PartialEq for DoubleVar {
+ fn eq(&self, other: &Self) -> bool {
+ self.normal == other.normal
+ }
+}
+
+impl std::cmp::Eq for DoubleVar {}
+
+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()
+ }
+}
+
#[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)),
@@ -66,7 +120,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()),
@@ -94,7 +148,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(
@@ -114,11 +169,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)),
))
@@ -140,7 +195,7 @@ pub(crate) enum Value {
NaturalSuccClosure,
Pi(Label, TypeThunk, TypeThunk),
- Var(V<Label>),
+ Var(DoubleVar),
Const(Const),
BoolLit(bool),
NaturalLit(Natural),
@@ -166,77 +221,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(),
+ if alpha { "_".into() } else { x.clone() },
+ 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(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();
- let a = a.normalize_to_expr();
+ 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)) => {
// Avoid accidental capture of the new `xs` variable
let v = v.shift(1, &Label::from("xs").into());
- let v = v.normalize_to_expr();
- let a = n.normalize_to_expr();
+ 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(),
+ if alpha { "_".into() } else { x.clone() },
+ 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(),
)),
@@ -244,23 +321,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| {
@@ -268,12 +356,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(),
)],
)),
@@ -285,10 +375,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)))
}
}
}
@@ -400,7 +490,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(),
@@ -497,7 +587,7 @@ 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(
@@ -611,11 +701,10 @@ impl Value {
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;
@@ -692,7 +781,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(
@@ -706,7 +795,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(
@@ -793,7 +882,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 {
@@ -804,11 +900,11 @@ 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()
}
}
@@ -850,18 +946,21 @@ impl TypeThunk {
}
}
- pub(crate) fn normalize_to_expr(&self) -> OutputSubExpr {
- self.normalize_nf().normalize_to_expr()
+ 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)),
@@ -1117,7 +1216,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),
_ => {}
}
@@ -1383,6 +1482,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");
@@ -1709,4 +1814,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");
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-06 10:52:50 +0000