feat(frontends/lean/elaborator): add support for nondependent eliminators in the new elaborator

library/init/datatypes.lean

@@ -6,6 +6,8 @@ Authors: Leonardo de Moura
 Basic datatypes
 -/
 prelude
+set_option new_elaborator true
+
 notation `Prop`  := Type.{0}
 notation `Type₁` := Type.{1}
 notation `Type₂` := Type.{2}
@@ -36,13 +38,13 @@ structure prod (A B : Type) :=
 inductive and (a b : Prop) : Prop
 | intro : a → b → and
 
-definition and.elim_left {a b : Prop} (H : and a b) : a  :=
-and.rec (λa b, a) H
+definition and.elim_left {a b : Prop} (H : and a b) : a :=
+and.rec (λ Ha Hb, Ha) H
 
 definition and.left := @and.elim_left
 
 definition and.elim_right {a b : Prop} (H : and a b) : b :=
-and.rec (λa b, b) H
+and.rec (λ Ha Hb, Hb) H
 
 definition and.right := @and.elim_right
 
@@ -362,7 +364,7 @@ namespace eq
   subst H₂ H₁
 
   theorem symm : a = b → b = a :=
-  eq.rec (refl a)
+  λ h, eq.rec (refl a) h
 end eq
 
 notation H1 ▸ H2 := eq.subst H1 H2

src/frontends/lean/elaborator.cpp

@@ -216,10 +216,43 @@ bool elaborator::is_elim_elab_candidate(name const & fn) {
     return false;
 }
 
+/** See comment at elim_info */
+auto elaborator::get_elim_info_for_builtin(name const & fn) -> elim_info {
+    lean_assert(is_aux_recursor(m_env, fn) || inductive::is_elim_rule(m_env, fn));
+    /* Remark: this is not just an optimization. The code at use_elim_elab_core
+       only works for dependent elimination. */
+    lean_assert(!fn.is_atomic());
+    name const & I_name    = fn.get_prefix();
+    optional<inductive::inductive_decl> decl = inductive::is_inductive_decl(m_env, I_name);
+    lean_assert(decl);
+    unsigned nparams  = decl->m_num_params;
+    unsigned nindices = *inductive::get_num_indices(m_env, I_name);
+    unsigned nminors  = length(decl->m_intro_rules);
+    elim_info r;
+    if (strcmp(fn.get_string(), "brec_on") == 0 || strcmp(fn.get_string(), "binduction_on") == 0) {
+        r.m_arity      = nparams + 1 /* motive */ + nindices + 1 /* major */ + 1;
+    } else {
+        r.m_arity      = nparams + 1 /* motive */ + nindices + 1 /* major */ + nminors;
+    }
+    r.m_nexplicit  = 1 /* major premise */ + nminors;
+    r.m_motive_idx = nparams;
+    unsigned major_idx;
+    if (inductive::is_elim_rule(m_env, fn)) {
+        major_idx = nparams + 1 + nindices + nminors;
+    } else {
+        major_idx = nparams + 1 + nindices;
+    }
+    r.m_idxs = to_list(major_idx);
+    return r;
+}
+
 /** See comment at elim_info */
 auto elaborator::use_elim_elab_core(name const & fn) -> optional<elim_info> {
     if (!is_elim_elab_candidate(fn))
         return optional<elim_info>();
+    if (is_aux_recursor(m_env, fn) || inductive::is_elim_rule(m_env, fn)) {
+        return optional<elim_info>(get_elim_info_for_builtin(fn));
+    }
     type_context::tmp_locals locals(m_ctx);
     declaration d     = m_env.get(fn);
     expr type         = d.get_type();
@@ -662,19 +695,19 @@ expr elaborator::visit_elim_app(expr const & fn, elim_info const & info, buffer<
         << "  arity:     " << info.m_arity << "\n"
         << "  nexplicit: " << info.m_nexplicit << "\n"
         << "  motive:    #" << (info.m_motive_idx+1) << "\n"
-        << "  major:    ";
-        for (unsigned idx : info.m_explicit_idxs)
+        << "  \"major\":  ";
+        for (unsigned idx : info.m_idxs)
             tout() << " #" << (idx+1);
         tout() << "\n";);
 
     expr fn_type = try_to_pi(infer_type(fn));
     buffer<expr> new_args;
 
-    /* In the first pass we only process the arguments at info.m_explicit_idxs */
+    /* In the first pass we only process the arguments at info.m_idxs */
     expr type = fn_type;
     unsigned i = 0;
     unsigned j = 0;
-    list<unsigned> main_idxs = info.m_explicit_idxs;
+    list<unsigned> main_idxs  = info.m_idxs;
     buffer<optional<expr>> postponed_args; // mark arguments that must be elaborated in the second pass.
     {
         while (is_pi(type)) {
@@ -749,9 +782,9 @@ expr elaborator::visit_elim_app(expr const & fn, elim_info const & info, buffer<
     trace_elab_debug(tout() << "compute motive by using keyed-abstraction:\n  " <<
                      instantiate_mvars(type) << "\nwith\n  " <<
                      expected_type << "\n";);
+    expr motive = expected_type;
     buffer<expr> keys;
     get_app_args(type, keys);
-    expr motive = expected_type;
     i = keys.size();
     while (i > 0) {
         --i;

src/frontends/lean/elaborator.h

@@ -59,13 +59,14 @@ private:
         of the form (C a_1 ... a_n) where C and a_i's are parameters. Moreover, the parameters a_i's
         can be inferred using explicit parameters. */
     struct elim_info {
-        unsigned       m_arity; /* "arity" of the "eliminator" */
-        unsigned       m_nexplicit; /* Number of explicit arguments */
+        unsigned       m_arity;      /* "arity" of the "eliminator" */
+        unsigned       m_nexplicit;  /* Number of explicit arguments */
         unsigned       m_motive_idx; /* Position of the motive (i.e., C) */
-        list<unsigned> m_explicit_idxs; /* Position of the explicit parameters that we use to synthesize the a_i's */
+        list<unsigned> m_idxs;       // Position of the explicit parameters that we use to synthesize the a_i's
+                                     // or need to be processed in the first pass.
         elim_info() {}
-        elim_info(unsigned arity, unsigned nexplicit, unsigned midx, list<unsigned> const & eidxs):
-            m_arity(arity), m_nexplicit(nexplicit), m_motive_idx(midx), m_explicit_idxs(eidxs) {}
+        elim_info(unsigned arity, unsigned nexplicit, unsigned midx, list<unsigned> const & idxs):
+            m_arity(arity), m_nexplicit(nexplicit), m_motive_idx(midx), m_idxs(idxs) {}
     };
 
     /** \brief Cache for constants that are handled using "eliminator" elaboration. */
@@ -134,6 +135,7 @@ private:
     expr enforce_type(expr const & e, expr const & expected_type, char const * header, expr const & ref);
 
     bool is_elim_elab_candidate(name const & fn);
+    elim_info get_elim_info_for_builtin(name const & fn);
     optional<elim_info> use_elim_elab_core(name const & fn);
     optional<elim_info> use_elim_elab(name const & fn);
 

tests/lean/671.lean.expected.out

@@ -1,2 +1,2 @@
 protected definition nat.add : ℕ → ℕ → ℕ :=
-λ a, nat.rec a (λ b₁, nat.succ)
+λ a b, nat.rec a (λ b₁ r, nat.succ r) b

tests/lean/def_inaccessible_issue.lean.expected.out

@@ -2,7 +2,7 @@ map2._main.equations.eqn_2 :
   ∀ (f : bool → bool → bool) (n : ℕ) (b1 : bool) (v1 : bv n) (b2 : bool) (v2 : bv n),
     map2._main f (cons n b1 v1) (cons n b2 v2) = cons n (f b1 b2) (map2._main f v1 v2)
 map2'._main.equations.eqn_2 :
-  ∀ (f : bool → bool → bool) (n : ℕ) (b1 : bool) (v1 : bv (nat.rec n (λ (b₁ : ℕ), succ) 0)) (b2 : bool)
-  (v2 : bv (nat.rec n (λ (b₁ : ℕ), succ) 0)),
-    map2'._main f (cons (nat.rec n (λ (b₁ : ℕ), succ) 0) b1 v1)
-      (cons (nat.rec n (λ (b₁ : ℕ), succ) 0) b2 v2) = cons n (f b1 b2) (map2'._main f v1 v2)
+  ∀ (f : bool → bool → bool) (n : ℕ) (b1 : bool) (v1 : bv (nat.rec n (λ (b₁ r : ℕ), succ r) 0)) (b2 : bool)
+  (v2 : bv (nat.rec n (λ (b₁ r : ℕ), succ r) 0)),
+    map2'._main f (cons (nat.rec n (λ (b₁ r : ℕ), succ r) 0) b1 v1)
+      (cons (nat.rec n (λ (b₁ r : ℕ), succ r) 0) b2 v2) = cons n (f b1 b2) (map2'._main f v1 v2)

tests/lean/set_attr1.lean.expected.out

@@ -1,3 +1,5 @@
+set_attr1.lean:8:11:failed to generate bytecode for 'ex1'
+set_attr1.lean:8:0: warning: proof generation for the prop_simplifier macro has not been implemented yet
 set_attr1.lean:15:0: error: tactic failed, result contains meta-variables
 state:
 n : ℕ

tests/lean/whnf.lean.expected.out

@@ -1,4 +1,4 @@
-succ (nat.rec 2 (λ b₁, succ) 0)
+succ (nat.rec 2 (λ b₁ r, succ r) 0)
 3
-succ (nat.rec a (λ b₁, succ) 0)
+succ (nat.rec a (λ b₁ r, succ r) 0)
 succ a

tests/lean/whnf_cache_bug.lean.expected.out

@@ -1,2 +1,2 @@
 ?m_1
-nat.succ (nat.rec 1 (λ b₁, nat.succ) 0)
+nat.succ (nat.rec 1 (λ b₁ r, nat.succ r) 0)

tests/lean/whnf_core1.lean.expected.out

@@ -1,4 +1,4 @@
-nat.succ (nat.rec a (λ b₁, nat.succ) (nat.rec 1 (λ b₁, nat.succ) 0))
-nat.succ (nat.rec a (λ b₁, nat.succ) (nat.rec 1 (λ b₁, nat.succ) 0))
+nat.succ (nat.rec a (λ b₁ r, nat.succ r) (nat.rec 1 (λ b₁ r, nat.succ r) 0))
+nat.succ (nat.rec a (λ b₁ r, nat.succ r) (nat.rec 1 (λ b₁ r, nat.succ r) 0))
 f a
 a + 2