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

feat(frontends/lean): display metavariable application arguments in check command

Browse source 
The idea is to "fix" counter-intuitive output like the ones were
produced in the tests check.lean and check2.lean
This commit is contained in:
Leonardo de Moura 2014-10-30 13:28:25 -07:00
parent dcd7e53fa7
commit 64c3ba7b74
5 changed files with 7 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/frontends/lean/builtin_cmds.cpp
View file

@ -218,8 +218,10 @@ environment check_cmd(parser & p) {
auto tc = mk_type_checker(p.env(), p.mk_ngen(), true); auto tc = mk_type_checker(p.env(), p.mk_ngen(), true);
expr type = tc->check(e, ls).first; expr type = tc->check(e, ls).first;
auto reg = p.regular_stream(); auto reg = p.regular_stream();
formatter const & fmt = reg.get_formatter(); formatter fmt = reg.get_formatter();
options opts = p.ios().get_options(); options opts = p.ios().get_options();
opts = opts.update(get_pp_metavar_args_name(), true);
fmt = fmt.update_options(opts);
unsigned indent = get_pp_indent(opts); unsigned indent = get_pp_indent(opts);
format r = group(fmt(e) + space() + colon() + nest(indent, line() + fmt(type))); format r = group(fmt(e) + space() + colon() + nest(indent, line() + fmt(type)));
reg << mk_pair(r, opts) << endl; reg << mk_pair(r, opts) << endl;

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

@ -121,6 +121,7 @@ name const & get_pp_coercions_option_name() { return *g_pp_coercions; }
name const & get_pp_full_names_option_name() { return *g_pp_full_names; } name const & get_pp_full_names_option_name() { return *g_pp_full_names; }
name const & get_pp_universes_option_name() { return *g_pp_universes; } name const & get_pp_universes_option_name() { return *g_pp_universes; }
name const & get_pp_notation_option_name() { return *g_pp_notation; } name const & get_pp_notation_option_name() { return *g_pp_notation; }
name const & get_pp_metavar_args_name() { return *g_pp_metavar_args; }
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_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); } unsigned get_pp_max_steps(options const & opts) { return opts.get_unsigned(*g_pp_max_steps, LEAN_DEFAULT_PP_MAX_STEPS); }

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

@ -11,6 +11,7 @@ name const & get_pp_coercions_option_name();
name const & get_pp_full_names_option_name(); name const & get_pp_full_names_option_name();
name const & get_pp_universes_option_name(); name const & get_pp_universes_option_name();
name const & get_pp_notation_option_name(); name const & get_pp_notation_option_name();
name const & get_pp_metavar_args_name();
unsigned get_pp_max_depth(options const & opts); unsigned get_pp_max_depth(options const & opts);
unsigned get_pp_max_steps(options const & opts); unsigned get_pp_max_steps(options const & opts);

2
tests/lean/check.lean.expected.out
View file

@ -1,4 +1,4 @@
and.intro : ?a → ?b → ?a ∧ ?b and.intro : ?a → ?b → ?a ∧ ?b
or.elim : ?a ∨ ?b → (?a → ?c) → (?b → ?c) → ?c or.elim : ?a ∨ ?b → (?a → ?c) → (?b → ?c) → ?c
eq : ?A → ?A → Prop eq : ?A → ?A → Prop
eq.rec : ?C → (Π {a : ?A}, ?a = a → ?C) eq.rec : ?C ?a → (Π {a : ?A}, ?a = a → ?C a)

2
tests/lean/check2.lean.expected.out
View file

@ -1 +1 @@
eq.rec_on : ?a = ?a_1 → ?C → ?C eq.rec_on : ?a = ?a_1 → ?C ?a → ?C ?a_1