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

refactor(frontends/lean/server): move option display_value to option_declarations

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-09-02 17:42:21 -07:00
parent b8c34eceed
commit 24fc89ff70
4 changed files with 59 additions and 42 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

42
src/frontends/lean/server.cpp
View file

@ -396,47 +396,7 @@ void server::show_options() {
for (auto it = decls.begin(); it != decls.end(); it++) {
option_declaration const & d = it->second;
m_out << "-- " << d.get_name() << "|" << d.kind() << "|";
bool contains = false;
if (o.contains(d.get_name())) {
sexpr s = o.get_sexpr(d.get_name());
switch (d.kind()) {
case BoolOption:
if (!is_nil(s) && is_bool(s)) {
m_out << (to_bool(s) ? "true" : "false");
contains = true;
}
break;
case IntOption:
if (!is_nil(s) && is_int(s)) {
m_out << to_int(s);
contains = true;
}
break;
case UnsignedOption:
if (!is_nil(s) && is_int(s)) {
m_out << static_cast<unsigned>(to_int(s));
contains = true;
}
break;
case DoubleOption:
if (!is_nil(s) && is_double(s)) {
m_out << to_double(s);
contains = true;
}
break;
case StringOption:
if (!is_nil(s) && is_string(s)) {
m_out << to_string(s);
contains = true;
}
break;
case SExprOption:
m_out << mk_pair(flatten(pp(s)), o);
contains = true;
}
}
if (!contains)
m_out << d.get_default_value();
d.display_value(m_out, o);
m_out << "|" << d.get_description() << "\n";
}
m_out << "-- ENDOPTIONS" << std::endl;

2
src/util/sexpr/CMakeLists.txt
View file

@ -1,2 +1,2 @@
add_library(sexpr sexpr.cpp sexpr_fn.cpp format.cpp options.cpp)
add_library(sexpr sexpr.cpp sexpr_fn.cpp format.cpp options.cpp option_declarations.cpp)
target_link_libraries(sexpr ${LEAN_LIBS})

54
src/util/sexpr/option_declarations.cpp Normal file
View file

@ -0,0 +1,54 @@
/*
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "util/sexpr/option_declarations.h"
#include "util/sexpr/format.h"
namespace lean {
void option_declaration::display_value(std::ostream & out, options const & o) const {
bool contains = false;
if (o.contains(get_name())) {
sexpr s = o.get_sexpr(get_name());
switch (kind()) {
case BoolOption:
if (!is_nil(s) && is_bool(s)) {
out << (to_bool(s) ? "true" : "false");
contains = true;
}
break;
case IntOption:
if (!is_nil(s) && is_int(s)) {
out << to_int(s);
contains = true;
}
break;
case UnsignedOption:
if (!is_nil(s) && is_int(s)) {
out << static_cast<unsigned>(to_int(s));
contains = true;
}
break;
case DoubleOption:
if (!is_nil(s) && is_double(s)) {
out << to_double(s);
contains = true;
}
break;
case StringOption:
if (!is_nil(s) && is_string(s)) {
out << to_string(s);
contains = true;
}
break;
case SExprOption:
out << mk_pair(flatten(pp(s)), o);
contains = true;
}
}
if (!contains)
out << get_default_value();
}
}

3
src/util/sexpr/option_declarations.h
View file

@ -26,6 +26,9 @@ public:
name const & get_name() const { return m_name; }
std::string const & get_default_value() const { return m_default; }
std::string const & get_description() const { return m_description; }
/** \brief Display value of this option declaration in \c o.
\remark if \c o does not set this option, then the default value is displayed. */
void display_value(std::ostream & out, options const & o) const;
};
typedef std::map<name, option_declaration> option_declarations;