Remove unnecessary files

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/library/CMakeLists.txt

@@ -1,4 +1,4 @@
 add_library(library basic_thms.cpp deep_copy.cpp max_sharing.cpp
   toplevel.cpp printer.cpp formatter.cpp context_to_lambda.cpp
-  state.cpp beta.cpp metavar.cpp elaborator.cpp)
+  state.cpp metavar.cpp elaborator.cpp)
 target_link_libraries(library ${LEAN_LIBS})

src/library/beta.cpp

@@ -1,58 +0,0 @@
-/*
-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 "beta.h"
-#include "instantiate.h"
-#include "environment.h"
-
-namespace lean {
-bool is_head_beta(expr const & e) {
-    return is_app(e) && is_lambda(arg(e, 0));
-}
-expr head_beta(expr const & e) {
-    if (!is_head_beta(e)) {
-        return e;
-    } else {
-        unsigned num  = num_args(e);
-        unsigned num1 = num - 1;
-        expr const * f = &arg(e, 0);
-        lean_assert(is_lambda(*f));
-        unsigned m = 1;
-        while (is_lambda(abst_body(*f)) && m < num1) {
-            f = &abst_body(*f);
-            m++;
-        }
-        lean_assert(m <= num1);
-        expr r = instantiate(abst_body(*f), m, &arg(e, 1));
-        if (m == num1) {
-            return r;
-        } else {
-            buffer<expr> args;
-            args.push_back(r);
-            m++;
-            for (; m < num; m++)
-                args.push_back(arg(e, m));
-            return mk_app(args.size(), args.data());
-        }
-    }
-}
-
-expr head_reduce(expr const & e, environment const & env, name_set const * defs) {
-    if (is_head_beta(e)) {
-        return head_beta(e);
-    } else if (is_let(e)) {
-        return instantiate(let_body(e), let_value(e));
-    } else if (is_constant(e)) {
-        name const & n = const_name(e);
-        if (defs == nullptr || defs->find(n) != defs->end()) {
-            object const & obj = env.find_object(n);
-            if (obj && obj.is_definition() && !obj.is_opaque())
-                return obj.get_value();
-        }
-    }
-    return e;
-}
-}

src/library/beta.h

@@ -1,31 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "expr.h"
-#include "name_set.h"
-
-namespace lean {
-class environment;
-/**
-    \brief Return true iff the given expression is of the form:
-
-    ((fun (x : A), B) Arg)
-*/
-bool is_head_beta(expr const & e);
-/** \brief Apply head beta-reduction to the given expression. */
-expr head_beta(expr const & e);
-
-/**
-   \brief Try to reduce the head of the given expression.
-   The following reductions are tried:
-   1- Beta reduction
-   2- Constant unfolding (if constant is defined in env, and defs ==
-   nullptr or it contains constant).
-   3- Let expansion
-*/
-expr head_reduce(expr const & e, environment const & env, name_set const * defs = nullptr);
-};

src/tests/library/CMakeLists.txt

@@ -1,9 +1,6 @@
 add_executable(implicit_args implicit_args.cpp)
 target_link_libraries(implicit_args ${EXTRA_LIBS})
 add_test(implicit_args ${CMAKE_CURRENT_BINARY_DIR}/implicit_args)
-add_executable(beta beta.cpp)
-target_link_libraries(beta ${EXTRA_LIBS})
-add_test(beta ${CMAKE_CURRENT_BINARY_DIR}/beta)
 add_executable(metavar metavar.cpp)
 target_link_libraries(metavar ${EXTRA_LIBS})
 add_test(metavar ${CMAKE_CURRENT_BINARY_DIR}/metavar)

src/tests/library/beta.cpp

@@ -1,43 +0,0 @@
-/*
-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;
-}