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

feat(library/rewriter): implement repeat/app/lambda/pi/try rewriter

Browse source 
- refactor to use rewriter_cell
 - implement display and operator<< for debugging
This commit is contained in:
Soonho Kong 2013-10-01 00:22:58 -07:00
parent e6c76fbe76
commit 7c0b56ad0d
2 changed files with 554 additions and 42 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

479
src/library/rewriter/rewriter.cpp
View file

@ -4,18 +4,19 @@
Author: Soonho Kong
*/
#include "util/trace.h"
#include "kernel/abstract.h"
#include "kernel/builtin.h"
#include "kernel/context.h"
#include "kernel/expr.h"
#include "kernel/environment.h"
#include "kernel/expr.h"
#include "kernel/replace.h"
#include "library/basic_thms.h"
#include "library/light_checker.h"
#include "library/printer.h"
#include "library/rewriter/fo_match.h"
#include "library/rewriter/rewriter.h"
#include "library/light_checker.h"
#include "util/buffer.h"
#include "util/trace.h"
using std::cout;
using std::endl;
@ -65,6 +66,7 @@ pair<expr, expr> theorem_rewriter_cell::operator()(environment const &, context
if (!fm.match(m_pattern, v, 0, s)) {
throw rewriter_exception();
}
lean_trace("rewriter", tout << "Subst = " << s << endl;);
// apply s to rhs
auto f = [&s](expr const & e, unsigned offset) -> expr {
@ -94,12 +96,18 @@ pair<expr, expr> theorem_rewriter_cell::operator()(environment const &, context
for (int i = m_num_args -1 ; i >= 0; i--) {
auto it = s.find(i);
lean_assert(it != s.end());
proof = mk_app(proof, it->second);
proof = proof(it->second);
lean_trace("rewriter", tout << "proof: " << i << "\t" << it->second << "\t" << proof << endl;);
}
lean_trace("rewriter", tout << "Proof = " << proof << endl;);
return make_pair(new_rhs, proof);
}
std::ostream & theorem_rewriter_cell::display(std::ostream & out) const {
out << "Thm_RW("
<< m_type << ", "
<< m_body << ")";
return out;
}
// OrElse Rewriter
orelse_rewriter_cell::orelse_rewriter_cell(rewriter const & rw1, rewriter const & rw2)
@ -120,6 +128,14 @@ pair<expr, expr> orelse_rewriter_cell::operator()(environment const & env, conte
// If the execution reaches here, it means every rewriter failed.
throw rewriter_exception();
}
std::ostream & orelse_rewriter_cell::display(std::ostream & out) const {
out << "Or_RW({";
iter(m_rwlist, [&out](rewriter const & rw) {
out << rw << "; ";
});
out << "})";
return out;
}
// Then Rewriter
then_rewriter_cell::then_rewriter_cell(rewriter const & rw1, rewriter const & rw2)
@ -134,12 +150,51 @@ pair<expr, expr> then_rewriter_cell::operator()(environment const & env, context
pair<expr, expr> new_result = result;
for (rewriter const & rw : cdr(m_rwlist)) {
new_result = rw(env, ctx, result.first);
expr const & t = light_checker(env)(v, ctx);
result = make_pair(new_result.first,
Trans(t, v, result.first, new_result.first, result.second, new_result.second));
expr const & ty = light_checker(env)(v, ctx);
if (v != new_result.first) {
result = make_pair(new_result.first,
Trans(ty, v, result.first, new_result.first, result.second, new_result.second));
}
}
return result;
}
std::ostream & then_rewriter_cell::display(std::ostream & out) const {
out << "Then_RW({";
iter(m_rwlist, [&out](rewriter const & rw) {
out << rw << "; ";
});
out << "})";
return out;
}
// Try Rewriter
try_rewriter_cell::try_rewriter_cell(rewriter const & rw1, rewriter const & rw2)
:rewriter_cell(rewriter_kind::Try), m_rwlist({rw1, rw2}) { }
try_rewriter_cell::try_rewriter_cell(std::initializer_list<rewriter> const & l)
:rewriter_cell(rewriter_kind::Try), m_rwlist(l) {
lean_assert(l.size() >= 1);
}
try_rewriter_cell::~try_rewriter_cell() { }
pair<expr, expr> try_rewriter_cell::operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception) {
for (rewriter const & rw : m_rwlist) {
try {
return rw(env, ctx, v);
} catch (rewriter_exception & ) {
// Do nothing
}
}
// If the execution reaches here, it means every rewriter failed.
expr const & t = light_checker(env)(v, ctx);
return make_pair(v, Refl(t, v));
}
std::ostream & try_rewriter_cell::display(std::ostream & out) const {
out << "Try_RW({";
iter(m_rwlist, [&out](rewriter const & rw) {
out << rw << "; ";
});
out << "})";
return out;
}
// App Rewriter
app_rewriter_cell::app_rewriter_cell(rewriter const & rw)
@ -150,12 +205,147 @@ pair<expr, expr> app_rewriter_cell::operator()(environment const & env, context
throw rewriter_exception();
unsigned n = num_args(v);
for (unsigned i = 0; i < n; i++) {
auto result = m_rw(env, ctx, arg(v, i));
}
lean_assert_ge(n, 2);
expr f = arg(v, 0);
pair<expr, expr> result = m_rw(env, ctx, f);
expr new_f = result.first;
bool f_changed = (f != new_f);
// TODO(soonhok)
throw rewriter_exception();
for (unsigned i = 1; i < n; i++) {
// Information about f
new_f = result.first;
expr proof_f = result.second;
light_checker lc(env);
expr const & f_ty = lc(f, ctx);
lean_assert(is_pi(f_ty));
expr f_ty_domain = abst_domain(f_ty); // A
expr f_ty_body = mk_lambda(abst_name(f_ty), f_ty_domain, abst_body(f_ty)); // B
// Information about arg_i
expr arg_i = arg(v, i);
pair<expr, expr> new_result = m_rw(env, ctx, arg_i);
expr new_arg_i = new_result.first;
expr proof_arg_i = new_result.second;
bool arg_changed = (arg_i != new_arg_i);
if (f_changed) {
if (arg_changed) {
// Congr : Pi (A : Type u) (B : A -> Type u) (f g : Pi (x : A) B x) (a b : A) (H1 : f = g) (H2 : a = b), f a = g b
expr new_v = new_f(new_arg_i);
expr new_proof = Congr(f_ty_domain,
f_ty_body,
f,
new_f,
arg_i,
new_arg_i,
proof_f,
proof_arg_i);
result = make_pair(new_v, new_proof);
} else {
// Congr1 : Pi (A : Type u) (B : A -> Type u) (f g: Pi (x : A) B x) (a : A) (H : f = g), f a = g a
expr new_v = new_f(new_arg_i);
expr new_proof = Congr1(f_ty_domain,
f_ty_body,
f,
new_f,
arg_i,
proof_f);
result = make_pair(new_v, new_proof);
}
} else {
if (arg_changed) {
// Congr2 : Pi (A : Type u) (B : A -> Type u) (a b : A) (f : Pi (x : A) B x) (H : a = b), f a = f b
expr new_v = new_f(new_arg_i);
expr new_proof = Congr2(f_ty_domain,
f_ty_body,
arg_i,
new_arg_i,
f,
proof_arg_i);
result = make_pair(new_v, new_proof);
f_changed = true;
} else {
// Refl
expr new_v = new_f(new_arg_i);
expr new_proof = Refl(lc(new_f, ctx), new_f);
result = make_pair(new_v, new_proof);
}
}
f = f(arg_i);
}
return result;
}
std::ostream & app_rewriter_cell::display(std::ostream & out) const {
out << "App_RW(" << m_rw << ")";
return out;
}
// Lambda Type Rewriter
lambda_type_rewriter_cell::lambda_type_rewriter_cell(rewriter const & rw)
:rewriter_cell(rewriter_kind::LambdaType), m_rw(rw) { }
lambda_type_rewriter_cell::~lambda_type_rewriter_cell() { }
pair<expr, expr> lambda_type_rewriter_cell::operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception) {
if (!is_lambda(v))
throw rewriter_exception();
expr const & ty = abst_domain(v);
pair<expr, expr> result = m_rw(env, ctx, ty);
expr const & new_ty = result.first;
light_checker lc(env);
expr const & ty_of_v = lc(v, ctx);
if (ty != new_ty) {
expr const & new_v = mk_lambda(abst_name(v), new_ty, abst_body(v));
expr const & ty_of_ty = lc(ty, ctx);
expr proof = Subst(ty_of_ty, ty, new_ty,
Fun({Const("x"), ty_of_ty},
Eq(mk_lambda(abst_name(v), ty, abst_body(v)),
mk_lambda(abst_name(v), Const("x"), abst_body(v)))),
Refl(ty_of_v, v),
result.second);
return make_pair(new_v, proof);
} else {
return make_pair(v, Refl(ty_of_v, v));
}
}
std::ostream & lambda_type_rewriter_cell::display(std::ostream & out) const {
out << "Lambda_Type_RW(" << m_rw << ")";
return out;
}
// Lambda Body Rewriter
lambda_body_rewriter_cell::lambda_body_rewriter_cell(rewriter const & rw)
:rewriter_cell(rewriter_kind::LambdaBody), m_rw(rw) { }
lambda_body_rewriter_cell::~lambda_body_rewriter_cell() { }
pair<expr, expr> lambda_body_rewriter_cell::operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception) {
if (!is_lambda(v))
throw rewriter_exception();
expr const & body = abst_body(v);
name const & n = abst_name(v);
expr const & ty = abst_domain(v);
context new_ctx = extend(ctx, n, ty);
pair<expr, expr> result = m_rw(env, new_ctx, body);
light_checker lc(env);
expr const & ty_of_v = lc(v, ctx);
expr const & new_body = result.first;
if (body != new_body) {
expr const & new_v = mk_lambda(n, ty, new_body);
expr const & ty_of_body = lc(body, new_ctx);
expr proof = Subst(ty_of_body, body, new_body,
Fun({Const("x"), ty_of_body},
Eq(mk_lambda(abst_name(v), ty, abst_body(v)),
mk_lambda(abst_name(v), ty, Const("x")))),
Refl(ty_of_v, v),
result.second);
return make_pair(new_v, proof);
} else {
return make_pair(v, Refl(ty_of_v, v));
}
}
std::ostream & lambda_body_rewriter_cell::display(std::ostream & out) const {
out << "Lambda_Body_RW(" << m_rw << ")";
return out;
}
// Lambda Rewriter
@ -166,14 +356,80 @@ lambda_rewriter_cell::~lambda_rewriter_cell() { }
pair<expr, expr> lambda_rewriter_cell::operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception) {
if (!is_lambda(v))
throw rewriter_exception();
expr const & domain = abst_domain(v);
expr const & body = abst_body(v);
rewriter rw = mk_then_rewriter(mk_lambda_type_rewriter(m_rw),
mk_lambda_body_rewriter(m_rw));
return rw(env, ctx, v);
}
std::ostream & lambda_rewriter_cell::display(std::ostream & out) const {
out << "Lambda_RW(" << m_rw << ")";
return out;
}
auto result_domain = m_rw(env, ctx, domain);
auto result_body = m_rw(env, ctx, body); // TODO(soonhok): add to context!
// Pi Type Rewriter
pi_type_rewriter_cell::pi_type_rewriter_cell(rewriter const & rw)
:rewriter_cell(rewriter_kind::PiType), m_rw(rw) { }
pi_type_rewriter_cell::~pi_type_rewriter_cell() { }
// TODO(soonhok)
throw rewriter_exception();
pair<expr, expr> pi_type_rewriter_cell::operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception) {
if (!is_pi(v))
throw rewriter_exception();
expr const & ty = abst_domain(v);
pair<expr, expr> result = m_rw(env, ctx, ty);
expr const & new_ty = result.first;
light_checker lc(env);
expr const & ty_of_v = lc(v, ctx);
if (ty != new_ty) {
expr const & new_v = mk_pi(abst_name(v), new_ty, abst_body(v));
expr const & ty_of_ty = lc(ty, ctx);
expr proof = Subst(ty_of_ty, ty, new_ty,
Fun({Const("x"), ty_of_ty},
Eq(mk_pi(abst_name(v), ty, abst_body(v)),
mk_pi(abst_name(v), Const("x"), abst_body(v)))),
Refl(ty_of_v, v),
result.second);
return make_pair(new_v, proof);
} else {
return make_pair(v, Refl(ty_of_v, v));
}
}
std::ostream & pi_type_rewriter_cell::display(std::ostream & out) const {
out << "Pi_Type_RW(" << m_rw << ")";
return out;
}
// Pi Body Rewriter
pi_body_rewriter_cell::pi_body_rewriter_cell(rewriter const & rw)
:rewriter_cell(rewriter_kind::PiBody), m_rw(rw) { }
pi_body_rewriter_cell::~pi_body_rewriter_cell() { }
pair<expr, expr> pi_body_rewriter_cell::operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception) {
if (!is_pi(v))
throw rewriter_exception();
expr const & body = abst_body(v);
name const & n = abst_name(v);
expr const & ty = abst_domain(v);
context new_ctx = extend(ctx, n, ty);
pair<expr, expr> result = m_rw(env, new_ctx, body);
light_checker lc(env);
expr const & ty_of_v = lc(v, ctx);
expr const & new_body = result.first;
if (body != new_body) {
expr const & new_v = mk_pi(n, ty, new_body);
expr const & ty_of_body = lc(body, new_ctx);
expr proof = Subst(ty_of_body, body, new_body,
Fun({Const("x"), ty_of_body},
Eq(mk_pi(abst_name(v), ty, abst_body(v)),
mk_pi(abst_name(v), ty, Const("x")))),
Refl(ty_of_v, v),
result.second);
return make_pair(new_v, proof);
} else {
return make_pair(v, Refl(ty_of_v, v));
}
}
std::ostream & pi_body_rewriter_cell::display(std::ostream & out) const {
out << "Pi_Body_RW(" << m_rw << ")";
return out;
}
// Pi Rewriter
@ -183,15 +439,111 @@ pi_rewriter_cell::~pi_rewriter_cell() { }
pair<expr, expr> pi_rewriter_cell::operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception) {
if (!is_pi(v))
throw rewriter_exception();
rewriter rw = mk_then_rewriter(mk_pi_type_rewriter(m_rw),
mk_pi_body_rewriter(m_rw));
return rw(env, ctx, v);
}
std::ostream & pi_rewriter_cell::display(std::ostream & out) const {
out << "Pi_RW(" << m_rw << ")";
return out;
}
expr const & domain = abst_domain(v);
expr const & body = abst_body(v);
// Let Type rewriter
let_type_rewriter_cell::let_type_rewriter_cell(rewriter const & rw)
:rewriter_cell(rewriter_kind::LetType), m_rw(rw) { }
let_type_rewriter_cell::~let_type_rewriter_cell() { }
pair<expr, expr> let_type_rewriter_cell::operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception) {
if (!is_let(v))
throw rewriter_exception();
expr const & ty = let_type(v);
pair<expr, expr> result = m_rw(env, ctx, ty);
expr const & new_ty = result.first;
light_checker lc(env);
expr const & ty_of_v = lc(v, ctx);
if (ty != new_ty) {
expr const & new_v = mk_let(let_name(v), new_ty, let_value(v), let_body(v));
expr const & ty_of_ty = lc(ty, ctx);
expr proof = Subst(ty_of_ty, ty, new_ty,
Fun({Const("x"), ty_of_ty},
Eq(mk_let(let_name(v), ty, let_value(v), let_body(v)),
mk_let(let_name(v), Const("x"), let_value(v), let_body(v)))),
Refl(ty_of_v, v),
result.second);
return make_pair(new_v, proof);
} else {
return make_pair(v, Refl(ty_of_v, v));
}
}
std::ostream & let_type_rewriter_cell::display(std::ostream & out) const {
out << "Let_Type_RW(" << m_rw << ")";
return out;
}
auto result_domain = m_rw(env, ctx, domain);
auto result_body = m_rw(env, ctx, body); // TODO(soonhok): add to context!
// Let Value rewriter
let_value_rewriter_cell::let_value_rewriter_cell(rewriter const & rw)
:rewriter_cell(rewriter_kind::LetValue), m_rw(rw) { }
let_value_rewriter_cell::~let_value_rewriter_cell() { }
pair<expr, expr> let_value_rewriter_cell::operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception) {
if (!is_let(v))
throw rewriter_exception();
expr const & val = let_value(v);
pair<expr, expr> result = m_rw(env, ctx, val);
expr const & new_val = result.first;
light_checker lc(env);
expr const & ty_of_v = lc(v, ctx);
if (val != new_val) {
expr const & new_v = mk_let(let_name(v), let_type(v), new_val, let_body(v));
expr const & ty_of_val = lc(val, ctx);
expr proof = Subst(ty_of_val, val, new_val,
Fun({Const("x"), ty_of_val},
Eq(mk_let(let_name(v), let_type(v), let_value(v), let_body(v)),
mk_let(let_name(v), let_type(v), Const("x"), let_body(v)))),
Refl(ty_of_v, v),
result.second);
return make_pair(new_v, proof);
} else {
return make_pair(v, Refl(ty_of_v, v));
}
}
std::ostream & let_value_rewriter_cell::display(std::ostream & out) const {
out << "Let_Value_RW(" << m_rw << ")";
return out;
}
// TODO(soonhok)
throw rewriter_exception();
// Let Body rewriter
let_body_rewriter_cell::let_body_rewriter_cell(rewriter const & rw)
:rewriter_cell(rewriter_kind::LetBody), m_rw(rw) { }
let_body_rewriter_cell::~let_body_rewriter_cell() { }
pair<expr, expr> let_body_rewriter_cell::operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception) {
if (!is_let(v))
throw rewriter_exception();
expr const & body = let_body(v);
name const & n = let_name(v);
expr const & ty = let_type(v);
expr const & val = let_value(v);
context new_ctx = extend(ctx, n, ty);
pair<expr, expr> result = m_rw(env, new_ctx, body);
light_checker lc(env);
expr const & ty_of_v = lc(v, ctx);
expr const & new_body = result.first;
if (body != new_body) {
expr const & new_v = mk_let(n, ty, val, new_body);
expr const & ty_of_body = lc(body, new_ctx);
expr proof = Subst(ty_of_body, body, new_body,
Fun({Const("x"), ty_of_body},
Eq(mk_let(let_name(v), let_type(v), let_value(v), let_body(v)),
mk_let(let_name(v), let_type(v), let_value(v), Const("x")))),
Refl(ty_of_v, v),
result.second);
return make_pair(new_v, proof);
} else {
return make_pair(v, Refl(ty_of_v, v));
}
}
std::ostream & let_body_rewriter_cell::display(std::ostream & out) const {
out << "Let_Body_RW(" << m_rw << ")";
return out;
}
// Let rewriter
@ -201,17 +553,14 @@ let_rewriter_cell::~let_rewriter_cell() { }
pair<expr, expr> let_rewriter_cell::operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception) {
if (!is_let(v))
throw rewriter_exception();
expr const & ty = let_type(v);
expr const & value = let_value(v);
expr const & body = let_body(v);
auto result_ty = m_rw(env, ctx, ty);
auto result_value = m_rw(env, ctx, value);
auto result_body = m_rw(env, ctx, body); // TODO(soonhok): add to context!
// TODO(soonhok)
throw rewriter_exception();
rewriter rw = mk_then_rewriter({mk_let_type_rewriter(m_rw),
mk_let_value_rewriter(m_rw),
mk_let_body_rewriter(m_rw)});
return rw(env, ctx, v);
}
std::ostream & let_rewriter_cell::display(std::ostream & out) const {
out << "Let_RW(" << m_rw << ")";
return out;
}
// Fail rewriter
@ -220,12 +569,21 @@ fail_rewriter_cell::~fail_rewriter_cell() { }
pair<expr, expr> fail_rewriter_cell::operator()(environment const &, context &, expr const &) const throw(rewriter_exception) {
throw rewriter_exception();
}
std::ostream & fail_rewriter_cell::display(std::ostream & out) const {
out << "Fail_RW()";
return out;
}
// Success rewriter (trivial)
success_rewriter_cell::success_rewriter_cell():rewriter_cell(rewriter_kind::Success) { }
success_rewriter_cell::~success_rewriter_cell() { }
pair<expr, expr> success_rewriter_cell::operator()(environment const &, context &, expr const & v) const throw(rewriter_exception) {
return make_pair(v, mk_app(Const("Refl"), v));
pair<expr, expr> success_rewriter_cell::operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception) {
expr const & t = light_checker(env)(v, ctx);
return make_pair(v, Refl(t, v));
}
std::ostream & success_rewriter_cell::display(std::ostream & out) const {
out << "Success_RW()";
return out;
}
// Repeat rewriter
@ -233,15 +591,24 @@ repeat_rewriter_cell::repeat_rewriter_cell(rewriter const & rw):rewriter_cell(re
repeat_rewriter_cell::~repeat_rewriter_cell() { }
pair<expr, expr> repeat_rewriter_cell::operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception) {
pair<expr, expr> result = mk_success_rewriter()(env, ctx, v);
// TODO(soonhok) fix
light_checker lc(env);
try {
while (true) {
result = m_rw(env, ctx, result.first);
pair<expr, expr> new_result = m_rw(env, ctx, result.first);
if (result.first == new_result.first)
break;
expr const & ty = lc(v, ctx);
result = make_pair(new_result.first,
Trans(ty, v, result.first, new_result.first, result.second, new_result.second));
}
}
catch (rewriter_exception & ) {
} catch (rewriter_exception &) {
return result;
}
return result;
}
std::ostream & repeat_rewriter_cell::display(std::ostream & out) const {
out << "Repeat_RW(" << m_rw << ")";
return out;
}
rewriter mk_theorem_rewriter(expr const & type, expr const & body) {
@ -253,6 +620,15 @@ rewriter mk_then_rewriter(rewriter const & rw1, rewriter const & rw2) {
rewriter mk_then_rewriter(std::initializer_list<rewriter> const & l) {
return rewriter(new then_rewriter_cell(l));
}
rewriter mk_try_rewriter(rewriter const & rw) {
return rewriter(new try_rewriter_cell({rw}));
}
rewriter mk_try_rewriter(rewriter const & rw1, rewriter const & rw2) {
return rewriter(new try_rewriter_cell(rw1, rw2));
}
rewriter mk_try_rewriter(std::initializer_list<rewriter> const & l) {
return rewriter(new try_rewriter_cell(l));
}
rewriter mk_orelse_rewriter(rewriter const & rw1, rewriter const & rw2) {
return rewriter(new orelse_rewriter_cell(rw1, rw2));
}
@ -262,12 +638,33 @@ rewriter mk_orelse_rewriter(std::initializer_list<rewriter> const & l) {
rewriter mk_app_rewriter(rewriter const & rw) {
return rewriter(new app_rewriter_cell(rw));
}
rewriter mk_lambda_type_rewriter(rewriter const & rw) {
return rewriter(new lambda_type_rewriter_cell(rw));
}
rewriter mk_lambda_body_rewriter(rewriter const & rw) {
return rewriter(new lambda_body_rewriter_cell(rw));
}
rewriter mk_lambda_rewriter(rewriter const & rw) {
return rewriter(new lambda_rewriter_cell(rw));
}
rewriter mk_pi_type_rewriter(rewriter const & rw) {
return rewriter(new pi_type_rewriter_cell(rw));
}
rewriter mk_pi_body_rewriter(rewriter const & rw) {
return rewriter(new pi_body_rewriter_cell(rw));
}
rewriter mk_pi_rewriter(rewriter const & rw) {
return rewriter(new pi_rewriter_cell(rw));
}
rewriter mk_let_type_rewriter(rewriter const & rw) {
return rewriter(new let_type_rewriter_cell(rw));
}
rewriter mk_let_value_rewriter(rewriter const & rw) {
return rewriter(new let_value_rewriter_cell(rw));
}
rewriter mk_let_body_rewriter(rewriter const & rw) {
return rewriter(new let_body_rewriter_cell(rw));
}
rewriter mk_let_rewriter(rewriter const & rw) {
return rewriter(new let_rewriter_cell(rw));
}

117
src/library/rewriter/rewriter.h
View file

@ -26,7 +26,11 @@ namespace lean {
class rewriter_exception : public exception {
};
enum class rewriter_kind {Theorem, OrElse, Then, App, Lambda, Pi, Let, Fail, Success, Repeat};
enum class rewriter_kind { Theorem, OrElse, Then, Try, App,
LambdaType, LambdaBody, Lambda,
PiType, PiBody, Pi,
LetType, LetValue, LetBody, Let,
Fail, Success, Repeat };
class rewriter;
@ -35,12 +39,14 @@ protected:
rewriter_kind m_kind;
MK_LEAN_RC();
void dealloc();
virtual std::ostream & display(std::ostream & out) const = 0;
public:
rewriter_cell(rewriter_kind k);
virtual ~rewriter_cell();
rewriter_kind kind() const { return m_kind; }
// unsigned hash() const { return m_hash; }
virtual std::pair<expr, expr> operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception) = 0;
friend std::ostream & operator<<(std::ostream & out, rewriter_cell const & rw);
};
class rewriter {
@ -62,6 +68,7 @@ public:
std::pair<expr, expr> operator()(environment const & env, context & ctx, expr const & v) const {
return (*m_ptr)(env, ctx, v);
}
friend std::ostream & operator<<(std::ostream & out, rewriter const & rw);
};
class theorem_rewriter_cell : public rewriter_cell {
@ -71,6 +78,7 @@ private:
expr m_pattern;
expr m_rhs;
unsigned m_num_args;
std::ostream & display(std::ostream & out) const;
public:
theorem_rewriter_cell(expr const & type, expr const & body);
@ -81,6 +89,7 @@ public:
class orelse_rewriter_cell : public rewriter_cell {
private:
list<rewriter> m_rwlist;
std::ostream & display(std::ostream & out) const;
public:
orelse_rewriter_cell(rewriter const & rw1, rewriter const & rw2);
orelse_rewriter_cell(std::initializer_list<rewriter> const & l);
@ -91,6 +100,7 @@ public:
class then_rewriter_cell : public rewriter_cell {
private:
list<rewriter> m_rwlist;
std::ostream & display(std::ostream & out) const;
public:
then_rewriter_cell(rewriter const & rw1, rewriter const & rw2);
then_rewriter_cell(std::initializer_list<rewriter> const & l);
@ -98,36 +108,122 @@ public:
std::pair<expr, expr> operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception);
};
class try_rewriter_cell : public rewriter_cell {
private:
list<rewriter> m_rwlist;
std::ostream & display(std::ostream & out) const;
public:
try_rewriter_cell(rewriter const & rw1, rewriter const & rw2);
try_rewriter_cell(std::initializer_list<rewriter> const & l);
~try_rewriter_cell();
std::pair<expr, expr> operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception);
};
class app_rewriter_cell : public rewriter_cell {
private:
rewriter m_rw;
std::ostream & display(std::ostream & out) const;
public:
app_rewriter_cell(rewriter const & rw);
~app_rewriter_cell();
std::pair<expr, expr> operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception);
};
class lambda_type_rewriter_cell : public rewriter_cell {
private:
rewriter m_rw;
std::ostream & display(std::ostream & out) const;
public:
lambda_type_rewriter_cell(rewriter const & rw);
~lambda_type_rewriter_cell();
std::pair<expr, expr> operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception);
};
class lambda_body_rewriter_cell : public rewriter_cell {
private:
rewriter m_rw;
std::ostream & display(std::ostream & out) const;
public:
lambda_body_rewriter_cell(rewriter const & rw);
~lambda_body_rewriter_cell();
std::pair<expr, expr> operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception);
};
class lambda_rewriter_cell : public rewriter_cell {
private:
rewriter m_rw;
std::ostream & display(std::ostream & out) const;
public:
lambda_rewriter_cell(rewriter const & rw);
~lambda_rewriter_cell();
std::pair<expr, expr> operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception);
};
class pi_type_rewriter_cell : public rewriter_cell {
private:
rewriter m_rw;
std::ostream & display(std::ostream & out) const;
public:
pi_type_rewriter_cell(rewriter const & rw);
~pi_type_rewriter_cell();
std::pair<expr, expr> operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception);
};
class pi_body_rewriter_cell : public rewriter_cell {
private:
rewriter m_rw;
std::ostream & display(std::ostream & out) const;
public:
pi_body_rewriter_cell(rewriter const & rw);
~pi_body_rewriter_cell();
std::pair<expr, expr> operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception);
};
class pi_rewriter_cell : public rewriter_cell {
private:
rewriter m_rw;
std::ostream & display(std::ostream & out) const;
public:
pi_rewriter_cell(rewriter const & rw);
~pi_rewriter_cell();
std::pair<expr, expr> operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception);
};
class let_type_rewriter_cell : public rewriter_cell {
private:
rewriter m_rw;
std::ostream & display(std::ostream & out) const;
public:
let_type_rewriter_cell(rewriter const & rw);
~let_type_rewriter_cell();
std::pair<expr, expr> operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception);
};
class let_value_rewriter_cell : public rewriter_cell {
private:
rewriter m_rw;
std::ostream & display(std::ostream & out) const;
public:
let_value_rewriter_cell(rewriter const & rw);
~let_value_rewriter_cell();
std::pair<expr, expr> operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception);
};
class let_body_rewriter_cell : public rewriter_cell {
private:
rewriter m_rw;
std::ostream & display(std::ostream & out) const;
public:
let_body_rewriter_cell(rewriter const & rw);
~let_body_rewriter_cell();
std::pair<expr, expr> operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception);
};
class let_rewriter_cell : public rewriter_cell {
private:
rewriter m_rw;
std::ostream & display(std::ostream & out) const;
public:
let_rewriter_cell(rewriter const & rw);
~let_rewriter_cell();
@ -135,6 +231,8 @@ public:
};
class fail_rewriter_cell : public rewriter_cell {
private:
std::ostream & display(std::ostream & out) const;
public:
fail_rewriter_cell();
~fail_rewriter_cell();
@ -142,6 +240,8 @@ public:
};
class success_rewriter_cell : public rewriter_cell {
private:
std::ostream & display(std::ostream & out) const;
public:
success_rewriter_cell();
~success_rewriter_cell();
@ -151,20 +251,35 @@ public:
class repeat_rewriter_cell : public rewriter_cell {
private:
rewriter m_rw;
std::ostream & display(std::ostream & out) const;
public:
repeat_rewriter_cell(rewriter const & rw);
~repeat_rewriter_cell();
std::pair<expr, expr> operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception);
};
/** \brief (For debugging) Display the content of this rewriter */
inline std::ostream & operator<<(std::ostream & out, rewriter_cell const & rc) { rc.display(out); return out; }
inline std::ostream & operator<<(std::ostream & out, rewriter const & rw) { out << *(rw.m_ptr); return out; }
rewriter mk_theorem_rewriter(expr const & type, expr const & body);
rewriter mk_then_rewriter(rewriter const & rw1, rewriter const & rw2);
rewriter mk_then_rewriter(std::initializer_list<rewriter> const & l);
rewriter mk_try_rewriter(rewriter const & rw);
rewriter mk_try_rewriter(rewriter const & rw1, rewriter const & rw2);
rewriter mk_try_rewriter(std::initializer_list<rewriter> const & l);
rewriter mk_orelse_rewriter(rewriter const & rw1, rewriter const & rw2);
rewriter mk_orelse_rewriter(std::initializer_list<rewriter> const & l);
rewriter mk_app_rewriter(rewriter const & rw);
rewriter mk_lambda_type_rewriter(rewriter const & rw);
rewriter mk_lambda_body_rewriter(rewriter const & rw);
rewriter mk_lambda_rewriter(rewriter const & rw);
rewriter mk_pi_type_rewriter(rewriter const & rw);
rewriter mk_pi_body_rewriter(rewriter const & rw);
rewriter mk_pi_rewriter(rewriter const & rw);
rewriter mk_let_type_rewriter(rewriter const & rw);
rewriter mk_let_value_rewriter(rewriter const & rw);
rewriter mk_let_body_rewriter(rewriter const & rw);
rewriter mk_let_rewriter(rewriter const & rw);
rewriter mk_fail_rewriter();
rewriter mk_success_rewriter();