michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean): remove tactic hints for specific classes

Browse source 
The idea is to separate class-instance resolution and tactic framework
as two independent engines.
This commit is contained in:
Leonardo de Moura 2014-10-07 09:44:01 -07:00
parent dc0e6861b7
commit 90ece4dd1b
8 changed files with 19 additions and 89 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/frontends/lean/class.cpp
View file

@ -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<name> 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<name>(cls_name);
} else {
return optional<name>();

63
src/frontends/lean/placeholder_elaborator.cpp
View file

@ -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<expr, constraint> mk_placeholder_elaborator(std::shared_ptr<placeholder_con
In this case, \c fn will do the following:
1) if the elaborated type of ?m is a 'class' C, then the stream will start with
a) all local instances of class C (if elaborator.local_instances == true)
b) solutions produced by tactic_hints for class C
2) if the elaborated type of ?m is not a class, then the stream will only contain
the solutions produced by tactic_hints.
The unifier only process delayed choice constraints when there are no other kind
of constraint to be processed.
This is a helper class for implementing this choice function.
b) all global instances of class C
*/
struct placeholder_elaborator : public choice_iterator {
std::shared_ptr<placeholder_context> 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<name> m_instances;
// Tactic hints for the class
list<tactic_hint_entry> m_tactics;
// result produce by last executed tactic.
proof_state_seq m_tactic_result;
justification m_jst;
placeholder_elaborator(std::shared_ptr<placeholder_context> const & C,
expr const & meta, expr const & meta_type,
list<expr> const & local_insts, list<name> const & instances,
list<tactic_hint_entry> 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<constraint> const & cs) {
@ -157,21 +140,6 @@ struct placeholder_elaborator : public choice_iterator {
}
}
optional<constraints> 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<constraints>();
}
virtual optional<constraints> 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<constraints>();
}
};
@ -207,9 +163,7 @@ struct placeholder_elaborator : public choice_iterator {
constraint mk_placeholder_cnstr(std::shared_ptr<placeholder_context> 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<expr> const & ctx = C->m_ctx.get_data();
@ -217,13 +171,10 @@ constraint mk_placeholder_cnstr(std::shared_ptr<placeholder_context> const & C,
if (C->use_local_instances())
local_insts = get_local_instances(C->tc(), ctx, cls_name);
list<name> insts = get_class_instances(env, cls_name);
list<tactic_hint_entry> 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<constraints>(); // nothing to be done
// we are always strict with placeholders associated with classes
return choose(std::make_shared<placeholder_elaborator>(C, meta, meta_type, local_insts, insts, tacs, j));
return choose(std::make_shared<placeholder_elaborator>(C, meta, meta_type, local_insts, insts, j));
} else {
// do nothing, type is not a class...
return lazy_list<constraints>(constraints());
@ -313,7 +264,7 @@ constraint mk_placeholder_root_cnstr(std::shared_ptr<placeholder_context> const
}
/** \brief Create a metavariable, and attach choice constraint for generating
solutions using class-instances and tactic-hints.
solutions using class-instances
*/
pair<expr, constraint> mk_placeholder_elaborator(
environment const & env, io_state const & ios, local_context const & ctx,

28
src/frontends/lean/tactic_hint.cpp
View file

@ -21,8 +21,6 @@ namespace lean {
typedef list<tactic_hint_entry> tactic_hint_entries;
struct tactic_hint_state {
typedef name_map<tactic_hint_entries> 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<unsigned> 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<tactic_hint_entry> 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<tactic_hint_entry> 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) {

6
src/frontends/lean/tactic_hint.h
View file

@ -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<tactic_hint_entry> get_tactic_hints(environment const & env, name const & cls_name);
list<tactic_hint_entry> get_tactic_hints(environment const & env);
class parser;
expr parse_tactic_name(parser & p);

2
tests/lean/run/tactic24.lean
View file

@ -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
:= _

2
tests/lean/run/tactic25.lean
View file

@ -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

2
tests/lean/run/tactic26.lean
View file

@ -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)

2
tests/lean/run/tactic28.lean
View file

@ -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)