michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(kernel): add static_assert to expr,expr_eq,replace

Browse source
This commit is contained in:
Soonho Kong 2013-10-01 16:39:52 -07:00
parent b823c7d779
commit e3b762e909
3 changed files with 17 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/kernel/expr.h
View file

@ -583,6 +583,9 @@ template<typename F> expr update_eq(expr const & e, F f) {
return e; return e;
} }
template<typename F> expr update_metavar(expr const & e, unsigned i, F f) { template<typename F> expr update_metavar(expr const & e, unsigned i, F f) {
static_assert(std::is_same<typename std::result_of<F(meta_entry const &)>::type,
meta_entry>::value,
"update_metavar: return type of f(meta_entry) is not meta_entry");
buffer<meta_entry> new_entries; buffer<meta_entry> new_entries;
bool modified = (i != metavar_idx(e)); bool modified = (i != metavar_idx(e));
for (meta_entry const & me : metavar_ctx(e)) { for (meta_entry const & me : metavar_ctx(e)) {
@ -603,6 +606,9 @@ template<typename F> expr update_metavar(expr const & e, unsigned i, F f) {
return e; return e;
} }
template<typename F> expr update_metavar(expr const & e, F f) { template<typename F> expr update_metavar(expr const & e, F f) {
static_assert(std::is_same<typename std::result_of<F(meta_entry const &)>::type,
meta_entry>::value,
"update_metavar: return type of f(meta_entry) is not meta_entry");
return update_metavar(e, metavar_idx(e), f); return update_metavar(e, metavar_idx(e), f);
} }
// ======================================= // =======================================

7
src/kernel/expr_eq.h
View file

@ -71,7 +71,12 @@ class expr_eq_fn {
lean_unreachable(); lean_unreachable();
} }
public: public:
expr_eq_fn(N const & norm = N()):m_norm(norm) {} expr_eq_fn(N const & norm = N()):m_norm(norm) {
// the return type of N()(e) should be expr const &
static_assert(std::is_same<typename std::result_of<decltype(std::declval<N>())(expr const &)>::type,
expr const &>::value,
"The return type of CMP()(k1, k2) is not int.");
}
bool operator()(expr const & a, expr const & b) { bool operator()(expr const & a, expr const & b) {
return apply(a, b); return apply(a, b);
} }

5
src/kernel/replace.h
View file

@ -36,6 +36,11 @@ template<typename F, typename P = default_replace_postprocessor>
class replace_fn { class replace_fn {
static_assert(std::is_same<typename std::result_of<F(expr const &, unsigned)>::type, expr>::value, static_assert(std::is_same<typename std::result_of<F(expr const &, unsigned)>::type, expr>::value,
"replace_fn: return type of F is not expr"); "replace_fn: return type of F is not expr");
// the return type of P()(e1, e2) should be void
static_assert(std::is_same<typename std::result_of<decltype(std::declval<P>())(expr const &, expr const &)>::type,
void>::value,
"The return type of P()(e1, e2) is not void");
expr_cell_offset_map<expr> m_cache; expr_cell_offset_map<expr> m_cache;
F m_f; F m_f;
P m_post; P m_post;