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

feat(library/equations_compiler/equations): add m_is_partial to equation header

Browse source
This commit is contained in:
Leonardo de Moura 2019-03-26 16:18:43 -07:00
parent 1f11429f98
commit 9ddc778ac3
3 changed files with 11 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -404,6 +404,7 @@ struct definition_info {
Remark: a regular (i.e., safe) declaration provided by the user may contain a unsafe subexpression (e.g., tactic).
*/
bool m_is_unsafe{false}; // true iff current block
bool m_is_partial{false};
bool m_is_noncomputable{false};
bool m_is_lemma{false};
bool m_aux_lemmas{false};
@ -422,8 +423,9 @@ declaration_info_scope::declaration_info_scope(name const & ns, decl_cmd_kind ki
info.m_actual_prefix = ns;
}
info.m_is_private = modifiers.m_is_private;
info.m_is_unsafe_decl = modifiers.m_is_unsafe;
info.m_is_unsafe = modifiers.m_is_unsafe;
info.m_is_unsafe_decl = modifiers.m_is_unsafe;
info.m_is_unsafe = modifiers.m_is_unsafe;
info.m_is_partial = modifiers.m_is_partial;
info.m_is_noncomputable = modifiers.m_is_noncomputable;
info.m_is_lemma = kind == decl_cmd_kind::Theorem;
info.m_aux_lemmas = kind != decl_cmd_kind::Theorem && !modifiers.m_is_unsafe;
@ -452,6 +454,7 @@ equations_header mk_equations_header(names const & ns, names const & actual_ns)
h.m_fn_actual_names = actual_ns;
h.m_is_private = get_definition_info().m_is_private;
h.m_is_unsafe = get_definition_info().m_is_unsafe;
h.m_is_partial = get_definition_info().m_is_partial;
h.m_is_noncomputable = get_definition_info().m_is_noncomputable;
h.m_is_lemma = get_definition_info().m_is_lemma;
h.m_aux_lemmas = get_definition_info().m_aux_lemmas;

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

@ -41,6 +41,7 @@ bool operator==(equations_header const & h1, equations_header const & h2) {
h1.m_is_private == h2.m_is_private &&
h1.m_is_lemma == h2.m_is_lemma &&
h1.m_is_unsafe == h2.m_is_unsafe &&
h1.m_is_partial == h2.m_is_partial &&
h1.m_is_noncomputable == h2.m_is_noncomputable &&
h1.m_aux_lemmas == h2.m_aux_lemmas &&
h1.m_prev_errors == h2.m_prev_errors &&
@ -154,7 +155,8 @@ equations_header get_equations_header(expr const & e) {
h.m_num_fns = get_nat(m, name(*g_equations_name, "num_fns"))->get_small_value();
h.m_is_private = *get_bool(m, name(*g_equations_name, "is_private"));
h.m_is_lemma = *get_bool(m, name(*g_equations_name, "is_lemma"));
h.m_is_unsafe = *get_bool(m, name(*g_equations_name, "is_unsafe"));
h.m_is_unsafe = *get_bool(m, name(*g_equations_name, "is_unsafe"));
h.m_is_partial = *get_bool(m, name(*g_equations_name, "is_partial"));
h.m_is_noncomputable = *get_bool(m, name(*g_equations_name, "is_noncomputable"));
h.m_aux_lemmas = *get_bool(m, name(*g_equations_name, "aux_lemmas"));
h.m_prev_errors = *get_bool(m, name(*g_equations_name, "prev_errors"));
@ -197,6 +199,7 @@ expr mk_equations(equations_header const & h, unsigned num_eqs, expr const * eqs
m = set_bool(m, name(*g_equations_name, "is_private"), h.m_is_private);
m = set_bool(m, name(*g_equations_name, "is_lemma"), h.m_is_lemma);
m = set_bool(m, name(*g_equations_name, "is_unsafe"), h.m_is_unsafe);
m = set_bool(m, name(*g_equations_name, "is_partial"), h.m_is_partial);
m = set_bool(m, name(*g_equations_name, "is_noncomputable"), h.m_is_noncomputable);
m = set_bool(m, name(*g_equations_name, "aux_lemmas"), h.m_aux_lemmas);
m = set_bool(m, name(*g_equations_name, "prev_errors"), h.m_prev_errors);

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

@ -43,7 +43,8 @@ struct equations_header {
names m_fn_actual_names; /* Full qualified name and/or private name */
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_unsafe{false}; /* the auxiliary declarations should be tagged as unsafe */
bool m_is_unsafe{false}; /* the auxiliary declarations should be tagged as unsafe */
bool m_is_partial{false}; /* partial functions */
bool m_is_noncomputable{false}; /* if true, equation is not computable and code should not be generated */
bool m_aux_lemmas{false}; /* if true, we must create equation lemmas and induction principle */
/* m_prev_errors is true when errors have already being found processing the file,