Use expected type of a definition in the elaborator. Improve elaborator solver. Add new example

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

examples/ex1.lean

@@ -19,10 +19,8 @@ Axiom H2 : b = e
 (* Proof that (h a b) = (h c e) *)
 Theorem T1 : (h a b) = (h c e) :=
     DisjCases H1
-              (fun C1 : _,
+              (λ C1, CongrH (Trans (Conjunct1 C1) (Conjunct2 C1)) H2)
-                   CongrH (Trans (Conjunct1 C1) (Conjunct2 C1)) H2)
+              (λ C2, CongrH (Trans (Conjunct1 C2) (Conjunct2 C2)) H2)
-              (fun C2 : _,
-                   CongrH (Trans (Conjunct1 C2) (Conjunct2 C2)) H2)
 
 (* We can use theorem T1 to prove other theorems *)
 Theorem T2 : (h a (h a b)) = (h a (h c e)) :=

examples/ex2.lean

@@ -0,0 +1,6 @@
+Theorem simple (p q r : Bool) : (p ⇒ q) ∧ (q ⇒ r) ⇒ p ⇒ r :=
+    Discharge (λ H1, Discharge (λ H2, MP (Conjunct2 H1) (MP (Conjunct1 H1) H2)))
+
+Set pp::implicit true
+Show Environment 1
+

src/frontends/lean/lean_elaborator.cpp

@@ -570,8 +570,22 @@ class elaborator::imp {
                 } else if (is_simple_ho_match(new_rhs, new_lhs, c.m_ctx)) {
                     delayed = 0;
                     unify_simple_ho_match(new_rhs, new_lhs, c);
+                } else if (has_assigned_metavar(new_lhs)) {
+                    delayed = 0;
+                    m_constraints.push_back(constraint(instantiate(new_lhs), new_rhs, c));
+                } else if (has_assigned_metavar(new_rhs)) {
+                    delayed = 0;
+                    m_constraints.push_back(constraint(new_lhs, instantiate(new_rhs), c));
                 } else {
-                    throw_unification_exception(c);
+                    m_constraints.push_back(c);
+                    if (delayed == 0) {
+                        last_num_constraints = m_constraints.size();
+                        delayed++;
+                    } else if (delayed > last_num_constraints) {
+                        throw_unification_exception(c);
+                    } else {
+                        delayed++;
+                    }
                 }
             }
         }
@@ -700,12 +714,18 @@ public:
         return m_env;
     }
 
-    expr operator()(expr const & e, elaborator const & elb) {
+    expr operator()(expr const & e, expr const & expected_type, elaborator const & elb) {
         m_constraints.clear();
         m_metavars.clear();
         m_owner = &elb;
         m_processing_root = true;
-        m_root = process(e, context()).first;
+        auto p = process(e, context());
+        m_root = p.first;
+        expr given_type = p.second;
+        if (expected_type) {
+            if (has_metavar(given_type))
+                m_constraints.push_back(constraint(expected_type, given_type, context(), e, context(), static_cast<unsigned>(-1)));
+        }
         if (has_metavar(m_root)) {
             solve();
             return instantiate(m_root);
@@ -738,7 +758,8 @@ public:
 };
 elaborator::elaborator(frontend const & fe):m_ptr(new imp(fe, nullptr)) {}
 elaborator::~elaborator() {}
-expr elaborator::operator()(expr const & e) { return (*m_ptr)(e, *this); }
+expr elaborator::operator()(expr const & e) { return (*m_ptr)(e, expr(), *this); }
+expr elaborator::operator()(expr const & e, expr const & expected_type) { return (*m_ptr)(e, expected_type, *this); }
 expr const & elaborator::get_original(expr const & e) const { return m_ptr->get_original(e); }
 void elaborator::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); }
 void elaborator::clear() { m_ptr->clear(); }

src/frontends/lean/lean_elaborator.h

@@ -25,6 +25,7 @@ public:
     ~elaborator();
 
     expr operator()(expr const & e);
+    expr operator()(expr const & e, expr const & expected_type);
 
     /**
         \brief If \c e is an expression instantiated by the elaborator, then it

src/frontends/lean/lean_parser.cpp

@@ -382,7 +382,7 @@ class parser::imp {
        \brief Return the function associated with the given operator.
        If the operator has been overloaded, it returns a choice expression
        of the form <tt>(choice f_1 f_2 ... f_k)</tt> where f_i's are different options.
-       After we finish parsing, the procedure #elaborate will
+       After we finish parsing, the elaborator
        resolve/decide which f_i should be used.
     */
     expr mk_fun(operator_info const & op) {
@@ -1009,10 +1009,6 @@ class parser::imp {
     }
     /*@}*/
 
-    expr elaborate(expr const & e) {
-        return m_elaborator(e);
-    }
-
     /**
        @name Parse Commands
     */
@@ -1043,9 +1039,9 @@ class parser::imp {
         buffer<std::tuple<pos_info, name, expr,bool>> bindings;
         if (curr_is_colon()) {
             next();
-            type = elaborate(parse_expr());
+            type = m_elaborator(parse_expr());
             check_assign_next("invalid definition, ':=' expected");
-            val  = elaborate(parse_expr());
+            val  = m_elaborator(parse_expr(), type);
         } else {
             mk_scope scope(*this);
             parse_object_bindings(bindings);
@@ -1053,8 +1049,8 @@ class parser::imp {
             expr type_body = parse_expr();
             check_assign_next("invalid definition, ':=' expected");
             expr val_body  = parse_expr();
-            type = elaborate(mk_abstraction(false, bindings, type_body));
+            type = m_elaborator(mk_abstraction(false, bindings, type_body));
-            val  = elaborate(mk_abstraction(true, bindings, val_body));
+            val  = m_elaborator(mk_abstraction(true, bindings, val_body), type);
         }
         if (is_definition) {
             m_frontend.add_definition(id, type, val);
@@ -1098,13 +1094,13 @@ class parser::imp {
         expr type;
         if (curr_is_colon()) {
             next();
-            type = elaborate(parse_expr());
+            type = m_elaborator(parse_expr());
         } else {
             mk_scope scope(*this);
             parse_object_bindings(bindings);
             check_colon_next("invalid variable/axiom declaration, ':' expected");
             expr type_body = parse_expr();
-            type = elaborate(mk_abstraction(false, bindings, type_body));
+            type = m_elaborator(mk_abstraction(false, bindings, type_body));
         }
         if (is_var)
             m_frontend.add_var(id, type);
@@ -1138,7 +1134,7 @@ class parser::imp {
     /** \brief Parse 'Eval' expr */
     void parse_eval() {
         next();
-        expr v = elaborate(parse_expr());
+        expr v = m_elaborator(parse_expr());
         normalizer norm(m_frontend);
         scoped_set_interruptable_ptr<normalizer> set(m_normalizer, &norm);
         expr r = norm(v);
@@ -1177,7 +1173,7 @@ class parser::imp {
                 throw parser_error("invalid Show command, expression, 'Options' or 'Environment' expected", m_last_cmd_pos);
             }
         } else {
-            expr v = elaborate(parse_expr());
+            expr v = m_elaborator(parse_expr());
             regular(m_frontend) << v << endl;
         }
     }
@@ -1185,7 +1181,7 @@ class parser::imp {
     /** \brief Parse 'Check' expr */
     void parse_check() {
         next();
-        expr v = elaborate(parse_expr());
+        expr v = m_elaborator(parse_expr());
         expr t = infer_type(v, m_frontend);
         regular(m_frontend) << t << endl;
     }
@@ -1570,7 +1566,7 @@ public:
     /** \brief Parse an expression. */
     expr parse_expr_main() {
         try {
-            return elaborate(parse_expr());
+            return m_elaborator(parse_expr());
         } catch (parser_error & ex) {
             throw parser_exception(ex.what(), ex.m_pos.first, ex.m_pos.second);
         }

src/shell/CMakeLists.txt

@@ -3,6 +3,7 @@ include_directories("${LEAN_BINARY_DIR}")
 add_executable(lean lean.cpp)
 target_link_libraries(lean ${EXTRA_LIBS})
 add_test(example1 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex1.lean")
+add_test(example2 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex2.lean")
 add_test(NAME leantests
          WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean"
          COMMAND "./test.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean")