From ef5fac1481fb1b75865b6099c2714e3a963b5fac Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 27 Mar 2019 08:02:04 -0700 Subject: [PATCH] chore(library/equations_compiler): add `partial_rec` skeleton --- src/library/equations_compiler/CMakeLists.txt | 9 ++-- src/library/equations_compiler/compiler.cpp | 13 ++++- .../equations_compiler/partial_rec.cpp | 54 +++++++++++++++++++ src/library/equations_compiler/partial_rec.h | 16 ++++++ .../equations_compiler/unbounded_rec.h | 2 +- 5 files changed, 86 insertions(+), 8 deletions(-) create mode 100644 src/library/equations_compiler/partial_rec.cpp create mode 100644 src/library/equations_compiler/partial_rec.h diff --git a/src/library/equations_compiler/CMakeLists.txt b/src/library/equations_compiler/CMakeLists.txt index 350be06f93..8f630910f8 100644 --- a/src/library/equations_compiler/CMakeLists.txt +++ b/src/library/equations_compiler/CMakeLists.txt @@ -1,5 +1,4 @@ -add_library(equations_compiler OBJECT - equations.cpp util.cpp pack_domain.cpp - structural_rec.cpp unbounded_rec.cpp - elim_match.cpp compiler.cpp wf_rec.cpp - pack_mutual.cpp init_module.cpp) +add_library(equations_compiler OBJECT equations.cpp util.cpp + pack_domain.cpp structural_rec.cpp unbounded_rec.cpp elim_match.cpp + compiler.cpp wf_rec.cpp partial_rec.cpp pack_mutual.cpp + init_module.cpp) diff --git a/src/library/equations_compiler/compiler.cpp b/src/library/equations_compiler/compiler.cpp index 210dbe6475..2f3717fe2b 100644 --- a/src/library/equations_compiler/compiler.cpp +++ b/src/library/equations_compiler/compiler.cpp @@ -19,6 +19,7 @@ Author: Leonardo de Moura #include "library/equations_compiler/structural_rec.h" #include "library/equations_compiler/unbounded_rec.h" #include "library/equations_compiler/wf_rec.h" +#include "library/equations_compiler/partial_rec.h" #include "library/equations_compiler/elim_match.h" #include "frontends/lean/elaborator.h" @@ -38,6 +39,7 @@ static eqn_compiler_result compile_equations_core(environment & env, elaborator trace_compiler(tout() << "nested recursion: " << has_nested_rec(eqns) << "\n";); trace_compiler(tout() << "using_well_founded: " << is_wf_equations(eqns) << "\n";); equations_header const & header = get_equations_header(eqns); + trace_compiler(tout() << "partial: " << header.m_is_partial << "\n";); lean_assert(header.m_is_unsafe || !has_nested_rec(eqns)); if (header.m_is_unsafe) { @@ -47,6 +49,13 @@ static eqn_compiler_result compile_equations_core(environment & env, elaborator return unbounded_rec(env, elab, mctx, lctx, eqns); } + if (header.m_is_partial && is_recursive_eqns(ctx, eqns)) { + if (is_wf_equations(eqns)) { + throw exception("invalid use of 'using_well_founded', we do not need to use well founded recursion for partial definitions, since they can use unbounded recursion"); + } + return partial_rec(env, elab, mctx, lctx, eqns); + } + if (is_wf_equations(eqns)) { return wf_rec(env, elab, mctx, lctx, eqns); } @@ -386,10 +395,10 @@ expr compile_equations(environment & env, elaborator & elab, metavar_context & m /* Then, we compile the equations again using `unsafe` and generate code. The motivations are: - Clear execution cost semantics for recursive functions. - - Auxiliary unsafe definition may assist recursive definition unfolding in the type_context_old object. - */ + - Auxiliary unsafe definition may assist recursive definition unfolding in the type_context_old object. */ equations_header aux_header = header; aux_header.m_is_unsafe = true; + aux_header.m_is_partial = false; 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)); diff --git a/src/library/equations_compiler/partial_rec.cpp b/src/library/equations_compiler/partial_rec.cpp new file mode 100644 index 0000000000..3cfa8a69e0 --- /dev/null +++ b/src/library/equations_compiler/partial_rec.cpp @@ -0,0 +1,54 @@ +/* +Copyright (c) 2019 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "library/trace.h" +#include "library/equations_compiler/structural_rec.h" + +namespace lean { +struct partial_rec_fn { + environment m_env; + elaborator & m_elab; + metavar_context m_mctx; + local_context m_lctx; + + expr m_ref; + equations_header m_header; + + partial_rec_fn(environment const & env, elaborator & elab, + metavar_context const & mctx, local_context const & lctx): + m_env(env), m_elab(elab), m_mctx(mctx), m_lctx(lctx) { + } + + expr add_fuel_param(expr const & eqns) { + // TODO(Leo): + return eqns; + } + + list add_some_fuel(list const & fns) { + // TODO(Leo): + return fns; + } + + eqn_compiler_result operator()(expr const & eqns) { + m_ref = eqns; + m_header = get_equations_header(eqns); + // TODO(Leo): if it mutual recursion, then we need to "pack" functions, and then add auxiliary "fuel" parameter. + expr new_eqns = add_fuel_param(eqns); + optional R = try_structural_rec(m_env, m_elab, m_mctx, m_lctx, new_eqns); + if (!R) + throw generic_exception(m_ref, "failed to compile partial definition, structural recursion failed after adding fuel"); + // TODO(Leo): if it is mutual recursion, then we need to "unpack" result, and then add default "fuel". + list fns = add_some_fuel(R->m_fns); + return eqn_compiler_result({ fns, R->m_counter_examples }); + } +}; + +eqn_compiler_result partial_rec(environment & env, elaborator & elab, + metavar_context & mctx, local_context const & lctx, + expr const & eqns) { + return partial_rec_fn(env, elab, mctx, lctx)(eqns); +} +} diff --git a/src/library/equations_compiler/partial_rec.h b/src/library/equations_compiler/partial_rec.h new file mode 100644 index 0000000000..d6cf3c30c7 --- /dev/null +++ b/src/library/equations_compiler/partial_rec.h @@ -0,0 +1,16 @@ +/* +Copyright (c) 2019 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "library/type_context.h" +#include "library/equations_compiler/util.h" +namespace lean { +class elaborator; +/** \brief Eliminate "recursive calls" using "fuel". */ +eqn_compiler_result partial_rec(environment & env, elaborator & elab, + metavar_context & mctx, local_context const & lctx, + expr const & eqns); +} diff --git a/src/library/equations_compiler/unbounded_rec.h b/src/library/equations_compiler/unbounded_rec.h index ec7ad58016..88004fa9a1 100644 --- a/src/library/equations_compiler/unbounded_rec.h +++ b/src/library/equations_compiler/unbounded_rec.h @@ -11,7 +11,7 @@ namespace lean { class elaborator; /** \brief Eliminate "recursive calls" using rec_fn_macro. - This compilation step can only be used to compile meta definitions. + This compilation step can only be used to compile unsafe definitions. If we use it on regular definitions, the kernel will reject it. */ eqn_compiler_result unbounded_rec(environment & env, elaborator & elab, metavar_context & mctx, local_context const & lctx,