experiment: index recursor_rules by constructor index

src/Lean/Declaration.lean

@@ -357,8 +357,8 @@ structure RecursorVal extends ConstantVal where
   numMotives : Nat
   /-- Number of minor premises -/
   numMinors : Nat
-  /-- A reduction for each Constructor -/
-  rules : List RecursorRule
+  /-- A reduction for each Constructor, indexed by constructor -/
+  rules : Array RecursorRule
   /-- It supports K-like reduction.
   A recursor is said to support K-like reduction if one can assume it behaves
   like `Eq` under axiom `K` --- that is, it has one constructor, the constructor has 0 arguments,
@@ -374,7 +374,7 @@ structure RecursorVal extends ConstantVal where
 
 @[export lean_mk_recursor_val]
 def mkRecursorValEx (name : Name) (levelParams : List Name) (type : Expr) (all : List Name) (numParams numIndices numMotives numMinors : Nat)
-    (rules : List RecursorRule) (k isUnsafe : Bool) : RecursorVal := {
+    (rules : Array RecursorRule) (k isUnsafe : Bool) : RecursorVal := {
   name, levelParams, type, all, numParams, numIndices,
   numMotives, numMinors, rules, k, isUnsafe
 }

src/Lean/Meta/WHNF.lean

@@ -130,10 +130,14 @@ private def mkNullaryCtor (type : Expr) (nparams : Nat) : MetaM (Option Expr) :=
   let (some ctor) ← getFirstCtor d | pure none
   return mkAppN (mkConst ctor lvls) (type.getAppArgs.shrink nparams)
 
-private def getRecRuleFor (recVal : RecursorVal) (major : Expr) : Option RecursorRule :=
+private def getRecRuleFor (recVal : RecursorVal) (major : Expr) : MetaM (Option RecursorRule) := do
   match major.getAppFn with
-  | .const fn _ => recVal.rules.find? fun r => r.ctor == fn
-  | _           => none
+  | .const fn _ =>
+    let .ctorInfo info ← getConstInfo fn | return none
+    let rule := recVal.rules[info.cidx]!
+    assert! rule.ctor == fn
+    return rule
+  | _           => return none
 
 private def toCtorWhenK (recVal : RecursorVal) (major : Expr) : MetaM Expr := do
   let majorType ← inferType major
@@ -242,7 +246,7 @@ private def reduceRec (recVal : RecursorVal) (recLvls : List Level) (recArgs : A
     major ← major.toCtorIfLit
     major ← cleanupNatOffsetMajor major
     major ← toCtorWhenStructure recVal.getMajorInduct major
-    match getRecRuleFor recVal major with
+    match (← getRecRuleFor recVal major) with
     | some rule =>
       let majorArgs := major.getAppArgs
       if recLvls.length != recVal.levelParams.length then

src/kernel/declaration.h

@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include <string>
 #include <limits>
 #include "kernel/expr.h"
+#include "runtime/array_ref.h"
 
 namespace lean {
 /**
@@ -346,7 +347,7 @@ public:
     expr const & get_rhs() const { return static_cast<expr const &>(cnstr_get_ref(*this, 2)); }
 };
 
-typedef list_ref<recursor_rule> recursor_rules;
+typedef array_ref<recursor_rule> recursor_rules;
 
 /*
 structure RecursorVal extends ConstantVal where
@@ -355,7 +356,7 @@ structure RecursorVal extends ConstantVal where
   numIndices : Nat
   numMotives : Nat
   numMinors : Nat
-  rules : List RecursorRule
+  rules : Array RecursorRule
   k : Bool         -- It supports K-like reduction.
   isUnsafe : Bool
 */

src/kernel/inductive.cpp

@@ -110,14 +110,17 @@ expr expand_eta_struct(environment const & env, expr const & e_type, expr const
     return result;
 }
 
-optional<recursor_rule> get_rec_rule_for(recursor_val const & rec_val, expr const & major) {
+optional<recursor_rule> get_rec_rule_for(environment const & env, recursor_val const & rec_val, expr const & major) {
     expr const & fn = get_app_fn(major);
     if (!is_constant(fn)) return optional<recursor_rule>();
-    for (recursor_rule const & rule : rec_val.get_rules()) {
-        if (rule.get_cnstr() == const_name(fn))
-            return optional<recursor_rule>(rule);
-    }
-    return optional<recursor_rule>();
+    optional<constant_info> ctor_info = env.find(const_name(fn));
+    if (!ctor_info || !ctor_info->is_constructor()) return optional<recursor_rule>();
+    constructor_val const & ctor_val = ctor_info->to_constructor_val();
+    recursor_rules const & rules = rec_val.get_rules();
+    lean_assert(ctor_val.get_cidx() < length(rules));
+    recursor_rule const & rule = rules[ctor_val.get_cidx()];
+    lean_assert(rule.get_cnstr() == const_name(fn));
+    return optional<recursor_rule>(rule);
 }
 
 /* Auxiliary class for adding a mutual inductive datatype declaration. */

src/kernel/inductive.h

@@ -49,7 +49,7 @@ inline expr to_cnstr_when_K(environment const & env, recursor_val const & rval,
     return *new_cnstr_app;
 }
 
-optional<recursor_rule> get_rec_rule_for(recursor_val const & rec_val, expr const & major);
+optional<recursor_rule> get_rec_rule_for(environment const & env, recursor_val const & rec_val, expr const & major);
 
 expr nat_lit_to_constructor(expr const & e);
 expr string_lit_to_constructor(expr const & e);
@@ -95,7 +95,7 @@ inline optional<expr> inductive_reduce_rec(environment const & env, expr const &
         major = whnf(string_lit_to_constructor(major));
     else
         major = to_cnstr_when_structure(env, rec_val.get_major_induct(), major, whnf, infer_type);
-    optional<recursor_rule> rule = get_rec_rule_for(rec_val, major);
+    optional<recursor_rule> rule = get_rec_rule_for(env, rec_val, major);
     if (!rule) return none_expr();
     buffer<expr> major_args;
     get_app_args(major, major_args);

stage0/src/stdlib_flags.h

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