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

feat(frontends/lean): add tactic_hint command

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-08 14:28:33 -07:00
parent 33cb2db5b5
commit a3be63af73
16 changed files with 297 additions and 51 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/standard/tactic.lean
View file

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

2
src/emacs/lean-mode.el
View file

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

2
src/frontends/lean/CMakeLists.txt
View file

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

2
src/frontends/lean/builtin_cmds.cpp
View file

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

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

@ -57,17 +57,22 @@ struct class_config {
template class scoped_ext<class_config>;
typedef scoped_ext<class_config> 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));
}

2
src/frontends/lean/class.h
View file

@ -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<name> 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);
}

90
src/frontends/lean/elaborator.cpp
View file

@ -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<expr> context;
typedef std::vector<constraint> constraint_vect;
typedef name_map<expr> tactic_hints;
typedef name_map<expr> local_tactic_hints;
typedef name_map<expr> mvar2meta;
typedef std::unique_ptr<type_checker> type_checker_ptr;
@ -136,7 +137,7 @@ 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.
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.
@ -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<expr> 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<tactic> 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<tactic>();
}
}
/** \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<tactic_hint_entry> 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<expr> pre_tac = get_pre_tactic_for(subst, mvar, visited);
if (!pre_tac)
return;
optional<tactic> 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");
if (auto local_hint = get_local_tactic_hint(subst, mvar, visited)) {
try_using(subst, mvar, ps, *local_hint, true);
} else {
subst = r->first.get_subst();
expr v = subst.instantiate(mvar);
subst = subst.assign(mlocal_name(mvar), v);
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));
}
}

8
src/frontends/lean/parser.cpp
View file

@ -469,22 +469,22 @@ expr parser::mk_Type() {
}
std::tuple<expr, level_param_names> 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<expr, level_param_names> 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<expr, level_param_names> 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<expr, expr, level_param_names> 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);
}

4
src/frontends/lean/parser.h
View file

@ -257,9 +257,13 @@ public:
std::tuple<expr, level_param_names> elaborate_type(expr const & e);
/** \brief Elaborate \c e in the given environment. */
std::tuple<expr, level_param_names> elaborate_at(environment const & env, expr const & e);
/** \brief Elaborate \c e (making sure the result does not have metavariables). */
std::tuple<expr, level_param_names> elaborate(expr const & e) { return elaborate_at(m_env, e); }
/** \brief Elaborate the definition n : t := v */
std::tuple<expr, expr, level_param_names> 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(); }
};

7
src/frontends/lean/proof_qed_ext.cpp
View file

@ -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<expr> 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));
}

124
src/frontends/lean/tactic_hint.cpp Normal file
View file

@ -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 <string>
#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_entry> tactic_hint_entries;
struct tactic_hint_state {
typedef rb_map<name, tactic_hint_entries, name_quick_cmp> 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<tactic_hint_config>;
typedef scoped_ext<tactic_hint_config> tactic_hint_ext;
list<tactic_hint_entry> 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<tactic_hint_entry>();
}
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;
}
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));
}
}

30
src/frontends/lean/tactic_hint.h Normal file
View file

@ -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<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);
void register_tactic_hint_cmd(cmd_table & r);
}

2
src/frontends/lean/token_table.cpp
View file

@ -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<char const *, char const *> aliases[] =

1
src/kernel/type_checker.h
View file

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

26
src/library/tactic/expr_to_tactic.cpp
View file

@ -84,14 +84,36 @@ tactic expr_to_tactic(type_checker & tc, expr e, pos_info_provider const * p) {
// unfold definition
buffer<expr> 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<level> 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);
}

23
tests/lean/run/tactic24.lean Normal file
View file

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