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

feat(frontends/lean/parser): apply type inference elaborator to fill remaining metavariables/holes (these are holes produced by tactics such as apply_tac)

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-07 13:09:39 -08:00
parent bc3a6a3185
commit 33b72f1dd0
5 changed files with 91 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -33,6 +33,7 @@ Author: Leonardo de Moura
#include "kernel/printer.h"
#include "kernel/metavar.h"
#include "kernel/for_each_fn.h"
#include "kernel/type_checker_justification.h"
#include "library/expr_lt.h"
#include "library/type_inferer.h"
#include "library/arith/arith.h"
@ -43,6 +44,7 @@ Author: Leonardo de Moura
#include "library/tactic/proof_state.h"
#include "library/tactic/tactic.h"
#include "library/tactic/apply_tactic.h"
#include "library/elaborator/elaborator.h"
#include "frontends/lean/frontend.h"
#include "frontends/lean/frontend_elaborator.h"
#include "frontends/lean/parser.h"
@ -1338,12 +1340,27 @@ class parser::imp {
It basically applies the proof_builder if \c s does not contain
any goals left. The position information is used to throw an exception
if \c s is not a final state.
The resultant proof must have type \c expected_type in the context \c ctx.
*/
expr mk_proof_for(proof_state const & s, pos_info const & p) {
expr mk_proof_for(proof_state const & s, pos_info const & p, context const & ctx, expr const & expected_type) {
if (s.is_proof_final_state()) {
assignment a(s.get_menv());
proof_map m;
expr pr = s.get_proof_builder()(m, a);
if (has_metavar(pr)) {
// Some tactics generate metavariables that can only be instantiated by type inference elaboration.
// Example: apply_tactic.
metavar_env menv = s.get_menv();
buffer<unification_constraint> ucs;
expr pr_type = type_checker(m_frontend).infer_type(pr, ctx, &menv, &ucs);
ucs.push_back(mk_convertible_constraint(ctx, pr_type, expected_type, mk_type_match_justification(ctx, expected_type, pr)));
elaborator elb(m_frontend, s.get_menv(), ucs.size(), ucs.data(), m_frontend.get_options());
metavar_env new_menv = elb.next();
pr = instantiate_metavars(pr, new_menv);
if (has_metavar(pr))
throw exception("synthesized proof object has unsolved metavars");
}
return pr;
} else {
throw tactic_cmd_error("invalid 'done' command, proof cannot be produced from this state", p, s);
@ -1410,16 +1427,18 @@ class parser::imp {
\brief Execute the \c done tactic command. It succeeds if
a proof for \c s can be built.
*/
expr done_cmd(proof_state const & s) {
expr done_cmd(proof_state const & s, context const & ctx, expr const & expected_type) {
auto p = pos();
next();
return mk_proof_for(s, p);
return mk_proof_for(s, p, ctx, expected_type);
}
/**
\brief Parse tactic command sequence for solving input state \c s.
The proof for \c s must have type \c expected_type in the context \c ctx.
*/
expr parse_tactic_cmds(proof_state s) {
expr parse_tactic_cmds(proof_state s, context const & ctx, expr const & expected_type) {
proof_state_seq_stack stack;
expr pr;
enum class status { Continue, Done, Eof, Abort };
@ -1446,7 +1465,7 @@ class parser::imp {
} else if (id == g_back) {
back_cmd(stack, s);
} else if (id == g_done) {
pr = done_cmd(s);
pr = done_cmd(s, ctx, expected_type);
if (pr)
st = status::Done;
} else if (id == g_abort) {
@ -1519,12 +1538,12 @@ class parser::imp {
if (hint_and_pos.first) {
// metavariable has an associated tactic hint
s = apply_tactic(s, hint_and_pos.first, hint_and_pos.second).first;
return mk_proof_for(s, hint_and_pos.second);
return mk_proof_for(s, hint_and_pos.second, context(), expected_type);
} else {
display_proof_state_if_interactive(s);
show_tactic_prompt();
check_period_next("invalid theorem, '.' expected before tactical proof");
return parse_tactic_cmds(s);
return parse_tactic_cmds(s, context(), expected_type);
}
} else {
buffer<expr> mvars;
@ -1553,14 +1572,14 @@ class parser::imp {
if (hint_and_pos.first) {
// metavariable has an associated tactic hint
s = apply_tactic(s, hint_and_pos.first, hint_and_pos.second).first;
menv.assign(mvar, mk_proof_for(s, hint_and_pos.second));
menv.assign(mvar, mk_proof_for(s, hint_and_pos.second, mvar_ctx, mvar_type));
} else {
if (curr_is_period()) {
display_proof_state_if_interactive(s);
show_tactic_prompt();
next();
}
expr mvar_val = parse_tactic_cmds(s);
expr mvar_val = parse_tactic_cmds(s, mvar_ctx, mvar_type);
if (mvar_val)
menv.assign(mvar, mvar_val);
}

14
src/kernel/type_checker_justification.cpp
View file

@ -91,4 +91,18 @@ void def_type_match_justification_cell::get_children(buffer<justification_cell*>
expr const & def_type_match_justification_cell::get_main_expr() const {
return m_value;
}
type_match_justification_cell::~type_match_justification_cell() {
}
format type_match_justification_cell::pp_header(formatter const &, options const &) const {
return format("Type of expression must be convertible to expected type.");
}
void type_match_justification_cell::get_children(buffer<justification_cell*> &) const {
}
expr const & type_match_justification_cell::get_main_expr() const {
return m_value;
}
}

20
src/kernel/type_checker_justification.h
View file

@ -120,9 +120,29 @@ public:
expr const & get_value() const { return m_value; }
};
/**
\brief Similar to def_type_match_justification_cell. It is used to sign that type of \c m_value
must be convertible to \c m_type at context \c m_ctx.
*/
class type_match_justification_cell : public justification_cell {
context m_ctx;
expr m_type;
expr m_value;
public:
type_match_justification_cell(context const & c, expr const & t, expr const & v):m_ctx(c), m_type(t), m_value(v) {}
virtual ~type_match_justification_cell();
virtual format pp_header(formatter const & fmt, options const & opts) const;
virtual void get_children(buffer<justification_cell*> &) const;
virtual expr const & get_main_expr() const;
context const & get_context() const { return m_ctx; }
expr const & get_type() const { return m_type; }
expr const & get_value() const { return m_value; }
};
inline justification mk_function_expected_justification(context const & ctx, expr const & app) { return justification(new function_expected_justification_cell(ctx, app)); }
inline justification mk_app_type_match_justification(context const & ctx, expr const & app, unsigned i) { return justification(new app_type_match_justification_cell(ctx, app, i)); }
inline justification mk_type_expected_justification(context const & ctx, expr const & type) { return justification(new type_expected_justification_cell(ctx, type)); }
inline justification mk_max_type_justification(context const & ctx, expr const & type) { return justification(new max_type_justification_cell(ctx, type)); }
inline justification mk_def_type_match_justification(context const & ctx, name const & n, expr const & v) { return justification(new def_type_match_justification_cell(ctx, n, v)); }
inline justification mk_type_match_justification(context const & ctx, expr const & t, expr const & v) { return justification(new type_match_justification_cell(ctx, t, v)); }
}

20
tests/lean/tactic13.lean Normal file
View file

@ -0,0 +1,20 @@
Variable f : Int -> Int -> Int
(**
refl_tac = apply_tac("Refl")
congr_tac = apply_tac("Congr")
symm_tac = apply_tac("Symm")
trans_tac = apply_tac("Trans")
unfold_homo_eq_tac = unfold_tac("eq")
auto = unfold_homo_eq_tac .. REPEAT(ORELSE(refl_tac, congr_tac, assumption_tac, THEN(symm_tac, assumption_tac, now_tac)))
**)
Theorem T1 (a b c : Int) (H1 : a = b) (H2 : a = c) : (f (f a a) b) = (f (f b c) a).
apply auto.
done.
Theorem T2 (a b c : Int) (H1 : a = b) (H2 : a = c) : (f (f a c)) = (f (f b a)).
apply auto.
done.
Show Environment 2.

9
tests/lean/tactic13.lean.expected.out Normal file
View file

@ -0,0 +1,9 @@
Set: pp::colors
Set: pp::unicode
Assumed: f
Proved: T1
Proved: T2
Theorem T1 (a b c : ℤ) (H1 : a = b) (H2 : a = c) : (f (f a a) b) = (f (f b c) a) :=
Congr (Congr (Refl f) (Congr (Congr (Refl f) H1) H2)) (Symm H1)
Theorem T2 (a b c : ℤ) (H1 : a = b) (H2 : a = c) : (f (f a c)) = (f (f b a)) :=
Congr (Refl f) (Congr (Congr (Refl f) H1) (Symm H2))