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

feat(util/sexpr/options): serialization for options

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-27 20:40:00 -08:00
parent dbebb4a4a1
commit 3715b10ce7
2 changed files with 28 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/tests/util/options.cpp
View file

@ -20,6 +20,19 @@ static void tst1() {
std::cout << opt << "\n"; std::cout << opt << "\n";
} }
static void check_serializer(options const & o) {
std::ostringstream out;
serializer s(out);
s << o << o;
std::istringstream in(out.str());
deserializer d(in);
options n1, n2;
d >> n1 >> n2;
lean_assert(o == n1);
lean_assert(o == n2);
lean_assert(is_eqp(n1, n2));
}
static void tst2() { static void tst2() {
options opt; options opt;
opt = update(opt, name{"test", "foo"}, 10); opt = update(opt, name{"test", "foo"}, 10);
@ -29,6 +42,7 @@ static void tst2() {
opt = update(opt, name{"sp", "order"}, sexpr{s, s, s, s, s, s}); opt = update(opt, name{"sp", "order"}, sexpr{s, s, s, s, s, s});
opt = update(opt, name{"test", "long", "names", "with", "several", "parts"}, true); opt = update(opt, name{"test", "long", "names", "with", "several", "parts"}, true);
std::cout << pp(opt) << "\n"; std::cout << pp(opt) << "\n";
check_serializer(opt);
} }
static void tst3() { static void tst3() {
@ -40,6 +54,7 @@ static void tst3() {
std::cout << pp(opt) << "\n"; std::cout << pp(opt) << "\n";
opt = update(opt, name{"color"}, 30); opt = update(opt, name{"color"}, 30);
std::cout << pp(opt) << "\n"; std::cout << pp(opt) << "\n";
check_serializer(opt);
} }
static void tst4() { static void tst4() {
@ -86,11 +101,13 @@ static void tst4() {
lean_assert(opt.contains("name")); lean_assert(opt.contains("name"));
lean_assert(!opt.contains("name2")); lean_assert(!opt.contains("name2"));
lean_assert(opt.contains("color")); lean_assert(opt.contains("color"));
check_serializer(opt);
options opt2; options opt2;
opt2 = update(opt2, "name", "Leo"); opt2 = update(opt2, "name", "Leo");
opt2 = update(opt2, "value", 10); opt2 = update(opt2, "value", 10);
opt2 = update(opt2, "flag", false); opt2 = update(opt2, "flag", false);
std::cout << "# " << opt << "\n# " << opt2 << "\n"; std::cout << "# " << opt << "\n# " << opt2 << "\n";
check_serializer(opt2);
options opt3 = join(opt, opt2); options opt3 = join(opt, opt2);
std::cout << "> " << opt3 << "\n"; std::cout << "> " << opt3 << "\n";
lean_assert(strcmp(opt3.get_string("name", ""), "Leo") == 0); lean_assert(strcmp(opt3.get_string("name", ""), "Leo") == 0);
@ -98,6 +115,7 @@ static void tst4() {
lean_assert(opt3.get_unsigned("color", 0) == 3); lean_assert(opt3.get_unsigned("color", 0) == 3);
lean_assert(opt3.get_double(name("freq"), 0.0) == 0.5); lean_assert(opt3.get_double(name("freq"), 0.0) == 0.5);
lean_assert(opt3.get_unsigned(name("freq"), 0) == 0); lean_assert(opt3.get_unsigned(name("freq"), 0) == 0);
check_serializer(opt3);
std::ostringstream s; std::ostringstream s;
option_kind k; option_kind k;
k = BoolOption; s << k << " "; k = BoolOption; s << k << " ";
@ -133,6 +151,7 @@ static void tst6() {
lean_assert(!is_eqp(opt, opt2)); lean_assert(!is_eqp(opt, opt2));
opt2 = opt; opt2 = opt;
lean_assert(is_eqp(opt, opt2)); lean_assert(is_eqp(opt, opt2));
check_serializer(opt);
} }
int main() { int main() {

9
src/util/sexpr/options.h
View file

@ -10,6 +10,7 @@ Author: Leonardo de Moura
#include "util/sexpr/sexpr.h" #include "util/sexpr/sexpr.h"
#include "util/sexpr/format.h" #include "util/sexpr/format.h"
#include "util/lua.h" #include "util/lua.h"
#include "util/serializer.h"
namespace lean { namespace lean {
enum option_kind { BoolOption, IntOption, UnsignedOption, DoubleOption, StringOption, SExprOption }; enum option_kind { BoolOption, IntOption, UnsignedOption, DoubleOption, StringOption, SExprOption };
@ -63,7 +64,15 @@ public:
friend format pp(options const & o); friend format pp(options const & o);
friend std::ostream & operator<<(std::ostream & out, options const & o); friend std::ostream & operator<<(std::ostream & out, options const & o);
friend serializer & operator<<(serializer & s, options const & o) { s << o.m_value; return s; }
friend options read_options(deserializer & d);
friend bool operator==(options const & a, options const & b) { return a.m_value == b.m_value; }
}; };
inline options read_options(deserializer & d) { return options(read_sexpr(d)); }
inline deserializer & operator>>(deserializer & d, options & o) { o = read_options(d); return d; }
template<typename T> options update(options const & o, name const & n, T const & v) { return o.update(n, sexpr(v)); } template<typename T> options update(options const & o, name const & n, T const & v) { return o.update(n, sexpr(v)); }
struct mk_option_declaration { struct mk_option_declaration {