chore(library/equations_compiler): add partial_rec skeleton

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)

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));

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<expr> add_some_fuel(list<expr> 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<eqn_compiler_result> 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<expr> 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);
+}
+}

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);
+}

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,