Fix problem with pretty printer. Add another test for elaborator

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/lean_frontend.cpp

@@ -297,6 +297,10 @@ struct frontend::imp {
         }
     }
 
+    bool is_explicit(name const & n) {
+        return !n.is_atomic() && get_explicit_version(n.get_prefix()) == n;
+    }
+
     void add_coercion(expr const & f) {
         expr type      = m_env.infer_type(f);
         expr norm_type = m_env.normalize(type);
@@ -412,6 +416,7 @@ void frontend::mark_implicit_arguments(name const & n, std::initializer_list<boo
 bool frontend::has_implicit_arguments(name const & n) const { return m_imp->has_implicit_arguments(n); }
 std::vector<bool> const & frontend::get_implicit_arguments(name const & n) const { return m_imp->get_implicit_arguments(n); }
 name const & frontend::get_explicit_version(name const & n) const { return m_imp->get_explicit_version(n); }
+bool frontend::is_explicit(name const & n) const { return m_imp->is_explicit(n); }
 
 void frontend::add_coercion(expr const & f) { m_imp->add_coercion(f); }
 expr frontend::get_coercion(expr const & given_type, expr const & expected_type, context const & ctx) const {

src/frontends/lean/lean_frontend.h

@@ -147,6 +147,11 @@ public:
         arguments.
     */
     name const & get_explicit_version(name const & n) const;
+    /**
+       \brief Return true iff \c n is the name of the "explicit"
+       version of an object with implicit arguments
+    */
+    bool is_explicit(name const & n) const;
     /*@}*/
 
     /**

src/frontends/lean/lean_pp.cpp

@@ -1182,7 +1182,15 @@ class pp_formatter_cell : public formatter_cell {
     }
 
     format pp_definition(object const & obj, options const & opts) {
-        return pp_compact_definition(obj.keyword(), obj.get_name(), obj.get_type(), obj.get_value(), opts);
+        if (m_frontend.is_explicit(obj.get_name())) {
+            // Hide implicit arguments when pretty printing the
+            // explicit version on an object.
+            // We do that because otherwise it looks like a recursive definition.
+            options new_opts = update(opts, g_pp_implicit, false);
+            return pp_compact_definition(obj.keyword(), obj.get_name(), obj.get_type(), obj.get_value(), new_opts);
+        } else {
+            return pp_compact_definition(obj.keyword(), obj.get_name(), obj.get_type(), obj.get_value(), opts);
+        }
     }
 
     format pp_notation_decl(object const & obj, options const & opts) {

tests/lean/elab4.lean

@@ -0,0 +1,12 @@
+Variable C {A B : Type} (H : A = B) (a : A) : B
+
+Variable D {A A' : Type} {B : A -> Type} {B' : A' -> Type} (H : (Pi x : A, B x) = (Pi x : A', B' x)) : A = A'
+
+Variable R {A A' : Type} {B : A -> Type} {B' : A' -> Type} (H : (Pi x : A, B x) = (Pi x : A', B' x)) (a : A) :
+             (B a) = (B' (C (D H) a))
+
+Theorem R2 : Pi (A1 A2 B1 B2 : Type) (H : A1 -> B1 = A2 -> B2) (a : A1), B1 = B2 :=
+    fun A1 A2 B1 B2 H a, R H a
+
+Set pp::implicit true
+Show Environment 7.

tests/lean/elab4.lean.expected.out

@@ -0,0 +1,23 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: C
+  Assumed: D
+  Assumed: R
+  Proved: R2
+  Set: lean::pp::implicit
+Variable C {A B : Type} (H : A = B) (a : A) : B
+Definition C::explicit (A B : Type) (H : A = B) (a : A) : B := C H a
+Variable D {A A' : Type} {B : A → Type} {B' : A' → Type} (H : (Π x : A, B x) = (Π x : A', B' x)) : A = A'
+Definition D::explicit (A A' : Type) (B : A → Type) (B' : A' → Type) (H : (Π x : A, B x) = (Π x : A', B' x)) : A =
+    A' :=
+    D H
+Variable R {A A' : Type} {B : A → Type} {B' : A' → Type} (H : (Π x : A, B x) = (Π x : A', B' x)) (a : A) :
+    (B a) = (B' (C::explicit A A' (D::explicit A A' B B' H) a))
+Definition R::explicit (A A' : Type)
+    (B : A → Type)
+    (B' : A' → Type)
+    (H : (Π x : A, B x) = (Π x : A', B' x))
+    (a : A) : (B a) = (B' (C (D H) a)) :=
+    R H a
+Theorem R2 (A1 A2 B1 B2 : Type) (H : A1 → B1 = A2 → B2) (a : A1) : B1 = B2 :=
+    R::explicit A1 A2 (λ a : A1, B1) (λ _ : A2, B2) H a

tests/lean/tst6.lean.expected.out

@@ -14,8 +14,7 @@ Theorem CongrH {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h
         b2
         (Congr::explicit N (λ x : N, N → N) h h a1 b1 (Refl::explicit (N → N → N) h) H1)
         H2
-Theorem CongrH::explicit (a1 a2 b1 b2 : N) (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) :=
-    CongrH::explicit a1 a2 b1 b2 H1 H2
+Theorem CongrH::explicit (a1 a2 b1 b2 : N) (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) := CongrH H1 H2
   Set: lean::pp::implicit
 Theorem CongrH {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) := Congr (Congr (Refl h) H1) H2
 Theorem CongrH::explicit (a1 a2 b1 b2 : N) (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) := CongrH H1 H2