Add rewrite and first-order pattern matching skeletal

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

src/library/rewrite/CMakeLists.txt

@@ -0,0 +1,2 @@
+add_library(rewrite rewrite.cpp fo_match.cpp)
+target_link_libraries(rewrite ${LEAN_LIBS})

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 <utility>
+#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);
+    }
+}
+}

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 <unordered_map>
+#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<unsigned, expr const &> 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);
+};
+}

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
+//

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 <iostream>
+#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);
+    }
+};
+}

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)

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;
+}