feat(frontends/lean/inductive_cmd): use new elaborator in the inductive command

library/data/list/sorted.lean

@@ -62,7 +62,7 @@ variable (R)
 
 inductive strongly_sorted : list A → Prop :=
 | base : strongly_sorted []
-| step : ∀ {a l}, all l (R a) → strongly_sorted l → strongly_sorted (a::l)
+| step : ∀ {a : A} {l : list A}, all l (R a) → strongly_sorted l → strongly_sorted (a::l)
 
 variable {R}
 

src/frontends/lean/inductive_cmd.cpp

@@ -680,7 +680,7 @@ struct inductive_cmd_fn {
         for (expr const & local : locals)
             locals_ctx = cons(local, locals_ctx);
         level_param_names new_ls;
-        std::tie(aux_type, new_ls) = m_p.old_elaborate_type(aux_type, locals_ctx);
+        std::tie(aux_type, new_ls) = m_p.elaborate_type(locals_ctx, aux_type);
         // save new levels
         for (auto l : new_ls)
             m_levels.push_back(l);

src/frontends/lean/parser.cpp

@@ -911,7 +911,7 @@ level parser::parse_level(unsigned rbp) {
 
     After the old elaborator is removed from the code base, we will be able to replace
     local_expr_decls with local_context in the parser, and avoid this adapter. */
-struct local_context_adapter {
+class local_context_adapter {
     local_context m_lctx;
     buffer<expr>  m_locals;
     buffer<expr>  m_local_refs;
@@ -926,6 +926,14 @@ struct local_context_adapter {
         return static_cast<bool>(find(e, [](expr const & e, unsigned) { return is_local(e) && !is_local_decl_ref(e); }));
     }
 
+    void add_local(expr const & local) {
+        expr const & local_type = mlocal_type(local);
+        expr new_local_type = translate_to(local_type);
+        expr new_local_ref  = m_lctx.mk_local_decl(local_pp_name(local), new_local_type, local_info(local));
+        m_locals.push_back(local);
+        m_local_refs.push_back(new_local_ref);
+    }
+
 public:
     void init(local_expr_decls const & ldecls) {
         lean_assert(m_lctx.empty() && m_locals.empty());
@@ -937,12 +945,19 @@ public:
             pair<name, expr> const & entry = entries[i];
             expr const & local = entry.second;
             if (!is_local(local)) continue;
+            add_local(local);
+        }
+    }
 
-            expr const & local_type = mlocal_type(local);
-            expr new_local_type = translate_to(local_type);
-            expr new_local_ref  = m_lctx.mk_local_decl(local_pp_name(local), new_local_type, local_info(local));
-            m_locals.push_back(local);
-            m_local_refs.push_back(new_local_ref);
+    void init(list<expr> const & lctx) {
+        lean_assert(std::all_of(lctx.begin(), lctx.end(), is_local));
+        lean_assert(m_lctx.empty() && m_locals.empty());
+        buffer<expr> entries;
+        to_buffer(lctx, entries);
+        unsigned i = entries.size();
+        while (i > 0) {
+            --i;
+            add_local(entries[i]);
         }
     }
 
@@ -990,9 +1005,8 @@ static expr replace_with_simple_metavars(metavar_context & mctx, expr const & e)
     return replace_with_simple_metavars(mctx, cache, e);
 }
 
-std::tuple<expr, level_param_names> parser::elaborate(metavar_context & mctx, expr const & e, bool check_unassigned) {
-    local_context_adapter adapter;
-    adapter.init(m_local_decls);
+std::tuple<expr, level_param_names> parser::elaborate(metavar_context & mctx, local_context_adapter const & adapter,
+                                                      expr const & e, bool check_unassigned) {
     expr tmp_e  = adapter.translate_to(e);
     std::tuple<expr, level_param_names> r =
         ::lean::elaborate(m_env, get_options(), mctx, adapter.lctx(), tmp_e, check_unassigned);
@@ -1004,11 +1018,30 @@ std::tuple<expr, level_param_names> parser::elaborate(metavar_context & mctx, ex
     return std::make_tuple(new_e, std::get<1>(r));
 }
 
+std::tuple<expr, level_param_names> parser::elaborate(metavar_context & mctx, expr const & e, bool check_unassigned) {
+    local_context_adapter adapter;
+    adapter.init(m_local_decls);
+    return elaborate(mctx, adapter, e, check_unassigned);
+}
+
 std::tuple<expr, level_param_names> parser::elaborate(expr const & e) {
     metavar_context mctx;
     return elaborate(mctx, e, true);
 }
 
+std::tuple<expr, level_param_names> parser::elaborate(list<expr> const & ctx, expr const & e) {
+    metavar_context mctx;
+    local_context_adapter adapter;
+    adapter.init(ctx);
+    return elaborate(mctx, adapter, e, true);
+}
+
+std::tuple<expr, level_param_names> parser::elaborate_type(list<expr> const & ctx, expr const & e) {
+    expr Type  = copy_tag(e, mk_sort(mk_level_placeholder()));
+    expr new_e = copy_tag(e, mk_typed_expr(Type, e));
+    return elaborate(ctx, new_e);
+}
+
 /* =========== BEGIN OF OLD ELABORATOR LEGACY CODE =========== */
 elaborator_context parser::mk_elaborator_context(bool check_unassigned) {
     return elaborator_context(m_env, get_options(), m_local_level_decls, check_unassigned);

src/frontends/lean/parser.h

@@ -41,6 +41,7 @@ struct interrupt_parser {};
 typedef local_decls<expr>       local_expr_decls;
 typedef environment             local_environment;
 class metavar_context;
+class local_context_adapter;
 
 /** \brief Extra data needed to be saved when we execute parser::push_local_scope */
 struct parser_scope {
@@ -501,8 +502,15 @@ public:
     std::tuple<expr, expr, level_param_names> old_elaborate_definition_at(environment const & env, local_level_decls const & lls,
                                                                           name const & n, expr const & t, expr const & v);
 
+private:
+    std::tuple<expr, level_param_names> elaborate(metavar_context & mctx, local_context_adapter const & adapter,
+                                                  expr const & e, bool check_unassigned = true);
+
+public:
     std::tuple<expr, level_param_names> elaborate(expr const & e);
     std::tuple<expr, level_param_names> elaborate(metavar_context & mctx, expr const & e, bool check_unassigned = true);
+    std::tuple<expr, level_param_names> elaborate(list<expr> const & ctx, expr const & e);
+    std::tuple<expr, level_param_names> elaborate_type(list<expr> const & ctx, expr const & e);
 
     expr mk_sorry(pos_info const & p);
     bool used_sorry() const { return m_used_sorry; }

tests/lean/ftree.lean.expected.out

@@ -1,2 +1,2 @@
 ftree.{l_1 l_2} : Type.{l_1} → Type.{l_2} → Type.{max 1 l_1 l_2}
-ftree.{l_1 l_2} : Type.{l_1} → Type.{l_2} → Type.{max 1 l_1 l_2}
+ftree.{l_1 l_2} : Type.{l_2} → Type.{l_1} → Type.{max 1 l_1 l_2}

tests/lean/no_confusion_type.lean

@@ -2,7 +2,7 @@ import logic
 open nat
 
 inductive vector (A : Type) : nat → Type :=
-vnil  : vector A zero |
+vnil  : vector A nat.zero |
 vcons : Π {n : nat}, A → vector A n → vector A (succ n)
 
 check vector.no_confusion_type

tests/lean/run/class_bug1.lean

@@ -22,6 +22,6 @@ section sec_cat
   definition id := category.rec (λ comp id assoc idr idl, id) Cat
   local infixr ∘ := compose
   inductive is_section {A B : ob} (f : mor A B) : Type :=
-  mk : ∀g, g ∘ f = id → is_section f
+  mk : ∀g : mor B A, g ∘ f = id → is_section f
 end sec_cat
 end category

tests/lean/run/injection1.lean

@@ -1,7 +1,7 @@
 open nat tactic
 
 inductive vec (A : Type) : nat → Type :=
-| nil  : vec A zero
+| nil  : vec A nat.zero
 | cons : ∀ {n}, A → vec A n → vec A (succ n)
 
 example (n : nat) (v w : vec nat n) (a b : nat) : vec.cons a v = vec.cons b w → a = b :=

tests/lean/run/vector2.lean

@@ -2,7 +2,7 @@ import logic data.nat.basic
 open nat
 
 inductive vector (A : Type) : nat → Type :=
-| vnil  : vector A zero
+| vnil  : vector A nat.zero
 | vcons : Π {n : nat}, A → vector A n → vector A (succ n)
 
 namespace vector

tests/lean/run/vector3.lean

@@ -2,7 +2,7 @@ import logic data.nat.basic
 open nat
 
 inductive vector (A : Type) : nat → Type :=
-| vnil  : vector A zero
+| vnil  : vector A nat.zero
 | vcons : Π {n : nat}, A → vector A n → vector A (succ n)
 
 namespace vector