michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

test(library/update_expr): add missing tests

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-11-17 13:36:15 -08:00
parent df94e44806
commit 5254dba195
2 changed files with 58 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/tests/library/CMakeLists.txt
View file

@ -16,3 +16,6 @@ add_test(deep_copy ${CMAKE_CURRENT_BINARY_DIR}/deep_copy)
add_executable(arith_tst arith.cpp) add_executable(arith_tst arith.cpp)
target_link_libraries(arith_tst ${EXTRA_LIBS}) target_link_libraries(arith_tst ${EXTRA_LIBS})
add_test(arith_tst ${CMAKE_CURRENT_BINARY_DIR}/arith_tst) add_test(arith_tst ${CMAKE_CURRENT_BINARY_DIR}/arith_tst)
add_executable(update_expr update_expr.cpp)
target_link_libraries(update_expr ${EXTRA_LIBS})
add_test(update_expr ${CMAKE_CURRENT_BINARY_DIR}/update_expr)

55
src/tests/library/update_expr.cpp Normal file
View file

@ -0,0 +1,55 @@
/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "util/test.h"
#include "kernel/abstract.h"
#include "library/update_expr.h"
using namespace lean;
static void tst1() {
expr a = Const("a");
expr b = Const("b");
expr eq1 = Eq(a, b);
expr eq2 = update_eq(eq1, a, a);
expr eq3 = update_eq(eq1, a, b);
lean_assert(eq_lhs(eq3) == a);
lean_assert(eq_rhs(eq3) == b);
lean_assert(is_eqp(eq1, eq3));
}
static void tst2() {
expr a = Const("a");
expr N = Const("N");
expr t1 = Fun(a, N, a);
expr b = Const("b");
expr t2 = update_abstraction(t1, N, abst_body(t1));
lean_assert(is_eqp(t1, t2));
t2 = update_abstraction(t1, N, a);
lean_assert(!is_eqp(t1, t2));
lean_assert(abst_body(t2) == a);
t1 = Pi(a, N, a);
t2 = update_abstraction(t1, N, abst_body(t1));
lean_assert(is_eqp(t1, t2));
}
void tst3() {
expr a = Const("a");
expr b = Const("b");
expr f = Const("f");
expr t1 = Let(a, b, f(a));
expr t2 = update_let(t1, expr(), b, let_body(t1));
lean_assert(is_eqp(t1, t2));
t2 = update_let(t1, expr(), a, let_body(t1));
lean_assert(!is_eqp(t1, t2));
lean_assert(t2 == Let(a, a, f(a)));
}
int main() {
tst1();
tst2();
tst3();
return has_violations() ? 1 : 0;
}