From dd6aae378f59434aa46c6d5045bd6007f22b4942 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 29 Jan 2014 13:27:40 -0800
Subject: [PATCH] fix(library/simplifier): must use metavar_env in is_ceq,
 otherwise it may ceqs that contain metavariables

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/library/simplifier/ceq.cpp   | 16 ++++++++++------
 src/library/simplifier/ceq.h     |  2 +-
 src/library/simplifier/congr.cpp |  3 ++-
 tests/lua/ceq1.lua               |  2 +-
 4 files changed, 14 insertions(+), 9 deletions(-)

diff --git a/src/library/simplifier/ceq.cpp b/src/library/simplifier/ceq.cpp
index 7a12c793c..c897b7e29 100644
--- a/src/library/simplifier/ceq.cpp
+++ b/src/library/simplifier/ceq.cpp
@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include "kernel/kernel.h"
 #include "kernel/free_vars.h"
 #include "kernel/for_each_fn.h"
+#include "kernel/type_checker.h"
 #include "library/expr_pair.h"
 #include "library/ite.h"
 #include "library/kernel_bindings.h"
@@ -16,7 +17,7 @@ Author: Leonardo de Moura
 namespace lean {
 static name g_Hc("Hc"); // auxiliary name for if-then-else
 
-bool is_ceq(ro_environment const & env, expr e);
+bool is_ceq(ro_environment const & env, optional<ro_metavar_env> const & menv, expr e);
 
 /**
    \brief Auxiliary functional object for creating "conditional equations"
@@ -122,7 +123,7 @@ public:
     to_ceqs_fn(ro_environment const & env, optional<ro_metavar_env> const & menv):m_env(env), m_menv(menv), m_idx(0) {}
 
     list<expr_pair> operator()(expr const & e, expr const & H) {
-        return filter(apply(e, H), [&](expr_pair const & p) { return is_ceq(m_env, p.first); });
+        return filter(apply(e, H), [&](expr_pair const & p) { return is_ceq(m_env, m_menv, p.first); });
     }
 };
 
@@ -130,7 +131,7 @@ list<expr_pair> to_ceqs(ro_environment const & env, optional<ro_metavar_env> con
     return to_ceqs_fn(env, menv)(e, H);
 }
 
-bool is_ceq(ro_environment const & env, expr e) {
+bool is_ceq(ro_environment const & env, optional<ro_metavar_env> const & menv, expr e) {
     buffer<bool> found_args;
     // Define a procedure for marking arguments found.
     auto visitor_fn = [&](expr const & e, unsigned offset) {
@@ -147,7 +148,7 @@ bool is_ceq(ro_environment const & env, expr e) {
         }
         return true;
     };
-
+    type_checker tc(env);
     context ctx;
     while (is_pi(e)) {
         if (!found_args.empty()) {
@@ -158,7 +159,7 @@ bool is_ceq(ro_environment const & env, expr e) {
         }
         // If a variable is a proposition, than if doesn't need to occurr in the lhs.
         // So, we mark it as true.
-        found_args.push_back(env->is_proposition(abst_domain(e), ctx));
+        found_args.push_back(tc.is_proposition(abst_domain(e), ctx, menv));
         ctx = extend(ctx, abst_name(e), abst_domain(e));
         e = abst_body(e);
     }
@@ -255,7 +256,10 @@ static int to_ceqs(lua_State * L) {
 
 static int is_ceq(lua_State * L) {
     ro_shared_environment env(L, 1);
-    lua_pushboolean(L, is_ceq(env, to_expr(L, 2)));
+    optional<ro_metavar_env> menv;
+    if (!lua_isnil(L, 2))
+        menv = to_metavar_env(L, 2);
+    lua_pushboolean(L, is_ceq(env, menv, to_expr(L, 3)));
     return 1;
 }
 
diff --git a/src/library/simplifier/ceq.h b/src/library/simplifier/ceq.h
index fce141f82..13bbbe8e9 100644
--- a/src/library/simplifier/ceq.h
+++ b/src/library/simplifier/ceq.h
@@ -41,7 +41,7 @@ list<expr_pair> to_ceqs(ro_environment const & env, optional<ro_metavar_env> con
    Moreover, for <tt>(forall x : A, ceq)</tt>, the variable x must occur in the \c ceq left-hand-size
    when \c A is not a proposition.
 */
-bool is_ceq(ro_environment const & env, expr e);
+bool is_ceq(ro_environment const & env, optional<ro_metavar_env> const & menv, expr e);
 /**
    \brief Return true iff the lhs is identical to the rhs modulo a
    permutation of the conditional equation arguments.
diff --git a/src/library/simplifier/congr.cpp b/src/library/simplifier/congr.cpp
index 7e6dda93a..c0736969d 100644
--- a/src/library/simplifier/congr.cpp
+++ b/src/library/simplifier/congr.cpp
@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #include <utility>
 #include "util/sstream.h"
 #include "kernel/kernel.h"
+#include "kernel/type_checker.h"
 #include "library/equality.h"
 #include "library/simplifier/congr.h"
 
@@ -89,7 +90,7 @@ void congr_theorem_info::display(std::ostream & out) const {
 }
 
 congr_theorem_info check_congr_theorem(ro_environment const & env, expr const & e) {
-    expr t = env->infer_type(e);
+    expr t = type_checker(env).infer_type(e);
     expr b = t;
     unsigned num = 0;
     while (is_pi(b)) {
diff --git a/tests/lua/ceq1.lua b/tests/lua/ceq1.lua
index f4da598c0..7fd69fb1b 100644
--- a/tests/lua/ceq1.lua
+++ b/tests/lua/ceq1.lua
@@ -5,7 +5,7 @@ function show_ceqs(ceqs)
    for i = 1, #ceqs do
       print(ceqs[i][1], ceqs[i][2], is_permutation_ceq(ceqs[i][1]))
       env:type_check(ceqs[i][2])
-      assert(is_ceq(env, ceqs[i][1]))
+      assert(is_ceq(env, nil, ceqs[i][1]))
    end
 end