diff --git a/library/standard/tactic.lean b/library/standard/tactic.lean index 18c4e457a2..d3f392ab6e 100644 --- a/library/standard/tactic.lean +++ b/library/standard/tactic.lean @@ -3,6 +3,7 @@ -- Author: Leonardo de Moura import logic +namespace tactic -- This is just a trick to embed the 'tactic language' as a -- Lean expression. We should view 'tactic' as automation -- that when execute produces a term. @@ -14,19 +15,19 @@ inductive tactic : Type := -- uses them when converting Lean expressions into actual tactic objects. -- The bultin 'by' construct triggers the process of converting a -- a term of type 'tactic' into a tactic that sythesizes a term -definition then_tac (t1 t2 : tactic) : tactic := tactic_value -definition orelse_tac (t1 t2 : tactic) : tactic := tactic_value -definition repeat_tac (t : tactic) : tactic := tactic_value -definition now_tac : tactic := tactic_value -definition exact_tac : tactic := tactic_value -definition state_tac : tactic := tactic_value -definition fail_tac : tactic := tactic_value -definition id_tac : tactic := tactic_value -definition beta_tac : tactic := tactic_value +definition and_then (t1 t2 : tactic) : tactic := tactic_value +definition or_else (t1 t2 : tactic) : tactic := tactic_value +definition repeat (t : tactic) : tactic := tactic_value +definition now : tactic := tactic_value +definition exact : tactic := tactic_value +definition state : tactic := tactic_value +definition fail : tactic := tactic_value +definition id : tactic := tactic_value +definition beta : tactic := tactic_value definition apply {B : Type} (b : B) : tactic := tactic_value -definition unfold_tac {B : Type} (b : B) : tactic := tactic_value - -infixl `;`:200 := then_tac -infixl `|`:100 := orelse_tac -notation `!`:max t:max := repeat_tac t +definition unfold {B : Type} (b : B) : tactic := tactic_value +infixl `;`:200 := and_then +infixl `|`:100 := or_else +notation `!`:max t:max := repeat t +end diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index bf89c1a931..c58b3b1f35 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -623,10 +623,22 @@ public: }); } + format pp_indent_expr(expr const & e) { + return ::lean::pp_indent_expr(m_ios.get_formatter(), m_env, m_ios.get_options(), e); + } + optional get_tactic_for(substitution const & substitution, expr const & mvar) { if (auto it = m_tactic_hints.find(mlocal_name(mvar))) { expr pre_tac = substitution.instantiate_metavars_wo_jst(*it); - return optional(expr_to_tactic(m_env, pre_tac, m_pos_provider)); + try { + return optional(expr_to_tactic(m_env, pre_tac, m_pos_provider)); + } catch (expr_to_tactic_exception & ex) { + regular out(m_env, m_ios); + display_error_pos(out, m_pos_provider, mvar); + out << " " << ex.what(); + out << pp_indent_expr(pre_tac) << endl << "failed at:" << pp_indent_expr(ex.get_expr()) << endl; + return optional(); + } } else { // TODO(Leo): m_env tactic hints return optional(); @@ -689,9 +701,9 @@ public: static format pp_type_mismatch(formatter const & fmt, environment const & env, options const & opts, expr const & expected_type, expr const & given_type) { format r("type mismatch, expected type"); - r += pp_indent_expr(fmt, env, opts, expected_type); + r += ::lean::pp_indent_expr(fmt, env, opts, expected_type); r += compose(line(), format("given type:")); - r += pp_indent_expr(fmt, env, opts, given_type); + r += ::lean::pp_indent_expr(fmt, env, opts, given_type); return r; } diff --git a/src/library/tactic/expr_to_tactic.cpp b/src/library/tactic/expr_to_tactic.cpp index 347657382c..eb16bc3720 100644 --- a/src/library/tactic/expr_to_tactic.cpp +++ b/src/library/tactic/expr_to_tactic.cpp @@ -38,20 +38,20 @@ tactic expr_to_tactic(environment const & env, expr const & e, pos_info_provider return expr_to_tactic(env, v, p); } } - throw exception("failed to convert expression into tactic"); + throw expr_to_tactic_exception(e, "failed to convert expression into tactic"); } else if (is_lambda(f)) { buffer locals; get_app_rev_args(e, locals); return expr_to_tactic(env, apply_beta(f, locals.size(), locals.data()), p); } else { - throw exception("failed to convert expression into tactic"); + throw expr_to_tactic_exception(e, "failed to convert expression into tactic"); } } register_simple_tac::register_simple_tac(name const & n, std::function f) { register_expr_to_tactic(n, [=](environment const &, expr const & e, pos_info_provider const *) { if (!is_constant(e)) - throw exception("invalid constant tactic"); + throw expr_to_tactic_exception(e, "invalid constant tactic"); return f(); }); } @@ -61,7 +61,7 @@ register_bin_tac::register_bin_tac(name const & n, std::function args; get_app_args(e, args); if (args.size() != 2) - throw exception("invalid binary tactic, it must have two arguments"); + throw expr_to_tactic_exception(e, "invalid binary tactic, it must have two arguments"); return f(expr_to_tactic(env, args[0], p), expr_to_tactic(env, args[1], p)); }); @@ -72,29 +72,30 @@ register_unary_tac::register_unary_tac(name const & n, std::function args; get_app_args(e, args); if (args.size() != 1) - throw exception("invalid unary tactic, it must have one argument"); + throw expr_to_tactic_exception(e, "invalid unary tactic, it must have one argument"); return f(expr_to_tactic(env, args[0], p)); }); } -static register_simple_tac reg_id(name("id_tac"), []() { return id_tactic(); }); -static register_simple_tac reg_now(name("now_tac"), []() { return now_tactic(); }); -static register_simple_tac reg_exact(name("exact_tac"), []() { return assumption_tactic(); }); -static register_simple_tac reg_fail(name("fail_tac"), []() { return fail_tactic(); }); -static register_simple_tac reg_beta(name("beta_tac"), []() { return beta_tactic(); }); -static register_bin_tac reg_then(name("then_tac"), [](tactic const & t1, tactic const & t2) { return then(t1, t2); }); -static register_bin_tac reg_orelse(name("orelse_tac"), [](tactic const & t1, tactic const & t2) { return orelse(t1, t2); }); -static register_unary_tac reg_repeat(name("repeat_tac"), [](tactic const & t1) { return repeat(t1); }); -static register_tac reg_state(name("state_tac"), [](environment const &, expr const & e, pos_info_provider const * p) { +static name g_tac("tactic"); +static register_simple_tac reg_id(name(g_tac, "id"), []() { return id_tactic(); }); +static register_simple_tac reg_now(name(g_tac, "now"), []() { return now_tactic(); }); +static register_simple_tac reg_exact(name(g_tac, "exact"), []() { return assumption_tactic(); }); +static register_simple_tac reg_fail(name(g_tac, "fail"), []() { return fail_tactic(); }); +static register_simple_tac reg_beta(name(g_tac, "beta"), []() { return beta_tactic(); }); +static register_bin_tac reg_then(name(g_tac, "and_then"), [](tactic const & t1, tactic const & t2) { return then(t1, t2); }); +static register_bin_tac reg_orelse(name(g_tac, "or_else"), [](tactic const & t1, tactic const & t2) { return orelse(t1, t2); }); +static register_unary_tac reg_repeat(name(g_tac, "repeat"), [](tactic const & t1) { return repeat(t1); }); +static register_tac reg_state(name(g_tac, "state"), [](environment const &, expr const & e, pos_info_provider const * p) { if (p) return trace_state_tactic(std::string(p->get_file_name()), p->get_pos_info(e)); else return trace_state_tactic("unknown", mk_pair(0, 0)); }); -static register_tac reg_apply(name("apply"), [](environment const &, expr const & e, pos_info_provider const *) { +static register_tac reg_apply(name(g_tac, "apply"), [](environment const &, expr const & e, pos_info_provider const *) { return apply_tactic(app_arg(e)); }); -static register_tac reg_unfold(name("unfold_tac"), [](environment const &, expr const & e, pos_info_provider const *) { +static register_tac reg_unfold(name(g_tac, "unfold"), [](environment const &, expr const & e, pos_info_provider const *) { expr id = get_app_fn(app_arg(e)); if (!is_constant(id)) return fail_tactic(); diff --git a/src/library/tactic/expr_to_tactic.h b/src/library/tactic/expr_to_tactic.h index b02c1c4ce9..d805720a6f 100644 --- a/src/library/tactic/expr_to_tactic.h +++ b/src/library/tactic/expr_to_tactic.h @@ -9,6 +9,13 @@ Author: Leonardo de Moura #include "library/tactic/tactic.h" namespace lean { +class expr_to_tactic_exception : public exception { + expr m_expr; +public: + expr_to_tactic_exception(expr const & e, char const * msg):exception(msg), m_expr(e) {} + expr const & get_expr() const { return m_expr; } +}; + typedef std::function expr_to_tactic_fn; void register_expr_to_tactic(name const & n, expr_to_tactic_fn const & fn); struct register_tac { diff --git a/tests/lean/run/have5.lean b/tests/lean/run/have5.lean index 7a080d4417..69de80fa08 100644 --- a/tests/lean/run/have5.lean +++ b/tests/lean/run/have5.lean @@ -1,11 +1,12 @@ import standard +using tactic variables a b c d : Bool axiom Ha : a axiom Hb : b axiom Hc : c print raw - have H1 : a, by exact_tac, - then have H2 : b, by exact_tac, - have H3 : c, by exact_tac, - then have H4 : d, by exact_tac, + have H1 : a, by exact, + then have H2 : b, by exact, + have H3 : c, by exact, + then have H4 : d, by exact, H4 \ No newline at end of file diff --git a/tests/lean/run/t8.lean b/tests/lean/run/t8.lean index d10e119f4e..316343cbb8 100644 --- a/tests/lean/run/t8.lean +++ b/tests/lean/run/t8.lean @@ -1,2 +1,3 @@ import standard -print raw (by exact_tac) \ No newline at end of file +using tactic +print raw (by exact) \ No newline at end of file diff --git a/tests/lean/run/tactic1.lean b/tests/lean/run/tactic1.lean index 24ce0f6b0c..09ed65769c 100644 --- a/tests/lean/run/tactic1.lean +++ b/tests/lean/run/tactic1.lean @@ -1,5 +1,5 @@ -import logic -import tactic +import standard +using tactic theorem tst {A B : Bool} (H1 : A) (H2 : B) : A -:= by exact_tac +:= by exact diff --git a/tests/lean/run/tactic2.lean b/tests/lean/run/tactic2.lean index 8db30957f7..1c66a94205 100644 --- a/tests/lean/run/tactic2.lean +++ b/tests/lean/run/tactic2.lean @@ -1,7 +1,7 @@ -import logic -import tactic +import standard +using tactic theorem tst {A B : Bool} (H1 : A) (H2 : B) : A -:= by state_tac; exact_tac +:= by state; exact check tst \ No newline at end of file diff --git a/tests/lean/run/tactic3.lean b/tests/lean/run/tactic3.lean index ef8a79712e..4906e84cf2 100644 --- a/tests/lean/run/tactic3.lean +++ b/tests/lean/run/tactic3.lean @@ -1,10 +1,9 @@ -import logic -import tactic +import standard using tactic theorem tst {A B : Bool} (H1 : A) (H2 : B) : A -:= by state_tac; now_tac | - state_tac; fail_tac | - exact_tac +:= by state; now | + state; fail | + exact check tst \ No newline at end of file diff --git a/tests/lean/run/tactic4.lean b/tests/lean/run/tactic4.lean index 97d0de97c1..43ae4be558 100644 --- a/tests/lean/run/tactic4.lean +++ b/tests/lean/run/tactic4.lean @@ -1,11 +1,12 @@ import standard +using tactic (renaming id->id_tac) definition id {A : Type} (a : A) := a -definition simple_tac {A : Bool} : tactic -:= unfold_tac @id.{1}; exact_tac +definition simple {A : Bool} : tactic +:= unfold @id.{1}; exact theorem tst {A B : Bool} (H1 : A) (H2 : B) : id A -:= by simple_tac +:= by simple check tst diff --git a/tests/lean/run/tactic5.lean b/tests/lean/run/tactic5.lean index 32a5873e76..ac9919fd76 100644 --- a/tests/lean/run/tactic5.lean +++ b/tests/lean/run/tactic5.lean @@ -1,8 +1,9 @@ import standard +using tactic (renaming id->id_tac) definition id {A : Type} (a : A) := a theorem tst {A B : Bool} (H1 : A) (H2 : B) : id A -:= by !(unfold_tac @id; state_tac); exact_tac +:= by !(unfold @id; state); exact check tst \ No newline at end of file diff --git a/tests/lean/run/tactic6.lean b/tests/lean/run/tactic6.lean index 6fc9e6b51c..455dbb3e7d 100644 --- a/tests/lean/run/tactic6.lean +++ b/tests/lean/run/tactic6.lean @@ -1,8 +1,9 @@ import standard +using tactic (renaming id->id_tac) definition id {A : Type} (a : A) := a theorem tst {A B : Bool} (H1 : A) (H2 : B) : id A -:= by unfold_tac id; exact_tac +:= by unfold id; exact check tst