From f80106a895497639fe65389a07e96d1f1bb033ee Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 2 Dec 2013 23:02:39 -0800
Subject: [PATCH] chore(*): use 'explicit operator bool' everywhere.

operator bool() may produce unwanted conversions.
For example, we had the following bug in the code base.

...
   object const & obj = find_object(const_name(n));
   if (obj && obj.is_builtin() && obj.get_name() == n)
...

obj.get_name() has type lean::name
n              has type lean::expr

Both have 'operator bool()', then the compiler uses the operator to
convert them to Boolean, and then compare the result.
Of course, this is not our intention.

After this commit, the compiler correctly signs the error.
The correct code is

...
   object const & obj = find_object(const_name(n));
   if (obj && obj.is_builtin() && obj.get_name() == const_name(n))
...

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/frontend.cpp     |  2 +-
 src/frontends/lean/operator_info.h  |  2 +-
 src/frontends/lean/pp.cpp           | 12 ++++++------
 src/kernel/context.h                |  2 +-
 src/kernel/environment.h            |  2 +-
 src/kernel/expr.h                   |  2 +-
 src/kernel/justification.h          |  2 +-
 src/kernel/metavar.cpp              | 16 ++++++++--------
 src/kernel/object.h                 |  2 +-
 src/kernel/occurs.cpp               |  4 ++--
 src/kernel/unification_constraint.h |  2 +-
 src/library/tactic/goal.h           |  2 +-
 src/library/tactic/tactic.h         |  2 +-
 src/util/list.h                     |  2 +-
 src/util/name.h                     |  2 +-
 src/util/optional.h                 |  2 +-
 src/util/sexpr/format.h             |  2 +-
 src/util/sexpr/sexpr.h              |  2 +-
 18 files changed, 31 insertions(+), 31 deletions(-)

diff --git a/src/frontends/lean/frontend.cpp b/src/frontends/lean/frontend.cpp
index 74d6a23c6c..0fd492fdde 100644
--- a/src/frontends/lean/frontend.cpp
+++ b/src/frontends/lean/frontend.cpp
@@ -403,7 +403,7 @@ operator_info frontend::find_op_for(expr const & n, bool unicode) const {
         return r;
     } else {
         object const & obj = find_object(const_name(n));
-        if (obj && obj.is_builtin() && obj.get_name() == n)
+        if (obj && obj.is_builtin() && obj.get_name() == const_name(n))
             return to_ext(m_env).find_op_for(obj.get_value(), unicode);
         else
             return r;
diff --git a/src/frontends/lean/operator_info.h b/src/frontends/lean/operator_info.h
index 686b1dc92d..3daef1d301 100644
--- a/src/frontends/lean/operator_info.h
+++ b/src/frontends/lean/operator_info.h
@@ -46,7 +46,7 @@ public:
 
     friend void swap(operator_info & o1, operator_info & o2) { std::swap(o1.m_ptr, o2.m_ptr); }
 
-    operator bool() const { return m_ptr != nullptr; }
+    explicit operator bool() const { return m_ptr != nullptr; }
 
     friend operator_info infix(name const & op, unsigned precedence);
     friend operator_info infixl(name const & op, unsigned precedence);
diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index e0ee6b92de..282869e469 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -1121,12 +1121,12 @@ class pp_fn {
     }
 
     bool uses_prefix(expr const & e, name const & prefix) {
-        return find(e, [&](expr const & e) {
-                return
-                    (is_constant(e) && is_prefix_of(prefix, const_name(e)))   ||
-                    (is_abstraction(e) && is_prefix_of(prefix, abst_name(e))) ||
-                    (is_let(e) && is_prefix_of(prefix, let_name(e)));
-            });
+        return static_cast<bool>(find(e, [&](expr const & e) {
+                    return
+                        (is_constant(e) && is_prefix_of(prefix, const_name(e)))   ||
+                        (is_abstraction(e) && is_prefix_of(prefix, abst_name(e))) ||
+                        (is_let(e) && is_prefix_of(prefix, let_name(e)));
+                }));
     }
 
     name find_unused_prefix(expr const & e) {
diff --git a/src/kernel/context.h b/src/kernel/context.h
index 92058bc4b6..f9436d926e 100644
--- a/src/kernel/context.h
+++ b/src/kernel/context.h
@@ -39,7 +39,7 @@ public:
     context_entry const & lookup(unsigned vidx) const;
     std::pair<context_entry const &, context> lookup_ext(unsigned vidx) const;
     bool empty() const { return is_nil(m_list); }
-    operator bool() const { return !empty(); }
+    explicit operator bool() const { return !empty(); }
     unsigned size() const { return length(m_list); }
     typedef list<context_entry>::iterator iterator;
     iterator begin() const { return m_list.begin(); }
diff --git a/src/kernel/environment.h b/src/kernel/environment.h
index 7ea90b9b92..9a5c1a6e6a 100644
--- a/src/kernel/environment.h
+++ b/src/kernel/environment.h
@@ -148,7 +148,7 @@ public:
     object const & find_object(name const & n) const;
 
     /** \brief Return true iff the environment has an object with the given name */
-    bool has_object(name const & n) const { return find_object(n); }
+    bool has_object(name const & n) const { return static_cast<bool>(find_object(n)); }
 
     /**
        \brief Return the type of \c e in the given context and this environment.
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index d147efd4ac..4fd952b55b 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -123,7 +123,7 @@ public:
 
     expr_cell * raw() const { return m_ptr; }
 
-    operator bool() const { return m_ptr != nullptr; }
+    explicit operator bool() const { return m_ptr != nullptr; }
 
     friend expr mk_var(unsigned idx);
     friend expr mk_constant(name const & n, expr const & t);
diff --git a/src/kernel/justification.h b/src/kernel/justification.h
index a8434a9bf6..3bd8b97642 100644
--- a/src/kernel/justification.h
+++ b/src/kernel/justification.h
@@ -61,7 +61,7 @@ public:
     justification(justification && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
     ~justification() { if (m_ptr) m_ptr->dec_ref(); }
 
-    operator bool() const { return m_ptr != nullptr; }
+    explicit operator bool() const { return m_ptr != nullptr; }
 
     justification_cell * raw() const { return m_ptr; }
 
diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp
index 6c23de869e..01d5c37f95 100644
--- a/src/kernel/metavar.cpp
+++ b/src/kernel/metavar.cpp
@@ -126,7 +126,7 @@ expr metavar_env::get_type(name const & m) {
 bool metavar_env::has_type(name const & m) const {
     auto it = const_cast<metavar_env*>(this)->m_metavar_data.splay_find(m);
     lean_assert(it);
-    return it->m_type;
+    return static_cast<bool>(it->m_type);
 }
 
 bool metavar_env::has_type(expr const & m) const {
@@ -343,7 +343,7 @@ expr add_inst(expr const & m, unsigned s, expr const & v) {
 }
 
 bool has_local_context(expr const & m) {
-    return metavar_lctx(m);
+    return static_cast<bool>(metavar_lctx(m));
 }
 
 expr pop_meta_context(expr const & m) {
@@ -361,12 +361,12 @@ bool has_metavar(expr const & e, expr const & m, metavar_env const & menv) {
     if (has_metavar(e)) {
         lean_assert(is_metavar(m));
         lean_assert(!menv.is_assigned(m));
-        return find(e, [&](expr const & m2) {
-                return
-                    is_metavar(m2) &&
-                    ((metavar_name(m) == metavar_name(m2)) ||
-                     (menv.is_assigned(m2) && has_metavar(menv.get_subst(m2), m, menv)));
-            });
+        return static_cast<bool>(find(e, [&](expr const & m2) {
+                    return
+                        is_metavar(m2) &&
+                        ((metavar_name(m) == metavar_name(m2)) ||
+                         (menv.is_assigned(m2) && has_metavar(menv.get_subst(m2), m, menv)));
+                }));
     } else {
         return false;
     }
diff --git a/src/kernel/object.h b/src/kernel/object.h
index 51df40ea3e..832c9c06c1 100644
--- a/src/kernel/object.h
+++ b/src/kernel/object.h
@@ -98,7 +98,7 @@ public:
     object & operator=(object const & s) { LEAN_COPY_REF(object, s); }
     object & operator=(object && s) { LEAN_MOVE_REF(object, s); }
 
-    operator bool() const { return m_ptr != nullptr; }
+    explicit operator bool() const { return m_ptr != nullptr; }
 
     object_kind kind() const { return m_ptr->kind(); }
 
diff --git a/src/kernel/occurs.cpp b/src/kernel/occurs.cpp
index 4b6e65edee..1396c6f450 100644
--- a/src/kernel/occurs.cpp
+++ b/src/kernel/occurs.cpp
@@ -9,11 +9,11 @@ Author: Leonardo de Moura
 
 namespace lean {
 bool occurs(name const & n, context const * c, unsigned sz, expr const * es) {
-    return find(c, sz, es, [&](expr const & e) { return is_constant(e) && const_name(e) == n; });
+    return static_cast<bool>(find(c, sz, es, [&](expr const & e) { return is_constant(e) && const_name(e) == n; }));
 }
 
 bool occurs(expr const & n, context const * c, unsigned sz, expr const * es) {
-    return find(c, sz, es, [&](expr const & e) { return e == n; });
+    return static_cast<bool>(find(c, sz, es, [&](expr const & e) { return e == n; }));
 }
 bool occurs(expr const & n, expr const & m) { return occurs(n, nullptr, 1, &m); }
 bool occurs(name const & n, expr const & m) { return occurs(n, nullptr, 1, &m); }
diff --git a/src/kernel/unification_constraint.h b/src/kernel/unification_constraint.h
index d635f541d8..de2c279e48 100644
--- a/src/kernel/unification_constraint.h
+++ b/src/kernel/unification_constraint.h
@@ -69,7 +69,7 @@ public:
     unification_constraint_kind kind() const { return m_ptr->kind(); }
     unification_constraint_cell * raw() const { return m_ptr; }
 
-    operator bool() const { return m_ptr != nullptr; }
+    explicit operator bool() const { return m_ptr != nullptr; }
 
     format pp(formatter const & fmt, options const & opts, pos_info_provider const * p = nullptr, bool include_justification = false) const {
         lean_assert(m_ptr);
diff --git a/src/library/tactic/goal.h b/src/library/tactic/goal.h
index fedded9bdb..48b47c3c75 100644
--- a/src/library/tactic/goal.h
+++ b/src/library/tactic/goal.h
@@ -26,7 +26,7 @@ public:
     goal(hypotheses const & hs, expr const & c);
     hypotheses const & get_hypotheses() const { return m_hypotheses; }
     expr const & get_conclusion() const { return m_conclusion; }
-    operator bool() const { return m_conclusion; }
+    explicit operator bool() const { return static_cast<bool>(m_conclusion); }
     format pp(formatter const & fmt, options const & opts) const;
     name mk_unique_hypothesis_name(name const & suggestion) const;
 };
diff --git a/src/library/tactic/tactic.h b/src/library/tactic/tactic.h
index acf1139d0f..66606ab7d2 100644
--- a/src/library/tactic/tactic.h
+++ b/src/library/tactic/tactic.h
@@ -74,7 +74,7 @@ public:
     tactic(tactic const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
     tactic(tactic && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
     ~tactic() { if (m_ptr) m_ptr->dec_ref(); }
-    operator bool() const { return m_ptr != nullptr; }
+    explicit operator bool() const { return m_ptr != nullptr; }
     friend void swap(tactic & a, tactic & b) { std::swap(a.m_ptr, b.m_ptr); }
     tactic & operator=(tactic const & s);
     tactic & operator=(tactic && s);
diff --git a/src/util/list.h b/src/util/list.h
index 33321b1326..21bdb0a6e7 100644
--- a/src/util/list.h
+++ b/src/util/list.h
@@ -79,7 +79,7 @@ public:
     cell * raw() const { return m_ptr; }
 
     /** \brief Return true iff it is not the empty/nil list. */
-    operator bool() const { return m_ptr != nullptr; }
+    explicit operator bool() const { return m_ptr != nullptr; }
 
     friend bool is_nil(list const & l) { return l.m_ptr == nullptr; }
     friend bool empty(list const & l) { return is_nil(l); }
diff --git a/src/util/name.h b/src/util/name.h
index fc8ee0d768..2a8be053d3 100644
--- a/src/util/name.h
+++ b/src/util/name.h
@@ -74,7 +74,7 @@ public:
     bool is_anonymous() const { return kind() == name_kind::ANONYMOUS; }
     bool is_string() const    { return kind() == name_kind::STRING; }
     bool is_numeral() const   { return kind() == name_kind::NUMERAL; }
-    operator bool() const     { return !is_anonymous(); }
+    explicit operator bool() const     { return !is_anonymous(); }
     unsigned get_numeral() const;
     /**
        \brief If the tail of the given hierarchical name is a string, then it returns this string.
diff --git a/src/util/optional.h b/src/util/optional.h
index 76db77b814..8761fc51d9 100644
--- a/src/util/optional.h
+++ b/src/util/optional.h
@@ -40,7 +40,7 @@ public:
             m_value.~T();
     }
 
-    operator bool() const { return m_some; }
+    explicit operator bool() const { return m_some; }
     T const * operator->() const { lean_assert(m_some); return &m_value; }
     T * operator->() { lean_assert(m_some); return &m_value; }
     T const & operator*() const { lean_assert(m_some); return m_value; }
diff --git a/src/util/sexpr/format.h b/src/util/sexpr/format.h
index 75fbf8a04e..798637ef2d 100644
--- a/src/util/sexpr/format.h
+++ b/src/util/sexpr/format.h
@@ -186,7 +186,7 @@ public:
     }
     unsigned hash() const { return m_value.hash(); }
 
-    operator bool() const { return m_value; }
+    explicit operator bool() const { return static_cast<bool>(m_value); }
 
     friend format compose(format const & f1, format const & f2);
     friend format nest(int i, format const & f);
diff --git a/src/util/sexpr/sexpr.h b/src/util/sexpr/sexpr.h
index cfaa6c6ad7..b8d0023ea4 100644
--- a/src/util/sexpr/sexpr.h
+++ b/src/util/sexpr/sexpr.h
@@ -60,7 +60,7 @@ public:
 
     sexpr_kind kind() const;
 
-    operator bool() const { return m_ptr != nullptr; }
+    explicit operator bool() const { return m_ptr != nullptr; }
 
     friend bool is_nil(sexpr const & s) { return s.m_ptr == nullptr; }
     friend sexpr const & head(sexpr const & s);