refactor(kernel/builtin): move helper decl macros to a separate file

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

src/kernel/builtin.cpp

@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include "kernel/environment.h"
 #include "kernel/abstract.h"
 #include "kernel/io_state.h"
+#include "kernel/decl_macros.h"
 
 namespace lean {
 // =======================================

src/kernel/builtin.h

@@ -219,33 +219,5 @@ inline expr ExistsElim(expr const & A, expr const & P, expr const & B, expr cons
 expr mk_exists_intro_fn();
 inline expr ExistsIntro(expr const & A, expr const & P, expr const & a, expr const & H) { return mk_app(mk_exists_intro_fn(), A, P, a, H); }
 
-/**
-   \brief Helper macro for defining constants such as bool_type, int_type, int_add, etc.
-*/
-#define MK_BUILTIN(Name, ClassName)                                     \
-expr mk_##Name() {                                                      \
-    static LEAN_THREAD_LOCAL expr r = mk_value(*(new ClassName()));     \
-    return r;                                                           \
-}
-
-/**
-   \brief Helper macro for generating "defined" constants.
-*/
-#define MK_CONSTANT(Name, NameObj)                                      \
-static name Name ## _name = NameObj;                                    \
-expr mk_##Name() {                                                      \
-    static LEAN_THREAD_LOCAL expr r = mk_constant(Name ## _name);       \
-    return r ;                                                          \
-}                                                                       \
-bool is_ ## Name(expr const & e) {                                      \
-    return is_constant(e) && const_name(e) == Name ## _name;            \
-}
-
-#define MK_IS_BUILTIN(Name, Builtin)                                    \
-bool Name(expr const & e) {                                             \
-    expr const & v = Builtin;                                           \
-    return e == v || (is_constant(e) && const_name(e) == to_value(v).get_name()); \
-}
-
 void import_kernel(environment const & env);
 }

src/kernel/decl_macros.h

@@ -0,0 +1,34 @@
+/*
+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
+/**
+   \brief Helper macro for defining constants such as bool_type, int_type, int_add, etc.
+*/
+#define MK_BUILTIN(Name, ClassName)                                     \
+expr mk_##Name() {                                                      \
+    static LEAN_THREAD_LOCAL expr r = mk_value(*(new ClassName()));     \
+    return r;                                                           \
+}
+
+/**
+   \brief Helper macro for generating "defined" constants.
+*/
+#define MK_CONSTANT(Name, NameObj)                                      \
+static name Name ## _name = NameObj;                                    \
+expr mk_##Name() {                                                      \
+    static LEAN_THREAD_LOCAL expr r = mk_constant(Name ## _name);       \
+    return r ;                                                          \
+}                                                                       \
+bool is_ ## Name(expr const & e) {                                      \
+    return is_constant(e) && const_name(e) == Name ## _name;            \
+}
+
+#define MK_IS_BUILTIN(Name, Builtin)                                    \
+bool Name(expr const & e) {                                             \
+    expr const & v = Builtin;                                           \
+    return e == v || (is_constant(e) && const_name(e) == to_value(v).get_name()); \
+}

src/library/arith/int.cpp

@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include "kernel/environment.h"
 #include "kernel/value.h"
 #include "kernel/io_state.h"
+#include "kernel/decl_macros.h"
 #include "library/kernel_bindings.h"
 #include "library/arith/int.h"
 #include "library/arith/nat.h"

src/library/arith/nat.cpp

@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include "kernel/environment.h"
 #include "kernel/value.h"
 #include "kernel/io_state.h"
+#include "kernel/decl_macros.h"
 #include "library/kernel_bindings.h"
 #include "library/arith/nat.h"
 

src/library/arith/real.cpp

@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include "kernel/environment.h"
 #include "kernel/value.h"
 #include "kernel/io_state.h"
+#include "kernel/decl_macros.h"
 #include "library/kernel_bindings.h"
 #include "library/arith/real.h"
 #include "library/arith/int.h"