diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp index 432a2d6f8..1a3a53ef8 100644 --- a/src/kernel/builtin.cpp +++ b/src/kernel/builtin.cpp @@ -57,12 +57,11 @@ 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); -static value::register_deserializer_fn false_ds("false", read_false); +static register_builtin_fn true_blt("true", []() { return True; }); +static register_builtin_fn false_blt("false", []() { return False; }); +static value::register_deserializer_fn true_ds("true", [](deserializer & ) { return True; }); +static value::register_deserializer_fn false_ds("false", [](deserializer & ) { return False; }); + expr mk_bool_value(bool v) { return v ? True : False; } @@ -114,10 +113,9 @@ 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()); +static register_builtin_fn if_blt("if", []() { return mk_if_fn(); }); +static value::register_deserializer_fn if_ds("if", [](deserializer & ) { return mk_if_fn(); }); // ======================================= MK_CONSTANT(implies_fn, name("implies")); diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index 49b668ec1..360ab3174 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -712,7 +712,7 @@ name_map> & get_available_builtins() { return *g_available_builtins; } -void register_available_builtin(name const & n, mk_builtin_fn mk, bool is_builtin_set) { +void register_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"); diff --git a/src/kernel/environment.h b/src/kernel/environment.h index a9b0972fd..d5459a713 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -418,10 +418,10 @@ typedef std::function 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); +void register_builtin(name const & n, mk_builtin_fn mk, bool is_builtin_set); +struct register_builtin_fn { + register_builtin_fn(name const & n, mk_builtin_fn mk, bool is_builtin_set = false) { + register_builtin(n, mk, is_builtin_set); } }; /** diff --git a/src/kernel/expr.h b/src/kernel/expr.h index 55d349bc1..560cda622 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -299,7 +299,7 @@ public: virtual int push_lua(lua_State * L) const; virtual unsigned hash() const; virtual void write(serializer & s) const = 0; - typedef expr (*reader)(deserializer & d); + typedef std::function reader; static void register_deserializer(std::string const & k, reader rd); struct register_deserializer_fn { register_deserializer_fn(std::string const & k, value::reader rd) { value::register_deserializer(k, rd); } diff --git a/src/library/arith/int.cpp b/src/library/arith/int.cpp index 4d3d0c6f9..6bb713cd4 100644 --- a/src/library/arith/int.cpp +++ b/src/library/arith/int.cpp @@ -51,9 +51,8 @@ public: expr mk_int_value(mpz const & v) { return mk_value(*(new int_value_value(v))); } -expr read_int_value(deserializer & d) { return mk_int_value(read_mpz(d)); } -static value::register_deserializer_fn int_value_ds("int", read_int_value); -static register_available_builtin_fn g_int_value(name({"Int", "numeral"}), []() { return mk_int_value(mpz(0)); }, true); +static value::register_deserializer_fn int_value_ds("int", [](deserializer & d) { return mk_int_value(read_mpz(d)); }); +static register_builtin_fn int_value_blt(name({"Int", "numeral"}), []() { return mk_int_value(mpz(0)); }, true); bool is_int_value(expr const & e) { return is_value(e) && dynamic_cast(&to_value(e)) != nullptr; @@ -86,17 +85,15 @@ constexpr char int_add_name[] = "add"; struct int_add_eval { mpz operator()(mpz const & v1, mpz const & v2) { return v1 + v2; }; }; typedef int_bin_op int_add_value; MK_BUILTIN(int_add_fn, int_add_value); -expr read_int_add(deserializer & ) { return mk_int_add_fn(); } -static value::register_deserializer_fn int_add_ds("int_add", read_int_add); -static register_available_builtin_fn g_int_add_value(name({"Int", "add"}), []() { return mk_int_add_fn(); }); +static value::register_deserializer_fn int_add_ds("int_add", [](deserializer & ) { return mk_int_add_fn(); }); +static register_builtin_fn g_int_add_value(name({"Int", "add"}), []() { return mk_int_add_fn(); }); constexpr char int_mul_name[] = "mul"; struct int_mul_eval { mpz operator()(mpz const & v1, mpz const & v2) { return v1 * v2; }; }; typedef int_bin_op int_mul_value; MK_BUILTIN(int_mul_fn, int_mul_value); -expr read_int_mul(deserializer & ) { return mk_int_mul_fn(); } -static value::register_deserializer_fn int_mul_ds("int_mul", read_int_mul); -static register_available_builtin_fn g_int_mul_value(name({"Int", "mul"}), []() { return mk_int_mul_fn(); }); +static value::register_deserializer_fn int_mul_ds("int_mul", [](deserializer & ) { return mk_int_mul_fn(); }); +static register_builtin_fn int_mul_blt(name({"Int", "mul"}), []() { return mk_int_mul_fn(); }); constexpr char int_div_name[] = "div"; struct int_div_eval { @@ -109,9 +106,8 @@ struct int_div_eval { }; typedef int_bin_op int_div_value; MK_BUILTIN(int_div_fn, int_div_value); -expr read_int_div(deserializer & ) { return mk_int_div_fn(); } -static value::register_deserializer_fn int_div_ds("int_div", read_int_div); -static register_available_builtin_fn g_int_div_value(name({"Int", "div"}), []() { return mk_int_div_fn(); }); +static value::register_deserializer_fn int_div_ds("int_div", [](deserializer & ) { return mk_int_div_fn(); }); +static register_builtin_fn int_div_blt(name({"Int", "div"}), []() { return mk_int_div_fn(); }); class int_le_value : public const_value { public: @@ -126,9 +122,8 @@ public: virtual void write(serializer & s) const { s << "int_le"; } }; MK_BUILTIN(int_le_fn, int_le_value); -expr read_int_le(deserializer & ) { return mk_int_le_fn(); } -static value::register_deserializer_fn int_le_ds("int_le", read_int_le); -static register_available_builtin_fn g_int_le_value(name({"Int", "le"}), []() { return mk_int_le_fn(); }); +static value::register_deserializer_fn int_le_ds("int_le", [](deserializer & ) { return mk_int_le_fn(); }); +static register_builtin_fn int_le_blt(name({"Int", "le"}), []() { return mk_int_le_fn(); }); MK_CONSTANT(int_sub_fn, name({"Int", "sub"})); MK_CONSTANT(int_neg_fn, name({"Int", "neg"})); @@ -155,9 +150,8 @@ public: virtual void write(serializer & s) const { s << "nat_to_int"; } }; MK_BUILTIN(nat_to_int_fn, nat_to_int_value); -expr read_nat_to_int(deserializer & ) { return mk_nat_to_int_fn(); } -static value::register_deserializer_fn nat_to_int_ds("nat_to_int", read_nat_to_int); -register_available_builtin_fn g_n2i_value(name({"nat_to_int"}), []() { return mk_nat_to_int_fn(); }); +static value::register_deserializer_fn nat_to_int_ds("nat_to_int", [](deserializer & ) { return mk_nat_to_int_fn(); }); +static register_builtin_fn nat_to_int_blt("nat_to_int", []() { return mk_nat_to_int_fn(); }); MK_CONSTANT(nat_sub_fn, name({"Nat", "sub"})); MK_CONSTANT(nat_neg_fn, name({"Nat", "neg"})); diff --git a/src/library/arith/nat.cpp b/src/library/arith/nat.cpp index 933ac9b98..3efa2cb2e 100644 --- a/src/library/arith/nat.cpp +++ b/src/library/arith/nat.cpp @@ -44,9 +44,8 @@ public: expr mk_nat_value(mpz const & v) { return mk_value(*(new nat_value_value(v))); } -expr read_nat_value(deserializer & d) { return mk_nat_value(read_mpz(d)); } -static value::register_deserializer_fn nat_value_ds("nat", read_nat_value); -register_available_builtin_fn g_nat_value(name({"Nat", "numeral"}), []() { return mk_nat_value(mpz(0)); }, true); +static value::register_deserializer_fn nat_value_ds("nat", [](deserializer & d) { return mk_nat_value(read_mpz(d)); }); +static register_builtin_fn nat_value_blt(name({"Nat", "numeral"}), []() { return mk_nat_value(mpz(0)); }, true); bool is_nat_value(expr const & e) { return is_value(e) && dynamic_cast(&to_value(e)) != nullptr; @@ -80,18 +79,16 @@ constexpr char nat_add_name[] = "add"; struct nat_add_eval { mpz operator()(mpz const & v1, mpz const & v2) { return v1 + v2; }; }; typedef nat_bin_op nat_add_value; MK_BUILTIN(nat_add_fn, nat_add_value); -expr read_nat_add(deserializer & ) { return mk_nat_add_fn(); } -static value::register_deserializer_fn nat_add_ds("nat_add", read_nat_add); -register_available_builtin_fn g_nat_add_value(name({"Nat", "add"}), []() { return mk_nat_add_fn(); }); +static value::register_deserializer_fn nat_add_ds("nat_add", [](deserializer & ) { return mk_nat_add_fn(); }); +static register_builtin_fn nat_add_blt(name({"Nat", "add"}), []() { return mk_nat_add_fn(); }); constexpr char nat_mul_name[] = "mul"; /** \brief Evaluator for * : Nat -> Nat -> Nat */ struct nat_mul_eval { mpz operator()(mpz const & v1, mpz const & v2) { return v1 * v2; }; }; typedef nat_bin_op nat_mul_value; MK_BUILTIN(nat_mul_fn, nat_mul_value); -expr read_nat_mul(deserializer & ) { return mk_nat_mul_fn(); } -static value::register_deserializer_fn nat_mul_ds("nat_mul", read_nat_mul); -register_available_builtin_fn g_nat_mul_value(name({"Nat", "mul"}), []() { return mk_nat_mul_fn(); }); +static value::register_deserializer_fn nat_mul_ds("nat_mul", [](deserializer & ) { return mk_nat_mul_fn(); }); +static register_builtin_fn nat_mul_blt(name({"Nat", "mul"}), []() { return mk_nat_mul_fn(); }); /** \brief Semantic attachment for less than or equal to operator with type @@ -110,9 +107,8 @@ public: virtual void write(serializer & s) const { s << "nat_le"; } }; MK_BUILTIN(nat_le_fn, nat_le_value); -expr read_nat_le(deserializer & ) { return mk_nat_le_fn(); } -static value::register_deserializer_fn nat_le_ds("nat_le", read_nat_le); -register_available_builtin_fn g_nat_le_value(name({"Nat", "le"}), []() { return mk_nat_le_fn(); }); +static value::register_deserializer_fn nat_le_ds("nat_le", [](deserializer & ) { return mk_nat_le_fn(); }); +static register_builtin_fn nat_le_blt(name({"Nat", "le"}), []() { return mk_nat_le_fn(); }); MK_CONSTANT(nat_ge_fn, name({"Nat", "ge"})); MK_CONSTANT(nat_lt_fn, name({"Nat", "lt"})); diff --git a/src/library/arith/real.cpp b/src/library/arith/real.cpp index d8fea49ee..b06c06a51 100644 --- a/src/library/arith/real.cpp +++ b/src/library/arith/real.cpp @@ -54,21 +54,14 @@ public: virtual void write(serializer & s) const { s << "real" << m_val; } }; -expr mk_real_value(mpq const & v) { - return mk_value(*(new real_value_value(v))); -} -expr read_real_value(deserializer & d) { return mk_real_value(read_mpq(d)); } -static value::register_deserializer_fn real_value_ds("real", read_real_value); -static register_available_builtin_fn g_real_value(name({"Real", "numeral"}), []() { return mk_real_value(mpq(0)); }, true); - -bool is_real_value(expr const & e) { - return is_value(e) && dynamic_cast(&to_value(e)) != nullptr; -} - +expr mk_real_value(mpq const & v) { return mk_value(*(new real_value_value(v))); } +bool is_real_value(expr const & e) { return is_value(e) && dynamic_cast(&to_value(e)) != nullptr; } mpq const & real_value_numeral(expr const & e) { lean_assert(is_real_value(e)); return static_cast(to_value(e)).get_num(); } +static value::register_deserializer_fn real_value_ds("real", [](deserializer & d) { return mk_real_value(read_mpq(d)); }); +static register_builtin_fn real_value_blt(name({"Real", "numeral"}), []() { return mk_real_value(mpq(0)); }, true); /** \brief Template for semantic attachments that are binary operators of @@ -93,9 +86,8 @@ constexpr char real_add_name[] = "add"; struct real_add_eval { mpq operator()(mpq const & v1, mpq const & v2) { return v1 + v2; }; }; typedef real_bin_op real_add_value; MK_BUILTIN(real_add_fn, real_add_value); -expr read_real_add(deserializer & ) { return mk_real_add_fn(); } -static value::register_deserializer_fn real_add_ds("real_add", read_real_add); -static register_available_builtin_fn g_real_add_value(name({"Real", "add"}), []() { return mk_real_add_fn(); }); +static value::register_deserializer_fn real_add_ds("real_add", [](deserializer & ) { return mk_real_add_fn(); }); +static register_builtin_fn real_add_blt(name({"Real", "add"}), []() { return mk_real_add_fn(); }); constexpr char real_mul_name[] = "mul"; @@ -103,9 +95,8 @@ constexpr char real_mul_name[] = "mul"; struct real_mul_eval { mpq operator()(mpq const & v1, mpq const & v2) { return v1 * v2; }; }; typedef real_bin_op real_mul_value; MK_BUILTIN(real_mul_fn, real_mul_value); -expr read_real_mul(deserializer & ) { return mk_real_mul_fn(); } -static value::register_deserializer_fn real_mul_ds("real_mul", read_real_mul); -static register_available_builtin_fn g_real_mul_value(name({"Real", "mul"}), []() { return mk_real_mul_fn(); }); +static value::register_deserializer_fn real_mul_ds("real_mul", [](deserializer & ) { return mk_real_mul_fn(); }); +static register_builtin_fn real_mul_blt(name({"Real", "mul"}), []() { return mk_real_mul_fn(); }); constexpr char real_div_name[] = "div"; /** \brief Evaluator for / : Real -> Real -> Real */ @@ -119,9 +110,8 @@ struct real_div_eval { }; typedef real_bin_op real_div_value; MK_BUILTIN(real_div_fn, real_div_value); -expr read_real_div(deserializer & ) { return mk_real_div_fn(); } -static value::register_deserializer_fn real_div_ds("real_div", read_real_div); -static register_available_builtin_fn g_real_div_value(name({"Real", "div"}), []() { return mk_real_div_fn(); }); +static value::register_deserializer_fn real_div_ds("real_div", [](deserializer & ) { return mk_real_div_fn(); }); +static register_builtin_fn real_div_blt(name({"Real", "div"}), []() { return mk_real_div_fn(); }); /** \brief Semantic attachment for less than or equal to operator with type @@ -140,9 +130,8 @@ public: virtual void write(serializer & s) const { s << "real_le"; } }; MK_BUILTIN(real_le_fn, real_le_value); -expr read_real_le(deserializer & ) { return mk_real_le_fn(); } -static value::register_deserializer_fn real_le_ds("real_le", read_real_le); -static register_available_builtin_fn g_real_le_value(name({"Real", "le"}), []() { return mk_real_le_fn(); }); +static value::register_deserializer_fn real_le_ds("real_le", [](deserializer & ) { return mk_real_le_fn(); }); +static register_builtin_fn real_le_btl(name({"Real", "le"}), []() { return mk_real_le_fn(); }); class int_to_real_value : public const_value { public: @@ -157,9 +146,8 @@ public: virtual void write(serializer & s) const { s << "int_to_real"; } }; MK_BUILTIN(int_to_real_fn, int_to_real_value); -expr read_int_to_real(deserializer & ) { return mk_int_to_real_fn(); } -static value::register_deserializer_fn int_to_real_ds("int_to_real", read_int_to_real); -static register_available_builtin_fn g_int_to_real_value("int_to_real", []() { return mk_int_to_real_fn(); }); +static value::register_deserializer_fn int_to_real_ds("int_to_real", [](deserializer & ) { return mk_int_to_real_fn(); }); +static register_builtin_fn int_to_real_blt("int_to_real", []() { return mk_int_to_real_fn(); }); MK_CONSTANT(real_sub_fn, name({"Real", "sub"})); MK_CONSTANT(real_neg_fn, name({"Real", "neg"}));