From 12e7626c9fd8c1c1699bc0043b6524704dc6be82 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 24 Dec 2019 22:08:22 +0000
Subject: Ensure normalization respects var names on the nose
---
dhall/build.rs | 1 +
dhall/src/semantics/phase/normalize.rs | 16 ++++++++--------
dhall/src/tests.rs | 15 +++++----------
3 files changed, 14 insertions(+), 18 deletions(-)
(limited to 'dhall')
diff --git a/dhall/build.rs b/dhall/build.rs
index 9b00684..b88c71f 100644
--- a/dhall/build.rs
+++ b/dhall/build.rs
@@ -285,6 +285,7 @@ fn generate_tests() -> std::io::Result<()> {
// TODO: waiting for https://github.com/dhall-lang/dhall-lang/pull/871
|| path == "unit/MergeNone"
|| path == "unit/MergeSome"
+ || path == "unit/NaturalBuildFoldFusion"
}),
input_type: FileType::Text,
output_type: Some(FileType::Text),
diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs
index 459eaf1..bf0c626 100644
--- a/dhall/src/semantics/phase/normalize.rs
+++ b/dhall/src/semantics/phase/normalize.rs
@@ -24,7 +24,7 @@ macro_rules! make_closure {
.into_value_with_type(make_closure!($($ty)*))
}};
// Warning: assumes that $ty, as a dhall value, has type `Type`
- (λ($var:ident : $($ty:tt)*) -> $($body:tt)*) => {{
+ (λ($var:tt : $($ty:tt)*) -> $($body:tt)*) => {{
let var: AlphaLabel = Label::from(stringify!($var)).into();
let ty = make_closure!($($ty)*);
let body = make_closure!($($body)*);
@@ -276,12 +276,12 @@ pub(crate) fn apply_builtin(
f.app(list_t.clone())
.app({
// Move `t` under new variables
- let t1 = t.under_binder(Label::from("x"));
- let t2 = t1.under_binder(Label::from("xs"));
+ let t1 = t.under_binder(Label::from("a"));
+ let t2 = t1.under_binder(Label::from("as"));
make_closure!(
- λ(x : #t) ->
- λ(xs : List #t1) ->
- [ var(x, 1, #t2) ] # var(xs, 0, List #t2)
+ λ(a : #t) ->
+ λ(as : List #t1) ->
+ [ var(a, 1, #t2) ] # var(as, 0, List #t2)
)
})
.app(EmptyListLit(t.clone()).into_value_with_type(list_t)),
@@ -303,8 +303,8 @@ pub(crate) fn apply_builtin(
Ret::Value(
f.app(optional_t.clone())
.app({
- let t1 = t.under_binder(Label::from("x"));
- make_closure!(λ(x: #t) -> Some(var(x, 0, #t1)))
+ let t1 = t.under_binder(Label::from("a"));
+ make_closure!(λ(a: #t) -> Some(var(a, 0, #t1)))
})
.app(
EmptyOptionalLit(t.clone())
diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs
index 0163c4d..f1648cf 100644
--- a/dhall/src/tests.rs
+++ b/dhall/src/tests.rs
@@ -206,11 +206,9 @@ pub fn run_test(test: Test<'_>) -> Result<()> {
let expr = parse_file_str(&expr_file_path)?
.resolve()?
.typecheck()?
- .normalize();
- let expected = parse_file_str(&expected_file_path)?
- .resolve()?
- .typecheck()?
- .normalize();
+ .normalize()
+ .to_expr();
+ let expected = parse_file_str(&expected_file_path)?.to_expr();
assert_eq_display!(expr, expected);
}
@@ -220,12 +218,9 @@ pub fn run_test(test: Test<'_>) -> Result<()> {
.typecheck()?
.normalize()
.to_expr_alpha();
- let expected = parse_file_str(&expected_file_path)?
- .resolve()?
- .typecheck()?
- .normalize();
+ let expected = parse_file_str(&expected_file_path)?.to_expr();
- assert_eq_display!(expr, expected.to_expr());
+ assert_eq_display!(expr, expected);
}
}
Ok(())
--
cgit v1.2.3