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

Change lean frontend specific options. Now, frontend specific options must begin with the frontend name.

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-22 10:55:55 -07:00
parent 0f6a7e4a95
commit f1462dc51e
3 changed files with 12 additions and 12 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::lean::notation false
Set lean::pp::notation false
Show Options
Show a/\b
Show Environment 5
Set pp::lean::notation true
Set lean::pp::notation true
Show Options
Show a/\b

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

@ -63,12 +63,12 @@ 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", "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"};
static name g_pp_max_depth {"lean", "pp", "max_depth"};
static name g_pp_max_steps {"lean", "pp", "max_steps"};
static name g_pp_implicit {"lean", "pp", "implicit"};
static name g_pp_notation {"lean", "pp", "notation"};
static name g_pp_extra_lets {"lean", "pp", "extra_lets"};
static name g_pp_alias_min_weight{"lean", "pp", "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");

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", "lean", "alias_min_weight"}, 100)) << std::endl;
std::cout << fmt2(g(t, t, t), options({"lean", "pp", "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", "lean", "notation"}, false);
f.set_option(name{"lean", "pp", "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", "lean", "notation"}, false);
f.set_option(name{"lean", "pp", "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", "lean", "max_depth"}, 5);
f.set_option(name{"lean", "pp", "max_depth"}, 5);
f.set_option(name{"pp", "colors"}, false);
regular(f) << t;
lean_assert(out->str() == "f (f (f (f (f (…)))))");