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

refactor(frontends/lean/proof_qed_elaborator): simplify

Browse source 
proof_qed_elaborator interface
This commit is contained in:
Leonardo de Moura 2014-09-25 08:38:02 -07:00
parent 18cfce60b9
commit a61b95a87e
3 changed files with 11 additions and 23 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -331,10 +331,10 @@ public:
expr visit_proof_qed(expr const & e, optional<expr> const & t, constraint_seq & cs) {
lean_assert(is_proof_qed_annotation(e));
pair<expr, constraint_seq> ecs = visit(get_annotation_arg(e));
pair<expr, constraint> mc = mk_proof_qed_elaborator(env(), m_full_context, ecs.first, t, ecs.second,
m_unifier_config, m_relax_main_opaque);
cs += mc.second;
return mc.first;
expr m = m_full_context.mk_meta(t, e.get_tag());
constraint c = mk_proof_qed_cnstr(env(), m, ecs.first, ecs.second, m_unifier_config, m_relax_main_opaque);
cs += c;
return m;
}
static bool is_implicit_pi(expr const & e) {

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

@ -8,9 +8,10 @@ Author: Leonardo de Moura
#include "library/reducible.h"
#include "library/metavar_closure.h"
#include "frontends/lean/util.h"
#include "frontends/lean/local_context.h"
namespace lean {
/** \brief Create a "choice" constraint that postpone the
solving the constraints <tt>(cs union (m =?= e))</tt>.
*/
constraint mk_proof_qed_cnstr(environment const & env, expr const & m, expr const & e,
constraint_seq const & cs, unifier_config const & cfg, bool relax) {
justification j = mk_failed_to_synthesize_jst(env, m);
@ -47,16 +48,4 @@ constraint mk_proof_qed_cnstr(environment const & env, expr const & m, expr cons
bool owner = false;
return mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::Epilogue), owner, j, relax);
}
/** \brief Create a metavariable m, and attach "choice" constraint that postpone the
solving the constraints <tt>(cs union m =?= e)</tt>.
*/
pair<expr, constraint> mk_proof_qed_elaborator(
environment const & env, local_context & ctx,
expr const & e, optional<expr> const & type, constraint_seq const & cs,
unifier_config const & cfg, bool relax) {
expr m = ctx.mk_meta(type, e.get_tag());
constraint c = mk_proof_qed_cnstr(env, m, e, cs, cfg, relax);
return mk_pair(m, c);
}
}

9
src/frontends/lean/proof_qed_elaborator.h
View file

@ -8,10 +8,9 @@ Author: Leonardo de Moura
#include "library/unifier.h"
namespace lean {
/** \brief Create a metavariable m, and attach "choice" constraint that postpone the
solving the constraints <tt>(cs union m =?= e)</tt>.
/** \brief Create a "choice" constraint that postpone the
solving the constraints <tt>(cs union (m =?= e))</tt>.
*/
pair<expr, constraint> mk_proof_qed_elaborator(environment const & env, local_context & ctx,
expr const & e, optional<expr> const & type, constraint_seq const & cs,
unifier_config const & cfg, bool relax);
constraint mk_proof_qed_cnstr(environment const & env, expr const & m, expr const & e,
constraint_seq const & cs, unifier_config const & cfg, bool relax);
}