feat(frontends/lean): modify begin-end semantics, closes #258

src/frontends/lean/begin_end_ext.cpp

@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include "kernel/type_checker.h"
 #include "library/scoped_ext.h"
 #include "library/kernel_serializer.h"
+#include "library/annotation.h"
 #include "library/tactic/expr_to_tactic.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/tactic_hint.h"
@@ -68,13 +69,27 @@ struct be_config {
 template class scoped_ext<be_config>;
 typedef scoped_ext<be_config> begin_end_ext;
 
+static name * g_begin_end = nullptr;
+static name * g_begin_end_element = nullptr;
+
+expr mk_begin_end_annotation(expr const & e) { return mk_annotation(*g_begin_end, e); }
+expr mk_begin_end_element_annotation(expr const & e) { return mk_annotation(*g_begin_end_element, e); }
+bool is_begin_end_annotation(expr const & e) { return is_annotation(e, *g_begin_end); }
+bool is_begin_end_element_annotation(expr const & e) { return is_annotation(e, *g_begin_end_element); }
+
 void initialize_begin_end_ext() {
     g_class_name = new name("begin_end");
     g_key        = new std::string("be_pre_tac");
     begin_end_ext::initialize();
+    g_begin_end  = new name("begin_end");
+    g_begin_end_element = new name("begin_end_element");
+    register_annotation(*g_begin_end);
+    register_annotation(*g_begin_end_element);
 }
 
 void finalize_begin_end_ext() {
+    delete g_begin_end;
+    delete g_begin_end_element;
     begin_end_ext::finalize();
     delete g_key;
     delete g_class_name;

src/frontends/lean/begin_end_ext.h

@@ -14,6 +14,11 @@ environment reset_begin_end_pre_tactic(environment const & env, expr const & pre
 optional<expr> get_begin_end_pre_tactic(environment const & env);
 void register_begin_end_cmds(cmd_table & r);
 
+expr mk_begin_end_annotation(expr const & e);
+expr mk_begin_end_element_annotation(expr const & e);
+bool is_begin_end_annotation(expr const & e);
+bool is_begin_end_element_annotation(expr const & e);
+
 void initialize_begin_end_ext();
 void finalize_begin_end_ext();
 }

src/frontends/lean/builtin_exprs.cpp

@@ -155,7 +155,7 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos) {
             p.check_token_next(get_comma_tk(), "invalid 'begin-end' expression, ',' expected");
             if (p.collecting_info()) {
                 expr info_tac = p.save_pos(mk_info_tactic_expr(), pos);
-                tacs.push_back(info_tac);
+                tacs.push_back(mk_begin_end_element_annotation(info_tac));
             }
         }
         if (p.curr_is_token(get_end_tk()))
@@ -169,7 +169,7 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos) {
             tac = p.mk_app(get_exact_tac_fn(), tac, pos);
         if (pre_tac)
             tac = p.mk_app({get_and_then_tac_fn(), *pre_tac, tac}, pos);
-        tac = p.mk_app(get_determ_tac_fn(), tac, pos);
+        tac = mk_begin_end_element_annotation(tac);
         tacs.push_back(tac);
     }
     auto end_pos = p.pos();
@@ -178,18 +178,14 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos) {
         expr tac = get_id_tac_fn();
         if (pre_tac)
             tac = p.mk_app({get_and_then_tac_fn(), *pre_tac, tac}, end_pos);
+        tac = mk_begin_end_element_annotation(tac);
         tacs.push_back(tac);
     }
     expr r = tacs[0];
-    if (tacs.size() == 1) {
-        // Hack: for having a uniform squiggle placement for unsolved goals.
-        // That is, the result is always of the form and_then(...).
-        r = p.mk_app({get_and_then_tac_fn(), r, get_id_tac_fn()}, end_pos);
-    }
     for (unsigned i = 1; i < tacs.size(); i++) {
         r = p.mk_app({get_and_then_tac_fn(), r, tacs[i]}, end_pos);
     }
-    return p.mk_by(r, end_pos);
+    return p.mk_by(mk_begin_end_annotation(r), end_pos);
 }
 
 static expr parse_begin_end(parser & p, unsigned, expr const *, pos_info const & pos) {

src/frontends/lean/elaborator.cpp

@@ -45,6 +45,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/proof_qed_elaborator.h"
 #include "frontends/lean/info_tactic.h"
 #include "frontends/lean/pp_options.h"
+#include "frontends/lean/begin_end_ext.h"
 
 namespace lean {
 /** \brief 'Choice' expressions <tt>(choice e_1 ... e_n)</tt> are mapped into a metavariable \c ?m
@@ -888,17 +889,21 @@ unify_result_seq elaborator::solve(constraint_seq const & cs) {
     return unify(env(), tmp.size(), tmp.data(), m_ngen.mk_child(), substitution(), m_unifier_config);
 }
 
-void elaborator::display_unsolved_proof_state(expr const & mvar, proof_state const & ps, char const * msg) {
+void elaborator::display_unsolved_proof_state(expr const & mvar, proof_state const & ps, char const * msg, expr const & pos) {
     lean_assert(is_metavar(mvar));
     if (!m_displayed_errors.contains(mlocal_name(mvar))) {
         m_displayed_errors.insert(mlocal_name(mvar));
         auto out = regular(env(), ios());
         flycheck_error err(out);
-        display_error_pos(out, pip(), mvar);
+        display_error_pos(out, pip(), pos);
-        out << " unsolved placeholder, " << msg << "\n" << ps << endl;
+        out << " " << msg << "\n" << ps << endl;
     }
 }
 
+void elaborator::display_unsolved_proof_state(expr const & mvar, proof_state const & ps, char const * msg) {
+    display_unsolved_proof_state(mvar, ps, msg, mvar);
+}
+
 optional<expr> elaborator::get_pre_tactic_for(substitution & subst, expr const & mvar, name_set & visited) {
     if (auto it = m_local_tactic_hints.find(mlocal_name(mvar))) {
         expr pre_tac = subst.instantiate(*it);
@@ -981,6 +986,56 @@ bool elaborator::try_using(substitution & subst, expr const & mvar, proof_state
     }
 }
 
+static void extract_begin_end_tactics(expr pre_tac, buffer<expr> & pre_tac_seq) {
+    if (is_begin_end_element_annotation(pre_tac)) {
+        pre_tac_seq.push_back(get_annotation_arg(pre_tac));
+    } else {
+        buffer<expr> args;
+        if (get_app_args(pre_tac, args) == get_and_then_tac_fn()) {
+            for (expr const & arg : args) {
+                extract_begin_end_tactics(arg, pre_tac_seq);
+            }
+        } else {
+            throw exception("internal error, invalid begin-end tactic");
+        }
+    }
+}
+
+void elaborator::try_using_begin_end(substitution & subst, expr const & mvar, proof_state ps, expr const & pre_tac) {
+    lean_assert(is_begin_end_annotation(pre_tac));
+    buffer<expr> pre_tac_seq;
+    extract_begin_end_tactics(get_annotation_arg(pre_tac), pre_tac_seq);
+    for (expr const & ptac : pre_tac_seq) {
+        if (auto tac = pre_tactic_to_tactic(ptac)) {
+            try {
+                proof_state_seq seq = (*tac)(env(), ios(), ps);
+                auto r = seq.pull();
+                if (!r) {
+                    // tactic failed to produce any result
+                    display_unsolved_proof_state(mvar, ps, "tactic failed", ptac);
+                    return;
+                }
+                ps = r->first;
+            } catch (tactic_exception & ex) {
+                auto out = regular(env(), ios());
+                display_error_pos(out, pip(), ex.get_expr());
+                out << " tactic failed: " << ex.what() << "\n";
+                return;
+            }
+        } else {
+            return;
+        }
+    }
+
+    if (!empty(ps.get_goals())) {
+        display_unsolved_proof_state(mvar, ps, "unsolved subgoals", pre_tac);
+    } else {
+        subst = ps.get_subst();
+        expr v = subst.instantiate(mvar);
+        subst.assign(mlocal_name(mvar), v);
+    }
+}
+
 void elaborator::solve_unassigned_mvar(substitution & subst, expr mvar, name_set & visited) {
     if (visited.contains(mlocal_name(mvar)))
         return;
@@ -994,11 +1049,20 @@ void elaborator::solve_unassigned_mvar(substitution & subst, expr mvar, name_set
     // first solve unassigned metavariables in type
     type = solve_unassigned_mvars(subst, type, visited);
     proof_state ps = to_proof_state(*meta, type, subst, m_ngen.mk_child());
-    if (auto local_hint = get_local_tactic_hint(subst, mvar, visited)) {
+    if (auto pre_tac = get_pre_tactic_for(subst, mvar, visited)) {
-        // using user provided tactic
+        if (is_begin_end_annotation(*pre_tac)) {
-        bool show_failure = true;
+            try_using_begin_end(subst, mvar, ps, *pre_tac);
-        try_using(subst, mvar, ps, *local_hint, show_failure);
+            return;
-    } else if (m_use_tactic_hints) {
+        }
+
+        if (auto tac = pre_tactic_to_tactic(*pre_tac)) {
+            bool show_failure = true;
+            try_using(subst, mvar, ps, *tac, show_failure);
+            return;
+        }
+    }
+
+    if (m_use_tactic_hints) {
         // using tactic_hints
         for (expr const & pre_tac : get_tactic_hints(env())) {
             if (auto tac = pre_tactic_to_tactic(pre_tac)) {
@@ -1036,7 +1100,7 @@ void elaborator::display_unassigned_mvars(expr const & e, substitution const & s
                     expr meta_type = tmp_s.instantiate(type_checker(env()).infer(meta).first);
                     goal g(meta, meta_type);
                     proof_state ps(goals(g), s, m_ngen, constraints());
-                    display_unsolved_proof_state(e, ps, "don't know how to synthesize it");
+                    display_unsolved_proof_state(e, ps, "don't know how to synthesize placeholder");
                 }
                 return false;
             });

src/frontends/lean/elaborator.h

@@ -122,12 +122,14 @@ class elaborator : public coercion_info_manager {
     pair<expr, constraint_seq> visit(expr const & e);
     expr visit(expr const & e, constraint_seq & cs);
     unify_result_seq solve(constraint_seq const & cs);
+    void display_unsolved_proof_state(expr const & mvar, proof_state const & ps, char const * msg, expr const & pos);
     void display_unsolved_proof_state(expr const & mvar, proof_state const & ps, char const * msg);
     optional<expr> get_pre_tactic_for(substitution & subst, expr const & mvar, name_set & visited);
     optional<tactic> pre_tactic_to_tactic(expr const & pre_tac);
     optional<tactic> get_local_tactic_hint(substitution & subst, expr const & mvar, name_set & visited);
     bool try_using(substitution & subst, expr const & mvar, proof_state const & ps, tactic const & tac,
                    bool show_failure);
+    void try_using_begin_end(substitution & subst, expr const & mvar, proof_state ps, expr const & pre_tac);
     void solve_unassigned_mvar(substitution & subst, expr mvar, name_set & visited);
     expr solve_unassigned_mvars(substitution & subst, expr e, name_set & visited);
     expr solve_unassigned_mvars(substitution & subst, expr const & e);

tests/lean/goals1.lean.expected.out

@@ -1,4 +1,4 @@
-goals1.lean:9:0: error: unsolved placeholder, unsolved subgoals
+goals1.lean:9:0: error: unsolved subgoals
 A : Type,
 a : A,
 b : A,

tests/lean/pstate.lean.expected.out

@@ -1,4 +1,4 @@
-pstate.lean:4:26: error: unsolved placeholder, don't know how to synthesize it
+pstate.lean:4:26: error: don't know how to synthesize placeholder
 A : Type,
 a : A,
 b : A,