From 1d8b7dc193cb6388e2f0cb4dc6bf1d99c2408192 Mon Sep 17 00:00:00 2001 From: Soonho Kong Date: Wed, 25 Sep 2013 16:46:39 -0700 Subject: [PATCH] Update 'orelse' and 'then' rewriter to take a list of rewriters --- src/library/rewriter/rewriter.cpp | 45 ++++++++++++++++++------- src/library/rewriter/rewriter.h | 10 +++--- src/tests/library/rewriter/rewriter.cpp | 37 ++++++++++++-------- 3 files changed, 62 insertions(+), 30 deletions(-) diff --git a/src/library/rewriter/rewriter.cpp b/src/library/rewriter/rewriter.cpp index ac90ce46f..66e0f211a 100644 --- a/src/library/rewriter/rewriter.cpp +++ b/src/library/rewriter/rewriter.cpp @@ -100,27 +100,42 @@ pair theorem_rewriter_cell::operator()(environment const &, context // OrElse Rewriter orelse_rewriter_cell::orelse_rewriter_cell(rewriter const & rw1, rewriter const & rw2) - :rewriter_cell(rewriter_kind::OrElse), m_rw1(rw1), m_rw2(rw2) { } + :rewriter_cell(rewriter_kind::OrElse), m_rwlist({rw1, rw2}) { } +orelse_rewriter_cell::orelse_rewriter_cell(std::initializer_list const & l) + :rewriter_cell(rewriter_kind::OrElse), m_rwlist(l) { + lean_assert(l.size() >= 2); +} orelse_rewriter_cell::~orelse_rewriter_cell() { } pair orelse_rewriter_cell::operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception) { - try { - return m_rw1(env, ctx, v); - } catch (rewriter_exception & ) { - return m_rw2(env, ctx, v); + 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. + throw rewriter_exception(); } // Then Rewriter then_rewriter_cell::then_rewriter_cell(rewriter const & rw1, rewriter const & rw2) - :rewriter_cell(rewriter_kind::Then), m_rw1(rw1), m_rw2(rw2) { } + :rewriter_cell(rewriter_kind::Then), m_rwlist({rw1, rw2}) { } +then_rewriter_cell::then_rewriter_cell(std::initializer_list const & l) + :rewriter_cell(rewriter_kind::Then), m_rwlist(l) { + lean_assert(l.size() >= 2); +} then_rewriter_cell::~then_rewriter_cell() { } pair then_rewriter_cell::operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception) { - pair result1 = m_rw1(env, ctx, v); - pair result2 = m_rw2(env, ctx, result1.first); - light_checker lc(env); - expr const & t = lc(v, ctx); - return make_pair(result2.first, - Trans(t, v, result1.first, result2.first, result1.second, result2.second)); + pair result = car(m_rwlist)(env, ctx, v); + 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)); + } + return result; } // App Rewriter @@ -232,9 +247,15 @@ rewriter mk_theorem_rewriter(expr const & type, expr const & body) { rewriter mk_then_rewriter(rewriter const & rw1, rewriter const & rw2) { return rewriter(new then_rewriter_cell(rw1, rw2)); } +rewriter mk_then_rewriter(std::initializer_list const & l) { + return rewriter(new then_rewriter_cell(l)); +} rewriter mk_orelse_rewriter(rewriter const & rw1, rewriter const & rw2) { return rewriter(new orelse_rewriter_cell(rw1, rw2)); } +rewriter mk_orelse_rewriter(std::initializer_list const & l) { + return rewriter(new orelse_rewriter_cell(l)); +} rewriter mk_app_rewriter(rewriter const & rw) { return rewriter(new app_rewriter_cell(rw)); } diff --git a/src/library/rewriter/rewriter.h b/src/library/rewriter/rewriter.h index cc1ed21ec..ecd75aa96 100644 --- a/src/library/rewriter/rewriter.h +++ b/src/library/rewriter/rewriter.h @@ -80,20 +80,20 @@ public: class orelse_rewriter_cell : public rewriter_cell { private: - rewriter m_rw1; - rewriter m_rw2; + list m_rwlist; public: orelse_rewriter_cell(rewriter const & rw1, rewriter const & rw2); + orelse_rewriter_cell(std::initializer_list const & l); ~orelse_rewriter_cell(); std::pair operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception); }; class then_rewriter_cell : public rewriter_cell { private: - rewriter m_rw1; - rewriter m_rw2; + list m_rwlist; public: then_rewriter_cell(rewriter const & rw1, rewriter const & rw2); + then_rewriter_cell(std::initializer_list const & l); ~then_rewriter_cell(); std::pair operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception); }; @@ -159,7 +159,9 @@ public: 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_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_rewriter(rewriter const & rw); rewriter mk_pi_rewriter(rewriter const & rw); diff --git a/src/tests/library/rewriter/rewriter.cpp b/src/tests/library/rewriter/rewriter.cpp index 4ffb5bc0e..ffcbf8970 100644 --- a/src/tests/library/rewriter/rewriter.cpp +++ b/src/tests/library/rewriter/rewriter.cpp @@ -51,7 +51,7 @@ static void theorem_rewriter1_tst() { cout << " " << concl << " := " << proof << endl; lean_assert(concl == mk_eq(a_plus_b, b_plus_a)); - lean_assert(proof == mk_app(mk_app(Const("ADD_COMM"), a), b)); + lean_assert(proof == Const("ADD_COMM")(a, b)); env.add_theorem("New_theorem1", concl, proof); } @@ -82,7 +82,7 @@ static void theorem_rewriter2_tst() { cout << " " << concl << " := " << proof << endl; lean_assert(concl == mk_eq(a_plus_zero, a)); - lean_assert(proof == mk_app(Const("ADD_ID"), a)); + lean_assert(proof == Const("ADD_ID")(a)); env.add_theorem("New_theorem2", concl, proof); } @@ -125,7 +125,7 @@ static void then_rewriter1_tst() { lean_assert(concl == mk_eq(zero_plus_a, a)); lean_assert(proof == Trans(Nat, zero_plus_a, a_plus_zero, a, - mk_app(mk_app(Const("ADD_COMM"), zero), a), mk_app(Const("ADD_ID"), a))); + Const("ADD_COMM")(zero, a), Const("ADD_ID")(a))); env.add_theorem("New_theorem3", concl, proof); } @@ -171,8 +171,10 @@ static void then_rewriter2_tst() { rewriter add_assoc_thm_rewriter = mk_theorem_rewriter(add_assoc_thm_type, add_assoc_thm_body); rewriter add_comm_thm_rewriter = mk_theorem_rewriter(add_comm_thm_type, add_comm_thm_body); rewriter add_id_thm_rewriter = mk_theorem_rewriter(add_id_thm_type, add_id_thm_body); - rewriter then_rewriter2 = mk_then_rewriter(mk_then_rewriter(add_assoc_thm_rewriter, add_id_thm_rewriter), - mk_then_rewriter(add_comm_thm_rewriter, add_id_thm_rewriter)); + rewriter then_rewriter2 = mk_then_rewriter({add_assoc_thm_rewriter, + add_id_thm_rewriter, + add_comm_thm_rewriter, + add_id_thm_rewriter}); context ctx; pair result = then_rewriter2(env, ctx, zero_plus_a_plus_zero); expr concl = mk_eq(zero_plus_a_plus_zero, result.first); @@ -183,13 +185,12 @@ static void then_rewriter2_tst() { cout << " " << concl << " := " << proof << endl; lean_assert(concl == mk_eq(zero_plus_a_plus_zero, a)); - lean_assert(proof == Trans(Nat, zero_plus_a_plus_zero, zero_plus_a, a, - Trans(Nat, zero_plus_a_plus_zero, zero_plus_a_plus_zero_, zero_plus_a, - mk_app(mk_app(mk_app(Const("ADD_ASSOC"), zero), a), zero), - mk_app(Const("ADD_ID"), zero_plus_a)), - Trans(Nat, zero_plus_a, a_plus_zero, a, - mk_app(mk_app(Const("ADD_COMM"), zero), a), - mk_app(Const("ADD_ID"), a)))); + lean_assert(proof == Trans(Nat, zero_plus_a_plus_zero, a_plus_zero, a, + Trans(Nat, zero_plus_a_plus_zero, zero_plus_a, a_plus_zero, + Trans(Nat, zero_plus_a_plus_zero, zero_plus_a_plus_zero_, zero_plus_a, + Const("ADD_ASSOC")(zero, a, zero), Const("ADD_ID")(zero_plus_a)), + Const("ADD_COMM")(zero, a)), + Const("ADD_ID")(a))); env.add_theorem("New_theorem4", concl, proof); } @@ -203,6 +204,7 @@ static void orelse_rewriter1_tst() { // Result : (b + a, ADD_COMM a b) expr a = Const("a"); // a : Nat expr b = Const("b"); // b : Nat + expr zero = nVal(0); // zero : Nat expr a_plus_b = nAdd(a, b); expr b_plus_a = nAdd(b, a); expr add_assoc_thm_type = Pi("x", Nat, @@ -215,6 +217,9 @@ static void orelse_rewriter1_tst() { Pi("y", Nat, Eq(nAdd(Const("x"), Const("y")), nAdd(Const("y"), Const("x"))))); expr add_comm_thm_body = Const("ADD_COMM"); + expr add_id_thm_type = Pi("x", Nat, + Eq(nAdd(Const("x"), zero), Const("x"))); + expr add_id_thm_body = Const("ADD_ID"); environment env = mk_toplevel(); env.add_var("a", Nat); @@ -224,7 +229,10 @@ static void orelse_rewriter1_tst() { // Rewriting rewriter add_assoc_thm_rewriter = mk_theorem_rewriter(add_assoc_thm_type, add_assoc_thm_body); rewriter add_comm_thm_rewriter = mk_theorem_rewriter(add_comm_thm_type, add_comm_thm_body); - rewriter add_assoc_or_comm_thm_rewriter = mk_orelse_rewriter(add_assoc_thm_rewriter, add_comm_thm_rewriter); + rewriter add_id_thm_rewriter = mk_theorem_rewriter(add_id_thm_type, add_id_thm_body); + rewriter add_assoc_or_comm_thm_rewriter = mk_orelse_rewriter({add_assoc_thm_rewriter, + add_comm_thm_rewriter, + add_id_thm_rewriter}); context ctx; pair result = add_assoc_or_comm_thm_rewriter(env, ctx, a_plus_b); expr concl = mk_eq(a_plus_b, result.first); @@ -232,10 +240,11 @@ static void orelse_rewriter1_tst() { cout << "Theorem: " << add_assoc_thm_type << " := " << add_assoc_thm_body << endl; cout << "Theorem: " << add_comm_thm_type << " := " << add_comm_thm_body << endl; + cout << "Theorem: " << add_id_thm_type << " := " << add_id_thm_body << endl; cout << " " << concl << " := " << proof << endl; lean_assert(concl == mk_eq(a_plus_b, b_plus_a)); - lean_assert(proof == mk_app(mk_app(Const("ADD_COMM"), a), b)); + lean_assert(proof == Const("ADD_COMM")(a, b)); env.add_theorem("New_theorem5", concl, proof); }