refactor(kernel/builtin): emove mk_bin_rop and mk_bin_lop to library

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

src/kernel/builtin.cpp

@@ -13,38 +13,6 @@ Author: Leonardo de Moura
 #endif
 
 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());
-}
-
 // =======================================
 // Bultin universe variables m and u
 static level m_lvl(name("M"));

src/kernel/builtin.h

@@ -8,20 +8,6 @@ Author: Leonardo de Moura
 #include "kernel/expr.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);
-
 /** \brief Return (Type m)  m >= bottom + Offset */
 extern expr const TypeM;
 
@@ -66,9 +52,7 @@ bool is_implies_fn(expr const & e);
 inline bool is_implies(expr const & e) { return is_app(e) && is_implies_fn(arg(e, 0)); }
 /** \brief Return the term (e1 => e2) */
 inline expr mk_implies(expr const & e1, expr const & e2) { return mk_app(mk_implies_fn(), e1, e2); }
-inline expr mk_implies(unsigned num_args, expr const * args) { lean_assert(num_args >= 2); return mk_bin_rop(mk_implies_fn(), False, num_args, args); }
 inline expr Implies(expr const & e1, expr const & e2) { return mk_implies(e1, e2); }
-inline expr Implies(std::initializer_list<expr> const & l) { return mk_implies(l.size(), l.begin()); }
 
 /** \brief Return the Lean Iff operator */
 expr mk_iff_fn();
@@ -76,9 +60,7 @@ bool is_iff_fn(expr const & e);
 inline bool is_iff(expr const & e) { return is_app(e) && is_iff_fn(arg(e, 0)); }
 /** \brief Return (e1 iff e2) */
 inline expr mk_iff(expr const & e1, expr const & e2) { return mk_app(mk_iff_fn(), e1, e2); }
-inline expr mk_iff(unsigned num_args, expr const * args) { return mk_bin_rop(mk_iff_fn(), True, num_args, args); }
 inline expr Iff(expr const & e1, expr const & e2) { return mk_iff(e1, e2); }
-inline expr Iff(std::initializer_list<expr> const & l) { return mk_iff(l.size(), l.begin()); }
 
 /** \brief Return the Lean And operator */
 expr mk_and_fn();
@@ -86,9 +68,7 @@ bool is_and_fn(expr const & e);
 inline bool is_and(expr const & e) { return is_app(e) && is_and_fn(arg(e, 0)); }
 /** \brief Return (e1 and e2) */
 inline expr mk_and(expr const & e1, expr const & e2) { return mk_app(mk_and_fn(), e1, e2); }
-inline expr mk_and(unsigned num_args, expr const * args) { return mk_bin_rop(mk_and_fn(), True, num_args, args); }
 inline expr And(expr const & e1, expr const & e2) { return mk_and(e1, e2); }
-inline expr And(std::initializer_list<expr> const & l) { return mk_and(l.size(), l.begin()); }
 
 /** \brief Return the Lean Or operator */
 expr mk_or_fn();
@@ -96,9 +76,7 @@ bool is_or_fn(expr const & e);
 inline bool is_or(expr const & e) { return is_app(e) && is_or_fn(arg(e, 0)); }
 /** \brief Return (e1 Or e2) */
 inline expr mk_or(expr const & e1, expr const & e2) { return mk_app(mk_or_fn(), e1, e2); }
-inline expr mk_or(unsigned num_args, expr const * args) { return mk_bin_rop(mk_or_fn(), False, num_args, args); }
 inline expr Or(expr const & e1, expr const & e2) { return mk_or(e1, e2); }
-inline expr Or(std::initializer_list<expr> const & l) { return mk_or(l.size(), l.begin()); }
 
 /** \brief Return the Lean not operator */
 expr mk_not_fn();

src/library/CMakeLists.txt

@@ -1,5 +1,5 @@
 add_library(library kernel_bindings.cpp basic_thms.cpp deep_copy.cpp
   max_sharing.cpp context_to_lambda.cpp io_state.cpp placeholder.cpp
-  expr_lt.cpp substitution.cpp fo_unify.cpp)
+  expr_lt.cpp substitution.cpp fo_unify.cpp bin_op.cpp)
 
 target_link_libraries(library ${LEAN_LIBS})

src/library/bin_op.cpp

@@ -0,0 +1,41 @@
+/*
+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

@@ -0,0 +1,36 @@
+/*
+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/builtin.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()); }
+
+inline expr mk_iff(unsigned num_args, expr const * args) { return mk_bin_rop(mk_iff_fn(), True, num_args, args); }
+inline expr Iff(std::initializer_list<expr> const & l) { return mk_iff(l.size(), l.begin()); }
+}

src/tests/frontends/lean/frontend.cpp

@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include "kernel/builtin.h"
 #include "kernel/abstract.h"
 #include "kernel/printer.h"
+#include "library/bin_op.h"
 #include "frontends/lean/frontend.h"
 #include "frontends/lean/operator_info.h"
 #include "frontends/lean/pp.h"

src/tests/kernel/expr.cpp

@@ -16,6 +16,7 @@ Author: Leonardo de Moura
 #include "kernel/instantiate.h"
 #include "kernel/printer.h"
 #include "library/max_sharing.h"
+#include "library/bin_op.h"
 #include "library/arith/arith.h"
 using namespace lean;