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

Add static_asserts to template funcs in expr.h & replace.h

Browse source
This commit is contained in:
Soonho Kong 2013-08-02 20:00:26 -07:00
parent fd7f0e9658
commit bac75541dc
2 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/kernel/expr.h
View file

@ -341,6 +341,8 @@ expr copy(expr const & e);
// =======================================
// Update
template<typename F> expr update_app(expr const & e, F f) {
static_assert(std::is_same<typename std::result_of<F(expr const &)>::type, expr>::value,
"update_app: return type of f is not expr");
buffer<expr> new_args;
bool modified = false;
for (expr const & a : args(e)) {
@ -354,6 +356,9 @@ template<typename F> expr update_app(expr const & e, F f) {
return e;
}
template<typename F> expr update_abst(expr const & e, F f) {
static_assert(std::is_same<typename std::result_of<F(expr const &, expr const &)>::type,
std::pair<expr, expr>>::value,
"update_abst: return type of f is not pair<expr, expr>");
expr const & old_t = abst_type(e);
expr const & old_b = abst_body(e);
std::pair<expr, expr> p = f(old_t, old_b);

2
src/kernel/replace.h
View file

@ -21,6 +21,8 @@ namespace lean {
*/
template<typename F>
class replace_fn {
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");
expr_cell_offset_map<expr> m_cache;
F m_f;