refactor(kernel/builtin): move builtin declarations to basic

There is a lot to be done. We should do the same for Nat, Int and Real.
We also should cleanup the file builtin.cpp and builtin.h.

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

src/builtin/basic.lean

@@ -1,5 +1,14 @@
 Import macros
 
+Universe M : 512.
+Universe U : M+512.
+
+Variable Bool : Type.
+(* The following builtin declarations can be removed as soon as Lean supports inductive datatypes and match expressions. *)
+Builtin true : Bool.
+Builtin false : Bool.
+Builtin if {A : (Type U)} : Bool → A → A → A.
+
 Definition TypeU := (Type U)
 Definition TypeM := (Type M)
 

src/frontends/lean/frontend.cpp

@@ -559,9 +559,7 @@ static lean_extension & to_ext(environment const & env) {
 */
 void init_frontend(environment const & env, io_state & ios, bool kernel_only) {
     ios.set_formatter(mk_pp_formatter(env));
-    if (kernel_only)
-        import_kernel(env);
-    else
+    if (!kernel_only)
         import_all(env);
     init_builtin_notation(env, ios, kernel_only);
 }

src/frontends/lean/notation.cpp

@@ -17,7 +17,7 @@ void init_builtin_notation(environment const & env, io_state & ios, bool kernel_
     env->import_builtin(
         "lean_notation",
         [&]() {
-            mark_implicit_arguments(env, mk_if_fn(), 1);
+            // mark_implicit_arguments(env, mk_if_fn(), 1);
 
 
             if (kernel_only)

src/frontends/lean/parser.cpp

@@ -106,6 +106,7 @@ static name g_push_kwd("Push");
 static name g_pop_kwd("Pop");
 static name g_scope_kwd("Scope");
 static name g_end_scope_kwd("EndScope");
+static name g_builtin_kwd("Builtin");
 static name g_apply("apply");
 static name g_done("done");
 static name g_back("back");
@@ -116,7 +117,7 @@ static list<name> g_tactic_cmds = { g_apply, g_done, g_back, g_abort, g_assumpti
 static list<name> g_command_keywords = {g_definition_kwd, g_variable_kwd, g_variables_kwd, g_theorem_kwd, g_axiom_kwd, g_universe_kwd, g_eval_kwd,
                                         g_show_kwd, g_check_kwd, g_infix_kwd, g_infixl_kwd, g_infixr_kwd, g_notation_kwd, g_echo_kwd,
                                         g_set_option_kwd, g_set_opaque_kwd, g_env_kwd, g_options_kwd, g_import_kwd, g_help_kwd, g_coercion_kwd,
-                                        g_exit_kwd, g_push_kwd, g_pop_kwd, g_scope_kwd, g_end_scope_kwd, g_alias_kwd};
+                                        g_exit_kwd, g_push_kwd, g_pop_kwd, g_scope_kwd, g_end_scope_kwd, g_alias_kwd, g_builtin_kwd};
 // ==========================================
 
 // ==========================================
@@ -2554,6 +2555,7 @@ class parser::imp {
     void parse_universe() {
         next();
         name id   = check_identifier_next("invalid universe declaration, identifier expected");
+        check_colon_next("invalid universe declaration, ':' expected");
         level lvl = parse_level();
         m_env->add_uvar(id, lvl);
     }
@@ -2566,6 +2568,44 @@ class parser::imp {
         add_alias(m_env, id, e);
     }
 
+    void parse_builtin() {
+        next();
+        auto id_pos = pos();
+        name id = check_identifier_next("invalid builtin declaration, identifier expected");
+        auto d  = get_builtin(id);
+        if (!d)
+            throw parser_error(sstream() << "unknown builtin '" << id << "'", id_pos);
+        expr b = d->first;
+        if (d->second) {
+            m_env->add_builtin_set(b);
+            return;
+        }
+        bindings_buffer bindings;
+        expr type;
+        if (curr_is_colon()) {
+            next();
+            auto p = m_elaborator(parse_expr());
+            check_no_metavar(p, "invalid builtin declaration, type still contains metavariables after elaboration");
+            type = p.first;
+        } else {
+            mk_scope scope(*this);
+            parse_var_decl_bindings(bindings);
+            check_colon_next("invalid builtin declaration, ':' expected");
+            expr type_body = parse_expr();
+            auto p = m_elaborator(mk_abstraction(false, bindings, type_body));
+            check_no_metavar(p, "invalid declaration, type still contains metavariables after elaboration");
+            type = p.first;
+        }
+        if (to_value(b).get_type() != type) {
+            diagnostic(m_io_state) << "Error, builtin expected type: " << to_value(b).get_type() << ", given: " << type << "\n";
+            throw parser_error(sstream() << "given type does not match builtin type", id_pos);
+        }
+        m_env->add_builtin(d->first);
+        if (m_verbose)
+            regular(m_io_state) << "  Added: " << id << endl;
+        register_implicit_arguments(id, bindings);
+    }
+
     /** \brief Parse a Lean command. */
     bool parse_command() {
         m_elaborator.clear();
@@ -2622,6 +2662,8 @@ class parser::imp {
             parse_universe();
         } else if (cmd_id == g_alias_kwd) {
             parse_alias();
+        } else if (cmd_id == g_builtin_kwd) {
+            parse_builtin();
         } else if (m_cmd_macros && m_cmd_macros->find(cmd_id) != m_cmd_macros->end()) {
             parse_cmd_macro(cmd_id, m_last_cmd_pos);
         } else {

src/kernel/builtin.cpp

@@ -59,6 +59,8 @@ public:
 };
 expr const True  = mk_value(*(new bool_value_value(true)));
 expr const False = mk_value(*(new bool_value_value(false)));
+register_available_builtin_fn g_true_value("true", []() { return  True; });
+register_available_builtin_fn g_false_value("false", []() { return False; });
 expr read_true(deserializer & ) { return True; }
 expr read_false(deserializer & ) { return False; }
 static value::register_deserializer_fn true_ds("true", read_true);
@@ -114,6 +116,7 @@ public:
     virtual void write(serializer & s) const { s << "if"; }
 };
 MK_BUILTIN(if_fn, if_fn_value);
+register_available_builtin_fn g_if_value("if", []() { return mk_if_fn(); });
 expr read_if(deserializer & ) { return mk_if_fn(); }
 static value::register_deserializer_fn if_ds("if", read_if);
 MK_IS_BUILTIN(is_if_fn, mk_if_fn());
@@ -139,17 +142,4 @@ MK_CONSTANT(abst_fn,        name("Abst"));
 
 MK_CONSTANT(htrans_fn,      name("HTrans"));
 MK_CONSTANT(hsymm_fn,       name("HSymm"));
-
-void import_kernel(environment const & env) {
-    env->import_builtin
-        ("kernel",
-         [&]() {
-            env->add_var(Bool_name, Type());
-            env->add_uvar(uvar_name(m_lvl), level() + LEAN_DEFAULT_LEVEL_SEPARATION);
-            env->add_uvar(uvar_name(u_lvl), m_lvl + LEAN_DEFAULT_LEVEL_SEPARATION);
-            env->add_builtin(mk_bool_value(true));
-            env->add_builtin(mk_bool_value(false));
-            env->add_builtin(mk_if_fn());
-        });
-}
 }

src/kernel/builtin.h

@@ -164,10 +164,6 @@ inline expr HTrans(expr const & A, expr const & B, expr const & C, expr const &
     return mk_app({mk_htrans_fn(), A, B, C, a, b, c, H1, H2});
 }
 
-class environment;
-/** \brief Initialize the environment with basic builtin declarations and axioms */
-void import_kernel(environment const & env);
-
 /**
    \brief Helper macro for defining constants such as bool_type, int_type, int_add, etc.
 */

src/kernel/environment.cpp

@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include <tuple>
 #include <fstream>
 #include <string>
+#include <utility>
 #include "util/thread.h"
 #include "util/safe_arith.h"
 #include "util/realpath.h"
@@ -380,7 +381,9 @@ void environment_cell::add_builtin(expr const & v) {
     check_name(u);
     register_named_object(mk_builtin(v));
     if (u != n) {
-        add_definition(u, to_value(v).get_type(), mk_constant(n), false);
+        auxiliary_section([&]() {
+                add_definition(u, to_value(v).get_type(), mk_constant(n), false);
+            });
     }
 }
 
@@ -701,4 +704,26 @@ read_write_shared_environment::read_write_shared_environment(environment const &
     m_lock(m_env.m_ptr->m_mutex) {
 }
 read_write_shared_environment::~read_write_shared_environment() {}
+
+static std::unique_ptr<name_map<std::pair<mk_builtin_fn, bool>>> g_available_builtins;
+name_map<std::pair<mk_builtin_fn, bool>> & get_available_builtins() {
+    if (!g_available_builtins)
+        g_available_builtins.reset(new name_map<std::pair<mk_builtin_fn, bool>>());
+    return *g_available_builtins;
+}
+
+void register_available_builtin(name const & n, mk_builtin_fn mk, bool is_builtin_set) {
+    auto & bs = get_available_builtins();
+    if (bs.find(n) != bs.end())
+        throw exception("invalid builtin object, system already has a builtin object with the given name");
+    bs[n] = mk_pair(mk, is_builtin_set);
+}
+
+optional<std::pair<expr, bool>> get_builtin(name const & n) {
+    auto it = get_available_builtins().find(n);
+    if (it != get_available_builtins().end())
+        return optional<std::pair<expr, bool>>(it->second.first(), it->second.second);
+    else
+        return optional<std::pair<expr, bool>>();
+}
 }

src/kernel/environment.h

@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include <vector>
 #include <set>
 #include <string>
+#include <utility>
 #include "util/lua.h"
 #include "util/shared_mutex.h"
 #include "util/name_map.h"
@@ -411,4 +412,21 @@ bool is_end_import(object const & obj);
     Return none if \c obj is not an import object.
 */
 optional<std::string> get_imported_module(object const & obj);
+
+typedef std::function<expr()> mk_builtin_fn;
+/**
+   \brief Register a builtin or builtin-set that is available to be added to
+   a Lean environment.
+*/
+void register_available_builtin(name const & n, mk_builtin_fn mk, bool is_builtin_set);
+struct register_available_builtin_fn {
+    register_available_builtin_fn(name const & n, mk_builtin_fn mk, bool is_builtin_set = false) {
+        register_available_builtin(n, mk, is_builtin_set);
+    }
+};
+/**
+   \brief Return a builtin/builtin-set associated with the name \c n.
+   Return none if there is no builtin associated the given name.
+*/
+optional<std::pair<expr, bool>> get_builtin(name const & n);
 }

src/library/all/all.cpp

@@ -11,7 +11,6 @@ Author: Leonardo de Moura
 
 namespace lean {
 void import_all(environment const & env) {
-    import_kernel(env);
     import_basic_thms(env);
     import_arith(env);
 }