From a50f5f92b878999cb0249e2d088ee8af50c86a1f Mon Sep 17 00:00:00 2001 From: Soonho Kong Date: Wed, 25 Sep 2013 15:38:16 -0700 Subject: [PATCH] Rename 'rewrite' to 'Rewriter', change type of rewriter::operator() --- src/CMakeLists.txt | 7 +- src/library/rewrite/CMakeLists.txt | 2 - src/library/rewrite/rewrite.cpp | 259 ------------------ src/library/rewrite/rewrite.h | 170 ------------ src/library/rewriter/CMakeLists.txt | 2 + .../{rewrite => rewriter}/fo_match.cpp | 4 +- src/library/{rewrite => rewriter}/fo_match.h | 0 src/library/rewriter/rewriter.cpp | 259 ++++++++++++++++++ src/library/rewriter/rewriter.h | 170 ++++++++++++ src/tests/library/rewrite/CMakeLists.txt | 3 - src/tests/library/rewriter/CMakeLists.txt | 3 + .../rewrite.cpp => rewriter/rewriter.cpp} | 70 ++--- 12 files changed, 474 insertions(+), 475 deletions(-) delete mode 100644 src/library/rewrite/CMakeLists.txt delete mode 100644 src/library/rewrite/rewrite.cpp delete mode 100644 src/library/rewrite/rewrite.h create mode 100644 src/library/rewriter/CMakeLists.txt rename src/library/{rewrite => rewriter}/fo_match.cpp (98%) rename src/library/{rewrite => rewriter}/fo_match.h (100%) create mode 100644 src/library/rewriter/rewriter.cpp create mode 100644 src/library/rewriter/rewriter.h delete mode 100644 src/tests/library/rewrite/CMakeLists.txt create mode 100644 src/tests/library/rewriter/CMakeLists.txt rename src/tests/library/{rewrite/rewrite.cpp => rewriter/rewriter.cpp} (79%) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 9e3683d63..fc38f8450 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -126,8 +126,8 @@ add_subdirectory(library/cast) set(LEAN_LIBS ${LEAN_LIBS} castlib) add_subdirectory(library/all) set(LEAN_LIBS ${LEAN_LIBS} alllib) -add_subdirectory(library/rewrite) -set(LEAN_LIBS ${LEAN_LIBS} rewrite) +add_subdirectory(library/rewriter) +set(LEAN_LIBS ${LEAN_LIBS} rewriter) add_subdirectory(frontends/lean) set(LEAN_LIBS ${LEAN_LIBS} lean_frontend) set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -pthread ${LEAN_EXTRA_LINKER_FLAGS}") @@ -139,7 +139,7 @@ add_subdirectory(tests/util/numerics) add_subdirectory(tests/interval) add_subdirectory(tests/kernel) add_subdirectory(tests/library) -add_subdirectory(tests/library/rewrite) +add_subdirectory(tests/library/rewriter) add_subdirectory(tests/frontends/lean) # Include style check @@ -151,4 +151,3 @@ file(GLOB_RECURSE LEAN_SOURCES add_style_check_target(style "${LEAN_SOURCES}") add_test(NAME style_check COMMAND ${LEAN_SOURCE_DIR}/cmake/Modules/cpplint.py ${LEAN_SOURCES}) - diff --git a/src/library/rewrite/CMakeLists.txt b/src/library/rewrite/CMakeLists.txt deleted file mode 100644 index 38ae4ea46..000000000 --- a/src/library/rewrite/CMakeLists.txt +++ /dev/null @@ -1,2 +0,0 @@ -add_library(rewrite rewrite.cpp fo_match.cpp) -target_link_libraries(rewrite ${LEAN_LIBS}) diff --git a/src/library/rewrite/rewrite.cpp b/src/library/rewrite/rewrite.cpp deleted file mode 100644 index 08148d3f6..000000000 --- a/src/library/rewrite/rewrite.cpp +++ /dev/null @@ -1,259 +0,0 @@ -/* - Copyright (c) 2013 Microsoft Corporation. All rights reserved. - Released under Apache 2.0 license as described in the file LICENSE. - - Author: Soonho Kong -*/ -#include "util/trace.h" -#include "kernel/abstract.h" -#include "kernel/builtin.h" -#include "kernel/context.h" -#include "kernel/environment.h" -#include "kernel/replace.h" -#include "library/basic_thms.h" -#include "library/printer.h" -#include "library/rewrite/fo_match.h" -#include "library/rewrite/rewrite.h" -#include "library/light_checker.h" - -using std::cout; -using std::endl; -using std::pair; -using std::make_pair; - -namespace lean { - -void rewrite_cell::dealloc() { - delete this; -} -rewrite_cell::rewrite_cell(rewrite_kind k):m_kind(k), m_rc(1) { } -rewrite_cell::~rewrite_cell() { -} - -// Theorem Rewrite -theorem_rewrite_cell::theorem_rewrite_cell(expr const & type, expr const & body) - : rewrite_cell(rewrite_kind::Theorem), m_type(type), m_body(body), m_num_args(0) { - lean_trace("rewrite", tout << "Type = " << m_type << endl;); - lean_trace("rewrite", tout << "Body = " << m_body << endl;); - - // We expect the theorem is in the form of - // Pi (x_1 : t_1 ... x_n : t_n), pattern = rhs - m_pattern = m_type; - while (is_pi(m_pattern)) { - m_pattern = abst_body(m_pattern); - m_num_args++; - } - if (!is_eq(m_pattern)) { - lean_trace("rewrite", tout << "Theorem " << m_type << " is not in the form of " - << "Pi (x_1 : t_1 ... x_n : t_n), pattern = rhs" << endl;); - } - m_rhs = eq_rhs(m_pattern); - m_pattern = eq_lhs(m_pattern); - - lean_trace("rewrite", tout << "Number of Arg = " << m_num_args << endl;); -} -theorem_rewrite_cell::~theorem_rewrite_cell() { } -pair theorem_rewrite_cell::operator()(context &, expr const & v, environment const & ) const throw(rewrite_exception) { - // lean_trace("rewrite", tout << "Context = " << ctx << endl;); - lean_trace("rewrite", tout << "Term = " << v << endl;); - lean_trace("rewrite", tout << "Pattern = " << m_pattern << endl;); - lean_trace("rewrite", tout << "Num Args = " << m_num_args << endl;); - - fo_match fm; - subst_map s; - if (!fm.match(m_pattern, v, 0, s)) { - throw rewrite_exception(); - } - - // apply s to rhs - auto f = [&s](expr const & e, unsigned offset) -> expr { - if (!is_var(e)) { - return e; - } - unsigned idx = var_idx(e); - if (idx < offset) { - return e; - } - - lean_trace("rewrite", tout << "Inside of apply : offset = " << offset - << ", e = " << e - << ", idx = " << var_idx(e) << endl;); - auto it = s.find(idx); - if (it != s.end()) { - lean_trace("rewrite", tout << "Inside of apply : s[" << idx << "] = " << s[idx] << endl;); - return s[idx]; - } - return e; - }; - - expr new_rhs = replace_fn(f)(m_rhs); - lean_trace("rewrite", tout << "New RHS = " << new_rhs << endl;); - - expr proof = m_body; - for (int i = m_num_args -1 ; i >= 0; i--) { - proof = mk_app(proof, s[i]); - lean_trace("rewrite", tout << "proof: " << i << "\t" << s[i] << "\t" << proof << endl;); - } - lean_trace("rewrite", tout << "Proof = " << proof << endl;); - return make_pair(new_rhs, proof); -} - -// OrElse Rewrite -orelse_rewrite_cell::orelse_rewrite_cell(rewrite const & rw1, rewrite const & rw2) - :rewrite_cell(rewrite_kind::OrElse), m_rw1(rw1), m_rw2(rw2) { } -orelse_rewrite_cell::~orelse_rewrite_cell() { } -pair orelse_rewrite_cell::operator()(context & ctx, expr const & v, environment const & env) const throw(rewrite_exception) { - try { - return m_rw1(ctx, v, env); - } catch (rewrite_exception & ) { - return m_rw2(ctx, v, env); - } -} - -// Then Rewrite -then_rewrite_cell::then_rewrite_cell(rewrite const & rw1, rewrite const & rw2) - :rewrite_cell(rewrite_kind::Then), m_rw1(rw1), m_rw2(rw2) { } -then_rewrite_cell::~then_rewrite_cell() { } -pair then_rewrite_cell::operator()(context & ctx, expr const & v, environment const & env) const throw(rewrite_exception) { - pair result1 = m_rw1(ctx, v, env); - pair result2 = m_rw2(ctx, result1.first, env); - 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)); -} - -// App Rewrite -app_rewrite_cell::app_rewrite_cell(rewrite const & rw) - :rewrite_cell(rewrite_kind::App), m_rw(rw) { } -app_rewrite_cell::~app_rewrite_cell() { } -pair app_rewrite_cell::operator()(context & ctx, expr const & v, environment const & env) const throw(rewrite_exception) { - if (!is_app(v)) - throw rewrite_exception(); - - unsigned n = num_args(v); - for (unsigned i = 0; i < n; i++) { - auto result = m_rw(ctx, arg(v, i), env); - } - - // TODO(soonhok) - throw rewrite_exception(); -} - -// Lambda Rewrite -lambda_rewrite_cell::lambda_rewrite_cell(rewrite const & rw) - :rewrite_cell(rewrite_kind::Lambda), m_rw(rw) { } -lambda_rewrite_cell::~lambda_rewrite_cell() { } - -pair lambda_rewrite_cell::operator()(context & ctx, expr const & v, environment const & env) const throw(rewrite_exception) { - if (!is_lambda(v)) - throw rewrite_exception(); - expr const & domain = abst_domain(v); - expr const & body = abst_body(v); - - auto result_domain = m_rw(ctx, domain, env); - auto result_body = m_rw(ctx, body, env); // TODO(soonhok): add to context! - - // TODO(soonhok) - throw rewrite_exception(); -} - -// Pi Rewrite -pi_rewrite_cell::pi_rewrite_cell(rewrite const & rw) - :rewrite_cell(rewrite_kind::Pi), m_rw(rw) { } -pi_rewrite_cell::~pi_rewrite_cell() { } -pair pi_rewrite_cell::operator()(context & ctx, expr const & v, environment const & env) const throw(rewrite_exception) { - if (!is_pi(v)) - throw rewrite_exception(); - - expr const & domain = abst_domain(v); - expr const & body = abst_body(v); - - auto result_domain = m_rw(ctx, domain, env); - auto result_body = m_rw(ctx, body, env); // TODO(soonhok): add to context! - - // TODO(soonhok) - throw rewrite_exception(); -} - -// Let rewrite -let_rewrite_cell::let_rewrite_cell(rewrite const & rw) - :rewrite_cell(rewrite_kind::Let), m_rw(rw) { } -let_rewrite_cell::~let_rewrite_cell() { } -pair let_rewrite_cell::operator()(context & ctx, expr const & v, environment const & env) const throw(rewrite_exception) { - if (!is_let(v)) - throw rewrite_exception(); - - expr const & ty = let_type(v); - expr const & value = let_value(v); - expr const & body = let_body(v); - - auto result_ty = m_rw(ctx, ty, env); - auto result_value = m_rw(ctx, value, env); - auto result_body = m_rw(ctx, body, env); // TODO(soonhok): add to context! - - // TODO(soonhok) - throw rewrite_exception(); -} - -// Fail rewrite -fail_rewrite_cell::fail_rewrite_cell():rewrite_cell(rewrite_kind::Fail) { } -fail_rewrite_cell::~fail_rewrite_cell() { } -pair fail_rewrite_cell::operator()(context &, expr const &, environment const &) const throw(rewrite_exception) { - throw rewrite_exception(); -} - -// Success rewrite (trivial) -success_rewrite_cell::success_rewrite_cell():rewrite_cell(rewrite_kind::Success) { } -success_rewrite_cell::~success_rewrite_cell() { } -pair success_rewrite_cell::operator()(context &, expr const & v, environment const &) const throw(rewrite_exception) { - return make_pair(v, mk_app(Const("Refl"), v)); -} - -// Repeat rewrite -repeat_rewrite_cell::repeat_rewrite_cell(rewrite const & rw):rewrite_cell(rewrite_kind::Repeat), m_rw(rw) { } -repeat_rewrite_cell::~repeat_rewrite_cell() { } -pair repeat_rewrite_cell::operator()(context & ctx, expr const & v, environment const & env) const throw(rewrite_exception) { - pair result = mk_success_rewrite()(ctx, v, env); - // TODO(soonhok) fix - try { - while (true) { - result = m_rw(ctx, result.first, env); - } - } - catch (rewrite_exception & ) { - return result; - } -} - -rewrite mk_theorem_rewrite(expr const & type, expr const & body) { - return rewrite(new theorem_rewrite_cell(type, body)); -} -rewrite mk_then_rewrite(rewrite const & rw1, rewrite const & rw2) { - return rewrite(new then_rewrite_cell(rw1, rw2)); -} -rewrite mk_orelse_rewrite(rewrite const & rw1, rewrite const & rw2) { - return rewrite(new orelse_rewrite_cell(rw1, rw2)); -} -rewrite mk_app_rewrite(rewrite const & rw) { - return rewrite(new app_rewrite_cell(rw)); -} -rewrite mk_lambda_rewrite(rewrite const & rw) { - return rewrite(new lambda_rewrite_cell(rw)); -} -rewrite mk_pi_rewrite(rewrite const & rw) { - return rewrite(new pi_rewrite_cell(rw)); -} -rewrite mk_let_rewrite(rewrite const & rw) { - return rewrite(new let_rewrite_cell(rw)); -} -rewrite mk_fail_rewrite() { - return rewrite(new fail_rewrite_cell()); -} -rewrite mk_success_rewrite() { - return rewrite(new success_rewrite_cell()); -} -rewrite mk_repeat_rewrite(rewrite const & rw) { - return rewrite(new repeat_rewrite_cell(rw)); -} -} diff --git a/src/library/rewrite/rewrite.h b/src/library/rewrite/rewrite.h deleted file mode 100644 index ac9ce0cdc..000000000 --- a/src/library/rewrite/rewrite.h +++ /dev/null @@ -1,170 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Soonho Kong -*/ -#pragma once -#include -#include -#include "util/exception.h" -#include "kernel/environment.h" - -// Term Rewriting -// APP_RW -// LAMBDA_RW -// PI_RW -// LET_RW -// DEPTH_RW -// TRIVIAL_RW -// FORALL -// FAIL -// FAIL_IF - -namespace lean { - -class rewrite_exception : public exception { -}; - -enum class rewrite_kind {Theorem, OrElse, Then, App, Lambda, Pi, Let, Fail, Success, Repeat}; - -class rewrite; - -class rewrite_cell { -protected: - rewrite_kind m_kind; - MK_LEAN_RC(); - void dealloc(); -public: - rewrite_cell(rewrite_kind k); - virtual ~rewrite_cell(); - rewrite_kind kind() const { return m_kind; } -// unsigned hash() const { return m_hash; } - virtual std::pair operator()(context & ctx, expr const & v, environment const & env) const throw(rewrite_exception) = 0; -}; - -class rewrite { -private: - rewrite_cell * m_ptr; -public: - explicit rewrite(rewrite_cell * ptr):m_ptr(ptr) {} - rewrite():m_ptr(nullptr) {} - rewrite(rewrite const & r):m_ptr(r.m_ptr) { - if (m_ptr) m_ptr->inc_ref(); - } - rewrite(rewrite && r):m_ptr(r.m_ptr) { r.m_ptr = nullptr; } - ~rewrite() { if (m_ptr) m_ptr->dec_ref(); } - void release() { if (m_ptr) m_ptr->dec_ref(); m_ptr = nullptr; } - friend void swap(rewrite & a, rewrite & b) { std::swap(a.m_ptr, b.m_ptr); } - rewrite_kind kind() const { return m_ptr->kind(); } - rewrite & operator=(rewrite const & s) { LEAN_COPY_REF(rewrite, s); } - rewrite & operator=(rewrite && s) { LEAN_MOVE_REF(rewrite, s); } - std::pair operator()(context & ctx, expr const & v, environment const & env) const { - return (*m_ptr)(ctx, v, env); - } -}; - -class theorem_rewrite_cell : public rewrite_cell { -private: - expr const & m_type; - expr const & m_body; - expr m_pattern; - expr m_rhs; - unsigned m_num_args; - -public: - theorem_rewrite_cell(expr const & type, expr const & body); - ~theorem_rewrite_cell(); - std::pair operator()(context & ctx, expr const & v, environment const & env) const throw(rewrite_exception); -}; - -class orelse_rewrite_cell : public rewrite_cell { -private: - rewrite m_rw1; - rewrite m_rw2; -public: - orelse_rewrite_cell(rewrite const & rw1, rewrite const & rw2); - ~orelse_rewrite_cell(); - std::pair operator()(context & ctx, expr const & v, environment const & env) const throw(rewrite_exception); -}; - -class then_rewrite_cell : public rewrite_cell { -private: - rewrite m_rw1; - rewrite m_rw2; -public: - then_rewrite_cell(rewrite const & rw1, rewrite const & rw2); - ~then_rewrite_cell(); - std::pair operator()(context & ctx, expr const & v, environment const & env) const throw(rewrite_exception); -}; - -class app_rewrite_cell : public rewrite_cell { -private: - rewrite m_rw; -public: - app_rewrite_cell(rewrite const & rw); - ~app_rewrite_cell(); - std::pair operator()(context & ctx, expr const & v, environment const & env) const throw(rewrite_exception); -}; - -class lambda_rewrite_cell : public rewrite_cell { -private: - rewrite m_rw; -public: - lambda_rewrite_cell(rewrite const & rw); - ~lambda_rewrite_cell(); - std::pair operator()(context & ctx, expr const & v, environment const & env) const throw(rewrite_exception); -}; - -class pi_rewrite_cell : public rewrite_cell { -private: - rewrite m_rw; -public: - pi_rewrite_cell(rewrite const & rw); - ~pi_rewrite_cell(); - std::pair operator()(context & ctx, expr const & v, environment const & env) const throw(rewrite_exception); -}; - -class let_rewrite_cell : public rewrite_cell { -private: - rewrite m_rw; -public: - let_rewrite_cell(rewrite const & rw); - ~let_rewrite_cell(); - std::pair operator()(context & ctx, expr const & v, environment const & env) const throw(rewrite_exception); -}; - -class fail_rewrite_cell : public rewrite_cell { -public: - fail_rewrite_cell(); - ~fail_rewrite_cell(); - std::pair operator()(context &, expr const &, environment const &) const throw(rewrite_exception); -}; - -class success_rewrite_cell : public rewrite_cell { -public: - success_rewrite_cell(); - ~success_rewrite_cell(); - std::pair operator()(context &, expr const &, environment const & env) const throw(rewrite_exception); -}; - -class repeat_rewrite_cell : public rewrite_cell { -private: - rewrite m_rw; -public: - repeat_rewrite_cell(rewrite const & rw); - ~repeat_rewrite_cell(); - std::pair operator()(context &, expr const &, environment const & env) const throw(rewrite_exception); -}; - -rewrite mk_theorem_rewrite(expr const & type, expr const & body); -rewrite mk_then_rewrite(rewrite const & rw1, rewrite const & rw2); -rewrite mk_orelse_rewrite(rewrite const & rw1, rewrite const & rw2); -rewrite mk_app_rewrite(rewrite const & rw); -rewrite mk_lambda_rewrite(rewrite const & rw); -rewrite mk_pi_rewrite(rewrite const & rw); -rewrite mk_let_rewrite(rewrite const & rw); -rewrite mk_fail_rewrite(); -rewrite mk_success_rewrite(); -rewrite mk_repeat_rewrite(rewrite const & rw); -} diff --git a/src/library/rewriter/CMakeLists.txt b/src/library/rewriter/CMakeLists.txt new file mode 100644 index 000000000..84fb906e1 --- /dev/null +++ b/src/library/rewriter/CMakeLists.txt @@ -0,0 +1,2 @@ +add_library(rewriter rewriter.cpp fo_match.cpp) +target_link_libraries(rewriter ${LEAN_LIBS}) diff --git a/src/library/rewrite/fo_match.cpp b/src/library/rewriter/fo_match.cpp similarity index 98% rename from src/library/rewrite/fo_match.cpp rename to src/library/rewriter/fo_match.cpp index 3c1df2e3e..ccdc556dd 100644 --- a/src/library/rewrite/fo_match.cpp +++ b/src/library/rewriter/fo_match.cpp @@ -11,8 +11,8 @@ Author: Soonho Kong #include "library/all/all.h" #include "library/arith/nat.h" #include "library/arith/arith.h" -#include "library/rewrite/fo_match.h" -#include "library/rewrite/rewrite.h" +#include "library/rewriter/fo_match.h" +#include "library/rewriter/rewriter.h" #include "library/printer.h" using std::cout; diff --git a/src/library/rewrite/fo_match.h b/src/library/rewriter/fo_match.h similarity index 100% rename from src/library/rewrite/fo_match.h rename to src/library/rewriter/fo_match.h diff --git a/src/library/rewriter/rewriter.cpp b/src/library/rewriter/rewriter.cpp new file mode 100644 index 000000000..ac90ce46f --- /dev/null +++ b/src/library/rewriter/rewriter.cpp @@ -0,0 +1,259 @@ +/* + Copyright (c) 2013 Microsoft Corporation. All rights reserved. + Released under Apache 2.0 license as described in the file LICENSE. + + Author: Soonho Kong +*/ +#include "util/trace.h" +#include "kernel/abstract.h" +#include "kernel/builtin.h" +#include "kernel/context.h" +#include "kernel/environment.h" +#include "kernel/replace.h" +#include "library/basic_thms.h" +#include "library/printer.h" +#include "library/rewriter/fo_match.h" +#include "library/rewriter/rewriter.h" +#include "library/light_checker.h" + +using std::cout; +using std::endl; +using std::pair; +using std::make_pair; + +namespace lean { + +void rewriter_cell::dealloc() { + delete this; +} +rewriter_cell::rewriter_cell(rewriter_kind k):m_kind(k), m_rc(1) { } +rewriter_cell::~rewriter_cell() { +} + +// Theorem Rewriter +theorem_rewriter_cell::theorem_rewriter_cell(expr const & type, expr const & body) + : rewriter_cell(rewriter_kind::Theorem), m_type(type), m_body(body), m_num_args(0) { + lean_trace("rewriter", tout << "Type = " << m_type << endl;); + lean_trace("rewriter", tout << "Body = " << m_body << endl;); + + // We expect the theorem is in the form of + // Pi (x_1 : t_1 ... x_n : t_n), pattern = rhs + m_pattern = m_type; + while (is_pi(m_pattern)) { + m_pattern = abst_body(m_pattern); + m_num_args++; + } + if (!is_eq(m_pattern)) { + lean_trace("rewriter", tout << "Theorem " << m_type << " is not in the form of " + << "Pi (x_1 : t_1 ... x_n : t_n), pattern = rhs" << endl;); + } + m_rhs = eq_rhs(m_pattern); + m_pattern = eq_lhs(m_pattern); + + lean_trace("rewriter", tout << "Number of Arg = " << m_num_args << endl;); +} +theorem_rewriter_cell::~theorem_rewriter_cell() { } +pair theorem_rewriter_cell::operator()(environment const &, context &, expr const & v) const throw(rewriter_exception) { + // lean_trace("rewriter", tout << "Context = " << ctx << endl;); + lean_trace("rewriter", tout << "Term = " << v << endl;); + lean_trace("rewriter", tout << "Pattern = " << m_pattern << endl;); + lean_trace("rewriter", tout << "Num Args = " << m_num_args << endl;); + + fo_match fm; + subst_map s; + if (!fm.match(m_pattern, v, 0, s)) { + throw rewriter_exception(); + } + + // apply s to rhs + auto f = [&s](expr const & e, unsigned offset) -> expr { + if (!is_var(e)) { + return e; + } + unsigned idx = var_idx(e); + if (idx < offset) { + return e; + } + + lean_trace("rewriter", tout << "Inside of apply : offset = " << offset + << ", e = " << e + << ", idx = " << var_idx(e) << endl;); + auto it = s.find(idx); + if (it != s.end()) { + lean_trace("rewriter", tout << "Inside of apply : s[" << idx << "] = " << s[idx] << endl;); + return s[idx]; + } + return e; + }; + + expr new_rhs = replace_fn(f)(m_rhs); + lean_trace("rewriter", tout << "New RHS = " << new_rhs << endl;); + + expr proof = m_body; + for (int i = m_num_args -1 ; i >= 0; i--) { + proof = mk_app(proof, s[i]); + lean_trace("rewriter", tout << "proof: " << i << "\t" << s[i] << "\t" << proof << endl;); + } + lean_trace("rewriter", tout << "Proof = " << proof << endl;); + return make_pair(new_rhs, proof); +} + +// 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) { } +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); + } +} + +// 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) { } +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)); +} + +// App Rewriter +app_rewriter_cell::app_rewriter_cell(rewriter const & rw) + :rewriter_cell(rewriter_kind::App), m_rw(rw) { } +app_rewriter_cell::~app_rewriter_cell() { } +pair app_rewriter_cell::operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception) { + if (!is_app(v)) + throw rewriter_exception(); + + unsigned n = num_args(v); + for (unsigned i = 0; i < n; i++) { + auto result = m_rw(env, ctx, arg(v, i)); + } + + // TODO(soonhok) + throw rewriter_exception(); +} + +// Lambda Rewriter +lambda_rewriter_cell::lambda_rewriter_cell(rewriter const & rw) + :rewriter_cell(rewriter_kind::Lambda), m_rw(rw) { } +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); + + auto result_domain = m_rw(env, ctx, domain); + auto result_body = m_rw(env, ctx, body); // TODO(soonhok): add to context! + + // TODO(soonhok) + throw rewriter_exception(); +} + +// Pi Rewriter +pi_rewriter_cell::pi_rewriter_cell(rewriter const & rw) + :rewriter_cell(rewriter_kind::Pi), m_rw(rw) { } +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(); + + expr const & domain = abst_domain(v); + expr const & body = abst_body(v); + + auto result_domain = m_rw(env, ctx, domain); + auto result_body = m_rw(env, ctx, body); // TODO(soonhok): add to context! + + // TODO(soonhok) + throw rewriter_exception(); +} + +// Let rewriter +let_rewriter_cell::let_rewriter_cell(rewriter const & rw) + :rewriter_cell(rewriter_kind::Let), m_rw(rw) { } +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(); +} + +// Fail rewriter +fail_rewriter_cell::fail_rewriter_cell():rewriter_cell(rewriter_kind::Fail) { } +fail_rewriter_cell::~fail_rewriter_cell() { } +pair fail_rewriter_cell::operator()(environment const &, context &, expr const &) const throw(rewriter_exception) { + throw rewriter_exception(); +} + +// 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)); +} + +// Repeat rewriter +repeat_rewriter_cell::repeat_rewriter_cell(rewriter const & rw):rewriter_cell(rewriter_kind::Repeat), m_rw(rw) { } +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 + try { + while (true) { + result = m_rw(env, ctx, result.first); + } + } + catch (rewriter_exception & ) { + return result; + } +} + +rewriter mk_theorem_rewriter(expr const & type, expr const & body) { + return rewriter(new theorem_rewriter_cell(type, body)); +} +rewriter mk_then_rewriter(rewriter const & rw1, rewriter const & rw2) { + return rewriter(new then_rewriter_cell(rw1, rw2)); +} +rewriter mk_orelse_rewriter(rewriter const & rw1, rewriter const & rw2) { + return rewriter(new orelse_rewriter_cell(rw1, rw2)); +} +rewriter mk_app_rewriter(rewriter const & rw) { + return rewriter(new app_rewriter_cell(rw)); +} +rewriter mk_lambda_rewriter(rewriter const & rw) { + return rewriter(new lambda_rewriter_cell(rw)); +} +rewriter mk_pi_rewriter(rewriter const & rw) { + return rewriter(new pi_rewriter_cell(rw)); +} +rewriter mk_let_rewriter(rewriter const & rw) { + return rewriter(new let_rewriter_cell(rw)); +} +rewriter mk_fail_rewriter() { + return rewriter(new fail_rewriter_cell()); +} +rewriter mk_success_rewriter() { + return rewriter(new success_rewriter_cell()); +} +rewriter mk_repeat_rewriter(rewriter const & rw) { + return rewriter(new repeat_rewriter_cell(rw)); +} +} diff --git a/src/library/rewriter/rewriter.h b/src/library/rewriter/rewriter.h new file mode 100644 index 000000000..cc1ed21ec --- /dev/null +++ b/src/library/rewriter/rewriter.h @@ -0,0 +1,170 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Soonho Kong +*/ +#pragma once +#include +#include +#include "util/exception.h" +#include "kernel/environment.h" + +// Term Rewriting +// APP_RW +// LAMBDA_RW +// PI_RW +// LET_RW +// DEPTH_RW +// TRIVIAL_RW +// FORALL +// FAIL +// FAIL_IF + +namespace lean { + +class rewriter_exception : public exception { +}; + +enum class rewriter_kind {Theorem, OrElse, Then, App, Lambda, Pi, Let, Fail, Success, Repeat}; + +class rewriter; + +class rewriter_cell { +protected: + rewriter_kind m_kind; + MK_LEAN_RC(); + void dealloc(); +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; +}; + +class rewriter { +private: + rewriter_cell * m_ptr; +public: + explicit rewriter(rewriter_cell * ptr):m_ptr(ptr) {} + rewriter():m_ptr(nullptr) {} + rewriter(rewriter const & r):m_ptr(r.m_ptr) { + if (m_ptr) m_ptr->inc_ref(); + } + rewriter(rewriter && r):m_ptr(r.m_ptr) { r.m_ptr = nullptr; } + ~rewriter() { if (m_ptr) m_ptr->dec_ref(); } + void release() { if (m_ptr) m_ptr->dec_ref(); m_ptr = nullptr; } + friend void swap(rewriter & a, rewriter & b) { std::swap(a.m_ptr, b.m_ptr); } + rewriter_kind kind() const { return m_ptr->kind(); } + rewriter & operator=(rewriter const & s) { LEAN_COPY_REF(rewriter, s); } + rewriter & operator=(rewriter && s) { LEAN_MOVE_REF(rewriter, s); } + std::pair operator()(environment const & env, context & ctx, expr const & v) const { + return (*m_ptr)(env, ctx, v); + } +}; + +class theorem_rewriter_cell : public rewriter_cell { +private: + expr const & m_type; + expr const & m_body; + expr m_pattern; + expr m_rhs; + unsigned m_num_args; + +public: + theorem_rewriter_cell(expr const & type, expr const & body); + ~theorem_rewriter_cell(); + std::pair operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception); +}; + +class orelse_rewriter_cell : public rewriter_cell { +private: + rewriter m_rw1; + rewriter m_rw2; +public: + orelse_rewriter_cell(rewriter const & rw1, rewriter const & rw2); + ~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; +public: + then_rewriter_cell(rewriter const & rw1, rewriter const & rw2); + ~then_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; +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_rewriter_cell : public rewriter_cell { +private: + rewriter m_rw; +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_rewriter_cell : public rewriter_cell { +private: + rewriter m_rw; +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_rewriter_cell : public rewriter_cell { +private: + rewriter m_rw; +public: + let_rewriter_cell(rewriter const & rw); + ~let_rewriter_cell(); + std::pair operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception); +}; + +class fail_rewriter_cell : public rewriter_cell { +public: + fail_rewriter_cell(); + ~fail_rewriter_cell(); + std::pair operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception); +}; + +class success_rewriter_cell : public rewriter_cell { +public: + success_rewriter_cell(); + ~success_rewriter_cell(); + std::pair operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception); +}; + +class repeat_rewriter_cell : public rewriter_cell { +private: + rewriter m_rw; +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); +}; + +rewriter mk_theorem_rewriter(expr const & type, expr const & body); +rewriter mk_then_rewriter(rewriter const & rw1, rewriter const & rw2); +rewriter mk_orelse_rewriter(rewriter const & rw1, rewriter const & rw2); +rewriter mk_app_rewriter(rewriter const & rw); +rewriter mk_lambda_rewriter(rewriter const & rw); +rewriter mk_pi_rewriter(rewriter const & rw); +rewriter mk_let_rewriter(rewriter const & rw); +rewriter mk_fail_rewriter(); +rewriter mk_success_rewriter(); +rewriter mk_repeat_rewriter(rewriter const & rw); +} diff --git a/src/tests/library/rewrite/CMakeLists.txt b/src/tests/library/rewrite/CMakeLists.txt deleted file mode 100644 index 84d2ca728..000000000 --- a/src/tests/library/rewrite/CMakeLists.txt +++ /dev/null @@ -1,3 +0,0 @@ -add_executable(rewrite_tst rewrite.cpp) -target_link_libraries(rewrite_tst ${EXTRA_LIBS}) -add_test(rewrite ${CMAKE_CURRENT_BINARY_DIR}/rewrite_tst) diff --git a/src/tests/library/rewriter/CMakeLists.txt b/src/tests/library/rewriter/CMakeLists.txt new file mode 100644 index 000000000..d77965cec --- /dev/null +++ b/src/tests/library/rewriter/CMakeLists.txt @@ -0,0 +1,3 @@ +add_executable(rewriter_tst rewriter.cpp) +target_link_libraries(rewriter_tst ${EXTRA_LIBS}) +add_test(rewriter ${CMAKE_CURRENT_BINARY_DIR}/rewriter_tst) diff --git a/src/tests/library/rewrite/rewrite.cpp b/src/tests/library/rewriter/rewriter.cpp similarity index 79% rename from src/tests/library/rewrite/rewrite.cpp rename to src/tests/library/rewriter/rewriter.cpp index 75dd3fdbb..4ffb5bc0e 100644 --- a/src/tests/library/rewrite/rewrite.cpp +++ b/src/tests/library/rewriter/rewriter.cpp @@ -11,8 +11,8 @@ Author: Soonho Kong #include "library/all/all.h" #include "library/arith/arith.h" #include "library/arith/nat.h" -#include "library/rewrite/fo_match.h" -#include "library/rewrite/rewrite.h" +#include "library/rewriter/fo_match.h" +#include "library/rewriter/rewriter.h" #include "library/basic_thms.h" #include "library/printer.h" using namespace lean; @@ -21,8 +21,8 @@ using std::cout; using std::pair; using std::endl; -static void theorem_rewrite1_tst() { - cout << "=== theorem_rewrite1_tst() ===" << endl; +static void theorem_rewriter1_tst() { + cout << "=== theorem_rewriter1_tst() ===" << endl; // Theorem: Pi(x y : N), x + y = y + x := ADD_COMM x y // Term : a + b // Result : (b + a, ADD_COMM a b) @@ -41,9 +41,9 @@ static void theorem_rewrite1_tst() { env.add_axiom("ADD_COMM", add_comm_thm_type); // ADD_COMM : Pi (x, y: N), x + y = y + z // Rewriting - rewrite add_comm_thm_rewriter = mk_theorem_rewrite(add_comm_thm_type, add_comm_thm_body); + rewriter add_comm_thm_rewriter = mk_theorem_rewriter(add_comm_thm_type, add_comm_thm_body); context ctx; - pair result = add_comm_thm_rewriter(ctx, a_plus_b, env); + pair result = add_comm_thm_rewriter(env, ctx, a_plus_b); expr concl = mk_eq(a_plus_b, result.first); expr proof = result.second; @@ -55,8 +55,8 @@ static void theorem_rewrite1_tst() { env.add_theorem("New_theorem1", concl, proof); } -static void theorem_rewrite2_tst() { - cout << "=== theorem_rewrite2_tst() ===" << endl; +static void theorem_rewriter2_tst() { + cout << "=== theorem_rewriter2_tst() ===" << endl; // Theorem: Pi(x : N), x + 0 = x := ADD_ID x // Term : a + 0 // Result : (a, ADD_ID a) @@ -72,9 +72,9 @@ static void theorem_rewrite2_tst() { env.add_axiom("ADD_ID", add_id_thm_type); // ADD_ID : Pi (x : N), x = x + 0 // Rewriting - rewrite add_id_thm_rewriter = mk_theorem_rewrite(add_id_thm_type, add_id_thm_body); + rewriter add_id_thm_rewriter = mk_theorem_rewriter(add_id_thm_type, add_id_thm_body); context ctx; - pair result = add_id_thm_rewriter(ctx, a_plus_zero, env); + pair result = add_id_thm_rewriter(env, ctx, a_plus_zero); expr concl = mk_eq(a_plus_zero, result.first); expr proof = result.second; @@ -86,8 +86,8 @@ static void theorem_rewrite2_tst() { env.add_theorem("New_theorem2", concl, proof); } -static void then_rewrite1_tst() { - cout << "=== then_rewrite1_tst() ===" << endl; +static void then_rewriter1_tst() { + cout << "=== then_rewriter1_tst() ===" << endl; // Theorem1: Pi(x y : N), x + y = y + x := ADD_COMM x y // Theorem2: Pi(x : N) , x + 0 = x := ADD_ID x // Term : 0 + a @@ -111,11 +111,11 @@ static void then_rewrite1_tst() { env.add_axiom("ADD_ID", add_id_thm_type); // ADD_ID : Pi (x : N), x = x + 0 // Rewriting - rewrite add_comm_thm_rewriter = mk_theorem_rewrite(add_comm_thm_type, add_comm_thm_body); - rewrite add_id_thm_rewriter = mk_theorem_rewrite(add_id_thm_type, add_id_thm_body); - rewrite then_rewriter1 = mk_then_rewrite(add_comm_thm_rewriter, add_id_thm_rewriter); + 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_rewriter1 = mk_then_rewriter(add_comm_thm_rewriter, add_id_thm_rewriter); context ctx; - pair result = then_rewriter1(ctx, zero_plus_a, env); + pair result = then_rewriter1(env, ctx, zero_plus_a); expr concl = mk_eq(zero_plus_a, result.first); expr proof = result.second; @@ -130,8 +130,8 @@ static void then_rewrite1_tst() { env.add_theorem("New_theorem3", concl, proof); } -static void then_rewrite2_tst() { - cout << "=== then_rewrite2_tst() ===" << endl; +static void then_rewriter2_tst() { + cout << "=== then_rewriter2_tst() ===" << endl; // Theorem1: Pi(x y z: N), x + (y + z) = (x + y) + z := ADD_ASSOC x y z // Theorem2: Pi(x y : N), x + y = y + x := ADD_COMM x y // Theorem3: Pi(x : N), x + 0 = x := ADD_ID x @@ -168,13 +168,13 @@ static void then_rewrite2_tst() { env.add_axiom("ADD_ID", add_id_thm_type); // ADD_ID : Pi (x : N), x = x + 0 // Rewriting - rewrite add_assoc_thm_rewriter = mk_theorem_rewrite(add_assoc_thm_type, add_assoc_thm_body); - rewrite add_comm_thm_rewriter = mk_theorem_rewrite(add_comm_thm_type, add_comm_thm_body); - rewrite add_id_thm_rewriter = mk_theorem_rewrite(add_id_thm_type, add_id_thm_body); - rewrite then_rewriter2 = mk_then_rewrite(mk_then_rewrite(add_assoc_thm_rewriter, add_id_thm_rewriter), - mk_then_rewrite(add_comm_thm_rewriter, add_id_thm_rewriter)); + 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)); context ctx; - pair result = then_rewriter2(ctx, zero_plus_a_plus_zero, env); + pair result = then_rewriter2(env, ctx, zero_plus_a_plus_zero); expr concl = mk_eq(zero_plus_a_plus_zero, result.first); expr proof = result.second; cout << "Theorem: " << add_assoc_thm_type << " := " << add_assoc_thm_body << endl; @@ -195,8 +195,8 @@ static void then_rewrite2_tst() { } -static void orelse_rewrite1_tst() { - cout << "=== orelse_rewrite1_tst() ===" << endl; +static void orelse_rewriter1_tst() { + cout << "=== orelse_rewriter1_tst() ===" << endl; // Theorem1: Pi(x y z: N), x + (y + z) = (x + y) + z := ADD_ASSOC x y z // Theorem2: Pi(x y : N), x + y = y + x := ADD_COMM x y // Term : a + b @@ -222,11 +222,11 @@ static void orelse_rewrite1_tst() { env.add_axiom("ADD_COMM", add_comm_thm_type); // ADD_COMM : Pi (x, y: N), x + y = y + z // Rewriting - rewrite add_assoc_thm_rewriter = mk_theorem_rewrite(add_assoc_thm_type, add_assoc_thm_body); - rewrite add_comm_thm_rewriter = mk_theorem_rewrite(add_comm_thm_type, add_comm_thm_body); - rewrite add_assoc_or_comm_thm_rewriter = mk_orelse_rewrite(add_assoc_thm_rewriter, add_comm_thm_rewriter); + 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); context ctx; - pair result = add_assoc_or_comm_thm_rewriter(ctx, a_plus_b, env); + pair result = add_assoc_or_comm_thm_rewriter(env, ctx, a_plus_b); expr concl = mk_eq(a_plus_b, result.first); expr proof = result.second; @@ -240,10 +240,10 @@ static void orelse_rewrite1_tst() { } int main() { - theorem_rewrite1_tst(); - theorem_rewrite2_tst(); - then_rewrite1_tst(); - then_rewrite2_tst(); - orelse_rewrite1_tst(); + theorem_rewriter1_tst(); + theorem_rewriter2_tst(); + then_rewriter1_tst(); + then_rewriter2_tst(); + orelse_rewriter1_tst(); return has_violations() ? 1 : 0; }