feat(frontends/lean): relax restricitions on parsing applications of functions containing implicit arguments

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

src/frontends/lean/parser.cpp

@@ -765,9 +765,11 @@ class parser::imp {
                     pos_info p = pos();
                     expr f = (k == object_kind::Builtin) ? obj->get_value() : mk_constant(obj->get_name());
                     args.push_back(save(f, p));
-                    // We parse all the arguments to make sure we
-                    // get all explicit arguments.
-                    for (unsigned i = 0; i < imp_args.size(); i++) {
+                    // We parse the arguments until we find the last implicit argument.
+                    auto last_imp = std::find(imp_args.rbegin(), imp_args.rend(), true);
+                    lean_assert(last_imp != imp_args.rend()); // it must contain an implicit argument
+                    unsigned num = static_cast<unsigned>(imp_args.rend() - last_imp);
+                    for (unsigned i = 0; i < num; i++) {
                         if (imp_args[i]) {
                             args.push_back(save(mk_placeholder(), pos()));
                         } else {

src/frontends/lean/pp.cpp

@@ -525,7 +525,10 @@ class pp_fn {
             if (has_implicit_arguments(owner, f)) {
                 name const & n = is_constant(f) ? const_name(f) : to_value(f).get_name();
                 m_implicit_args = &(get_implicit_arguments(env, n));
-                if (show_implicit || num_args(e) - 1 < m_implicit_args->size()) {
+                auto last_imp = std::find(m_implicit_args->rbegin(), m_implicit_args->rend(), true);
+                lean_assert(last_imp != m_implicit_args->rend()); // it must contain an implicit argument
+                unsigned num = static_cast<unsigned>(m_implicit_args->rend() - last_imp);
+                if (show_implicit || num_args(e) - 1 < num) {
                     // we are showing implicit arguments, thus we do
                     // not need the bit-mask for implicit arguments
                     m_implicit_args = nullptr;

tests/lean/implicit2.lean

@@ -0,0 +1,12 @@
+Variable f {A : Type} (x y : A) : A
+Check f 10 20
+Check f 10
+Check f::explicit
+Variable g {A : Type} (x1 x2 : A) {B : Type} (y1 y2 : B) : B
+Check g 10 20 true
+Check let r : Real -> Real -> Real := g 10 20
+      in r
+Check g 10
+Set pp::implicit true
+Check let r : Real -> Real -> Real := g 10 20
+      in r

tests/lean/implicit2.lean.expected.out

@@ -0,0 +1,12 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: f
+f 10 20 : ℕ
+f 10 : ℕ → ℕ
+f::explicit : Π (A : Type), A → A → A
+  Assumed: g
+g 10 20 ⊤ : Bool → Bool
+let r : ℝ → ℝ → ℝ := g 10 20 in r : ℝ → ℝ → ℝ
+Error (line: 10, pos: 0) invalid expression, unexpected token
+  Set: lean::pp::implicit
+let r : ℝ → ℝ → ℝ := g::explicit ℕ 10 20 ℝ in r : ℝ → ℝ → ℝ