diff --git a/src/tests/util/numerics/mpq.cpp b/src/tests/util/numerics/mpq.cpp index c862435f7..8f025d736 100644 --- a/src/tests/util/numerics/mpq.cpp +++ b/src/tests/util/numerics/mpq.cpp @@ -7,6 +7,7 @@ Author: Leonardo de Moura #include #include #include "util/test.h" +#include "util/serializer.h" #include "util/numerics/mpq.h" using namespace lean; @@ -173,6 +174,27 @@ static void tst6() { lean_assert(cmp(mpq(-3, 2), mpz(-1)) < 0); } +static void tst7() { + std::ostringstream out; + serializer s(out); + mpq n1("-100000000000000000000000000000000000/3"); + lean_assert(n1.is_neg()); + mpq n2("-3/4"); + mpq n3("1200/2131"); + mpq n4("321/345"); + mpq n5(1, 3); + s << n1 << n2 << n3 << n4 << n5; + std::istringstream in(out.str()); + deserializer d(in); + mpq m1, m2, m3, m4, m5; + d >> m1 >> m2 >> m3 >> m4 >> m5; + lean_assert(n1 == m1); + lean_assert(n2 == m2); + lean_assert(n3 == m3); + lean_assert(n4 == m4); + lean_assert(n5 == m5); +} + int main() { tst0(); tst1(); @@ -181,5 +203,6 @@ int main() { tst4(); tst5(); tst6(); + tst7(); return has_violations() ? 1 : 0; } diff --git a/src/tests/util/numerics/mpz.cpp b/src/tests/util/numerics/mpz.cpp index 0efe6fa22..3b07b7a1b 100644 --- a/src/tests/util/numerics/mpz.cpp +++ b/src/tests/util/numerics/mpz.cpp @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include #include #include "util/test.h" +#include "util/serializer.h" #include "util/numerics/mpz.h" using namespace lean; @@ -43,7 +44,27 @@ static void tst1() { } } +static void tst2() { + std::ostringstream out; + serializer s(out); + mpz n1("-100000000000000000000000000000000000"); + lean_assert(n1.is_neg()); + mpz n2("0"); + mpz n3("1200"); + mpz n4("321"); + s << n1 << n2 << n3 << n4; + std::istringstream in(out.str()); + deserializer d(in); + mpz m1, m2, m3, m4; + d >> m1 >> m2 >> m3 >> m4; + lean_assert(n1 == m1); + lean_assert(n2 == m2); + lean_assert(n3 == m3); + lean_assert(n4 == m4); +} + int main() { tst1(); + tst2(); return has_violations() ? 1 : 0; } diff --git a/src/util/numerics/mpq.cpp b/src/util/numerics/mpq.cpp index f4e5cf2dc..192d0429b 100644 --- a/src/util/numerics/mpq.cpp +++ b/src/util/numerics/mpq.cpp @@ -125,6 +125,17 @@ mpq const & numeric_traits::zero() { return g_zero; } +serializer & operator<<(serializer & s, mpq const & n) { + std::ostringstream out; + out << n; + s << out.str(); + return s; +} + +mpq read_mpq(deserializer & d) { + return mpq(d.read_string().c_str()); +} + DECL_UDATA(mpq) template diff --git a/src/util/numerics/mpq.h b/src/util/numerics/mpq.h index c3f3b3a6a..3a84a181d 100644 --- a/src/util/numerics/mpq.h +++ b/src/util/numerics/mpq.h @@ -277,6 +277,10 @@ public: static void atanh(mpq & ) { lean_unreachable(); } // LCOV_EXCL_LINE }; +serializer & operator<<(serializer & s, mpq const & n); +mpq read_mpq(deserializer & d); +inline deserializer & operator>>(deserializer & d, mpq & n) { n = read_mpq(d); return d; } + UDATA_DEFS(mpq) mpq to_mpq_ext(lua_State * L, int idx); void open_mpq(lua_State * L); diff --git a/src/util/numerics/mpz.cpp b/src/util/numerics/mpz.cpp index 5b62ce773..c3a6e2262 100644 --- a/src/util/numerics/mpz.cpp +++ b/src/util/numerics/mpz.cpp @@ -84,6 +84,17 @@ mpz const & numeric_traits::zero() { return g_zero; } +serializer & operator<<(serializer & s, mpz const & n) { + std::ostringstream out; + out << n; + s << out.str(); + return s; +} + +mpz read_mpz(deserializer & d) { + return mpz(d.read_string().c_str()); +} + DECL_UDATA(mpz) template diff --git a/src/util/numerics/mpz.h b/src/util/numerics/mpz.h index a8e42876c..19d5bec5f 100644 --- a/src/util/numerics/mpz.h +++ b/src/util/numerics/mpz.h @@ -9,6 +9,7 @@ Author: Leonardo de Moura #include #include "util/debug.h" #include "util/lua.h" +#include "util/serializer.h" #include "util/numerics/numeric_traits.h" namespace lean { @@ -236,6 +237,10 @@ public: static mpz const & zero(); }; +serializer & operator<<(serializer & s, mpz const & n); +mpz read_mpz(deserializer & d); +inline deserializer & operator>>(deserializer & d, mpz & n) { n = read_mpz(d); return d; } + UDATA_DEFS(mpz) mpz to_mpz_ext(lua_State * L, int idx); void open_mpz(lua_State * L);