feat(frontends/lean): add very basic 'begin ... end' block support

library/init/meta/default.lean

@@ -12,3 +12,4 @@ import init.meta.congr_lemma init.meta.match_tactic init.meta.ac_tactics
 import init.meta.backward init.meta.rewrite_tactic init.meta.unfold_tactic
 import init.meta.mk_dec_eq_instance init.meta.mk_inhabited_instance
 import init.meta.simp_tactic init.meta.defeq_simp_tactic init.meta.set_get_option_tactics
+import init.meta.interactive

library/init/meta/interactive.lean

@@ -0,0 +1,19 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import init.meta.tactic
+
+namespace tactic
+namespace interactive
+
+meta definition apply (q : pexpr) : tactic unit :=
+to_expr q >>= tactic.apply
+
+meta definition refine : pexpr → tactic unit :=
+tactic.refine
+
+end interactive
+end tactic

library/init/meta/tactic.lean

@@ -94,6 +94,9 @@ meta definition try (t : tactic A) : tactic unit :=
 meta definition skip : tactic unit :=
 success ()
 
+meta definition consume (t : tactic A) : tactic unit :=
+t >> skip
+
 open list
 meta definition foreach : list A → (A → tactic unit) → tactic unit
 | []      fn := skip

src/frontends/lean/CMakeLists.txt

@@ -7,4 +7,4 @@ pp.cpp structure_cmd.cpp structure_instance.cpp
 init_module.cpp type_util.cpp local_ref_info.cpp decl_attributes.cpp nested_declaration.cpp
 opt_cmd.cpp prenum.cpp print_cmd.cpp elaborator.cpp
 match_expr.cpp local_context_adapter.cpp decl_util.cpp definition_cmds.cpp
-brackets.cpp)
+brackets.cpp begin_end_block.cpp)

src/frontends/lean/begin_end_block.cpp

@@ -0,0 +1,103 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "library/annotation.h"
+#include "library/constants.h"
+#include "library/tactic/elaborate.h"
+#include "frontends/lean/parser.h"
+#include "frontends/lean/tokens.h"
+#include "frontends/lean/util.h"
+
+namespace lean {
+static name * g_begin_end = nullptr;
+static name * g_begin_end_element = nullptr;
+
+static expr mk_begin_end_block(expr const & e) { return mk_annotation(*g_begin_end, e, nulltag); }
+bool is_begin_end_block(expr const & e) { return is_annotation(e, *g_begin_end); }
+
+static expr mk_begin_end_element(expr const & e) { return mk_annotation(*g_begin_end_element, e, nulltag); }
+static bool is_begin_end_element(expr const & e) { return is_annotation(e, *g_begin_end_element); }
+
+static expr mk_begin_end_element(parser & p, expr tac, pos_info const & pos) {
+    if (tac.get_tag() == nulltag)
+        tac = p.save_pos(tac, pos);
+    tac = p.save_pos(mk_app(mk_constant(get_tactic_consume_name()), tac), pos);
+    return p.save_pos(mk_begin_end_element(tac), pos);
+}
+
+static expr concat(parser & p, expr const & r, expr tac, pos_info const & start_pos, pos_info const & pos) {
+    tac = mk_begin_end_element(p, tac, pos);
+    return p.save_pos(mk_app(mk_constant(get_monad_and_then_name()), r, tac), start_pos);
+}
+
+void get_begin_end_block_elements(expr const & e, buffer<expr> & elems) {
+    lean_assert(is_begin_end_block(e));
+    if (is_app(e)) {
+        get_begin_end_block_elements(app_fn(e), elems);
+        get_begin_end_block_elements(app_arg(e), elems);
+    } else if (is_begin_end_element(e)) {
+        elems.push_back(get_annotation_arg(e));
+    } else {
+        /* do nothing */
+    }
+}
+
+expr parse_begin_end_core(parser & p, pos_info const & start_pos,
+                          name const & end_token, bool nested = false) {
+    p.next();
+    bool first = true;
+    expr r = mk_begin_end_element(p, mk_constant(get_tactic_skip_name()), start_pos);
+    try {
+        while (!p.curr_is_token(end_token)) {
+            auto pos = p.pos();
+            if (first) {
+                first = false;
+            } else {
+                p.check_token_next(get_comma_tk(), "invalid 'begin-end' expression, ',' expected");
+            }
+            /* parse next element */
+            if (p.curr_is_token(get_begin_tk())) {
+                r = concat(p, r, parse_begin_end_core(p, pos, get_end_tk(), true), start_pos, pos);
+            } else if (p.curr_is_token(get_lcurly_tk())) {
+                r = concat(p, r, parse_begin_end_core(p, pos, get_rcurly_tk(), true), start_pos, pos);
+            } else if (p.curr_is_token(end_token)) {
+                break;
+            } else {
+                expr tac = p.parse_expr();
+                r = concat(p, r, tac, start_pos, pos);
+            }
+        }
+    } catch (exception & ex) {
+        if (end_token == get_end_tk())
+            consume_until_end(p);
+        throw;
+    }
+    auto end_pos = p.pos();
+    p.next();
+    r = p.save_pos(mk_begin_end_block(r), end_pos);
+    if (nested)
+        return r;
+    else
+        return p.save_pos(mk_by(r), end_pos);
+}
+
+expr parse_begin_end(parser & p, unsigned, expr const *, pos_info const & pos) {
+    return parse_begin_end_core(p, pos, get_end_tk());
+}
+
+void initialize_begin_end_block() {
+    g_begin_end  = new name("begin_end");
+    register_annotation(*g_begin_end);
+
+    g_begin_end_element = new name("begin_end_element");
+    register_annotation(*g_begin_end_element);
+}
+
+void finalize_begin_end_block() {
+    delete g_begin_end;
+    delete g_begin_end_element;
+}
+}

src/frontends/lean/begin_end_block.h

@@ -0,0 +1,17 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "frontends/lean/parser.h"
+namespace lean {
+expr parse_begin_end_core(parser & p, pos_info const & start_pos, name const & end_token, bool nested = false);
+expr parse_begin_end(parser & p, unsigned, expr const *, pos_info const & pos);
+bool is_begin_end_block(expr const & e);
+void get_begin_end_block_elements(expr const & e, buffer<expr> & elems);
+expr update_begin_end_block(expr const & e, buffer<expr> const & elems);
+void initialize_begin_end_block();
+void finalize_begin_end_block();
+}

src/frontends/lean/builtin_exprs.cpp

@@ -33,6 +33,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/match_expr.h"
 #include "frontends/lean/decl_util.h"
 #include "frontends/lean/brackets.h"
+#include "frontends/lean/begin_end_block.h"
 
 #ifndef LEAN_DEFAULT_PARSER_CHECKPOINT_HAVE
 #define LEAN_DEFAULT_PARSER_CHECKPOINT_HAVE true
@@ -165,15 +166,6 @@ static expr parse_by(parser & p, unsigned, expr const *, pos_info const & pos) {
     return p.save_pos(mk_by(r), pos);
 }
 
-static expr parse_begin_end_core(parser & /*p*/, pos_info const & start_pos,
-                                 name const & /*end_token*/, bool /*nested*/ = false) {
-    throw parser_error("begin-end-exprs have been disabled", start_pos);
-}
-
-static expr parse_begin_end(parser & p, unsigned, expr const *, pos_info const & pos) {
-    return parse_begin_end_core(p, pos, get_end_tk());
-}
-
 static expr parse_proof(parser & p);
 
 static expr parse_proof(parser & p) {

src/frontends/lean/init_module.cpp

@@ -23,6 +23,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/elaborator.h"
 #include "frontends/lean/match_expr.h"
 #include "frontends/lean/notation_cmd.h"
+#include "frontends/lean/begin_end_block.h"
 
 namespace lean {
 void initialize_frontend_lean_module() {
@@ -45,8 +46,10 @@ void initialize_frontend_lean_module() {
     initialize_match_expr();
     initialize_elaborator();
     initialize_notation_cmd();
+    initialize_begin_end_block();
 }
 void finalize_frontend_lean_module() {
+    finalize_begin_end_block();
     finalize_notation_cmd();
     finalize_elaborator();
     finalize_match_expr();

src/library/constants.cpp

@@ -337,8 +337,11 @@ name const * g_sum_cases_on = nullptr;
 name const * g_sum_inl = nullptr;
 name const * g_sum_inr = nullptr;
 name const * g_tactic = nullptr;
-name const * g_tactic_try = nullptr;
 name const * g_tactic_constructor = nullptr;
+name const * g_tactic_interactive = nullptr;
+name const * g_tactic_consume = nullptr;
+name const * g_tactic_skip = nullptr;
+name const * g_tactic_try = nullptr;
 name const * g_to_string = nullptr;
 name const * g_to_int = nullptr;
 name const * g_to_real = nullptr;
@@ -696,8 +699,11 @@ void initialize_constants() {
     g_sum_inl = new name{"sum", "inl"};
     g_sum_inr = new name{"sum", "inr"};
     g_tactic = new name{"tactic"};
-    g_tactic_try = new name{"tactic", "try"};
     g_tactic_constructor = new name{"tactic", "constructor"};
+    g_tactic_interactive = new name{"tactic", "interactive"};
+    g_tactic_consume = new name{"tactic", "consume"};
+    g_tactic_skip = new name{"tactic", "skip"};
+    g_tactic_try = new name{"tactic", "try"};
     g_to_string = new name{"to_string"};
     g_to_int = new name{"to_int"};
     g_to_real = new name{"to_real"};
@@ -1056,8 +1062,11 @@ void finalize_constants() {
     delete g_sum_inl;
     delete g_sum_inr;
     delete g_tactic;
-    delete g_tactic_try;
     delete g_tactic_constructor;
+    delete g_tactic_interactive;
+    delete g_tactic_consume;
+    delete g_tactic_skip;
+    delete g_tactic_try;
     delete g_to_string;
     delete g_to_int;
     delete g_to_real;
@@ -1415,8 +1424,11 @@ name const & get_sum_cases_on_name() { return *g_sum_cases_on; }
 name const & get_sum_inl_name() { return *g_sum_inl; }
 name const & get_sum_inr_name() { return *g_sum_inr; }
 name const & get_tactic_name() { return *g_tactic; }
-name const & get_tactic_try_name() { return *g_tactic_try; }
 name const & get_tactic_constructor_name() { return *g_tactic_constructor; }
+name const & get_tactic_interactive_name() { return *g_tactic_interactive; }
+name const & get_tactic_consume_name() { return *g_tactic_consume; }
+name const & get_tactic_skip_name() { return *g_tactic_skip; }
+name const & get_tactic_try_name() { return *g_tactic_try; }
 name const & get_to_string_name() { return *g_to_string; }
 name const & get_to_int_name() { return *g_to_int; }
 name const & get_to_real_name() { return *g_to_real; }

src/library/constants.h

@@ -339,8 +339,11 @@ name const & get_sum_cases_on_name();
 name const & get_sum_inl_name();
 name const & get_sum_inr_name();
 name const & get_tactic_name();
-name const & get_tactic_try_name();
 name const & get_tactic_constructor_name();
+name const & get_tactic_interactive_name();
+name const & get_tactic_consume_name();
+name const & get_tactic_skip_name();
+name const & get_tactic_try_name();
 name const & get_to_string_name();
 name const & get_to_int_name();
 name const & get_to_real_name();

src/library/constants.txt

@@ -332,8 +332,11 @@ sum.cases_on
 sum.inl
 sum.inr
 tactic
-tactic.try
 tactic.constructor
+tactic.interactive
+tactic.consume
+tactic.skip
+tactic.try
 to_string
 to_int
 to_real

tests/lean/run/begin_end1.lean

@@ -0,0 +1,10 @@
+open tactic
+
+example (p q : Prop) : p → q → q ∧ p :=
+begin
+  intros,
+  constructor,
+  trace_state,
+  assumption,
+  assumption
+end