max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/tactic/simplify): simp default behavior should eliminate annotations

Browse source
This commit is contained in:
Leonardo de Moura 2017-03-27 15:10:47 -07:00
parent 68c1ff6219
commit 34f6a92e24
2 changed files with 13 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/library/tactic/simplify.cpp
View file

@ -17,6 +17,7 @@ Author: Daniel Selsam, Leonardo de Moura
#include "kernel/find_fn.h"
#include "kernel/instantiate.h"
#include "library/trace.h"
#include "library/annotation.h"
#include "library/pp_options.h"
#include "library/constants.h"
#include "library/normalize.h"
@ -726,9 +727,11 @@ simp_result simplify_core_fn::visit(expr const & e, optional<expr> const & paren
case expr_kind::Meta:
case expr_kind::Sort:
case expr_kind::Constant:
case expr_kind::Macro:
new_result = curr_result;
break;
case expr_kind::Macro:
new_result = join(curr_result, visit_macro(curr_result.get_new()));
break;
case expr_kind::Var:
lean_unreachable();
case expr_kind::Lambda:
@ -1059,6 +1062,14 @@ simp_result simplify_ext_core_fn::visit_pi(expr const & e) {
return simplify_core_fn::visit_pi(e);
}
simp_result simplify_ext_core_fn::visit_macro(expr const & e) {
if (is_annotation(e)) {
return visit(get_annotation_arg(e), none_expr());
} else {
return simplify_core_fn::visit_macro(e);
}
}
simp_result simplify_ext_core_fn::visit_let(expr const & e) {
/* TODO(Leo): when m_zeta is false, we need to implement efficient code for checking whether the abstraction of
a let-body is type correct or not */

1
src/library/tactic/simplify.h
View file

@ -145,6 +145,7 @@ protected:
virtual simp_result visit_lambda(expr const & e) override;
virtual simp_result visit_pi(expr const & e) override;
virtual simp_result visit_let(expr const & e) override;
virtual simp_result visit_macro(expr const & e) override;
public:
simplify_ext_core_fn(type_context & ctx, defeq_canonizer::state & dcs, simp_lemmas const & slss,
simp_config const & cfg);