refactor(library): remove dead files

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

src/library/CMakeLists.txt

@@ -1,7 +1,5 @@
 add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp
   occurs.cpp kernel_bindings.cpp io_state_stream.cpp)
-# context_to_lambda.cpp placeholder.cpp
-# fo_unify.cpp bin_op.cpp equality.cpp
-# hop_match.cpp)
+# placeholder.cpp fo_unify.cpp hop_match.cpp)
 
 target_link_libraries(library ${LEAN_LIBS})

src/library/bin_op.cpp

@@ -1,41 +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 "library/bin_op.h"
-
-namespace lean {
-expr mk_bin_rop(expr const & op, expr const & unit, unsigned num_args, expr const * args) {
-    if (num_args == 0) {
-        return unit;
-    } else {
-        expr r = args[num_args - 1];
-        unsigned i = num_args - 1;
-        while (i > 0) {
-            --i;
-            r = mk_app({op, args[i], r});
-        }
-        return r;
-    }
-}
-expr mk_bin_rop(expr const & op, expr const & unit, std::initializer_list<expr> const & l) {
-    return mk_bin_rop(op, unit, l.size(), l.begin());
-}
-
-expr mk_bin_lop(expr const & op, expr const & unit, unsigned num_args, expr const * args) {
-    if (num_args == 0) {
-        return unit;
-    } else {
-        expr r = args[0];
-        for (unsigned i = 1; i < num_args; i++) {
-            r = mk_app({op, r, args[i]});
-        }
-        return r;
-    }
-}
-expr mk_bin_lop(expr const & op, expr const & unit, std::initializer_list<expr> const & l) {
-    return mk_bin_lop(op, unit, l.size(), l.begin());
-}
-}

src/library/bin_op.h

@@ -1,33 +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 "kernel/kernel.h"
-
-namespace lean {
-/**
-   \brief Return unit if <tt>num_args == 0</tt>, args[0] if <tt>num_args == 1</tt>, and
-   <tt>(op args[0] (op args[1] (op ... )))</tt>
-*/
-expr mk_bin_rop(expr const & op, expr const & unit, unsigned num_args, expr const * args);
-expr mk_bin_rop(expr const & op, expr const & unit, std::initializer_list<expr> const & l);
-
-/**
-   \brief Return unit if <tt>num_args == 0</tt>, args[0] if <tt>num_args == 1</tt>, and
-   <tt>(op ... (op (op args[0] args[1]) args[2]) ...)</tt>
-*/
-expr mk_bin_lop(expr const & op, expr const & unit, unsigned num_args, expr const * args);
-expr mk_bin_lop(expr const & op, expr const & unit, std::initializer_list<expr> const & l);
-
-inline expr mk_implies(unsigned num_args, expr const * args) { return mk_bin_rop(mk_implies_fn(), False, num_args, args); }
-inline expr Implies(std::initializer_list<expr> const & l) { return mk_implies(l.size(), l.begin()); }
-
-inline expr mk_and(unsigned num_args, expr const * args) { return mk_bin_rop(mk_and_fn(), True, num_args, args); }
-inline expr And(std::initializer_list<expr> const & l) { return mk_and(l.size(), l.begin()); }
-
-inline expr mk_or(unsigned num_args, expr const * args) { return mk_bin_rop(mk_or_fn(), False, num_args, args); }
-inline expr Or(std::initializer_list<expr> const & l) { return mk_or(l.size(), l.begin()); }
-}

src/library/equality.cpp

@@ -1,30 +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 "kernel/kernel.h"
-#include "library/expr_pair.h"
-
-namespace lean {
-bool is_equality(expr const & e) {
-    return is_eq(e) || is_iff(e);
-}
-
-bool is_equality(expr const & e, expr & lhs, expr & rhs) {
-    if (is_eq(e) || is_iff(e)) {
-        unsigned num = num_args(e);
-        lhs = arg(e, num - 2);
-        rhs = arg(e, num - 1);
-        return true;
-    } else {
-        return false;
-    }
-}
-
-expr_pair get_equality_args(expr const & e) {
-    unsigned num = num_args(e);
-    return mk_pair(arg(e, num - 2), arg(e, num - 1));
-}
-}

src/library/equality.h

@@ -1,14 +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 "library/expr_pair.h"
-
-namespace lean {
-bool is_equality(expr const & e);
-bool is_equality(expr const & e, expr & lhs, expr & rhs);
-expr_pair get_equality_args(expr const & e);
-}