max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: remove obsolete serializer code

Browse source
This commit is contained in:
Sebastian Ullrich 2021-07-22 18:50:52 +02:00
parent 5b1cfc25d8
commit 2b451a3fed
23 changed files with 1 additions and 968 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/include/lean/mpq.h
View file

@ -6,7 +6,6 @@ Author: Leonardo de Moura
*/
#pragma once
#include <lean/mpz.h>
#include <lean/serializer.h>
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; }
}

142
src/include/lean/serializer.h
View file

@ -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 <vector>
#include <iostream>
#include <string>
#include <sstream>
#include <functional>
#include <unordered_map>
#include <cstring>
#include <lean/object.h>
#include <lean/optional.h>
namespace lean {
class serializer {
std::ostream & m_out;
std::unordered_map<object*, unsigned, std::hash<object*>, std::equal_to<object*>> 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<object*> m_objs;
optional<std::string> 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<std::string> const & fname):m_in(in), m_fname(fname) {}
~deserializer();
std::string read_string();
unsigned read_unsigned() {
unsigned r = static_cast<unsigned>(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<std::string> 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<typename T>
serializer & write_optional(serializer & s, optional<T> const & a) {
if (a)
s << true << *a;
else
s << false;
return s;
}
template<typename T>
optional<T> read_optional(deserializer & d) {
if (d.read_bool()) {
T r;
d >> r;
return optional<T>(r);
} else {
return optional<T>();
}
}
template<typename T>
serializer & operator<<(serializer & s, optional<T> const & a) {
return write_optional<T>(s, a);
}
template<typename T>
deserializer & operator>>(deserializer & d, optional<T> & a) {
a = read_optional<T>(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; }
}

14
src/kernel/expr.h
View file

@ -13,7 +13,6 @@ Author: Leonardo de Moura
#include <string>
#include <lean/optional.h>
#include <lean/thread.h>
#include <lean/serializer.h>
#include <lean/hash.h>
#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<expr> exprs;
typedef pair<expr, expr> 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<expr>(d); }
inline deserializer & operator>>(deserializer & d, expr & e) { e = read_expr(d); return d; }
inline optional<expr> none_expr() { return optional<expr>(); }
inline optional<expr> some_expr(expr const & e) { return optional<expr>(e); }
inline optional<expr> some_expr(expr && e) { return optional<expr>(std::forward<expr>(e)); }

8
src/kernel/level.h
View file

@ -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<level>(d); }
inline deserializer & operator>>(deserializer & d, level & l) { l = read_level(d); return d; }
inline optional<level> none_level() { return optional<level>(); }
inline optional<level> some_level(level const & e) { return optional<level>(e); }
inline optional<level> some_level(level && e) { return optional<level>(std::forward<level>(e)); }

2
src/library/compiler/specialize.cpp
View file

@ -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<names const &>(cnstr_get_ref(*this, 0)); }
spec_arg_kinds const & get_arg_kinds() const { return static_cast<spec_arg_kinds const &>(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);

1
src/library/module.h
View file

@ -9,7 +9,6 @@ Authors: Leonardo de Moura, Gabriel Ebner, Sebastian Ullrich
#include <iostream>
#include <utility>
#include <vector>
#include <lean/serializer.h>
#include <lean/optional.h>
#include "kernel/environment.h"

2
src/runtime/CMakeLists.txt
View file

@ -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})

3
src/runtime/init_module.cpp
View file

@ -6,7 +6,6 @@ Author: Leonardo de Moura
*/
#include <lean/alloc.h>
#include <lean/debug.h>
#include <lean/serializer.h>
#include <lean/thread.h>
#include <lean/object.h>
#include <lean/io.h>
@ -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();

11
src/runtime/mpq.cpp
View file

@ -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; }

383
src/runtime/serializer.cpp
View file

@ -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 <vector>
#include <string>
#include <limits>
#include <stdio.h>
#include <utility>
#include <ios>
#include <lean/exception.h>
#include <lean/serializer.h>
#include <lean/object.h>
#include <lean/mpz.h>
namespace lean {
void initialize_serializer() {
}
void finalize_serializer() {
}
serializer::~serializer() {
for (std::pair<object * const, unsigned> 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<uint64>(i));
} else {
lean_assert(sizeof(i) == 4);
write_unsigned(static_cast<unsigned>(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<unsigned>(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<double>::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<unsigned>(m_in.get()) << 24;
r |= static_cast<unsigned>(m_in.get()) << 16;
r |= static_cast<unsigned>(m_in.get()) << 8;
r |= static_cast<unsigned>(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<unsigned short>(m_in.get()) << 8;
r |= static_cast<unsigned short>(m_in.get());
return r;
}
uint64 deserializer::read_uint64() {
uint64 r;
static_assert(sizeof(r) == 8, "unexpected uint64 size");
r = static_cast<uint64>(read_unsigned()) << 32;
r |= static_cast<uint64>(read_unsigned());
return r;
}
size_t deserializer::read_size_t() {
if (sizeof(size_t) == 8) {
return static_cast<size_t>(read_uint64());
} else {
lean_assert(sizeof(size_t) == 4);
return static_cast<size_t>(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<unsigned char*>(reinterpret_cast<unsigned char const *>(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;
}
}
}

1
src/tests/util/compact.cpp
View file

@ -6,7 +6,6 @@ Author: Leonardo de Moura
*/
#include <iostream>
#include "util/test.h"
#include <lean/serializer.h>
#include <lean/sstream.h>
#include <lean/compact.h>
#include "util/object_ref.h"

203
src/tests/util/name.cpp
View file

@ -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 <cstring>
#include <sstream>
#include <string>
#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<unsigned>(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<unsigned>(s[0]) << "\n";
std::cout << ">> " << static_cast<unsigned>(s[1]) << "\n";
std::cout << ">> " << static_cast<unsigned>(s[2]) << "\n";
std::cout << "------\n";
string_ref v(s);
std::cout << ">> " << static_cast<unsigned>(v.data()[0]) << "\n";
std::cout << ">> " << static_cast<unsigned>(v.data()[1]) << "\n";
std::cout << ">> " << static_cast<unsigned>(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;
}

21
src/tests/util/object.cpp
View file

@ -12,7 +12,6 @@ Author: Leonardo de Moura
#include "util/timeit.h"
#include <lean/stackinfo.h>
#include <lean/thread.h>
#include <lean/serializer.h>
#include <lean/sstream.h>
#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;

99
src/tests/util/serializer.cpp
View file

@ -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 <iostream>
#include <sstream>
#include <string>
#include <cstring>
#include <vector>
#include <functional>
#include <cmath>
#include <lean/debug.h>
#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<int>(static_cast<unsigned char>(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;
}

6
src/util/kvmap.h
View file

@ -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<data_value_kind>(cnstr_tag(raw())); }
string_ref const & get_string() const { lean_assert(kind() == data_value_kind::String); return static_cast<string_ref const &>(cnstr_get_ref(*this, 0)); }
nat const & get_nat() const { lean_assert(kind() == data_value_kind::Nat); return static_cast<nat const &>(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<name, data_value> kvmap_entry;
typedef list_ref<kvmap_entry> kvmap;

23
src/util/list.h
View file

@ -8,7 +8,6 @@ Author: Leonardo de Moura
#include <iostream>
#include <iterator>
#include <lean/debug.h>
#include <lean/serializer.h>
#include <lean/optional.h>
#include "util/rc.h"
#include "util/buffer.h"
@ -240,26 +239,4 @@ template<typename T>
list<T> reverse_to_list(buffer<T> const & b) {
return reverse_to_list(b.begin(), b.end());
}
template<typename T>
serializer & write_list(serializer & s, list<T> const & ls) {
s << length(ls);
for (auto const & e : ls)
s << e;
return s;
}
template<typename T, typename R>
list<T> read_list(deserializer & d, R && t_reader) {
unsigned num = d.read_unsigned();
buffer<T> ls;
for (unsigned i = 0; i < num; i++)
ls.push_back(t_reader(d));
return to_list(ls.begin(), ls.end());
}
template<typename T>
list<T> read_list(deserializer & d) {
return read_list<T>(d, [](deserializer & d) { T r; d >> r; return r; });
}
}

5
src/util/list_ref.h
View file

@ -47,8 +47,6 @@ public:
friend list_ref cons(T const & h, list_ref<T> 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<typename T> size_t length(list_ref<T> const & l) {
return r;
}
template<typename T> serializer & operator<<(serializer & s, list_ref<T> const & l) { l.serialize(s); return s; }
template<typename T> list_ref<T> read_list_ref(deserializer & d) { return list_ref<T>::deserialize(d); }
template<typename T> optional<T> head_opt(list_ref<T> const & l) { return is_nil(l) ? optional<T>() : some(head(l)); }
/** \brief Given `[a_0, ..., a_k]`, return `[f a_0, ..., f a_k]`. */

9
src/util/name.h
View file

@ -11,7 +11,6 @@ Author: Leonardo de Moura
#include <algorithm>
#include <utility>
#include <lean/optional.h>
#include <lean/serializer.h>
#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<unsigned>(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<bool(name const &)> 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<name> names;
inline serializer & operator<<(serializer & s, names const & ns) { ns.serialize(s); return s; }
inline names read_names(deserializer & d) { return read_list_ref<name>(d); }
void initialize_name();
void finalize_name();

5
src/util/nat.h
View file

@ -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<nat> to_optional_nat(obj_arg o) {
@ -73,8 +71,5 @@ inline optional<nat> 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; }
};

1
src/util/object_ref.h
View file

@ -9,7 +9,6 @@ Author: Leonardo de Moura
#include <string>
#include <lean/object.h>
#include <lean/optional.h>
#include <lean/serializer.h>
namespace lean {
/* Smart point for Lean objects. It is useful for writing C++ code that manipulates Lean objects. */

7
src/util/option_ref.h
View file

@ -28,9 +28,6 @@ public:
explicit operator bool() const { return !is_scalar(raw()); }
optional<T> get() const { return *this ? some(static_cast<T const &>(cnstr_get_ref(*this, 0))) : optional<T>(); }
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<typename T> serializer & operator<<(serializer & s, option_ref<T> const & l) { l.serialize(s); return s; }
template<typename T> option_ref<T> read_option_ref(deserializer & d) { return option_ref<T>::deserialize(d); }
}

11
src/util/pair.h
View file

@ -6,7 +6,6 @@ Author: Leonardo de Moura
*/
#pragma once
#include <utility>
#include <lean/serializer.h>
namespace lean {
template<typename T1, typename T2>
@ -17,14 +16,4 @@ template<typename T1, typename T2>
inline pair<T1, T2> mk_pair(T1 const & v1, T2 const & v2) {
return std::make_pair(v1, v2);
}
template<typename T1, typename T2>
inline serializer & operator<<(serializer & s, pair<T1, T2> const & p) {
s << p.first << p.second; return s;
}
template<typename T1, typename T2>
inline deserializer & operator>>(deserializer & d, pair<T1, T2> & p) {
d >> p.first >> p.second; return d;
}
}

7
src/util/pair_ref.h
View file

@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include <lean/serializer.h>
#include "util/object_ref.h"
namespace lean {
@ -23,9 +22,6 @@ public:
T1 const & fst() const { return static_cast<T1 const &>(cnstr_get_ref(*this, 0)); }
T2 const & snd() const { return static_cast<T2 const &>(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<typename T1, typename T2> bool operator==(pair_ref<T1, T2> const & a, pair_ref<T1, T2> const & b) {
@ -40,7 +36,4 @@ template<typename T1, typename T2> bool operator<(pair_ref<T1, T2> const & a, pa
if (a.fst() != b.fst()) return a.fst() < b.fst();
else return a.snd() < b.snd();
}
template<typename T1, typename T2> serializer & operator<<(serializer & s, pair_ref<T1, T2> const & p) { p.serialize(s); return s; }
template<typename T1, typename T2> pair_ref<T1, T2> read_pair_ref(deserializer & d) { return pair_ref<T1, T2>::deserialize(d); }
}