diff options
| -rw-r--r-- | dhall/src/expr.rs | 20 | ||||
| -rw-r--r-- | dhall/src/normalize.rs | 214 | ||||
| -rw-r--r-- | dhall/src/tests.rs | 9 | ||||
| -rw-r--r-- | dhall/src/typecheck.rs | 20 |
4 files changed, 194 insertions, 69 deletions
diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs index 5bde68f..90efd39 100644 --- a/dhall/src/expr.rs +++ b/dhall/src/expr.rs @@ -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), @@ -207,16 +211,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 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"); } 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 fc9db9f..fcf4bd8 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 { @@ -73,10 +75,10 @@ impl Type { 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 +150,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 +175,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)), @@ -756,7 +758,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(); |