diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp index 596660b00..3085662f9 100644 --- a/src/kernel/builtin.cpp +++ b/src/kernel/builtin.cpp @@ -61,8 +61,8 @@ expr const True = mk_value(*(new bool_value_value(true))); expr const False = mk_value(*(new bool_value_value(false))); expr read_true(deserializer & ) { return True; } expr read_false(deserializer & ) { return False; } -static register_deserializer_fn true_ds("true", read_true); -static register_deserializer_fn false_ds("false", read_false); +static value::register_deserializer_fn true_ds("true", read_true); +static value::register_deserializer_fn false_ds("false", read_false); expr mk_bool_value(bool v) { return v ? True : False; } @@ -115,7 +115,7 @@ public: }; MK_BUILTIN(if_fn, if_fn_value); expr read_if(deserializer & ) { return mk_if_fn(); } -static register_deserializer_fn if_ds("if", read_if); +static value::register_deserializer_fn if_ds("if", read_if); MK_IS_BUILTIN(is_if_fn, mk_if_fn()); // ======================================= diff --git a/src/kernel/expr.h b/src/kernel/expr.h index 7482ff925..55d349bc1 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -301,9 +301,9 @@ public: virtual void write(serializer & s) const = 0; typedef expr (*reader)(deserializer & d); 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); } + struct register_deserializer_fn { + register_deserializer_fn(std::string const & k, value::reader rd) { value::register_deserializer(k, rd); } + }; }; /** \brief Semantic attachments */ diff --git a/src/kernel/value.h b/src/kernel/value.h index ef100844a..0ad7336a1 100644 --- a/src/kernel/value.h +++ b/src/kernel/value.h @@ -30,14 +30,4 @@ public: virtual ~const_value() {} virtual expr get_type() const { return m_type; } }; - -/** - \brief Base class for values that have a hierarchical name attached to it, and - have type Type(). -*/ -class type_value : public named_value { -public: - type_value(name const & n):named_value(n) {} - virtual expr get_type() const { return Type(); } -}; } diff --git a/src/library/arith/int.cpp b/src/library/arith/int.cpp index a08b0a8de..e41461612 100644 --- a/src/library/arith/int.cpp +++ b/src/library/arith/int.cpp @@ -50,7 +50,7 @@ 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 register_deserializer_fn int_value_ds("int", read_int_value); +static value::register_deserializer_fn int_value_ds("int", read_int_value); bool is_int_value(expr const & e) { return is_value(e) && dynamic_cast(&to_value(e)) != nullptr; @@ -84,14 +84,14 @@ struct int_add_eval { mpz operator()(mpz const & v1, mpz const & v2) { return v1 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 register_deserializer_fn int_add_ds("int_add", read_int_add); +static value::register_deserializer_fn int_add_ds("int_add", read_int_add); 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 register_deserializer_fn int_mul_ds("int_mul", read_int_mul); +static value::register_deserializer_fn int_mul_ds("int_mul", read_int_mul); constexpr char int_div_name[] = "div"; struct int_div_eval { @@ -105,7 +105,7 @@ 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 register_deserializer_fn int_div_ds("int_div", read_int_div); +static value::register_deserializer_fn int_div_ds("int_div", read_int_div); class int_le_value : public const_value { public: @@ -121,7 +121,7 @@ public: }; MK_BUILTIN(int_le_fn, int_le_value); expr read_int_le(deserializer & ) { return mk_int_le_fn(); } -static register_deserializer_fn int_le_ds("int_le", read_int_le); +static value::register_deserializer_fn int_le_ds("int_le", read_int_le); MK_CONSTANT(int_sub_fn, name({"Int", "sub"})); MK_CONSTANT(int_neg_fn, name({"Int", "neg"})); @@ -149,7 +149,7 @@ public: }; MK_BUILTIN(nat_to_int_fn, nat_to_int_value); expr read_nat_to_int(deserializer & ) { return mk_nat_to_int_fn(); } -static register_deserializer_fn nat_to_int_ds("nat_to_int", read_nat_to_int); +static value::register_deserializer_fn nat_to_int_ds("nat_to_int", read_nat_to_int); 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 e42e59453..16b2abf1e 100644 --- a/src/library/arith/nat.cpp +++ b/src/library/arith/nat.cpp @@ -43,7 +43,7 @@ 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 register_deserializer_fn nat_value_ds("nat", read_nat_value); +static value::register_deserializer_fn nat_value_ds("nat", read_nat_value); bool is_nat_value(expr const & e) { return is_value(e) && dynamic_cast(&to_value(e)) != nullptr; @@ -78,7 +78,7 @@ struct nat_add_eval { mpz operator()(mpz const & v1, mpz const & v2) { return v1 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 register_deserializer_fn nat_add_ds("nat_add", read_nat_add); +static value::register_deserializer_fn nat_add_ds("nat_add", read_nat_add); constexpr char nat_mul_name[] = "mul"; /** \brief Evaluator for * : Nat -> Nat -> Nat */ @@ -86,7 +86,7 @@ struct nat_mul_eval { mpz operator()(mpz const & v1, mpz const & v2) { return v1 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 register_deserializer_fn nat_mul_ds("nat_mul", read_nat_mul); +static value::register_deserializer_fn nat_mul_ds("nat_mul", read_nat_mul); /** \brief Semantic attachment for less than or equal to operator with type @@ -106,7 +106,7 @@ public: }; MK_BUILTIN(nat_le_fn, nat_le_value); expr read_nat_le(deserializer & ) { return mk_nat_le_fn(); } -static register_deserializer_fn nat_le_ds("nat_le", read_nat_le); +static value::register_deserializer_fn nat_le_ds("nat_le", read_nat_le); 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 22ec0cab0..be8d56b7b 100644 --- a/src/library/arith/real.cpp +++ b/src/library/arith/real.cpp @@ -56,7 +56,7 @@ 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 register_deserializer_fn real_value_ds("real", read_real_value); +static value::register_deserializer_fn real_value_ds("real", read_real_value); bool is_real_value(expr const & e) { return is_value(e) && dynamic_cast(&to_value(e)) != nullptr; @@ -91,7 +91,7 @@ struct real_add_eval { mpq operator()(mpq const & v1, mpq const & v2) { return v 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 register_deserializer_fn real_add_ds("real_add", read_real_add); +static value::register_deserializer_fn real_add_ds("real_add", read_real_add); constexpr char real_mul_name[] = "mul"; /** \brief Evaluator for * : Real -> Real -> Real */ @@ -99,7 +99,7 @@ struct real_mul_eval { mpq operator()(mpq const & v1, mpq const & v2) { return v 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 register_deserializer_fn real_mul_ds("real_mul", read_real_mul); +static value::register_deserializer_fn real_mul_ds("real_mul", read_real_mul); constexpr char real_div_name[] = "div"; /** \brief Evaluator for / : Real -> Real -> Real */ @@ -114,7 +114,7 @@ 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 register_deserializer_fn real_div_ds("real_div", read_real_div); +static value::register_deserializer_fn real_div_ds("real_div", read_real_div); /** \brief Semantic attachment for less than or equal to operator with type @@ -134,7 +134,7 @@ public: }; MK_BUILTIN(real_le_fn, real_le_value); expr read_real_le(deserializer & ) { return mk_real_le_fn(); } -static register_deserializer_fn real_le_ds("real_le", read_real_le); +static value::register_deserializer_fn real_le_ds("real_le", read_real_le); MK_CONSTANT(real_sub_fn, name({"Real", "sub"})); MK_CONSTANT(real_neg_fn, name({"Real", "neg"})); @@ -183,7 +183,7 @@ public: }; MK_BUILTIN(int_to_real_fn, int_to_real_value); expr read_int_to_real(deserializer & ) { return mk_int_to_real_fn(); } -static register_deserializer_fn int_to_real_ds("int_to_real", read_int_to_real); +static value::register_deserializer_fn int_to_real_ds("int_to_real", read_int_to_real); MK_CONSTANT(nat_to_real_fn, name("nat_to_real")); void import_int_to_real_coercions(environment const & env) {