From e8560d0dcb6c8051e2059f369258ec4bf07879f3 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 5 May 2019 00:10:58 +0200 Subject: Implement alpha-normalization Closes #12 --- dhall/src/expr.rs | 20 +++-- dhall/src/normalize.rs | 214 +++++++++++++++++++++++++++++++++++++------------ dhall/src/tests.rs | 9 ++- dhall/src/typecheck.rs | 20 ++--- 4 files changed, 194 insertions(+), 69 deletions(-) (limited to 'dhall/src') 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 { + 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