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

chore(frontend/lean/pp_options): use consistent name convention for pp option names

Browse source
This commit is contained in:
Leonardo de Moura 2014-09-08 08:30:08 -07:00
parent b460c02017
commit 4088cdc139
8 changed files with 19 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/info_manager.cpp
View file

@ -187,7 +187,7 @@ public:
virtual void display(io_state_stream const & ios, unsigned line) const {
ios << "-- COERCION|" << line << "|" << get_column() << "\n";
options os = ios.get_options();
os = os.update(get_pp_coercion_option_name(), true);
os = os.update(get_pp_coercions_option_name(), true);
ios.update_options(os) << m_expr << endl << "--" << endl << m_type << endl;
ios << "-- ACK" << endl;
}

2
src/frontends/lean/pp.cpp
View file

@ -114,7 +114,7 @@ void pretty_fn::set_options_core(options const & o) {
m_max_steps = get_pp_max_steps(o);
m_implict = get_pp_implicit(o);
m_unicode = get_pp_unicode(o);
m_coercion = get_pp_coercion(o);
m_coercion = get_pp_coercions(o);
m_notation = get_pp_notation(o);
m_universes = get_pp_universes(o);
m_full_names = get_pp_full_names(o);

22
src/frontends/lean/pp_options.cpp
View file

@ -22,8 +22,8 @@ Author: Leonardo de Moura
#define LEAN_DEFAULT_PP_IMPLICIT false
#endif
#ifndef LEAN_DEFAULT_PP_COERCION
#define LEAN_DEFAULT_PP_COERCION false
#ifndef LEAN_DEFAULT_PP_COERCIONS
#define LEAN_DEFAULT_PP_COERCIONS false
#endif
#ifndef LEAN_DEFAULT_PP_UNIVERSES
@ -47,24 +47,24 @@ static name g_pp_max_depth {"pp", "max_depth"};
static name g_pp_max_steps {"pp", "max_steps"};
static name g_pp_notation {"pp", "notation"};
static name g_pp_implicit {"pp", "implicit"};
static name g_pp_coercion {"pp", "coercion"};
static name g_pp_coercions {"pp", "coercions"};
static name g_pp_universes {"pp", "universes"};
static name g_pp_full_names {"pp", "full_names"};
static name g_pp_private_names {"pp", "private_names"};
static name g_pp_metavar_args {"pp", "metavar_args"};
name const & get_pp_coercion_option_name() { return g_pp_coercion; }
name const & get_pp_coercions_option_name() { return g_pp_coercions; }
name const & get_pp_full_names_option_name() { return g_pp_full_names; }
list<options> const & get_distinguishing_pp_options() {
static options g_universes_true(g_pp_universes, true);
static options g_implicit_true(g_pp_implicit, true);
static options g_coercion_true(g_pp_coercion, true);
static options g_coercions_true(g_pp_coercions, true);
static options g_notation_false(g_pp_notation, false);
static options g_implicit_coercion = join(g_coercion_true, g_implicit_true);
static options g_implicit_coercions = join(g_coercions_true, g_implicit_true);
static options g_implicit_notation = join(g_notation_false, g_implicit_true);
static options g_all = join(join(g_universes_true, g_implicit_true), join(g_coercion_true, g_notation_false));
static list<options> g_distinguishing_pp_options({g_implicit_true, g_coercion_true, g_implicit_coercion, g_implicit_notation, g_universes_true, g_all});
static options g_all = join(join(g_universes_true, g_implicit_true), join(g_coercions_true, g_notation_false));
static list<options> g_distinguishing_pp_options({g_implicit_true, g_coercions_true, g_implicit_coercions, g_implicit_notation, g_universes_true, g_all});
return g_distinguishing_pp_options;
}
@ -76,8 +76,8 @@ RegisterBoolOption(g_pp_notation, LEAN_DEFAULT_PP_NOTATION,
"(pretty printer) disable/enable notation (infix, mixfix, postfix operators and unicode characters)");
RegisterBoolOption(g_pp_implicit, LEAN_DEFAULT_PP_IMPLICIT,
"(pretty printer) display implicit parameters");
RegisterBoolOption(g_pp_coercion, LEAN_DEFAULT_PP_COERCION,
"(pretty printer) display coercions");
RegisterBoolOption(g_pp_coercions, LEAN_DEFAULT_PP_COERCIONS,
"(pretty printer) display coercionss");
RegisterBoolOption(g_pp_universes, LEAN_DEFAULT_PP_UNIVERSES,
"(pretty printer) display universes");
RegisterBoolOption(g_pp_full_names, LEAN_DEFAULT_PP_FULL_NAMES,
@ -91,7 +91,7 @@ unsigned get_pp_max_depth(options const & opts) { return opts.get_unsigned(g
unsigned get_pp_max_steps(options const & opts) { return opts.get_unsigned(g_pp_max_steps, LEAN_DEFAULT_PP_MAX_STEPS); }
bool get_pp_notation(options const & opts) { return opts.get_bool(g_pp_notation, LEAN_DEFAULT_PP_NOTATION); }
bool get_pp_implicit(options const & opts) { return opts.get_bool(g_pp_implicit, LEAN_DEFAULT_PP_IMPLICIT); }
bool get_pp_coercion(options const & opts) { return opts.get_bool(g_pp_coercion, LEAN_DEFAULT_PP_COERCION); }
bool get_pp_coercions(options const & opts) { return opts.get_bool(g_pp_coercions, LEAN_DEFAULT_PP_COERCIONS); }
bool get_pp_universes(options const & opts) { return opts.get_bool(g_pp_universes, LEAN_DEFAULT_PP_UNIVERSES); }
bool get_pp_full_names(options const & opts) { return opts.get_bool(g_pp_full_names, LEAN_DEFAULT_PP_FULL_NAMES); }
bool get_pp_private_names(options const & opts) { return opts.get_bool(g_pp_private_names, LEAN_DEFAULT_PP_PRIVATE_NAMES); }

4
src/frontends/lean/pp_options.h
View file

@ -7,14 +7,14 @@ Author: Leonardo de Moura
#pragma once
#include "util/sexpr/options.h"
namespace lean {
name const & get_pp_coercion_option_name();
name const & get_pp_coercions_option_name();
name const & get_pp_full_names_option_name();
unsigned get_pp_max_depth(options const & opts);
unsigned get_pp_max_steps(options const & opts);
bool get_pp_notation(options const & opts);
bool get_pp_implicit(options const & opts);
bool get_pp_coercion(options const & opts);
bool get_pp_coercions(options const & opts);
bool get_pp_universes(options const & opts);
bool get_pp_full_names(options const & opts);
bool get_pp_private_names(options const & opts);

2
tests/lean/run/choice_ctx.lean
View file

@ -1,7 +1,7 @@
import data.nat.basic
open nat
open eq
set_option pp.coercion true
set_option pp.coercions true
namespace foo
theorem trans {a b c : nat} (H1 : a = b) (H2 : b = c) : a = c :=

2
tests/lean/run/class_coe.lean
View file

@ -29,7 +29,7 @@ coercion nat_to_int
coercion int_to_real
set_option pp.implicit true
set_option pp.coercion true
set_option pp.coercions true
check n + m
check i + j
check x + y

2
tests/lean/run/coe1.lean
View file

@ -6,7 +6,7 @@ variable g : B → B → B
variables a1 a2 a3 : A
variables b1 b2 b3 : B
check g a1 b1
set_option pp.coercion true
set_option pp.coercions true
check g a1 b1
variable eq {A : Type} : A → A → Type.{0}

2
tests/lean/run/coe6.lean
View file

@ -10,6 +10,6 @@ variable nsucc : nat → nat
definition f [coercion] (a : unit) : int := izero
definition g [coercion] (a : unit) : nat := nzero
set_option pp.coercion true
set_option pp.coercions true
check isucc star
check nsucc star