feat(frontends/lean): improve error messages when users forget to import 'tactic'

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

src/frontends/lean/builtin_exprs.cpp

@@ -129,10 +129,12 @@ static expr parse_placeholder(parser & p, unsigned, expr const *, pos_info const
 
 static expr parse_by(parser & p, unsigned, expr const *, pos_info const & pos) {
     expr t = p.parse_expr();
-    return p.save_pos(mk_by(t), pos);
+    return p.mk_by(t, pos);
 }
 
-static expr parse_proof_qed(parser & p, unsigned, expr const *, pos_info const &) {
+static expr parse_proof_qed(parser & p, unsigned, expr const *, pos_info const & pos) {
+    if (!p.has_tactic_decls())
+        throw parser_error("invalid 'proof' expression, tactic module has not been imported", pos);
     optional<expr> pre_tac = get_proof_qed_pre_tactic(p.env());
     optional<expr> r;
     while (true) {
@@ -148,7 +150,7 @@ static expr parse_proof_qed(parser & p, unsigned, expr const *, pos_info const &
         if (p.curr_is_token(g_qed)) {
             auto pos = p.pos();
             p.next();
-            return p.save_pos(mk_by(*r), pos);
+            return p.mk_by(*r, pos);
         } else if (p.curr_is_token(g_comma)) {
             p.next();
         } else {
@@ -167,7 +169,7 @@ static expr parse_proof(parser & p, expr const & prop) {
         auto pos = p.pos();
         p.next();
         expr t = p.parse_expr();
-        return p.save_pos(mk_by(t), pos);
+        return p.mk_by(t, pos);
     } else if (p.curr_is_token(g_using)) {
         // parse: 'using' locals* ',' proof
         auto using_pos = p.pos();

src/frontends/lean/parser.cpp

@@ -28,6 +28,7 @@ Author: Leonardo de Moura
 #include "library/num.h"
 #include "library/string.h"
 #include "library/error_handling/error_handling.h"
+#include "library/tactic/expr_to_tactic.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/parser_bindings.h"
 #include "frontends/lean/notation_cmd.h"
@@ -100,6 +101,18 @@ parser::parser(environment const & env, io_state const & ios,
                    [&]() { sync_command(); });
 }
 
+bool parser::has_tactic_decls() {
+    if (!m_has_tactic_decls)
+        m_has_tactic_decls = ::lean::has_tactic_decls(m_env);
+    return *m_has_tactic_decls;
+}
+
+expr parser::mk_by(expr const & t, pos_info const & pos) {
+    if (!has_tactic_decls())
+        throw parser_error("invalid 'by' expression, tactic module has not been imported", pos);
+    return save_pos(::lean::mk_by(t), pos);
+}
+
 void parser::updt_options() {
     m_verbose = get_verbose(m_ios.get_options());
     m_show_errors = get_parser_show_errors(m_ios.get_options());

src/frontends/lean/parser.h

@@ -66,6 +66,7 @@ class parser {
     bool                    m_no_undef_id_error;
     optional<bool>          m_has_num;
     optional<bool>          m_has_string;
+    optional<bool>          m_has_tactic_decls;
 
     void display_error_pos(unsigned line, unsigned pos);
     void display_error_pos(pos_info p);
@@ -139,6 +140,9 @@ public:
     local_level_decls const & get_local_level_decls() const { return m_local_level_decls; }
     local_expr_decls const & get_local_expr_decls() const { return m_local_decls; }
 
+    bool has_tactic_decls();
+    expr mk_by(expr const & t, pos_info const & pos);
+
     void updt_options();
     template<typename T> void set_option(name const & n, T const & v) { m_ios.set_option(n, v); }
 

src/library/tactic/expr_to_tactic.cpp

@@ -25,18 +25,31 @@ void register_expr_to_tactic(name const & n, expr_to_tactic_fn const & fn) {
     get_expr_to_tactic_map().insert(mk_pair(n, fn));
 }
 
-static name g_tac("tactic"), g_builtin_tac(g_tac, "builtin_tactic");
+static name g_tac("tactic"), g_tac_name(g_tac, "tactic"), g_builtin_tac_name(g_tac, "builtin_tactic");
-static name g_tac_name(g_tac, "tactic"), g_exact_tac_name(g_tac, "exact"), g_and_then_tac_name(g_tac, "and_then");
+static name g_exact_tac_name(g_tac, "exact"), g_and_then_tac_name(g_tac, "and_then");
 static name g_or_else_tac_name(g_tac, "or_else"), g_repeat_tac_name(g_tac, "repeat");
 static expr g_exact_tac_fn(Const(g_exact_tac_name)), g_and_then_tac_fn(Const(g_and_then_tac_name));
 static expr g_or_else_tac_fn(Const(g_or_else_tac_name)), g_repeat_tac_fn(Const(g_repeat_tac_name));
-static expr g_tac_type(Const(g_tac_name));
+static expr g_tac_type(Const(g_tac_name)), g_builtin_tac(Const(g_builtin_tac_name));
 expr const & get_exact_tac_fn() { return g_exact_tac_fn; }
 expr const & get_and_then_tac_fn() { return g_and_then_tac_fn; }
 expr const & get_or_else_tac_fn() { return g_or_else_tac_fn; }
 expr const & get_repeat_tac_fn() { return g_repeat_tac_fn; }
 expr const & get_tactic_type() { return g_tac_type; }
 
+bool has_tactic_decls(environment const & env) {
+    try {
+        type_checker tc(env);
+        return
+            tc.infer(g_builtin_tac) == g_tac_type &&
+            tc.infer(g_and_then_tac_fn) == g_tac_type >> (g_tac_type >> g_tac_type) &&
+            tc.infer(g_or_else_tac_fn) == g_tac_type >> (g_tac_type >> g_tac_type) &&
+            tc.infer(g_repeat_tac_fn) == g_tac_type >> g_tac_type;
+    } catch (...) {
+        return false;
+    }
+}
+
 static void throw_failed(expr const & e) {
     throw expr_to_tactic_exception(e, "failed to convert expression into tactic");
 }
@@ -45,7 +58,7 @@ static void throw_failed(expr const & e) {
 static bool is_builtin_tactic(expr const & v) {
     if (is_lambda(v))
         return is_builtin_tactic(binding_body(v));
-    else if (is_constant(v) && const_name(v) == g_builtin_tac)
+    else if (v == g_builtin_tac)
         return true;
     else
         return false;

src/library/tactic/expr_to_tactic.h

@@ -9,6 +9,44 @@ Author: Leonardo de Moura
 #include "library/tactic/tactic.h"
 
 namespace lean {
+/**
+   \brief Return true iff the environment \c env contains the following declarations
+   in the namespace 'tactic'
+       builtin_tactic : tactic
+       and_then : tactic -> tactic -> tactic
+       or_else  : tactic -> tactic -> tactic
+       repeat   : tactic -> tactic
+*/
+bool has_tactic_decls(environment const & env);
+
+/**
+   \brief Creates a tactic by 'executing' \c e. Definitions are unfolded, whnf procedure is invoked,
+   and definitions marked as 'tactic.builtin_tactic' are handled by the code registered using
+   \c register_expr_to_tactic.
+*/
+tactic expr_to_tactic(environment const & env, expr const & e, pos_info_provider const *p);
+
+/**
+   \brief Create an expression `by t`, where \c t is an expression of type `tactic`.
+   This kind of expression only affects the elaborator, the kernel will reject
+   any declaration that contains it.
+
+   \post get_by_arg(mk_by(t)) == t
+   \post is_by(mk_by(t))
+*/
+expr mk_by(expr const & t);
+/** \brief Return true iff \c t is an expression created using \c mk_by */
+bool is_by(expr const & t);
+/** \see mk_by */
+expr const & get_by_arg(expr const & t);
+
+expr const & get_tactic_type();
+expr const & get_exact_tac_fn();
+expr const & get_and_then_tac_fn();
+expr const & get_or_else_tac_fn();
+expr const & get_repeat_tac_fn();
+
+/** \brief Exception used to report a problem when an expression is being converted into a tactic. */
 class expr_to_tactic_exception : public tactic_exception {
 public:
     expr_to_tactic_exception(expr const & e, char const * msg):tactic_exception(e, msg) {}
@@ -16,7 +54,10 @@ public:
 };
 
 typedef std::function<tactic(type_checker & tc, expr const & e, pos_info_provider const *)> expr_to_tactic_fn;
+
+/** \brief Register a new "procedural attachment" for expr_to_tactic. */
 void register_expr_to_tactic(name const & n, expr_to_tactic_fn const & fn);
+
 struct register_tac {
     register_tac(name const & n, expr_to_tactic_fn fn) { register_expr_to_tactic(n, fn); }
 };
@@ -32,15 +73,4 @@ struct register_unary_tac {
 struct register_unary_num_tac {
     register_unary_num_tac(name const & n, std::function<tactic(tactic const &, unsigned)> f);
 };
-
-expr const & get_tactic_type();
-expr const & get_exact_tac_fn();
-expr const & get_and_then_tac_fn();
-expr const & get_or_else_tac_fn();
-expr const & get_repeat_tac_fn();
-
-tactic expr_to_tactic(environment const & env, expr const & e, pos_info_provider const *p);
-expr mk_by(expr const & e);
-bool is_by(expr const & e);
-expr const & get_by_arg(expr const & e);
 }