From 5e15ac0c9272a1a8322714fd28778299f966eb1e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 22 Oct 2014 15:18:43 -0700 Subject: [PATCH] feat(library/tactic): add new approach for embedding non-elaborated expressions into tactics --- library/tools/tactic.lean | 9 ++++ src/frontends/lean/builtin_exprs.cpp | 2 + src/frontends/lean/builtin_tactics.cpp | 8 --- src/frontends/lean/elaborator.cpp | 23 ++++---- src/frontends/lean/token_table.cpp | 2 +- src/library/tactic/apply_tactic.cpp | 10 ++-- src/library/tactic/expr_to_tactic.cpp | 75 ++++++++++++++++++++++++++ src/library/tactic/expr_to_tactic.h | 6 +++ tests/lean/run/beginend2.lean | 6 +-- 9 files changed, 115 insertions(+), 26 deletions(-) diff --git a/library/tools/tactic.lean b/library/tools/tactic.lean index 251f9b60d..839f0c52f 100644 --- a/library/tools/tactic.lean +++ b/library/tools/tactic.lean @@ -36,6 +36,15 @@ opaque definition state : tactic := builtin opaque definition fail : tactic := builtin opaque definition id : tactic := builtin opaque definition beta : tactic := builtin + +-- This is just a trick to embed expressions into tactics. +-- The nested expressions are "raw". They tactic should +-- elaborate them when it is executed. +inductive expr : Type := +builtin : expr + +opaque definition apply (e : expr) : tactic := builtin + opaque definition unfold {B : Type} (b : B) : tactic := builtin opaque definition exact {B : Type} (b : B) : tactic := builtin opaque definition trace (s : string) : tactic := builtin diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 17cb81398..b43ac65da 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -115,6 +115,7 @@ 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) { + parser::no_undef_id_error_scope scope(p); expr t = p.parse_expr(); return p.mk_by(t, pos); } @@ -125,6 +126,7 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos) { optional pre_tac = get_begin_end_pre_tactic(p.env()); buffer tacs; bool first = true; + parser::no_undef_id_error_scope scope(p); while (!p.curr_is_token(get_end_tk())) { if (first) first = false; diff --git a/src/frontends/lean/builtin_tactics.cpp b/src/frontends/lean/builtin_tactics.cpp index dc6179381..bb299962a 100644 --- a/src/frontends/lean/builtin_tactics.cpp +++ b/src/frontends/lean/builtin_tactics.cpp @@ -6,7 +6,6 @@ Author: Leonardo de Moura */ #include #include "library/explicit.h" -#include "library/tactic/apply_tactic.h" #include "library/tactic/rename_tactic.h" #include "library/tactic/intros_tactic.h" #include "frontends/lean/parser.h" @@ -18,12 +17,6 @@ namespace lean { using notation::transition; using notation::mk_ext_action; -static expr parse_apply(parser & p, unsigned, expr const *, pos_info const & pos) { - parser::no_undef_id_error_scope scope(p); - expr e = p.parse_expr(LEAN_APPLY_RBP); - return p.save_pos(mk_apply_tactic_macro(e), pos); -} - static expr parse_rename(parser & p, unsigned, expr const *, pos_info const & pos) { name from = p.check_id_next("invalid 'rename' tactic, identifier expected"); name to = p.check_id_next("invalid 'rename' tactic, identifier expected"); @@ -41,7 +34,6 @@ static expr parse_intros(parser & p, unsigned, expr const *, pos_info const & po void init_nud_tactic_table(parse_table & r) { expr x0 = mk_var(0); - r = r.add({transition("apply", mk_ext_action(parse_apply))}, x0); r = r.add({transition("rename", mk_ext_action(parse_rename))}, x0); r = r.add({transition("intros", mk_ext_action(parse_intros))}, x0); } diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index d3f7b7be3..2d6d83a59 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -553,15 +553,20 @@ expr elaborator::visit_app(expr const & e, constraint_seq & cs) { } constraint_seq a_cs; expr d_type = binding_domain(f_type); - expr a = visit_expecting_type_of(app_arg(e), d_type, a_cs); - expr a_type = infer_type(a, a_cs); - expr r = mk_app(f, a, e.get_tag()); - - justification j = mk_app_justification(r, a, d_type, a_type); - auto new_a_cs = ensure_has_type(a, a_type, d_type, j, m_relax_main_opaque); - expr new_a = new_a_cs.first; - cs += f_cs + new_a_cs.second + a_cs; - return update_app(r, app_fn(r), new_a); + if (d_type == get_tactic_expr_type()) { + expr r = mk_app(f, mk_tactic_expr(app_arg(e)), e.get_tag()); + cs += f_cs + a_cs; + return r; + } else { + expr a = visit_expecting_type_of(app_arg(e), d_type, a_cs); + expr a_type = infer_type(a, a_cs); + expr r = mk_app(f, a, e.get_tag()); + justification j = mk_app_justification(r, a, d_type, a_type); + auto new_a_cs = ensure_has_type(a, a_type, d_type, j, m_relax_main_opaque); + expr new_a = new_a_cs.first; + cs += f_cs + new_a_cs.second + a_cs; + return update_app(r, app_fn(r), new_a); + } } expr elaborator::visit_placeholder(expr const & e, constraint_seq & cs) { diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 4f1dc67a4..7eca1223b 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -76,7 +76,7 @@ void init_token_table(token_table & t) { {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {":=", 0}, {"--", 0}, {"#", 0}, {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"proof", g_max_prec}, {"qed", 0}, {"@", g_max_prec}, {"sorry", g_max_prec}, {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {"local", 0}, - {"apply", 0}, {"rename", 0}, {"intros", 0}, {nullptr, 0}}; + {"rename", 0}, {"intros", 0}, {nullptr, 0}}; char const * commands[] = {"theorem", "axiom", "variable", "protected", "private", "opaque", "definition", "coercion", diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp index 189f07335..233ded8c7 100644 --- a/src/library/tactic/apply_tactic.cpp +++ b/src/library/tactic/apply_tactic.cpp @@ -139,11 +139,11 @@ expr mk_apply_tactic_macro(expr const & e) { void initialize_apply_tactic() { g_apply_tactic_name = new name({"tactic", "apply"}); - auto fn = [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) { - check_macro_args(e, 1, "invalid 'apply' tactic, it must have one argument"); - return apply_tactic(fn, macro_arg(e, 0)); - }; - register_tactic_macro(*g_apply_tactic_name, fn); + register_tac(*g_apply_tactic_name, + [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) { + check_tactic_expr(app_arg(e), "invalid 'apply' tactic, invalid argument"); + return apply_tactic(fn, get_tactic_expr_expr(app_arg(e))); + }); register_simple_tac(name({"tactic", "eassumption"}), []() { return eassumption_tactic(); }); diff --git a/src/library/tactic/expr_to_tactic.cpp b/src/library/tactic/expr_to_tactic.cpp index dba5a5199..0de81754f 100644 --- a/src/library/tactic/expr_to_tactic.cpp +++ b/src/library/tactic/expr_to_tactic.cpp @@ -57,14 +57,70 @@ bool has_tactic_decls(environment const & env) { } } +static expr * g_tactic_expr_type = nullptr; +static expr * g_tactic_expr_builtin = nullptr; + +expr const & get_tactic_expr_type() { return *g_tactic_expr_type; } +expr const & get_tactic_expr_builtin() { return *g_tactic_expr_builtin; } + +static name * g_tactic_expr_name = nullptr; +static std::string * g_tactic_expr_opcode = nullptr; + static name * g_tactic_name = nullptr; static std::string * g_tactic_opcode = nullptr; +name const & get_tactic_expr_name() { return *g_tactic_expr_name; } +std::string const & get_tactic_expr_opcode() { return *g_tactic_expr_opcode; } + name const & get_tactic_name() { return *g_tactic_name; } std::string const & get_tactic_opcode() { return *g_tactic_opcode; } LEAN_THREAD_VALUE(bool, g_unfold_tactic_macros, true); +class tactic_expr_macro_definition_cell : public macro_definition_cell { +public: + tactic_expr_macro_definition_cell() {} + virtual name get_name() const { return get_tactic_expr_name(); } + virtual pair get_type(expr const &, extension_context &) const { + return mk_pair(get_tactic_expr_type(), constraint_seq()); + } + virtual optional expand(expr const &, extension_context &) const { + // Remark: small hack for conditionally expanding tactic expr macros. + // When type checking a macro definition, we want to unfold it, + // otherwise the kernel will not accept it. + // When converting it to a tactic object, we don't want to unfold it. + // The procedure expr_to_tactic temporarily sets g_unfold_tactic_macros to false. + // This is a thread local storage. So, there is no danger. + if (g_unfold_tactic_macros) + return some_expr(get_tactic_expr_builtin()); + else + return none_expr(); + } + virtual void write(serializer & s) const { + s.write_string(get_tactic_expr_opcode()); + } +}; + +static macro_definition * g_tactic_expr_macro = nullptr; + +expr mk_tactic_expr(expr const & e) { + return mk_macro(*g_tactic_expr_macro, 1, &e, e.get_tag()); +} + +bool is_tactic_expr(expr const & e) { + return is_macro(e) && macro_def(e).get_name() == get_tactic_expr_name(); +} + +expr const & get_tactic_expr_expr(expr const & e) { + lean_assert(is_tactic_expr(e)); + return macro_arg(e, 0); +} + +void check_tactic_expr(expr const & e, char const * msg) { + if (!is_tactic_expr(e)) + throw expr_to_tactic_exception(e, msg); +} + /** \brief We use macros to wrap some builtin tactics that would not type check otherwise. Example: in the tactic `apply t`, `t` is a pre-term (i.e., a term before elaboration). Moreover its context depends on the goal it is applied to. @@ -289,6 +345,20 @@ void initialize_expr_to_tactic() { g_map = new expr_to_tactic_map(); g_tactic_name = new name("tactic"); + + g_tactic_expr_type = new expr(mk_constant(name(*g_tactic_name, "expr"))); + g_tactic_expr_builtin = new expr(mk_constant(name(const_name(*g_tactic_expr_type), "builtin"))); + g_tactic_expr_name = new name("tactic-expr"); + g_tactic_expr_opcode = new std::string("TACE"); + g_tactic_expr_macro = new macro_definition(new tactic_expr_macro_definition_cell()); + + register_macro_deserializer(*g_tactic_expr_opcode, + [](deserializer &, unsigned num, expr const * args) { + if (num != 1) + throw corrupted_stream_exception(); + return mk_tactic_expr(args[0]); + }); + g_tactic_opcode = new std::string("TAC"); g_tactic_macros = new tactic_macros(); @@ -364,6 +434,11 @@ void initialize_expr_to_tactic() { } void finalize_expr_to_tactic() { + delete g_tactic_expr_type; + delete g_tactic_expr_builtin; + delete g_tactic_expr_name; + delete g_tactic_expr_opcode; + delete g_tactic_expr_macro; delete g_fixpoint_tac; delete g_builtin_tac; delete g_tac_type; diff --git a/src/library/tactic/expr_to_tactic.h b/src/library/tactic/expr_to_tactic.h index c33993287..dbacb6edd 100644 --- a/src/library/tactic/expr_to_tactic.h +++ b/src/library/tactic/expr_to_tactic.h @@ -26,6 +26,12 @@ bool has_tactic_decls(environment const & env); */ tactic expr_to_tactic(environment const & env, elaborate_fn const & fn, expr const & e, pos_info_provider const * p); +expr const & get_tactic_expr_type(); +expr mk_tactic_expr(expr const & e); +bool is_tactic_expr(expr const & e); +expr const & get_tactic_expr_expr(expr const & e); +void check_tactic_expr(expr const & e, char const * msg); + /** \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 diff --git a/tests/lean/run/beginend2.lean b/tests/lean/run/beginend2.lean index 5483c1dc1..2489cd30c 100644 --- a/tests/lean/run/beginend2.lean +++ b/tests/lean/run/beginend2.lean @@ -6,7 +6,7 @@ open path (induction_on) definition concat_whisker2 {A} {x y z : A} (p p' : x ≈ y) (q q' : y ≈ z) (a : p ≈ p') (b : q ≈ q') : (whiskerR a q) ⬝ (whiskerL p' b) ≈ (whiskerL p b) ⬝ (whiskerR a q') := begin - apply induction_on b, - apply induction_on a, - apply (concat_1p _)⁻¹, + apply (induction_on b), + apply (induction_on a), + apply ((concat_1p _)⁻¹), end