perf: experiment: abstract recursors in recursor's RHSs

src/Lean/Declaration.lean

@@ -349,6 +349,8 @@ structure RecursorRule where
 structure RecursorVal extends ConstantVal where
   /-- List of all inductive datatypes in the mutual declaration that generated this recursor -/
   all : List Name
+  /-- List of all recursors mutually recursive with this one. Can be more than `all` with nested recursion -/
+  recs : List Name
   /-- Number of parameters -/
   numParams : Nat
   /-- Number of indices -/
@@ -373,9 +375,9 @@ structure RecursorVal extends ConstantVal where
   deriving Inhabited, BEq
 
 @[export lean_mk_recursor_val]
-def mkRecursorValEx (name : Name) (levelParams : List Name) (type : Expr) (all : List Name) (numParams numIndices numMotives numMinors : Nat)
+def mkRecursorValEx (name : Name) (levelParams : List Name) (type : Expr) (all : List Name) (recs : List Name) (numParams numIndices numMotives numMinors : Nat)
     (rules : List RecursorRule) (k isUnsafe : Bool) : RecursorVal := {
-  name, levelParams, type, all, numParams, numIndices,
+  name, levelParams, type, all, recs, numParams, numIndices,
   numMotives, numMinors, rules, k, isUnsafe
 }
 

src/Lean/Elab/Print.lean

@@ -96,6 +96,21 @@ private def printInduct (id : Name) (levelParams : List Name) (numParams : Nat)
     m := m ++ Format.line ++ ctor ++ " : " ++ cinfo.type
   logInfo m
 
+private def printRecursor (recInfo : RecursorVal) : CommandElabM Unit := do
+  let mut m ← mkHeader "recursor" recInfo.name recInfo.levelParams recInfo.type (if recInfo.isUnsafe then .unsafe else .safe)
+  if recInfo.recs.length > 1 then
+    m := m ++ Format.line ++ m!"mutual with: {recInfo.recs}"
+  m := m ++ Format.line ++ m!"number of parameters: {recInfo.numParams}"
+  m := m ++ Format.line ++ m!"number of indices: {recInfo.numIndices}"
+  m := m ++ Format.line ++ m!"number of motives: {recInfo.numMotives}"
+  m := m ++ Format.line ++ m!"number of minors: {recInfo.numMinors}"
+  if recInfo.k then
+    m := m ++ Format.line ++ m!"supports k-like reduction"
+  m := m ++ Format.line ++ "rules:"
+  for rule in recInfo.rules do
+    m := m ++ Format.line ++ m!"for {rule.ctor} ({rule.nfields} fields): {rule.rhs}"
+  logInfo m
+
 /--
 Computes the origin of a field. Returns its `StructureFieldInfo` at the origin.
 Multiple parents could be the origin of a field, but we say the first parent that provides it is the one that determines the origin.
@@ -196,7 +211,7 @@ private def printIdCore (sigOnly : Bool) (id : Name) : CommandElabM Unit := do
   | ConstantInfo.opaqueInfo  { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "opaque" id us t (if u then .unsafe else .safe)
   | ConstantInfo.quotInfo  { levelParams := us, type := t, .. } => printQuot id us t
   | ConstantInfo.ctorInfo { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "constructor" id us t (if u then .unsafe else .safe)
-  | ConstantInfo.recInfo { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "recursor" id us t (if u then .unsafe else .safe)
+  | ConstantInfo.recInfo recInfo => printRecursor recInfo
   | ConstantInfo.inductInfo { levelParams := us, numParams, type := t, ctors, isUnsafe := u, .. } =>
     if isStructure env id then
       printStructure id us numParams t ctors[0]! u

src/Lean/Meta/WHNF.lean

@@ -225,8 +225,10 @@ private def cleanupNatOffsetMajor (e : Expr) : MetaM Expr := do
     return mkNatSucc (mkNatAdd e (toExpr (k - 1)))
 
 /-- Auxiliary function for reducing recursor applications. -/
-private def reduceRec (recVal : RecursorVal) (recLvls : List Level) (recArgs : Array Expr) (failK : Unit → MetaM α) (successK : Expr → MetaM α) : MetaM α :=
+private def reduceRec (recVal : RecursorVal) (recLvls : List Level) (e : Expr) (failK : Unit → MetaM α) (successK : Expr → MetaM α) : MetaM α :=
+  let recArgs := e.getAppArgs
   let majorIdx := recVal.getMajorIdx
+  let recApp := e.stripArgsN (recArgs.size - (recVal.numParams + recVal.numMotives + recVal.numMinors))
   if h : majorIdx < recArgs.size then do
     let major := recArgs[majorIdx]
     let mut major ← if isWFRec recVal.name && (← getTransparency) == .default then
@@ -250,7 +252,16 @@ private def reduceRec (recVal : RecursorVal) (recLvls : List Level) (recArgs : A
       else
         let rhs := rule.rhs.instantiateLevelParams recVal.levelParams recLvls
         -- Apply parameters, motives and minor premises from recursor application.
-        let rhs := mkAppRange rhs 0 (recVal.numParams+recVal.numMotives+recVal.numMinors) recArgs
+        let rhs := mkAppRange rhs 0 (recVal.numParams+recVal.numMotives) recArgs
+        let rhs :=
+          if recVal.numMotives = 1 then
+            mkApp rhs recApp
+          else
+            let recApps := recVal.recs.toArray.map fun recName =>
+              mkAppRange (mkConst recName recLvls)
+                0 (recVal.numParams+recVal.numMotives+recVal.numMinors) recArgs
+            mkAppN rhs recApps
+        let rhs := mkAppRange rhs (recVal.numParams+recVal.numMotives) (recVal.numParams+recVal.numMotives+recVal.numMinors) recArgs
         /- The number of parameters in the constructor is not necessarily
            equal to the number of parameters in the recursor when we have
            nested inductive types. -/
@@ -683,7 +694,7 @@ where
             let .const cname lvls := f'.getAppFn | return e
             let some cinfo := (← getEnv).find? cname | return e
             match cinfo with
-            | .recInfo rec    => reduceRec rec lvls e.getAppArgs (fun _ => return e) (fun e => do recordUnfold cinfo.name; go e)
+            | .recInfo rec    => reduceRec rec lvls e (fun _ => return e) (fun e => do recordUnfold cinfo.name; go e)
             | .quotInfo rec   => reduceQuotRec rec e.getAppArgs (fun _ => return e) (fun e => do recordUnfold cinfo.name; go e)
             | c@(.defnInfo _) => do
               if (← isAuxDef c.name) then
@@ -924,7 +935,7 @@ def reduceRecMatcher? (e : Expr) : MetaM (Option Expr) := do
       let .const cname lvls := e.getAppFn | return none
       let some cinfo := (← getEnv).find? cname | return none
       match cinfo with
-      | .recInfo «rec»  => reduceRec «rec» lvls e.getAppArgs (fun _ => pure none) (fun e => do recordUnfold cinfo.name; pure (some e))
+      | .recInfo «rec»  => reduceRec «rec» lvls e (fun _ => pure none) (fun e => do recordUnfold cinfo.name; pure (some e))
       | .quotInfo «rec» => reduceQuotRec «rec» e.getAppArgs (fun _ => pure none) (fun e => do recordUnfold cinfo.name; pure (some e))
       | c@(.defnInfo _) =>
         if (← isAuxDef c.name) then

src/kernel/declaration.cpp

@@ -128,16 +128,16 @@ constructor_val::constructor_val(name const & n, names const & lparams, expr con
 }
 bool constructor_val::is_unsafe() const { return lean_constructor_val_is_unsafe(to_obj_arg()); }
 
-extern "C" object * lean_mk_recursor_val(object * n, object * lparams, object * type, object * all,
+extern "C" object * lean_mk_recursor_val(object * n, object * lparams, object * type, object * all, object * recs,
                                          object * nparams, object * nindices, object * nmotives, object * nminors,
                                          object * rules, uint8 k, uint8 unsafe);
 extern "C" uint8 lean_recursor_k(object * v);
 extern "C" uint8 lean_recursor_is_unsafe(object * v);
 
 recursor_val::recursor_val(name const & n, names const & lparams, expr const & type,
-                           names const & all, unsigned nparams, unsigned nindices, unsigned nmotives,
+                           names const & all, names const & recs, unsigned nparams, unsigned nindices, unsigned nmotives,
                            unsigned nminors, recursor_rules const & rules, bool k, bool is_unsafe):
-    object_ref(lean_mk_recursor_val(n.to_obj_arg(), lparams.to_obj_arg(), type.to_obj_arg(), all.to_obj_arg(),
+    object_ref(lean_mk_recursor_val(n.to_obj_arg(), lparams.to_obj_arg(), type.to_obj_arg(), all.to_obj_arg(), recs.to_obj_arg(),
                                     nat(nparams).to_obj_arg(), nat(nindices).to_obj_arg(), nat(nmotives).to_obj_arg(),
                                     nat(nminors).to_obj_arg(), rules.to_obj_arg(), k, is_unsafe)) {
 }

src/kernel/declaration.h

@@ -351,6 +351,7 @@ typedef list_ref<recursor_rule> recursor_rules;
 /*
 structure RecursorVal extends ConstantVal where
   all : List Name  -- List of all inductive datatypes in the mutual declaration that generated this recursor
+  recs : List Name -- Recursors mutually recursive with this one
   numParams : Nat
   numIndices : Nat
   numMotives : Nat
@@ -362,7 +363,7 @@ structure RecursorVal extends ConstantVal where
 class recursor_val : public object_ref {
 public:
     recursor_val(name const & n, names const & lparams, expr const & type,
-                 names const & all, unsigned nparams, unsigned nindices, unsigned nmotives,
+                 names const & all, names const & recs, unsigned nparams, unsigned nindices, unsigned nmotives,
                  unsigned nminors, recursor_rules const & rules, bool k, bool is_unsafe);
     recursor_val(recursor_val const & other):object_ref(other) {}
     recursor_val(recursor_val && other):object_ref(std::move(other)) {}
@@ -372,12 +373,13 @@ class recursor_val : public object_ref {
     name const & get_name() const { return to_constant_val().get_name(); }
     name const & get_major_induct() const;
     names const & get_all() const { return static_cast<names const &>(cnstr_get_ref(*this, 1)); }
-    unsigned get_nparams() const { return static_cast<nat const &>(cnstr_get_ref(*this, 2)).get_small_value(); }
-    unsigned get_nindices() const { return static_cast<nat const &>(cnstr_get_ref(*this, 3)).get_small_value(); }
-    unsigned get_nmotives() const { return static_cast<nat const &>(cnstr_get_ref(*this, 4)).get_small_value(); }
-    unsigned get_nminors() const { return static_cast<nat const &>(cnstr_get_ref(*this, 5)).get_small_value(); }
+    names const & get_recs() const { return static_cast<names const &>(cnstr_get_ref(*this, 2)); }
+    unsigned get_nparams() const { return static_cast<nat const &>(cnstr_get_ref(*this, 3)).get_small_value(); }
+    unsigned get_nindices() const { return static_cast<nat const &>(cnstr_get_ref(*this, 4)).get_small_value(); }
+    unsigned get_nmotives() const { return static_cast<nat const &>(cnstr_get_ref(*this, 5)).get_small_value(); }
+    unsigned get_nminors() const { return static_cast<nat const &>(cnstr_get_ref(*this, 6)).get_small_value(); }
     unsigned get_major_idx() const { return get_nparams() + get_nmotives() + get_nminors() + get_nindices(); }
-    recursor_rules const & get_rules() const { return static_cast<recursor_rules const &>(cnstr_get_ref(*this, 6)); }
+    recursor_rules const & get_rules() const { return static_cast<recursor_rules const &>(cnstr_get_ref(*this, 7)); }
     bool is_k() const;
     bool is_unsafe() const;
 };

src/kernel/expr.cpp

@@ -271,6 +271,15 @@ expr const & get_app_fn(expr const & e) {
     return *it;
 }
 
+expr const & get_app_fn_n(expr const & e, unsigned n) {
+    expr const * it = &e;
+    while (is_app(*it) && n > 0) {
+        it = &(app_fn(*it));
+        n--;
+    }
+    return *it;
+}
+
 unsigned get_app_num_args(expr const & e) {
     expr const * it = &e;
     unsigned n = 0;

src/kernel/expr.h

@@ -301,6 +301,8 @@ expr const & get_app_args_at_most(expr const & e, unsigned num, buffer<expr> & a
 expr const & get_app_rev_args(expr const & e, buffer<expr> & args);
 /** \brief Given \c e of the form <tt>(...(f a_1) ... a_n)</tt>, return \c f. If \c e is not an application, then return \c e. */
 expr const & get_app_fn(expr const & e);
+/** \brief Given \c e of the form <tt>(...(f a_1) ... a_n)</tt>, return \c f. */
+expr const & get_app_fn_n(expr const & e, unsigned n);
 /** \brief Given \c e of the form <tt>(...(f a_1) ... a_n)</tt>, return \c n. If \c e is not an application, then return 0. */
 unsigned get_app_num_args(expr const & e);
 

src/kernel/inductive.cpp

@@ -703,6 +703,19 @@ class add_inductive_fn {
     recursor_rules mk_rec_rules(unsigned d_idx, buffer<expr> const & Cs, buffer<expr> const & minors, unsigned & minor_idx) {
         inductive_type const & d = m_ind_types[d_idx];
         levels lvls = get_rec_levels();
+
+        buffer<expr> recs;
+        for (unsigned i = 0; i < m_ind_types.size(); i++) {
+            rec_info const & info = m_rec_infos[i];
+            expr C_app            = mk_app(mk_app(Cs[i], info.m_indices), info.m_major);
+            expr rec_ty           = mk_pi (info.m_indices, mk_pi(info.m_major, C_app));
+            name rec_name("rec");
+            if (m_ind_types.size() > 1)
+                rec_name = name(rec_name).append_after(i+1);
+            expr rec = mk_local_decl(rec_name, rec_ty);
+            recs.push_back(rec);
+        }
+
         buffer<recursor_rule> rules;
         for (constructor const & cnstr : d.get_cnstrs()) {
             buffer<expr> b_u;
@@ -733,13 +746,11 @@ class add_inductive_fn {
                 }
                 buffer<expr> it_indices;
                 unsigned it_idx = get_I_indices(u_i_ty, it_indices);
-                name rec_name   = mk_rec_name(m_ind_types[it_idx].get_name());
-                expr rec_app    = mk_constant(rec_name, lvls);
-                rec_app         = mk_app(mk_app(mk_app(mk_app(mk_app(rec_app, m_params), Cs), minors), it_indices), mk_app(u_i, xs));
+                expr rec_app    = mk_app(mk_app(recs[it_idx],it_indices), mk_app(u_i, xs));
                 v.push_back(mk_lambda(xs, rec_app));
             }
             expr e_app    = mk_app(mk_app(minors[minor_idx], b_u), v);
-            expr comp_rhs = mk_lambda(m_params, mk_lambda(Cs, mk_lambda(minors, mk_lambda(b_u, e_app))));
+            expr comp_rhs = mk_lambda(m_params, mk_lambda(Cs, mk_lambda(recs, mk_lambda(minors, mk_lambda(b_u, e_app)))));
             rules.push_back(recursor_rule(constructor_name(cnstr), b_u.size(), comp_rhs));
             minor_idx++;
         }
@@ -753,6 +764,7 @@ class add_inductive_fn {
         unsigned nminors   = minors.size();
         unsigned nmotives  = Cs.size();
         names all          = get_all_inductive_names();
+        names recs         = map(all, [](name const & n) { return mk_rec_name(n); });
         unsigned minor_idx = 0;
         for (unsigned d_idx = 0; d_idx < m_ind_types.size(); d_idx++) {
             rec_info const & info = m_rec_infos[d_idx];
@@ -766,7 +778,7 @@ class add_inductive_fn {
             recursor_rules rules  = mk_rec_rules(d_idx, Cs, minors, minor_idx);
             name rec_name         = mk_rec_name(m_ind_types[d_idx].get_name());
             names rec_lparams     = get_rec_lparams();
-            m_env.add_core(constant_info(recursor_val(rec_name, rec_lparams, rec_ty, all,
+            m_env.add_core(constant_info(recursor_val(rec_name, rec_lparams, rec_ty, all, recs,
                                                       m_nparams, m_nindices[d_idx], nmotives, nminors,
                                                       rules, m_K_target, m_is_unsafe)));
         }
@@ -822,7 +834,7 @@ struct elim_nested_inductive_result {
         return cnstr_name.replace_prefix(p->second, const_name(I));
     }
 
-    expr restore_nested(expr e, environment const & aux_env, name_map<name> const & aux_rec_name_map = name_map<name>()) {
+    expr restore_nested(expr e, environment const & aux_env) {
         local_ctx lctx;
         buffer<expr> As;
         bool pi = is_pi(e);
@@ -832,11 +844,6 @@ struct elim_nested_inductive_result {
             e = instantiate(binding_body(e), As.back());
         }
         e = replace(e, [&](expr const & t, unsigned) {
-                if (is_constant(t)) {
-                    if (name const * rec_name = aux_rec_name_map.find(const_name(t))) {
-                        return some_expr(mk_constant(*rec_name, const_levels(t)));
-                    }
-                }
                 expr const & fn = get_app_fn(t);
                 if (is_constant(fn)) {
                     if (expr const * nested = m_aux2nested.find(const_name(fn))) {
@@ -1130,11 +1137,17 @@ environment environment::add_inductive(declaration const & d) const {
             if (name const * new_name = aux_rec_name_map.find(rec_name))
                 new_rec_name = *new_name;
             constant_info rec_info = aux_env.get(rec_name);
-            expr new_rec_type      = res.restore_nested(rec_info.get_type(), aux_env, aux_rec_name_map);
+            expr new_rec_type      = res.restore_nested(rec_info.get_type(), aux_env);
             recursor_val rec_val   = rec_info.to_recursor_val();
             buffer<recursor_rule> new_rules;
+            names all_new_rec_names = map(rec_val.get_recs(), [&](name const & rec_name) {
+                    if (name const * new_name = aux_rec_name_map.find(rec_name))
+                        return *new_name;
+                    else
+                        return rec_name;
+            });
             for (recursor_rule const & rule : rec_val.get_rules()) {
-                expr new_rhs        = res.restore_nested(rule.get_rhs(), aux_env, aux_rec_name_map);
+                expr new_rhs        = res.restore_nested(rule.get_rhs(), aux_env);
                 name cnstr_name     = rule.get_cnstr();
                 name new_cnstr_name = cnstr_name;
                 if (new_rec_name != rec_name) {
@@ -1145,7 +1158,8 @@ environment environment::add_inductive(declaration const & d) const {
             }
             new_env.check_name(new_rec_name);
             new_env.add_core(constant_info(recursor_val(new_rec_name, rec_info.get_lparams(), new_rec_type,
-                                                        all_ind_names, rec_val.get_nparams(), rec_val.get_nindices(), rec_val.get_nmotives(),
+                                                        all_ind_names, all_new_rec_names,
+                                                        rec_val.get_nparams(), rec_val.get_nindices(), rec_val.get_nmotives(),
                                                         rec_val.get_nminors(), recursor_rules(new_rules),
                                                         rec_val.is_k(), rec_val.is_unsafe())));
         };

src/kernel/inductive.h

@@ -102,8 +102,19 @@ inline optional<expr> inductive_reduce_rec(environment const & env, expr const &
     if (rule->get_nfields() > major_args.size()) return none_expr();
     if (length(const_levels(rec_fn)) != length(rec_info->get_lparams())) return none_expr();
     expr rhs = instantiate_lparams(rule->get_rhs(), rec_info->get_lparams(), const_levels(rec_fn));
-    /* apply parameters, motives and minor premises from recursor application. */
-    rhs      = mk_app(rhs, rec_val.get_nparams() + rec_val.get_nmotives() + rec_val.get_nminors(), rec_args.data());
+    /* apply parameters, motives, recursor application and minor premises from recursor application. */
+    rhs      = mk_app(rhs, rec_val.get_nparams() + rec_val.get_nmotives(), rec_args.data());
+    expr rec_app = get_app_fn_n(e, rec_args.size() - (rec_val.get_nparams() + rec_val.get_nmotives() + rec_val.get_nminors()));
+    if (rec_val.get_nmotives() == 1) {
+        rhs      = mk_app(rhs, rec_app);
+    } else {
+        for (name rec_name : rec_val.get_recs()) {
+            expr rec_app2 = mk_const(rec_name, const_levels(rec_fn));
+            rec_app2 = mk_app(rec_app2, rec_val.get_nparams() + rec_val.get_nmotives() + rec_val.get_nminors(), rec_args.data());
+            rhs = mk_app(rhs, rec_app2);
+        }
+    }
+    rhs      = mk_app(rhs, rec_val.get_nminors(), rec_args.data() + rec_val.get_nparams() + rec_val.get_nmotives());
     /* The number of parameters in the constructor is not necessarily
        equal to the number of parameters in the recursor when we have
        nested inductive types. */

stage0/src/stdlib_flags.h

@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// please update me
+
 namespace lean {
 options get_default_options() {
     options opts;