max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/equations_compiler): add flag indicating whether we are compiling a lemma or not

Browse source
This commit is contained in:
Leonardo de Moura 2016-09-06 15:09:54 -07:00
parent 385a28a410
commit c9cee9a702
6 changed files with 23 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/frontends/lean/decl_util.cpp
View file

@ -268,24 +268,27 @@ struct definition_info {
name m_prefix;
bool m_is_private{false};
bool m_is_meta{false};
bool m_lemmas{false};
bool m_is_lemma{false};
bool m_aux_lemmas{false};
unsigned m_next_match_idx{1};
};
MK_THREAD_LOCAL_GET_DEF(definition_info, get_definition_info);
declaration_info_scope::declaration_info_scope(environment const & env, bool is_private, bool is_meta, bool lemmas) {
declaration_info_scope::declaration_info_scope(environment const & env, bool is_private, bool is_meta,
bool is_lemma, bool aux_lemmas) {
definition_info & info = get_definition_info();
lean_assert(info.m_prefix.is_anonymous());
info.m_prefix = is_private ? name() : get_namespace(env);
info.m_is_private = is_private;
info.m_is_meta = is_meta;
info.m_lemmas = lemmas;
info.m_is_lemma = is_lemma;
info.m_aux_lemmas = aux_lemmas;
info.m_next_match_idx = 1;
}
declaration_info_scope::declaration_info_scope(environment const & env, bool is_private, def_cmd_kind k):
declaration_info_scope(env, is_private, k == MetaDefinition, k == Definition) {}
declaration_info_scope(env, is_private, k == MetaDefinition, k == Theorem, k == Definition) {}
declaration_info_scope::~declaration_info_scope() {
definition_info & info = get_definition_info();
@ -298,7 +301,8 @@ equations_header mk_equations_header(list<name> const & ns) {
h.m_fn_names = ns;
h.m_is_private = get_definition_info().m_is_private;
h.m_is_meta = get_definition_info().m_is_meta;
h.m_lemmas = get_definition_info().m_lemmas;
h.m_is_lemma = get_definition_info().m_is_lemma;
h.m_aux_lemmas = get_definition_info().m_aux_lemmas;
return h;
}

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

@ -77,7 +77,7 @@ environment add_local_ref(parser & p, environment const & env, name const & c_na
nested definitions. */
class declaration_info_scope {
public:
declaration_info_scope(environment const & env, bool is_private, bool is_meta, bool lemmas);
declaration_info_scope(environment const & env, bool is_private, bool is_meta, bool is_lemma, bool aux_lemmas);
declaration_info_scope(environment const & env, bool is_private, def_cmd_kind k);
~declaration_info_scope();
};

6
src/library/equations_compiler/elim_match.cpp
View file

@ -54,7 +54,7 @@ struct elim_match_fn {
expr m_ref;
unsigned m_depth{0};
buffer<bool> m_used_eqns;
bool m_lemmas;
bool m_aux_lemmas;
bool m_use_ite;
/* m_enum is a mapping from inductive type name to flag indicating whether it is
an enumeration type or not. */
@ -895,7 +895,7 @@ struct elim_match_fn {
m_used_eqns[eqn.m_eqn_idx] = true;
expr rhs = apply(eqn.m_rhs, eqn.m_subst);
m_mctx.assign(P.m_goal, rhs);
if (m_lemmas) {
if (m_aux_lemmas) {
lemma L;
L.m_lctx = eqn.m_lctx;
L.m_vars = eqn.m_vars;
@ -963,7 +963,7 @@ struct elim_match_fn {
type_context ctx = mk_type_context(lctx);
lean_assert(!is_recursive_eqns(ctx, eqns));
});
m_lemmas = get_equations_header(eqns).m_lemmas;
m_aux_lemmas = get_equations_header(eqns).m_aux_lemmas;
m_ref = eqns;
problem P; expr fn;
std::tie(P, fn) = mk_problem(lctx, eqns);

5
src/library/equations_compiler/equations.cpp
View file

@ -50,7 +50,8 @@ public:
virtual expr check_type(expr const &, abstract_type_context &, bool) const { throw_eqs_ex(); }
virtual optional<expr> expand(expr const &, abstract_type_context &) const { throw_eqs_ex(); }
virtual void write(serializer & s) const {
s << *g_equations_opcode << m_header.m_num_fns << m_header.m_is_private << m_header.m_is_meta << m_header.m_lemmas;
s << *g_equations_opcode << m_header.m_num_fns << m_header.m_is_private << m_header.m_is_meta
<< m_header.m_is_lemma << m_header.m_aux_lemmas;
write_list(s, m_header.m_fn_names);
}
equations_header const & get_header() const { return m_header; }
@ -228,7 +229,7 @@ void initialize_equations() {
register_macro_deserializer(*g_equations_opcode,
[](deserializer & d, unsigned num, expr const * args) {
equations_header h;
d >> h.m_num_fns >> h.m_is_private >> h.m_is_meta >> h.m_lemmas;
d >> h.m_num_fns >> h.m_is_private >> h.m_is_meta >> h.m_is_lemma >> h.m_aux_lemmas;
h.m_fn_names = read_list<name>(d);
if (num == 0 || h.m_num_fns == 0)
throw corrupted_stream_exception();

11
src/library/equations_compiler/equations.h
View file

@ -28,11 +28,12 @@ expr mk_inaccessible(expr const & e);
bool is_inaccessible(expr const & e);
struct equations_header {
unsigned m_num_fns{0}; /* number of functions being defined */
list<name> m_fn_names; /* names for functions */
bool m_is_private{false}; /* if true, it must be a private definition */
bool m_is_meta{false}; /* the auxiliary declarations should be tagged as meta */
bool m_lemmas{false}; /* if true, we must create equation lemmas and induction principle */
unsigned m_num_fns{0}; /* number of functions being defined */
list<name> m_fn_names; /* names for functions */
bool m_is_private{false}; /* if true, it must be a private definition */
bool m_is_lemma{false}; /* if true, equations are defining a lemma */
bool m_is_meta{false}; /* the auxiliary declarations should be tagged as meta */
bool m_aux_lemmas{false}; /* if true, we must create equation lemmas and induction principle */
equations_header() {}
equations_header(unsigned num_fns):m_num_fns(num_fns) {}
};

2
src/library/equations_compiler/structural_rec.cpp
View file

@ -846,7 +846,7 @@ struct structural_rec_fn {
if (!new_eqns) return none_expr();
elim_match_result R = elim_match(m_env, m_opts, m_mctx, m_lctx, *new_eqns);
expr fn = mk_function(R.m_fn);
if (m_header.m_lemmas) {
if (m_header.m_aux_lemmas) {
lean_assert(!m_header.m_is_meta);
mk_lemmas(fn, R.m_lemmas);
}