From c9cee9a70277786c84e55df013d1fde7135cdc85 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 6 Sep 2016 15:09:54 -0700 Subject: [PATCH] feat(library/equations_compiler): add flag indicating whether we are compiling a lemma or not --- src/frontends/lean/decl_util.cpp | 14 +++++++++----- src/frontends/lean/decl_util.h | 2 +- src/library/equations_compiler/elim_match.cpp | 6 +++--- src/library/equations_compiler/equations.cpp | 5 +++-- src/library/equations_compiler/equations.h | 11 ++++++----- src/library/equations_compiler/structural_rec.cpp | 2 +- 6 files changed, 23 insertions(+), 17 deletions(-) diff --git a/src/frontends/lean/decl_util.cpp b/src/frontends/lean/decl_util.cpp index 078ee46785..0fa51a45d4 100644 --- a/src/frontends/lean/decl_util.cpp +++ b/src/frontends/lean/decl_util.cpp @@ -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 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; } diff --git a/src/frontends/lean/decl_util.h b/src/frontends/lean/decl_util.h index 87d716b490..5738cf0a15 100644 --- a/src/frontends/lean/decl_util.h +++ b/src/frontends/lean/decl_util.h @@ -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(); }; diff --git a/src/library/equations_compiler/elim_match.cpp b/src/library/equations_compiler/elim_match.cpp index e5e03a81c1..10a6254c99 100644 --- a/src/library/equations_compiler/elim_match.cpp +++ b/src/library/equations_compiler/elim_match.cpp @@ -54,7 +54,7 @@ struct elim_match_fn { expr m_ref; unsigned m_depth{0}; buffer 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); diff --git a/src/library/equations_compiler/equations.cpp b/src/library/equations_compiler/equations.cpp index aab2f7e2df..9d5eac0e88 100644 --- a/src/library/equations_compiler/equations.cpp +++ b/src/library/equations_compiler/equations.cpp @@ -50,7 +50,8 @@ public: virtual expr check_type(expr const &, abstract_type_context &, bool) const { throw_eqs_ex(); } virtual optional 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(d); if (num == 0 || h.m_num_fns == 0) throw corrupted_stream_exception(); diff --git a/src/library/equations_compiler/equations.h b/src/library/equations_compiler/equations.h index b05ecd8833..2953bbb1c7 100644 --- a/src/library/equations_compiler/equations.h +++ b/src/library/equations_compiler/equations.h @@ -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 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 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) {} }; diff --git a/src/library/equations_compiler/structural_rec.cpp b/src/library/equations_compiler/structural_rec.cpp index 59384f25fc..58d5e4b842 100644 --- a/src/library/equations_compiler/structural_rec.cpp +++ b/src/library/equations_compiler/structural_rec.cpp @@ -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); }