From a3be63af73ca1068dab7069c04d19ce973d50457 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 8 Jul 2014 14:28:33 -0700 Subject: [PATCH] feat(frontends/lean): add tactic_hint command Signed-off-by: Leonardo de Moura --- library/standard/tactic.lean | 2 + src/emacs/lean-mode.el | 2 +- src/frontends/lean/CMakeLists.txt | 2 +- src/frontends/lean/builtin_cmds.cpp | 2 + src/frontends/lean/class.cpp | 17 ++-- src/frontends/lean/class.h | 2 +- src/frontends/lean/elaborator.cpp | 94 +++++++++++++------ src/frontends/lean/parser.cpp | 8 +- src/frontends/lean/parser.h | 4 + src/frontends/lean/proof_qed_ext.cpp | 9 +- src/frontends/lean/tactic_hint.cpp | 124 ++++++++++++++++++++++++++ src/frontends/lean/tactic_hint.h | 30 +++++++ src/frontends/lean/token_table.cpp | 2 +- src/kernel/type_checker.h | 1 + src/library/tactic/expr_to_tactic.cpp | 26 +++++- tests/lean/run/tactic24.lean | 23 +++++ 16 files changed, 297 insertions(+), 51 deletions(-) create mode 100644 src/frontends/lean/tactic_hint.cpp create mode 100644 src/frontends/lean/tactic_hint.h create mode 100644 tests/lean/run/tactic24.lean diff --git a/library/standard/tactic.lean b/library/standard/tactic.lean index 6269050dc..676ca800e 100644 --- a/library/standard/tactic.lean +++ b/library/standard/tactic.lean @@ -44,6 +44,8 @@ infixl ; := and_then notation `!` t:max := repeat t -- [ t_1 | ... | t_n ] notation notation `[` h:100 `|` r:(foldl 100 `|` (e r, or_else r e) h) `]` := r +-- [ t_1 || ... || t_n ] notation +notation `[` h:100 `||` r:(foldl 100 `||` (e r, par r e) h) `]` := r definition try (t : tactic) : tactic := [ t | id ] notation `?` t:max := try t definition repeat1 (t : tactic) : tactic := t ; !t diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el index 7fbd90be7..1ec6ce886 100644 --- a/src/emacs/lean-mode.el +++ b/src/emacs/lean-mode.el @@ -24,7 +24,7 @@ (define-generic-mode 'lean-mode ;; name of the mode to create '("--") ;; comments start with - '("import" "abbreviation" "opaque_hint" "definition" "hiding" "exposing" "parameter" "parameters" "proof" "qed" "conjecture" "hypothesis" "lemma" "corollary" "variable" "variables" "print" "theorem" "axiom" "inductive" "with" "universe" "alias" "help" "environment" "options" "precedence" "postfix" "prefix" "calc_trans" "calc_subst" "calc_refl" "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end" "using" "namespace" "builtin" "including" "class" "instance" "section" "set_option" "add_rewrite") ;; some keywords + '("import" "abbreviation" "opaque_hint" "tactic_hint" "definition" "hiding" "exposing" "parameter" "parameters" "proof" "qed" "conjecture" "hypothesis" "lemma" "corollary" "variable" "variables" "print" "theorem" "axiom" "inductive" "with" "universe" "alias" "help" "environment" "options" "precedence" "postfix" "prefix" "calc_trans" "calc_subst" "calc_refl" "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end" "using" "namespace" "builtin" "including" "class" "instance" "section" "set_option" "add_rewrite") ;; some keywords '(("\\_<\\(Bool\\|Int\\|Nat\\|Real\\|Type\\|TypeU\\|ℕ\\|ℤ\\)\\_>" . 'font-lock-type-face) ("\\_<\\(calc\\|have\\|show\\|by\\|in\\|let\\|forall\\|fun\\|exists\\|if\\|then\\|else\\|assume\\|take\\|obtain\\|from\\)\\_>" . font-lock-keyword-face) ("\"[^\"]*\"" . 'font-lock-string-face) diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt index c73b1ec49..69bd8f4bd 100644 --- a/src/frontends/lean/CMakeLists.txt +++ b/src/frontends/lean/CMakeLists.txt @@ -4,6 +4,6 @@ parser_pos_provider.cpp builtin_cmds.cpp builtin_exprs.cpp interactive.cpp notation_cmd.cpp calc.cpp decl_cmds.cpp util.cpp inductive_cmd.cpp elaborator.cpp dependencies.cpp parser_bindings.cpp proof_qed_ext.cpp -class.cpp pp_options.cpp) +class.cpp pp_options.cpp tactic_hint.cpp) target_link_libraries(lean_frontend ${LEAN_LIBS}) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index f09b78649..a98735e61 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -23,6 +23,7 @@ Author: Leonardo de Moura #include "frontends/lean/proof_qed_ext.h" #include "frontends/lean/decl_cmds.h" #include "frontends/lean/class.h" +#include "frontends/lean/tactic_hint.h" namespace lean { static name g_raw("raw"); @@ -306,6 +307,7 @@ cmd_table init_cmd_table() { register_calc_cmds(r); register_proof_qed_cmds(r); register_class_cmds(r); + register_tactic_hint_cmd(r); return r; } diff --git a/src/frontends/lean/class.cpp b/src/frontends/lean/class.cpp index 9eccbd856..83f6e4f6c 100644 --- a/src/frontends/lean/class.cpp +++ b/src/frontends/lean/class.cpp @@ -57,17 +57,22 @@ struct class_config { template class scoped_ext; typedef scoped_ext class_ext; +name get_class_name(environment const & env, expr const & e) { + if (!is_constant(e)) + throw exception("class expected, expression is not a constant"); + name const & c_name = const_name(e); + declaration c_d = env.get(c_name); + if (c_d.is_definition() && !c_d.is_opaque()) + throw exception(sstream() << "invalid class, '" << c_name << "' is a transparent definition"); + return c_name; +} + environment add_instance(environment const & env, name const & n) { declaration d = env.get(n); expr type = d.get_type(); while (is_pi(type)) type = binding_body(type); - if (!is_constant(get_app_fn(type))) - throw exception(sstream() << "invalid class instance declaration '" << n << "' resultant type must be a class"); - name const & c = const_name(get_app_fn(type)); - declaration c_d = env.get(c); - if (c_d.is_definition() && !c_d.is_opaque()) - throw exception(sstream() << "invalid class instance declaration, '" << c << "' is not a valid class, it is a transparent definition"); + name c = get_class_name(env, get_app_fn(type)); return class_ext::add_entry(env, get_dummy_ios(), class_entry(c, n)); } diff --git a/src/frontends/lean/class.h b/src/frontends/lean/class.h index f4aa04ef9..965ee406f 100644 --- a/src/frontends/lean/class.h +++ b/src/frontends/lean/class.h @@ -17,6 +17,6 @@ environment add_instance(environment const & env, name const & n); bool is_class(environment const & env, name const & c); /** \brief Return the instances of the given class. */ list get_class_instances(environment const & env, name const & c); - +name get_class_name(environment const & env, expr const & e); void register_class_cmds(cmd_table & r); } diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index a4b41183b..8e07c5f3a 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -31,6 +31,7 @@ Author: Leonardo de Moura #include "library/error_handling/error_handling.h" #include "frontends/lean/local_decls.h" #include "frontends/lean/class.h" +#include "frontends/lean/tactic_hint.h" #ifndef LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES #define LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES true @@ -122,7 +123,7 @@ public: class elaborator { typedef list context; typedef std::vector constraint_vect; - typedef name_map tactic_hints; + typedef name_map local_tactic_hints; typedef name_map mvar2meta; typedef std::unique_ptr type_checker_ptr; @@ -136,8 +137,8 @@ class elaborator { pos_info_provider * m_pos_provider; // optional expression position information used when reporting errors. justification m_accumulated; // accumulate justification of eagerly used substitutions constraint_vect m_constraints; // constraints that must be solved for the elaborated term to be type correct. - tactic_hints m_tactic_hints; // mapping from metavariable name ?m to tactic expression that should be used to solve it. - // this mapping is populated by the 'by tactic-expr' expression. + local_tactic_hints m_local_tactic_hints; // mapping from metavariable name ?m to tactic expression that should be used to solve it. + // this mapping is populated by the 'by tactic-expr' expression. mvar2meta m_mvar2meta; // mapping from metavariable ?m to the (?m l_1 ... l_n) where [l_1 ... l_n] are the local constants // representing the context where ?m was created. name_set m_displayed_errors; // set of metavariables that we already reported unsolved/unassigned @@ -552,7 +553,7 @@ public: lean_assert(is_by(e)); expr tac = visit(get_by_arg(e)); expr m = mk_meta(t, e.get_tag()); - m_tactic_hints.insert(mlocal_name(get_app_fn(m)), tac); + m_local_tactic_hints.insert(mlocal_name(get_app_fn(m)), tac); return m; } @@ -876,7 +877,7 @@ public: } optional get_pre_tactic_for(substitution & subst, expr const & mvar, name_set & visited) { - if (auto it = m_tactic_hints.find(mlocal_name(mvar))) { + if (auto it = m_local_tactic_hints.find(mlocal_name(mvar))) { expr pre_tac = subst.instantiate(*it); pre_tac = solve_unassigned_mvars(subst, pre_tac, visited); check_exact_tacs(pre_tac, subst); @@ -899,6 +900,58 @@ public: } } + optional get_local_tactic_hint(substitution & subst, expr const & mvar, name_set & visited) { + if (auto pre_tac = get_pre_tactic_for(subst, mvar, visited)) { + return pre_tactic_to_tactic(*pre_tac, mvar); + } else { + return optional(); + } + } + + /** \brief Try to instantiate meta-variable \c mvar (modulo its state ps) using the given tactic. + If it succeeds, then update subst with the solution. + If \c report_failure is true, then display error messages. to the user. + Return true iff the metavariable \c mvar has been assigned. + */ + bool try_using(substitution & subst, expr const & mvar, proof_state const & ps, tactic const & tac, bool report_failure) { + lean_assert(length(ps.get_goals()) == 1); + lean_assert(get_app_fn(head(ps.get_goals()).get_meta()) == mvar); // make sure ps is a really a proof state for mvar. + try { + proof_state_seq seq = tac(m_env, m_ios, ps); + auto r = seq.pull(); + if (!r) { + // tactic failed to produce any result + if (report_failure) + display_unsolved_proof_state(mvar, ps, "tactic failed"); + return false; + } else if (!empty(r->first.get_goals())) { + // tactic contains unsolved subgoals + if (report_failure) + display_unsolved_proof_state(mvar, r->first, "unsolved subgoals"); + return false; + } else { + subst = r->first.get_subst(); + expr v = subst.instantiate(mvar); + subst = subst.assign(mlocal_name(mvar), v); + return true; + } + } catch (tactic_exception & ex) { + if (report_failure) { + regular out(m_env, m_ios); + display_error_pos(out, m_pos_provider, ex.get_expr()); + out << " tactic failed: " << ex.what() << "\n"; + } + return false; + } + } + + bool try_using(substitution & subst, expr const & mvar, proof_state const & ps, list const & tacs) { + return std::any_of(tacs.begin(), tacs.end(), + [&](tactic_hint_entry const & e) { + return try_using(subst, mvar, ps, e.get_tactic(), false); + }); + } + void solve_unassigned_mvar(substitution & subst, expr mvar, name_set & visited) { if (visited.contains(mlocal_name(mvar))) return; @@ -916,30 +969,15 @@ public: // first solve unassigned metavariables in type type = solve_unassigned_mvars(subst, type, visited); proof_state ps(goals(goal(*meta, type)), subst, m_ngen.mk_child()); - optional pre_tac = get_pre_tactic_for(subst, mvar, visited); - if (!pre_tac) - return; - optional tac = pre_tactic_to_tactic(*pre_tac, mvar); - if (!tac) - return; - try { - proof_state_seq seq = (*tac)(m_env, m_ios, ps); - auto r = seq.pull(); - if (!r) { - // tactic failed to produce any result - display_unsolved_proof_state(mvar, ps, "tactic failed"); - } else if (!empty(r->first.get_goals())) { - // tactic contains unsolved subgoals - display_unsolved_proof_state(mvar, r->first, "unsolved subgoals"); - } else { - subst = r->first.get_subst(); - expr v = subst.instantiate(mvar); - subst = subst.assign(mlocal_name(mvar), v); + if (auto local_hint = get_local_tactic_hint(subst, mvar, visited)) { + try_using(subst, mvar, ps, *local_hint, true); + } else { + if (is_constant(get_app_fn(type))) { + name cls = const_name(get_app_fn(type)); + if (try_using(subst, mvar, ps, get_tactic_hints(m_env, cls))) + return; } - } catch (tactic_exception & ex) { - regular out(m_env, m_ios); - display_error_pos(out, m_pos_provider, ex.get_expr()); - out << " tactic failed: " << ex.what() << "\n"; + try_using(subst, mvar, ps, get_tactic_hints(m_env)); } } diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 2ec77d526..b64ff515c 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -469,22 +469,22 @@ expr parser::mk_Type() { } std::tuple parser::elaborate_relaxed(expr const & e) { - parser_pos_provider pp(m_pos_table, get_stream_name(), m_last_cmd_pos); + parser_pos_provider pp = get_pos_provider(); return ::lean::elaborate(m_env, m_local_level_decls, m_ios, e, &pp, false); } std::tuple parser::elaborate_type(expr const & e) { - parser_pos_provider pp(m_pos_table, get_stream_name(), m_last_cmd_pos); + parser_pos_provider pp = get_pos_provider(); return ::lean::elaborate(m_env, m_local_level_decls, m_ios, e, &pp, true, true); } std::tuple parser::elaborate_at(environment const & env, expr const & e) { - parser_pos_provider pp(m_pos_table, get_stream_name(), m_last_cmd_pos); + parser_pos_provider pp = get_pos_provider(); return ::lean::elaborate(env, m_local_level_decls, m_ios, e, &pp); } std::tuple parser::elaborate_definition(name const & n, expr const & t, expr const & v) { - parser_pos_provider pp(m_pos_table, get_stream_name(), m_last_cmd_pos); + parser_pos_provider pp = get_pos_provider(); return ::lean::elaborate(m_env, m_local_level_decls, m_ios, n, t, v, &pp); } diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 018e72132..03a8ce9ed 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -257,9 +257,13 @@ public: std::tuple elaborate_type(expr const & e); /** \brief Elaborate \c e in the given environment. */ std::tuple elaborate_at(environment const & env, expr const & e); + /** \brief Elaborate \c e (making sure the result does not have metavariables). */ + std::tuple elaborate(expr const & e) { return elaborate_at(m_env, e); } /** \brief Elaborate the definition n : t := v */ std::tuple elaborate_definition(name const & n, expr const & t, expr const & v); + parser_pos_provider get_pos_provider() const { return parser_pos_provider(m_pos_table, get_stream_name(), m_last_cmd_pos); } + /** parse all commands in the input stream */ bool operator()() { return parse_commands(); } }; diff --git a/src/frontends/lean/proof_qed_ext.cpp b/src/frontends/lean/proof_qed_ext.cpp index 19b5a49fe..36dbbab61 100644 --- a/src/frontends/lean/proof_qed_ext.cpp +++ b/src/frontends/lean/proof_qed_ext.cpp @@ -10,6 +10,7 @@ Author: Leonardo de Moura #include "library/kernel_serializer.h" #include "library/tactic/expr_to_tactic.h" #include "frontends/lean/parser.h" +#include "frontends/lean/tactic_hint.h" namespace lean { // This (scoped) environment extension allows us to set a tactic to be applied before every element @@ -84,12 +85,6 @@ optional get_proof_qed_pre_tactic(environment const & env) { return s.m_pre_tac; } -static expr parse_tactic_name(parser & p) { - auto pos = p.pos(); - name id = p.check_id_next("invalid proof_qed configuration command, indentifier expected"); - return p.id_to_expr(id, pos); -} - environment add_proof_qed_cmd(parser & p) { return add_proof_qed_pre_tactic(p.env(), parse_tactic_name(p)); } @@ -99,7 +94,7 @@ environment set_proof_qed_cmd(parser & p) { } void register_proof_qed_cmds(cmd_table & r) { - add_cmd(r, cmd_info("add_proof_qed", "add a new tactic to be automatically applied before every component in a 'proof-qed' block", + add_cmd(r, cmd_info("add_proof_qed", "add a new tactic to be automatically applied before every component in a 'proof-qed' block", add_proof_qed_cmd)); add_cmd(r, cmd_info("set_proof_qed", "reset the tactic that is automatically applied before every component in a 'proof-qed' block", set_proof_qed_cmd)); diff --git a/src/frontends/lean/tactic_hint.cpp b/src/frontends/lean/tactic_hint.cpp new file mode 100644 index 000000000..8faa5fd11 --- /dev/null +++ b/src/frontends/lean/tactic_hint.cpp @@ -0,0 +1,124 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include +#include "util/sstream.h" +#include "kernel/type_checker.h" +#include "library/scoped_ext.h" +#include "library/kernel_serializer.h" +#include "library/tactic/tactic.h" +#include "library/tactic/expr_to_tactic.h" +#include "frontends/lean/tactic_hint.h" +#include "frontends/lean/cmd_table.h" +#include "frontends/lean/parser.h" +#include "frontends/lean/class.h" + +namespace lean { +typedef list tactic_hint_entries; + +struct tactic_hint_state { + typedef rb_map class_tactics; + class_tactics m_class_tactics; + tactic_hint_entries m_tactics; +}; + +struct tactic_hint_config { + typedef tactic_hint_state state; + typedef tactic_hint_entry entry; + typedef tactic_hint_entries entries; + + static entries add(entries const & l, entry const & e) { + return cons(e, filter(l, [&](entry const & e1) { return e1.m_pre_tactic != e.m_pre_tactic; })); + } + + static void add_entry_core(state & s, entry const & e) { + if (e.m_class.is_anonymous()) + s.m_tactics = add(s.m_tactics, e); + else if (auto it = s.m_class_tactics.find(e.m_class)) + s.m_class_tactics.insert(e.m_class, add(*it, e)); + else + s.m_class_tactics.insert(e.m_class, entries(e)); + } + + static void add_entry(environment const & env, io_state const &, state & s, entry const & e) { + if (!e.m_compiled) { + entry new_e(e); + new_e.m_tactic = expr_to_tactic(env, e.m_pre_tactic, nullptr); + new_e.m_compiled = true; + add_entry_core(s, new_e); + } else { + add_entry_core(s, e); + } + } + + static name const & get_class_name() { + static name g_class_name("tactic_hint"); + return g_class_name; + } + + static std::string const & get_serialization_key() { + static std::string g_key("tachint"); + return g_key; + } + + static void write_entry(serializer & s, entry const & e) { + s << e.m_class << e.m_pre_tactic; + } + + static entry read_entry(deserializer & d) { + entry e; + d >> e.m_class >> e.m_pre_tactic; + return e; + } +}; + +template class scoped_ext; +typedef scoped_ext tactic_hint_ext; + +list get_tactic_hints(environment const & env, name const & c) { + tactic_hint_state const & s = tactic_hint_ext::get_state(env); + if (auto it = s.m_class_tactics.find(c)) + return *it; + else + return list(); +} + +list get_tactic_hints(environment const & env) { + tactic_hint_state const & s = tactic_hint_ext::get_state(env); + return s.m_tactics; +} + +expr parse_tactic_name(parser & p) { + auto pos = p.pos(); + name id = p.check_id_next("invalid tactic name, identifier expected"); + expr pre_tac = p.id_to_expr(id, pos); + if (!is_constant(pre_tac)) + throw parser_error(sstream() << "invalid tactic name, '" << id << "' is not a constant", pos); + expr pre_tac_type = p.env().get(const_name(pre_tac)).get_type(); + if (!is_constant(pre_tac_type) || const_name(pre_tac_type) != name({"tactic", "tactic"})) + throw parser_error(sstream() << "invalid tactic name, '" << id << "' is not a tactic", pos); + return pre_tac; +} + +static name g_lbracket("["); +static name g_rbracket("]"); + +environment tactic_hint_cmd(parser & p) { + name cls; + if (p.curr_is_token(g_lbracket)) { + p.next(); + cls = get_class_name(p.env(), p.parse_expr()); + p.check_token_next(g_rbracket, "invalid tactic hint, ']' expected"); + } + expr pre_tac = parse_tactic_name(p); + tactic tac = expr_to_tactic(p.env(), pre_tac, nullptr); + return tactic_hint_ext::add_entry(p.env(), get_dummy_ios(), tactic_hint_entry(cls, pre_tac, tac)); +} + +void register_tactic_hint_cmd(cmd_table & r) { + add_cmd(r, cmd_info("tactic_hint", "add a new tactic hint", tactic_hint_cmd)); +} +} diff --git a/src/frontends/lean/tactic_hint.h b/src/frontends/lean/tactic_hint.h new file mode 100644 index 000000000..314832bab --- /dev/null +++ b/src/frontends/lean/tactic_hint.h @@ -0,0 +1,30 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "library/tactic/tactic.h" +#include "frontends/lean/cmd_table.h" + +namespace lean { +class tactic_hint_entry { + friend class tactic_hint_config; + name m_class; + expr m_pre_tactic; + tactic m_tactic; + bool m_compiled; +public: + tactic_hint_entry():m_compiled(false) {} + tactic_hint_entry(name const & c, expr const & pre_tac, tactic const & tac): + m_class(c), m_pre_tactic(pre_tac), m_tactic(tac), m_compiled(true) {} + expr const & get_pre_tactic() const { return m_pre_tactic; } + tactic const & get_tactic() const { return m_tactic; } +}; +list get_tactic_hints(environment const & env, name const & cls_name); +list get_tactic_hints(environment const & env); +class parser; +expr parse_tactic_name(parser & p); +void register_tactic_hint_cmd(cmd_table & r); +} diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index c6c504a84..b44546065 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -77,7 +77,7 @@ token_table init_token_table() { "abbreviation", "opaque_hint", "evaluate", "check", "print", "end", "namespace", "section", "import", "abbreviation", "inductive", "record", "structure", "module", "universe", "precedence", "infixl", "infixr", "infix", "postfix", "prefix", "notation", - "exit", "set_option", "using", "calc_subst", "calc_refl", "calc_trans", + "exit", "set_option", "using", "calc_subst", "calc_refl", "calc_trans", "tactic_hint", "add_proof_qed", "set_proof_qed", "#setline", "class", "instance", nullptr}; std::pair aliases[] = diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h index 33433815c..31ef7dd95 100644 --- a/src/kernel/type_checker.h +++ b/src/kernel/type_checker.h @@ -113,6 +113,7 @@ public: ~type_checker(); environment const & env() const { return m_env; } + name_generator mk_ngen() { return m_gen.mk_child(); } /** \brief Return the type of \c t. diff --git a/src/library/tactic/expr_to_tactic.cpp b/src/library/tactic/expr_to_tactic.cpp index 4a3f93d29..752fde92a 100644 --- a/src/library/tactic/expr_to_tactic.cpp +++ b/src/library/tactic/expr_to_tactic.cpp @@ -84,14 +84,36 @@ tactic expr_to_tactic(type_checker & tc, expr e, pos_info_provider const * p) { // unfold definition buffer locals; get_app_rev_args(e, locals); - v = instantiate_univ_params(v, it->get_univ_params(), const_levels(f)); + level_param_names const & ps = it->get_univ_params(); + levels ls = const_levels(f); + unsigned num_ps = length(ps); + unsigned num_ls = length(ls); + if (num_ls > num_ps) + throw expr_to_tactic_exception(e, sstream() << "invalid number of universes"); + if (num_ls < num_ps) { + buffer extra_ls; + name_generator ngen = tc.mk_ngen(); + for (unsigned i = num_ls; i < num_ps; i++) + extra_ls.push_back(mk_meta_univ(ngen.next())); + ls = append(ls, to_list(extra_ls.begin(), extra_ls.end())); + } + v = instantiate_univ_params(v, ps, ls); v = apply_beta(v, locals.size(), locals.data()); return expr_to_tactic(tc, v, p); } } +static name g_tmp_prefix = name::mk_internal_unique_name(); +MK_THREAD_LOCAL_GET(unsigned, get_expr_tac_id, 0) +static name_generator next_name_generator() { + unsigned & c = get_expr_tac_id(); + unsigned r = c; + c++; + return name_generator(name(g_tmp_prefix, r)); +} + tactic expr_to_tactic(environment const & env, expr const & e, pos_info_provider const * p) { - type_checker tc(env); + type_checker tc(env, next_name_generator()); return expr_to_tactic(tc, e, p); } diff --git a/tests/lean/run/tactic24.lean b/tests/lean/run/tactic24.lean new file mode 100644 index 000000000..f9772bc2d --- /dev/null +++ b/tests/lean/run/tactic24.lean @@ -0,0 +1,23 @@ +import standard +using tactic + +definition my_tac1 := apply @refl +definition my_tac2 := repeat (apply @and_intro; assumption) + +tactic_hint my_tac1 +tactic_hint my_tac2 + +theorem T1 {A : Type.{2}} (a : A) : a = a +:= _ + +theorem T2 {a b c : Bool} (Ha : a) (Hb : b) (Hc : c) : a ∧ b ∧ c +:= _ + +definition my_tac3 := fixpoint (λ f, [apply @or_intro_left; f | + apply @or_intro_right; f | + assumption]) + +tactic_hint [or] my_tac3 + +theorem T3 {a b c : Bool} (Hb : b) : a ∨ b ∨ c +:= _