From c5e8c10c9d2eb05885aa2e1042017f9fc1c879e0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 20 May 2014 11:53:58 -0700
Subject: [PATCH] fix(library/normalize): bug in normalize

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/library/normalize.cpp | 10 +++++++++-
 tests/lua/expr10.lua      |  8 ++++++++
 2 files changed, 17 insertions(+), 1 deletion(-)
 create mode 100644 tests/lua/expr10.lua

diff --git a/src/library/normalize.cpp b/src/library/normalize.cpp
index 0fe995173..74fc86bdd 100644
--- a/src/library/normalize.cpp
+++ b/src/library/normalize.cpp
@@ -23,6 +23,14 @@ class normalize_fn {
         return update_binding(e, d, b);
     }
 
+    expr normalize_app(expr const & e) {
+        buffer<expr> args;
+        expr f = get_app_rev_args(e, args);
+        for (expr & a : args)
+            a = normalize(a);
+        return mk_rev_app(f, args);
+    }
+
     expr normalize(expr e) {
         e = m_tc.whnf(e);
         switch (e.kind()) {
@@ -34,7 +42,7 @@ class normalize_fn {
         case expr_kind::Lambda: case expr_kind::Pi:
             return normalize_binding(e);
         case expr_kind::App:
-            return update_app(e, app_fn(e), normalize(app_arg(e)));
+            return normalize_app(e);
         }
         lean_unreachable(); // LCOV_EXCL_LINE
     }
diff --git a/tests/lua/expr10.lua b/tests/lua/expr10.lua
new file mode 100644
index 000000000..4145977d7
--- /dev/null
+++ b/tests/lua/expr10.lua
@@ -0,0 +1,8 @@
+local env = environment()
+local f = Local("f", mk_arrow(Bool, Bool, Bool))
+local a = Local("a", Bool)
+local b = Local("b", Bool)
+local x = Local("x", Bool)
+local t = Fun({f, a, b}, f(Fun(x, x)(b), a))
+print(env:normalize(t))
+assert(env:normalize(t) == Fun({f, a, b}, f(b, a)))