test(fo_match): add more unittests
[skip ci]
This commit is contained in:
Soonho Kong
parent
285495313b
commit
6a0d211d54
2 changed files with 473 additions and 1 deletions
|
|
@ -1,3 +1,7 @@
|
|||
add_executable(rewriter_tst rewriter.cpp)
|
||||
target_link_libraries(rewriter_tst ${EXTRA_LIBS})
|
||||
add_test(rewriter ${CMAKE_CURRENT_BINARY_DIR}/rewriter_tst)
|
||||
add_test(rewriter_tst ${CMAKE_CURRENT_BINARY_DIR}/rewriter_tst)
|
||||
|
||||
add_executable(fo_match_tst fo_match.cpp)
|
||||
target_link_libraries(fo_match_tst ${EXTRA_LIBS})
|
||||
add_test(fo_match_tst ${CMAKE_CURRENT_BINARY_DIR}/fo_match_tst)
|
||||
|
|
|
|||
468
src/tests/library/rewriter/fo_match.cpp
Normal file
468
src/tests/library/rewriter/fo_match.cpp
Normal file
|
|
@ -0,0 +1,468 @@
|
|||
/*
|
||||
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/test.h"
|
||||
#include "util/trace.h"
|
||||
#include "kernel/abstract.h"
|
||||
#include "kernel/expr.h"
|
||||
#include "library/all/all.h"
|
||||
#include "library/arith/arith.h"
|
||||
#include "library/arith/nat.h"
|
||||
#include "library/rewriter/fo_match.h"
|
||||
#include "library/rewriter/rewriter.h"
|
||||
#include "library/basic_thms.h"
|
||||
#include "library/printer.h"
|
||||
using namespace lean;
|
||||
|
||||
using std::cout;
|
||||
using std::pair;
|
||||
using std::endl;
|
||||
|
||||
static bool test_match(expr const & p, expr const & v, unsigned o, subst_map & s) {
|
||||
fo_match fm;
|
||||
cout << "match(" << p << ", " << endl
|
||||
<< " " << v << ", " << endl
|
||||
<< " " << o << ", " << s << ")" << endl;
|
||||
bool result = fm.match(p, v, o, s);
|
||||
cout << "= (" << (result ? "true" : "false") << ", "
|
||||
<< s << ")" << endl;
|
||||
return result;
|
||||
}
|
||||
|
||||
static void match_var_tst1() {
|
||||
cout << "--- match_var_tst1() ---" << endl;
|
||||
expr f = Var(0);
|
||||
expr a = Const("a");
|
||||
subst_map s;
|
||||
bool result = test_match(f, a, 0, s);
|
||||
lean_assert_eq(result, true);
|
||||
lean_assert_eq(s.find(0)->second, a);
|
||||
}
|
||||
|
||||
static void match_var_tst2() {
|
||||
cout << "--- match_var_tst2() ---" << endl;
|
||||
expr f = Var(0);
|
||||
expr a = Const("a");
|
||||
subst_map s;
|
||||
bool result = test_match(a, f, 0, s);
|
||||
lean_assert_eq(result, false);
|
||||
lean_assert(s.find(0) == s.end(), s);
|
||||
lean_assert_eq(s.empty(), true)
|
||||
}
|
||||
|
||||
static void match_var_tst3() {
|
||||
cout << "--- match_var_tst3() ---" << endl;
|
||||
expr f = Var(0);
|
||||
expr a = Const("a");
|
||||
subst_map s;
|
||||
bool result = test_match(f, a, 1, s);
|
||||
lean_assert_eq(result, false);
|
||||
lean_assert_eq(s.empty(), true);
|
||||
}
|
||||
|
||||
static void match_var_tst4() {
|
||||
cout << "--- match_var_tst4() ---" << endl;
|
||||
expr f = Var(0);
|
||||
expr a = Const("a");
|
||||
subst_map s;
|
||||
s.insert(0, a);
|
||||
bool result = test_match(f, a, 0, s);
|
||||
lean_assert_eq(result, true);
|
||||
lean_assert_eq(s.find(0)->second, a);
|
||||
}
|
||||
|
||||
static void match_var_tst5() {
|
||||
cout << "--- match_var_tst5() ---" << endl;
|
||||
expr f = Var(0);
|
||||
expr a = Const("a");
|
||||
expr b = Const("b");
|
||||
subst_map s;
|
||||
s.insert(0, b);
|
||||
bool result = test_match(f, a, 0, s);
|
||||
lean_assert_eq(result, false);
|
||||
lean_assert_eq(s.find(0)->second, b);
|
||||
}
|
||||
|
||||
static void match_constant_tst1() {
|
||||
cout << "--- match_constant_tst1() ---" << endl;
|
||||
expr a = Const("a");
|
||||
expr b = Const("b");
|
||||
subst_map s;
|
||||
bool result = test_match(a, a, 0, s);
|
||||
lean_assert_eq(result, true);
|
||||
lean_assert_eq(s.empty(), true);
|
||||
}
|
||||
|
||||
static void match_constant_tst2() {
|
||||
cout << "--- match_constant_tst2() ---" << endl;
|
||||
expr a = Const("a");
|
||||
expr b = Const("b");
|
||||
subst_map s;
|
||||
bool result = test_match(a, b, 0, s);
|
||||
lean_assert_eq(result, false);
|
||||
lean_assert_eq(s.empty(), true);
|
||||
}
|
||||
|
||||
static void match_value_tst1() {
|
||||
cout << "--- match_value_tst1() ---" << endl;
|
||||
expr zero = nVal(0);
|
||||
expr a = Const("a");
|
||||
subst_map s;
|
||||
bool result = test_match(zero, a, 0, s);
|
||||
lean_assert_eq(result, false);
|
||||
lean_assert_eq(s.empty(), true);
|
||||
}
|
||||
|
||||
static void match_value_tst2() {
|
||||
cout << "--- match_value_tst2() ---" << endl;
|
||||
expr zero = nVal(0);
|
||||
expr a = Const("a");
|
||||
subst_map s;
|
||||
bool result = test_match(zero, zero, 0, s);
|
||||
lean_assert_eq(result, true);
|
||||
lean_assert_eq(s.empty(), true);
|
||||
}
|
||||
|
||||
static void match_lambda_tst1() {
|
||||
cout << "--- match_lambda_tst1() ---" << endl;
|
||||
expr a = Const("a");
|
||||
expr zero = nVal(0);
|
||||
expr x = Var(0);
|
||||
expr y = Var(1);
|
||||
expr ty = Type();
|
||||
expr fun1 = mk_lambda("x", ty, x(y));
|
||||
expr fun2 = mk_lambda("x", ty, x(zero));
|
||||
subst_map s;
|
||||
bool result = test_match(fun1, fun2, 0, s);
|
||||
lean_assert_eq(result, true);
|
||||
lean_assert_eq(s.find(0)->second, zero);
|
||||
lean_assert_eq(s.size(), 1);
|
||||
}
|
||||
|
||||
static void match_lambda_tst2() {
|
||||
cout << "--- match_lambda_tst2() ---" << endl;
|
||||
expr a = Const("a");
|
||||
expr x = Var(0);
|
||||
expr y = Var(1);
|
||||
expr ty = Type();
|
||||
expr fun1 = mk_lambda("x", ty, x(y));
|
||||
subst_map s;
|
||||
bool result = test_match(fun1, a, 0, s);
|
||||
lean_assert_eq(result, false);
|
||||
lean_assert_eq(s.empty(), true);
|
||||
}
|
||||
|
||||
static void match_lambda_tst3() {
|
||||
cout << "--- match_lambda_tst3() ---" << endl;
|
||||
expr a = Const("a");
|
||||
expr zero = nVal(0);
|
||||
expr x = Var(0);
|
||||
expr y = Var(1);
|
||||
expr fun1 = mk_lambda("x", Int, x(y));
|
||||
expr fun2 = mk_lambda("x", Nat, x(zero));
|
||||
subst_map s;
|
||||
bool result = test_match(fun1, fun2, 0, s);
|
||||
lean_assert_eq(result, false);
|
||||
lean_assert_eq(s.empty(), true);
|
||||
}
|
||||
|
||||
static void match_lambda_tst4() {
|
||||
cout << "--- match_lambda_tst4() ---" << endl;
|
||||
expr a = Const("a");
|
||||
expr zero = nVal(0);
|
||||
expr x = Var(0);
|
||||
expr y = Var(1);
|
||||
expr ty = Type();
|
||||
expr fun1 = mk_lambda("x", ty, x(y, y));
|
||||
expr fun2 = mk_lambda("x", ty, x(zero));
|
||||
subst_map s;
|
||||
bool result = test_match(fun1, fun2, 0, s);
|
||||
lean_assert_eq(result, false);
|
||||
lean_assert_eq(s.empty(), true);
|
||||
}
|
||||
|
||||
|
||||
static void match_pi_tst1() {
|
||||
cout << "--- match_pi_tst1() ---" << endl;
|
||||
expr a = Const("a");
|
||||
expr zero = nVal(0);
|
||||
expr x = Var(0);
|
||||
expr y = Var(1);
|
||||
expr ty = Type();
|
||||
expr fun1 = mk_pi("x", ty, x(y));
|
||||
expr fun2 = mk_pi("x", ty, x(zero));
|
||||
subst_map s;
|
||||
bool result = test_match(fun1, fun2, 0, s);
|
||||
lean_assert_eq(result, true);
|
||||
lean_assert_eq(s.find(0)->second, zero);
|
||||
lean_assert_eq(s.size(), 1);
|
||||
}
|
||||
|
||||
static void match_pi_tst2() {
|
||||
cout << "--- match_pi_tst2() ---" << endl;
|
||||
expr a = Const("a");
|
||||
expr x = Var(0);
|
||||
expr y = Var(1);
|
||||
expr ty = Type();
|
||||
expr fun1 = mk_pi("x", ty, x(y));
|
||||
subst_map s;
|
||||
bool result = test_match(fun1, a, 0, s);
|
||||
lean_assert_eq(result, false);
|
||||
lean_assert_eq(s.empty(), true);
|
||||
}
|
||||
|
||||
static void match_pi_tst3() {
|
||||
cout << "--- match_pi_tst3() ---" << endl;
|
||||
expr a = Const("a");
|
||||
expr zero = nVal(0);
|
||||
expr x = Var(0);
|
||||
expr y = Var(1);
|
||||
expr fun1 = mk_pi("x", Int, x(y));
|
||||
expr fun2 = mk_pi("x", Nat, x(zero));
|
||||
subst_map s;
|
||||
bool result = test_match(fun1, fun2, 0, s);
|
||||
lean_assert_eq(result, false);
|
||||
lean_assert_eq(s.empty(), true);
|
||||
}
|
||||
|
||||
static void match_pi_tst4() {
|
||||
cout << "--- match_pi_tst4() ---" << endl;
|
||||
expr a = Const("a");
|
||||
expr zero = nVal(0);
|
||||
expr x = Var(0);
|
||||
expr y = Var(1);
|
||||
expr ty = Type();
|
||||
expr fun1 = mk_pi("x", ty, x(y, y));
|
||||
expr fun2 = mk_pi("x", ty, x(zero));
|
||||
subst_map s;
|
||||
bool result = test_match(fun1, fun2, 0, s);
|
||||
lean_assert_eq(result, false);
|
||||
lean_assert_eq(s.empty(), true);
|
||||
}
|
||||
|
||||
static void match_type_tst1() {
|
||||
cout << "--- match_type_tst1() ---" << endl;
|
||||
expr t0 = Type();
|
||||
subst_map s;
|
||||
bool result = test_match(t0, t0, 0, s);
|
||||
lean_assert_eq(result, true);
|
||||
lean_assert_eq(s.empty(), true);
|
||||
}
|
||||
|
||||
static void match_type_tst2() {
|
||||
cout << "--- match_type_tst2() ---" << endl;
|
||||
expr t0 = Type();
|
||||
expr t1 = Type(level()+1);
|
||||
subst_map s;
|
||||
bool result = test_match(t0, t1, 0, s);
|
||||
lean_assert_eq(result, false);
|
||||
lean_assert_eq(s.empty(), true);
|
||||
}
|
||||
|
||||
static void match_let_tst1() {
|
||||
cout << "--- match_let_tst1() ---" << endl;
|
||||
expr l = mk_let("a", Type(), Const("b"), Var(0));
|
||||
subst_map s;
|
||||
bool result = test_match(l, l, 0, s);
|
||||
lean_assert_eq(result, true);
|
||||
lean_assert_eq(s.empty(), true);
|
||||
}
|
||||
|
||||
static void match_let_tst2() {
|
||||
cout << "--- match_let_tst2() ---" << endl;
|
||||
expr t = Eq(Const("a"), Const("b"));
|
||||
expr l = mk_let("a", Type(), Const("b"), Var(0));
|
||||
subst_map s;
|
||||
bool result = test_match(l, t, 0, s);
|
||||
lean_assert_eq(result, false);
|
||||
lean_assert_eq(s.empty(), true);
|
||||
}
|
||||
|
||||
static void match_let_tst3() {
|
||||
cout << "--- match_let_tst3() ---" << endl;
|
||||
expr t = Eq(Const("a"), Const("b"));
|
||||
expr l1 = mk_let("a", Var(0), Const("b"), Var(0));
|
||||
expr l2 = mk_let("a", Int, Const("b"), Var(0));
|
||||
subst_map s;
|
||||
bool result = test_match(l1, l2, 0, s);
|
||||
lean_assert_eq(result, true);
|
||||
lean_assert_eq(s.find(0)->second, Int);
|
||||
lean_assert_eq(s.size(), 1);
|
||||
}
|
||||
|
||||
static void match_let_tst4() {
|
||||
cout << "--- match_let_tst4() ---" << endl;
|
||||
expr t = Eq(Const("a"), Const("b"));
|
||||
expr l1 = mk_let("a", Nat, Const("b"), Var(0));
|
||||
expr l2 = mk_let("a", Int, Const("b"), Var(0));
|
||||
subst_map s;
|
||||
bool result = test_match(l1, l2, 0, s);
|
||||
lean_assert_eq(result, false);
|
||||
lean_assert_eq(s.empty(), true);
|
||||
}
|
||||
|
||||
static void match_let_tst5() {
|
||||
cout << "--- match_let_tst5() ---" << endl;
|
||||
expr t = Eq(Const("a"), Const("b"));
|
||||
expr l1 = mk_let("a", Int, Var(3), Var(0));
|
||||
expr l2 = mk_let("a", Int, Const("b"), Const("b"));
|
||||
subst_map s;
|
||||
bool result = test_match(l1, l2, 0, s);
|
||||
lean_assert_eq(result, false);
|
||||
lean_assert_eq(s.empty(), true);
|
||||
}
|
||||
|
||||
static void match_let_tst6() {
|
||||
cout << "--- match_let_tst6() ---" << endl;
|
||||
expr t = Eq(Const("a"), Const("b"));
|
||||
expr l1 = mk_let("a", Var(0), Var(1), Var(0));
|
||||
expr l2 = mk_let("a", Int, Const("b"), Const("b"));
|
||||
subst_map s;
|
||||
bool result = test_match(l1, l2, 0, s);
|
||||
lean_assert_eq(result, false);
|
||||
lean_assert_eq(s.empty(), true);
|
||||
}
|
||||
|
||||
static void match_let_tst7() {
|
||||
cout << "--- match_let_tst7() ---" << endl;
|
||||
expr t = Eq(Const("a"), Const("b"));
|
||||
expr l1 = mk_let("a", Var(0), Var(1), Var(0));
|
||||
expr l2 = mk_let("a", Int, Const("b"), Var(0));
|
||||
subst_map s;
|
||||
bool result = test_match(l1, l2, 0, s);
|
||||
lean_assert_eq(result, true);
|
||||
lean_assert_eq(s.find(0)->second, Int);
|
||||
lean_assert_eq(s.find(1)->second, Const("b"));
|
||||
lean_assert_eq(s.size(), 2);
|
||||
}
|
||||
|
||||
static void match_let_tst8() {
|
||||
cout << "--- match_let_tst8() ---" << endl;
|
||||
expr t = Eq(Const("a"), Const("b"));
|
||||
expr l1 = mk_let("a", Nat, Var(1), Var(0));
|
||||
expr l2 = mk_let("a", Int, Const("b"), Var(0));
|
||||
subst_map s;
|
||||
bool result = test_match(l1, l2, 0, s);
|
||||
lean_assert_eq(result, false);
|
||||
lean_assert_eq(s.empty(), true);
|
||||
}
|
||||
|
||||
static void match_let_tst9() {
|
||||
cout << "--- match_let_tst9() ---" << endl;
|
||||
expr t = Eq(Const("a"), Const("b"));
|
||||
expr l1 = mk_let("a", Var(0), Var(0), Var(0));
|
||||
expr l2 = mk_let("a", Nat, Const("b"), Const("a"));
|
||||
subst_map s;
|
||||
bool result = test_match(l1, l2, 0, s);
|
||||
lean_assert_eq(result, false);
|
||||
lean_assert_eq(s.empty(), true);
|
||||
}
|
||||
|
||||
static void match_eq_tst1() {
|
||||
cout << "--- match_eq_tst1() ---" << endl;
|
||||
expr x = Var(0);
|
||||
expr f = Const("f");
|
||||
expr a = Const("a");
|
||||
subst_map s;
|
||||
bool result = test_match(mk_eq(x, a), mk_eq(f, a), 0, s);
|
||||
lean_assert_eq(result, true);
|
||||
lean_assert_eq(s.find(0)->second, f);
|
||||
lean_assert_eq(s.size(), 1);
|
||||
}
|
||||
|
||||
static void match_eq_tst2() {
|
||||
cout << "--- match_eq_tst2() ---" << endl;
|
||||
expr x = Var(0);
|
||||
expr f = Const("f");
|
||||
expr a = Const("a");
|
||||
subst_map s;
|
||||
bool result = test_match(mk_eq(nAdd(x, a), x), mk_eq(nAdd(f, a), f), 0, s);
|
||||
lean_assert_eq(result, true);
|
||||
lean_assert_eq(s.find(0)->second, f);
|
||||
lean_assert_eq(s.size(), 1);
|
||||
}
|
||||
|
||||
static void match_eq_tst3() {
|
||||
cout << "--- match_eq_tst3() ---" << endl;
|
||||
expr x = Var(0);
|
||||
expr f = Const("f");
|
||||
expr a = Const("a");
|
||||
subst_map s;
|
||||
bool result = test_match(mk_eq(nAdd(x, a), x), f, 0, s);
|
||||
lean_assert_eq(result, false);
|
||||
lean_assert_eq(s.empty(), true);
|
||||
}
|
||||
|
||||
static void match_metavar_tst1() {
|
||||
cout << "--- match_metavar_tst1() ---" << endl;
|
||||
expr m1 = mk_metavar(0);
|
||||
expr m2 = mk_metavar(1);
|
||||
expr f = Const("f");
|
||||
subst_map s;
|
||||
bool result = test_match(m1, m1, 0, s);
|
||||
lean_assert_eq(result, true);
|
||||
lean_assert_eq(s.size(), 0);
|
||||
}
|
||||
|
||||
static void match_metavar_tst2() {
|
||||
cout << "--- match_metavar_tst2() ---" << endl;
|
||||
expr m1 = mk_metavar(0);
|
||||
expr m2 = mk_metavar(1);
|
||||
expr f = Const("f");
|
||||
subst_map s;
|
||||
bool result = test_match(m1, m2, 0, s);
|
||||
lean_assert_eq(result, false);
|
||||
lean_assert_eq(s.size(), 0);
|
||||
}
|
||||
|
||||
static void match_metavar_tst3() {
|
||||
cout << "--- match_metavar_tst3() ---" << endl;
|
||||
expr m1 = mk_metavar(0);
|
||||
expr f = Const("f");
|
||||
subst_map s;
|
||||
bool result = test_match(m1, f, 0, s);
|
||||
lean_assert_eq(result, false);
|
||||
lean_assert_eq(s.size(), 0);
|
||||
}
|
||||
|
||||
int main() {
|
||||
match_var_tst1();
|
||||
match_var_tst2();
|
||||
match_var_tst3();
|
||||
match_var_tst4();
|
||||
match_var_tst5();
|
||||
match_constant_tst1();
|
||||
match_constant_tst2();
|
||||
match_value_tst1();
|
||||
match_value_tst2();
|
||||
match_lambda_tst1();
|
||||
match_lambda_tst2();
|
||||
match_lambda_tst3();
|
||||
match_lambda_tst4();
|
||||
match_pi_tst1();
|
||||
match_pi_tst2();
|
||||
match_pi_tst3();
|
||||
match_pi_tst4();
|
||||
match_type_tst1();
|
||||
match_type_tst2();
|
||||
match_let_tst1();
|
||||
match_let_tst2();
|
||||
match_let_tst3();
|
||||
match_let_tst4();
|
||||
match_let_tst5();
|
||||
match_let_tst6();
|
||||
match_let_tst7();
|
||||
match_let_tst8();
|
||||
match_let_tst9();
|
||||
enable_trace("fo_match");
|
||||
match_eq_tst1();
|
||||
match_eq_tst2();
|
||||
match_eq_tst3();
|
||||
match_metavar_tst1();
|
||||
match_metavar_tst2();
|
||||
match_metavar_tst3();
|
||||
return has_violations() ? 1 : 0;
|
||||
}
|
||||
Loading…
Reference in a new issue