fix(kernel): add declarations for operator<<(std::ostream&, expr const&) and operator<<(std::ostream&, context const&) in the kernel

The actual implementation of these two operators is outside of the
kernel. They are implemented in the file 'library/printer.cpp'.
We declare them in the kernel to prevent the following problem.
Suppose there is a file 'foo.cpp' that does not include
'library/printer.h', but contains

    expr a;
    ...
    std::cout << a << "\n";
    ...

The compiler does not generate an error message. It silently uses the
operator bool() to coerce the expression into a Boolean. This produces
counter-intuitive behavior, and may confuse developers.
This commit is contained in:
Leonardo de Moura 2013-09-25 17:45:13 -07:00
parent 4a66712ef2
commit 9f0dab1add
2 changed files with 8 additions and 0 deletions

View file

@ -59,4 +59,8 @@ inline context_entry const & lookup(context const & c, unsigned i) { return c.lo
inline context extend(context const & c, name const & n, expr const & d, expr const & b) { return context(c, n, d, b); }
inline context extend(context const & c, name const & n, expr const & d) { return context(c, n, d); }
inline bool empty(context const & c) { return c.empty(); }
// Remark: the implementation is at library/printer.cpp
// We add the definition here to prevent the compiler from using the coercion to bool.
std::ostream & operator<<(std::ostream & out, context const & ctx);
}

View file

@ -604,4 +604,8 @@ template<typename F> expr update_metavar(expr const & e, F f) {
return update_metavar(e, metavar_idx(e), f);
}
// =======================================
// Remark: the implementation is at library/printer.cpp
// We add the definition here to prevent the compiler from using the coercion to bool.
std::ostream & operator<<(std::ostream & out, expr const & e);
}