feat(frontends/lean): simplify how implicit parameters are marked

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

src/frontends/lean/frontend.cpp

@@ -143,13 +143,34 @@ struct lean_extension : public environment::extension {
 
     /**
         \brief Two operator (aka notation) denotations are compatible
-        iff one of the following holds:
+        iff after ignoring all implicit arguments in the prefix and
-
+        explicit arguments in the suffix, the remaining implicit arguments
-        1) Both do not have implicit arguments
-
-        2) Both have implicit arguments, and the implicit arguments
         occur in the same positions.
 
+        Let us denote implicit arguments with a '_' and explicit with a '*'.
+        Then a denotation can be associated with a pattern containing one or more
+        '_' and '*'.
+        Two denotations are compatible, if we have the same pattern after
+        removed the '_' from the prefix and '*' from the suffix.
+
+        Here is an example of compatible denotations
+                 f : Int -> Int -> Int              Pattern   * *
+                 g : Pi {A : Type}, A -> A -> A     Pattern   _ * *
+                 h : Pi {A B : Type}, A -> B -> A   Pattern   _ _ * *
+            They are compatible, because after we remove the _ from the prefix, and * from the suffix,
+            all of them reduce to the empty sequence
+
+        Here is another example of compatible denotations:
+                 f : Pi {A : Type} (a : A) {B : Type} (b : B), A    Pattern _ * _ *
+                 g : Pi (i : Int) {T : Type} (x : T), T             Pattern * _ *
+            They are compatible, because after we remove the _ from the prefix, and * from the suffix,
+            we get the same sequence:  * _
+
+        The following two are not compatible
+                 f : Pi {A : Type} (a : A) {B : Type} (b : B), A    Pattern _ * _ *
+                 g : Pi {A B : Type} (a : A) (b : B), A             Pattern _ _ * *
+
+       TODO(Leo): not implemented yet
     */
     bool compatible_denotation(expr const & d1, expr const & d2) {
         return get_implicit_arguments(d1) == get_implicit_arguments(d2);
@@ -243,9 +264,13 @@ struct lean_extension : public environment::extension {
         while (is_pi(it)) { num_args++; it = abst_body(it); }
         if (sz > num_args)
             throw exception(sstream() << "failed to mark implicit arguments for '" << n << "', object has only " << num_args << " arguments, but trying to mark " << sz << " arguments");
+        // remove explicit suffix
+        while (sz > 0 && !implicit[sz - 1]) sz--;
+        if (sz == 0)
+            throw exception(sstream() << "failed to mark implicit arguments for '" << n << "', all arguments are explicit");
         std::vector<bool> v(implicit, implicit+sz);
         m_implicit_table[n] = mk_pair(v, explicit_version);
-        expr body = mk_explicit_definition_body(type, n, 0, sz);
+        expr body = mk_explicit_definition_body(type, n, 0, num_args);
         if (obj.is_axiom() || obj.is_theorem()) {
             env.add_theorem(explicit_version, type, body);
         } else {
@@ -445,6 +470,18 @@ operator_info frontend::find_led(name const & n) const {
 void frontend::mark_implicit_arguments(name const & n, unsigned sz, bool const * implicit) {
     to_ext(m_env).mark_implicit_arguments(n, sz, implicit, m_env);
 }
+void frontend::mark_implicit_arguments(name const & n, unsigned prefix_sz) {
+    buffer<bool> implicit; implicit.resize(prefix_sz, true);
+    mark_implicit_arguments(n, implicit.size(), implicit.data());
+}
+void frontend::mark_implicit_arguments(expr const & n, unsigned prefix_sz) {
+    if (is_constant(n)) {
+        mark_implicit_arguments(const_name(n), prefix_sz);
+    } else {
+        lean_assert(is_value(n));
+        mark_implicit_arguments(to_value(n).get_name(), prefix_sz);
+    }
+}
 void frontend::mark_implicit_arguments(name const & n, std::initializer_list<bool> const & l) {
     mark_implicit_arguments(n, l.size(), l.begin());
 }

src/frontends/lean/frontend.h

@@ -120,6 +120,11 @@ public:
     void mark_implicit_arguments(name const & n, unsigned sz, bool const * mask);
     void mark_implicit_arguments(name const & n, std::initializer_list<bool> const & l);
     void mark_implicit_arguments(expr const & n, std::initializer_list<bool> const & l);
+    /**
+       \brief Syntax sugar for mark_implicit_arguments(n, {true, ..., true}), with prefix_sz true's.
+    */
+    void mark_implicit_arguments(name const & n, unsigned prefix_sz);
+    void mark_implicit_arguments(expr const & n, unsigned prefix_sz);
     /** \brief Return true iff \c n has implicit arguments */
     bool has_implicit_arguments(name const & n) const;
     /** \brief Return the position of the arguments that are implicit. */

src/frontends/lean/notation.cpp

@@ -23,8 +23,8 @@ void init_builtin_notation(frontend & f) {
     if (!f.get_environment().mark_builtin_imported("lean_notation"))
         return;
     f.add_infix("=",  50, mk_homo_eq_fn());
-    f.mark_implicit_arguments(mk_homo_eq_fn(), {true, false, false});
+    f.mark_implicit_arguments(mk_homo_eq_fn(), 1);
-    f.mark_implicit_arguments(mk_if_fn(), {true, false, false, false});
+    f.mark_implicit_arguments(mk_if_fn(), 1);
 
     f.add_prefix("\u00ac", 40, mk_not_fn());     // "¬"
     f.add_infixr("&&", 35, mk_and_fn());         // "&&"
@@ -83,41 +83,41 @@ void init_builtin_notation(frontend & f) {
     f.add_coercion(mk_nat_to_real_fn());
 
     // implicit arguments for builtin axioms
-    f.mark_implicit_arguments(mk_cast_fn(), {true, true, false, false});
+    f.mark_implicit_arguments(mk_cast_fn(), 2);
-    f.mark_implicit_arguments(mk_mp_fn(), {true, true, false, false});
+    f.mark_implicit_arguments(mk_mp_fn(), 2);
-    f.mark_implicit_arguments(mk_discharge_fn(), {true, true, false});
+    f.mark_implicit_arguments(mk_discharge_fn(), 2);
-    f.mark_implicit_arguments(mk_refl_fn(), {true, false});
+    f.mark_implicit_arguments(mk_refl_fn(), 1);
-    f.mark_implicit_arguments(mk_subst_fn(), {true, true, true, true, false, false});
+    f.mark_implicit_arguments(mk_subst_fn(), 4);
     add_alias(f, "Subst", "SubstP");
-    f.mark_implicit_arguments("SubstP", {true, true, true, false, false, false});
+    f.mark_implicit_arguments("SubstP", 3);
-    f.mark_implicit_arguments(mk_trans_ext_fn(), {true, true, true, true, true, true, false, false});
+    f.mark_implicit_arguments(mk_trans_ext_fn(), 6);
-    f.mark_implicit_arguments(mk_eta_fn(), {true, true, false});
+    f.mark_implicit_arguments(mk_eta_fn(), 2);
-    f.mark_implicit_arguments(mk_abst_fn(), {true, true, true, true, false});
+    f.mark_implicit_arguments(mk_abst_fn(), 4);
-    f.mark_implicit_arguments(mk_imp_antisym_fn(), {true, true, false, false});
+    f.mark_implicit_arguments(mk_imp_antisym_fn(), 2);
-    f.mark_implicit_arguments(mk_dom_inj_fn(), {true, true, true, true, false});
+    f.mark_implicit_arguments(mk_dom_inj_fn(), 4);
-    f.mark_implicit_arguments(mk_ran_inj_fn(), {true, true, true, true, false, false});
+    f.mark_implicit_arguments(mk_ran_inj_fn(), 4);
 
     // implicit arguments for basic theorems
-    f.mark_implicit_arguments(mk_absurd_fn(), {true, false, false});
+    f.mark_implicit_arguments(mk_absurd_fn(), 1);
-    f.mark_implicit_arguments(mk_double_neg_elim_fn(), {true, true, false});
+    f.mark_implicit_arguments(mk_double_neg_elim_fn(), 2);
-    f.mark_implicit_arguments(mk_mt_fn(), {true, true, false, false});
+    f.mark_implicit_arguments(mk_mt_fn(), 2);
-    f.mark_implicit_arguments(mk_contrapos_fn(), {true, true, false});
+    f.mark_implicit_arguments(mk_contrapos_fn(), 2);
-    f.mark_implicit_arguments(mk_eq_mp_fn(), {true, true, false, false});
+    f.mark_implicit_arguments(mk_eq_mp_fn(), 2);
-    f.mark_implicit_arguments(mk_not_imp1_fn(), {true, true, false});
+    f.mark_implicit_arguments(mk_not_imp1_fn(), 2);
-    f.mark_implicit_arguments(mk_not_imp2_fn(), {true, true, false});
+    f.mark_implicit_arguments(mk_not_imp2_fn(), 2);
-    f.mark_implicit_arguments(mk_conj_fn(), {true, true, false, false});
+    f.mark_implicit_arguments(mk_conj_fn(), 2);
-    f.mark_implicit_arguments(mk_conjunct1_fn(), {true, true, false});
+    f.mark_implicit_arguments(mk_conjunct1_fn(), 2);
-    f.mark_implicit_arguments(mk_conjunct2_fn(), {true, true, false});
+    f.mark_implicit_arguments(mk_conjunct2_fn(), 2);
-    f.mark_implicit_arguments(mk_disj1_fn(), {true, false, false});
+    f.mark_implicit_arguments(mk_disj1_fn(), 1);
-    f.mark_implicit_arguments(mk_disj2_fn(), {true, false, false});
+    f.mark_implicit_arguments(mk_disj2_fn(), 1);
-    f.mark_implicit_arguments(mk_disj_cases_fn(), {true, true, true, false, false, false});
+    f.mark_implicit_arguments(mk_disj_cases_fn(), 3);
-    f.mark_implicit_arguments(mk_symm_fn(), {true, true, true, false});
+    f.mark_implicit_arguments(mk_symm_fn(), 3);
-    f.mark_implicit_arguments(mk_trans_fn(), {true, true, true, true, false, false});
+    f.mark_implicit_arguments(mk_trans_fn(), 4);
-    f.mark_implicit_arguments(mk_eqt_elim_fn(), {true, false});
+    f.mark_implicit_arguments(mk_eqt_elim_fn(), 1);
-    f.mark_implicit_arguments(mk_eqt_intro_fn(), {true, false});
+    f.mark_implicit_arguments(mk_eqt_intro_fn(), 1);
-    f.mark_implicit_arguments(mk_congr1_fn(), {true, true, true, true, false, false});
+    f.mark_implicit_arguments(mk_congr1_fn(), 4);
-    f.mark_implicit_arguments(mk_congr2_fn(), {true, true, true, true, false, false});
+    f.mark_implicit_arguments(mk_congr2_fn(), 4);
-    f.mark_implicit_arguments(mk_congr_fn(),  {true, true, true, true, true, true, false, false});
+    f.mark_implicit_arguments(mk_congr_fn(),  6);
-    f.mark_implicit_arguments(mk_forall_elim_fn(), {true, true, false, false});
+    f.mark_implicit_arguments(mk_forall_elim_fn(), 2);
 }
 }

src/frontends/lean/parser.cpp

@@ -627,6 +627,8 @@ class parser::imp {
                     i++;
                 }
             }
+            for (; i < num_args; i++)
+                new_args.push_back(args[i]);
         } else {
             new_args.append(num_args, args);
         }
@@ -765,11 +767,7 @@ 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 the arguments until we find the last implicit argument.
+                    for (unsigned i = 0; i < imp_args.size(); i++) {
-                    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,10 +525,7 @@ 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));
-                auto last_imp = std::find(m_implicit_args->rbegin(), m_implicit_args->rend(), true);
+                if (show_implicit || num_args(e) - 1 < m_implicit_args->size()) {
-                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;
@@ -796,7 +793,7 @@ class pp_fn {
     }
 
     bool is_implicit(std::vector<bool> const * implicit_args, unsigned arg_pos) {
-        return implicit_args && (*implicit_args)[arg_pos];
+        return implicit_args && arg_pos < implicit_args->size() && (*implicit_args)[arg_pos];
     }
 
     /**

src/tests/frontends/lean/frontend.cpp

@@ -174,7 +174,7 @@ static void tst11() {
     name gexp = f.get_explicit_version("g");
     lean_assert(f.find_object(gexp));
     lean_assert(f.find_object("g")->get_type() == f.find_object(gexp)->get_type());
-    lean_assert(f.get_implicit_arguments("g") == std::vector<bool>({true, false, false}));
+    lean_assert(f.get_implicit_arguments("g") == std::vector<bool>({true})); // the trailing "false" marks are removed
     try {
         f.mark_implicit_arguments("g", {true, false, false});
         lean_unreachable();

tests/lean/implicit3.lean

@@ -0,0 +1,9 @@
+Show 10 = 20
+Variable f : Int -> Int -> Int
+Variable g : Int -> Int -> Int -> Int
+Notation 10 _ ++ _ : f
+Notation 10 _ ++ _ : g
+Set pp::implicit true
+Set pp::notation false
+Show (10 ++ 20)
+Show (10 ++ 20) 10

tests/lean/implicit3.lean.expected.out

@@ -0,0 +1,9 @@
+  Set: pp::colors
+  Set: pp::unicode
+10 = 20
+  Assumed: f
+  Assumed: g
+  Set: lean::pp::implicit
+  Set: lean::pp::notation
+f 10 20
+g 10 20 10