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

Add option declarations. Add Help.

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-21 16:43:59 -07:00
parent 65898f6d5b
commit 31460aa5b8
10 changed files with 163 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
examples/ex11.lean
View file

@ -2,11 +2,11 @@ Show Options
Variable a : Bool
Variable b : Bool
Show a/\b
Set pp::notation false
Set pp::lean::notation false
Show Options
Show a/\b
Show Environment 5
Set pp::notation true
Set pp::lean::notation true
Show Options
Show a/\b

2
src/exprlib/state.h
View file

@ -52,7 +52,7 @@ struct diagnostic {
};
// hack for using std::endl with channels
struct endl_class {};
struct endl_class { endl_class() {} };
const endl_class endl;
inline regular const & operator<<(regular const & out, endl_class) {
out.m_state.get_regular_channel().get_stream() << std::endl;

66
src/frontends/lean/lean_parser.cpp
View file

@ -14,6 +14,7 @@ Author: Leonardo de Moura
#include "arith.h"
#include "printer.h"
#include "state.h"
#include "option_declarations.h"
#include "lean_frontend.h"
#include "lean_parser.h"
#include "lean_scanner.h"
@ -44,11 +45,12 @@ static name g_set_kwd("Set");
static name g_options_kwd("Options");
static name g_env_kwd("Environment");
static name g_import_kwd("Import");
static name g_help_kwd("Help");
/** \brief Table/List with all builtin command keywords */
static list<name> g_command_keywords = {g_definition_kwd, g_variable_kwd, g_theorem_kwd, g_axiom_kwd, g_universe_kwd, g_eval_kwd,
g_show_kwd, g_check_kwd, g_infix_kwd, g_infixl_kwd, g_infixr_kwd, g_prefix_kwd,
g_postfix_kwd, g_mixfixl_kwd, g_mixfixr_kwd, g_mixfixc_kwd, g_echo_kwd,
g_set_kwd, g_env_kwd, g_options_kwd, g_import_kwd};
g_set_kwd, g_env_kwd, g_options_kwd, g_import_kwd, g_help_kwd};
// ==========================================
// ==========================================
@ -799,10 +801,13 @@ class parser_fn {
type = elaborate(mk_abstraction(false, bindings, type_body));
val = elaborate(mk_abstraction(true, bindings, val_body));
}
if (is_definition)
if (is_definition) {
m_frontend.add_definition(id, type, val);
else
regular(m_frontend) << " Defined: " << id << endl;
} else {
m_frontend.add_theorem(id, type, val);
regular(m_frontend) << " Proved: " << id << endl;
}
}
/**
@ -834,6 +839,7 @@ class parser_fn {
check_colon_next("invalid variable declaration, ':' expected");
expr type = elaborate(parse_expr());
m_frontend.add_var(id, type);
regular(m_frontend) << " Assumed: " << id << endl;
}
/** \brief Parse 'Axiom' ID ':' expr */
@ -843,6 +849,7 @@ class parser_fn {
check_colon_next("invalid axiom, ':' expected");
expr type = elaborate(parse_expr());
m_frontend.add_axiom(id, type);
regular(m_frontend) << " Assumed: " << id << endl;
}
/** \brief Parse 'Eval' expr */
@ -966,27 +973,40 @@ class parser_fn {
void parse_set() {
next();
name id = check_identifier_next("invalid set options, identifier (i.e., option name) expected");
auto decl_it = get_option_declarations().find(id);
if (decl_it == get_option_declarations().end())
throw parser_error("unknown option, type 'Help Options.' for list of available options");
option_kind k = decl_it->second.kind();
switch (curr()) {
case scanner::token::Id:
if (k != BoolOption)
throw parser_error("invalid option value, given option is not Boolean");
if (curr_name() == "true")
m_frontend.set_option(id, true);
else if (curr_name() == "false")
m_frontend.set_option(id, false);
else
throw parser_error("invalid option value, 'true', 'false', string, integer or decimal value expected");
throw parser_error("invalid Boolean option value, 'true' or 'false' expected");
break;
case scanner::token::StringVal:
if (k != StringOption)
throw parser_error("invalid option value, given option is not a string");
m_frontend.set_option(id, curr_string());
break;
case scanner::token::IntVal:
if (k != IntOption && k != UnsignedOption)
throw parser_error("invalid option value, given option is not an integer");
m_frontend.set_option(id, parse_unsigned("invalid option value, value does not fit in a machine integer"));
break;
case scanner::token::DecimalVal:
if (k != DoubleOption)
throw parser_error("invalid option value, given option is not floating point value");
m_frontend.set_option(id, parse_double());
break;
default:
throw parser_error("invalid option value, 'true', 'false', string, integer or decimal value expected");
}
regular(m_frontend) << " Set option: " << id << endl;
next();
}
@ -999,6 +1019,43 @@ class parser_fn {
::lean::parse_commands(m_frontend, in, m_use_exceptions);
}
void parse_help() {
next();
if (curr() == scanner::token::CommandId) {
name opt_id = curr_name();
next();
if (opt_id == g_options_kwd) {
regular(m_frontend) << "Available options:" << endl;
for (auto p : get_option_declarations()) {
auto opt = p.second;
regular(m_frontend) << " " << opt.get_name() << " (" << opt.kind() << ") " << opt.get_description() << " (default: " << opt.get_default_value() << ")" << endl;
}
} else {
throw parser_error("invalid help command");
}
} else {
regular(m_frontend) << "Available commands:" << endl
<< " Axiom [id] : [type] assert/postulate a new axiom" << endl
<< " Check [expr] type check the given expression" << endl
<< " Definition [id] : [type] := [expr] define a new element" << endl
<< " Theorem [id] : [type] := [expr] define a new theorem" << endl
<< " Echo [string] display the given string" << endl
<< " Eval [expr] evaluate the given expression" << endl
<< " Help display this message" << endl
<< " Help Options display available options" << endl
<< " Help Notation describe commands for defining infix,mixfix,postfix operators" << endl
<< " Import [string] load the given file" << endl
<< " Set [id] [value] set option [id] with value [value]" << endl
<< " Show [expr] pretty print the given expression" << endl
<< " Show Options show current the set of assigned options" << endl
<< " Show Environment show objects in the environment, if [Num] provided, then show only the last [Num] objects" << endl
<< " Show Environment [num] show the last num objects in the environment" << endl
<< " Variable [id] : [type] declare/postulate an element of the given type" << endl
<< " Universe [id] [level] declare a new universe variable that is >= the given level" << endl
<< "Type Ctrl-D to exit" << endl;
}
}
/** \brief Parse a Lean command. */
void parse_command() {
name const & cmd_id = curr_name();
@ -1020,6 +1077,7 @@ class parser_fn {
else if (cmd_id == g_echo_kwd) parse_echo();
else if (cmd_id == g_set_kwd) parse_set();
else if (cmd_id == g_import_kwd) parse_import();
else if (cmd_id == g_help_kwd) parse_help();
else { next(); throw parser_error("invalid command"); }
}
/*@}*/

19
src/frontends/lean/lean_pp.cpp
View file

@ -63,12 +63,19 @@ static format g_in_fmt = highlight_keyword(format("in"));
static format g_assign_fmt = highlight_keyword(format(":="));
static format g_geq_fmt = format("\u2265");
static name g_pp_max_depth {"pp", "max_depth"};
static name g_pp_max_steps {"pp", "max_steps"};
static name g_pp_implicit {"pp", "implicit"};
static name g_pp_notation {"pp", "notation"};
static name g_pp_extra_lets {"pp", "extra_lets"};
static name g_pp_alias_min_weight{"pp", "alias_min_weight"};
static name g_pp_max_depth {"pp", "lean", "max_depth"};
static name g_pp_max_steps {"pp", "lean", "max_steps"};
static name g_pp_implicit {"pp", "lean", "implicit"};
static name g_pp_notation {"pp", "lean", "notation"};
static name g_pp_extra_lets {"pp", "lean", "extra_lets"};
static name g_pp_alias_min_weight{"pp", "lean", "alias_min_weight"};
RegisterUnsignedOption(g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH, "(lean pretty printer) maximum expression depth, after that it will use ellipsis");
RegisterUnsignedOption(g_pp_max_steps, LEAN_DEFAULT_PP_MAX_STEPS, "(lean pretty printer) maximum number of visited expressions, after that it will use ellipsis");
RegisterBoolOption(g_pp_implicit, LEAN_DEFAULT_PP_IMPLICIT, "(lean pretty printer) display implicit parameters");
RegisterBoolOption(g_pp_notation, LEAN_DEFAULT_PP_NOTATION, "(lean pretty printer) disable/enable notation (infix, mixfix, postfix operators and unicode characters)");
RegisterBoolOption(g_pp_extra_lets, LEAN_DEFAULT_PP_EXTRA_LETS, "(lean pretty printer) introduce extra let expressions when displaying shared terms");
RegisterUnsignedOption(g_pp_alias_min_weight, LEAN_DEFAULT_PP_ALIAS_MIN_WEIGHT, "(lean pretty printer) mimimal weight (approx. size) of a term to be considered a shared term");
unsigned get_pp_max_depth(options const & opts) { return opts.get_unsigned(g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH); }
unsigned get_pp_max_steps(options const & opts) { return opts.get_unsigned(g_pp_max_steps, LEAN_DEFAULT_PP_MAX_STEPS); }

1
src/shell/lean.cpp
View file

@ -8,6 +8,7 @@ using namespace lean;
int main(int argc, char ** argv) {
std::cout << "Lean (version " << LEAN_VERSION_MAJOR << "." << LEAN_VERSION_MINOR << ")\n";
std::cout << "Type Ctrl-D to exit or 'Help.' for help."<< std::endl;
frontend f;
if (argc == 1) {
return parse_commands(f, std::cin) ? 0 : 1;

8
src/tests/frontends/lean/lean_pp.cpp
View file

@ -38,7 +38,7 @@ static void tst2() {
expr g = Const("g");
std::cout << fmt(g(t, t, t)) << std::endl;
formatter fmt2 = mk_pp_formatter(f);
std::cout << fmt2(g(t, t, t), options({"pp", "alias_min_weight"}, 100)) << std::endl;
std::cout << fmt2(g(t, t, t), options({"pp", "lean", "alias_min_weight"}, 100)) << std::endl;
}
static void tst3() {
@ -64,7 +64,7 @@ static void tst4() {
regular(s1) << And(Const("a"), Const("b")) << "\n";
regular(f) << And(Const("a"), Const("b")) << "\n";
diagnostic(f) << And(Const("a"), Const("b")) << "\n";
f.set_option(name{"pp", "notation"}, false);
f.set_option(name{"pp", "lean", "notation"}, false);
regular(f) << And(Const("a"), Const("b")) << "\n";
regular(s1) << And(Const("a"), Const("b")) << "\n";
regular(s2) << And(Const("a"), Const("b")) << "\n";
@ -76,7 +76,7 @@ static void tst5() {
f.set_regular_channel(out);
regular(f) << And(Const("a"), Const("b"));
lean_assert(out->str() == "a ∧ b");
f.set_option(name{"pp", "notation"}, false);
f.set_option(name{"pp", "lean", "notation"}, false);
regular(f) << " " << And(Const("a"), Const("b"));
lean_assert(out->str() == "a ∧ b and a b");
}
@ -93,7 +93,7 @@ static void tst6() {
std::shared_ptr<string_output_channel> out(new string_output_channel());
f.set_regular_channel(out);
expr t = mk_deep(10);
f.set_option(name{"pp", "max_depth"}, 5);
f.set_option(name{"pp", "lean", "max_depth"}, 5);
f.set_option(name{"pp", "colors"}, false);
regular(f) << t;
lean_assert(out->str() == "f (f (f (f (f (…)))))");

4
src/util/sexpr/format.cpp
View file

@ -40,6 +40,10 @@ static name g_pp_indent{"pp", "indent"};
static name g_pp_colors{"pp", "colors"};
static name g_pp_width{"pp", "width"};
RegisterUnsignedOption(g_pp_indent, LEAN_DEFAULT_PP_INDENTATION, "(pretty printer) default indentation");
RegisterBoolOption(g_pp_colors, LEAN_DEFAULT_PP_COLORS, "(pretty printer) use colors");
RegisterUnsignedOption(g_pp_width, LEAN_DEFAULT_PP_WIDTH, "(pretty printer) line width");
unsigned get_pp_indent(options const & o) {
return o.get_unsigned(g_pp_indent, LEAN_DEFAULT_PP_INDENTATION);
}

32
src/util/sexpr/option_declarations.h Normal file
View file

@ -0,0 +1,32 @@
/*
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 <map>
#include "options.h"
namespace lean {
/**
\brief Datastructure for storing information about available
configuration options.
*/
class option_declaration {
name m_name;
option_kind m_kind;
std::string m_default;
std::string m_description;
public:
option_declaration(name const & n, option_kind k, char const * default_val, char const * descr):
m_name(n), m_kind(k), m_default(default_val), m_description(descr) {}
option_kind kind() const { return m_kind; }
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; }
};
typedef std::map<name, option_declaration> option_declarations;
option_declarations const & get_option_declarations();
}

29
src/util/sexpr/options.cpp
View file

@ -4,10 +4,39 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <memory>
#include "options.h"
#include "option_declarations.h"
#include "sexpr_funcs.h"
namespace lean {
std::ostream & operator<<(std::ostream & out, option_kind k) {
switch (k) {
case BoolOption: out << "Bool"; break;
case IntOption: out << "Int"; break;
case UnsignedOption: out << "Unsigned Int"; break;
case DoubleOption: out << "Double"; break;
case StringOption: out << "String"; break;
case SExprOption: out << "S-Expression"; break;
}
return out;
}
static std::unique_ptr<option_declarations> g_option_declarations;
option_declarations & get_option_declarations_core() {
if (!g_option_declarations)
g_option_declarations.reset(new option_declarations());
return *g_option_declarations;
}
option_declarations const & get_option_declarations() {
return get_option_declarations_core();
}
mk_option_declaration::mk_option_declaration(name const & n, option_kind k, char const * default_value, char const * description) {
get_option_declarations_core().insert(mk_pair(n, option_declaration(n, k, default_value, description)));
}
bool options::empty() const {
return is_nil(m_value);

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

@ -11,6 +11,9 @@ Author: Leonardo de Moura
#include "name.h"
namespace lean {
enum option_kind { BoolOption, IntOption, UnsignedOption, DoubleOption, StringOption, SExprOption };
std::ostream & operator<<(std::ostream & out, option_kind k);
/** \brief Configuration options. */
class options {
sexpr m_value;
@ -59,4 +62,16 @@ public:
friend std::ostream & operator<<(std::ostream & out, options const & o);
};
template<typename T> options update(options const & o, name const & n, T const & v) { return o.update(n, sexpr(v)); }
struct mk_option_declaration {
mk_option_declaration(name const & n, option_kind k, char const * default_value, char const * description);
};
#define LEAN_MAKE_OPTION_NAME_CORE(LINE) LEAN_OPTION_ ## LINE
#define LEAN_MAKE_OPTION_NAME(LINE) LEAN_MAKE_OPTION_NAME_CORE(LINE)
#define LEAN_OPTION_UNIQUE_NAME LEAN_MAKE_OPTION_NAME(__LINE__)
#define RegisterOption(N,K,D,DESC) ::lean::mk_option_declaration LEAN_OPTION_UNIQUE_NAME(N,K,D,DESC)
#define RegisterOptionCore(N,K,D,DESC) RegisterOption(N,K,#D,DESC)
#define RegisterBoolOption(N,D,DESC) RegisterOptionCore(N, BoolOption, D, DESC);
#define RegisterUnsignedOption(N,D,DESC) RegisterOptionCore(N, UnsignedOption, D, DESC);
}