From 5ff200c516dc1cd47012bdf2ae53821199df57d1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 14 Oct 2014 15:55:52 -0700 Subject: [PATCH] chore(library/simplifier): delete old simplifier This was the simplifier used in Lean 0.1. --- src/CMakeLists.txt | 2 - src/library/simplifier/CMakeLists.txt | 2 - src/library/simplifier/ceq.cpp | 417 ---- src/library/simplifier/ceq.h | 90 - src/library/simplifier/congr.cpp | 202 -- src/library/simplifier/congr.h | 144 -- src/library/simplifier/register_module.h | 22 - src/library/simplifier/rewrite_rule_set.cpp | 381 ---- src/library/simplifier/rewrite_rule_set.h | 153 -- src/library/simplifier/simplifier.cpp | 1903 ------------------- src/library/simplifier/simplifier.h | 165 -- 11 files changed, 3481 deletions(-) delete mode 100644 src/library/simplifier/CMakeLists.txt delete mode 100644 src/library/simplifier/ceq.cpp delete mode 100644 src/library/simplifier/ceq.h delete mode 100644 src/library/simplifier/congr.cpp delete mode 100644 src/library/simplifier/congr.h delete mode 100644 src/library/simplifier/register_module.h delete mode 100644 src/library/simplifier/rewrite_rule_set.cpp delete mode 100644 src/library/simplifier/rewrite_rule_set.h delete mode 100644 src/library/simplifier/simplifier.cpp delete mode 100644 src/library/simplifier/simplifier.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index f9b71b572a..b1416f3dc0 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -319,8 +319,6 @@ add_subdirectory(tests/util/numerics) add_subdirectory(tests/util/interval) add_subdirectory(tests/kernel) add_subdirectory(tests/library) -# add_subdirectory(tests/library/rewriter) -# add_subdirectory(tests/library/tactic) add_subdirectory(tests/frontends/lean) # Include style check diff --git a/src/library/simplifier/CMakeLists.txt b/src/library/simplifier/CMakeLists.txt deleted file mode 100644 index dceec2e0af..0000000000 --- a/src/library/simplifier/CMakeLists.txt +++ /dev/null @@ -1,2 +0,0 @@ -add_library(simplifier ceq.cpp congr.cpp rewrite_rule_set.cpp simplifier.cpp) -target_link_libraries(simplifier ${LEAN_LIBS}) diff --git a/src/library/simplifier/ceq.cpp b/src/library/simplifier/ceq.cpp deleted file mode 100644 index 75ba55032d..0000000000 --- a/src/library/simplifier/ceq.cpp +++ /dev/null @@ -1,417 +0,0 @@ -/* -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include "util/list_fn.h" -#include "kernel/kernel.h" -#include "kernel/free_vars.h" -#include "kernel/for_each_fn.h" -#include "kernel/type_checker.h" -#include "kernel/instantiate.h" -#include "kernel/occurs.h" -#include "library/expr_pair.h" -#include "library/kernel_bindings.h" -#include "library/equality.h" - -namespace lean { -static name g_Hc("Hc"); // auxiliary name for if-then-else - -bool is_ceq(ro_environment const & env, optional const & menv, expr e); - -/** - \brief Auxiliary functional object for creating "conditional equations" -*/ -class to_ceqs_fn { - ro_environment const & m_env; - optional const & m_menv; - unsigned m_idx; - - static list mk_singleton(expr const & e, expr const & H) { - return to_list(mk_pair(e, H)); - } - - expr lift_free_vars(expr const & e, unsigned d) { - return ::lean::lift_free_vars(e, d, m_menv); - } - - name mk_aux_name() { - if (m_idx == 0) { - m_idx = 1; - return g_Hc; - } else { - name r = name(g_Hc, m_idx); - m_idx++; - return r; - } - } - - list apply(expr const & e, expr const & H) { - if (is_equality(e)) { - return mk_singleton(e, H); - } else if (is_neq(e)) { - expr T = arg(e, 1); - expr lhs = arg(e, 2); - expr rhs = arg(e, 3); - expr new_e = mk_iff(mk_eq(T, lhs, rhs), False); - expr new_H = mk_neq_elim_th(T, lhs, rhs, H); - return mk_singleton(new_e, new_H); - } else if (is_not(e)) { - expr a = arg(e, 1); - if (is_not(a)) { - return apply(arg(a, 1), mk_not_not_elim_th(arg(a, 1), H)); - } else if (is_neq(a)) { - return mk_singleton(update_app(a, 0, mk_eq_fn()), - mk_not_neq_elim_th(arg(a, 1), arg(a, 2), arg(a, 3), H)); - } else if (is_or(a)) { - return apply(mk_and(mk_not(arg(a, 1)), mk_not(arg(a, 2))), - mk_not_or_elim_th(arg(a, 1), arg(a, 2), H)); - } else { - expr new_e = mk_iff(a, False); - expr new_H = mk_eqf_intro_th(a, H); - return mk_singleton(new_e, new_H); - } - } else if (is_and(e)) { - expr a1 = arg(e, 1); - expr a2 = arg(e, 2); - expr new_H1 = mk_and_eliml_th(a1, a2, H); - expr new_H2 = mk_and_elimr_th(a1, a2, H); - return append(apply(a1, new_H1), apply(a2, new_H2)); - } else if (is_pi(e)) { - expr new_e = abst_body(e); - expr new_H = mk_app(lift_free_vars(H, 1), mk_var(0)); - auto ceqs = apply(new_e, new_H); - if (length(ceqs) == 1 && new_e == car(ceqs).first) { - return mk_singleton(e, H); - } else { - return map(ceqs, [&](expr_pair const & e_H) -> expr_pair { - expr new_e = mk_pi(abst_name(e), abst_domain(e), e_H.first); - expr new_H = mk_lambda(abst_name(e), abst_domain(e), e_H.second); - return mk_pair(new_e, new_H); - }); - } - } else if (is_ite(e)) { - expr c = arg(e, 2); - expr not_c = mk_not(c); - expr c1 = lift_free_vars(c, 1); - expr a1 = lift_free_vars(arg(e, 3), 1); - expr b1 = lift_free_vars(arg(e, 4), 1); - expr H1 = lift_free_vars(H, 1); - auto then_ceqs = apply(a1, mk_if_imp_then_th(c1, a1, b1, H1, mk_var(0))); - auto else_ceqs = apply(b1, mk_if_imp_else_th(c1, a1, b1, H1, mk_var(0))); - name Hc = mk_aux_name(); - auto new_then_ceqs = map(then_ceqs, [&](expr_pair const & e_H) { - expr new_e = mk_pi(Hc, c, e_H.first); - expr new_H = mk_lambda(Hc, c, e_H.second); - return mk_pair(new_e, new_H); - }); - auto new_else_ceqs = map(else_ceqs, [&](expr_pair const & e_H) { - expr new_e = mk_pi(Hc, not_c, e_H.first); - expr new_H = mk_lambda(Hc, not_c, e_H.second); - return mk_pair(new_e, new_H); - }); - return append(new_then_ceqs, new_else_ceqs); - } else { - return mk_singleton(mk_iff(e, True), mk_eqt_intro_th(e, H)); - } - } -public: - to_ceqs_fn(ro_environment const & env, optional const & menv):m_env(env), m_menv(menv), m_idx(0) {} - - list operator()(expr const & e, expr const & H) { - return filter(apply(e, H), [&](expr_pair const & p) { return is_ceq(m_env, m_menv, p.first); }); - } -}; - -list to_ceqs(ro_environment const & env, optional const & menv, expr const & e, expr const & H) { - return to_ceqs_fn(env, menv)(e, H); -} - -static name g_unique = name::mk_internal_unique_name(); - -bool is_ceq(ro_environment const & env, optional const & menv, expr e) { - buffer found_args; - // Define a procedure for marking arguments found. - auto visitor_fn = [&](expr const & e, unsigned offset) { - if (is_var(e)) { - unsigned vidx = var_idx(e); - if (vidx >= offset) { - vidx -= offset; - if (vidx >= found_args.size()) { - // it is a free variable - } else { - found_args[found_args.size() - vidx - 1] = true; - } - } - } - return true; - }; - type_checker tc(env); - context ctx; - buffer hypothesis; // arguments that are propositions - expr e_prime = e; // in e_prime we replace local variables with fresh constants - unsigned next_idx = 0; - while (is_pi(e)) { - if (!found_args.empty()) { - // Support for dependent types. - // We may find the instantiation for the previous variables - // by matching the type. - for_each(abst_domain(e), visitor_fn); - } - // If a variable is a proposition, than if doesn't need to occurr in the lhs. - // So, we mark it as true. - if (tc.is_proposition(abst_domain(e), ctx, menv)) { - found_args.push_back(true); - hypothesis.push_back(abst_domain(e_prime)); - } else { - found_args.push_back(false); - } - ctx = extend(ctx, abst_name(e), abst_domain(e)); - next_idx++; - e_prime = instantiate(abst_body(e_prime), mk_constant(name(g_unique, next_idx)), menv); - e = abst_body(e); - } - expr lhs, rhs; - if (is_equality(e, lhs, rhs)) { - // traverse lhs, and mark all variables that occur there in is_lhs. - for_each(lhs, visitor_fn); - if (std::find(found_args.begin(), found_args.end(), false) != found_args.end()) - return false; - // basic looping ceq detection: the left-hand-side should not occur in the right-hand-side, - // nor it should occur in any of the hypothesis - expr lhs_prime, rhs_prime; - lean_verify(is_equality(e_prime, lhs_prime, rhs_prime)); - return - !occurs(lhs_prime, rhs_prime) && - std::all_of(hypothesis.begin(), hypothesis.end(), [&](expr const & h) { return !occurs(lhs_prime, h); }); - } else { - return false; - } -} - -static bool is_permutation(expr const & lhs, expr const & rhs, unsigned offset, buffer> & p) { - if (lhs.kind() != rhs.kind()) - return false; - switch (lhs.kind()) { - case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: case expr_kind::MetaVar: - return lhs == rhs; - case expr_kind::Var: - if (var_idx(lhs) < offset) { - return lhs == rhs; // locally bound variable - } else if (var_idx(lhs) - offset < p.size()) { - if (p[var_idx(lhs) - offset]) { - return *(p[var_idx(lhs) - offset]) == var_idx(rhs); - } else { - p[var_idx(lhs) - offset] = var_idx(rhs); - return true; - } - } else { - return lhs == rhs; // free variable - } - case expr_kind::HEq: - return - is_permutation(heq_lhs(lhs), heq_lhs(rhs), offset, p) && - is_permutation(heq_rhs(lhs), heq_rhs(rhs), offset, p); - case expr_kind::Proj: - return proj_first(lhs) == proj_first(rhs) && is_permutation(proj_arg(lhs), proj_arg(rhs), offset, p); - case expr_kind::Pair: - return - is_permutation(pair_first(lhs), pair_first(rhs), offset, p) && - is_permutation(pair_second(lhs), pair_second(rhs), offset, p) && - is_permutation(pair_type(lhs), pair_type(rhs), offset, p); - case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Sigma: - return - is_permutation(abst_domain(lhs), abst_domain(rhs), offset, p) && - is_permutation(abst_body(lhs), abst_body(rhs), offset+1, p); - case expr_kind::App: - if (num_args(lhs) == num_args(rhs)) { - for (unsigned i = 0; i < num_args(lhs); i++) { - if (!is_permutation(arg(lhs, i), arg(rhs, i), offset, p)) - return false; - } - return true; - } else { - return false; - } - case expr_kind::Let: - if (static_cast(let_type(lhs)) != static_cast(let_type(rhs))) - return false; - if (static_cast(let_type(lhs)) && !is_permutation(*let_type(lhs), *let_type(rhs), offset, p)) - return false; - return - is_permutation(let_value(lhs), let_value(rhs), offset, p) && - is_permutation(let_body(lhs), let_value(rhs), offset+1, p); - } - lean_unreachable(); -} - -bool is_permutation_ceq(expr e) { - unsigned num_args = 0; - while (is_pi(e)) { - e = abst_body(e); - num_args++; - } - expr lhs, rhs; - if (is_equality(e, lhs, rhs)) { - buffer> permutation; - permutation.resize(num_args); - return is_permutation(lhs, rhs, 0, permutation); - } else { - return false; - } -} - -// Quick approximate test for e == (Type U). -// If the result is true, then \c e is definitionally equal to TypeU. -// If the result is false, then it may or may not be. -static bool is_TypeU(ro_environment const & env, expr const & e) { - if (is_type(e)) { - return e == TypeU; - } else if (is_constant(e)) { - auto obj = env->find_object(const_name(e)); - return obj && obj->is_definition() && is_TypeU(obj->get_value()); - } else { - return false; - } -} - -bool is_safe_to_skip_check_ceq_types(ro_environment const & env, optional const & menv, expr ceq) { - lean_assert(is_ceq(env, menv, ceq)); - type_checker tc(env); - buffer args; - buffer skip; - unsigned next_idx = 0; - bool to_check = false; - while (is_pi(ceq)) { - expr d = abst_domain(ceq); - expr a = mk_constant(name(g_unique, next_idx), d); - args.push_back(a); - if (tc.is_proposition(d, context(), menv) || - is_TypeU(env, d)) { - // See comment at ceq.h - // 1- The argument has type (Type U). In Lean, (Type U) is the maximal universe. - // 2- The argument is a proposition. - skip.push_back(true); - } else { - skip.push_back(false); - to_check = true; - } - ceq = instantiate(abst_body(ceq), a); - next_idx++; - } - if (!to_check) - return true; - - expr lhs, rhs; - lean_verify(is_equality(ceq, lhs, rhs)); - - auto arg_idx_core_fn = [&](expr const & e) -> optional { - if (is_constant(e)) { - name const & n = const_name(e); - if (!n.is_atomic() && n.get_prefix() == g_unique) { - return some(n.get_numeral()); - } - } - return optional(); - }; - - auto arg_idx_fn = [&](expr const & e) -> optional { - if (is_app(e)) - return arg_idx_core_fn(arg(e, 0)); - else if (is_lambda(e)) - return arg_idx_core_fn(abst_body(e)); - else - return arg_idx_core_fn(e); - }; - - // Return true if the application \c e has an argument or an - // application (f ...) where f is an argument. - auto has_target_fn = [&](expr const & e) -> bool { - lean_assert(is_app(e)); - for (unsigned i = 1; i < num_args(e); i++) { - expr const & a = arg(e, i); - if (arg_idx_fn(a)) - return true; - } - return false; - }; - - // 3- There is an application (f x) in the left-hand-side, and - // the type expected by f is definitionally equal to the argument type. - // 4- There is an application (f (x ...)) in the left-hand-side, and - // the type expected by f is definitionally equal to the type of (x ...) - // 5- There is an application (f (fun y, x)) in the left-hand-side, - // and the type expected by f is definitionally equal to the type of (fun y, x) - std::function visit_fn = - [&](expr const & e, context const & ctx) { - if (is_app(e)) { - expr const & f = arg(e, 0); - if (has_target_fn(e)) { - expr f_type = tc.infer_type(f, ctx, menv); - for (unsigned i = 1; i < num_args(e); i++) { - f_type = tc.ensure_pi(f_type, ctx, menv); - expr const & a = arg(e, i); - auto arg_idx = arg_idx_fn(a); - if (arg_idx && !skip[*arg_idx]) { - expr const & expected_type = abst_domain(f_type); - expr const & given_type = tc.infer_type(a, ctx, menv); - if (tc.is_definitionally_equal(given_type, expected_type)) { - skip[*arg_idx] = true; - } - } - f_type = instantiate(abst_body(f_type), a); - } - } - for (expr const & a : ::lean::args(e)) - visit_fn(a, ctx); - } else if (is_abstraction(e)) { - visit_fn(abst_domain(e), ctx); - visit_fn(abst_body(e), extend(ctx, abst_name(e), abst_body(e))); - } - }; - - visit_fn(lhs, context()); - return std::all_of(skip.begin(), skip.end(), [](bool b) { return b; }); -} - -static int to_ceqs(lua_State * L) { - ro_shared_environment env(L, 1); - optional menv; - if (!lua_isnil(L, 2)) - menv = to_metavar_env(L, 2); - auto r = to_ceqs(env, menv, to_expr(L, 3), to_expr(L, 4)); - lua_newtable(L); - int i = 1; - for (auto p : r) { - lua_newtable(L); - push_expr(L, p.first); - lua_rawseti(L, -2, 1); - push_expr(L, p.second); - lua_rawseti(L, -2, 2); - lua_rawseti(L, -2, i); - i = i + 1; - } - return 1; -} - -static int is_ceq(lua_State * L) { - ro_shared_environment env(L, 1); - optional menv; - if (!lua_isnil(L, 2)) - menv = to_metavar_env(L, 2); - lua_pushboolean(L, is_ceq(env, menv, to_expr(L, 3))); - return 1; -} - -static int is_permutation_ceq(lua_State * L) { - lua_pushboolean(L, is_permutation_ceq(to_expr(L, 1))); - return 1; -} - -void open_ceq(lua_State * L) { - SET_GLOBAL_FUN(to_ceqs, "to_ceqs"); - SET_GLOBAL_FUN(is_ceq, "is_ceq"); - SET_GLOBAL_FUN(is_permutation_ceq, "is_permutation_ceq"); -} -} diff --git a/src/library/simplifier/ceq.h b/src/library/simplifier/ceq.h deleted file mode 100644 index 4e10312aaf..0000000000 --- a/src/library/simplifier/ceq.h +++ /dev/null @@ -1,90 +0,0 @@ -/* -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include "util/lua.h" -#include "kernel/environment.h" -#include "kernel/metavar.h" -#include "library/expr_pair.h" -namespace lean { -/** - \brief Given a proposition \c e and its proof H, return a list of conditional equations (and proofs) extracted from \c e. - - The following rules are used to convert \c e into conditional equations. - - [not P] ---> P = false - [P /\ Q] ---> [P], [Q] - [if P then Q else R] ---> P -> [Q], not P -> [Q] - [P -> Q] ---> P -> [Q] - [forall x : A, P] ---> forall x : A, [P] - [a ≠ b] ---> (a = b) = false - - P ---> P = true (if none of the rules above apply and P is not an equality) - - \remark if the left-hand-side of an equation does not contain all variables, then it is - discarded. That is, all elements in the resultant list satisfy the predicate \c is_ceq. -*/ -list to_ceqs(ro_environment const & env, optional const & menv, expr const & e, expr const & H); -/** - \brief Return true iff \c e is a conditional equation. - - A conditional equation ceq has the form - - ceq := (forall x : A, ceq) - | lhs = rhs - | lhs == rhs - - - Moreover, for (forall x : A, ceq), the variable x must occur in the \c ceq left-hand-size - when \c A is not a proposition. -*/ -bool is_ceq(ro_environment const & env, optional const & menv, expr e); -/** - \brief Return true iff the lhs is identical to the rhs modulo a - permutation of the conditional equation arguments. -*/ -bool is_permutation_ceq(expr e); -/* - Given a ceq C, in principle, whenever we want to create an application (C t1 ... tn), - we must check whether the types of t1 ... tn are convertible to the expected types by C. - - This check is needed because of universe cumulativity. - Here is an example that illustrates the issue: - - universe U >= 2 - variable f (A : (Type 1)) : (Type 1) - axiom Ax1 (a : Type) : f a = a - rewrite_set S - add_rewrite Ax1 eq_id : S - theorem T1 (A : (Type 1)) : f A = A - := by simp S - - In this example, Ax1 is a ceq. It has an argument of type Type. - Note that f expects an element of type (Type 1). So, the term (f a) is type correct. - - The axiom Ax1 is only for arguments convertible to Type (i.e., Type 0), but - argument A in T1 lives in (Type 1) - - Scenarios like the one above do not occur very frequently. Moveover, it is quite expensive - to check if the types are convertible for each application of a ceq. - - In most cases, we can statically determine that the checks are not needed when applying - a ceq. Here is a sufficient condition for skipping the test: if for all - arguments x of ceq, one of the following conditions must hold: - 1- The argument has type (Type U). In Lean, (Type U) is the maximal universe. - 2- The argument is a proposition. - 3- There is an application (f x) in the left-hand-side, and - the type expected by f is definitionally equal to the argument type. - 4- There is an application (f (x ...)) in the left-hand-side, and - the type expected by f is definitionally equal to the type of (x ...) - 5- There is an application (f (fun y, x)) in the left-hand-side, - and the type expected by f is definitionally equal to the type of (fun y, x) - \pre is_ceq(env, menv, ceq) -*/ -bool is_safe_to_skip_check_ceq_types(ro_environment const & env, optional const & menv, expr ceq); - -void open_ceq(lua_State * L); -} diff --git a/src/library/simplifier/congr.cpp b/src/library/simplifier/congr.cpp deleted file mode 100644 index 8ef76fe411..0000000000 --- a/src/library/simplifier/congr.cpp +++ /dev/null @@ -1,202 +0,0 @@ -/* -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include "util/sstream.h" -#include "kernel/kernel.h" -#include "kernel/type_checker.h" -#include "library/equality.h" -#include "library/simplifier/congr.h" - -namespace lean { -typedef congr_theorem_info::app_arg_info app_arg_info; -/** - \brief Return true iff arg_info contains an entry s.t. m_proof_arg_pos or m_proof_new_arg_pos is pos. -*/ -static bool contains_pos(buffer const & arg_info, unsigned pos) { - return std::any_of(arg_info.begin(), arg_info.end(), - [&](app_arg_info const & info) { - return - info.get_pos_at_proof() == pos || - (info.get_new_pos_at_proof() && *info.get_new_pos_at_proof() == pos); - }); -} - -static void check_conclusion_lhs_rhs(expr const & lhs, expr const & rhs, unsigned num) { - if (!is_var(lhs) || !is_var(rhs)) - throw exception("invalid congruence theorem, the arguments in the left and right-hand-sides must be variables"); - if (var_idx(lhs) >= num) - throw exception("invalid congruence theorem, left-hand-side contains free variables"); - if (var_idx(rhs) >= num) - throw exception("invalid congruence theorem, right-hand-side contains free variables"); -} - -static void check_arg_lhs_rhs(expr const & lhs, expr const & rhs, unsigned num) { - if (!is_var(lhs) || !is_var(rhs)) - throw exception(sstream() << "invalid congruence theorem, type of argument #" << (num+1) << " is not an equality between variables"); - if (var_idx(lhs) >= num) - throw exception(sstream() << "invalid congruence theorem, left-hand-side of argument #" << (num+1) << " contains free variables"); - if (var_idx(rhs) >= num) - throw exception(sstream() << "invalid congruence theorem, right-hand-side of argument #" << (num+1) << " contains free variables"); -} - -static buffer::iterator find_arg_info(buffer & arg_infos, unsigned proof_arg_pos, unsigned proof_new_arg_pos) { - return std::find_if(arg_infos.begin(), arg_infos.end(), [&](app_arg_info const & info) { - return info.get_pos_at_proof() == proof_arg_pos && info.get_new_pos_at_proof() && *info.get_new_pos_at_proof() == proof_new_arg_pos; - }); -} - -static pair find_hypothesis(buffer & arg_infos, unsigned vidx, unsigned num) { - for (auto const & info : arg_infos) { - if (vidx == info.get_pos_at_proof()) { - return mk_pair(info.get_arg_pos(), false); - } else if (info.get_new_pos_at_proof() && vidx == *info.get_new_pos_at_proof()) { - return mk_pair(info.get_arg_pos(), true); - } - } - throw exception(sstream() << "invalid congruence theorem, invalid hypothesis for argument #" << num - << ", variable must occur in the left or right hand side of the conclusion of the theorem"); -} - -void congr_theorem_info::context::display(std::ostream & out) const { - if (!m_pos) - out << "!"; - out << "#" << m_arg; - if (m_new) - out << "'"; -} - -void congr_theorem_info::app_arg_info::display(std::ostream & out) const { - out << "#" << m_arg_pos << ": "; - if (m_context) { - m_context->display(out); - out << " -> "; - } - out << "#" << m_proof_arg_pos; - if (m_proof_new_arg_pos) - out << " #" << *m_proof_new_arg_pos << " #" << *m_proof_proof_pos; -} - -void congr_theorem_info::display(std::ostream & out) const { - out << m_fun << " " << m_num_proof_args << "\n" << m_proof << "\n"; - for (auto const & info : m_arg_info) { - info.display(out); - out << "\n"; - } - out << "\n"; -} - -congr_theorem_info check_congr_theorem(ro_environment const & env, expr const & e) { - expr t = type_checker(env).infer_type(e); - expr b = t; - unsigned num = 0; - while (is_pi(b)) { - b = abst_body(b); - num++; - } - expr lhs, rhs; - if (!is_equality(b, lhs, rhs)) - throw exception("invalid congruence theorem, conclusion is not an equality"); - if (!is_app(lhs)) - throw exception("invalid congruence theorem, left-hand-side of the conclusion is not a function application"); - if (!is_app(rhs)) - throw exception("invalid congruence theorem, right-hand-side of the conclusion is not a function application"); - if (arg(lhs, 0) != arg(rhs, 0)) - throw exception("invalid congruence theorem, the functions in the left and right-hand-sides are different"); - if (num_args(lhs) != num_args(rhs)) - throw exception("invalid congruence theorem, the number of arguments in the left and right-hand-sides is different"); - - congr_theorem_info r; - r.m_fun = arg(lhs, 0); - r.m_proof = e; - r.m_num_proof_args = num; - - buffer arg_infos; - for (unsigned i = 1; i < num_args(lhs); i++) { - expr a = arg(lhs, i); - expr new_a = arg(rhs, i); - check_conclusion_lhs_rhs(a, new_a, num); - unsigned proof_arg_pos = num - var_idx(a) - 1; - unsigned proof_new_arg_pos = num - var_idx(new_a) - 1; - - if (contains_pos(arg_infos, proof_arg_pos) || - contains_pos(arg_infos, proof_new_arg_pos)) - throw exception("invalid congruence theorem, variables can only occur once in the left and right-hand sides"); - - if (proof_arg_pos == proof_new_arg_pos) { - // this argument does not need proof, then add it directly to - // r.m_arg_info - r.m_arg_info.push_back(app_arg_info(i, proof_arg_pos)); - } else { - // we have to find where the proof for this one is located - arg_infos.push_back(app_arg_info(i, proof_arg_pos, proof_new_arg_pos)); - } - } - - bool progress = true; - while (progress) { - progress = false; - expr b = t; - num = 0; - while (is_pi(b)) { - expr d = abst_domain(b); - expr lhs, rhs; - if (is_equality(d, lhs, rhs)) { - check_arg_lhs_rhs(lhs, rhs, num); - auto it = find_arg_info(arg_infos, num - var_idx(lhs) - 1, num - var_idx(rhs) - 1); - if (it == arg_infos.end()) - throw exception(sstream() << "invalid congruence theorem, argument #" << num << " does not match conclusion of the theorem"); - if (!it->m_proof_proof_pos) { - progress = true; - it->m_proof_proof_pos = num; - r.m_arg_info.push_back(*it); - } - } else if (is_pi(d) && is_equality(abst_body(d), lhs, rhs)) { - check_arg_lhs_rhs(lhs, rhs, num+1); - auto it = find_arg_info(arg_infos, num - var_idx(lhs), num - var_idx(rhs)); - if (it == arg_infos.end()) - throw exception(sstream() << "invalid congruence theorem, argument #" << num - << " does not match conclusion of the theorem"); - if (!it->m_proof_proof_pos) { - bool ctx_pos; - pair p; - if (is_var(abst_domain(d))) { - ctx_pos = true; - p = find_hypothesis(arg_infos, num - var_idx(abst_domain(d)) - 1, num); - } else if (is_not(abst_domain(d)) && is_var(arg(abst_domain(d), 1))) { - ctx_pos = false; - p = find_hypothesis(arg_infos, num - var_idx(arg(abst_domain(d), 1)) - 1, num); - } else { - throw exception(sstream() << "invalid congruence theorem, hypothesis for argument #" << num - << " must be a variable or the negation of variable"); - } - progress = true; - unsigned ctx_arg = p.first; - bool ctx_new = p.second; - it->m_proof_proof_pos = num; - it->m_context = congr_theorem_info::context(ctx_arg, ctx_pos, ctx_new); - r.m_arg_info.push_back(*it); - } - } - b = abst_body(b); - num++; - } - } - buffer found_args; - found_args.resize(num, false); - for (auto const & info : r.m_arg_info) { - found_args[info.get_pos_at_proof()] = true; - if (info.get_new_pos_at_proof()) - found_args[*info.get_new_pos_at_proof()] = true; - if (info.get_proof_pos_at_proof()) - found_args[*info.get_proof_pos_at_proof()] = true; - } - for (unsigned i = 0; i < num; i++) - if (!found_args[i]) - throw exception(sstream() << "invalid congruence theorem, cannot synthesize argument #" << i); - return r; -} -} diff --git a/src/library/simplifier/congr.h b/src/library/simplifier/congr.h deleted file mode 100644 index 77851723a0..0000000000 --- a/src/library/simplifier/congr.h +++ /dev/null @@ -1,144 +0,0 @@ -/* -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include -#include "kernel/environment.h" - -namespace lean { -/* - By default, Lean's simplifier will use the standard congruence theorem. - To simplify (f s), it will simplify f and s, and obtain the new terms - f' and s', and proofs H_f and H_s - H_f : f = f' - H_s : s = s' - Then, it uses the congr theorem to obtain - congr H_f H_s : f s = f' s' - - This behavior can be customize by providing specialized congruence rules - for specific operators. - - For example, kernel.lean contains the theorem: - - theorem or_congrr {a b c d : Bool} (H_ac : ∀ (H_nb : ¬ b), a = c) (H_bd : ∀ (H_nc : ¬ c), b = d) : a ∨ b ↔ c ∨ d - - It tells us that we can simplify a ∨ b, by first simplifying a under the assumption that b is false, - and then simplifying b under the assumption that the result of a simplification is false. - - We say or_congrr is a congruence theorem. This module is used to identify congruence theorems and - "compile" them into simple instructions that can be efficiently applied by the simplifier. -*/ -class congr_theorem_info { - friend congr_theorem_info check_congr_theorem(ro_environment const & env, expr const & e); -public: - /** - \brief Each argument may or may not be simplified under a new context. - For example, in or_congrr, b is simplified under a context containing not c. - - This class store this dependency. - */ - class context { - friend congr_theorem_info check_congr_theorem(ro_environment const & env, expr const & e); - /** - The position of the dependent argument. For or_congrr this field has value 0 for b, - since b depends on the new value c of a (after simplification). - */ - unsigned m_arg; - /** - Indicate whether is a positive or negative dependency. - For or_congrr, this field is false for b, since it depends negatively on c. - */ - bool m_pos; - /** - Indicate whether the dependecy is before/after simplification. - For or_congrr, this field is true for b, since it depends on the new value c of a (after simplification). - */ - bool m_new; - context(unsigned arg, bool pos, bool n):m_arg(arg), m_pos(pos), m_new(n) {} - public: - unsigned get_arg_pos() const { return m_arg; } - bool is_pos_dep() const { return m_pos; } - bool use_new_val() const { return m_new; } - void display(std::ostream & out) const; - }; - - /** - \brief This class indicates how to process an argument of the function application. - */ - class app_arg_info { - friend congr_theorem_info check_congr_theorem(ro_environment const & env, expr const & e); - /** - \brief Position of the argument to be processed. - For or_congrr, this field is 2 for b. - */ - unsigned m_arg_pos; - /** - \brief The context (if any) is used to simplify the argument - */ - optional m_context; - /** - \brief Position where this argument goes in the proof term. - For or_congrr, this field is 1 for b. - */ - unsigned m_proof_arg_pos; - /** - \brief Position where the simplified argument goes in the proof term. - If the argument should not be simplified, then this field is none. - - For or_congrr, this field is 3 for b. - */ - optional m_proof_new_arg_pos; - /** - \brief Position where the proof for new = old goes in the proof term. - - For or_congrr, this field is 5 for b. - */ - optional m_proof_proof_pos; - app_arg_info(unsigned arg_pos, unsigned proof_arg_pos):m_arg_pos(arg_pos), m_proof_arg_pos(proof_arg_pos) {} - app_arg_info(unsigned arg_pos, unsigned proof_arg_pos, unsigned proof_new_arg_pos): - m_arg_pos(arg_pos), m_proof_arg_pos(proof_arg_pos), m_proof_new_arg_pos(proof_new_arg_pos) {} - public: - unsigned get_arg_pos() const { return m_arg_pos; } - optional const & get_context() const { return m_context; } - unsigned get_pos_at_proof() const { return m_proof_arg_pos; } - optional const & get_new_pos_at_proof() const { return m_proof_new_arg_pos; } - optional const & get_proof_pos_at_proof() const { return m_proof_proof_pos; } - bool should_simplify() const { return static_cast(get_new_pos_at_proof()); } - void display(std::ostream & out) const; - }; - -private: - /** - Indicate for which function this theorem is a congruence for. - */ - expr m_fun; - - /** - Proof term for the theorem, in most cases is just a constant (e.g., or_congrr) that references a theorem in a Lean environment. - */ - expr m_proof; - /** - Number of arguments the theorem takes. For example, or_congrr has 6 arguments. - */ - unsigned m_num_proof_args; - /** - \brief Store the sequence the application arguments should be processed. - */ - std::vector m_arg_info; -public: - expr const & get_fun() const { return m_fun; } - expr const & get_proof() const { return m_proof; } - unsigned get_num_proof_args() const { return m_num_proof_args; } - std::vector const & get_arg_info() const { return m_arg_info; } - void display(std::ostream & out) const; -}; - -/** - \brief Check whether \c e is a congruence theorem in the given environment. - If it is, then returns a congr_theorem_info object. Otherwise, throws an exception. -*/ -congr_theorem_info check_congr_theorem(ro_environment const & env, expr const & e); -} diff --git a/src/library/simplifier/register_module.h b/src/library/simplifier/register_module.h deleted file mode 100644 index 5cf681caaf..0000000000 --- a/src/library/simplifier/register_module.h +++ /dev/null @@ -1,22 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include "util/script_state.h" -#include "library/simplifier/ceq.h" -#include "library/simplifier/rewrite_rule_set.h" -#include "library/simplifier/simplifier.h" - -namespace lean { -inline void open_simplifier_module(lua_State * L) { - open_ceq(L); - open_rewrite_rule_set(L); - open_simplifier(L); -} -inline void register_simplifier_module() { - script_state::register_module(open_simplifier_module); -} -} diff --git a/src/library/simplifier/rewrite_rule_set.cpp b/src/library/simplifier/rewrite_rule_set.cpp deleted file mode 100644 index 84b2265dab..0000000000 --- a/src/library/simplifier/rewrite_rule_set.cpp +++ /dev/null @@ -1,381 +0,0 @@ -/* -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include "util/splay_tree.h" -#include "util/list_fn.h" -#include "util/sstream.h" -#include "kernel/environment.h" -#include "library/io_state_stream.h" -#include "library/equality.h" -#include "library/kernel_bindings.h" -#include "library/simplifier/ceq.h" -#include "library/simplifier/rewrite_rule_set.h" - -namespace lean { -rewrite_rule::rewrite_rule(name const & id, expr const & lhs, expr const & rhs, expr const & ceq, expr const & proof, - unsigned num_args, bool is_permutation, bool must_check): - m_id(id), m_lhs(lhs), m_rhs(rhs), m_ceq(ceq), m_proof(proof), m_num_args(num_args), - m_is_permutation(is_permutation), m_must_check_types(must_check) { -} - -rewrite_rule_set::rewrite_rule_set(ro_environment const & env):m_env(env.to_weak_ref()) {} -rewrite_rule_set::rewrite_rule_set(rewrite_rule_set const & other): - m_env(other.m_env), m_rule_set(other.m_rule_set), m_disabled_rules(other.m_disabled_rules), m_congr_thms(other.m_congr_thms) {} -rewrite_rule_set::~rewrite_rule_set() {} - -void rewrite_rule_set::insert(name const & id, expr const & th, expr const & proof, optional const & menv) { - ro_environment env(m_env); - for (auto const & p : to_ceqs(env, menv, th, proof)) { - expr const & ceq = p.first; - expr const & proof = p.second; - bool is_perm = is_permutation_ceq(ceq); - expr eq = ceq; - unsigned num = 0; - while (is_pi(eq)) { - eq = abst_body(eq); - num++; - } - lean_assert(is_equality(eq)); - bool must_check = !is_safe_to_skip_check_ceq_types(m_env, menv, ceq); - m_rule_set = cons(rewrite_rule(id, arg(eq, num_args(eq) - 2), arg(eq, num_args(eq) - 1), - ceq, proof, num, is_perm, must_check), - m_rule_set); - } -} - -void rewrite_rule_set::insert(name const & th_name) { - ro_environment env(m_env); - auto obj = env->find_object(th_name); - if (obj && (obj->is_theorem() || obj->is_axiom())) { - insert(th_name, obj->get_type(), mk_constant(th_name), none_ro_menv()); - } else { - throw exception(sstream() << "'" << th_name << "' is not a theorem nor an axiom"); - } -} - -bool rewrite_rule_set::enabled(rewrite_rule const & rule) const { - return !m_disabled_rules.contains(rule.get_id()); -} - -bool rewrite_rule_set::enabled(name const & id) const { - return !m_disabled_rules.contains(id); -} - -void rewrite_rule_set::enable(name const & id, bool f) { - if (f) - m_disabled_rules.erase(id); - else - m_disabled_rules.insert(id); -} - -void rewrite_rule_set::insert_congr(expr const & e) { - ro_environment env(m_env); - m_congr_thms.emplace_front(check_congr_theorem(env, e)); -} - -void rewrite_rule_set::insert_congr(name const & th_name) { - insert_congr(mk_constant(th_name)); -} - -bool rewrite_rule_set::find_match(expr const &, match_fn const & fn) const { - auto l = m_rule_set; - for (auto const & rule : l) { - if (enabled(rule) && fn(rule)) - return true; - } - return false; -} - -void rewrite_rule_set::for_each(visit_fn const & fn) const { - auto l = m_rule_set; - for (auto const & rule : l) { - fn(rule, enabled(rule)); - } -} - -void rewrite_rule_set::for_each_congr(visit_congr_fn const & fn) const { - for (auto const & congr_th : m_congr_thms) { - fn(congr_th); - } -} - -format rewrite_rule_set::pp(formatter const & fmt, options const & opts) const { - format r; - bool first = true; - unsigned indent = get_pp_indent(opts); - for_each([&](rewrite_rule const & rule, bool enabled) { - if (first) - first = false; - else - r += line(); - r += format(rule.get_id()); - if (!enabled) - r += format(" [disabled]"); - if (rule.must_check_types()) - r += format(" [check]"); - r += space() + colon() + space(); - r += nest(indent, fmt(rule.get_ceq(), opts)); - }); - return r; -} - -io_state_stream const & operator<<(io_state_stream const & out, rewrite_rule_set const & rs) { - out << mk_pair(rs.pp(out.get_formatter(), out.get_options()), out.get_options()); - return out; -} - -class mk_rewrite_rule_set_obj : public neutral_object_cell { - name m_rule_set_id; -public: - mk_rewrite_rule_set_obj(name const & id):m_rule_set_id(id) {} - virtual ~mk_rewrite_rule_set_obj() {} - virtual char const * keyword() const { return "mk_rewrite_rule_set"; } - virtual void write(serializer & s) const { s << "mk_rrs" << m_rule_set_id; } -}; -static void read_rrs(environment const & env, io_state const &, deserializer & d) { - name n = read_name(d); - mk_rewrite_rule_set(env, n); -} -static object_cell::register_deserializer_fn mk_rrs_ds("mk_rrs", read_rrs); - -class add_rewrite_rules_obj : public neutral_object_cell { - name m_rule_set_id; - name m_th_name; -public: - add_rewrite_rules_obj(name const & rsid, name const & th_name):m_rule_set_id(rsid), m_th_name(th_name) {} - virtual ~add_rewrite_rules_obj() {} - virtual char const * keyword() const { return "add_rewrite_rules"; } - virtual void write(serializer & s) const { s << "add_rr" << m_rule_set_id << m_th_name; } -}; -static void read_arr(environment const & env, io_state const &, deserializer & d) { - name rsid = read_name(d); - name th = read_name(d); - add_rewrite_rules(env, rsid, th); -} -static object_cell::register_deserializer_fn add_rr_ds("add_rr", read_arr); - -class enable_rewrite_rules_obj : public neutral_object_cell { - name m_rule_set_id; - name m_rule_id; - bool m_flag; -public: - enable_rewrite_rules_obj(name const & rsid, name const & id, bool flag):m_rule_set_id(rsid), m_rule_id(id), m_flag(flag) {} - virtual ~enable_rewrite_rules_obj() {} - virtual char const * keyword() const { return "enable_rewrite_rules_obj"; } - virtual void write(serializer & s) const { s << "enable_rr" << m_rule_set_id << m_rule_id << m_flag; } -}; -static void read_enable_rr(environment const & env, io_state const &, deserializer & d) { - name rsid = read_name(d); - name id = read_name(d); - bool flag = d.read_bool(); - enable_rewrite_rules(env, rsid, id, flag); -} -static object_cell::register_deserializer_fn enable_rr_ds("enable_rr", read_enable_rr); - -class add_congr_theorem_obj : public neutral_object_cell { - name m_rule_set_id; - name m_th_name; -public: - add_congr_theorem_obj(name const & rsid, name const & th_name):m_rule_set_id(rsid), m_th_name(th_name) {} - virtual ~add_congr_theorem_obj() {} - virtual char const * keyword() const { return "add_congr_theorem"; } - virtual void write(serializer & s) const { s << "add_ct" << m_rule_set_id << m_th_name; } -}; -static void read_ct(environment const & env, io_state const &, deserializer & d) { - name rsid = read_name(d); - name th = read_name(d); - add_congr_theorem(env, rsid, th); -} -static object_cell::register_deserializer_fn add_ct_ds("add_ct", read_ct); - -/** - \brief Extension for managing rewrite rule sets. -*/ -struct rewrite_rule_set_extension : public environment_extension { - name_map m_rule_sets; - - rewrite_rule_set_extension const * get_parent() const { - return environment_extension::get_parent(); - } - - rewrite_rule_set const * find_ro_core(name const & rule_set_id) const { - auto it = m_rule_sets.find(rule_set_id); - if (it != m_rule_sets.end()) { - return &(it->second); - } - auto p = get_parent(); - if (p) { - return p->find_ro_core(rule_set_id); - } else { - return nullptr; - } - } - - rewrite_rule_set const & find_ro(name const & rule_set_id) const { - auto rs = find_ro_core(rule_set_id); - if (rs) - return *rs; - throw exception(sstream() << "environment does not contain a rewrite rule set named '" << rule_set_id << "'"); - } - - rewrite_rule_set & find_rw(name const & rule_set_id) { - auto it = m_rule_sets.find(rule_set_id); - if (it != m_rule_sets.end()) - return it->second; - auto p = get_parent(); - if (p) { - auto const & rs = p->find_ro(rule_set_id); - m_rule_sets.insert(mk_pair(rule_set_id, rewrite_rule_set(rs))); - return m_rule_sets.find(rule_set_id)->second; - } - throw exception(sstream() << "environment does not contain a rewrite rule set named '" << rule_set_id << "'"); - } - - void mk_rewrite_rule_set(environment const & env, name const & rule_set_id) { - if (find_ro_core(rule_set_id)) - throw exception(sstream() << "environment already contains a rewrite rule set named '" << rule_set_id << "'"); - m_rule_sets.insert(mk_pair(rule_set_id, rewrite_rule_set(env))); - env->add_neutral_object(new mk_rewrite_rule_set_obj(rule_set_id)); - } - - void add_rewrite_rules(environment const & env, name const & rule_set_id, name const & th_name) { - auto & rs = find_rw(rule_set_id); - rs.insert(th_name); - env->add_neutral_object(new add_rewrite_rules_obj(rule_set_id, th_name)); - } - - void enable_rewrite_rules(environment const & env, name const & rule_set_id, name const & rule_id, bool flag) { - auto & rs = find_rw(rule_set_id); - rs.enable(rule_id, flag); - env->add_neutral_object(new enable_rewrite_rules_obj(rule_set_id, rule_id, flag)); - } - - void add_congr_theorem(environment const & env, name const & rule_set_id, name const & th_name) { - auto & rs = find_rw(rule_set_id); - rs.insert_congr(th_name); - env->add_neutral_object(new add_congr_theorem_obj(rule_set_id, th_name)); - } - - rewrite_rule_set get_rewrite_rule_set(name const & rule_set_id) const { - return find_ro(rule_set_id); - } -}; - -struct rewrite_rule_set_extension_initializer { - unsigned m_extid; - rewrite_rule_set_extension_initializer() { - m_extid = environment_cell::register_extension([](){ - return std::unique_ptr(new rewrite_rule_set_extension()); - }); - } -}; - -static rewrite_rule_set_extension_initializer g_rewrite_rule_set_extension_initializer; - -static rewrite_rule_set_extension const & to_ext(ro_environment const & env) { - return env->get_extension(g_rewrite_rule_set_extension_initializer.m_extid); -} - -static rewrite_rule_set_extension & to_ext(environment const & env) { - return env->get_extension(g_rewrite_rule_set_extension_initializer.m_extid); -} - -static name g_default_rewrite_rule_set_id("default"); -name const & get_default_rewrite_rule_set_id() { - return g_default_rewrite_rule_set_id; -} - -void mk_rewrite_rule_set(environment const & env, name const & rule_set_id) { - to_ext(env).mk_rewrite_rule_set(env, rule_set_id); -} - -void add_rewrite_rules(environment const & env, name const & rule_set_id, name const & th_name) { - to_ext(env).add_rewrite_rules(env, rule_set_id, th_name); -} - -void enable_rewrite_rules(environment const & env, name const & rule_set_id, name const & rule_id, bool flag) { - to_ext(env).enable_rewrite_rules(env, rule_set_id, rule_id, flag); -} - -void add_congr_theorem(environment const & env, name const & rule_set_id, name const & th_name) { - to_ext(env).add_congr_theorem(env, rule_set_id, th_name); -} - -rewrite_rule_set get_rewrite_rule_set(ro_environment const & env, name const & rule_set_id) { - return to_ext(env).get_rewrite_rule_set(rule_set_id); -} - -static int mk_rewrite_rule_set(lua_State * L) { - int nargs = lua_gettop(L); - if (nargs == 0) - mk_rewrite_rule_set(rw_shared_environment(L)); - else if (nargs == 1) - mk_rewrite_rule_set(rw_shared_environment(L), to_name_ext(L, 1)); - else - mk_rewrite_rule_set(rw_shared_environment(L, 2), to_name_ext(L, 1)); - return 0; -} - -static int add_rewrite_rules(lua_State * L) { - int nargs = lua_gettop(L); - if (nargs == 1) - add_rewrite_rules(rw_shared_environment(L), to_name_ext(L, 1)); - else if (nargs == 2) - add_rewrite_rules(rw_shared_environment(L), to_name_ext(L, 1), to_name_ext(L, 2)); - else - add_rewrite_rules(rw_shared_environment(L, 3), to_name_ext(L, 1), to_name_ext(L, 2)); - return 0; -} - -static int enable_rewrite_rules(lua_State * L) { - int nargs = lua_gettop(L); - if (nargs == 2) - enable_rewrite_rules(rw_shared_environment(L), to_name_ext(L, 1), lua_toboolean(L, 2)); - else if (nargs == 3) - enable_rewrite_rules(rw_shared_environment(L), to_name_ext(L, 1), to_name_ext(L, 2), lua_toboolean(L, 3)); - else - enable_rewrite_rules(rw_shared_environment(L, 4), to_name_ext(L, 1), to_name_ext(L, 2), lua_toboolean(L, 3)); - return 0; -} - -static int add_congr_theorem(lua_State * L) { - int nargs = lua_gettop(L); - if (nargs == 1) - add_congr_theorem(rw_shared_environment(L), to_name_ext(L, 1)); - else if (nargs == 2) - add_congr_theorem(rw_shared_environment(L), to_name_ext(L, 1), to_name_ext(L, 2)); - else - add_congr_theorem(rw_shared_environment(L, 3), to_name_ext(L, 1), to_name_ext(L, 2)); - return 0; -} - -static int show_rewrite_rules(lua_State * L) { - int nargs = lua_gettop(L); - formatter fmt = get_global_formatter(L); - options opts = get_global_options(L); - format r; - if (nargs == 0) - r = get_rewrite_rule_set(ro_shared_environment(L)).pp(fmt, opts); - else if (nargs == 1) - r = get_rewrite_rule_set(ro_shared_environment(L), to_name_ext(L, 1)).pp(fmt, opts); - else - r = get_rewrite_rule_set(ro_shared_environment(L, 2), to_name_ext(L, 1)).pp(fmt, opts); - io_state * ios = get_io_state(L); - if (ios) - regular(*ios) << mk_pair(r, opts) << endl; - else - std::cout << mk_pair(r, opts) << "\n"; - return 0; -} - -void open_rewrite_rule_set(lua_State * L) { - SET_GLOBAL_FUN(mk_rewrite_rule_set, "mk_rewrite_rule_set"); - SET_GLOBAL_FUN(add_rewrite_rules, "add_rewrite_rules"); - SET_GLOBAL_FUN(enable_rewrite_rules, "enable_rewrite_rules"); - SET_GLOBAL_FUN(add_congr_theorem, "add_congr_theorem"); - SET_GLOBAL_FUN(show_rewrite_rules, "show_rewrite_rules"); -} -} diff --git a/src/library/simplifier/rewrite_rule_set.h b/src/library/simplifier/rewrite_rule_set.h deleted file mode 100644 index 83406699a1..0000000000 --- a/src/library/simplifier/rewrite_rule_set.h +++ /dev/null @@ -1,153 +0,0 @@ -/* -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include -#include -#include "util/lua.h" -#include "util/list.h" -#include "util/splay_tree.h" -#include "util/name.h" -#include "kernel/environment.h" -#include "kernel/metavar.h" -#include "kernel/formatter.h" -#include "library/io_state_stream.h" -#include "library/simplifier/congr.h" - -namespace lean { -class rewrite_rule_set; -class rewrite_rule { - friend class rewrite_rule_set; - name m_id; - expr m_lhs; - expr m_rhs; - expr m_ceq; - expr m_proof; - unsigned m_num_args; - bool m_is_permutation; - bool m_must_check_types; // if true, then we must check if the given types are convertible to the expected types - rewrite_rule(name const & id, expr const & lhs, expr const & rhs, expr const & ceq, expr const & proof, - unsigned num_args, bool is_permutation, bool must_check); -public: - name const & get_id() const { return m_id; } - expr const & get_lhs() const { return m_lhs; } - expr const & get_rhs() const { return m_rhs; } - expr const & get_ceq() const { return m_ceq; } - expr const & get_proof() const { return m_proof; } - unsigned get_num_args() const { return m_num_args; } - bool is_permutation() const { return m_is_permutation; } - bool must_check_types() const { return m_must_check_types; } -}; - -/** - \brief Actual implementation of the \c rewrite_rule_set class. -*/ -class rewrite_rule_set { - typedef splay_tree name_set; - ro_environment::weak_ref m_env; - list m_rule_set; // TODO(Leo): use better data-structure, e.g., discrimination trees - name_set m_disabled_rules; - list m_congr_thms; // This is probably ok since we usually have very few congruence theorems - - bool enabled(rewrite_rule const & rule) const; -public: - rewrite_rule_set(ro_environment const & env); - rewrite_rule_set(rewrite_rule_set const & other); - ~rewrite_rule_set(); - - /** - \brief Convert the theorem \c th with proof \c proof into conditional rewrite rules, and - insert the rules into this rule set. The new rules are tagged with the given \c id. - */ - void insert(name const & id, expr const & th, expr const & proof, optional const & menv); - - /** - \brief Convert the theorem/axiom named \c th_name in the environment into conditional rewrite rules, - and insert the rules into this rule set. The new rules are tagged with the theorem name. - - This method throws an exception if the environment does not have a theorem/axiom named \c th_name. - */ - void insert(name const & th_name); - - /** \brief Return true iff the conditional rewrite rules tagged with the given id are enabled. */ - bool enabled(name const & id) const; - - /** \brief Enable/disable the conditional rewrite rules tagged with the given identifier. */ - void enable(name const & id, bool f); - - /** \brief Add a new congruence theorem. */ - void insert_congr(expr const & e); - void insert_congr(name const & th_name); - - typedef std::function match_fn; // NOLINT - typedef std::function visit_fn; - - /** - \brief Execute fn(rule) for each (enabled) rule whose the left-hand-side may - match \c e. - The traversal is interrupted as soon as \c fn returns true. - */ - bool find_match(expr const &, match_fn const & fn) const; - - /** \brief Execute fn(rule, enabled) for each rule in this rule set. */ - void for_each(visit_fn const & fn) const; - - typedef std::function visit_congr_fn; // NOLINT - - /** \brief Execute fn(congr_th) for each congruence theorem in this rule set. */ - void for_each_congr(visit_congr_fn const & fn) const; - - /** \brief Pretty print this rule set. */ - format pp(formatter const & fmt, options const & opts) const; -}; -io_state_stream const & operator<<(io_state_stream const & out, rewrite_rule_set const & rs); - -name const & get_default_rewrite_rule_set_id(); -/** - \brief Create a rewrite rule set inside the given environment. - - \remark The rule set is saved when the environment is serialized. - \remark This procedure throws an exception if the environment already contains a rule set named \c rule_set_id. -*/ -void mk_rewrite_rule_set(environment const & env, name const & rule_set_id = get_default_rewrite_rule_set_id()); -/** - \brief Convert the theorem named \c th_name into conditional rewrite rules - and insert them in the rule set named \c rule_set_id in the given environment. - - \remark This procedure throws an exception if the environment does not have a theorem/axiom named \c th_name. - \remark This procedure throws an exception if the environment does not have a rule set named \c rule_set_id. -*/ -void add_rewrite_rules(environment const & env, name const & rule_set_id, name const & th_name); -inline void add_rewrite_rules(environment const & env, name const & th_name) { - add_rewrite_rules(env, get_default_rewrite_rule_set_id(), th_name); -} - -/** - \brief Enable/disable the rewrite rules whose id is \c rule_id in the given rule set. - - \remark This procedure throws an exception if the environment does not have a rule set named \c rule_set_id. -*/ -void enable_rewrite_rules(environment const & env, name const & rule_set_id, name const & rule_id, bool flag); -inline void enable_rewrite_rules(environment const & env, name const & rule_id, bool flag) { - enable_rewrite_rules(env, get_default_rewrite_rule_set_id(), rule_id, flag); -} - -/** - \brief Add a new congruence theorem to the given rewrite rule set. -*/ -void add_congr_theorem(environment const & env, name const & rule_set_id, name const & th_name); -inline void add_congr_theorem(environment const & env, name const & th_name) { - add_congr_theorem(env, get_default_rewrite_rule_set_id(), th_name); -} - -/** - \brief Return the rule set name \c rule_set_id in the given environment. - - \remark This procedure throws an exception if the environment does not have a rule set named \c rule_set_id. -*/ -rewrite_rule_set get_rewrite_rule_set(ro_environment const & env, name const & rule_set_id = get_default_rewrite_rule_set_id()); -void open_rewrite_rule_set(lua_State * L); -} diff --git a/src/library/simplifier/simplifier.cpp b/src/library/simplifier/simplifier.cpp deleted file mode 100644 index 92691287a0..0000000000 --- a/src/library/simplifier/simplifier.cpp +++ /dev/null @@ -1,1903 +0,0 @@ -/* -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include -#include "util/flet.h" -#include "util/freset.h" -#include "util/interrupt.h" -#include "util/luaref.h" -#include "util/script_state.h" -#include "kernel/type_checker.h" -#include "kernel/free_vars.h" -#include "kernel/instantiate.h" -#include "kernel/abstract.h" -#include "kernel/normalizer.h" -#include "kernel/kernel.h" -#include "kernel/max_sharing.h" -#include "kernel/occurs.h" -#include "library/kernel_bindings.h" -#include "library/expr_pair.h" -#include "library/hop_match.h" -#include "library/expr_lt.h" -#include "library/simplifier/rewrite_rule_set.h" -#include "library/simplifier/simplifier.h" - -#ifndef LEAN_SIMPLIFIER_PROOFS -#define LEAN_SIMPLIFIER_PROOFS true -#endif - -#ifndef LEAN_SIMPLIFIER_CONTEXTUAL -#define LEAN_SIMPLIFIER_CONTEXTUAL true -#endif - -#ifndef LEAN_SIMPLIFIER_SINGLE_PASS -#define LEAN_SIMPLIFIER_SINGLE_PASS false -#endif - -#ifndef LEAN_SIMPLIFIER_BETA -#define LEAN_SIMPLIFIER_BETA true -#endif - -#ifndef LEAN_SIMPLIFIER_ETA -#define LEAN_SIMPLIFIER_ETA true -#endif - -#ifndef LEAN_SIMPLIFIER_EVAL -#define LEAN_SIMPLIFIER_EVAL true -#endif - -#ifndef LEAN_SIMPLIFIER_UNFOLD -#define LEAN_SIMPLIFIER_UNFOLD false -#endif - -#ifndef LEAN_SIMPLIFIER_CONDITIONAL -#define LEAN_SIMPLIFIER_CONDITIONAL true -#endif - -#ifndef LEAN_SIMPLIFIER_MEMOIZE -#define LEAN_SIMPLIFIER_MEMOIZE true -#endif - -#ifndef LEAN_SIMPLIFIER_HEQ -#define LEAN_SIMPLIFIER_HEQ false -#endif - -#ifndef LEAN_SIMPLIFIER_PRESERVE_BINDER_NAMES -#define LEAN_SIMPLIFIER_PRESERVE_BINDER_NAMES true -#endif - -#ifndef LEAN_SIMPLIFIER_MAX_STEPS -#define LEAN_SIMPLIFIER_MAX_STEPS std::numeric_limits::max() -#endif - -namespace lean { -static name g_simplifier_proofs {"simplifier", "proofs"}; -static name g_simplifier_contextual {"simplifier", "contextual"}; -static name g_simplifier_single_pass {"simplifier", "single_pass"}; -static name g_simplifier_beta {"simplifier", "beta"}; -static name g_simplifier_eta {"simplifier", "eta"}; -static name g_simplifier_eval {"simplifier", "eval"}; -static name g_simplifier_unfold {"simplifier", "unfold"}; -static name g_simplifier_conditional {"simplifier", "conditional"}; -static name g_simplifier_memoize {"simplifier", "memoize"}; -static name g_simplifier_max_steps {"simplifier", "max_steps"}; -static name g_simplifier_heq {"simplifier", "heq"}; -static name g_simplifier_preserve_binder_names {"simplifier", "preserve_binder_names"}; - -RegisterBoolOption(g_simplifier_proofs, LEAN_SIMPLIFIER_PROOFS, "(simplifier) generate proofs"); -RegisterBoolOption(g_simplifier_contextual, LEAN_SIMPLIFIER_CONTEXTUAL, "(simplifier) contextual simplification"); -RegisterBoolOption(g_simplifier_single_pass, LEAN_SIMPLIFIER_SINGLE_PASS, "(simplifier) if false then the simplifier keeps applying simplifications as long as possible"); -RegisterBoolOption(g_simplifier_beta, LEAN_SIMPLIFIER_BETA, "(simplifier) use beta-reduction"); -RegisterBoolOption(g_simplifier_eta, LEAN_SIMPLIFIER_ETA, "(simplifier) use eta-reduction"); -RegisterBoolOption(g_simplifier_eval, LEAN_SIMPLIFIER_EVAL, "(simplifier) apply reductions based on computation"); -RegisterBoolOption(g_simplifier_unfold, LEAN_SIMPLIFIER_UNFOLD, "(simplifier) unfolds non-opaque definitions"); -RegisterBoolOption(g_simplifier_conditional, LEAN_SIMPLIFIER_CONDITIONAL, "(simplifier) conditional rewriting"); -RegisterBoolOption(g_simplifier_memoize, LEAN_SIMPLIFIER_MEMOIZE, "(simplifier) memoize/cache intermediate results"); -RegisterBoolOption(g_simplifier_preserve_binder_names, LEAN_SIMPLIFIER_PRESERVE_BINDER_NAMES, - "(simplifier) (try to) preserve binder names when applying higher-order rewrite rules"); -RegisterBoolOption(g_simplifier_heq, LEAN_SIMPLIFIER_HEQ, "(simplifier) use heterogeneous equality support"); -RegisterUnsignedOption(g_simplifier_max_steps, LEAN_SIMPLIFIER_MAX_STEPS, "(simplifier) maximum number of steps"); - -bool get_simplifier_proofs(options const & opts) { return opts.get_bool(g_simplifier_proofs, LEAN_SIMPLIFIER_PROOFS); } -bool get_simplifier_contextual(options const & opts) { return opts.get_bool(g_simplifier_contextual, LEAN_SIMPLIFIER_CONTEXTUAL); } -bool get_simplifier_single_pass(options const & opts) { return opts.get_bool(g_simplifier_single_pass, LEAN_SIMPLIFIER_SINGLE_PASS); } -bool get_simplifier_beta(options const & opts) { return opts.get_bool(g_simplifier_beta, LEAN_SIMPLIFIER_BETA); } -bool get_simplifier_eta(options const & opts) { return opts.get_bool(g_simplifier_eta, LEAN_SIMPLIFIER_ETA); } -bool get_simplifier_eval(options const & opts) { return opts.get_bool(g_simplifier_eval, LEAN_SIMPLIFIER_EVAL); } -bool get_simplifier_unfold(options const & opts) { return opts.get_bool(g_simplifier_unfold, LEAN_SIMPLIFIER_UNFOLD); } -bool get_simplifier_conditional(options const & opts) { return opts.get_bool(g_simplifier_conditional, LEAN_SIMPLIFIER_CONDITIONAL); } -bool get_simplifier_memoize(options const & opts) { return opts.get_bool(g_simplifier_memoize, LEAN_SIMPLIFIER_MEMOIZE); } -bool get_simplifier_heq(options const & opts) { return opts.get_bool(g_simplifier_heq, LEAN_SIMPLIFIER_HEQ); } -bool get_simplifier_preserve_binder_names(options const & opts) { - return opts.get_bool(g_simplifier_preserve_binder_names, LEAN_SIMPLIFIER_PRESERVE_BINDER_NAMES); -} -unsigned get_simplifier_max_steps(options const & opts) { return opts.get_unsigned(g_simplifier_max_steps, LEAN_SIMPLIFIER_MAX_STEPS); } - -static name g_local("local"); -static name g_C("C"); -static name g_H("H"); -static name g_x("x"); -static name g_unique = name::mk_internal_unique_name(); - -class simplifier_cell::imp { - friend class simplifier_cell; - friend class simplifier; - - typedef std::vector rule_sets; - typedef expr_map cache; - typedef std::vector congr_thms; - typedef cache const_map; - std::weak_ptr m_this; - ro_environment m_env; - options m_options; - type_checker m_tc; - rule_sets m_rule_sets; - cache m_cache; - max_sharing_fn m_max_sharing; - const_map m_const_map; // mapping from old to new constants in hfunext and hpiext - congr_thms m_congr_thms; - unsigned m_next_idx; // index used to create fresh constants - unsigned m_num_steps; // number of steps performed - unsigned m_depth; // recursion depth - name_map m_name_subst; - cached_ro_metavar_env m_menv; - std::shared_ptr m_monitor; - - // Configuration - bool m_proofs_enabled; - bool m_contextual; - bool m_single_pass; - bool m_beta; - bool m_eta; - bool m_eval; - bool m_unfold; - bool m_conditional; - bool m_memoize; - bool m_preserve_binder_names; - bool m_use_heq; - unsigned m_max_steps; - - struct updt_rule_set { - imp & m_fn; - rewrite_rule_set m_old; - freset m_reset_cache; // must reset the cache whenever we update the rule set. - /** - \brief Update the rule set using a constant H : P, where P is a proposition. - - \pre const_type(H) - */ - updt_rule_set(imp & fn, expr const & H): - m_fn(fn), m_old(m_fn.m_rule_sets[0]), m_reset_cache(m_fn.m_cache) { - lean_assert(const_type(H)); - m_fn.m_rule_sets[0].insert(g_local, *const_type(H), H, m_fn.m_menv.to_some_menv()); - } - ~updt_rule_set() { - m_fn.m_rule_sets[0] = m_old; - // Remark: m_reset_cache destructor will restore the cache - } - }; - - struct updt_const_map { - imp & m_fn; - expr const & m_old_x; - updt_const_map(imp & fn, expr const & old_x, expr const & new_x, expr const & H): - m_fn(fn), m_old_x(old_x) { - m_fn.m_const_map[old_x] = result(new_x, H, true); - } - ~updt_const_map() { - m_fn.m_const_map.erase(m_old_x); - } - }; - - static expr mk_lambda(name const & n, expr const & d, expr const & b) { - return ::lean::mk_lambda(n, d, b); - } - - /** - \brief Return a lambda with body \c new_body, and name and domain from abst. - */ - static expr mk_lambda(expr const & abst, expr const & new_body) { - return mk_lambda(abst_name(abst), abst_domain(abst), new_body); - } - - bool is_proposition(expr const & e) { return m_tc.is_proposition(e, context(), m_menv.to_some_menv()); } - bool is_convertible(expr const & t1, expr const & t2) { return m_tc.is_convertible(t1, t2, context(), m_menv.to_some_menv()); } - bool is_definitionally_equal(expr const & t1, expr const & t2) { - return m_tc.is_definitionally_equal(t1, t2, context(), m_menv.to_some_menv()); - } - expr infer_type(expr const & e) { return m_tc.infer_type(e, context(), m_menv.to_some_menv()); } - expr ensure_pi(expr const & e) { return m_tc.ensure_pi(e, context(), m_menv.to_some_menv()); } - expr normalize(expr const & e) { - normalizer & proc = m_tc.get_normalizer(); - return proc(e, context(), m_menv.to_some_menv()); - } - expr lift_free_vars(expr const & e, unsigned s, unsigned d) { return ::lean::lift_free_vars(e, s, d, m_menv.to_some_menv()); } - expr lower_free_vars(expr const & e, unsigned s, unsigned d) { return ::lean::lower_free_vars(e, s, d, m_menv.to_some_menv()); } - expr instantiate(expr const & e, expr const & s) { return ::lean::instantiate(e, s, m_menv.to_some_menv()); } - expr instantiate(expr const & e, unsigned n, expr const * s) { return ::lean::instantiate(e, n, s, m_menv.to_some_menv()); } - expr head_beta_reduce(expr const & t) { return ::lean::head_beta_reduce(t, m_menv.to_some_menv()); } - - expr mk_fresh_const(expr const & type) { - m_next_idx++; - return mk_constant(name(g_unique, m_next_idx), type); - } - - /** - \brief Auxiliary method for converting a proof H of (@eq A a b) into (@eq B a b) when - type A is convertible to B, but not definitionally equal. - */ - expr translate_eq_proof(expr const & A, expr const & a, expr const & b, expr const & H, expr const & B) { - if (A != B) - return mk_to_eq_th(B, a, b, mk_to_heq_th(A, a, b, H)); - else - return H; - } - - expr mk_congr1_th(expr const & f_type, expr const & f, expr const & new_f, expr const & a, expr const & Heq_f) { - expr const & A = abst_domain(f_type); - if (is_arrow(f_type)) { - expr B = lower_free_vars(abst_body(f_type), 1, 1); - return ::lean::mk_congr1_th(A, B, f, new_f, Heq_f, a); - } else { - return ::lean::mk_hcongr1_th(A, mk_lambda(g_x, A, abst_body(f_type)), f, new_f, Heq_f, a); - } - } - - expr mk_congr2_th(expr const & f_type, expr const & a, expr const & new_a, expr const & f, expr Heq_a) { - expr const & A = abst_domain(f_type); - expr B = lower_free_vars(abst_body(f_type), 1, 1); - expr a_type = infer_type(a); - if (!is_definitionally_equal(A, a_type)) - Heq_a = translate_eq_proof(a_type, a, new_a, Heq_a, A); - return ::lean::mk_congr2_th(A, B, a, new_a, f, Heq_a); - } - - expr mk_congr_th(expr const & f_type, expr const & f, expr const & new_f, expr const & a, expr const & new_a, - expr const & Heq_f, expr Heq_a) { - expr const & A = abst_domain(f_type); - expr B = lower_free_vars(abst_body(f_type), 1, 1); - expr a_type = infer_type(a); - if (!is_definitionally_equal(A, a_type)) - Heq_a = translate_eq_proof(a_type, a, new_a, Heq_a, A); - return ::lean::mk_congr_th(A, B, f, new_f, a, new_a, Heq_f, Heq_a); - } - - expr get_proof(result const & rhs) { - if (rhs.m_proof) { - return *rhs.m_proof; - } else { - // lhs and rhs are definitionally equal - return mk_refl_th(infer_type(rhs.m_expr), rhs.m_expr); - } - } - - /** - \brief Return true if \c e is definitionally equal to (Type U) - - This is an approximated solution. It may return false for cases where \c e - is definitionally to TypeU. - */ - bool is_TypeU(expr const & e) { - if (is_type(e)) { - return e == TypeU; - } else if (is_constant(e)) { - auto obj = m_env->find_object(const_name(e)); - return obj && obj->is_definition() && is_TypeU(obj->get_value()); - } else { - return false; - } - } - - /** - \brief Create heterogeneous congruence proof. - */ - optional mk_hcongr_th(expr const & f_type, expr const & new_f_type, expr const & f, expr const & new_f, - expr const & Heq_f, expr const & a, result const & new_a, - // the following two arguments are used only for invoking the simplifier monitor - expr const & e, unsigned i) { - expr const & A = abst_domain(f_type); - expr const & new_A = abst_domain(new_f_type); - expr a_type = infer_type(a); - expr new_a_type = infer_type(new_a.m_expr); - if (!is_convertible(new_a_type, new_A)) { - if (m_monitor) - m_monitor->failed_app_eh(ro_simplifier(m_this), e, i, simplifier_monitor::failure_kind::TypeMismatch); - return none_expr(); // failed - } - expr Heq_a = get_proof(new_a); - if (!new_a.is_heq_proof()) - Heq_a = mk_to_heq_th(a_type, a, new_a.m_expr, Heq_a); - return some_expr(::lean::mk_hcongr_th(A, - new_A, - mk_lambda(f_type, abst_body(f_type)), - mk_lambda(new_f_type, abst_body(new_f_type)), - f, new_f, a, new_a.m_expr, Heq_f, Heq_a)); - } - - /** - \brief Given - a = b_res.m_expr with proof b_res.m_proof - b_res.m_expr = c with proof H_bc - This method returns a new result r s.t. r.m_expr == c and a proof of a = c - */ - result mk_trans_result(expr const & a, result const & b_res, expr const & c, expr H_bc) { - if (m_proofs_enabled) { - if (!b_res.m_proof) { - // The proof of a = b is reflexivity - return result(c, H_bc); - } else { - expr const & b = b_res.m_expr; - expr new_proof; - bool heq_proof = false; - if (b_res.is_heq_proof()) { - expr b_type = infer_type(b); - new_proof = ::lean::mk_htrans_th(infer_type(a), b_type, b_type, /* b and c must have the same type */ - a, b, c, *b_res.m_proof, mk_to_heq_th(b_type, b, c, H_bc)); - heq_proof = true; - } else { - new_proof = ::lean::mk_trans_th(infer_type(a), a, b, c, *b_res.m_proof, H_bc); - } - return result(c, new_proof, heq_proof); - } - } else { - return result(c); - } - } - - /** - \brief Given - a = b_res.m_expr with proof b_res.m_proof - b_res.m_expr = c_res.m_expr with proof c_res.m_proof - - This method returns a new result r s.t. r.m_expr == c and a proof of a = c_res.m_expr - */ - result mk_trans_result(expr const & a, result const & b_res, result const & c_res) { - if (m_proofs_enabled) { - if (!b_res.m_proof) { - // the proof of a == b is reflexivity - return c_res; - } else if (!c_res.m_proof) { - // the proof of b == c is reflexivity - return b_res.update_expr(c_res.m_expr); - } else { - bool heq_proof = b_res.is_heq_proof() || c_res.is_heq_proof(); - expr new_proof; - expr const & b = b_res.m_expr; - expr const & c = c_res.m_expr; - if (heq_proof) { - expr a_type = infer_type(a); - expr b_type = infer_type(b); - expr c_type = infer_type(c); - expr H_ab = *b_res.m_proof; - if (!b_res.is_heq_proof()) - H_ab = mk_to_heq_th(a_type, a, b, H_ab); - expr H_bc = *c_res.m_proof; - if (!c_res.is_heq_proof()) - H_bc = mk_to_heq_th(b_type, b, c, H_bc); - new_proof = ::lean::mk_htrans_th(a_type, b_type, c_type, a, b, c, H_ab, H_bc); - } else { - new_proof = ::lean::mk_trans_th(infer_type(a), a, b, c, *b_res.m_proof, *c_res.m_proof); - } - return result(c, new_proof, heq_proof); - } - } else { - // proof generation is disabled - return c_res; - } - } - - expr mk_app_prefix(unsigned i, expr const & a) { - lean_assert(i > 0); - if (i == 1) - return arg(a, 0); - else - return mk_app(i, &arg(a, 0)); - } - - expr mk_app_prefix(unsigned i, buffer const & args) { - lean_assert(i > 0); - if (i == 1) - return args[0]; - else - return mk_app(i, args.data()); - } - - result simplify_app(expr const & e) { - if (m_use_heq && is_cast(e)) { - // e is of the form (cast A B H a) - // a : A - // e : B - expr A = arg(e, 1); - expr B = arg(e, 2); - expr H = arg(e, 3); - expr a = arg(e, 4); - if (m_proofs_enabled) { - result res_a = simplify(a); - expr c = res_a.m_expr; - if (res_a.m_proof) { - expr Hec; - expr Hac = *res_a.m_proof; - if (!res_a.is_heq_proof()) { - Hec = ::lean::mk_htrans_th(B, A, A, e, a, c, - update_app(e, 0, mk_cast_heq_fn()), // cast A B H a == a - mk_to_heq_th(infer_type(a), a, c, Hac)); // a == c - } else { - Hec = ::lean::mk_htrans_th(B, A, infer_type(c), e, a, c, - update_app(e, 0, mk_cast_heq_fn()), // cast A B H a == a - Hac); // a == c - } - return result(c, Hec, true); - - } else { - // c is definitionally equal to a - // So, we use cast_heq theorem cast_heq : cast A B H a == a - return result(c, update_app(e, 0, mk_cast_heq_fn()), true); - } - } else { - return simplify(arg(e, 4)); - } - } - if (m_contextual) { - expr const & f = arg(e, 0); - for (auto congr_th : m_congr_thms) { - if (congr_th->get_fun() == f) - return simplify_app_congr(e, *congr_th); - } - } - return simplify_app_default(e); - } - - /** - \brief Make sure the proof in rhs is using homogeneous equality, and return true. - If it is not possible to transform it in a homogeneous equality proof, then return false. - */ - bool ensure_homogeneous(expr const & lhs, result & rhs) { - if (rhs.is_heq_proof()) { - // try to convert back to homogeneous - lean_assert(rhs.m_proof); - expr lhs_type = infer_type(lhs); - expr rhs_type = infer_type(rhs.m_expr); - if (is_definitionally_equal(lhs_type, rhs_type)) { - // move back to homogeneous equality using to_eq - rhs.m_proof = mk_to_eq_th(lhs_type, lhs, rhs.m_expr, *rhs.m_proof); - return true; - } else { - return false; - } - } else { - return true; - } - } - - void ensure_heterogeneous(expr const & lhs, result & rhs) { - if (!rhs.is_heq_proof()) { - if (!rhs.m_proof) - rhs.m_proof = mk_hrefl_th(infer_type(lhs), lhs); - else - rhs.m_proof = mk_to_heq_th(infer_type(lhs), lhs, rhs.m_expr, *rhs.m_proof); - rhs.m_heq_proof = true; - } - } - - /** - \brief Simplify \c e under the new assumption \c H. - - \remark \c H must be a constant of type P, where P is a proposition. - - \pre is_constant(H) && const_type(H) - */ - result simplify_using(expr const & e, expr const & H) { - lean_assert(is_constant(H) && const_type(H)); - updt_rule_set update(*this, H); - return simplify(e); - } - - /** - \brief Simplify \c e using H : old_x == new_x - */ - result simplify_remapping_constant(expr const & e, expr const & old_x, expr const & new_x, expr const & H) { - updt_const_map update(*this, old_x, new_x, H); - return simplify(e); - } - - /** - \brief Simplify \c e using the given congruence theorem. - See congr.h for a description of congr_theorem_info. - */ - result simplify_app_congr(expr const & e, congr_theorem_info const & cg_thm) { - lean_assert(is_app(e)); - lean_assert(arg(e, 0) == cg_thm.get_fun()); - buffer new_args; - bool changed = false; - new_args.resize(num_args(e)); - new_args[0] = arg(e, 0); - buffer proof_args_buf; - expr * proof_args = nullptr; - if (m_proofs_enabled) { - proof_args_buf.resize(cg_thm.get_num_proof_args() + 1); - proof_args_buf[0] = cg_thm.get_proof(); - proof_args = proof_args_buf.data()+1; - } - for (auto const & info : cg_thm.get_arg_info()) { - unsigned pos = info.get_arg_pos(); - expr const & a = arg(e, pos); - if (info.should_simplify()) { - optional const & ctx = info.get_context(); - if (!ctx) { - // argument does not have a context - result res_a = simplify(a); - new_args[pos] = res_a.m_expr; - if (m_proofs_enabled) { - if (!ensure_homogeneous(a, res_a)) - return simplify_app_default(e); // fallback to default congruence - proof_args[info.get_pos_at_proof()] = a; - proof_args[*info.get_new_pos_at_proof()] = new_args[pos]; - proof_args[*info.get_proof_pos_at_proof()] = get_proof(res_a); - } - } else { - unsigned dep_pos = ctx->get_arg_pos(); - expr C = ctx->use_new_val() ? new_args[dep_pos] : arg(e, dep_pos); - if (!ctx->is_pos_dep()) - C = mk_not(C); - // We will simplify the \c a under the hypothesis C - expr H = mk_fresh_const(C); - result res_a = simplify_using(a, H); - new_args[pos] = res_a.m_expr; - if (m_proofs_enabled) { - if (!ensure_homogeneous(a, res_a)) - return simplify_app_default(e); // fallback to default congruence - proof_args[info.get_pos_at_proof()] = a; - proof_args[*info.get_new_pos_at_proof()] = new_args[pos]; - name C_name(g_C, m_next_idx++); // H is a cryptic unique name - proof_args[*info.get_proof_pos_at_proof()] = mk_lambda(C_name, C, abstract(get_proof(res_a), H)); - } - } - if (new_args[pos] != a) - changed = true; - } else { - // argument should not be simplified - new_args[pos] = arg(e, pos); - if (m_proofs_enabled) - proof_args[info.get_pos_at_proof()] = arg(e, pos); - } - } - - if (!changed) { - return rewrite_app(e, result(e)); - } else if (!m_proofs_enabled) { - return rewrite_app(e, result(mk_app(new_args))); - } else { - return rewrite_app(e, result(mk_app(new_args), mk_app(proof_args_buf))); - } - } - - result simplify_app_default(expr const & e) { - lean_assert(is_app(e)); - buffer new_args; - buffer> proofs; // used only if m_proofs_enabled - buffer f_types, new_f_types; // used only if m_proofs_enabled - buffer heq_proofs; // used only if m_use_heq && m_proofs_enabled - bool changed = false; - expr f = arg(e, 0); - expr f_type = infer_type(f); - result res_f = simplify(f); - expr new_f = res_f.m_expr; - expr new_f_type; - if (new_f != f) - changed = true; - new_args.push_back(new_f); - if (m_proofs_enabled) { - proofs.push_back(res_f.m_proof); - f_types.push_back(f_type); - new_f_type = res_f.is_heq_proof() ? infer_type(new_f) : f_type; - new_f_types.push_back(new_f_type); - if (m_use_heq) - heq_proofs.push_back(res_f.is_heq_proof()); - } - unsigned num = num_args(e); - for (unsigned i = 1; i < num; i++) { - f_type = ensure_pi(f_type); - bool f_arrow = is_arrow(f_type); - expr const & a = arg(e, i); - result res_a(a); - if (m_use_heq || f_arrow) { - res_a = simplify(a); - if (res_a.m_expr != a) - changed = true; - } - expr new_a = res_a.m_expr; - new_args.push_back(new_a); - if (m_proofs_enabled) { - proofs.push_back(res_a.m_proof); - if (m_use_heq) - heq_proofs.push_back(res_a.is_heq_proof()); - bool changed_f_type = !is_eqp(f_type, new_f_type); - if (f_arrow) { - f_type = lower_free_vars(abst_body(f_type), 1, 1); - new_f_type = changed_f_type ? lower_free_vars(abst_body(new_f_type), 1, 1) : f_type; - } else if (is_eqp(a, new_a)) { - f_type = pi_body_at(f_type, a); - new_f_type = changed_f_type ? pi_body_at(new_f_type, a) : f_type; - } else { - f_type = pi_body_at(f_type, a); - new_f_type = pi_body_at(new_f_type, new_a); - } - f_types.push_back(f_type); - new_f_types.push_back(new_f_type); - } - } - - if (!changed) { - return rewrite_app(e, result(e)); - } else if (!m_proofs_enabled) { - return rewrite_app(e, result(mk_app(new_args))); - } else { - expr out = mk_app(new_args); - unsigned i = 0; - while (i < num && !proofs[i]) { - // skip "reflexive" proofs - i++; - } - if (i == num) - return rewrite_app(e, result(out)); - expr pr; - bool heq_proof = false; - if (i == 0) { - pr = *(proofs[0]); - heq_proof = m_use_heq && heq_proofs[0]; - } else if (m_use_heq && (heq_proofs[i] || !is_arrow(f_types[i-1]))) { - expr f = mk_app_prefix(i, new_args); - expr pr_i = *proofs[i]; - auto new_pr = mk_hcongr_th(f_types[i-1], f_types[i-1], f, f, mk_hrefl_th(f_types[i-1], f), - arg(e, i), result(new_args[i], pr_i, heq_proofs[i]), - e, i); - if (!new_pr) - return rewrite_app(e, result(e)); // failed to create congruence proof - pr = *new_pr; - heq_proof = true; - } else { - expr f = mk_app_prefix(i, new_args); - pr = mk_congr2_th(f_types[i-1], arg(e, i), new_args[i], f, *(proofs[i])); - } - i++; - for (; i < num; i++) { - expr f = mk_app_prefix(i, e); - expr new_f = mk_app_prefix(i, new_args); - if (proofs[i]) { - expr pr_i = *proofs[i]; - if (m_use_heq && heq_proofs[i]) { - if (!heq_proof) - pr = mk_to_heq_th(f_types[i], f, new_f, pr); - auto new_pr = mk_hcongr_th(f_types[i-1], new_f_types[i-1], f, new_f, pr, - arg(e, i), result(new_args[i], pr_i, true), - e, i); - if (!new_pr) - return rewrite_app(e, result(e)); // failed to create congruence proof - pr = *new_pr; - heq_proof = true; - } else if (heq_proof) { - lean_assert(!heq_proofs[i]); - auto new_pr = mk_hcongr_th(f_types[i-1], new_f_types[i-1], f, new_f, pr, - arg(e, i), result(new_args[i], pr_i, false), - e, i); - if (!new_pr) - return rewrite_app(e, result(e)); // failed to create congruence proof - pr = *new_pr; - } else { - pr = mk_congr_th(f_types[i-1], f, new_f, arg(e, i), new_args[i], pr, pr_i); - } - } else if (heq_proof) { - auto new_pr = mk_hcongr_th(f_types[i-1], new_f_types[i-1], f, new_f, pr, - arg(e, i), result(arg(e, i)), - e, i); - if (!new_pr) - return rewrite_app(e, result(e)); // failed to create congruence proof - pr = *new_pr; - } else { - lean_assert(!heq_proof); - pr = mk_congr1_th(f_types[i-1], f, new_f, arg(e, i), pr); - } - } - return rewrite_app(e, result(out, pr, heq_proof)); - } - } - - /** \brief Return true when \c e is a value from the point of view of the simplifier */ - static bool is_value(expr const & e) { - // Currently only semantic attachments are treated as value. - // We may relax that in the future. - return ::lean::is_value(e) || is_true(e) || is_false(e); - } - - /** - \brief Return true iff the simplifier should use the evaluator/normalizer to reduce application - */ - bool evaluate_app(expr const & e) const { - lean_assert(is_app(e)); - // only evaluate if it is enabled - if (!m_eval) - return false; - // if all arguments are values, we should evaluate - if (std::all_of(args(e).begin()+1, args(e).end(), [](expr const & a) { return is_value(a); })) - return true; - // The previous test fails for equality/disequality because the first arguments are types. - // Should we have something more general for cases like that? - // Some possibilities: - // - We have a table mapping constants to argument positions. The positions tell the simplifier - // which arguments must be value to trigger evaluation. - // - We have an external predicate that is invoked by the simplifier to decide whether to normalize/evaluate an - // expression. - unsigned num = num_args(e); - return - (is_eq(e) || is_neq(e) || is_heq(e)) && - is_value(arg(e, num-2)) && - is_value(arg(e, num-1)); - } - - /** - \brief Given (applications) lhs and rhs s.t. lhs = rhs.m_expr - with proof rhs.m_proof, this method applies rewrite rules, beta - and evaluation to \c rhs.m_expr, and return a new result object - new_rhs s.t. lhs = new_rhs.m_expr with proof new_rhs.m_proof - - \pre is_app(lhs) - \pre is_app(rhs.m_expr) - */ - result rewrite_app(expr const & lhs, result const & rhs) { - lean_assert(is_app(rhs.m_expr)); - lean_assert(is_app(lhs)); - if (evaluate_app(rhs.m_expr)) { - // try to evaluate if all arguments are values. - expr new_rhs = normalize(rhs.m_expr); - if (is_value(new_rhs)) { - // We don't need to create a new proof term since rhs.m_expr and new_rhs are - // definitionally equal. - return rewrite(lhs, rhs.update_expr(new_rhs)); - } - } - - expr f = arg(rhs.m_expr, 0); - if (m_beta && is_lambda(f)) { - expr new_rhs = head_beta_reduce(rhs.m_expr); - // rhs.m_expr and new_rhs are also definitionally equal - return rewrite(lhs, rhs.update_expr(new_rhs)); - } - return rewrite(lhs, rhs); - } - - - bool found_all_args(unsigned num, buffer> const & subst, buffer & new_args) { - for (unsigned i = 0; i < num; i++) { - if (!subst[i]) - return false; - new_args[i+1] = *subst[i]; - } - return true; - } - - struct rename_binder_names_fn : public replace_visitor { - name_map const & m_name_subst; - rename_binder_names_fn(name_map const & s):m_name_subst(s) {} - virtual expr visit_abst(expr const & e, context const & ctx) { - auto it = m_name_subst.find(abst_name(e)); - if (it != m_name_subst.end()) { - if (is_lambda(e)) - return replace_visitor::visit_abst(mk_lambda(it->second, abst_domain(e), abst_body(e)), ctx); - else - return replace_visitor::visit_abst(mk_pi(it->second, abst_domain(e), abst_body(e)), ctx); - } else { - return replace_visitor::visit_abst(e, ctx); - } - } - }; - - expr rename_binder_names(expr const & e, name_map const & name_subst) { - if (m_preserve_binder_names && !name_subst.empty()) - return rename_binder_names_fn(name_subst)(e); - else - return e; - } - - /** - \brief Given lhs and rhs s.t. lhs = rhs.m_expr with proof rhs.m_proof, - this method applies rewrite rules, beta and evaluation to \c rhs.m_expr, - and return a new result object new_rhs s.t. - lhs = new_rhs.m_expr - with proof new_rhs.m_proof - */ - result rewrite(expr const & lhs, result const & rhs) { - expr target = rhs.m_expr; - buffer> subst; - buffer new_args; - expr new_rhs; - expr new_proof; - auto check_rule_fn = [&](rewrite_rule const & rule) -> bool { - unsigned num = rule.get_num_args(); - subst.clear(); - subst.resize(num); - m_name_subst.clear(); - if (hop_match(rule.get_lhs(), target, subst, optional(m_env), - m_menv.to_some_menv(), &m_name_subst)) { - new_args.clear(); - new_args.resize(num+1); - if (found_all_args(num, subst, new_args)) { - // easy case: all arguments found - expr rhs = rename_binder_names(rule.get_rhs(), m_name_subst); - new_rhs = instantiate(rhs, num, new_args.data() + 1); - if (rule.is_permutation() && !is_lt(new_rhs, target, false)) - return false; - if (rule.must_check_types()) { - // This check is needed because of universe cumulativity. - // Consider the following example: - // - // universe U >= 2 - // variable f (A : (Type 1)) : (Type 1) - // axiom Ax1 (a : Type) : f a = a - // rewrite_set S - // add_rewrite Ax1 eq_id : S - // theorem T1 (A : (Type 1)) : f A = A - // := by simp S - // - // The axiom Ax1 is only for arguments convertible to Type (i.e., Type 0), but - // argument A in T1 lives in (Type 1) - // - // In many cases, we can statically determine that this check is not needed. - // By statically, we mean the time we are inserting ceqs into rewrite rule sets. - expr ceq = rule.get_ceq(); - unsigned i = 0; - while (is_pi(ceq)) { - expr arg = new_args[i+1]; - if (!is_convertible(infer_type(arg), abst_domain(ceq))) { - if (m_monitor) - m_monitor->failed_rewrite_eh(ro_simplifier(m_this), target, rule.get_ceq(), rule.get_id(), - i, simplifier_monitor::failure_kind::TypeMismatch); - return false; - } - ceq = instantiate(abst_body(ceq), arg); - i = i + 1; - } - } - if (new_rhs == target) { - if (m_monitor) - m_monitor->failed_rewrite_eh(ro_simplifier(m_this), target, rule.get_ceq(), rule.get_id(), - 0, simplifier_monitor::failure_kind::LoopPrevention); - return false; - } - if (m_proofs_enabled) { - if (num > 0) { - new_args[0] = rule.get_proof(); - new_proof = mk_app(new_args); - } else { - new_proof = rule.get_proof(); - } - } - if (m_monitor) - m_monitor->rewrite_eh(ro_simplifier(m_this), target, new_rhs, rule.get_ceq(), rule.get_id()); - return true; - } else { - // Conditional rewriting: we try to fill the missing - // arguments by trying to find a proof for ones that are - // propositions. - expr ceq = rename_binder_names(rule.get_ceq(), m_name_subst); - buffer & proof_args = new_args; - proof_args.clear(); - if (m_proofs_enabled) - proof_args.push_back(rule.get_proof()); - for (unsigned i = 0; i < num; i++) { - lean_assert(is_pi(ceq)); - if (subst[i]) { - if (rule.must_check_types() && !is_convertible(infer_type(*subst[i]), abst_domain(ceq))) { - // See before the previous is_convertible - if (m_monitor) - m_monitor->failed_rewrite_eh(ro_simplifier(m_this), target, rule.get_ceq(), rule.get_id(), - i, simplifier_monitor::failure_kind::TypeMismatch); - return false; - } - ceq = instantiate(abst_body(ceq), *subst[i]); - if (m_proofs_enabled) - proof_args.push_back(*subst[i]); - } else { - expr d = abst_domain(ceq); - if (is_proposition(d)) { - result d_res = simplify(d); - if (d_res.m_expr == True) { - if (m_proofs_enabled) { - expr d_proof; - if (!d_res.m_proof) { - // No proof available. So d should be definitionally equal to True - d_proof = mk_trivial(); - } else if (d_res.m_heq_proof) { - d_proof = mk_heqt_elim_th(d, *d_res.m_proof); - } else { - d_proof = mk_eqt_elim_th(d, *d_res.m_proof); - } - ceq = instantiate(abst_body(ceq), d_proof); - proof_args.push_back(d_proof); - } else if (is_arrow(ceq)) { - ceq = lower_free_vars(abst_body(ceq), 1, 1); - } else { - // The body of ceq depends on this argument, - // but proof generation is not enabled. - // So, we should fail - if (m_monitor) - m_monitor->failed_rewrite_eh(ro_simplifier(m_this), target, rule.get_ceq(), rule.get_id(), - i, simplifier_monitor::failure_kind::Unsupported); - return false; - } - } else { - // failed to prove proposition - if (m_monitor) - m_monitor->failed_rewrite_eh(ro_simplifier(m_this), target, rule.get_ceq(), rule.get_id(), - i, simplifier_monitor::failure_kind::AssumptionNotProved); - return false; - } - } else { - // failed, the argument is not a proposition - if (m_monitor) - m_monitor->failed_rewrite_eh(ro_simplifier(m_this), target, rule.get_ceq(), rule.get_id(), - i, simplifier_monitor::failure_kind::MissingArgument); - return false; - } - } - } - new_proof = mk_app(proof_args); - new_rhs = arg(ceq, num_args(ceq) - 1); - if (new_rhs == target || (rule.is_permutation() && !is_lt(new_rhs, target, false))) { - if (m_monitor) - m_monitor->failed_rewrite_eh(ro_simplifier(m_this), target, rule.get_ceq(), rule.get_id(), - 0, simplifier_monitor::failure_kind::LoopPrevention); - return false; - } - if (m_monitor) - m_monitor->rewrite_eh(ro_simplifier(m_this), target, new_rhs, rule.get_ceq(), rule.get_id()); - return true; - } - } - return false; - }; - // Traverse all rule sets - for (rewrite_rule_set const & rs : m_rule_sets) { - if (rs.find_match(target, check_rule_fn)) { - // the result is in new_rhs and proof at new_proof - result new_r1 = mk_trans_result(lhs, rhs, new_rhs, new_proof); - if (m_single_pass) { - return new_r1; - } else { - result new_r2 = simplify(new_r1.m_expr); - return mk_trans_result(lhs, new_r1, new_r2); - } - } - } - if (!m_single_pass && lhs != rhs.m_expr) { - result new_rhs = simplify(rhs.m_expr); - return mk_trans_result(lhs, rhs, new_rhs); - } else { - return rhs; - } - } - - result simplify_constant(expr const & e) { - lean_assert(is_constant(e)); - auto it = m_const_map.find(e); - if (it != m_const_map.end()) { - return it->second; - } else if (m_unfold || m_eval) { - auto obj = m_env->find_object(const_name(e)); - if (obj) { - if (m_unfold && should_unfold(obj)) { - expr e = obj->get_value(); - if (m_single_pass) { - return result(e); - } else { - return simplify(e); - } - } - if (m_eval && obj->is_builtin()) { - return result(obj->get_value()); - } - } - } - return rewrite(e, result(e)); - } - - /** - \brief Return true iff Eta-reduction can be applied to \c e. - - \remark Actually this is a partial test. Given, - fun x : T, f x - This method does not check whether f has type - Pi x : T, B x - This check must be performed in the caller. - Otherwise the proof (eta T (fun x : T, B x) f) will not type check. - */ - bool is_eta_target(expr const & e) const { - if (is_lambda(e)) { - expr b = abst_body(e); - return - is_app(b) && is_var(arg(b, num_args(b) - 1), 0) && - std::all_of(begin_args(b), end_args(b) - 1, [](expr const & a) { return !has_free_var(a, 0); }); - } else { - return false; - } - } - - /** - \brief Given (lambdas) lhs and rhs s.t. lhs = rhs.m_expr - with proof rhs.m_proof, this method applies rewrite rules, and - eta reduction, and return a new result object new_rhs s.t. - lhs = new_rhs.m_expr with proof new_rhs.m_proof - - \pre is_lambda(lhs) - \pre is_lambda(rhs.m_expr) - */ - result rewrite_lambda(expr const & lhs, result const & rhs) { - lean_assert(is_lambda(lhs)); - lean_assert(is_lambda(rhs.m_expr)); - if (m_eta && is_eta_target(rhs.m_expr)) { - expr b = abst_body(rhs.m_expr); - expr new_rhs; - if (num_args(b) > 2) { - new_rhs = mk_app(num_args(b) - 1, &arg(b, 0)); - } else { - new_rhs = arg(b, 0); - } - new_rhs = lower_free_vars(new_rhs, 1, 1); - expr new_rhs_type = ensure_pi(infer_type(new_rhs)); - if (is_definitionally_equal(abst_domain(new_rhs_type), abst_domain(rhs.m_expr))) { - if (m_proofs_enabled) { - expr new_proof = mk_eta_th(abst_domain(rhs.m_expr), - mk_lambda(rhs.m_expr, abst_body(new_rhs_type)), - new_rhs); - return rewrite(lhs, mk_trans_result(lhs, rhs, new_rhs, new_proof)); - } else { - return rewrite(lhs, result(new_rhs)); - } - } - } - return rewrite(lhs, rhs); - } - - /** - \brief Simplify only the body of the lambda expression, it does not 'touch' the domain. - */ - result simplify_lambda_body(expr const & e) { - lean_assert(is_lambda(e)); - expr const & d = abst_domain(e); - expr fresh_const = mk_fresh_const(d); - expr bi = instantiate(abst_body(e), fresh_const); - result res_bi = simplify(bi); - expr new_bi = res_bi.m_expr; - if (is_eqp(new_bi, bi)) - return rewrite_lambda(e, result(e)); - expr new_e = mk_lambda(e, abstract(new_bi, fresh_const)); - if (!m_proofs_enabled || !res_bi.m_proof) - return rewrite_lambda(e, result(new_e)); - if (res_bi.is_heq_proof()) { - lean_assert(m_use_heq); - // Using - // theorem hsfunext {A : Type U+1} {B B' : A → TypeU} {f : ∀ x, B x} {f' : ∀ x, B' x} : - // (∀ x, f x == f' x) → f == f' - expr new_proof = mk_hsfunext_th(d, // A - mk_lambda(e, infer_type(abst_body(e))), // B - mk_lambda(e, abstract(infer_type(new_bi), fresh_const)), // B' - e, // f - new_e, // f' - mk_lambda(g_x, d, abstract(*res_bi.m_proof, fresh_const))); - return rewrite_lambda(e, result(new_e, new_proof, true)); - } else { - expr body_type = infer_type(abst_body(e)); - // Using - // axiom funext {A : Type U} {B : A → Type U} {f g : ∀ x : A, B x} (H : ∀ x : A, f x = g x) : f = g - expr new_proof = mk_funext_th(d, mk_lambda(e, body_type), e, new_e, - mk_lambda(e, abstract(*res_bi.m_proof, fresh_const))); - return rewrite_lambda(e, result(new_e, new_proof)); - } - } - - /** - \brief Simplify a lambda abstraction when the heq module is available. - In this case, we can simplify the domain and body of the lambda expression. - */ - result simplify_lambda_with_heq(expr const & e) { - expr const & d = abst_domain(e); - result res_d = simplify(d); - expr new_d = res_d.m_expr; - if (is_eqp(d, new_d)) - return simplify_lambda_body(e); - if (is_definitionally_equal(d, new_d)) - return simplify_lambda_body(update_lambda(e, new_d, abst_body(e))); - // d and new_d are only provably equal, so we need to use hfunext - expr x_old = mk_fresh_const(d); - expr x_new = mk_fresh_const(new_d); - expr x_old_eq_x_new = mk_heq(x_old, x_new); - expr H_x_old_eq_x_new = mk_fresh_const(x_old_eq_x_new); - expr bi = instantiate(abst_body(e), x_old); - result res_bi = simplify_remapping_constant(bi, x_old, x_new, H_x_old_eq_x_new); - expr new_bi = res_bi.m_expr; - if (occurs(x_old, new_bi)) { - // failed, simplifier didn't manage to replace x_old with x_new - if (m_monitor) - m_monitor->failed_abstraction_eh(ro_simplifier(m_this), e, simplifier_monitor::failure_kind::AbstractionBody); - return rewrite(e, result(e)); - } - expr new_e = update_lambda(e, new_d, abstract(new_bi, x_new)); - if (!m_proofs_enabled) - return rewrite(e, result(new_e)); - ensure_heterogeneous(d, res_d); - ensure_heterogeneous(bi, res_bi); - // Using - // axiom hfunext {A A' : Type U+1} {B : A → Type U+1} {B' : A' → Type U+1} {f : ∀ x, B x} {f' : ∀ x, B' x} : - // A == A' → (∀ x x', x == x' → f x == f' x') → f == f' - expr new_proof = mk_hfunext_th(d, // A - new_d, // A' - Fun(x_old, d, infer_type(bi)), // B - Fun(x_new, new_d, infer_type(new_bi)), // B' - e, // f - new_e, // f' - *res_d.m_proof, // A == A' - // fun (x_old : d) (x_new : new_d) (H : x_old == x_new), bi == new_bi - mk_lambda(abst_name(e), d, - mk_lambda(name(abst_name(e), 1), lift_free_vars(new_d, 0, 1), - mk_lambda(name(g_H, m_next_idx++), abstract(x_old_eq_x_new, {x_old, x_new}), - abstract(*res_bi.m_proof, {x_old, x_new, H_x_old_eq_x_new}))))); - return rewrite(e, result(new_e, new_proof, true)); - } - - result simplify_lambda(expr const & e) { - lean_assert(is_lambda(e)); - if (m_use_heq) { - return simplify_lambda_with_heq(e); - } else { - return simplify_lambda_body(e); - } - } - - /** - \brief Simplify A -> B when A -> B is a proposition. - */ - result simplify_implication(expr const & e) { - expr const & d = abst_domain(e); - expr b = abst_body(e); - if (m_contextual) { - // Contextual simplification for A -> B - // Rewrite A to A' - // And rewrite B to B' using A' - result res_d = simplify(d); - ensure_homogeneous(d, res_d); - expr new_d = res_d.m_expr; - expr H = mk_fresh_const(new_d); - expr bi = lower_free_vars(b, 1, 1); - result res_bi = simplify_using(bi, H); - expr new_bi = res_bi.m_expr; - ensure_homogeneous(bi, res_bi); - if (is_eqp(new_d, d) && is_eqp(new_bi, bi)) - return rewrite(e, result(e)); - expr new_e = update_pi(e, new_d, lift_free_vars(new_bi, 0, 1)); - if (!m_proofs_enabled) - return rewrite(e, result(new_e)); - name C_name(g_C, m_next_idx++); - expr new_proof = mk_imp_congr_th(d, bi, new_d, new_bi, - get_proof(res_d), mk_lambda(C_name, new_d, abstract(get_proof(res_bi), H))); - return rewrite(e, result(new_e, new_proof)); - } else { - // Simplify A -> B (when m_contextual == false) - result res_d = simplify(d); - expr new_d = res_d.m_expr; - ensure_homogeneous(d, res_d); - expr bi = lower_free_vars(b, 1, 1); - result res_bi = simplify(bi); - expr new_bi = res_bi.m_expr; - ensure_homogeneous(bi, res_bi); - if (is_eqp(new_d, d) && is_eqp(new_bi, bi)) - return rewrite(e, result(e)); - expr new_e = update_pi(e, new_d, lift_free_vars(new_bi, 0, 1)); - if (!m_proofs_enabled) - return rewrite(e, result(new_e)); - expr new_proof = mk_imp_congr_th(d, bi, new_d, new_bi, - get_proof(res_d), mk_lambda(g_H, new_d, lift_free_vars(get_proof(res_bi), 0, 1))); - return rewrite(e, result(new_e, new_proof)); - } - } - - /** - \brief Simplify the domain of an arrow type A -> B when it is not a proposition. - - This procedure can be used even when the heq module is not available. - */ - result simplify_arrow_domain(expr const & e) { - lean_assert(is_arrow(e)); - expr const & A = abst_domain(e); - result res_A = simplify(A); - expr const & new_A = res_A.m_expr; - if (is_eqp(A, new_A)) { - return result(e); - } else if (!m_proofs_enabled || is_definitionally_equal(A, new_A)) { - return result(update_pi(e, new_A, abst_body(e))); - } else { - expr e_type = infer_type(e); - if (is_TypeU(e_type) || !ensure_homogeneous(A, res_A)) { - if (m_monitor) - m_monitor->failed_abstraction_eh(ro_simplifier(m_this), e, simplifier_monitor::failure_kind::TypeMismatch); - return result(e); // failed, we can't use subst theorem - } else { - expr H = get_proof(res_A); - // We create the following proof term for (@eq (e_type) (A -> B) (new_A -> B)) - // @subst A_type A new_A (fun x : A_type, (@eq e_type (A -> B) (x -> B))) (@refl e_type (A -> B)) H - expr A_type = infer_type(A); - expr x_arrow_B = update_pi(e, Var(0), abst_body(e)); - expr new_proof = mk_subst_th(A_type, A, new_A, - mk_lambda(g_x, A_type, mk_eq(e_type, e, x_arrow_B)), - mk_refl_th(e_type, e), - H); - return result(update_pi(e, new_A, abst_body(e)), new_proof); - } - } - } - - /** - \brief Simplify the body of an arrow type A -> B when it is not a proposition. - - This procedure can be used even when the heq module is not available. - */ - result simplify_arrow_body(expr const & e) { - lean_assert(is_arrow(e)); - expr const & B = lower_free_vars(abst_body(e), 1, 1); - result res_B = simplify(B); - expr const & new_B = res_B.m_expr; - if (is_eqp(B, new_B)) { - return result(e); - } else if (!m_proofs_enabled || is_definitionally_equal(B, new_B)) { - return result(update_pi(e, abst_domain(e), lift_free_vars(new_B, 1, 1))); - } else { - expr e_type = infer_type(e); - if (is_TypeU(e_type) || !ensure_homogeneous(B, res_B)) { - if (m_monitor) - m_monitor->failed_abstraction_eh(ro_simplifier(m_this), e, simplifier_monitor::failure_kind::TypeMismatch); - return result(e); // failed, we can't use subst theorem - } else { - expr H = get_proof(res_B); - // We create the following proof term for (@eq (e_type) (A -> B) (A -> new_B)) - // @subst B_type B new_B (fun x : B_type, (@eq e_type (A -> B) (A -> x))) (@refl e_type (A -> B)) H - expr B_type = infer_type(B); - expr A_arrow_x = update_pi(e, abst_domain(e), Var(1)); - expr new_proof = mk_subst_th(B_type, B, new_B, - mk_lambda(g_x, B_type, mk_eq(e_type, e, A_arrow_x)), - mk_refl_th(e_type, e), - H); - return result(update_pi(e, abst_domain(e), lift_free_vars(new_B, 1, 1)), new_proof); - } - } - } - - /** - \brief Simplify A -> B when A -> B is a not proposition. - */ - result simplify_arrow(expr const & e) { - result r1 = simplify_arrow_body(e); - result r2 = simplify_arrow_domain(r1.m_expr); - return rewrite(e, mk_trans_result(e, r1, r2)); - } - - /** - \brief Simplify the body of (forall x : A, P x), when P x is a proposition. - */ - result simplify_forall_body(expr const & e) { - lean_assert(is_pi(e) && is_proposition(e)); - expr fresh_const = mk_fresh_const(abst_domain(e)); - expr const & d = abst_domain(e); - expr b = abst_body(e); - expr bi = instantiate(b, fresh_const); - result res_bi = simplify(bi); - expr new_bi = res_bi.m_expr; - if (is_eqp(new_bi, bi)) - return rewrite(e, result(e)); - expr new_e = mk_pi(abst_name(e), d, abstract(new_bi, fresh_const)); - if (!m_proofs_enabled || !res_bi.m_proof) - return rewrite(e, result(new_e)); - ensure_homogeneous(bi, res_bi); - expr new_proof = mk_allext_th(d, - mk_lambda(e, b), - mk_lambda(e, abst_body(new_e)), - mk_lambda(e, abstract(*res_bi.m_proof, fresh_const))); - return rewrite(e, result(new_e, new_proof)); - } - - /** - \brief Simplify (forall x : A, P x) proposition when the heq module is available. - In this case, we can simplify the domain and body of the forall expression. - */ - result simplify_forall_with_heq(expr const & e) { - lean_assert(is_pi(e) && is_proposition(e)); - // We don't support Pi's that are not proposition yet. - // The problem is that - // axiom hpiext {A A' : Type U+1} {B : A → Type U+1} {B' : A' → Type U+1} : - // A == A' → (∀ x x', x == x' → B x == B' x') → (∀ x, B x) == (∀ x, B' x) - // produces an equality in TypeM even if A, A', B and B' live in smaller universes. - // - // This limitation does not seem to be a big problem in practice. - expr const & d = abst_domain(e); - result res_d = simplify(d); - expr new_d = res_d.m_expr; - if (is_eqp(d, new_d)) - return simplify_forall_body(e); - if (is_definitionally_equal(d, new_d)) - return simplify_forall_body(update_pi(e, new_d, abst_body(e))); - // d and new_d are only provably equal, so we need to use hpiext or hallext - expr x_old = mk_fresh_const(d); - expr x_new = mk_fresh_const(new_d); - expr x_old_eq_x_new = mk_heq(x_old, x_new); - expr H_x_old_eq_x_new = mk_fresh_const(x_old_eq_x_new); - expr bi = instantiate(abst_body(e), x_old); - result res_bi = simplify_remapping_constant(bi, x_old, x_new, H_x_old_eq_x_new); - expr new_bi = res_bi.m_expr; - if (occurs(x_old, new_bi)) { - // failed, simplifier didn't manage to replace x_old with x_new - if (m_monitor) - m_monitor->failed_abstraction_eh(ro_simplifier(m_this), e, simplifier_monitor::failure_kind::AbstractionBody); - return rewrite(e, result(e)); - } - expr new_e = update_pi(e, new_d, abstract(new_bi, x_new)); - if (!m_proofs_enabled || is_definitionally_equal(e, new_e)) { - if (m_monitor) - m_monitor->failed_abstraction_eh(ro_simplifier(m_this), e, simplifier_monitor::failure_kind::TypeMismatch); - return rewrite(e, result(new_e)); - } - ensure_heterogeneous(d, res_d); - ensure_homogeneous(bi, res_bi); - // Remark: the argument with type A = A' in hallext and hpiext is actually @eq TypeM A A', - // so we need to translate the proof d_eq_new_d_proof : d = new_d to a TypeM equality proof - expr bi_eq_new_bi_proof = get_proof(res_bi); - // Heqb : (∀ x x', x == x' → B x = B' x') - expr Heqb = mk_lambda(abst_name(e), d, - mk_lambda(name(abst_name(e), 1), lift_free_vars(new_d, 0, 1), - mk_lambda(name(g_H, m_next_idx++), abstract(x_old_eq_x_new, {x_old, x_new}), - abstract(bi_eq_new_bi_proof, {x_old, x_new, H_x_old_eq_x_new})))); - // Using - // theorem hallext {A A' : Type U+1} {B : A → Bool} {B' : A' → Bool} : - // A == A' → (∀ x x', x == x' → B x = B' x') → (∀ x, B x) = (∀ x, B' x) - expr new_proof = mk_hallext_th(d, new_d, - Fun(x_old, d, bi), // B - Fun(x_new, new_d, new_bi), // B' - *res_d.m_proof, // A == A' - Heqb); - return rewrite(e, result(new_e, new_proof)); - } - - result simplify_pi(expr const & e) { - lean_assert(is_pi(e)); - if (is_arrow(e)) { - if (is_proposition(abst_domain(e)) && is_proposition(abst_body(e))) - return simplify_implication(e); - else - return simplify_arrow(e); - } else if (is_proposition(e)) { - if (m_use_heq) - return simplify_forall_with_heq(e); - else - return simplify_forall_body(e); - } else { - // We currently do simplify (forall x : A, B x) when it is not a proposition. - if (m_monitor) - m_monitor->failed_abstraction_eh(ro_simplifier(m_this), e, simplifier_monitor::failure_kind::Unsupported); - return result(e); - } - } - - result rewrite_heq(expr const & old_heq, result const & new_heq) { - expr const & new_lhs = heq_lhs(new_heq.m_expr); - expr const & new_rhs = heq_rhs(new_heq.m_expr); - if (new_lhs == new_rhs) { - // We currently cannot use heq_id as rewrite rule. - // heq_id (A : (Type U+1)) (a : A) : (a == a) ↔ true - // The problem is that A does not occur (even implicitly) in the left-hand-side, - // and it is not a proposition. - // In principle, we could extend the rewrite method to use type inference for computing A. - // IF we find more instances of this problem, we will do it. Before that, it is easier to test - // if the theorem is applicable here. - if (!m_proofs_enabled) { - return result(True); - } else { - return mk_trans_result(old_heq, new_heq, result(True, mk_heq_id_th(infer_type(new_lhs), new_lhs))); - } - } else { - return rewrite(old_heq, new_heq); - } - } - - result simplify_heq(expr const & e) { - lean_assert(is_heq(e)); - expr const & lhs = heq_lhs(e); - expr const & rhs = heq_rhs(e); - result new_lhs = simplify(lhs); - result new_rhs = simplify(rhs); - if (is_eqp(lhs, new_lhs.m_expr) && is_eqp(rhs, new_rhs.m_expr)) { - return rewrite_heq(e, result(e)); - } else { - expr new_heq = mk_heq(new_lhs.m_expr, new_rhs.m_expr); - if (!m_proofs_enabled) { - return rewrite_heq(e, result(new_heq)); - } else { - expr A_prime = infer_type(new_lhs.m_expr); - expr B_prime = infer_type(new_rhs.m_expr); - if (!new_lhs.is_heq_proof() && !new_rhs.is_heq_proof() && !is_TypeU(A_prime) && !is_TypeU(B_prime)) { - return rewrite_heq(e, result(new_heq, mk_heq_congr_th(A_prime, B_prime, - lhs, new_lhs.m_expr, rhs, new_rhs.m_expr, - get_proof(new_lhs), get_proof(new_rhs)))); - } else { - ensure_heterogeneous(lhs, new_lhs); - ensure_heterogeneous(rhs, new_rhs); - return rewrite_heq(e, result(new_heq, mk_hheq_congr_th(infer_type(lhs), A_prime, - infer_type(rhs), B_prime, - lhs, new_lhs.m_expr, rhs, new_rhs.m_expr, - *new_lhs.m_proof, *new_rhs.m_proof))); - } - } - } - } - - result save(expr const & e, result const & r) { - if (m_memoize) { - result new_r = r.update_expr(m_max_sharing(r.m_expr)); - m_cache.insert(mk_pair(e, new_r)); - if (m_monitor) - m_monitor->step_eh(ro_simplifier(m_this), e, new_r.m_expr, new_r.m_proof); - return new_r; - } else { - return r; - } - } - - result simplify(expr e) { - check_system("simplifier"); - m_num_steps++; - flet inc_depth(m_depth, m_depth+1); - if (m_num_steps > m_max_steps) - throw exception("simplifier failed, maximum number of steps exceeded"); - if (m_memoize) { - e = m_max_sharing(e); - auto it = m_cache.find(e); - if (it != m_cache.end()) { - return it->second; - } - } - if (m_monitor) - m_monitor->pre_eh(ro_simplifier(m_this), e); - switch (e.kind()) { - case expr_kind::Var: return result(e); - case expr_kind::Constant: return save(e, simplify_constant(e)); - case expr_kind::Type: return result(e); - case expr_kind::MetaVar: - case expr_kind::Value: return rewrite(e, result(e)); - case expr_kind::App: return save(e, simplify_app(e)); - case expr_kind::Lambda: return save(e, simplify_lambda(e)); - case expr_kind::Pi: return save(e, simplify_pi(e)); - case expr_kind::Let: return save(e, simplify(instantiate(let_body(e), let_value(e)))); - case expr_kind::HEq: return save(e, simplify_heq(e)); - } - lean_unreachable(); - } - - void collect_congr_thms() { - if (m_contextual) { - for (auto const & rs : m_rule_sets) { - rs.for_each_congr([&](congr_theorem_info const & info) { - if (std::all_of(m_congr_thms.begin(), m_congr_thms.end(), - [&](congr_theorem_info const * info2) { - return info2->get_fun() != info.get_fun(); })) { - m_congr_thms.push_back(&info); - } - }); - } - } - } - - void set_options(options const & o) { - m_proofs_enabled = get_simplifier_proofs(o); - m_contextual = get_simplifier_contextual(o); - m_single_pass = get_simplifier_single_pass(o); - m_beta = get_simplifier_beta(o); - m_eta = get_simplifier_eta(o); - m_eval = get_simplifier_eval(o); - m_unfold = get_simplifier_unfold(o); - m_conditional = get_simplifier_conditional(o); - m_memoize = get_simplifier_memoize(o); - m_max_steps = get_simplifier_max_steps(o); - m_use_heq = get_simplifier_heq(o); - m_preserve_binder_names = get_simplifier_preserve_binder_names(o); - } - -public: - imp(ro_environment const & env, options const & o, unsigned num_rs, rewrite_rule_set const * rs, - std::shared_ptr const & monitor): - m_env(env), m_options(o), m_tc(env), m_monitor(monitor) { - set_options(o); - if (m_contextual) { - // We need an extra rule set if we are performing contextual rewriting - m_rule_sets.push_back(rewrite_rule_set(env)); - } - m_rule_sets.insert(m_rule_sets.end(), rs, rs + num_rs); - collect_congr_thms(); - m_next_idx = 0; - } - - result operator()(expr const & e, optional const & menv) { - if (m_menv.update(menv)) - m_cache.clear(); - m_num_steps = 0; - m_depth = 0; - try { - auto r = simplify(e); - if (m_proofs_enabled && !r.get_proof()) - return r.update_proof(get_proof(r)); - else - return r; - } catch (stack_space_exception & ex) { - throw simplifier_stack_space_exception(); - } - } -}; - -simplifier_cell::simplifier_cell(ro_environment const & env, options const & o, unsigned num_rs, rewrite_rule_set const * rs, - std::shared_ptr const & monitor): - m_ptr(new imp(env, o, num_rs, rs, monitor)) { -} - -simplifier_cell::result simplifier_cell::operator()(expr const & e, optional const & menv) { - return m_ptr->operator()(e, menv); -} -void simplifier_cell::clear() { return m_ptr->m_cache.clear(); } -unsigned simplifier_cell::get_depth() const { return m_ptr->m_depth; } -ro_environment const & simplifier_cell::get_environment() const { return m_ptr->m_env; } -options const & simplifier_cell::get_options() const { return m_ptr->m_options; } - -simplifier::simplifier(ro_environment const & env, options const & o, unsigned num_rs, rewrite_rule_set const * rs, - std::shared_ptr const & monitor): - m_ptr(std::make_shared(env, o, num_rs, rs, monitor)) { - m_ptr->m_ptr->m_this = m_ptr; -} - -ro_simplifier::ro_simplifier(simplifier const & env): - m_ptr(env.m_ptr) { -} - -ro_simplifier::ro_simplifier(weak_ref const & r) { - if (r.expired()) - throw exception("weak reference to simplifier object has expired (i.e., the simplifier has been deleted)"); - m_ptr = r.lock(); -} - -simplifier::result simplify(expr const & e, ro_environment const & env, options const & opts, - unsigned num_rs, rewrite_rule_set const * rs, - optional const & menv, - std::shared_ptr const & monitor) { - return simplifier(env, opts, num_rs, rs, monitor)(e, menv); -} - -simplifier::result simplify(expr const & e, ro_environment const & env, options const & opts, - unsigned num_ns, name const * ns, - optional const & menv, - std::shared_ptr const & monitor) { - buffer rules; - for (unsigned i = 0; i < num_ns; i++) - rules.push_back(get_rewrite_rule_set(env, ns[i])); - return simplify(e, env, opts, num_ns, rules.data(), menv, monitor); -} - -simplifier_stack_space_exception::simplifier_stack_space_exception():stack_space_exception("simplifier") {} -char const * simplifier_stack_space_exception::what() const noexcept { - return "deep recursion was detected at 'simplifier', this is probably due to a non-terminating set of rewrite rules, you may use a simplifier_monitor object to track the simplifier behavior (see the simplifier manual); if your problem is very big, you may try to increase stack space in your system"; -} -exception * simplifier_stack_space_exception::clone() const { return new simplifier_stack_space_exception(); } -void simplifier_stack_space_exception::rethrow() const { throw *this; } - -DECL_UDATA(simplifier) -DECL_UDATA(ro_simplifier) - -/** - \brief Simplifier monitor implemented using Lua functions -*/ -class lua_simplifier_monitor : public simplifier_monitor { - optional m_pre_eh; - optional m_step_eh; - optional m_rewrite_eh; - optional m_failed_app_eh; - optional m_failed_rewrite_eh; - optional m_failed_abstraction_eh; -public: - lua_simplifier_monitor(optional const & pre_eh, optional const & step_eh, optional const & rewrite_eh, - optional const & failed_app_eh, optional const & failed_rewrite_eh, optional const & failed_abstraction_eh): - m_pre_eh(pre_eh), m_step_eh(step_eh), m_rewrite_eh(rewrite_eh), - m_failed_app_eh(failed_app_eh), m_failed_rewrite_eh(failed_rewrite_eh), m_failed_abstraction_eh(failed_abstraction_eh) { - } - virtual ~lua_simplifier_monitor() {} - - virtual void pre_eh(ro_simplifier const & s, expr const & e) { - if (m_pre_eh) { - lua_State * L = m_pre_eh->get_state(); - m_pre_eh->push(); - push_ro_simplifier(L, s); - push_expr(L, e); - pcall(L, 2, 0, 0); - } - } - - virtual void step_eh(ro_simplifier const & s, expr const & e, expr const & new_e, optional const & pr) { - if (m_step_eh) { - lua_State * L = m_step_eh->get_state(); - m_step_eh->push(); - push_ro_simplifier(L, s); - push_expr(L, e); - push_expr(L, new_e); - push_optional_expr(L, pr); - pcall(L, 4, 0, 0); - } - } - - virtual void rewrite_eh(ro_simplifier const & s, expr const & e, expr const & new_e, expr const & ceq, name const & ceq_id) { - if (m_rewrite_eh) { - lua_State * L = m_rewrite_eh->get_state(); - m_rewrite_eh->push(); - push_ro_simplifier(L, s); - push_expr(L, e); - push_expr(L, new_e); - push_expr(L, ceq); - push_name(L, ceq_id); - pcall(L, 5, 0, 0); - } - } - - virtual void failed_app_eh(ro_simplifier const & s, expr const & e, unsigned i, failure_kind k) { - if (m_failed_app_eh) { - lua_State * L = m_failed_app_eh->get_state(); - m_failed_app_eh->push(); - push_ro_simplifier(L, s); - push_expr(L, e); - lua_pushinteger(L, i); - lua_pushinteger(L, static_cast(k)); - pcall(L, 4, 0, 0); - } - } - - virtual void failed_rewrite_eh(ro_simplifier const & s, expr const & e, expr const & ceq, name const & ceq_id, unsigned i, failure_kind k) { - if (m_failed_rewrite_eh) { - lua_State * L = m_failed_rewrite_eh->get_state(); - m_failed_rewrite_eh->push(); - push_ro_simplifier(L, s); - push_expr(L, e); - push_expr(L, ceq); - push_name(L, ceq_id); - lua_pushinteger(L, i); - lua_pushinteger(L, static_cast(k)); - pcall(L, 6, 0, 0); - } - } - - virtual void failed_abstraction_eh(ro_simplifier const & s, expr const & e, failure_kind k) { - if (m_failed_abstraction_eh) { - lua_State * L = m_failed_abstraction_eh->get_state(); - m_failed_abstraction_eh->push(); - push_ro_simplifier(L, s); - push_expr(L, e); - lua_pushinteger(L, static_cast(k)); - pcall(L, 3, 0, 0); - } - } -}; - -typedef std::shared_ptr simplifier_monitor_ptr; - -DECL_UDATA(simplifier_monitor_ptr) - -static const struct luaL_Reg simplifier_monitor_ptr_m[] = { - {"__gc", simplifier_monitor_ptr_gc}, - {0, 0} -}; - -static optional get_opt_callback(lua_State * L, int i) { - if (i > lua_gettop(L) || lua_isnil(L, i)) { - return optional(); - } else { - luaL_checktype(L, i, LUA_TFUNCTION); // user-fun - return optional(luaref(L, i)); - } -} - -static int mk_simplifier_monitor(lua_State * L) { - simplifier_monitor_ptr r = std::make_shared(get_opt_callback(L, 1), - get_opt_callback(L, 2), - get_opt_callback(L, 3), - get_opt_callback(L, 4), - get_opt_callback(L, 5), - get_opt_callback(L, 6)); - return push_simplifier_monitor_ptr(L, r); -} - -/** - \brief Fill the the rewrite_rule_set \c rs using the object at position \c i in the Lua stack. -*/ -static void get_rewrite_rule_set(lua_State * L, int i, ro_environment const & env, buffer & rs) { - if (i > lua_gettop(L)) { - rs.push_back(get_rewrite_rule_set(env)); - } else if (lua_isstring(L, i)) { - rs.push_back(get_rewrite_rule_set(env, to_name_ext(L, i))); - } else { - luaL_checktype(L, i, LUA_TTABLE); - name r; - int n = objlen(L, i); - for (int j = 1; j <= n; j++) { - lua_rawgeti(L, i, j); - rs.push_back(get_rewrite_rule_set(env, to_name_ext(L, -1))); - lua_pop(L, 1); - } - } -} - -static int mk_simplifier(lua_State * L, ro_environment const & env) { - int nargs = lua_gettop(L); - buffer rules; - get_rewrite_rule_set(L, 1, env, rules); - options opts; - if (nargs >= 2) - opts = to_options(L, 2); - simplifier_monitor_ptr monitor; - if (nargs >= 3 && !lua_isnil(L, 3)) - monitor = to_simplifier_monitor_ptr(L, 3); - return push_simplifier(L, simplifier(env, opts, rules.size(), rules.data(), monitor)); -} - -static int mk_simplifier(lua_State * L) { - int nargs = lua_gettop(L); - if (nargs <= 3) - return mk_simplifier(L, ro_shared_environment(L)); - else - return mk_simplifier(L, ro_shared_environment(L, 4)); -} - -static int simplifier_apply(lua_State * L) { - int nargs = lua_gettop(L); - simplifier::result r; - if (nargs == 2) - r = to_simplifier(L, 1)(to_expr(L, 2), none_ro_menv()); - else - r = to_simplifier(L, 1)(to_expr(L, 2), some_ro_menv(to_metavar_env(L, 3))); - push_expr(L, r.get_expr()); - push_optional_expr(L, r.get_proof()); - lua_pushboolean(L, r.is_heq_proof()); - return 3; -} - -static int simplifier_clear(lua_State * L) { to_simplifier(L, 1)->clear(); return 0; } -static int simplifier_depth(lua_State * L) { lua_pushinteger(L, to_simplifier(L, 1)->get_depth()); return 1; } -static int simplifier_environment(lua_State * L) { return push_environment(L, to_simplifier(L, 1)->get_environment()); } -static int simplifier_options(lua_State * L) { return push_options(L, to_simplifier(L, 1)->get_options()); } -static int ro_simplifier_depth(lua_State * L) { lua_pushinteger(L, to_ro_simplifier(L, 1)->get_depth()); return 1; } -static int ro_simplifier_environment(lua_State * L) { return push_environment(L, to_ro_simplifier(L, 1)->get_environment()); } -static int ro_simplifier_options(lua_State * L) { return push_options(L, to_ro_simplifier(L, 1)->get_options()); } - -static const struct luaL_Reg simplifier_m[] = { - {"__gc", simplifier_gc}, - {"__call", safe_function}, - {"clear", safe_function}, - {"depth", safe_function}, - {"get_environment", safe_function}, - {"get_options", safe_function}, - {0, 0} -}; - -static const struct luaL_Reg ro_simplifier_m[] = { - {"__gc", ro_simplifier_gc}, - {"depth", safe_function}, - {"get_environment", safe_function}, - {"get_options", safe_function}, - {0, 0} -}; - -static int simplify_core(lua_State * L, ro_shared_environment const & env) { - int nargs = lua_gettop(L); - expr const & e = to_expr(L, 1); - buffer rules; - get_rewrite_rule_set(L, 2, env, rules); - options opts; - if (nargs >= 3) - opts = to_options(L, 3); - optional menv; - if (nargs >= 5) - menv = some_ro_menv(to_metavar_env(L, 5)); - auto r = simplify(e, env, opts, rules.size(), rules.data(), menv, get_simplifier_monitor(L, 6)); - push_expr(L, r.get_expr()); - push_optional_expr(L, r.get_proof()); - lua_pushboolean(L, r.is_heq_proof()); - return 3; -} - -static int simplify(lua_State * L) { - int nargs = lua_gettop(L); - if (nargs <= 4) - return simplify_core(L, ro_shared_environment(L)); - else - return simplify_core(L, ro_shared_environment(L, 4)); -} - -static char g_set_simplifier_monitor_key; - -void set_global_simplifier_monitor(lua_State * L, std::shared_ptr const & monitor) { - lua_pushlightuserdata(L, static_cast(&g_set_simplifier_monitor_key)); - push_simplifier_monitor_ptr(L, monitor); - lua_settable(L, LUA_REGISTRYINDEX); -} - -std::shared_ptr get_global_simplifier_monitor(lua_State * L) { - lua_pushlightuserdata(L, static_cast(&g_set_simplifier_monitor_key)); - lua_gettable(L, LUA_REGISTRYINDEX); - if (lua_isnil(L, -1)) { - lua_pop(L, 1); - return std::shared_ptr(); - } else { - std::shared_ptr r(to_simplifier_monitor_ptr(L, -1)); - lua_pop(L, 1); - return r; - } -} - -std::shared_ptr get_simplifier_monitor(lua_State * L, int i) { - if (i > lua_gettop(L) || lua_isnil(L, i)) - return get_global_simplifier_monitor(L); - else - return to_simplifier_monitor_ptr(L, 3); -} - -static int set_simplifier_monitor(lua_State * L) { - set_global_simplifier_monitor(L, to_simplifier_monitor_ptr(L, 1)); - return 0; -} - -static int get_simplifier_monitor(lua_State * L) { - auto r = get_global_simplifier_monitor(L); - if (r) - push_simplifier_monitor_ptr(L, r); - else - lua_pushnil(L); - return 1; -} - -void open_simplifier(lua_State * L) { - luaL_newmetatable(L, simplifier_mt); - lua_pushvalue(L, -1); - lua_setfield(L, -2, "__index"); - setfuncs(L, simplifier_m, 0); - SET_GLOBAL_FUN(simplifier_pred, "is_simplifier"); - - SET_GLOBAL_FUN(mk_simplifier, "simplifier"); - - luaL_newmetatable(L, ro_simplifier_mt); - lua_pushvalue(L, -1); - lua_setfield(L, -2, "__index"); - setfuncs(L, ro_simplifier_m, 0); - SET_GLOBAL_FUN(ro_simplifier_pred, "is_ro_simplifier"); - - luaL_newmetatable(L, simplifier_monitor_ptr_mt); - lua_pushvalue(L, -1); - lua_setfield(L, -2, "__index"); - setfuncs(L, simplifier_monitor_ptr_m, 0); - SET_GLOBAL_FUN(simplifier_monitor_ptr_pred, "is_simplifier_monitor"); - - SET_GLOBAL_FUN(mk_simplifier_monitor, "simplifier_monitor"); - - lua_newtable(L); - SET_ENUM("Unsupported", simplifier_monitor::failure_kind::Unsupported); - SET_ENUM("TypeMismatch", simplifier_monitor::failure_kind::TypeMismatch); - SET_ENUM("AssumptionNotProved", simplifier_monitor::failure_kind::AssumptionNotProved); - SET_ENUM("MissingArgument", simplifier_monitor::failure_kind::MissingArgument); - SET_ENUM("LoopPrevention", simplifier_monitor::failure_kind::LoopPrevention); - SET_ENUM("AbstractionBody", simplifier_monitor::failure_kind::AbstractionBody); - lua_setglobal(L, "simplifier_failure"); - - SET_GLOBAL_FUN(simplify, "simplify"); - SET_GLOBAL_FUN(set_simplifier_monitor, "set_simplifier_monitor"); - SET_GLOBAL_FUN(get_simplifier_monitor, "get_simplifier_monitor"); -} -} diff --git a/src/library/simplifier/simplifier.h b/src/library/simplifier/simplifier.h deleted file mode 100644 index 96455d6d0c..0000000000 --- a/src/library/simplifier/simplifier.h +++ /dev/null @@ -1,165 +0,0 @@ -/* -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include -#include "util/lua.h" -#include "kernel/environment.h" -#include "kernel/metavar.h" -#include "library/expr_pair.h" -#include "library/simplifier/rewrite_rule_set.h" - -namespace lean { -class simplifier_monitor; - -/** \brief Simplifier object cell. */ -class simplifier_cell { - friend class simplifier; - class imp; - std::unique_ptr m_ptr; -public: - /** - \brief Simplification result - */ - class result { - friend class imp; - expr m_expr; // new expression - optional m_proof; // a proof that the m_expr is equal to the input (when m_proofs_enabled) - bool m_heq_proof; // true if the proof has type lhs == rhs (i.e., it is a heterogeneous equality) - explicit result(expr const & out, bool heq_proof = false):m_expr(out), m_heq_proof(heq_proof) {} - result(expr const & out, expr const & pr, bool heq_proof = false):m_expr(out), m_proof(pr), m_heq_proof(heq_proof) {} - result(expr const & out, optional const & pr, bool heq_proof = false): - m_expr(out), m_proof(pr), m_heq_proof(heq_proof) {} - result update_expr(expr const & new_e) const { return result(new_e, m_proof, m_heq_proof); } - result update_proof(expr const & new_pr) const { return result(m_expr, new_pr, m_heq_proof); } - public: - result() {} - expr get_expr() const { return m_expr; } - optional get_proof() const { return m_proof; } - bool is_heq_proof() const { return m_heq_proof; } - }; - - simplifier_cell(ro_environment const & env, options const & o, unsigned num_rs, rewrite_rule_set const * rs, - std::shared_ptr const & monitor); - result operator()(expr const & e, optional const & menv); - void clear(); - - unsigned get_depth() const; - ro_environment const & get_environment() const; - options const & get_options() const; -}; - -/** \brief Reference to simplifier object */ -class simplifier { - friend class ro_simplifier; - std::shared_ptr m_ptr; -public: - typedef simplifier_cell::result result; - simplifier(ro_environment const & env, options const & o, unsigned num_rs, rewrite_rule_set const * rs, - std::shared_ptr const & monitor); - simplifier_cell * operator->() const { return m_ptr.get(); } - simplifier_cell & operator*() const { return *(m_ptr.get()); } - result operator()(expr const & e, optional const & menv) { - return (*m_ptr)(e, menv); - } -}; - -/** \brief Read only reference to simplifier object */ -class ro_simplifier { - std::shared_ptr m_ptr; -public: - typedef std::weak_ptr weak_ref; - ro_simplifier(simplifier const & s); - ro_simplifier(weak_ref const & s); - explicit operator weak_ref() const { return weak_ref(m_ptr); } - weak_ref to_weak_ref() const { return weak_ref(m_ptr); } - simplifier_cell const * operator->() const { return m_ptr.get(); } - simplifier_cell const & operator*() const { return *(m_ptr.get()); } -}; - -/** - \brief Abstract class that specifies the interface for monitoring - the behavior of the simplifier. -*/ -class simplifier_monitor { -public: - virtual ~simplifier_monitor() {} - /** - \brief This method is invoked to sign that the simplifier is starting to process the expression \c e. - */ - virtual void pre_eh(ro_simplifier const & s, expr const & e) = 0; - - /** - \brief This method is invoked to sign that \c e has be rewritten into \c new_e with proof \c pr. - The proof is none if proof generation is disabled or if \c e and \c new_e are definitionally equal. - */ - virtual void step_eh(ro_simplifier const & s, expr const & e, expr const & new_e, optional const & pr) = 0; - /** - \brief This method is invoked to sign that \c e has be rewritten into \c new_e using the conditional equation \c ceq. - */ - virtual void rewrite_eh(ro_simplifier const & s, expr const & e, expr const & new_e, expr const & ceq, name const & ceq_id) = 0; - - enum class failure_kind { Unsupported, TypeMismatch, AssumptionNotProved, MissingArgument, LoopPrevention, AbstractionBody }; - - /** - \brief This method is invoked when the simplifier fails to rewrite an application \c e. - \c i is the argument where the simplifier gave up, and \c k is the reason for failure. - Two possible values are: Unsupported or TypeMismatch (may happen when simplifying terms that use dependent types). - */ - virtual void failed_app_eh(ro_simplifier const & s, expr const & e, unsigned i, failure_kind k) = 0; - - /** - \brief This method is invoked when the simplifier fails to apply a conditional equation \c ceq to \c e. - The \c ceq may have several arguments, the value \c i is the argument where the simplifier gave up, and \c k is the reason for failure. - The possible failure values are: AssumptionNotProved (failed to synthesize a proof for an assumption required by \c ceq), - MissingArgument (failed to infer one of the arguments needed by the conditional equation), PermutationGe - (the conditional equation is a permutation, and the result is not smaller in the term ordering, \c i is irrelevant in this case). - */ - virtual void failed_rewrite_eh(ro_simplifier const & s, expr const & e, expr const & ceq, name const & ceq_id, unsigned i, failure_kind k) = 0; - - /** - \brief This method is invoked when the simplifier fails to simplify an abstraction (Pi or Lambda). - The possible failure values are: Unsupported, TypeMismatch, and AbstractionBody (failed to rewrite the body of the abstraction, - this may happen when we are using dependent types). - */ - virtual void failed_abstraction_eh(ro_simplifier const & s, expr const & e, failure_kind k) = 0; -}; - -class simplifier_stack_space_exception : public stack_space_exception { -public: - simplifier_stack_space_exception(); - virtual char const * what() const noexcept; - virtual exception * clone() const; - virtual void rethrow() const; -}; - -simplifier::result simplify(expr const & e, ro_environment const & env, options const & pts, - unsigned num_rs, rewrite_rule_set const * rs, - optional const & menv = none_ro_menv(), - std::shared_ptr const & monitor = std::shared_ptr()); -simplifier::result simplify(expr const & e, ro_environment const & env, options const & opts, - unsigned num_ns, name const * ns, - optional const & menv = none_ro_menv(), - std::shared_ptr const & monitor = std::shared_ptr()); -void open_simplifier(lua_State * L); -/** - \brief Associate the given simplifier monitor with the lua_State object \c L. -*/ -void set_global_simplifier_monitor(lua_State * L, std::shared_ptr const & monitor); -/** - \brief Return the simplifier monitor associated with the given lua_State. - The result is nullptr if the lua_State object does not have a monitor associated with it. -*/ -std::shared_ptr get_global_simplifier_monitor(lua_State * L); -/** - \brief Return a simplifier object at position \c i on the Lua stack. If there is a nil stored - on this position of the stack, then return \c get_global_simplifier_monitor. - - \remark This procedure throws an exception if the object stored at position \c i not a - simplifier monitor nor nil. -*/ -std::shared_ptr get_simplifier_monitor(lua_State * L, int i); -}