diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 313ee93477..9e3683d630 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -126,6 +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(frontends/lean) set(LEAN_LIBS ${LEAN_LIBS} lean_frontend) set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -pthread ${LEAN_EXTRA_LINKER_FLAGS}") @@ -137,6 +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/frontends/lean) # Include style check diff --git a/src/library/rewrite/CMakeLists.txt b/src/library/rewrite/CMakeLists.txt new file mode 100644 index 0000000000..38ae4ea46c --- /dev/null +++ b/src/library/rewrite/CMakeLists.txt @@ -0,0 +1,2 @@ +add_library(rewrite rewrite.cpp fo_match.cpp) +target_link_libraries(rewrite ${LEAN_LIBS}) diff --git a/src/library/rewrite/fo_match.cpp b/src/library/rewrite/fo_match.cpp new file mode 100644 index 0000000000..47f09fcfd2 --- /dev/null +++ b/src/library/rewrite/fo_match.cpp @@ -0,0 +1,181 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Soonho Kong +*/ +#include +#include "kernel/expr.h" +#include "kernel/context.h" +#include "library/all/all.h" +#include "library/arith/nat.h" +#include "library/arith/arith.h" +#include "library/rewrite/rewrite.h" + +namespace lean { + + +std::ostream & operator<<(std::ostream & out, expr_pair const & p) { + out << "(" + << p.first << ", " + << p.second << ")"; + return out; +} + +bool fo_match::match_var(context & ctx, expr const & p, expr const & t, subst_map & s) { + std::cerr << "match_var : (" + << ctx << " ," + << p << ", " + << t << ", " +// << s << ")" + << std::endl; + s.insert(std::make_pair(var_idx(p), t)); + return true; +} +bool fo_match::match_constant(context & ctx, expr const & p, expr const & t, subst_map & s) { + std::cerr << "match_constant : (" + << ctx << " ," + << p << ", " + << t << ", " +// << s << ")" + << std::endl; + if (is_constant(t) && const_name(p) == const_name(t)) { + return true; + } else { + return false; + } +} +bool fo_match::match_value(context & ctx, expr const & p, expr const & t, subst_map & s) { + std::cerr << "match_value : (" + << ctx << " ," + << p << ", " + << t << ", " +// << s << ")" + << std::endl; + if (is_value(t) && to_value(p) == to_value(t)) { + return true; + } else { + return false; + } +} +bool fo_match::match_app(context & ctx, expr const & p, expr const & t, subst_map & s) { + std::cerr << "match_app : (" + << ctx << " ," + << p << ", " + << t << ", " +// << s << ")" + << std::endl; + unsigned num_p = num_args(p); + unsigned num_t = num_args(p); + if (num_p != num_t) { + return false; + } + + for unsigned i = 0; i <= num_p; i++) { + if (!match(ctx, arg(p, i), arg(t, i), s)) + return false; + } + return true; +} +bool fo_match::match_lambda(context & ctx, expr const & p, expr const & t, subst_map & s) { + std::cerr << "match_lambda : (" + << ctx << " ," + << p << ", " + << t << ", " +// << s << ")" + << std::endl; + // TODO(soonho) + std::cerr << "fun (" << abst_name(p) + << " : " << abst_domain(p) + << "), " << abst_body(p) << std::endl; + if (!is_lambda(t)) { + return false; + } + + return true; +} +bool fo_match::match_pi(context & ctx, expr const & p, expr const & t, subst_map & s) { + std::cerr << "match_pi : (" + << ctx << " ," + << p << ", " + << t << ", " +// << s << ")" + << std::endl; + // TODO(soonho) + std::cerr << "Pi (" << abst_name(p) + << " : " << abst_domain(p) + << "), " << abst_body(p) << std::endl; + return true; +} +bool fo_match::match_type(context & ctx, expr const & p, expr const & t, subst_map & s) { + std::cerr << "match_type : (" + << ctx << " ," + << p << ", " + << t << ", " +// << s << ")" + << std::endl; + // TODO(soonho) + return true; +} +bool fo_match::match_eq(context & ctx, expr const & p, expr const & t, subst_map & s) { + std::cerr << "match_eq : (" + << ctx << " ," + << p << ", " + << t << ", " +// << s << ")" + << std::endl; + // TODO(soonho) + return true; +} +bool fo_match::match_let(context & ctx, expr const & p, expr const & t, subst_map & s) { + std::cerr << "match_let : (" + << ctx << " ," + << p << ", " + << t << ", " +// << s << ")" + << std::endl; + // TODO(soonho) + return true; +} +bool fo_match::match_metavar(context & ctx, expr const & p, expr const & t, subst_map & s) { + std::cerr << "match_meta : (" + << ctx << " ," + << p << ", " + << t << ", " +// << s << ")" + << std::endl; + // TODO(soonho) + return true; +} +bool fo_match::match(context & ctx, expr const & p, expr const & t, subst_map & s) { + std::cerr << "match : (" + << ctx << " ," + << p << ", " + << t << ", " +// << s << ")" + << std::endl; + + switch (p.kind()) { + case expr_kind::Var: + return match_var(ctx, p, t, s); + case expr_kind::Constant: + return match_constant(ctx, p, t, s); + case expr_kind::Value: + return match_value(ctx, p, t, s); + case expr_kind::App: + return match_app(ctx, p, t, s); + case expr_kind::Lambda: + return match_lambda(ctx, p, t, s); + case expr_kind::Pi: + return match_pi(ctx, p, t, s); + case expr_kind::Type: + return match_type(ctx, p, t, s); + case expr_kind::Eq: + return match_eq(ctx, p, t, s); + case expr_kind::Let: + return match_let(ctx, p, t, s); + case expr_kind::MetaVar: + return match_metavar(ctx, p, t, s); + } +} +} diff --git a/src/library/rewrite/fo_match.h b/src/library/rewrite/fo_match.h new file mode 100644 index 0000000000..b096f706d1 --- /dev/null +++ b/src/library/rewrite/fo_match.h @@ -0,0 +1,36 @@ +/* +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 "kernel/expr.h" +#include "kernel/context.h" +#include "util/list.h" +#include "library/all/all.h" +#include "library/expr_pair.h" +#include "library/arith/nat.h" +#include "library/arith/arith.h" + +namespace lean { + +typedef std::unordered_map subst_map; + +class fo_match { +private: + bool match_var(context & ctx, expr const & p, expr const & t, subst_map & s); + bool match_constant(context & ctx, expr const & p, expr const & t, subst_map & s); + bool match_value(context & ctx, expr const & p, expr const & t, subst_map & s); + bool match_app(context & ctx, expr const & p, expr const & t, subst_map & s); + bool match_lambda(context & ctx, expr const & p, expr const & t, subst_map & s); + bool match_pi(context & ctx, expr const & p, expr const & t, subst_map & s); + bool match_type(context & ctx, expr const & p, expr const & t, subst_map & s); + bool match_eq(context & ctx, expr const & p, expr const & t, subst_map & s); + bool match_let(context & ctx, expr const & p, expr const & t, subst_map & s); + bool match_metavar(context & ctx, expr const & p, expr const & t, subst_map & s); +public: + bool match(context & ctx, expr const & p, expr const & t, subst_map & s); +}; +} diff --git a/src/library/rewrite/rewrite.cpp b/src/library/rewrite/rewrite.cpp new file mode 100644 index 0000000000..20784fe20f --- /dev/null +++ b/src/library/rewrite/rewrite.cpp @@ -0,0 +1,26 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Soonho Kong +*/ +#include "kernel/environment.h" +#include "kernel/abstract.h" +#include "kernel/builtin.h" +#include "library/rewrite/rewrite.h" + +// Term Rewriting + +// +// ORELSE +// APP_RW +// LAMBDA_RW +// PI_RW +// LET_RW +// DEPTH_RW +// THEOREM2RW +// TRIVIAL_RW +// FORALL +// FAIL +// FAIL_IF +// diff --git a/src/library/rewrite/rewrite.h b/src/library/rewrite/rewrite.h new file mode 100644 index 0000000000..4e48c2589e --- /dev/null +++ b/src/library/rewrite/rewrite.h @@ -0,0 +1,65 @@ +/* +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 "kernel/context.h" +#include "kernel/environment.h" +#include "library/printer.h" +#include "library/rewrite/fo_match.h" + +namespace lean { + +/** + \brief Format + + uses `sexpr` as an internal representation. + + nil = ["NIL"] + text s = ("TEXT" . s) + choice f1 f2 = ("CHOICE" f1 . f2) + compose f1 ... fn = ["COMPOSE" f1 ... fn] + line = ["LINE"] + nest n f = ("NEST" n . f) + highlight c f = ("HIGHLIGHT" c . f) +*/ + +class theorem_rw { +private: + expr const & thm_t; + expr const & thm_v; + unsigned num_args; +public: + theorem_rw(expr const & t, expr const & v) + : thm_t(t), thm_v(v), num_args(0) { + std::cout << "Theorem_Rewrite " + << "(" << thm_v << " : " << thm_t << ")" + << std::endl; + // We expect the theorem is in the form of + // Pi (x_1 : t_1 ... x_n : t_n), t = s + expr tmp = t; + while (is_pi(tmp)) { + tmp = abst_body(tmp); + num_args++; + } + if (!is_eq(tmp)) { + std::cout << "Theorem " << t << " is not in the form of " + << "Pi (x_1 : t_1 ... x_n : t_n), t = s" << std::endl; + } + std::cout << "Theorem " << t << " is OK. Number of Arg = " << num_args << std::endl; + } + + void operator()(context & ctx, expr const & t) { + std::cout << "Theorem_Rewrite: (" + << "Context : " << ctx + << ", Term : " << t + << ")" << std::endl; + fo_match fm; + subst_map s; + fm.match(ctx, thm_t, t, s); + } +}; +} diff --git a/src/tests/library/rewrite/CMakeLists.txt b/src/tests/library/rewrite/CMakeLists.txt new file mode 100644 index 0000000000..84d2ca7285 --- /dev/null +++ b/src/tests/library/rewrite/CMakeLists.txt @@ -0,0 +1,3 @@ +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/rewrite/rewrite.cpp b/src/tests/library/rewrite/rewrite.cpp new file mode 100644 index 0000000000..c53e004c17 --- /dev/null +++ b/src/tests/library/rewrite/rewrite.cpp @@ -0,0 +1,39 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Soonho Kong +*/ +#include "kernel/abstract.h" +#include "kernel/context.h" +#include "kernel/expr.h" +#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" +using namespace lean; + +using std::cout; +using std::endl; + +int main() { + environment env = mk_toplevel(); + env.add_var("x", Nat); + expr x = Const("x"); // x : Nat + expr y = Const("y"); // y : Nat + expr zero = nVal(0); // 0 : Nat + expr x_plus_zero = nAdd(x, zero); // x_plus_zero := x + 0 + expr y_plus_zero = nAdd(y, zero); // y_plus_zero := y + 0 + std::cout << x_plus_zero << std::endl; + env.display(std::cout); + + expr thm_t = Pi("x", Nat, Eq(nAdd(Const("x"), nVal(0)), Const("x"))); // Pi (x : Z), x + 0 = x + env.add_axiom("H1", thm_t); // H1 : Pi (x : N), x = x + 0 + expr thm_v = Const("H1"); + + theorem_rw trw(thm_t, thm_v); + context ctx; + trw(ctx, y_plus_zero); + return 0; +}