feat(frontends/lean): implement relaxed operator compatibility in the parser

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

src/frontends/lean/frontend.cpp

@@ -504,6 +504,12 @@ bool frontend::has_implicit_arguments(name const & n) const {
 std::vector<bool> const & frontend::get_implicit_arguments(name const & n) const {
     return to_ext(m_env).get_implicit_arguments(n);
 }
+std::vector<bool> const & frontend::get_implicit_arguments(expr const & n) const {
+    if (is_constant(n))
+        return get_implicit_arguments(const_name(n));
+    else
+        return g_empty_vector;
+}
 name const & frontend::get_explicit_version(name const & n) const {
     return to_ext(m_env).get_explicit_version(n);
 }

src/frontends/lean/frontend.h

@@ -129,6 +129,11 @@ public:
     bool has_implicit_arguments(name const & n) const;
     /** \brief Return the position of the arguments that are implicit. */
     std::vector<bool> const & get_implicit_arguments(name const & n) const;
+    /**
+        \brief Return the position of the arguments that are implicit.
+        \remark If \c n is not a constant, then return the empty vector.
+    */
+    std::vector<bool> const & get_implicit_arguments(expr const & n) const;
     /**
         \brief This frontend associates an definition with each
         definition (or postulate) that has implicit arguments. The

src/frontends/lean/frontend_elaborator.cpp

@@ -15,6 +15,7 @@ Author: Leonardo de Moura
 #include "kernel/replace_visitor.h"
 #include "kernel/unification_constraint.h"
 #include "kernel/instantiate.h"
+#include "kernel/builtin.h"
 #include "library/type_inferer.h"
 #include "library/placeholder.h"
 #include "library/elaborator/elaborator.h"
@@ -23,29 +24,52 @@ Author: Leonardo de Moura
 
 namespace lean {
 static name g_x_name("x");
-static name g_choice_name = name::mk_internal_unique_name();
-static expr g_choice = mk_constant(g_choice_name);
 static format g_assignment_fmt  = format(":=");
 static format g_unification_u_fmt = format("\u2248");
 static format g_unification_fmt = format("=?=");
 
+/**
+   \brief Internal value used to store choices for the elaborator.
+   This is a transient value that is only used to setup a problem
+   for the elaborator.
+*/
+struct choice_value : public value {
+    std::vector<expr> m_choices;
+    choice_value(unsigned num_fs, expr const * fs):m_choices(fs, fs + num_fs) {}
+    virtual ~choice_value() {}
+    virtual expr get_type() const { lean_unreachable(); } // LCOV_EXCL_LINE
+    virtual name get_name() const { return name("Choice"); }
+    virtual void display(std::ostream & out) const {
+        out << "(Choice";
+        for (auto c : m_choices) {
+            out << " (" << c << ")";
+        }
+        out << ")";
+    }
+    // Remark: we don't implement the pp methods because the lean::pp_fn formatter
+    // object has support for formatting choice internal values.
+};
+
 expr mk_choice(unsigned num_fs, expr const * fs) {
     lean_assert(num_fs >= 2);
-    return mk_eq(g_choice, mk_app(num_fs, fs));
+    return mk_value(*(new choice_value(num_fs, fs)));
 }
 
 bool is_choice(expr const & e) {
-    return is_eq(e) && eq_lhs(e) == g_choice;
+    return is_value(e) && dynamic_cast<choice_value const *>(&to_value(e)) != nullptr;
+}
+
+choice_value const & to_choice_value(expr const & e) {
+    lean_assert(is_choice(e));
+    return static_cast<choice_value const &>(to_value(e));
 }
 
 unsigned get_num_choices(expr const & e) {
-    lean_assert(is_choice(e));
-    return num_args(eq_rhs(e));
+    return to_choice_value(e).m_choices.size();
 }
 
 expr const & get_choice(expr const & e, unsigned i) {
-    lean_assert(is_choice(e));
-    return arg(eq_rhs(e), i);
+    return to_choice_value(e).m_choices[i];
 }
 
 class coercion_justification_cell : public justification_cell {
@@ -251,6 +275,7 @@ class frontend_elaborator::imp {
             } else {
                 buffer<expr> to_keep;
                 buffer<optional<expr>> to_keep_types;
+                std::sort(matched.begin(), matched.end()); // we must preserve the original order
                 for (unsigned i : matched) {
                     to_keep.push_back(f_choices[i]);
                     to_keep_types.push_back(f_choice_types[i]);

src/frontends/lean/parser.cpp

@@ -17,6 +17,7 @@ Author: Leonardo de Moura
 #include <string>
 #include <tuple>
 #include <vector>
+#include <limits>
 #include "util/scoped_map.h"
 #include "util/exception.h"
 #include "util/sstream.h"
@@ -579,6 +580,41 @@ class parser::imp {
     */
     /*@{*/
 
+    /**
+       \brief Return the size of the implicit vector associated with the given denotation.
+    */
+    unsigned get_implicit_vector_size(expr const & d) {
+        return m_frontend.get_implicit_arguments(d).size();
+    }
+
+    /**
+       \brief Return a vector \c v that is the implicit vector for some \c d in \c ds,
+       and <tt>v.size() == min{get_implicit_vector_size(d) | d in ds}</tt>
+    */
+    std::vector<bool> const & get_smallest_implicit_vector(list<expr> const & ds) {
+        std::vector<bool> const * r = nullptr;
+        unsigned m = std::numeric_limits<unsigned>::max();
+        for (expr const & d : ds) {
+            std::vector<bool> const & v = m_frontend.get_implicit_arguments(d);
+            unsigned s = v.size();
+            if (s == 0) {
+                return v;
+            } else if (s < m) {
+                r = &v;
+                m = s;
+            }
+        }
+        lean_assert(r);
+        return *r;
+    }
+
+    /**
+       \brief Return <tt>min{get_implicit_vector_size(d) | d in ds}</tt>
+    */
+    unsigned get_smallest_implicit_vector_size(list<expr> const & ds) {
+        return get_smallest_implicit_vector(ds).size();
+    }
+
     /**
        \brief Return the function associated with the given operator.
        If the operator has been overloaded, it returns a choice expression
@@ -586,7 +622,7 @@ class parser::imp {
        After we finish parsing, the elaborator
        resolve/decide which f_i should be used.
     */
-    expr mk_fun(operator_info const & op) {
+    expr mk_fun(operator_info const & op, pos_info const & pos) {
         list<expr> const & fs = op.get_denotations();
         lean_assert(!is_nil(fs));
         auto it = fs.begin();
@@ -595,10 +631,24 @@ class parser::imp {
         if (it == fs.end()) {
             return r;
         } else {
+            unsigned min_sz = get_smallest_implicit_vector_size(fs);
             buffer<expr> alternatives;
-            alternatives.push_back(r);
+            auto add_alternative = [&](expr const & d) {
+                unsigned sz = get_implicit_vector_size(d);
+                if (sz > min_sz) {
+                    // must fill the difference with placeholders
+                    buffer<expr> aux;
+                    aux.push_back(d);
+                    for (unsigned i = min_sz; i < sz; i++)
+                        aux.push_back(save(mk_placeholder(), pos));
+                    alternatives.push_back(mk_app(aux));
+                } else {
+                    alternatives.push_back(d);
+                }
+            };
+            add_alternative(r);
             for (; it != fs.end(); ++it)
-                alternatives.push_back(*it);
+                add_alternative(*it);
             return mk_choice(alternatives.size(), alternatives.data());
         }
     }
@@ -609,13 +659,10 @@ class parser::imp {
     */
     expr mk_application(operator_info const & op, pos_info const & pos, unsigned num_args, expr const * args) {
         buffer<expr> new_args;
-        expr f = save(mk_fun(op), pos);
+        expr f = save(mk_fun(op, pos), pos);
         new_args.push_back(f);
-        // I'm using the fact that all denotations are compatible.
         // See lean_frontend.cpp for the definition of compatible denotations.
-        expr const & d = head(op.get_denotations());
-        if (is_constant(d) && m_frontend.has_implicit_arguments(const_name(d))) {
-            std::vector<bool> const & imp_args = m_frontend.get_implicit_arguments(const_name(d));
+        auto imp_args = get_smallest_implicit_vector(op.get_denotations());
         unsigned i = 0;
         for (unsigned j = 0; j < imp_args.size(); j++) {
             if (imp_args[j]) {
@@ -629,9 +676,6 @@ class parser::imp {
         }
         for (; i < num_args; i++)
             new_args.push_back(args[i]);
-        } else {
-            new_args.append(num_args, args);
-        }
         return save(mk_app(new_args), pos);
     }
     expr mk_application(operator_info const & op, pos_info const & pos, std::initializer_list<expr> const & l) {

src/frontends/lean/pp.cpp

@@ -200,8 +200,10 @@ class pp_fn {
     */
     bool is_atomic(expr const & e) {
         switch (e.kind()) {
-        case expr_kind::Var: case expr_kind::Constant: case expr_kind::Value:
+        case expr_kind::Var: case expr_kind::Constant:
             return true;
+        case expr_kind::Value:
+            return !is_choice(e);
         case expr_kind::Type:
             return e == Type();
         case expr_kind::MetaVar:
@@ -700,6 +702,8 @@ class pp_fn {
             result p;
             if (is_constant(f))
                 p = mk_result(format(const_name(f)), 1);
+            else if (is_choice(f))
+                p = pp_child(f, depth);
             else if (is_value(f))
                 p = mk_result(to_value(f).pp(m_unicode, m_coercion), 1);
             else

tests/lean/implicit6.lean

@@ -0,0 +1,10 @@
+Variable f {A : Type} : A -> A -> A
+Infixl 65 + : f
+Show true + false
+Show 10 + 20
+Show 10 + (- 20)
+Set pp::notation false
+Set pp::coercion true
+Show true + false
+Show 10 + 20
+Show 10 + (- 20)

tests/lean/implicit6.lean.expected.out

@@ -0,0 +1,11 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: f
+⊤ + ⊥
+10 + 20
+10 + - 20
+  Set: lean::pp::notation
+  Set: lean::pp::coercion
+f ⊤ ⊥
+Nat::add 10 20
+Int::add (nat_to_int 10) (Nat::neg 20)

tests/lean/implicit7.lean

@@ -0,0 +1,18 @@
+(*
+   TODO(Leo):
+   Improve elaborator's performance on this example.
+   The main problem is that we don't have any indexing technique
+   for the elaborator.
+*)
+Variable f {A : Type} (a : A) {B : Type} : A -> B -> A
+Variable g {A B : Type} (a : A) {C : Type} : B -> C -> C
+Notation 100 _ ; _ ; _ : f
+Notation 100 _ ; _ ; _ : g
+Check 10 ; true ; false
+Check 10 ; 10 ; true
+Set pp::notation false
+Check 10 ; true ; false
+Check 10 ; 10 ; true
+Set pp::implicit true
+Check 10 ; true ; false
+Check 10 ; 10 ; true

tests/lean/implicit7.lean.expected.out

@@ -0,0 +1,12 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: f
+  Assumed: g
+10 ; ⊤ ; ⊥ : Bool
+10 ; 10 ; ⊤ : ℕ
+  Set: lean::pp::notation
+g 10 ⊤ ⊥ : Bool
+f 10 10 ⊤ : ℕ
+  Set: lean::pp::implicit
+g::explicit ℕ Bool 10 Bool ⊤ ⊥ : Bool
+f::explicit ℕ 10 Bool 10 ⊤ : ℕ