From 90ece4dd1b491427bad98f8ea9788ffa503befcd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 7 Oct 2014 09:44:01 -0700 Subject: [PATCH] feat(frontends/lean): remove tactic hints for specific classes The idea is to separate class-instance resolution and tactic framework as two independent engines. --- src/frontends/lean/class.cpp | 3 +- src/frontends/lean/placeholder_elaborator.cpp | 63 +++---------------- src/frontends/lean/tactic_hint.cpp | 28 ++------- src/frontends/lean/tactic_hint.h | 6 +- tests/lean/run/tactic24.lean | 2 +- tests/lean/run/tactic25.lean | 2 +- tests/lean/run/tactic26.lean | 2 +- tests/lean/run/tactic28.lean | 2 +- 8 files changed, 19 insertions(+), 89 deletions(-) diff --git a/src/frontends/lean/class.cpp b/src/frontends/lean/class.cpp index f8b30b3faf..306cd50e22 100644 --- a/src/frontends/lean/class.cpp +++ b/src/frontends/lean/class.cpp @@ -14,7 +14,6 @@ Author: Leonardo de Moura #include "library/num.h" #include "frontends/lean/parser.h" #include "frontends/lean/util.h" -#include "frontends/lean/tactic_hint.h" #include "frontends/lean/tokens.h" #ifndef LEAN_INSTANCE_DEFAULT_PRIORITY @@ -229,7 +228,7 @@ void register_class_cmds(cmd_table & r) { /** \brief If the constant \c e is a class, return its name */ optional constant_is_ext_class(environment const & env, expr const & e) { name const & cls_name = const_name(e); - if (is_class(env, cls_name) || !empty(get_tactic_hints(env, cls_name))) { + if (is_class(env, cls_name)) { return optional(cls_name); } else { return optional(); diff --git a/src/frontends/lean/placeholder_elaborator.cpp b/src/frontends/lean/placeholder_elaborator.cpp index 431927c304..7aad2c9c94 100644 --- a/src/frontends/lean/placeholder_elaborator.cpp +++ b/src/frontends/lean/placeholder_elaborator.cpp @@ -15,7 +15,6 @@ Author: Leonardo de Moura #include "library/error_handling/error_handling.h" #include "frontends/lean/util.h" #include "frontends/lean/class.h" -#include "frontends/lean/tactic_hint.h" #include "frontends/lean/local_context.h" #include "frontends/lean/choice_iterator.h" @@ -55,15 +54,7 @@ pair mk_placeholder_elaborator(std::shared_ptr m_C; @@ -77,22 +68,14 @@ struct placeholder_elaborator : public choice_iterator { // global declaration names that are class instances. // This information is retrieved using #get_class_instances. list m_instances; - // Tactic hints for the class - list m_tactics; - // result produce by last executed tactic. - proof_state_seq m_tactic_result; justification m_jst; placeholder_elaborator(std::shared_ptr const & C, expr const & meta, expr const & meta_type, list const & local_insts, list const & instances, - list const & tacs, justification const & j): - choice_iterator(), m_C(C), - m_meta(meta), m_meta_type(meta_type), - m_local_instances(local_insts), m_instances(instances), - m_tactics(tacs), - m_jst(j) { + choice_iterator(), m_C(C), m_meta(meta), m_meta_type(meta_type), + m_local_instances(local_insts), m_instances(instances), m_jst(j) { } constraints mk_constraints(constraint const & c, buffer const & cs) { @@ -157,21 +140,6 @@ struct placeholder_elaborator : public choice_iterator { } } - optional get_next_tactic_result() { - while (auto next = m_tactic_result.pull()) { - m_tactic_result = next->second; - if (!empty(next->first.get_goals())) - continue; // has unsolved goals - substitution subst = next->first.get_subst(); - expr const & mvar = get_app_fn(m_meta); - bool relax = m_C->m_relax; - constraints cs = metavar_closure(m_meta_type).mk_constraints(subst, m_jst, relax); - constraint c = mk_eq_cnstr(mvar, subst.instantiate(mvar), m_jst, relax); - return some(cons(c, cs)); - } - return optional(); - } - virtual optional next() { while (!empty(m_local_instances)) { expr inst = head(m_local_instances); @@ -187,18 +155,6 @@ struct placeholder_elaborator : public choice_iterator { if (auto cs = try_instance(inst)) return cs; } - if (auto cs = get_next_tactic_result()) - return cs; - while (!empty(m_tactics)) { - tactic const & tac = head(m_tactics).get_tactic(); - m_tactics = tail(m_tactics); - proof_state ps(goals(goal(m_meta, m_meta_type)), substitution(), m_C->m_ngen.mk_child()); - try { - m_tactic_result = tac(m_C->env(), m_C->ios(), ps); - if (auto cs = get_next_tactic_result()) - return cs; - } catch (exception &) {} - } return optional(); } }; @@ -207,9 +163,7 @@ struct placeholder_elaborator : public choice_iterator { constraint mk_placeholder_cnstr(std::shared_ptr const & C, expr const & m) { environment const & env = C->env(); justification j = mk_failed_to_synthesize_jst(env, m); - auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & s, - name_generator const & /* ngen */) { - expr const & mvar = get_app_fn(meta); + auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const &, name_generator const &) { if (auto cls_name_it = is_ext_class(C->tc(), meta_type)) { name cls_name = *cls_name_it; list const & ctx = C->m_ctx.get_data(); @@ -217,13 +171,10 @@ constraint mk_placeholder_cnstr(std::shared_ptr const & C, if (C->use_local_instances()) local_insts = get_local_instances(C->tc(), ctx, cls_name); list insts = get_class_instances(env, cls_name); - list tacs; - if (!s.is_assigned(mvar)) - tacs = get_tactic_hints(env, cls_name); - if (empty(local_insts) && empty(insts) && empty(tacs)) + if (empty(local_insts) && empty(insts)) return lazy_list(); // nothing to be done // we are always strict with placeholders associated with classes - return choose(std::make_shared(C, meta, meta_type, local_insts, insts, tacs, j)); + return choose(std::make_shared(C, meta, meta_type, local_insts, insts, j)); } else { // do nothing, type is not a class... return lazy_list(constraints()); @@ -313,7 +264,7 @@ constraint mk_placeholder_root_cnstr(std::shared_ptr const } /** \brief Create a metavariable, and attach choice constraint for generating - solutions using class-instances and tactic-hints. + solutions using class-instances */ pair mk_placeholder_elaborator( environment const & env, io_state const & ios, local_context const & ctx, diff --git a/src/frontends/lean/tactic_hint.cpp b/src/frontends/lean/tactic_hint.cpp index b424347946..61d78be066 100644 --- a/src/frontends/lean/tactic_hint.cpp +++ b/src/frontends/lean/tactic_hint.cpp @@ -21,8 +21,6 @@ namespace lean { typedef list tactic_hint_entries; struct tactic_hint_state { - typedef name_map class_tactics; - class_tactics m_class_tactics; tactic_hint_entries m_tactics; }; @@ -39,12 +37,7 @@ struct tactic_hint_config { } 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)); + s.m_tactics = add(s.m_tactics, e); } static void add_entry(environment const & env, io_state const &, state & s, entry const & e) { @@ -67,16 +60,16 @@ struct tactic_hint_config { } static void write_entry(serializer & s, entry const & e) { - s << e.m_class << e.m_pre_tactic; + s << e.m_pre_tactic; } static entry read_entry(deserializer & d) { entry e; - d >> e.m_class >> e.m_pre_tactic; + d >> e.m_pre_tactic; return e; } static optional get_fingerprint(entry const & e) { - return some(hash(e.m_class.hash(), e.m_pre_tactic.hash())); + return some(e.m_pre_tactic.hash()); } }; @@ -95,11 +88,6 @@ void finalize_tactic_hint() { delete g_class_name; } -list get_tactic_hints(environment const & env, name const & c) { - tactic_hint_state const & s = tactic_hint_ext::get_state(env); - return ptr_to_list(s.m_class_tactics.find(c)); -} - list get_tactic_hints(environment const & env) { tactic_hint_state const & s = tactic_hint_ext::get_state(env); return s.m_tactics; @@ -119,15 +107,9 @@ expr parse_tactic_name(parser & p) { } environment tactic_hint_cmd(parser & p) { - name cls; - if (p.curr_is_token(get_lbracket_tk())) { - p.next(); - cls = get_class_name(p.env(), p.parse_expr()); - p.check_token_next(get_rbracket_tk(), "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)); + return tactic_hint_ext::add_entry(p.env(), get_dummy_ios(), tactic_hint_entry(pre_tac, tac)); } void register_tactic_hint_cmd(cmd_table & r) { diff --git a/src/frontends/lean/tactic_hint.h b/src/frontends/lean/tactic_hint.h index c380ea72c2..c236f22e41 100644 --- a/src/frontends/lean/tactic_hint.h +++ b/src/frontends/lean/tactic_hint.h @@ -11,18 +11,16 @@ Author: Leonardo de Moura namespace lean { class tactic_hint_entry { friend struct 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) {} + tactic_hint_entry(expr const & pre_tac, tactic const & tac): + 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); diff --git a/tests/lean/run/tactic24.lean b/tests/lean/run/tactic24.lean index a56c8abf76..9326510649 100644 --- a/tests/lean/run/tactic24.lean +++ b/tests/lean/run/tactic24.lean @@ -17,7 +17,7 @@ definition my_tac3 := fixpoint (λ f, [apply @or.intro_left; f | apply @or.intro_right; f | assumption]) -tactic_hint [or] my_tac3 +tactic_hint my_tac3 theorem T3 {a b c : Prop} (Hb : b) : a ∨ b ∨ c := _ diff --git a/tests/lean/run/tactic25.lean b/tests/lean/run/tactic25.lean index 2d5014dbae..2d06a5ac78 100644 --- a/tests/lean/run/tactic25.lean +++ b/tests/lean/run/tactic25.lean @@ -15,5 +15,5 @@ definition my_tac3 := fixpoint (λ f, [apply @or.intro_left; f | apply @or.intro_right; f | assumption]) -tactic_hint [or] my_tac3 +tactic_hint my_tac3 theorem T3 {a b c : Prop} (Hb : b) : a ∨ b ∨ c diff --git a/tests/lean/run/tactic26.lean b/tests/lean/run/tactic26.lean index c2b5771470..ca254f9d61 100644 --- a/tests/lean/run/tactic26.lean +++ b/tests/lean/run/tactic26.lean @@ -17,7 +17,7 @@ definition my_tac := fixpoint (λ t, [ apply @inl_inhabited; t | apply @num.is_inhabited ]) -tactic_hint [inhabited] my_tac +tactic_hint my_tac theorem T : inhabited (sum false num) diff --git a/tests/lean/run/tactic28.lean b/tests/lean/run/tactic28.lean index d2a665d6a0..669722659a 100644 --- a/tests/lean/run/tactic28.lean +++ b/tests/lean/run/tactic28.lean @@ -20,7 +20,7 @@ definition my_tac := repeat (trace "iteration"; state; .. apply @num.is_inhabited; trace "used num")) ; now -tactic_hint [inhabited] my_tac +tactic_hint my_tac theorem T : inhabited (sum false num)