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