From 79bf13e3edb4e80a71c5d866110d5d727eb8cef2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 9 May 2016 13:24:20 -0700
Subject: [PATCH] feat(compiler/inliner): simplify cases_on and nonrecursive
 recursor applications when possible

---
 src/compiler/inliner.cpp | 50 +++++++++++++++++++++++++++++++++++++++-
 1 file changed, 49 insertions(+), 1 deletion(-)

diff --git a/src/compiler/inliner.cpp b/src/compiler/inliner.cpp
index 4066dbbcf5..f4bd911a05 100644
--- a/src/compiler/inliner.cpp
+++ b/src/compiler/inliner.cpp
@@ -4,9 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include "kernel/inductive/inductive.h"
 #include "library/util.h"
 #include "library/module.h"
 #include "library/trace.h"
+#include "library/normalize.h"
+#include "compiler/util.h"
 #include "compiler/compiler_step_visitor.h"
 
 namespace lean {
@@ -94,12 +97,57 @@ class inline_simple_definitions_fn : public compiler_step_visitor {
         return compiler_step_visitor::visit_app(e);
     }
 
+    bool is_nonrecursive_recursor(name const & n) {
+        if (auto I_name = inductive::is_elim_rule(env(), n)) {
+            return !is_recursive_datatype(env(), *I_name);
+        }
+        return false;
+    }
+
+    /* Try to reduce cases_on (and nonrecursive recursor) application
+       if major became a constructor */
+    expr visit_cases_on_app(expr const & e_0) {
+        expr e = default_visit_app(e_0);
+        buffer<expr> args;
+        expr const & fn = get_app_args(e, args);
+        lean_assert(is_constant(fn));
+        bool is_cases_on            = is_cases_on_recursor(env(), const_name(fn));
+        name const & rec_name       = const_name(fn);
+        name const & I_name         = rec_name.get_prefix();
+        unsigned nparams            = *inductive::get_num_params(env(), I_name);
+        unsigned nindices           = *inductive::get_num_indices(env(), I_name);
+        unsigned major_idx;
+        if (is_cases_on) {
+            major_idx       = nparams + 1 + nindices;
+        } else {
+            major_idx       = *inductive::get_elim_major_idx(env(), rec_name);
+        }
+        expr major = beta_reduce(args[major_idx]);
+        if (is_constructor_app(env(), major)) {
+            /* Major premise became a constructor. So, we should reduce. */
+            expr new_e = e;
+            if (is_cases_on) {
+                /* unfold cases_on */
+                if (auto r = unfold_term(env(), new_e))
+                    new_e = *r;
+                else
+                    return e;
+            }
+            /* reduce */
+            if (auto r = ctx().norm_ext(new_e))
+                return compiler_step_visitor::visit(beta_reduce(*r));
+        }
+        return e;
+    }
+
     virtual expr visit_app(expr const & e) override {
         expr const & fn = get_app_fn(e);
         if (!is_constant(fn))
             return default_visit_app(e);
-        unsigned nargs  = get_app_num_args(e);
         name const & n  = const_name(fn);
+        if (is_cases_on_recursor(env(), n) || is_nonrecursive_recursor(n))
+            return visit_cases_on_app(e);
+        unsigned nargs  = get_app_num_args(e);
         declaration d   = env().get(n);
         if (!d.is_definition() || d.is_theorem())
             return default_visit_app(e);