From a9eb2a9307e116f3af03197780ac2084db5dbb31 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 29 Nov 2013 11:35:58 -0800 Subject: [PATCH] feat(kernel/builtin): add is_* functions Signed-off-by: Leonardo de Moura --- src/kernel/builtin.cpp | 36 +++++++++++++++++++++++--- src/kernel/builtin.h | 45 +++++++++++++++++++++++++++++++++ src/library/kernel_bindings.cpp | 2 ++ src/library/tactic/boolean.cpp | 22 +++------------- 4 files changed, 83 insertions(+), 22 deletions(-) diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp index 5b37b9f84..da6fa2c21 100644 --- a/src/kernel/builtin.cpp +++ b/src/kernel/builtin.cpp @@ -66,9 +66,7 @@ public: }; expr const Bool = mk_value(*(new bool_type_value())); expr mk_bool_type() { return Bool; } -bool is_bool(expr const & e) { - return e == Bool || (is_constant(e) && const_name(e) == to_value(Bool).get_name()); -} +MK_IS_BUILTIN(is_bool, Bool) // ======================================= // ======================================= @@ -153,16 +151,48 @@ public: } }; MK_BUILTIN(if_fn, if_fn_value); +MK_IS_BUILTIN(is_if_fn, mk_if_fn()); +bool is_if(expr const & n, expr & c, expr & t, expr & e) { + if (is_if(n)) { + c = arg(n, 2); + t = arg(n, 3); + e = arg(n, 4); + return true; + } else { + return false; + } +} // ======================================= 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")); MK_CONSTANT(homo_eq_fn, name("eq")); +bool is_homo_eq(expr const & e, expr & lhs, expr & rhs) { + if (is_homo_eq(e)) { + lhs = arg(e, 2); + rhs = arg(e, 3); + return true; + } else { + return false; + } +} // Axioms MK_CONSTANT(mp_fn, name("MP")); diff --git a/src/kernel/builtin.h b/src/kernel/builtin.h index 6d194d275..05cbdea01 100644 --- a/src/kernel/builtin.h +++ b/src/kernel/builtin.h @@ -51,6 +51,9 @@ bool is_false(expr const & e); /** \brief Return the Lean If-Then-Else operator. It has type: pi (A : Type), bool -> A -> A -> A */ expr mk_if_fn(); +bool is_if_fn(expr const & e); +inline bool is_if(expr const & e) { return is_app(e) && is_if_fn(arg(e, 0)); } +bool is_if(expr const & n, expr & c, expr & t, expr & e); /** \brief Return the term (if A c t e) */ inline expr mk_if(expr const & A, expr const & c, expr const & t, expr const & e) { return mk_app(mk_if_fn(), A, c, t, e); } inline expr If(expr const & A, expr const & c, expr const & t, expr const & e) { return mk_if(A, c, t, e); } @@ -60,6 +63,9 @@ inline expr bIf(expr const & c, expr const & t, expr const & e) { return mk_bool /** \brief Return the Lean Implies operator */ 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); } @@ -68,6 +74,9 @@ inline expr Implies(std::initializer_list const & l) { return mk_implies(l /** \brief Return the Lean Iff operator */ expr mk_iff_fn(); +bool is_iff_fn(expr const & e); +inline bool is_iff(expr const & e) { return is_app(e) && is_iff_fn(arg(e, 0)); } +bool is_iff(expr const & e, expr & a1, expr & a2); /** \brief Return (e1 iff e2) */ inline expr mk_iff(expr const & e1, expr const & e2) { return mk_app(mk_iff_fn(), e1, e2); } inline expr mk_iff(unsigned num_args, expr const * args) { return mk_bin_rop(mk_iff_fn(), True, num_args, args); } @@ -76,6 +85,9 @@ inline expr Iff(std::initializer_list const & l) { return mk_iff(l.size(), /** \brief Return the Lean And operator */ 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); } @@ -84,6 +96,9 @@ inline expr And(std::initializer_list const & l) { return mk_and(l.size(), /** \brief Return the Lean Or operator */ 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); } @@ -92,24 +107,34 @@ inline expr Or(std::initializer_list const & l) { return mk_or(l.size(), l /** \brief Return the Lean not operator */ 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); } /** \brief Return the Lean forall operator. It has type: Pi (A : Type), (A -> bool) -> Bool */ expr mk_forall_fn(); +bool is_forall_fn(expr const & e); +inline bool is_forall(expr const & e) { return is_app(e) && is_forall_fn(arg(e, 0)); } /** \brief Return the term (Forall A P), where A is a type and P : A -> bool */ inline expr mk_forall(expr const & A, expr const & P) { return mk_app(mk_forall_fn(), A, P); } inline expr Forall(expr const & A, expr const & P) { return mk_forall(A, P); } /** \brief Return the Lean exists operator. It has type: Pi (A : Type), (A -> Bool) -> Bool */ expr mk_exists_fn(); +bool is_exists_fn(expr const & e); +inline bool is_exists(expr const & e) { return is_app(e) && is_exists_fn(arg(e, 0)); } /** \brief Return the term (exists A P), where A is a type and P : A -> bool */ inline expr mk_exists(expr const & A, expr const & P) { return mk_app(mk_exists_fn(), A, P); } inline expr Exists(expr const & A, expr const & P) { return mk_exists(A, P); } /** \brief Homogeneous equality. It has type: Pi (A : Type), A -> A -> Bool */ expr mk_homo_eq_fn(); +bool is_homo_eq_fn(expr const & e); +inline bool is_homo_eq(expr const & e) { return is_app(e) && is_homo_eq_fn(arg(e, 0)); } +bool is_homo_eq(expr const & e, expr & a1, expr & a2); /** \brief Return the term (homo_eq A l r) */ inline expr mk_homo_eq(expr const & A, expr const & l, expr const & r) { return mk_app(mk_homo_eq_fn(), A, l, r); } inline expr hEq(expr const & A, expr const & l, expr const & r) { return mk_homo_eq(A, l, r); } @@ -177,5 +202,25 @@ static name Name ## _name = NameObj; \ expr mk_##Name() { \ static thread_local expr r = mk_constant(Name ## _name); \ return r ; \ +} \ +bool is_ ## Name(expr const & e) { \ + return is_constant(e) && const_name(e) == Name ## _name; \ +} + +#define MK_IS_BUILTIN(Name, Builtin) \ +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; \ + } \ } } diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index 2b4515454..d720b6a08 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -1560,6 +1560,8 @@ static void open_metavar_env(lua_State * L) { SET_GLOBAL_FUN(instantiate_metavars, "instantiate_metavars"); } + + void open_kernel_module(lua_State * L) { open_level(L); open_local_context(L); diff --git a/src/library/tactic/boolean.cpp b/src/library/tactic/boolean.cpp index 9b1cbe40f..68f64de60 100644 --- a/src/library/tactic/boolean.cpp +++ b/src/library/tactic/boolean.cpp @@ -16,23 +16,8 @@ Author: Leonardo de Moura #include "library/tactic/tactic.h" namespace lean { -bool is_app_of(expr const & e, expr const & f) { - return is_app(e) && arg(e, 0) == f; -} - -bool is_app_of(expr const & e, expr const & f, expr & arg1, expr & arg2) { - if (is_app_of(e, f)) { - arg1 = arg(e, 1); - arg2 = arg(e, 2); - return true; - } else { - return false; - } -} - tactic conj_tactic(bool all) { return mk_tactic01([=](environment const &, io_state const &, proof_state const & s) -> optional { - expr andfn = mk_and_fn(); bool found = false; buffer> new_goals_buf; list> proof_info; @@ -41,7 +26,7 @@ tactic conj_tactic(bool all) { goal const & g = p.second; expr const & c = g.get_conclusion(); expr c1, c2; - if ((all || !found) && is_app_of(c, andfn, c1, c2)) { + if ((all || !found) && is_and(c, c1, c2)) { found = true; name const & n = p.first; proof_info.emplace_front(n, c); @@ -80,7 +65,7 @@ tactic imp_tactic(name const & H_name, bool all) { goals new_goals = map_goals(s, [&](name const & g_name, goal const & g) -> goal { expr const & c = g.get_conclusion(); expr new_h, new_c; - if ((all || !found) && is_app_of(c, impfn, new_h, new_c)) { + if ((all || !found) && is_implies(c, new_h, new_c)) { found = true; name new_h_name = g.mk_unique_hypothesis_name(H_name); proof_info.emplace_front(g_name, new_h_name, c); @@ -113,7 +98,6 @@ tactic imp_tactic(name const & H_name, bool all) { tactic conj_hyp_tactic(bool all) { return mk_tactic01([=](environment const &, io_state const &, proof_state const & s) -> optional { - expr andfn = mk_and_fn(); bool found = false; list> proof_info; // goal name -> expanded hypotheses goals new_goals = map_goals(s, [&](name const & ng, goal const & g) -> goal { @@ -124,7 +108,7 @@ tactic conj_hyp_tactic(bool all) { name const & H_name = p.first; expr const & H_prop = p.second; expr H1, H2; - if ((all || !found) && is_app_of(H_prop, andfn, H1, H2)) { + if ((all || !found) && is_and(H_prop, H1, H2)) { found = true; proof_info_data = add_hypothesis(p, proof_info_data); new_hyp_buf.emplace_back(name(H_name, 1), H1);