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

refactor(kernel/builtin): remove unnecessary predicates

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-29 12:20:29 -08:00
parent ac9801c7d7
commit df3686634d
4 changed files with 14 additions and 41 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/kernel/builtin.cpp
View file

@ -174,22 +174,10 @@ bool is_if(expr const & n, expr & c, expr & t, expr & e) {
// =======================================
MK_CONSTANT(implies_fn, name("implies"));
MK_IS_BINARY_APP(is_implies)
MK_CONSTANT(iff_fn, name("iff"));
MK_IS_BINARY_APP(is_iff)
MK_CONSTANT(and_fn, name("and"));
MK_IS_BINARY_APP(is_and)
MK_CONSTANT(or_fn, name("or"));
MK_IS_BINARY_APP(is_or)
MK_CONSTANT(not_fn, name("not"));
bool is_not(expr const & e, expr & a) {
if (is_not(e)) {
a = arg(e, 1);
return true;
} else {
return false;
}
}
MK_CONSTANT(forall_fn, name("forall"));
MK_CONSTANT(exists_fn, name("exists"));

15
src/kernel/builtin.h
View file

@ -65,7 +65,6 @@ inline expr bIf(expr const & c, expr const & t, expr const & e) { return mk_bool
expr mk_implies_fn();
bool is_implies_fn(expr const & e);
inline bool is_implies(expr const & e) { return is_app(e) && is_implies_fn(arg(e, 0)); }
bool is_implies(expr const & e, expr & a1, expr & a2);
/** \brief Return the term (e1 => e2) */
inline expr mk_implies(expr const & e1, expr const & e2) { return mk_app(mk_implies_fn(), e1, e2); }
inline expr mk_implies(unsigned num_args, expr const * args) { lean_assert(num_args >= 2); return mk_bin_rop(mk_implies_fn(), False, num_args, args); }
@ -87,7 +86,6 @@ inline expr Iff(std::initializer_list<expr> const & l) { return mk_iff(l.size(),
expr mk_and_fn();
bool is_and_fn(expr const & e);
inline bool is_and(expr const & e) { return is_app(e) && is_and_fn(arg(e, 0)); }
bool is_and(expr const & e, expr & a1, expr & a2);
/** \brief Return (e1 and e2) */
inline expr mk_and(expr const & e1, expr const & e2) { return mk_app(mk_and_fn(), e1, e2); }
inline expr mk_and(unsigned num_args, expr const * args) { return mk_bin_rop(mk_and_fn(), True, num_args, args); }
@ -98,7 +96,6 @@ inline expr And(std::initializer_list<expr> const & l) { return mk_and(l.size(),
expr mk_or_fn();
bool is_or_fn(expr const & e);
inline bool is_or(expr const & e) { return is_app(e) && is_or_fn(arg(e, 0)); }
bool is_or(expr const & e, expr & a1, expr & a2);
/** \brief Return (e1 Or e2) */
inline expr mk_or(expr const & e1, expr const & e2) { return mk_app(mk_or_fn(), e1, e2); }
inline expr mk_or(unsigned num_args, expr const * args) { return mk_bin_rop(mk_or_fn(), False, num_args, args); }
@ -109,7 +106,6 @@ inline expr Or(std::initializer_list<expr> const & l) { return mk_or(l.size(), l
expr mk_not_fn();
bool is_not_fn(expr const & e);
inline bool is_not(expr const & e) { return is_app(e) && is_not_fn(arg(e, 0)); }
bool is_not(expr const & e, expr & a1);
/** \brief Return (Not e) */
inline expr mk_not(expr const & e) { return mk_app(mk_not_fn(), e); }
inline expr Not(expr const & e) { return mk_not(e); }
@ -224,15 +220,4 @@ bool Name(expr const & e) { \
expr const & v = Builtin; \
return e == v || (is_constant(e) && const_name(e) == to_value(v).get_name()); \
}
#define MK_IS_BINARY_APP(Name) \
bool Name(expr const & e, expr & a1, expr & a2) { \
if (Name(e)) { \
a1 = arg(e, 1); \
a2 = arg(e, 2); \
return true; \
} else { \
return false; \
} \
}
}

4
src/library/basic_thms.cpp
View file

@ -5,13 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "kernel/environment.h"
#include "kernel/abstract.h"
#include "kernel/type_checker.h"
#include "library/io_state.h"
#include "library/basic_thms.h"
#include "kernel/kernel_exception.h"
namespace lean {
MK_CONSTANT(trivial, name("Trivial"));

24
src/library/tactic/boolean_tactics.cpp
View file

@ -25,8 +25,9 @@ tactic conj_tactic(bool all) {
check_interrupted();
goal const & g = p.second;
expr const & c = g.get_conclusion();
expr c1, c2;
if ((all || !found) && is_and(c, c1, c2)) {
if ((all || !found) && is_and(c)) {
expr c1 = arg(c, 1);
expr c2 = arg(c, 2);
found = true;
name const & n = p.first;
proof_info.emplace_front(n, c);
@ -64,8 +65,9 @@ tactic imp_tactic(name const & H_name, bool all) {
list<std::tuple<name, name, expr>> proof_info;
goals new_goals = map_goals(s, [&](name const & g_name, goal const & g) -> optional<goal> {
expr const & c = g.get_conclusion();
expr new_h, new_c;
if ((all || !found) && is_implies(c, new_h, new_c)) {
if ((all || !found) && is_implies(c)) {
expr new_h = arg(c, 1);
expr new_c = arg(c, 2);
found = true;
name new_h_name = g.mk_unique_hypothesis_name(H_name);
proof_info.emplace_front(g_name, new_h_name, c);
@ -107,8 +109,9 @@ tactic conj_hyp_tactic(bool all) {
for (auto const & p : g.get_hypotheses()) {
name const & H_name = p.first;
expr const & H_prop = p.second;
expr H1, H2;
if ((all || !found) && is_and(H_prop, H1, H2)) {
if ((all || !found) && is_and(H_prop)) {
expr H1 = arg(H_prop, 1);
expr H2 = arg(H_prop, 2);
found = true;
proof_info_data = add_hypothesis(p, proof_info_data);
new_hyp_buf.emplace_back(name(H_name, 1), H1);
@ -257,8 +260,9 @@ optional<proof_state_pair> disj_tactic(proof_state const & s, name gname) {
if (!conclusion && ((gname.is_anonymous() && is_or(c)) || p.first == gname)) {
gname = p.first;
conclusion = c;
expr c1, c2;
if (is_or(c, c1, c2)) {
if (is_or(c)) {
expr c1 = arg(c, 1);
expr c2 = arg(c, 2);
new_goals_buf1.emplace_back(gname, update(g, c1));
new_goals_buf2.emplace_back(gname, update(g, c2));
} else {
@ -328,8 +332,8 @@ tactic absurd_tactic() {
expr const & c = g.get_conclusion();
for (auto const & p1 : g.get_hypotheses()) {
check_interrupted();
expr a;
if (is_not(p1.second, a)) {
if (is_not(p1.second)) {
expr a = arg(p1.second, 1);
for (auto const & p2 : g.get_hypotheses()) {
if (p2.second == a) {
expr pr = AbsurdElim(a, c, mk_constant(p2.first), mk_constant(p1.first));