style(library/blast/simplifier): whitespace
This commit is contained in:
Daniel Selsam
Leonardo de Moura
parent
bacb9f99aa
commit
f3caeb77cd
6 changed files with 133 additions and 149 deletions
|
|
@ -1320,9 +1320,9 @@ static environment simplify_cmd(parser & p) {
|
|||
expr e; level_param_names ls;
|
||||
std::tie(e, ls) = parse_local_expr(p);
|
||||
|
||||
blast::scope_debug scope(p.env(),p.ios());
|
||||
blast::scope_debug scope(p.env(), p.ios());
|
||||
blast::branch b;
|
||||
blast::simp::result r = blast::simplify(b,rel,e);
|
||||
blast::simp::result r = blast::simplify(b, rel, e);
|
||||
|
||||
flycheck_information info(p.regular_stream());
|
||||
if (info.enabled()) {
|
||||
|
|
@ -1332,8 +1332,7 @@ static environment simplify_cmd(parser & p) {
|
|||
|
||||
if (r.is_none()) {
|
||||
p.regular_stream() << "<refl>" << endl;
|
||||
}
|
||||
else {
|
||||
} else {
|
||||
auto tc = mk_type_checker(p.env(), p.mk_ngen());
|
||||
|
||||
expr pf_type = tc->check(r.get_proof(), ls).first;
|
||||
|
|
|
|||
|
|
@ -22,7 +22,6 @@ Author: Daniel Selsam
|
|||
#include "util/sexpr/option_declarations.h"
|
||||
#include <array>
|
||||
#include <map>
|
||||
#include <iostream> // TODO just for occasional debugging
|
||||
|
||||
#ifndef LEAN_DEFAULT_SIMPLIFY_MAX_STEPS
|
||||
#define LEAN_DEFAULT_SIMPLIFY_MAX_STEPS 100
|
||||
|
|
@ -114,7 +113,7 @@ class simplifier {
|
|||
|
||||
/* Cache */
|
||||
typedef expr_bi_struct_map<result> simplify_cache;
|
||||
typedef std::map<name,simplify_cache,name_quick_cmp> simplify_caches;
|
||||
typedef std::map<name, simplify_cache, name_quick_cmp> simplify_caches;
|
||||
simplify_caches m_simplify_caches;
|
||||
|
||||
optional<result> cache_lookup(expr const & e);
|
||||
|
|
@ -132,10 +131,10 @@ class simplifier {
|
|||
simp_rule_sets add_to_srss(simp_rule_sets const & _srss, buffer<expr> & ls) {
|
||||
simp_rule_sets srss = _srss;
|
||||
for (unsigned i = 0; i < ls.size(); i++) {
|
||||
// TODO assert no metas?
|
||||
// TODO(dhs): assert no metas
|
||||
expr & l = ls[i];
|
||||
tmp_type_context tctx(env(),ios());
|
||||
srss = add(tctx,srss,mlocal_name(l),tctx.infer(l),l);
|
||||
tmp_type_context tctx(env(), ios());
|
||||
srss = add(tctx, srss, mlocal_name(l), tctx.infer(l), l);
|
||||
}
|
||||
return srss;
|
||||
}
|
||||
|
|
@ -170,7 +169,6 @@ class simplifier {
|
|||
public:
|
||||
simplifier(branch const & b, name const & rel);
|
||||
result operator()(expr const & e) { return simplify(e); }
|
||||
|
||||
};
|
||||
|
||||
/* Constructor */
|
||||
|
|
@ -188,7 +186,7 @@ optional<result> simplifier::cache_lookup(expr const & e) {
|
|||
}
|
||||
void simplifier::cache_save(expr const & e, result const & r) {
|
||||
simplify_cache & cache = m_simplify_caches[m_rel];
|
||||
cache.insert(mk_pair(e,r));
|
||||
cache.insert(mk_pair(e, r));
|
||||
}
|
||||
|
||||
/* Results */
|
||||
|
|
@ -197,49 +195,47 @@ result simplifier::lift_from_eq(expr const & x, result const & r) {
|
|||
lean_assert(!r.is_none());
|
||||
|
||||
expr l = m_tmp_tctx->mk_tmp_local(m_tmp_tctx->infer(x));
|
||||
auto motive_local = m_app_builder.mk_app(m_rel,x,l);
|
||||
auto motive_local = m_app_builder.mk_app(m_rel, x, l);
|
||||
lean_assert(motive_local);
|
||||
|
||||
expr motive = Fun(l,*motive_local);
|
||||
expr motive = Fun(l, *motive_local);
|
||||
|
||||
auto Rxx = m_app_builder.mk_refl(m_rel,x);
|
||||
auto Rxx = m_app_builder.mk_refl(m_rel, x);
|
||||
lean_assert(Rxx);
|
||||
|
||||
auto pf = m_app_builder.mk_eq_rec(motive,*Rxx,r.get_proof());
|
||||
return result(r.get_new(),pf);
|
||||
auto pf = m_app_builder.mk_eq_rec(motive, *Rxx, r.get_proof());
|
||||
return result(r.get_new(), pf);
|
||||
}
|
||||
|
||||
result simplifier::join(result const & r1, result const & r2) {
|
||||
/* Assumes that both results are with respect to the same relation */
|
||||
if (r1.is_none()) {
|
||||
return r2;
|
||||
}
|
||||
else if (r2.is_none()) {
|
||||
} else if (r2.is_none()) {
|
||||
return r1;
|
||||
}
|
||||
else {
|
||||
auto trans = m_app_builder.mk_trans(m_rel,r1.get_proof(),r2.get_proof());
|
||||
} else {
|
||||
auto trans = m_app_builder.mk_trans(m_rel, r1.get_proof(), r2.get_proof());
|
||||
lean_assert(trans);
|
||||
return result(r2.get_new(),*trans);
|
||||
return result(r2.get_new(), *trans);
|
||||
}
|
||||
}
|
||||
|
||||
result simplifier::funext(result const & r, expr const & l) {
|
||||
// theorem funext {f₁ f₂ : Πx : A, B x} : (∀x, f₁ x = f₂ x) → f₁ = f₂ :=
|
||||
lean_assert(!r.is_none());
|
||||
expr e = Fun(l,r.get_new());
|
||||
if (auto pf = m_app_builder.mk_app(get_funext_name(),Fun(l,r.get_proof())))
|
||||
return result(e,*pf);
|
||||
expr e = Fun(l, r.get_new());
|
||||
if (auto pf = m_app_builder.mk_app(get_funext_name(), Fun(l, r.get_proof())))
|
||||
return result(e, *pf);
|
||||
else
|
||||
throw blast_exception("failed on [funext] matching",e);
|
||||
throw blast_exception("failed on [funext] matching", e);
|
||||
}
|
||||
|
||||
result simplifier::finalize(result const & r) {
|
||||
if (!r.is_none()) return r;
|
||||
if (auto pf = m_app_builder.mk_refl(m_rel,r.get_new()))
|
||||
return result(r.get_new(),*pf);
|
||||
if (auto pf = m_app_builder.mk_refl(m_rel, r.get_new()))
|
||||
return result(r.get_new(), *pf);
|
||||
else
|
||||
throw blast_exception("failed on [refl] matching",r.get_new());
|
||||
throw blast_exception("failed on [refl] matching", r.get_new());
|
||||
}
|
||||
|
||||
/* Simplification */
|
||||
|
|
@ -276,33 +272,33 @@ result simplifier::simplify(expr const & e) {
|
|||
lean_unreachable();
|
||||
case expr_kind::Macro:
|
||||
if (m_expand_macros) {
|
||||
if (auto m = m_tmp_tctx->expand_macro(e)) r = join(r,simplify(whnf(*m)));
|
||||
if (auto m = m_tmp_tctx->expand_macro(e)) r = join(r, simplify(whnf(*m)));
|
||||
}
|
||||
break;
|
||||
case expr_kind::Lambda:
|
||||
if (using_eq()) r = join(r,simplify_lambda(r.get_new()));
|
||||
if (using_eq()) r = join(r, simplify_lambda(r.get_new()));
|
||||
break;
|
||||
case expr_kind::Pi:
|
||||
r = join(r,simplify_pi(r.get_new()));
|
||||
r = join(r, simplify_pi(r.get_new()));
|
||||
break;
|
||||
case expr_kind::App:
|
||||
r = join(r,simplify_app(r.get_new()));
|
||||
r = join(r, simplify_app(r.get_new()));
|
||||
break;
|
||||
}
|
||||
|
||||
if (!m_top_down) r = join(r,rewrite(whnf(r.get_new())));
|
||||
if (!m_top_down) r = join(r, rewrite(whnf(r.get_new())));
|
||||
|
||||
if (r.get_new() == e && !using_eq()) {
|
||||
{
|
||||
flet<name> use_eq(m_rel, get_eq_name());
|
||||
r = simplify(r.get_new());
|
||||
}
|
||||
if (!r.is_none()) r = lift_from_eq(e,r);
|
||||
if (!r.is_none()) r = lift_from_eq(e, r);
|
||||
}
|
||||
|
||||
if (m_exhaustive && r.get_new() != e) r = join(r,simplify(r.get_new()));
|
||||
if (m_exhaustive && r.get_new() != e) r = join(r, simplify(r.get_new()));
|
||||
|
||||
if (m_memoize) cache_save(e,r);
|
||||
if (m_memoize) cache_save(e, r);
|
||||
|
||||
return r;
|
||||
}
|
||||
|
|
@ -314,15 +310,15 @@ result simplifier::simplify_lambda(expr const & _e) {
|
|||
buffer<expr> ls;
|
||||
while (is_lambda(e)) {
|
||||
expr d = instantiate_rev(binding_domain(e), ls.size(), ls.data());
|
||||
expr l = m_tmp_tctx->mk_tmp_local(d,binding_info(e));
|
||||
expr l = m_tmp_tctx->mk_tmp_local(d, binding_info(e));
|
||||
ls.push_back(l);
|
||||
e = instantiate(binding_body(e),l);
|
||||
e = instantiate(binding_body(e), l);
|
||||
}
|
||||
|
||||
result r = simplify(e);
|
||||
if (r.is_none()) { return result(_e); }
|
||||
|
||||
for (int i = ls.size() - 1; i >= 0; --i) r = funext(r,ls[i]);
|
||||
for (int i = ls.size() - 1; i >= 0; --i) r = funext(r, ls[i]);
|
||||
|
||||
return r;
|
||||
}
|
||||
|
|
@ -338,13 +334,13 @@ result simplifier::simplify_app(expr const & e) {
|
|||
/* (1) Try user-defined congruences */
|
||||
result r = try_congrs(e);
|
||||
if (!r.is_none()) {
|
||||
if (using_eq()) return join(r,simplify_fun(r.get_new()));
|
||||
if (using_eq()) return join(r, simplify_fun(r.get_new()));
|
||||
else return r;
|
||||
}
|
||||
|
||||
/* (2) Synthesize congruence lemma */
|
||||
if (using_eq()) {
|
||||
// TODO
|
||||
// TODO(dhs): synthesize congruence lemma
|
||||
}
|
||||
|
||||
/* (3) Fall back on generic binary congruence */
|
||||
|
|
@ -356,14 +352,13 @@ result simplifier::simplify_app(expr const & e) {
|
|||
|
||||
if (is_dependent_fn(f)) {
|
||||
if (r_f.is_none()) return e;
|
||||
else return congr_fun(r_f,arg);
|
||||
}
|
||||
else {
|
||||
else return congr_fun(r_f, arg);
|
||||
} else {
|
||||
result r_arg = simplify(arg);
|
||||
if (r_f.is_none() && r_arg.is_none()) return e;
|
||||
else if (r_f.is_none()) return congr_arg(f,r_arg);
|
||||
else if (r_arg.is_none()) return congr_fun(r_f,arg);
|
||||
else return congr(r_f,r_arg);
|
||||
else if (r_f.is_none()) return congr_arg(f, r_arg);
|
||||
else if (r_arg.is_none()) return congr_fun(r_f, arg);
|
||||
else return congr(r_f, r_arg);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -376,7 +371,7 @@ result simplifier::simplify_fun(expr const & e) {
|
|||
expr const & f = get_app_args(e, args);
|
||||
result r_f = simplify(f);
|
||||
if (r_f.is_none()) return result(e);
|
||||
else return congr_funs(simplify(f),args);
|
||||
else return congr_funs(simplify(f), args);
|
||||
}
|
||||
|
||||
/* Rewriting */
|
||||
|
|
@ -384,10 +379,10 @@ result simplifier::simplify_fun(expr const & e) {
|
|||
result simplifier::rewrite(expr const & e) {
|
||||
result r(e);
|
||||
while (true) {
|
||||
result r_ctx = rewrite(r.get_new(),m_ctx_srss);
|
||||
result r_new = rewrite(r_ctx.get_new(),get_simp_rule_sets(env()));
|
||||
result r_ctx = rewrite(r.get_new(), m_ctx_srss);
|
||||
result r_new = rewrite(r_ctx.get_new(), get_simp_rule_sets(env()));
|
||||
if (r_ctx.is_none() && r_new.is_none()) break;
|
||||
r = join(join(r,r_ctx),r_new);
|
||||
r = join(join(r, r_ctx), r_new);
|
||||
}
|
||||
return r;
|
||||
}
|
||||
|
|
@ -401,18 +396,18 @@ result simplifier::rewrite(expr const & e, simp_rule_sets const & srss) {
|
|||
list<simp_rule> const * srs = sr->find_simp(e);
|
||||
if (!srs) return r;
|
||||
|
||||
for_each(*srs,[&](simp_rule const & sr) {
|
||||
result r_new = rewrite(r.get_new(),sr);
|
||||
for_each(*srs, [&](simp_rule const & sr) {
|
||||
result r_new = rewrite(r.get_new(), sr);
|
||||
if (r_new.is_none()) return;
|
||||
r = join(r,r_new);
|
||||
r = join(r, r_new);
|
||||
});
|
||||
return r;
|
||||
}
|
||||
|
||||
result simplifier::rewrite(expr const & e, simp_rule const & sr) {
|
||||
blast_tmp_type_context tmp_tctx(sr.get_num_umeta(),sr.get_num_emeta());
|
||||
blast_tmp_type_context tmp_tctx(sr.get_num_umeta(), sr.get_num_emeta());
|
||||
|
||||
if (!tmp_tctx->is_def_eq(e,sr.get_lhs())) return result(e);
|
||||
if (!tmp_tctx->is_def_eq(e, sr.get_lhs())) return result(e);
|
||||
|
||||
if (m_trace) {
|
||||
expr new_lhs = tmp_tctx->instantiate_uvars_mvars(sr.get_lhs());
|
||||
|
|
@ -448,12 +443,12 @@ result simplifier::rewrite(expr const & e, simp_rule const & sr) {
|
|||
|
||||
expr m_type = tmp_tctx->instantiate_uvars_mvars(tmp_tctx->infer(m));
|
||||
if (tmp_tctx->is_prop(m_type)) {
|
||||
flet<name> set_name(m_rel,get_iff_name());
|
||||
flet<name> set_name(m_rel, get_iff_name());
|
||||
result r_cond = simplify(m_type);
|
||||
if (is_constant(r_cond.get_new()) && const_name(r_cond.get_new()) == get_true_name()) {
|
||||
auto pf = m_app_builder.mk_app(name("iff","elim_right"),finalize(r_cond).get_proof(),mk_constant(get_true_intro_name()));
|
||||
auto pf = m_app_builder.mk_app(name("iff", "elim_right"), finalize(r_cond).get_proof(), mk_constant(get_true_intro_name()));
|
||||
lean_assert(pf);
|
||||
bool success = tmp_tctx->is_def_eq(m,*pf);
|
||||
bool success = tmp_tctx->is_def_eq(m, *pf);
|
||||
lean_assert(success);
|
||||
continue;
|
||||
}
|
||||
|
|
@ -475,12 +470,12 @@ result simplifier::rewrite(expr const & e, simp_rule const & sr) {
|
|||
expr new_rhs = tmp_tctx->instantiate_uvars_mvars(sr.get_rhs());
|
||||
|
||||
if (sr.is_perm()) {
|
||||
if (!is_lt(new_rhs,new_lhs,false))
|
||||
if (!is_lt(new_rhs, new_lhs, false))
|
||||
return result(e);
|
||||
}
|
||||
|
||||
expr pf = tmp_tctx->instantiate_uvars_mvars(sr.get_proof());
|
||||
return result(result(new_rhs,pf));
|
||||
return result(result(new_rhs, pf));
|
||||
}
|
||||
|
||||
|
||||
|
|
@ -490,31 +485,31 @@ result simplifier::rewrite(expr const & e, simp_rule const & sr) {
|
|||
result simplifier::congr(result const & r_f, result const & r_arg) {
|
||||
lean_assert(!r_f.is_none() && !r_arg.is_none());
|
||||
// theorem congr {A B : Type} {f₁ f₂ : A → B} {a₁ a₂ : A} (H₁ : f₁ = f₂) (H₂ : a₁ = a₂) : f₁ a₁ = f₂ a₂
|
||||
expr e = mk_app(r_f.get_new(),r_arg.get_new());
|
||||
if (auto pf = m_app_builder.mk_app(get_congr_name(),r_f.get_proof(),r_arg.get_proof()))
|
||||
return result(e,*pf);
|
||||
expr e = mk_app(r_f.get_new(), r_arg.get_new());
|
||||
if (auto pf = m_app_builder.mk_app(get_congr_name(), r_f.get_proof(), r_arg.get_proof()))
|
||||
return result(e, *pf);
|
||||
else
|
||||
throw blast_exception("failed on [congr] matching",e);
|
||||
throw blast_exception("failed on [congr] matching", e);
|
||||
}
|
||||
|
||||
result simplifier::congr_fun(result const & r_f, expr const & arg) {
|
||||
lean_assert(!r_f.is_none());
|
||||
// theorem congr_fun {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) (a : A) : f a = g a
|
||||
expr e = mk_app(r_f.get_new(),arg);
|
||||
if (auto pf = m_app_builder.mk_app(get_congr_fun_name(),r_f.get_proof(),arg))
|
||||
return result(e,*pf);
|
||||
expr e = mk_app(r_f.get_new(), arg);
|
||||
if (auto pf = m_app_builder.mk_app(get_congr_fun_name(), r_f.get_proof(), arg))
|
||||
return result(e, *pf);
|
||||
else
|
||||
throw blast_exception("failed on [congr_fun] matching",e);
|
||||
throw blast_exception("failed on [congr_fun] matching", e);
|
||||
}
|
||||
|
||||
result simplifier::congr_arg(expr const & f, result const & r_arg) {
|
||||
lean_assert(!r_arg.is_none());
|
||||
// theorem congr_arg {A B : Type} {a₁ a₂ : A} (f : A → B) : a₁ = a₂ → f a₁ = f a₂
|
||||
expr e = mk_app(f,r_arg.get_new());
|
||||
if (auto pf = m_app_builder.mk_app(get_congr_arg_name(),f,r_arg.get_proof()))
|
||||
return result(e,*pf);
|
||||
expr e = mk_app(f, r_arg.get_new());
|
||||
if (auto pf = m_app_builder.mk_app(get_congr_arg_name(), f, r_arg.get_proof()))
|
||||
return result(e, *pf);
|
||||
else
|
||||
throw blast_exception("failed on [congr_arg] matching",e);
|
||||
throw blast_exception("failed on [congr_arg] matching", e);
|
||||
}
|
||||
|
||||
result simplifier::congr_funs(result const & r_f, buffer<expr> const & args) {
|
||||
|
|
@ -523,12 +518,12 @@ result simplifier::congr_funs(result const & r_f, buffer<expr> const & args) {
|
|||
expr e = r_f.get_new();
|
||||
expr pf = r_f.get_proof();
|
||||
for (unsigned i = 0; i < args.size(); ++i) {
|
||||
e = mk_app(e,args[i]);
|
||||
auto p = m_app_builder.mk_app(get_congr_fun_name(),pf,args[i]);
|
||||
e = mk_app(e, args[i]);
|
||||
auto p = m_app_builder.mk_app(get_congr_fun_name(), pf, args[i]);
|
||||
if (p) pf = *p;
|
||||
else throw blast_exception("failed on [congr_fun] matching",e);
|
||||
else throw blast_exception("failed on [congr_fun] matching", e);
|
||||
}
|
||||
return result(e,pf);
|
||||
return result(e, pf);
|
||||
}
|
||||
|
||||
result simplifier::try_congrs(expr const & e) {
|
||||
|
|
@ -539,17 +534,17 @@ result simplifier::try_congrs(expr const & e) {
|
|||
if (!crs) return result(e);
|
||||
|
||||
result r(e);
|
||||
for_each(*crs,[&](congr_rule const & cr) {
|
||||
for_each(*crs, [&](congr_rule const & cr) {
|
||||
if (!r.is_none()) return;
|
||||
r = try_congr(e,cr);
|
||||
r = try_congr(e, cr);
|
||||
});
|
||||
return r;
|
||||
}
|
||||
|
||||
result simplifier::try_congr(expr const & e, congr_rule const & cr) {
|
||||
blast_tmp_type_context tmp_tctx(cr.get_num_umeta(),cr.get_num_emeta());
|
||||
blast_tmp_type_context tmp_tctx(cr.get_num_umeta(), cr.get_num_emeta());
|
||||
|
||||
if (!tmp_tctx->is_def_eq(e,cr.get_lhs())) return result(e);
|
||||
if (!tmp_tctx->is_def_eq(e, cr.get_lhs())) return result(e);
|
||||
|
||||
if (m_trace) {
|
||||
ios().get_diagnostic_channel() << "<" << cr.get_id() << "> "
|
||||
|
|
@ -560,16 +555,16 @@ result simplifier::try_congr(expr const & e, congr_rule const & cr) {
|
|||
bool failed = false;
|
||||
bool simplified = false;
|
||||
list<expr> const & congr_hyps = cr.get_congr_hyps();
|
||||
for_each(congr_hyps,[&](expr const & m) {
|
||||
for_each(congr_hyps, [&](expr const & m) {
|
||||
if (failed) return;
|
||||
buffer<expr> ls;
|
||||
expr m_type = tmp_tctx->instantiate_uvars_mvars(tmp_tctx->infer(m));
|
||||
|
||||
while (is_pi(m_type)) {
|
||||
expr d = instantiate_rev(binding_domain(m_type), ls.size(), ls.data());
|
||||
expr l = tmp_tctx->mk_tmp_local(d,binding_info(m_type));
|
||||
expr l = tmp_tctx->mk_tmp_local(d, binding_info(m_type));
|
||||
ls.push_back(l);
|
||||
m_type = instantiate(binding_body(m_type),l);
|
||||
m_type = instantiate(binding_body(m_type), l);
|
||||
}
|
||||
|
||||
expr h_rel, h_lhs, h_rhs;
|
||||
|
|
@ -577,23 +572,22 @@ result simplifier::try_congr(expr const & e, congr_rule const & cr) {
|
|||
lean_assert(valid);
|
||||
{
|
||||
simplify_caches fresh_caches;
|
||||
flet<simplify_caches> set_simplify_caches(m_simplify_caches,fresh_caches);
|
||||
flet<name> set_name(m_rel,const_name(h_rel));
|
||||
flet<simplify_caches> set_simplify_caches(m_simplify_caches, fresh_caches);
|
||||
flet<name> set_name(m_rel, const_name(h_rel));
|
||||
|
||||
flet<simp_rule_sets> set_ctx_srss(m_ctx_srss,add_to_srss(m_ctx_srss,ls));
|
||||
flet<simp_rule_sets> set_ctx_srss(m_ctx_srss, add_to_srss(m_ctx_srss, ls));
|
||||
|
||||
h_lhs = tmp_tctx->instantiate_uvars_mvars(h_lhs);
|
||||
result r_congr_hyp = simplify(h_lhs);
|
||||
expr hyp;
|
||||
if (r_congr_hyp.is_none()) {
|
||||
hyp = finalize(r_congr_hyp).get_proof();
|
||||
}
|
||||
else {
|
||||
} else {
|
||||
hyp = r_congr_hyp.get_proof();
|
||||
simplified = true;
|
||||
}
|
||||
|
||||
if (!tmp_tctx->is_def_eq(m,Fun(ls,hyp))) failed = true;
|
||||
if (!tmp_tctx->is_def_eq(m, Fun(ls, hyp))) failed = true;
|
||||
}
|
||||
});
|
||||
|
||||
|
|
@ -617,7 +611,7 @@ result simplifier::try_congr(expr const & e, congr_rule const & cr) {
|
|||
if (tmp_tctx->is_mvar_assigned(i)) continue;
|
||||
|
||||
if (tmp_tctx->is_prop(tmp_tctx->infer(m))) {
|
||||
// TODO try to prove
|
||||
// TODO(dhs): should I try to prove?
|
||||
return result(e);
|
||||
}
|
||||
|
||||
|
|
@ -636,7 +630,7 @@ result simplifier::try_congr(expr const & e, congr_rule const & cr) {
|
|||
|
||||
expr e_s = tmp_tctx->instantiate_uvars_mvars(cr.get_rhs());
|
||||
expr pf = tmp_tctx->instantiate_uvars_mvars(cr.get_proof());
|
||||
return result(e_s,pf);
|
||||
return result(e_s, pf);
|
||||
}
|
||||
|
||||
/* Setup and teardown */
|
||||
|
|
@ -652,26 +646,18 @@ void initialize_simplifier() {
|
|||
|
||||
register_unsigned_option(*g_simplify_max_steps, LEAN_DEFAULT_SIMPLIFY_MAX_STEPS,
|
||||
"(simplify) max allowed steps in simplification");
|
||||
|
||||
register_bool_option(*g_simplify_top_down, LEAN_DEFAULT_SIMPLIFY_TOP_DOWN,
|
||||
"(simplify) use top-down rewriting instead of bottom-up");
|
||||
|
||||
register_bool_option(*g_simplify_exhaustive, LEAN_DEFAULT_SIMPLIFY_EXHAUSTIVE,
|
||||
"(simplify) rewrite exhaustively");
|
||||
|
||||
register_bool_option(*g_simplify_memoize, LEAN_DEFAULT_SIMPLIFY_MEMOIZE,
|
||||
"(simplify) memoize simplifications");
|
||||
|
||||
register_bool_option(*g_simplify_contextual, LEAN_DEFAULT_SIMPLIFY_CONTEXTUAL,
|
||||
"(simplify) use contextual simplification");
|
||||
|
||||
register_bool_option(*g_simplify_expand_macros, LEAN_DEFAULT_SIMPLIFY_EXPAND_MACROS,
|
||||
"(simplify) expand macros");
|
||||
|
||||
register_bool_option(*g_simplify_trace, LEAN_DEFAULT_SIMPLIFY_TRACE,
|
||||
"(simplify) trace");
|
||||
|
||||
|
||||
}
|
||||
|
||||
void finalize_simplifier() {
|
||||
|
|
@ -687,7 +673,7 @@ void finalize_simplifier() {
|
|||
/* Entry point */
|
||||
|
||||
result simplify(branch const & b, name const & rel, expr const & e) {
|
||||
return simplifier(b,rel)(e);
|
||||
return simplifier(b, rel)(e);
|
||||
}
|
||||
|
||||
}}
|
||||
|
|
|
|||
|
|
@ -29,7 +29,6 @@ public:
|
|||
|
||||
/* The following assumes that [e] and [m_new] are definitionally equal */
|
||||
void update(expr const & e) { m_new = e; }
|
||||
|
||||
};
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -14,6 +14,7 @@ Author: Leonardo de Moura
|
|||
#include "library/relation_manager.h"
|
||||
#include "library/simplifier/ceqv.h"
|
||||
#include "library/simplifier/simp_rule_set.h"
|
||||
#include <vector>
|
||||
|
||||
namespace lean {
|
||||
simp_rule_core::simp_rule_core(name const & id, levels const & umetas, std::vector<expr> const & emetas,
|
||||
|
|
@ -271,7 +272,7 @@ simp_rule_sets add_core(tmp_type_context & tctx, simp_rule_sets const & s,
|
|||
emetas.push_back(mvar);
|
||||
instances.push_back(binding_info(rule).is_inst_implicit());
|
||||
rule = tctx.whnf(instantiate(binding_body(rule), mvar));
|
||||
proof = mk_app(proof,mvar);
|
||||
proof = mk_app(proof, mvar);
|
||||
}
|
||||
expr rel, lhs, rhs;
|
||||
if (is_simp_relation(env, rule, rel, lhs, rhs) && is_constant(rel)) {
|
||||
|
|
@ -373,7 +374,7 @@ void add_congr_core(tmp_type_context & tctx, simp_rule_sets & s, name const & n)
|
|||
explicits.push_back(is_explicit(binding_info(rule)));
|
||||
instances.push_back(binding_info(rule).is_inst_implicit());
|
||||
rule = tctx.whnf(instantiate(binding_body(rule), mvar));
|
||||
proof = mk_app(proof,mvar);
|
||||
proof = mk_app(proof, mvar);
|
||||
}
|
||||
expr rel, lhs, rhs;
|
||||
if (!is_simp_relation(tctx.env(), rule, rel, lhs, rhs) || !is_constant(rel)) {
|
||||
|
|
@ -455,7 +456,6 @@ void add_congr_core(tmp_type_context & tctx, simp_rule_sets & s, name const & n)
|
|||
congr_hyps.push_back(mvar);
|
||||
}
|
||||
}
|
||||
|
||||
s.insert(const_name(rel), congr_rule(n, ls, emetas, instances, lhs, rhs, proof, to_list(congr_hyps)));
|
||||
}
|
||||
|
||||
|
|
@ -465,14 +465,14 @@ struct rrs_state {
|
|||
name_set m_congr_names;
|
||||
|
||||
void add_simp(environment const & env, io_state const & ios, name const & cname) {
|
||||
tmp_type_context tctx{env,ios};
|
||||
tmp_type_context tctx{env, ios};
|
||||
m_sets = add_core(tctx, m_sets, cname);
|
||||
m_simp_names.insert(cname);
|
||||
}
|
||||
|
||||
void add_congr(environment const & env, io_state const & ios, name const & n) {
|
||||
tmp_type_context tctx{env,ios};
|
||||
add_congr_core(tctx,m_sets, n);
|
||||
tmp_type_context tctx{env, ios};
|
||||
add_congr_core(tctx, m_sets, n);
|
||||
m_congr_names.insert(n);
|
||||
}
|
||||
};
|
||||
|
|
@ -530,7 +530,7 @@ simp_rule_sets get_simp_rule_sets(environment const & env, io_state const & ios,
|
|||
simp_rule_sets set;
|
||||
list<pair<bool, name>> const * cnames = rrs_ext::get_entries(env, ns);
|
||||
if (cnames) {
|
||||
tmp_type_context tctx(env,ios);
|
||||
tmp_type_context tctx(env, ios);
|
||||
for (pair<bool, name> const & p : *cnames) {
|
||||
set = add_core(tctx, set, p.second);
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in a new issue