Add implicit argument management to lean frontend.

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

src/frontends/lean/lean_frontend.cpp

@@ -9,17 +9,21 @@ Author: Leonardo de Moura
 #include "toplevel.h"
 #include "map.h"
 #include "state.h"
+#include "sstream.h"
+#include "exception.h"
 #include "lean_operator_info.h"
 #include "lean_frontend.h"
 #include "lean_notation.h"
 #include "lean_pp.h"
 
 namespace lean {
+static std::vector<unsigned> g_empty_vector;
 /** \brief Implementation of the Lean frontend */
 struct frontend::imp {
+    typedef std::pair<std::vector<unsigned>, name> implicit_info;
     // Remark: only named objects are stored in the dictionary.
     typedef std::unordered_map<name, operator_info, name_hash, name_eq> operator_table;
-    typedef std::unordered_map<name, unsigned, name_hash, name_eq> implicit_table;
+    typedef std::unordered_map<name, implicit_info, name_hash, name_eq> implicit_table;
     typedef std::unordered_map<expr, operator_info, expr_hash, std::equal_to<expr>> expr_to_operator;
     std::atomic<unsigned> m_num_children;
     std::shared_ptr<imp>  m_parent;
@@ -163,6 +167,67 @@ struct frontend::imp {
     void add_mixfixr(unsigned sz, name const * opns, unsigned p, expr const & d) { add_op(mixfixr(sz, opns, p), d, true);  }
     void add_mixfixc(unsigned sz, name const * opns, unsigned p, expr const & d) { add_op(mixfixc(sz, opns, p), d, false); }
 
+    void mark_implicit_arguments(name const & n, unsigned sz, unsigned * implicit) {
+        if (has_children())
+            throw exception(sstream() << "failed to mark implicit arguments, frontend object is read-only");
+        object const & obj = m_env.get_object(n);
+        if (obj.kind() != object_kind::Definition && obj.kind() != object_kind::Postulate)
+            throw exception(sstream() << "failed to mark implicit arguments, the object '" << n << "' is not a definition or postulate");
+        if (has_implicit_arguments(n))
+            throw exception(sstream() << "the object '" << n << "' already has implicit argument information associated with it");
+        name explicit_version(n, "explicit");
+        if (m_env.find_object(explicit_version))
+            throw exception(sstream() << "failed to mark implicit arguments for '" << n << "', the frontend already has an object named '" << explicit_version << "'");
+        expr const & type = obj.get_type();
+        unsigned num_args = 0;
+        expr it = type;
+        while (is_pi(it)) { num_args++; it = abst_body(it); }
+        std::vector<unsigned> v;
+        for (unsigned i = 0; i < sz; i++) {
+            if (implicit[i] >= num_args)
+                throw exception(sstream() << "failed to mark implicit arguments for '" << n << "', object has only " << num_args << " arguments, but trying to mark argument " << implicit[i]+1 << " as implicit");
+            v.push_back(implicit[i]);
+        }
+        m_implicit_table[n] = mk_pair(v, explicit_version);
+        if (obj.is_axiom() || obj.is_theorem()) {
+            m_env.add_theorem(explicit_version, type, mk_constant(n));
+        } else {
+            m_env.add_definition(explicit_version, type, mk_constant(n));
+        }
+    }
+
+    bool has_implicit_arguments(name const & n) {
+        if (m_implicit_table.find(n) != m_implicit_table.end()) {
+            return true;
+        } else if (has_parent()) {
+            return m_parent->has_implicit_arguments(n);
+        } else {
+            return false;
+        }
+    }
+
+    std::vector<unsigned> const & get_implicit_arguments(name const & n) {
+        auto it = m_implicit_table.find(n);
+        if (it != m_implicit_table.end()) {
+            return it->second.first;
+        } else if (has_parent()) {
+            return m_parent->get_implicit_arguments(n);
+        } else {
+            return g_empty_vector;
+        }
+    }
+
+    name const & get_explicit_version(name const & n) {
+        auto it = m_implicit_table.find(n);
+        if (it != m_implicit_table.end()) {
+            return it->second.second;
+        } else if (has_parent()) {
+            return m_parent->get_explicit_version(n);
+        } else {
+            return name::anonymous();
+        }
+    }
+
     void set_interrupt(bool flag) {
         m_env.set_interrupt(flag);
         m_state.set_interrupt(flag);
@@ -235,6 +300,17 @@ operator_info frontend::find_op_for(expr const & n) const { return m_imp->find_o
 operator_info frontend::find_nud(name const & n) const { return m_imp->find_nud(n); }
 operator_info frontend::find_led(name const & n) const { return m_imp->find_led(n); }
 
+void frontend::mark_implicit_arguments(name const & n, unsigned num) {
+    buffer<unsigned> tmp;
+    for (unsigned i = 0; i < num; i++) tmp.push_back(i);
+    mark_implicit_arguments(n, tmp.size(), tmp.data());
+}
+void frontend::mark_implicit_arguments(name const & n, unsigned sz, unsigned * implicit) { m_imp->mark_implicit_arguments(n, sz, implicit); }
+bool frontend::has_implicit_arguments(name const & n) { return m_imp->has_implicit_arguments(n); }
+std::vector<unsigned> const & frontend::get_implicit_arguments(name const & n) { return m_imp->get_implicit_arguments(n); }
+name const & frontend::get_explicit_version(name const & n) { return m_imp->get_explicit_version(n); }
+
+
 state const & frontend::get_state() const { return m_imp->m_state; }
 state & frontend::get_state_core() { return m_imp->m_state; }
 void frontend::set_options(options const & opts) { return m_imp->m_state.set_options(opts); }

src/frontends/lean/lean_frontend.h

@@ -116,6 +116,38 @@ public:
     operator_info find_led(name const & n) const;
     /*@}*/
 
+    /**
+       @name Implicit arguments.
+    */
+    /**
+       \brief Mark the first \c num arguments of the definition (or
+       postulate) named \c n as implicit.
+
+       It throws an exception if \c n already has implicit arguments
+       markups; or if \c n is not a definition or postulate; or if
+       the number of arguments of \c n is less than \c num.
+    */
+    void mark_implicit_arguments(name const & n, unsigned num);
+    /**
+       \brief Mark the given arguments of \c n as implicit.
+       The array specify the position of the implicit arguments.
+    */
+    void mark_implicit_arguments(name const & n, unsigned sz, unsigned * implicit);
+    /** \brief Return true iff \c n has implicit arguments */
+    bool has_implicit_arguments(name const & n);
+    /** \brief Return the position of the arguments that are implicit. */
+    std::vector<unsigned> const & get_implicit_arguments(name const & n);
+    /**
+        \brief This frontend associates an definition with each
+        definition (or postulate) that has implicit arguments. The
+        additional definition has explicit arguments, and it is called
+        n::explicit. The explicit version can be used when the Lean
+        frontend can't figure out the value for the implicit
+        arguments.
+    */
+    name const & get_explicit_version(name const & n);
+    /*@}*/
+
     /**
        @name State management.
     */

src/kernel/object.cpp

@@ -94,6 +94,7 @@ class axiom_object_cell : public postulate_object_cell {
 public:
     axiom_object_cell(name const & n, expr const & t):postulate_object_cell(n, t) {}
     virtual char const * keyword() const { return "Axiom"; }
+    virtual bool is_axiom() const { return true; }
 };
 
 /**
@@ -103,6 +104,7 @@ class variable_decl_object_cell : public postulate_object_cell {
 public:
     variable_decl_object_cell(name const & n, expr const & t):postulate_object_cell(n, t) {}
     virtual char const * keyword() const { return "Variable"; }
+    virtual bool is_var_decl() const { return true; }
 };
 
 /**
@@ -130,6 +132,7 @@ public:
     theorem_object_cell(name const & n, expr const & t, expr const & v):
         definition_object_cell(n, t, v, true) {}
     virtual char const * keyword() const { return "Theorem"; }
+    virtual bool is_theorem() const { return true; }
 };
 
 object mk_uvar_decl(name const & n, level const & l) { return object(new uvar_declaration_object_cell(n, l)); }

src/kernel/object.h

@@ -53,6 +53,10 @@ public:
     virtual bool is_opaque() const = 0;
     /** \brief Return object value. \pre is_definition() */
     virtual expr const & get_value() const = 0;
+
+    virtual bool is_axiom() const { return false; }
+    virtual bool is_theorem() const { return false; }
+    virtual bool is_var_decl() const { return false; }
 };
 
 /**
@@ -123,6 +127,10 @@ public:
     bool is_opaque() const { return m_ptr->is_opaque(); }
     expr const & get_value() const { return m_ptr->get_value(); }
 
+    bool is_axiom() const { return m_ptr->is_axiom(); }
+    bool is_theorem() const { return m_ptr->is_theorem(); }
+    bool is_var_decl() const { return m_ptr->is_var_decl(); }
+
     object_cell const * cell() const { return m_ptr; }
 };
 object mk_uvar_decl(name const & n, level const & l);

src/tests/frontends/lean/lean_frontend.cpp

@@ -164,6 +164,46 @@ static void tst10() {
     std::cout << fmt(e) << "\n";
 }
 
+static void tst11() {
+    frontend f;
+    expr A = Const("A");
+    f.add_var("g", Pi({A, Type()}, A >> (A >> A)));
+    lean_assert(!f.has_implicit_arguments("g"))
+    f.mark_implicit_arguments("g", 1);
+    lean_assert(f.has_implicit_arguments("g"))
+    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<unsigned>{0});
+    try {
+        f.mark_implicit_arguments("g", 1);
+        lean_unreachable();
+    } catch (exception & ex) {
+        std::cout << "Expected error: " << ex.what() << std::endl;
+    }
+    f.add_var("s", Pi({A, Type()}, A >> (A >> A)));
+    try {
+        f.mark_implicit_arguments("s", 4);
+        lean_unreachable();
+    } catch (exception & ex) {
+        std::cout << "Expected error: " << ex.what() << std::endl;
+    }
+    f.add_var(name{"h","explicit"}, Pi({A, Type()}, A >> (A >> A)));
+    f.add_var("h", Pi({A, Type()}, A >> (A >> A)));
+    try {
+        f.mark_implicit_arguments("h", 1);
+        lean_unreachable();
+    } catch (exception & ex) {
+        std::cout << "Expected error: " << ex.what() << std::endl;
+    }
+    try {
+        f.mark_implicit_arguments("u", 1);
+        lean_unreachable();
+    } catch (exception & ex) {
+        std::cout << "Expected error: " << ex.what() << std::endl;
+    }
+}
+
 int main() {
     tst1();
     tst2();
@@ -175,5 +215,6 @@ int main() {
     tst8();
     tst9();
     tst10();
+    tst11();
     return has_violations() ? 1 : 0;
 }