From 7c0b56ad0da9816fb6cfe96d838ea4d37ee8bf5b Mon Sep 17 00:00:00 2001 From: Soonho Kong Date: Tue, 1 Oct 2013 00:22:58 -0700 Subject: [PATCH] feat(library/rewriter): implement repeat/app/lambda/pi/try rewriter - refactor to use rewriter_cell - implement display and operator<< for debugging --- src/library/rewriter/rewriter.cpp | 479 +++++++++++++++++++++++++++--- src/library/rewriter/rewriter.h | 117 +++++++- 2 files changed, 554 insertions(+), 42 deletions(-) diff --git a/src/library/rewriter/rewriter.cpp b/src/library/rewriter/rewriter.cpp index 6ef15f467e..6230b69bbf 100644 --- a/src/library/rewriter/rewriter.cpp +++ b/src/library/rewriter/rewriter.cpp @@ -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 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 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 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 then_rewriter_cell::operator()(environment const & env, context pair 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 const & l) + :rewriter_cell(rewriter_kind::Try), m_rwlist(l) { + lean_assert(l.size() >= 1); +} +try_rewriter_cell::~try_rewriter_cell() { } +pair 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 success_rewriter_cell::operator()(environment const &, context &, expr const & v) const throw(rewriter_exception) { - return make_pair(v, mk_app(Const("Refl"), v)); +pair 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 repeat_rewriter_cell::operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception) { pair 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 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 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 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 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)); } diff --git a/src/library/rewriter/rewriter.h b/src/library/rewriter/rewriter.h index ecd75aa96d..afa89c1f71 100644 --- a/src/library/rewriter/rewriter.h +++ b/src/library/rewriter/rewriter.h @@ -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 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 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 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 const & l); @@ -91,6 +100,7 @@ public: class then_rewriter_cell : public rewriter_cell { private: list 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 const & l); @@ -98,36 +108,122 @@ public: std::pair operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception); }; +class try_rewriter_cell : public rewriter_cell { +private: + list 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 const & l); + ~try_rewriter_cell(); + std::pair 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 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 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 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 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 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 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 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 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 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 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 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 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 const & l); rewriter mk_orelse_rewriter(rewriter const & rw1, rewriter const & rw2); rewriter mk_orelse_rewriter(std::initializer_list 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();