chore(library/simplifier): delete old simplifier
This was the simplifier used in Lean 0.1.
This commit is contained in:
Leonardo de Moura
parent
de7c850782
commit
5ff200c516
11 changed files with 0 additions and 3481 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -1,2 +0,0 @@
|
|||
add_library(simplifier ceq.cpp congr.cpp rewrite_rule_set.cpp simplifier.cpp)
|
||||
target_link_libraries(simplifier ${LEAN_LIBS})
|
||||
|
|
@ -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<ro_metavar_env> const & menv, expr e);
|
||||
|
||||
/**
|
||||
\brief Auxiliary functional object for creating "conditional equations"
|
||||
*/
|
||||
class to_ceqs_fn {
|
||||
ro_environment const & m_env;
|
||||
optional<ro_metavar_env> const & m_menv;
|
||||
unsigned m_idx;
|
||||
|
||||
static list<expr_pair> 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<expr_pair> 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<ro_metavar_env> const & menv):m_env(env), m_menv(menv), m_idx(0) {}
|
||||
|
||||
list<expr_pair> 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<expr_pair> to_ceqs(ro_environment const & env, optional<ro_metavar_env> 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<ro_metavar_env> const & menv, expr e) {
|
||||
buffer<bool> 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<expr> 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<optional<unsigned>> & 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<bool>(let_type(lhs)) != static_cast<bool>(let_type(rhs)))
|
||||
return false;
|
||||
if (static_cast<bool>(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<optional<unsigned>> 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<ro_metavar_env> const & menv, expr ceq) {
|
||||
lean_assert(is_ceq(env, menv, ceq));
|
||||
type_checker tc(env);
|
||||
buffer<expr> args;
|
||||
buffer<bool> 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<unsigned> {
|
||||
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<unsigned>();
|
||||
};
|
||||
|
||||
auto arg_idx_fn = [&](expr const & e) -> optional<unsigned> {
|
||||
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<void(expr const &, context const & ctx)> 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<ro_metavar_env> 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<ro_metavar_env> 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");
|
||||
}
|
||||
}
|
||||
|
|
@ -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<expr_pair> to_ceqs(ro_environment const & env, optional<ro_metavar_env> 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
|
||||
<code>
|
||||
ceq := (forall x : A, ceq)
|
||||
| lhs = rhs
|
||||
| lhs == rhs
|
||||
</code>
|
||||
|
||||
Moreover, for <tt>(forall x : A, ceq)</tt>, 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<ro_metavar_env> 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<ro_metavar_env> const & menv, expr ceq);
|
||||
|
||||
void open_ceq(lua_State * L);
|
||||
}
|
||||
|
|
@ -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 <utility>
|
||||
#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<app_arg_info> 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<app_arg_info>::iterator find_arg_info(buffer<app_arg_info> & 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<unsigned, bool> find_hypothesis(buffer<app_arg_info> & 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<app_arg_info> 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<unsigned, bool> 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<bool> 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;
|
||||
}
|
||||
}
|
||||
|
|
@ -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 <vector>
|
||||
#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<context> 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<unsigned> 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<unsigned> 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<context> const & get_context() const { return m_context; }
|
||||
unsigned get_pos_at_proof() const { return m_proof_arg_pos; }
|
||||
optional<unsigned> const & get_new_pos_at_proof() const { return m_proof_new_arg_pos; }
|
||||
optional<unsigned> const & get_proof_pos_at_proof() const { return m_proof_proof_pos; }
|
||||
bool should_simplify() const { return static_cast<bool>(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<app_arg_info> 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<app_arg_info> 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);
|
||||
}
|
||||
|
|
@ -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);
|
||||
}
|
||||
}
|
||||
|
|
@ -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<ro_metavar_env> 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<rewrite_rule_set> m_rule_sets;
|
||||
|
||||
rewrite_rule_set_extension const * get_parent() const {
|
||||
return environment_extension::get_parent<rewrite_rule_set_extension>();
|
||||
}
|
||||
|
||||
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<environment_extension>(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<rewrite_rule_set_extension>(g_rewrite_rule_set_extension_initializer.m_extid);
|
||||
}
|
||||
|
||||
static rewrite_rule_set_extension & to_ext(environment const & env) {
|
||||
return env->get_extension<rewrite_rule_set_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");
|
||||
}
|
||||
}
|
||||
|
|
@ -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 <memory>
|
||||
#include <functional>
|
||||
#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, name_quick_cmp> name_set;
|
||||
ro_environment::weak_ref m_env;
|
||||
list<rewrite_rule> m_rule_set; // TODO(Leo): use better data-structure, e.g., discrimination trees
|
||||
name_set m_disabled_rules;
|
||||
list<congr_theorem_info> 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<ro_metavar_env> 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<bool(rewrite_rule const &)> match_fn; // NOLINT
|
||||
typedef std::function<void(rewrite_rule const &, bool)> visit_fn;
|
||||
|
||||
/**
|
||||
\brief Execute <tt>fn(rule)</tt> 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 <tt>fn(rule, enabled)</tt> for each rule in this rule set. */
|
||||
void for_each(visit_fn const & fn) const;
|
||||
|
||||
typedef std::function<void(congr_theorem_info const &)> visit_congr_fn; // NOLINT
|
||||
|
||||
/** \brief Execute <tt>fn(congr_th)</tt> 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);
|
||||
}
|
||||
File diff suppressed because it is too large
Load diff
|
|
@ -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 <memory>
|
||||
#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<imp> m_ptr;
|
||||
public:
|
||||
/**
|
||||
\brief Simplification result
|
||||
*/
|
||||
class result {
|
||||
friend class imp;
|
||||
expr m_expr; // new expression
|
||||
optional<expr> 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<expr> 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<expr> 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<simplifier_monitor> const & monitor);
|
||||
result operator()(expr const & e, optional<ro_metavar_env> 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<simplifier_cell> 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<simplifier_monitor> const & monitor);
|
||||
simplifier_cell * operator->() const { return m_ptr.get(); }
|
||||
simplifier_cell & operator*() const { return *(m_ptr.get()); }
|
||||
result operator()(expr const & e, optional<ro_metavar_env> const & menv) {
|
||||
return (*m_ptr)(e, menv);
|
||||
}
|
||||
};
|
||||
|
||||
/** \brief Read only reference to simplifier object */
|
||||
class ro_simplifier {
|
||||
std::shared_ptr<simplifier_cell const> m_ptr;
|
||||
public:
|
||||
typedef std::weak_ptr<simplifier_cell const> 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<expr> 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<ro_metavar_env> const & menv = none_ro_menv(),
|
||||
std::shared_ptr<simplifier_monitor> const & monitor = std::shared_ptr<simplifier_monitor>());
|
||||
simplifier::result simplify(expr const & e, ro_environment const & env, options const & opts,
|
||||
unsigned num_ns, name const * ns,
|
||||
optional<ro_metavar_env> const & menv = none_ro_menv(),
|
||||
std::shared_ptr<simplifier_monitor> const & monitor = std::shared_ptr<simplifier_monitor>());
|
||||
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<simplifier_monitor> 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<simplifier_monitor> 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<simplifier_monitor> get_simplifier_monitor(lua_State * L, int i);
|
||||
}
|
||||
Loading…
Reference in a new issue