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

refactor(library/tactic/defeq_simplifier): move VM binding for defeq_simp

Browse source
This commit is contained in:
Leonardo de Moura 2016-06-24 13:24:11 -07:00
parent 4ffdbff68e
commit 2be8fa646c
2 changed files with 22 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
src/library/tactic/defeq_simplifier/defeq_simplifier.cpp
View file

@ -11,6 +11,8 @@ Author: Daniel Selsam
#include "kernel/inductive/inductive.h"
#include "library/trace.h"
#include "library/util.h"
#include "library/vm/vm_expr.h"
#include "library/tactic/tactic_state.h"
#include "library/tactic/defeq_simplifier/defeq_simplifier.h"
#ifndef LEAN_DEFAULT_DEFEQ_SIMPLIFY_MAX_SIMP_ROUNDS
@ -294,9 +296,28 @@ public:
}
};
/* Setup and teardown */
/* Entry point */
expr defeq_simplify(type_context & ctx, defeq_simp_lemmas const & simp_lemmas, expr const & e) {
return defeq_simplify_fn(ctx, simp_lemmas)(e);
}
vm_obj tactic_defeq_simp(vm_obj const & e, vm_obj const & s0) {
tactic_state const & s = to_tactic_state(s0);
try {
metavar_context mctx_tmp = s.mctx();
type_context ctx = mk_type_context_for(s, mctx_tmp);
defeq_simp_lemmas lemmas = get_defeq_simp_lemmas(s.env());
expr new_e = defeq_simplify(ctx, lemmas, to_expr(e));
return mk_tactic_success(to_obj(new_e), s);
} catch (exception & e) {
return mk_tactic_exception(e, s);
}
}
/* Setup and teardown */
void initialize_defeq_simplifier() {
DECLARE_VM_BUILTIN(name({"tactic", "defeq_simp"}), tactic_defeq_simp);
register_trace_class("defeq_simplifier");
register_trace_class(name({"defeq_simplifier", "rewrite"}));
register_trace_class(name({"defeq_simplifier", "failure"}));
@ -326,9 +347,4 @@ void finalize_defeq_simplifier() {
delete g_simplify_max_rewrite_rounds;
delete g_simplify_max_simp_rounds;
}
/* Entry point */
expr defeq_simplify(type_context & ctx, defeq_simp_lemmas const & simp_lemmas, expr const & e) {
return defeq_simplify_fn(ctx, simp_lemmas)(e);
}
}

15
src/library/tactic/tactic_state.cpp
View file

@ -18,7 +18,6 @@ Author: Leonardo de Moura
#include "library/vm/vm_level.h"
#include "library/vm/vm_expr.h"
#include "library/vm/vm_list.h"
#include "library/tactic/defeq_simplifier/defeq_simplifier.h"
#include "library/tactic/tactic_state.h"
namespace lean {
@ -369,19 +368,6 @@ vm_obj tactic_to_expr(vm_obj const & qe, vm_obj const & s) {
return mk_tactic_success(qe, to_tactic_state(s));
}
vm_obj tactic_defeq_simp(vm_obj const & e, vm_obj const & s0) {
tactic_state const & s = to_tactic_state(s0);
try {
metavar_context mctx_tmp = s.mctx();
type_context ctx = mk_type_context_for(s, mctx_tmp);
defeq_simp_lemmas lemmas = get_defeq_simp_lemmas(s.env());
expr new_e = defeq_simplify(ctx, lemmas, to_expr(e));
return mk_tactic_success(to_obj(new_e), s);
} catch (exception & e) {
return mk_tactic_exception(e, s);
}
}
vm_obj rotate_left(unsigned n, tactic_state const & s) {
buffer<expr> gs;
to_buffer(s.goals(), gs);
@ -490,7 +476,6 @@ void initialize_tactic_state() {
DECLARE_VM_BUILTIN(name({"tactic", "get_local"}), tactic_get_local);
DECLARE_VM_BUILTIN(name({"tactic", "local_context"}), tactic_local_context);
DECLARE_VM_BUILTIN(name({"tactic", "to_expr"}), tactic_to_expr);
DECLARE_VM_BUILTIN(name({"tactic", "defeq_simp"}), tactic_defeq_simp);
DECLARE_VM_BUILTIN(name({"tactic", "rotate_left"}), tactic_rotate_left);
DECLARE_VM_BUILTIN(name({"tactic", "get_goals"}), tactic_get_goals);
DECLARE_VM_BUILTIN(name({"tactic", "set_goals"}), tactic_set_goals);