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

fix(library/equations_compiler): make sure _unsafe_rec auxiliary definitions contain all local constants used in the safe one

Browse source 
cc @kha
This commit is contained in:
Leonardo de Moura 2019-03-28 12:57:15 -07:00
parent 1f197b5293
commit 4dbae58646
3 changed files with 20 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -355,7 +355,8 @@ struct eta_expand_rec_apps_fn : public replace_visitor_with_tc {
};
static expr compile_equations_main(environment & env, elaborator & elab,
metavar_context & mctx, local_context const & lctx, expr const & _eqns, bool report_cexs) {
metavar_context & mctx, local_context const & lctx, expr const & _eqns,
bool report_cexs) {
// all following code assumes that all recursive occurrences are applications
type_context_old ctx(env, mctx, lctx, elab.get_cache(), transparency_mode::Semireducible);
expr eqns = eta_expand_rec_apps_fn(ctx)(_eqns);
@ -402,7 +403,8 @@ expr compile_equations(environment & env, elaborator & elab, metavar_context & m
aux_header.m_aux_lemmas = false;
aux_header.m_fn_actual_names = map(header.m_fn_actual_names, mk_unsafe_rec_name);
expr aux_eqns = remove_wf_annotation_from_equations(update_equations(eqns, aux_header));
compile_equations_main(env, elab, mctx, lctx, aux_eqns, false);
aux_eqns = eta_expand_rec_apps_fn(ctx)(aux_eqns);
unbounded_rec(env, elab, mctx, lctx, aux_eqns, some_expr(result));
return result;
} else {
return compile_equations_main(env, elab, mctx, lctx, eqns, true);

8
src/library/equations_compiler/unbounded_rec.cpp
View file

@ -82,7 +82,8 @@ static expr fix_rec_apps(expr const & e, name_map<name> const & aux_rec_name2act
eqn_compiler_result unbounded_rec(environment & env, elaborator & elab,
metavar_context & mctx, local_context const & lctx,
expr const & e) {
expr const & e, optional<expr> const & safe_result) {
lean_assert(!safe_result || is_equations_result(*safe_result));
/* Split recursive equations by using new auxiliary `.rec` locals */
buffer<expr> aux_rec_fns;
buffer<expr> es;
@ -118,6 +119,11 @@ eqn_compiler_result unbounded_rec(environment & env, elaborator & elab,
for (list<expr> const & ts : R.m_counter_examples) {
counter_examples.push_back(mk_app(ues.get_fn(0), ts));
}
if (safe_result) {
lean_assert(is_equations_result(*safe_result));
lean_assert(get_equations_result_size(*safe_result) == es.size());
helper.collect(get_equations_result(*safe_result, fidx));
}
}
helper.finalize_collection();

12
src/library/equations_compiler/unbounded_rec.h
View file

@ -9,11 +9,17 @@ Author: Leonardo de Moura
#include "library/equations_compiler/util.h"
namespace lean {
class elaborator;
/** \brief Eliminate "recursive calls" using rec_fn_macro.
/** \brief Eliminate "recursive calls" using unbounded recursion.
This compilation step can only be used to compile unsafe definitions.
If we use it on regular definitions, the kernel will reject it. */
If we use it on regular definitions, the kernel will reject it.
Remark: If `eqns` has already been compiled in safe mode,
then `safe_result` contains the result of the compilation.
We need this information to make sure the type of the auxiliary `_unsafe_rec` definitions
match the type of the regular ones.
*/
eqn_compiler_result unbounded_rec(environment & env, elaborator & elab,
metavar_context & mctx, local_context const & lctx,
expr const & eqns);
expr const & eqns, optional<expr> const & safe_result = optional<expr>());
}