From 2b451a3fed237f72da7e20f6b7062cf118114880 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 22 Jul 2021 18:50:52 +0200 Subject: [PATCH] chore: remove obsolete serializer code --- src/include/lean/mpq.h | 5 - src/include/lean/serializer.h | 142 ----------- src/kernel/expr.h | 14 - src/kernel/level.h | 8 - src/library/compiler/specialize.cpp | 2 - src/library/module.h | 1 - src/runtime/CMakeLists.txt | 2 +- src/runtime/init_module.cpp | 3 - src/runtime/mpq.cpp | 11 - src/runtime/serializer.cpp | 383 ---------------------------- src/tests/util/compact.cpp | 1 - src/tests/util/name.cpp | 203 --------------- src/tests/util/object.cpp | 21 -- src/tests/util/serializer.cpp | 99 ------- src/util/kvmap.h | 6 - src/util/list.h | 23 -- src/util/list_ref.h | 5 - src/util/name.h | 9 - src/util/nat.h | 5 - src/util/object_ref.h | 1 - src/util/option_ref.h | 7 - src/util/pair.h | 11 - src/util/pair_ref.h | 7 - 23 files changed, 1 insertion(+), 968 deletions(-) delete mode 100644 src/include/lean/serializer.h delete mode 100644 src/runtime/serializer.cpp delete mode 100644 src/tests/util/name.cpp delete mode 100644 src/tests/util/serializer.cpp diff --git a/src/include/lean/mpq.h b/src/include/lean/mpq.h index d606232cc4..daeaee258c 100644 --- a/src/include/lean/mpq.h +++ b/src/include/lean/mpq.h @@ -6,7 +6,6 @@ Author: Leonardo de Moura */ #pragma once #include -#include namespace lean { /** @@ -218,8 +217,4 @@ public: friend std::ostream & operator<<(std::ostream & out, decimal const & d) { display_decimal(out, d.m_val, d.m_prec); return out; } }; }; - -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; } } diff --git a/src/include/lean/serializer.h b/src/include/lean/serializer.h deleted file mode 100644 index 1294413ade..0000000000 --- a/src/include/lean/serializer.h +++ /dev/null @@ -1,142 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include -#include -#include -#include -#include -#include -#include -#include -#include - -namespace lean { -class serializer { - std::ostream & m_out; - std::unordered_map, std::equal_to> m_obj_table; - void write_constructor(object * o); - void write_closure(object * o); - void write_thunk(object * o); - void write_task(object * o); - void write_array(object * o); - void write_scalar_array(object * o); - void write_string_object(object * o); - void write_external(object * o); -public: - serializer(std::ostream & out):m_out(out) {} - ~serializer(); - void write_string(char const * str) { m_out.write(str, strlen(str) + 1); } - void write_string(std::string const & str) { write_string(str.c_str()); } - void write_unsigned_short(unsigned short i); - void write_unsigned(unsigned i); - void write_uint64(uint64 i); - void write_size_t(size_t i); - void write_int(int i); - void write_char(char c) { m_out.put(c); } - void write_bool(bool b) { m_out.put(b ? 1 : 0); } - void write_double(double b); - void write_mpz(mpz const & m); - void write_object(object * o); - void write_blob(std::string const &); -}; - -inline serializer & operator<<(serializer & s, char const * str) { s.write_string(str); return s; } -inline serializer & operator<<(serializer & s, std::string const & str) { s.write_string(str); return s; } -inline serializer & operator<<(serializer & s, unsigned i) { s.write_unsigned(i); return s; } -inline serializer & operator<<(serializer & s, uint64 i) { s.write_uint64(i); return s; } -inline serializer & operator<<(serializer & s, int i) { s.write_int(i); return s; } -inline serializer & operator<<(serializer & s, char c) { s.write_char(c); return s; } -inline serializer & operator<<(serializer & s, bool b) { s.write_bool(b); return s; } -inline serializer & operator<<(serializer & s, double b) { s.write_double(b); return s; } -inline serializer & operator<<(serializer & s, object * o) { s.write_object(o); return s; } - -class deserializer { - std::istream & m_in; - std::vector m_objs; - optional m_fname; - unsigned read_unsigned_ext(); - object * read_constructor(); - object * read_closure(); - object * read_thunk(); - object * read_task(); - object * read_array(); - object * read_scalar_array(); - object * read_string_object(); - object * read_external(); -public: - deserializer(std::istream & in):m_in(in) {} - deserializer(std::istream & in, optional const & fname):m_in(in), m_fname(fname) {} - ~deserializer(); - std::string read_string(); - unsigned read_unsigned() { - unsigned r = static_cast(m_in.get()); - return r < 255 ? r : read_unsigned_ext(); - } - uint64 read_uint64(); - size_t read_size_t(); - int read_int() { return read_unsigned(); } - char read_char() { return m_in.get(); } - bool read_bool() { return m_in.get() != 0; } - unsigned short read_unsigned_short(); - double read_double(); - mpz read_mpz(); - std::string read_blob(); - object * read_object(); - optional get_fname() const { return m_fname; } -}; - -inline deserializer & operator>>(deserializer & d, std::string & str) { str = d.read_string(); return d; } -inline deserializer & operator>>(deserializer & d, unsigned & i) { i = d.read_unsigned(); return d; } -inline deserializer & operator>>(deserializer & d, uint64 & i) { i = d.read_uint64(); return d; } -inline deserializer & operator>>(deserializer & d, int & i) { i = d.read_int(); return d; } -inline deserializer & operator>>(deserializer & d, char & c) { c = d.read_char(); return d; } -inline deserializer & operator>>(deserializer & d, bool & b) { b = d.read_bool(); return d; } -inline deserializer & operator>>(deserializer & d, double & b) { b = d.read_double(); return d; } - -class corrupted_stream_exception : public exception { -public: - corrupted_stream_exception(); -}; - -void initialize_serializer(); -void finalize_serializer(); - -template -serializer & write_optional(serializer & s, optional const & a) { - if (a) - s << true << *a; - else - s << false; - return s; -} - -template -optional read_optional(deserializer & d) { - if (d.read_bool()) { - T r; - d >> r; - return optional(r); - } else { - return optional(); - } -} - -template -serializer & operator<<(serializer & s, optional const & a) { - return write_optional(s, a); -} - -template -deserializer & operator>>(deserializer & d, optional & a) { - a = read_optional(d); - return d; -} - -inline serializer & operator<<(serializer & s, mpz const & n) { s.write_mpz(n); return s; } -inline deserializer & operator>>(deserializer & d, mpz & n) { n = d.read_mpz(); return d; } -} diff --git a/src/kernel/expr.h b/src/kernel/expr.h index 67d4407ce3..4c0c0fbac5 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -13,7 +13,6 @@ Author: Leonardo de Moura #include #include #include -#include #include #include "util/name.h" #include "util/nat.h" @@ -63,13 +62,8 @@ public: bool is_zero() const { return kind() == literal_kind::Nat && get_nat().is_zero(); } friend bool operator==(literal const & a, literal const & b); friend bool operator<(literal const & a, literal const & b); - void serialize(serializer & s) const { s.write_object(raw()); } - static literal deserialize(deserializer & d) { return literal(d.read_object(), true); } }; inline bool operator!=(literal const & a, literal const & b) { return !(a == b); } -inline serializer & operator<<(serializer & s, literal const & l) { l.serialize(s); return s; } -inline literal read_literal(deserializer & d) { return literal::deserialize(d); } -inline deserializer & operator>>(deserializer & d, literal & l) { l = read_literal(d); return d; } /* ======================================= Expressions @@ -117,19 +111,11 @@ public: expr & operator=(expr && other) { object_ref::operator=(other); return *this; } friend bool is_eqp(expr const & e1, expr const & e2) { return e1.raw() == e2.raw(); } - void serialize(serializer & s) const { s.write_object(raw()); } - static expr deserialize(deserializer & d) { return expr(d.read_object(), true); } }; typedef list_ref exprs; typedef pair expr_pair; -inline serializer & operator<<(serializer & s, expr const & e) { e.serialize(s); return s; } -inline serializer & operator<<(serializer & s, exprs const & es) { es.serialize(s); return s; } -inline expr read_expr(deserializer & d) { return expr::deserialize(d); } -inline exprs read_exprs(deserializer & d) { return read_list_ref(d); } -inline deserializer & operator>>(deserializer & d, expr & e) { e = read_expr(d); return d; } - inline optional none_expr() { return optional(); } inline optional some_expr(expr const & e) { return optional(e); } inline optional some_expr(expr && e) { return optional(std::forward(e)); } diff --git a/src/kernel/level.h b/src/kernel/level.h index e9b52e7e25..2a88aa6949 100644 --- a/src/kernel/level.h +++ b/src/kernel/level.h @@ -52,8 +52,6 @@ public: level & operator=(level && other) { object_ref::operator=(other); return *this; } friend bool is_eqp(level const & l1, level const & l2) { return l1.raw() == l2.raw(); } - void serialize(serializer & s) const { s.write_object(raw()); } - static level deserialize(deserializer & d) { return level(d.read_object(), true); } bool is_zero() const { return kind() == level_kind::Zero; } bool is_succ() const { return kind() == level_kind::Succ; } @@ -83,12 +81,6 @@ inline bool operator!=(level const & l1, level const & l2) { return !operator==( struct level_hash { unsigned operator()(level const & n) const { return n.hash(); } }; struct level_eq { bool operator()(level const & n1, level const & n2) const { return n1 == n2; } }; -inline serializer & operator<<(serializer & s, level const & l) { l.serialize(s); return s; } -inline serializer & operator<<(serializer & s, levels const & ls) { ls.serialize(s); return s; } -inline level read_level(deserializer & d) { return level::deserialize(d); } -inline levels read_levels(deserializer & d) { return read_list_ref(d); } -inline deserializer & operator>>(deserializer & d, level & l) { l = read_level(d); return d; } - inline optional none_level() { return optional(); } inline optional some_level(level const & e) { return optional(e); } inline optional some_level(level && e) { return optional(std::forward(e)); } diff --git a/src/library/compiler/specialize.cpp b/src/library/compiler/specialize.cpp index d45033565d..41fa3ea0ea 100644 --- a/src/library/compiler/specialize.cpp +++ b/src/library/compiler/specialize.cpp @@ -97,8 +97,6 @@ public: spec_info & operator=(spec_info && other) { object_ref::operator=(other); return *this; } names const & get_mutual_decls() const { return static_cast(cnstr_get_ref(*this, 0)); } spec_arg_kinds const & get_arg_kinds() const { return static_cast(cnstr_get_ref(*this, 1)); } - void serialize(serializer & s) const { s.write_object(raw()); } - static spec_info deserialize(deserializer & d) { return spec_info(d.read_object(), true); } }; extern "C" object* lean_add_specialization_info(object* env, object* fn, object* info); diff --git a/src/library/module.h b/src/library/module.h index 97d12aa416..60d8ba6dd9 100644 --- a/src/library/module.h +++ b/src/library/module.h @@ -9,7 +9,6 @@ Authors: Leonardo de Moura, Gabriel Ebner, Sebastian Ullrich #include #include #include -#include #include #include "kernel/environment.h" diff --git a/src/runtime/CMakeLists.txt b/src/runtime/CMakeLists.txt index 25a71f48f6..228d639ced 100644 --- a/src/runtime/CMakeLists.txt +++ b/src/runtime/CMakeLists.txt @@ -1,6 +1,6 @@ set(RUNTIME_OBJS debug.cpp thread.cpp mpz.cpp mpq.cpp utf8.cpp object.cpp apply.cpp exception.cpp interrupt.cpp memory.cpp -serializer.cpp stackinfo.cpp compact.cpp init_module.cpp io.cpp hash.cpp +stackinfo.cpp compact.cpp init_module.cpp io.cpp hash.cpp platform.cpp alloc.cpp allocprof.cpp sharecommon.cpp stack_overflow.cpp process.cpp) add_library(runtime OBJECT ${RUNTIME_OBJS}) diff --git a/src/runtime/init_module.cpp b/src/runtime/init_module.cpp index 5424c6dc5b..84d96aa3b3 100644 --- a/src/runtime/init_module.cpp +++ b/src/runtime/init_module.cpp @@ -6,7 +6,6 @@ Author: Leonardo de Moura */ #include #include -#include #include #include #include @@ -19,7 +18,6 @@ extern "C" void lean_initialize_runtime_module() { initialize_debug(); initialize_object(); initialize_io(); - initialize_serializer(); initialize_thread(); initialize_process(); initialize_stack_overflow(); @@ -31,7 +29,6 @@ void finalize_runtime_module() { finalize_stack_overflow(); finalize_process(); finalize_thread(); - finalize_serializer(); finalize_io(); finalize_object(); finalize_debug(); diff --git a/src/runtime/mpq.cpp b/src/runtime/mpq.cpp index 0f36a71766..07af2a378c 100644 --- a/src/runtime/mpq.cpp +++ b/src/runtime/mpq.cpp @@ -104,17 +104,6 @@ void display_decimal(std::ostream & out, mpq const & a, unsigned prec) { } out << "?"; } - -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()); -} } void print(lean::mpq const & v) { std::cout << v << std::endl; } diff --git a/src/runtime/serializer.cpp b/src/runtime/serializer.cpp deleted file mode 100644 index a05a1a9d93..0000000000 --- a/src/runtime/serializer.cpp +++ /dev/null @@ -1,383 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include -#include -#include -#include -#include -#include -#include -#include -#include - -namespace lean { -void initialize_serializer() { -} - -void finalize_serializer() { -} - -serializer::~serializer() { - for (std::pair const & it : m_obj_table) { - dec_ref(it.first); - } -} - -void serializer::write_unsigned_short(unsigned short i) { - static_assert(sizeof(i) == 2, "unexpected unsigned short size"); - m_out.put((i >> 8) & 0xff); - m_out.put(i & 0xff); -} - -void serializer::write_unsigned(unsigned i) { - static_assert(sizeof(i) == 4, "unexpected unsigned size"); - if (i < 255) { - m_out.put(i & 0xff); - } else { - m_out.put(-1); - m_out.put((i >> 24) & 0xff); - m_out.put((i >> 16) & 0xff); - m_out.put((i >> 8) & 0xff); - m_out.put(i & 0xff); - } -} - -void serializer::write_uint64(uint64 i) { - static_assert(sizeof(i) == 8, "unexpected uint64 size"); - write_unsigned((i >> 32) & 0xffffffff); - write_unsigned(i & 0xffffffff); -} - -void serializer::write_size_t(size_t i) { - if (sizeof(i) == 8) { - write_uint64(static_cast(i)); - } else { - lean_assert(sizeof(i) == 4); - write_unsigned(static_cast(i)); - } -} - -void serializer::write_int(int i) { - static_assert(sizeof(i) == 4, "unexpected int size"); - write_unsigned(i); -} - -void serializer::write_blob(std::string const & s) { - write_unsigned(s.size()); - m_out.write(&s[0], s.size()); -} - -void serializer::write_constructor(object * o) { - lean_assert(is_cnstr(o)); - unsigned num_objs = cnstr_num_objs(o); - unsigned obj_size = lean_object_byte_size(o); - unsigned main_size = sizeof(lean_ctor_object) + sizeof(lean_object*)*num_objs; - lean_assert(obj_size >= main_size); - unsigned scalar_sz = obj_size - main_size; - write_unsigned_short(cnstr_tag(o)); - write_unsigned_short(num_objs); - write_unsigned_short(scalar_sz); - object ** it = cnstr_obj_cptr(o); - object ** end = it + num_objs; - for (; it != end; ++it) - write_object(*it); - unsigned char * sit = cnstr_scalar_cptr(o); - unsigned char * send = sit + scalar_sz; - for (; sit != send; ++sit) - m_out.put(*sit); -} - -void serializer::write_closure(object *) { // NOLINT - /* TODO(Leo): we need a table from function pointer to unique name id. - - For serializing bytecode, we will need to retrieve the unique name id too. - The trick of storing the bytecode index as the first argument of an "eval" - C function is not going to work. It seems we will to store the index as - a tagged pointer and handle it at `apply`. - */ - lean_internal_panic("serializer for closures has not been implemented yet"); -} - -void serializer::write_thunk(object * o) { - object * r = thunk_get(o); - write_object(r); -} - -void serializer::write_task(object * o) { - object * r = task_get(o); - write_object(r); -} - -void serializer::write_array(object * o) { - lean_assert(is_array(o)); - size_t sz = sarray_size(o); - write_size_t(sz); - object ** it = array_cptr(o); - object ** end = it + sz; - for (; it != end; ++it) - write_object(*it); -} - -void serializer::write_scalar_array(object * o) { - lean_assert(is_sarray(o)); - unsigned esz = sarray_elem_size(o); - size_t sz = sarray_size(o); - write_unsigned(esz); - write_size_t(sz); - size_t num_bytes = sz*esz; - uint8 const * it = sarray_cptr(o); - uint8 const * end = it + num_bytes; - for (; it != end; ++it) - m_out.put(*it); -} - -void serializer::write_string_object(object * o) { - size_t sz = string_size(o); - size_t len = string_len(o); - write_size_t(sz); - write_size_t(len); - char const * it = string_cstr(o); - char const * end = it + sz; - for (; it != end; ++it) - m_out.put(*it); -} - -void serializer::write_mpz(mpz const & n) { - std::ostringstream out; - out << n; - write_string(out.str()); -} - -void serializer::write_external(object *) { // NOLINT - /* TODO(Leo): we need support for registering serializers/deserializers - for external objects. - */ - lean_internal_panic("serializer for external objects has not been implemented yet"); -} - -void serializer::write_object(object * o) { - if (is_scalar(o)) { - m_out.put(0); - write_unsigned(unbox(o)); - } else { - auto it = m_obj_table.find(o); - if (it != m_obj_table.end()) { - m_out.put(1); - write_unsigned(it->second); - } else { - uint8 k = lean_ptr_tag(o); - m_out.put(static_cast(k) + 2); - switch (k) { - case LeanClosure: write_closure(o); break; - case LeanTask: write_task(o); break; - case LeanThunk: write_thunk(o); break; - case LeanArray: write_array(o); break; - case LeanScalarArray: write_scalar_array(o); break; - case LeanString: write_string_object(o); break; - case LeanMPZ: write_mpz(mpz_value(o)); break; - case LeanExternal: write_external(o); break; - case LeanReserved: lean_unreachable(); break; - default: write_constructor(o); break; - } - inc_ref(o); - m_obj_table.insert(std::make_pair(o, m_obj_table.size())); - } - } -} - -corrupted_stream_exception::corrupted_stream_exception(): - exception("corrupted binary file") {} - -void serializer::write_double(double d) { - std::ostringstream out; - // TODO(Leo): the following code may miss precision. - // We should use std::ios::hexfloat, but it is not supported by - // g++ yet. - out.flags (std::ios::scientific); - out.precision(std::numeric_limits::digits10 + 1); - out << std::hex << d; - write_string(out.str()); -} - -deserializer::~deserializer() { - for (object * o : m_objs) - dec_ref(o); -} - -std::string deserializer::read_string() { - std::string r; - while (true) { - char c = m_in.get(); - if (c == 0) - break; - if (m_in.eof()) - throw corrupted_stream_exception(); - r += c; - } - return r; -} - -unsigned deserializer::read_unsigned_ext() { - unsigned r; - static_assert(sizeof(r) == 4, "unexpected unsigned size"); - r = static_cast(m_in.get()) << 24; - r |= static_cast(m_in.get()) << 16; - r |= static_cast(m_in.get()) << 8; - r |= static_cast(m_in.get()); - return r; -} - -unsigned short deserializer::read_unsigned_short() { - unsigned short r; - static_assert(sizeof(r) == 2, "unexpected unsigned short size"); - r = static_cast(m_in.get()) << 8; - r |= static_cast(m_in.get()); - return r; -} - -uint64 deserializer::read_uint64() { - uint64 r; - static_assert(sizeof(r) == 8, "unexpected uint64 size"); - r = static_cast(read_unsigned()) << 32; - r |= static_cast(read_unsigned()); - return r; -} - -size_t deserializer::read_size_t() { - if (sizeof(size_t) == 8) { - return static_cast(read_uint64()); - } else { - lean_assert(sizeof(size_t) == 4); - return static_cast(read_unsigned()); - } -} - -double deserializer::read_double() { - // TODO(Leo): use std::hexfloat as soon as it is supported by g++ - std::istringstream in(read_string()); - double r; - in >> r; - return r; -} - -mpz deserializer::read_mpz() { - return mpz(read_string().c_str()); -} - -std::string deserializer::read_blob() { - unsigned sz = read_unsigned(); - std::string s(sz, '\0'); - m_in.read(&s[0], sz); - return s; -} - -object * deserializer::read_constructor() { - unsigned tag = read_unsigned_short(); - unsigned num_objs = read_unsigned_short(); - unsigned scalar_sz = read_unsigned_short(); - object * r = alloc_cnstr(tag, num_objs, scalar_sz); - for (unsigned i = 0; i < num_objs; i++) { - object * o = read_object(); - inc(o); - cnstr_set(r, i, o); - } - unsigned char * it = cnstr_scalar_cptr(r); - unsigned char * end = it + scalar_sz; - for (; it != end; ++it) - *it = m_in.get(); - return r; -} - -object * deserializer::read_closure() { - lean_internal_panic("serializer for closures has not been implemented yet"); -} - -object * deserializer::read_thunk() { - object * v = read_object(); - inc(v); - return thunk_pure(v); -} - -object * deserializer::read_task() { - object * v = read_object(); - inc(v); - return task_pure(v); -} - -object * deserializer::read_array() { - size_t sz = read_size_t(); - object * r = alloc_array(sz, sz); - object ** it = array_cptr(r); - object ** end = it + sz; - for (; it != end; ++it) { - object * o = read_object(); - inc(o); - *it = o; - } - return r; -} - -object * deserializer::read_scalar_array() { - unsigned esz = read_unsigned(); - size_t sz = read_size_t(); - object * r = alloc_sarray(esz, sz, sz); - uint8 * it = sarray_cptr(r); - uint8 * end = it + sz*esz; - for (; it != end; ++it) - *it = m_in.get(); - return r; -} - -object * deserializer::read_string_object() { - size_t sz = read_size_t(); - size_t len = read_size_t(); - object * r = alloc_string(sz, sz, len); - unsigned char * it = const_cast(reinterpret_cast(string_cstr(r))); - unsigned char * end = it + sz; - for (; it != end; ++it) - *it = m_in.get(); - return r; -} - -object * deserializer::read_external() { - lean_internal_panic("serializer for external objects has not been implemented yet"); -} - -object * deserializer::read_object() { - unsigned c = m_in.get(); - if (c == 0) { - return box(read_unsigned()); - } else if (c == 1) { - unsigned i = read_unsigned(); - if (i >= m_objs.size()) - throw corrupted_stream_exception(); - return m_objs[i]; - } else { - object * r; - switch (c - 2) { - case LeanClosure: r = read_closure(); break; - case LeanThunk: r = read_thunk(); break; - case LeanTask: r = read_task(); break; - case LeanArray: r = read_array(); break; - case LeanScalarArray: r = read_scalar_array(); break; - case LeanString: r = read_string_object(); break; - case LeanMPZ: r = alloc_mpz(read_mpz()); break; - case LeanExternal: r = read_external(); break; - case LeanReserved: throw corrupted_stream_exception(); - default: - if (c - 2 < LeanMaxCtorTag) - r = read_constructor(); - else - throw corrupted_stream_exception(); - break; - } - m_objs.push_back(r); - return r; - } -} -} diff --git a/src/tests/util/compact.cpp b/src/tests/util/compact.cpp index bf65ba249b..6c3b5b774c 100644 --- a/src/tests/util/compact.cpp +++ b/src/tests/util/compact.cpp @@ -6,7 +6,6 @@ Author: Leonardo de Moura */ #include #include "util/test.h" -#include #include #include #include "util/object_ref.h" diff --git a/src/tests/util/name.cpp b/src/tests/util/name.cpp deleted file mode 100644 index f65155694f..0000000000 --- a/src/tests/util/name.cpp +++ /dev/null @@ -1,203 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include -#include -#include "util/test.h" -#include "util/name.h" -#include "util/name_set.h" -#include "util/init_module.h" -using namespace lean; - -static void tst1() { - name n("foo"); - lean_assert(n == name("foo")); - lean_assert(name(n, 1) != name(n, 2)); - lean_assert(name(n, 1) == name(n, 1)); - lean_assert(name(name(n, 1), 2) != name(name(n, 1), 1)); - lean_assert(name(name(n, 1), 1) == name(name(n, 1), 1)); - lean_assert(name(name(n, 2), 1) != name(name(n, 1), 1)); - lean_assert(name(name(n, "bla"), 1) == name(name(n, "bla"), 1)); - lean_assert(name(name(n, "foo"), 1) != name(name(n, "bla"), 1)); - lean_assert(name(name(name("f"), "bla"), 1) != name(name(n, "bla"), 1)); - lean_assert(n != name()); - lean_assert(name().kind() == name_kind::ANONYMOUS); - lean_assert(name(name(), "foo") == name("foo")); - - lean_assert(name(n, 1) < name(n, 2)); - std::cout << "cmp(" << name(n, 1) << ", " << name(n, 2) << ") = " << cmp(name(n, 1), name(n, 2)) << "\n"; - lean_assert(!(name(n, 1) >= name(n, 2))); - lean_assert(name(n, 1) < name(name(n, 1), 1)); - lean_assert(n < name(n, 1)); - lean_assert(name(n, 2) > name(name(n, 1), 1)); - lean_assert(name(name("aa"), 2) < name(name(n, 1), 1)); - lean_assert(name(n, "aaa") < name(n, "xxx")); - lean_assert(name(n, 1) < name(n, "xxx")); - lean_assert(name(n, 1) < name(name(n, "xxx"), 1)); - lean_assert(name() < name(name(n, "xxx"), 1)); -} - -static name mk_big_name(unsigned num) { - name n("foo"); - for (unsigned i = 0; i < num; i++) { - n = name(n, "bla"); - } - return n; -} - -static void tst2() { - name n1 = mk_big_name(2000); - name n2 = mk_big_name(2000); - lean_assert(n1.hash() == n2.hash()); - for (unsigned i = 0; i < 10000; i++) - n1.hash(); - std::cout << "n1.hash(): " << n1.hash() << "\n"; -} - -static void tst3() { - name n{"foo", "bla", "tst"}; - std::cout << n << "\n"; - lean_assert(n == name(name(name("foo"), "bla"), "tst")); -} - -static void tst4() { - lean_assert(is_prefix_of(name{"foo", "bla"}, name{"foo", "bla"})); - lean_assert(is_prefix_of(name{"foo", "bla"}, name{"foo", "bla", "foo"})); - lean_assert(is_prefix_of(name{"foo"}, name{"foo", "bla", "foo"})); - lean_assert(!is_prefix_of(name{"foo"}, name{"fo", "bla", "foo"})); - lean_assert(!is_prefix_of(name{"foo", "bla", "foo"}, name{"foo", "bla"})); - lean_assert(is_prefix_of(name{"foo", "bla"}, name(name{"foo", "bla"}, 0u))); - lean_assert(is_prefix_of(name("aaa"), name("aaa"))); - lean_assert(!is_prefix_of(name("aaa"), name("aaab"))); - lean_assert(!is_prefix_of(name("aaab"), name("aaa"))); - lean_assert(!is_prefix_of(name{"foo", "bla"}, name{"foo"})); - lean_assert(is_prefix_of(name{"foo"}, name{"foo", "bla"})); -} - -static void tst5() { - lean_assert(name().size() > 0); - lean_assert(name({"foo", "bla", "boing"}).get_prefix() == name({"foo", "bla"})); - lean_assert(!name({"foo", "bla", "boing"}).is_atomic()); - lean_assert(name({"foo"}).is_atomic()); - lean_assert(name({"foo", "bla", "boing"}).get_string() == "boing"); - lean_assert(name(name("foo"), 1u).get_numeral() == nat(1)); - lean_assert(name::anonymous().is_anonymous()); - name n1("foo"); - name n2 = n1; - lean_assert(n2 == n1); - std::cout << name::anonymous() << "\n"; - std::cout << name({"foo", "bla", "boing"}).get_prefix() << "\n"; - lean_assert(name("foo").is_string()); - lean_assert(name(name("boo"), "foo").is_string()); - lean_assert(name(name("foo"), 0u).is_numeral()); - lean_assert(name(name("foo"), 0u).get_prefix().is_string()); -} - -static void tst6() { - lean_assert(name({"foo", "bla"}).is_safe_ascii()); - lean_assert(!name({"foo", "b∀aaa"}).is_safe_ascii()); - lean_assert(!name({"∀", "boo"}).is_safe_ascii()); - lean_assert(!name(name(name("baa"), "bla∀"), "foo").is_safe_ascii()); -} - -static void tst7() { - lean_assert(name("foo") + name("bla") == name({"foo", "bla"})); - lean_assert(name("foo") + name({"bla", "test"}) == name({"foo", "bla", "test"})); - lean_assert(name({"foo", "hello"}) + name({"bla", "test"}) == name({"foo", "hello", "bla", "test"})); - lean_assert(name("foo") + (name("bla") + name({"bla", "test"})) == name(name(name(name("foo"), "bla"), "bla"), "test")); - lean_assert(name() + name({"bla", "test"}) == name({"bla", "test"})); - lean_assert(name({"bla", "test"}) + name() == name({"bla", "test"})); -} - -static void tst8() { - name u1 = name::mk_internal_unique_name(); - name u2 = name::mk_internal_unique_name(); - lean_assert(u1 != u2); - std::cout << u1 << " " << u2 << "\n"; -} - -static void tst11() { - name n1("a"); - name n2("b"); - swap(n1, n2); - lean_assert(n1 == name("b")); - lean_assert(n2 == name("a")); -} - -static void tst12() { - name_set s; - s.insert(name("foo")); - s.insert(name(name("foo"), 1)); - s.insert(name("bla")); - lean_assert(mk_unique(s, name("boo")) == name("boo")); - lean_assert(mk_unique(s, name("bla")) == name(name("bla"), 1)); - lean_assert(mk_unique(s, name("foo")) == name(name("foo"), 2)); -} - -static void tst13() { - std::ostringstream ostrm; - serializer out(ostrm); - name s1({"a", "b"}); - out << s1; - std::cout << "------\n"; - unsigned i = 0; - for (unsigned char c : ostrm.str()) { - std::cout << i << ": " << static_cast(c) << "\n"; - i++; - } - std::istringstream istrm(ostrm.str()); - deserializer in(istrm); - name s2; - in >> s2; - std::cout << "h1: " << s1.hash() << "\nh2: " << s2.hash() << "\n"; - std::cout << "s1>> " << s1 << "\ns2>> " << s2 << "\n"; - lean_assert(s1 == s2); -} - -static void tst14() { - name a("a"); - name b(a, nat("100000000000000000000000000")); - lean_assert(b.get_numeral() == nat("100000000000000000000000000")); -} - -static void tst15() { - std::string s("a"); - s.push_back(0); - s.push_back('b'); - std::cout << ">> " << static_cast(s[0]) << "\n"; - std::cout << ">> " << static_cast(s[1]) << "\n"; - std::cout << ">> " << static_cast(s[2]) << "\n"; - std::cout << "------\n"; - string_ref v(s); - std::cout << ">> " << static_cast(v.data()[0]) << "\n"; - std::cout << ">> " << static_cast(v.data()[1]) << "\n"; - std::cout << ">> " << static_cast(v.data()[2]) << "\n"; - lean_assert(v.to_std_string() == s); - name a(s); - lean_assert(a.get_string().to_std_string() == s); - lean_assert(a.get_string().num_bytes() == 3); -} - -int main() { - save_stack_info(); - initialize_util_module(); - tst1(); - tst2(); - tst3(); - tst4(); - tst5(); - tst6(); - tst7(); - tst8(); - tst11(); - tst12(); - tst13(); - tst14(); - tst15(); - finalize_util_module(); - return has_violations() ? 1 : 0; -} diff --git a/src/tests/util/object.cpp b/src/tests/util/object.cpp index f3dc49e0d5..5122ac5046 100644 --- a/src/tests/util/object.cpp +++ b/src/tests/util/object.cpp @@ -12,7 +12,6 @@ Author: Leonardo de Moura #include "util/timeit.h" #include #include -#include #include #include "util/object_ref.h" #include "util/array_ref.h" @@ -94,26 +93,6 @@ void tst4() { USED(r3); USED(r4); } -void tst5() { - object_ref t(mk_thunk(alloc_closure(r, 0))); - std::ostringstream out; - serializer s(out); - object_ref o(mk_string("bla bla")); - s.write_object(o.raw()); - s.write_object(t.raw()); - s.write_object(t.raw()); - std::istringstream in(out.str()); - deserializer d(in); - d.read_object(); - object * r1 = d.read_object(); - object * r2 = d.read_object(); - lean_assert(r1 == r2); - lean_assert(is_thunk(r1)); - object * str = thunk_get(r1); - lean_assert(strcmp(string_cstr(str), "hello world") == 0); - USED(r2); USED(str); -} - unsigned g_counter = 0; mutex g_io_mutex; diff --git a/src/tests/util/serializer.cpp b/src/tests/util/serializer.cpp deleted file mode 100644 index afe37aed97..0000000000 --- a/src/tests/util/serializer.cpp +++ /dev/null @@ -1,99 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include -#include -#include -#include -#include -#include -#include -#include "util/test.h" -#include "util/list.h" -#include "util/name.h" -#include "util/init_module.h" -using namespace lean; - -void display(std::ostringstream const & out) { - std::cout << "OUT: "; - auto str = out.str(); - for (auto c : str) { - std::cout << static_cast(static_cast(c)) << " "; - } - std::cout << "\n"; -} - -static void tst1() { - std::ostringstream out; - serializer s(out); - s.write_int(10); s.write_int(-20); s.write_bool(false); s.write_string("hello"); s.write_int(30); - display(out); - std::istringstream in(out.str()); - deserializer d(in); - lean_assert(d.read_int() == 10); - lean_assert(d.read_int() == -20); - lean_assert(!d.read_bool()); - lean_assert(d.read_string() == "hello"); - lean_assert(d.read_int() == 30); -} - -static void tst2() { -} - -static void tst3() { - std::ostringstream out; - serializer s(out); - name n1{"foo", "bla"}; - name n2(n1, 10); - name n3(n2, "tst"); - name n4(n1, "hello"); - name n5("simple"); - s << n1 << n2 << n3 << n4 << n2 << n5; - display(out); - std::istringstream in(out.str()); - deserializer d(in); - name m1, m2, m3, m4, m5, m6; - d >> m1 >> m2 >> m3 >> m4 >> m5 >> m6; - lean_assert(n1 == m1); - lean_assert(n2 == m2); - lean_assert(n3 == m3); - lean_assert(n4 == m4); - lean_assert(n2 == m5); - lean_assert(n5 == m6); -} - -static void tst4() { - std::ostringstream out; - serializer s(out); - double d1, d2, d3, d4, d5; - d1 = 0.1; - d2 = -0.3; - d3 = 0.0; - d4 = 12317.123; - d5 = std::atan(1.0)*4; - s << d1 << d2 << d3 << d4 << d5; - std::istringstream in(out.str()); - deserializer d(in); - double o1, o2, o3, o4, o5; - d >> o1 >> o2 >> o3 >> o4 >> o5; - lean_assert_eq(d1, o1); - lean_assert_eq(d2, o2); - lean_assert_eq(d3, o3); - lean_assert_eq(d4, o4); - lean_assert_eq(d5, o5); -} - -int main() { - save_stack_info(); - initialize_util_module(); - tst1(); - tst2(); - tst3(); - tst4(); - finalize_util_module(); - return has_violations() ? 1 : 0; -} diff --git a/src/util/kvmap.h b/src/util/kvmap.h index 2c3ef66af0..f3f95d353b 100644 --- a/src/util/kvmap.h +++ b/src/util/kvmap.h @@ -33,9 +33,6 @@ public: data_value & operator=(data_value const & other) { object_ref::operator=(other); return *this; } data_value & operator=(data_value && other) { object_ref::operator=(other); return *this; } - void serialize(serializer & s) const { s.write_object(raw()); } - static data_value deserialize(deserializer & d) { return data_value(d.read_object(), true); } - data_value_kind kind() const { return static_cast(cnstr_tag(raw())); } string_ref const & get_string() const { lean_assert(kind() == data_value_kind::String); return static_cast(cnstr_get_ref(*this, 0)); } nat const & get_nat() const { lean_assert(kind() == data_value_kind::Nat); return static_cast(cnstr_get_ref(*this, 0)); } @@ -50,9 +47,6 @@ bool operator==(data_value const & a, data_value const & b); inline bool operator!=(data_value const & a, data_value const & b) { return !(a == b); } bool operator<(data_value const & a, data_value const & b); -inline serializer & operator<<(serializer & s, data_value const & v) { v.serialize(s); return s; } -inline data_value read_data_value(deserializer & d) { return data_value::deserialize(d); } - typedef pair_ref kvmap_entry; typedef list_ref kvmap; diff --git a/src/util/list.h b/src/util/list.h index aa763826ce..598de731b2 100644 --- a/src/util/list.h +++ b/src/util/list.h @@ -8,7 +8,6 @@ Author: Leonardo de Moura #include #include #include -#include #include #include "util/rc.h" #include "util/buffer.h" @@ -240,26 +239,4 @@ template list reverse_to_list(buffer const & b) { return reverse_to_list(b.begin(), b.end()); } - -template -serializer & write_list(serializer & s, list const & ls) { - s << length(ls); - for (auto const & e : ls) - s << e; - return s; -} - -template -list read_list(deserializer & d, R && t_reader) { - unsigned num = d.read_unsigned(); - buffer ls; - for (unsigned i = 0; i < num; i++) - ls.push_back(t_reader(d)); - return to_list(ls.begin(), ls.end()); -} - -template -list read_list(deserializer & d) { - return read_list(d, [](deserializer & d) { T r; d >> r; return r; }); -} } diff --git a/src/util/list_ref.h b/src/util/list_ref.h index 6f1401aeef..0ce50700aa 100644 --- a/src/util/list_ref.h +++ b/src/util/list_ref.h @@ -47,8 +47,6 @@ public: friend list_ref cons(T const & h, list_ref const & t) { return list_ref(h, t); } friend bool is_eqp(list_ref const & l1, list_ref const & l2) { return l1.raw() == l2.raw(); } - void serialize(serializer & s) const { s.write_object(raw()); } - static list_ref deserialize(deserializer & d) { return list_ref(d.read_object(), true); } /** \brief Structural equality. */ friend bool operator==(list_ref const & l1, list_ref const & l2) { @@ -131,9 +129,6 @@ template size_t length(list_ref const & l) { return r; } -template serializer & operator<<(serializer & s, list_ref const & l) { l.serialize(s); return s; } -template list_ref read_list_ref(deserializer & d) { return list_ref::deserialize(d); } - template optional head_opt(list_ref const & l) { return is_nil(l) ? optional() : some(head(l)); } /** \brief Given `[a_0, ..., a_k]`, return `[f a_0, ..., f a_k]`. */ diff --git a/src/util/name.h b/src/util/name.h index 143bf5336b..57b020dded 100644 --- a/src/util/name.h +++ b/src/util/name.h @@ -11,7 +11,6 @@ Author: Leonardo de Moura #include #include #include -#include #include "util/buffer.h" #include "util/pair.h" #include "util/nat.h" @@ -61,7 +60,6 @@ public: static int cmp_core(object * o1, object * o2); size_t size_core(bool unicode) const; private: - friend name read_name(deserializer & d); explicit name(object_ref && r):object_ref(r) {} public: name():object_ref(box(static_cast(name_kind::ANONYMOUS))) {} @@ -197,7 +195,6 @@ public: return cmp(a, b); } } - void serialize(serializer & s) const { s.write_object(raw()); } }; name string_to_name(std::string const & str); @@ -238,16 +235,10 @@ struct name_pair_quick_cmp { typedef std::function name_predicate; // NOLINT -inline serializer & operator<<(serializer & s, name const & n) { n.serialize(s); return s; } -inline name read_name(deserializer & d) { return name(d.read_object(), true); } -inline deserializer & operator>>(deserializer & d, name & n) { n = read_name(d); return d; } - /** \brief Return true if it is a lean internal name, i.e., the name starts with a `_` */ bool is_internal_name(name const & n); typedef list_ref names; -inline serializer & operator<<(serializer & s, names const & ns) { ns.serialize(s); return s; } -inline names read_names(deserializer & d) { return read_list_ref(d); } void initialize_name(); void finalize_name(); diff --git a/src/util/nat.h b/src/util/nat.h index ed19b1804e..a0c9be3d4e 100644 --- a/src/util/nat.h +++ b/src/util/nat.h @@ -62,8 +62,6 @@ public: friend nat operator*(nat const & a, nat const & b) { return nat(nat_mul(a.raw(), b.raw())); } friend nat operator/(nat const & a, nat const & b) { return nat(nat_div(a.raw(), b.raw())); } friend nat operator%(nat const & a, nat const & b) { return nat(nat_mod(a.raw(), b.raw())); } - void serialize(serializer & s) const { s.write_object(raw()); } - static nat deserialize(deserializer & d) { return nat(d.read_object(), true); } }; inline optional to_optional_nat(obj_arg o) { @@ -73,8 +71,5 @@ inline optional to_optional_nat(obj_arg o) { return r; } -inline serializer & operator<<(serializer & s, nat const & n) { n.serialize(s); return s; } -inline nat read_nat(deserializer & d) { return nat::deserialize(d); } -inline deserializer & operator>>(deserializer & d, nat & n) { n = read_nat(d); return d; } inline std::ostream & operator<<(std::ostream & out, nat const & n) { out << n.to_mpz(); return out; } }; diff --git a/src/util/object_ref.h b/src/util/object_ref.h index 4a1d8cad62..10d0480972 100644 --- a/src/util/object_ref.h +++ b/src/util/object_ref.h @@ -9,7 +9,6 @@ Author: Leonardo de Moura #include #include #include -#include namespace lean { /* Smart point for Lean objects. It is useful for writing C++ code that manipulates Lean objects. */ diff --git a/src/util/option_ref.h b/src/util/option_ref.h index 8c540c8306..c789d170dd 100644 --- a/src/util/option_ref.h +++ b/src/util/option_ref.h @@ -28,9 +28,6 @@ public: explicit operator bool() const { return !is_scalar(raw()); } optional get() const { return *this ? some(static_cast(cnstr_get_ref(*this, 0))) : optional(); } - void serialize(serializer & s) const { s.write_object(raw()); } - static option_ref deserialize(deserializer & d) { return option_ref(d.read_object()); } - /** \brief Structural equality. */ friend bool operator==(option_ref const & o1, option_ref const & o2) { return o1.get() == o2.get(); @@ -58,8 +55,4 @@ public: } */ }; - -template serializer & operator<<(serializer & s, option_ref const & l) { l.serialize(s); return s; } -template option_ref read_option_ref(deserializer & d) { return option_ref::deserialize(d); } - } diff --git a/src/util/pair.h b/src/util/pair.h index 1fbf5019e8..92e681ae7e 100644 --- a/src/util/pair.h +++ b/src/util/pair.h @@ -6,7 +6,6 @@ Author: Leonardo de Moura */ #pragma once #include -#include namespace lean { template @@ -17,14 +16,4 @@ template inline pair mk_pair(T1 const & v1, T2 const & v2) { return std::make_pair(v1, v2); } - -template -inline serializer & operator<<(serializer & s, pair const & p) { - s << p.first << p.second; return s; -} - -template -inline deserializer & operator>>(deserializer & d, pair & p) { - d >> p.first >> p.second; return d; -} } diff --git a/src/util/pair_ref.h b/src/util/pair_ref.h index f41107a2dd..9130514cd0 100644 --- a/src/util/pair_ref.h +++ b/src/util/pair_ref.h @@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include #include "util/object_ref.h" namespace lean { @@ -23,9 +22,6 @@ public: T1 const & fst() const { return static_cast(cnstr_get_ref(*this, 0)); } T2 const & snd() const { return static_cast(cnstr_get_ref(*this, 1)); } - - void serialize(serializer & s) const { s.write_object(raw()); } - static pair_ref deserialize(deserializer & d) { return pair_ref(d.read_object(), true); } }; template bool operator==(pair_ref const & a, pair_ref const & b) { @@ -40,7 +36,4 @@ template bool operator<(pair_ref const & a, pa if (a.fst() != b.fst()) return a.fst() < b.fst(); else return a.snd() < b.snd(); } - -template serializer & operator<<(serializer & s, pair_ref const & p) { p.serialize(s); return s; } -template pair_ref read_pair_ref(deserializer & d) { return pair_ref::deserialize(d); } }