From 64c3ba7b743558b47739024b0f445b388bda0bba Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 30 Oct 2014 13:28:25 -0700
Subject: [PATCH] feat(frontends/lean): display metavariable application
 arguments in check command

The idea is to "fix" counter-intuitive output like the ones were
produced in the tests check.lean and check2.lean
---
 src/frontends/lean/builtin_cmds.cpp | 4 +++-
 src/frontends/lean/pp_options.cpp   | 1 +
 src/frontends/lean/pp_options.h     | 1 +
 tests/lean/check.lean.expected.out  | 2 +-
 tests/lean/check2.lean.expected.out | 2 +-
 5 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index ab886b426..ed2d060b1 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -218,8 +218,10 @@ environment check_cmd(parser & p) {
     auto tc = mk_type_checker(p.env(), p.mk_ngen(), true);
     expr type = tc->check(e, ls).first;
     auto reg              = p.regular_stream();
-    formatter const & fmt = reg.get_formatter();
+    formatter fmt         = reg.get_formatter();
     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);
     format r = group(fmt(e) + space() + colon() + nest(indent, line() + fmt(type)));
     reg << mk_pair(r, opts) << endl;
diff --git a/src/frontends/lean/pp_options.cpp b/src/frontends/lean/pp_options.cpp
index a4c0a8dcf..81b2a67f6 100644
--- a/src/frontends/lean/pp_options.cpp
+++ b/src/frontends/lean/pp_options.cpp
@@ -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_universes_option_name() { return *g_pp_universes; }
 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_steps(options const & opts)     { return opts.get_unsigned(*g_pp_max_steps, LEAN_DEFAULT_PP_MAX_STEPS); }
diff --git a/src/frontends/lean/pp_options.h b/src/frontends/lean/pp_options.h
index f60718721..141f4cffe 100644
--- a/src/frontends/lean/pp_options.h
+++ b/src/frontends/lean/pp_options.h
@@ -11,6 +11,7 @@ name const & get_pp_coercions_option_name();
 name const & get_pp_full_names_option_name();
 name const & get_pp_universes_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_steps(options const & opts);
diff --git a/tests/lean/check.lean.expected.out b/tests/lean/check.lean.expected.out
index 4f4683182..34ad91a3f 100644
--- a/tests/lean/check.lean.expected.out
+++ b/tests/lean/check.lean.expected.out
@@ -1,4 +1,4 @@
 and.intro : ?a → ?b → ?a ∧ ?b
 or.elim : ?a ∨ ?b → (?a → ?c) → (?b → ?c) → ?c
 eq : ?A → ?A → Prop
-eq.rec : ?C → (Π {a : ?A}, ?a = a → ?C)
+eq.rec : ?C ?a → (Π {a : ?A}, ?a = a → ?C a)
diff --git a/tests/lean/check2.lean.expected.out b/tests/lean/check2.lean.expected.out
index 68a1c254e..e04c8a2e7 100644
--- a/tests/lean/check2.lean.expected.out
+++ b/tests/lean/check2.lean.expected.out
@@ -1 +1 @@
-eq.rec_on : ?a = ?a_1 → ?C → ?C
+eq.rec_on : ?a = ?a_1 → ?C ?a → ?C ?a_1