From ab1a89e24c6562ef09543a5a9c632c9a03448f09 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 14 May 2014 14:44:52 -0700 Subject: [PATCH] refactor(library): remove dead files Signed-off-by: Leonardo de Moura --- src/library/CMakeLists.txt | 4 +--- src/library/bin_op.cpp | 41 -------------------------------------- src/library/bin_op.h | 33 ------------------------------ src/library/equality.cpp | 30 ---------------------------- src/library/equality.h | 14 ------------- 5 files changed, 1 insertion(+), 121 deletions(-) delete mode 100644 src/library/bin_op.cpp delete mode 100644 src/library/bin_op.h delete mode 100644 src/library/equality.cpp delete mode 100644 src/library/equality.h diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index cad233401..05d180c3c 100644 --- a/src/library/CMakeLists.txt +++ b/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}) diff --git a/src/library/bin_op.cpp b/src/library/bin_op.cpp deleted file mode 100644 index bc3c2df52..000000000 --- a/src/library/bin_op.cpp +++ /dev/null @@ -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 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 const & l) { - return mk_bin_lop(op, unit, l.size(), l.begin()); -} -} diff --git a/src/library/bin_op.h b/src/library/bin_op.h deleted file mode 100644 index 7dbe5d712..000000000 --- a/src/library/bin_op.h +++ /dev/null @@ -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 num_args == 0, args[0] if num_args == 1, and - (op args[0] (op args[1] (op ... ))) -*/ -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 const & l); - -/** - \brief Return unit if num_args == 0, args[0] if num_args == 1, and - (op ... (op (op args[0] args[1]) args[2]) ...) -*/ -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 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 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 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 const & l) { return mk_or(l.size(), l.begin()); } -} diff --git a/src/library/equality.cpp b/src/library/equality.cpp deleted file mode 100644 index e853c13c5..000000000 --- a/src/library/equality.cpp +++ /dev/null @@ -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)); -} -} diff --git a/src/library/equality.h b/src/library/equality.h deleted file mode 100644 index 2716d3745..000000000 --- a/src/library/equality.h +++ /dev/null @@ -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); -}