michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

chore(*): cleanup builtin registration

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-30 12:19:00 -08:00
parent 2a2f0b0d89
commit a80fccea93
7 changed files with 47 additions and 71 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/kernel/builtin.cpp
View file

@ -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"));

2
src/kernel/environment.cpp
View file

@ -712,7 +712,7 @@ name_map<std::pair<mk_builtin_fn, bool>> & 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");

8
src/kernel/environment.h
View file

@ -418,10 +418,10 @@ 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);
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);
}
};
/**

2
src/kernel/expr.h
View file

@ -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<expr(deserializer&)> 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); }

30
src/library/arith/int.cpp
View file

@ -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<int_value_value const *>(&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_name, int_add_eval> 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_name, int_mul_eval> 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_name, int_div_eval> 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"}));

20
src/library/arith/nat.cpp
View file

@ -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<nat_value_value const *>(&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_name, nat_add_eval> 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_name, nat_mul_eval> 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"}));

40
src/library/arith/real.cpp
View file

@ -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<real_value_value const *>(&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<real_value_value const *>(&to_value(e)) != nullptr; }
mpq const & real_value_numeral(expr const & e) {
lean_assert(is_real_value(e));
return static_cast<real_value_value const &>(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_name, real_add_eval> 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_name, real_mul_eval> 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_name, real_div_eval> 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"}));