From f08c06d582eb503a51b0a5b7f41a2a57a9f36ffa Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 23 Aug 2013 09:35:35 -0700
Subject: [PATCH] Add head_beta tests

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/CMakeLists.txt               |  1 +
 src/tests/library/CMakeLists.txt |  3 +++
 src/tests/library/beta.cpp       | 43 ++++++++++++++++++++++++++++++++
 3 files changed, 47 insertions(+)
 create mode 100644 src/tests/library/CMakeLists.txt
 create mode 100644 src/tests/library/beta.cpp

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index c07627c3e..7655db1a8 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -104,4 +104,5 @@ add_subdirectory(tests/util)
 add_subdirectory(tests/util/numerics)
 add_subdirectory(tests/interval)
 add_subdirectory(tests/kernel)
+add_subdirectory(tests/library)
 add_subdirectory(tests/frontends/lean)
diff --git a/src/tests/library/CMakeLists.txt b/src/tests/library/CMakeLists.txt
new file mode 100644
index 000000000..fa8376974
--- /dev/null
+++ b/src/tests/library/CMakeLists.txt
@@ -0,0 +1,3 @@
+add_executable(beta beta.cpp)
+target_link_libraries(beta ${EXTRA_LIBS})
+add_test(beta ${CMAKE_CURRENT_BINARY_DIR}/beta)
diff --git a/src/tests/library/beta.cpp b/src/tests/library/beta.cpp
new file mode 100644
index 000000000..1b3a7c22e
--- /dev/null
+++ b/src/tests/library/beta.cpp
@@ -0,0 +1,43 @@
+/*
+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 "test.h"
+#include "beta.h"
+#include "abstract.h"
+#include "printer.h"
+using namespace lean;
+
+static void tst1() {
+    expr f = Const("f");
+    expr g = Const("g");
+    expr x = Const("x");
+    expr y = Const("y");
+    expr z = Const("z");
+    expr A = Const("A");
+    expr a = Const("a");
+    expr b = Const("b");
+    expr c = Const("c");
+    expr d = Const("d");
+    expr F = Fun({{x, A}, {y, A}, {z, A}}, f(x, g(y, x, z)));
+    lean_assert(is_head_beta(F(a, b)));
+    lean_assert(!is_head_beta(f(a,b)));
+    lean_assert(!is_head_beta(Fun({x,A}, x)));
+    std::cout << head_beta(F(a,b)) << "\n";
+    lean_assert(head_beta(F(a,b)) == Fun({z, A}, f(a, g(b, a, z))));
+    lean_assert(head_beta(F(a,b,c)) == f(a, g(b, a, c)));
+    std::cout << head_beta(F(a,b,c,d)) << "\n";
+    lean_assert(head_beta(F(a,b,c,d)) == mk_app(f(a, g(b, a, c)), d));
+    lean_assert(head_beta(F(a)) == Fun({{y, A}, {z, A}}, f(a, g(y, a, z))));
+    lean_assert(head_beta(F) == F);
+    lean_assert(head_beta(f(a,b)) == f(a,b));
+    lean_assert(head_beta(mk_app(Fun({x,A}, x), a, b)) == a(b));
+    lean_assert(head_beta(mk_app(Fun({x,A}, x), a)) == a);
+}
+
+int main() {
+    tst1();
+    return has_violations() ? 1 : 0;
+}