feat(library/compiler): add new compilation step where we reduce cases_on, constructor and projection applications into a basic primitives

src/library/compiler/CMakeLists.txt

@@ -1,4 +1,4 @@
 add_library(compiler OBJECT util.cpp eta_expansion.cpp simp_pr1_rec.cpp preprocess_rec.cpp
   compiler_step_visitor.cpp elim_recursors.cpp comp_irrelevant.cpp
   inliner.cpp rec_fn_macro.cpp erase_irrelevant.cpp reduce_arity.cpp
-  lambda_lifting.cpp init_module.cpp)
+  lambda_lifting.cpp simp_inductive.cpp init_module.cpp)

src/library/compiler/erase_irrelevant.cpp

@@ -19,6 +19,11 @@ Author: Leonardo de Moura
 namespace lean {
 static expr * g_neutral_expr     = nullptr;
 static expr * g_unreachable_expr = nullptr;
+
+expr mk_neutral_expr() {
+    return *g_neutral_expr;
+}
+
 class erase_irrelevant_fn : public compiler_step_visitor {
 
     virtual expr visit_sort(expr const &) override {

src/library/compiler/erase_irrelevant.h

@@ -22,6 +22,8 @@ expr erase_irrelevant(environment const & env, expr const & e);
 bool is_neutral_expr(expr const & e);
 bool is_unreachable_expr(expr const & e);
 
+expr mk_neutral_expr();
+
 void initialize_erase_irrelevant();
 void finalize_erase_irrelevant();
 }

src/library/compiler/init_module.cpp

@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include "library/compiler/inliner.h"
 #include "library/compiler/rec_fn_macro.h"
 #include "library/compiler/erase_irrelevant.h"
+#include "library/compiler/simp_inductive.h"
 
 namespace lean {
 void initialize_compiler_module() {
@@ -17,8 +18,10 @@ void initialize_compiler_module() {
     initialize_inliner();
     initialize_rec_fn_macro();
     initialize_erase_irrelevant();
+    initialize_simp_inductive();
 }
 void finalize_compiler_module() {
+    finalize_simp_inductive();
     finalize_erase_irrelevant();
     finalize_rec_fn_macro();
     finalize_inliner();

src/library/compiler/preprocess_rec.cpp

@@ -21,6 +21,7 @@ Author: Leonardo de Moura
 #include "library/compiler/erase_irrelevant.h"
 #include "library/compiler/reduce_arity.h"
 #include "library/compiler/lambda_lifting.h"
+#include "library/compiler/simp_inductive.h"
 
 namespace lean {
 class expand_aux_recursors_fn : public compiler_step_visitor {
@@ -147,6 +148,9 @@ public:
         lean_trace(name({"compiler", "reduce_arity"}), tout() << "\n"; display(procs););
         lambda_lifting(m_env, d.get_name(), procs);
         lean_trace(name({"compiler", "lambda_lifting"}), tout() << "\n"; display(procs););
+        simp_inductive(m_env, procs);
+        lean_trace(name({"compiler", "simplify_inductive"}), tout() << "\n"; display(procs););
+
         display(procs);
         // TODO(Leo)
     }
@@ -167,6 +171,7 @@ void initialize_preprocess_rec() {
     register_trace_class({"compiler", "erase_irrelevant"});
     register_trace_class({"compiler", "reduce_arity"});
     register_trace_class({"compiler", "lambda_lifting"});
+    register_trace_class({"compiler", "simplify_inductive"});
     g_tmp_prefix = new name(name::mk_internal_unique_name());
 }
 

src/library/compiler/simp_inductive.cpp

@@ -0,0 +1,185 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "kernel/instantiate.h"
+#include "kernel/inductive/inductive.h"
+#include "library/util.h"
+#include "library/projection.h"
+#include "library/constants.h"
+#include "library/compiler/util.h"
+#include "library/compiler/erase_irrelevant.h"
+#include "library/compiler/compiler_step_visitor.h"
+
+namespace lean {
+static name * g_cases = nullptr;
+static name * g_cnstr = nullptr;
+static name * g_proj  = nullptr;
+
+static expr mk_constructor(unsigned cidx) {
+    return mk_constant(name(*g_cnstr, cidx));
+}
+
+static expr mk_proj(unsigned idx) {
+    return mk_constant(name(*g_proj, idx));
+}
+
+static expr mk_cases(unsigned n) {
+    return mk_constant(name(*g_cases, n));
+}
+
+static optional<unsigned> is_internal_symbol(expr const & e, name const & prefix) {
+    if (!is_constant(e))
+        return optional<unsigned>();
+    name const & n = const_name(e);
+    if (n.is_atomic() || !n.is_numeral())
+        return optional<unsigned>();
+    if (n.get_prefix() == prefix)
+        return optional<unsigned>(n.get_numeral());
+    else
+        return optional<unsigned>();
+}
+
+optional<unsigned> is_internal_cnstr(expr const & e) {
+    return is_internal_symbol(e, *g_cnstr);
+}
+
+optional<unsigned> is_internal_cases(expr const & e) {
+    return is_internal_symbol(e, *g_cases);
+}
+
+optional<unsigned> is_internal_proj(expr const & e) {
+    return is_internal_symbol(e, *g_proj);
+}
+
+class simp_inductive_fn : public compiler_step_visitor {
+    name_map<list<bool>> m_constructor_info;
+
+    static bool ignore(name const & n) {
+        return n == get_nat_zero_name() || n == get_nat_succ_name() || n == get_nat_cases_on_name();
+    }
+
+    void get_constructor_info(name const & n, buffer<bool> & rel_fields) {
+        if (auto r = m_constructor_info.find(n)) {
+            to_buffer(*r, rel_fields);
+        } else {
+            get_constructor_relevant_fields(env(), n, rel_fields);
+            m_constructor_info.insert(n, to_list(rel_fields));
+        }
+    }
+
+    expr visit_minor_premise(expr e, buffer<bool> const & rel_fields) {
+        type_context::tmp_locals locals(ctx());
+        for (unsigned i = 0; i < rel_fields.size(); i++) {
+            lean_assert(is_lambda(e));
+            if (rel_fields[i]) {
+                expr l = locals.push_local_from_binding(e);
+                e = instantiate(binding_body(e), l);
+            } else {
+                e = instantiate(binding_body(e), mk_neutral_expr());
+            }
+        }
+        e = visit(e);
+        return locals.mk_lambda(e);
+    }
+
+    expr visit_cases_on(name const & fn, buffer<expr> & args) {
+        name const & I_name = fn.get_prefix();
+        buffer<name> cnames;
+        get_intro_rule_names(env(), I_name, cnames);
+        /* Process major premise */
+        args[0] = visit(args[0]);
+        /* We distribute applications over cases_on minor premises in
+           previous preprocessing steps. */
+        lean_assert(args.size() == cnames.size() + 1);
+        /* Process minor premises */
+        for (unsigned i = 0; i < cnames.size(); i++) {
+            buffer<bool> rel_fields;
+            get_constructor_info(cnames[i], rel_fields);
+            args[i+1] = visit_minor_premise(args[i+1], rel_fields);
+        }
+
+        return mk_app(mk_cases(cnames.size()), args);
+    }
+
+    expr visit_constructor(name const & fn, buffer<expr> const & args) {
+        name I_name      = *inductive::is_intro_rule(env(), fn);
+        unsigned nparams = *inductive::get_num_params(env(), I_name);
+        unsigned cidx    = get_constructor_idx(env(), fn);
+        buffer<bool> rel_fields;
+        get_constructor_info(fn, rel_fields);
+        lean_assert(args.size() == nparams + rel_fields.size());
+        buffer<expr> new_args;
+        for (unsigned i = 0; i < rel_fields.size(); i++) {
+            if (rel_fields[i]) {
+                new_args.push_back(visit(args[nparams + i]));
+            }
+        }
+        return mk_app(mk_constructor(cidx), new_args);
+    }
+
+    expr visit_projection(name const & fn, buffer<expr> const & args) {
+        projection_info const & info = *get_projection_info(env(), fn);
+        expr major = visit(args[info.m_nparams]);
+        buffer<bool> rel_fields;
+        get_constructor_info(info.m_constructor, rel_fields);
+        lean_assert(info.m_i < rel_fields.size());
+        lean_assert(rel_fields[info.m_i]); /* We already erased irrelevant information */
+        /* Adjust projection index by ignoring irrelevant fields */
+        unsigned j = 0;
+        for (unsigned i = 0; i < info.m_i; i++) {
+            if (rel_fields[i])
+                j++;
+        }
+        expr r     = mk_app(mk_proj(j), major);
+        /* Add additional arguments */
+        for (unsigned i = info.m_nparams + 1; i < args.size(); i++)
+            r = mk_app(r, visit(args[i]));
+        return r;
+    }
+
+    virtual expr visit_app(expr const & e) override {
+        buffer<expr> args;
+        expr const & fn = get_app_args(e, args);
+        if (is_constant(fn)) {
+            name const & n = const_name(fn);
+            if (!ignore(n)) {
+                if (is_cases_on_recursor(env(), n)) {
+                    return visit_cases_on(n, args);
+                } else if (inductive::is_intro_rule(env(), n)) {
+                    return visit_constructor(n, args);
+                } else if (is_projection(env(), n)) {
+                    return visit_projection(n, args);
+                }
+            }
+        }
+        return compiler_step_visitor::visit_app(e);
+    }
+public:
+    simp_inductive_fn(environment const & env):compiler_step_visitor(env) {}
+};
+
+expr simp_inductive(environment const & env, expr const & e) {
+    return simp_inductive_fn(env)(e);
+}
+
+void simp_inductive(environment const & env, buffer<pair<name, expr>> & procs) {
+    simp_inductive_fn fn(env);
+    for (auto & proc : procs)
+        proc.second = fn(proc.second);
+}
+
+void initialize_simp_inductive() {
+    g_cases = new name("_cases");
+    g_proj  = new name("_proj");
+    g_cnstr = new name("_cnstr");
+}
+
+void finalize_simp_inductive() {
+    delete g_cases;
+    delete g_proj;
+    delete g_cnstr;
+}
+}

src/library/compiler/simp_inductive.h

@@ -0,0 +1,26 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "kernel/environment.h"
+
+namespace lean {
+/** \brief Replaces cases_on, projections and constructor applications with _cases.idx, _proj.idx and _cnstr.idx
+    It also removes irrelevant fields from constructors.
+    \remark nat.cases_on, nat.succ and nat.zero are ignored. */
+expr simp_inductive(environment const & env, expr const & e);
+void simp_inductive(environment const & env, buffer<pair<name, expr>> & procs);
+
+/** \brief Return non-none idx iff \c e is of the form _cnstr.idx */
+optional<unsigned> is_internal_cnstr(expr const & e);
+/** \brief Return non-none idx iff \c e is of the form _proj.idx */
+optional<unsigned> is_internal_proj(expr const & e);
+/** \brief Return non-none n iff \c e is of the form _cases.n */
+optional<unsigned> is_internal_cases(expr const & e);
+
+void initialize_simp_inductive();
+void finalize_simp_inductive();
+}