refactor(library/definitional): add new to_telescope procedure, and remove code duplication in no_confusion.cpp

src/library/definitional/no_confusion.cpp

@@ -39,11 +39,7 @@ optional<environment> mk_no_confusion_type(environment const & env, name const &
     name heq_name("heq");
     // All inductive datatype parameters and indices are arguments
     buffer<expr> args;
-    while (is_pi(ind_type)) {
+    ind_type = to_telescope(ngen, ind_type, args, some(mk_implicit_binder_info()));
-        expr arg = mk_local(ngen.next(), binding_name(ind_type), binding_domain(ind_type), mk_implicit_binder_info());
-        args.push_back(arg);
-        ind_type = instantiate(binding_body(ind_type), arg);
-    }
     if (!is_sort(ind_type) || args.size() < nparams)
         throw_corrupted(n);
     lean_assert(!(env.impredicative() && is_zero(sort_level(ind_type))));
@@ -79,24 +75,14 @@ optional<environment> mk_no_confusion_type(environment const & env, name const &
     buffer<expr> outer_cases_on_args;
     unsigned idx1 = 0;
     while (is_pi(t1)) {
-        expr minor1 = tc.whnf(binding_domain(t1)).first;
         buffer<expr> minor1_args;
-        while (is_pi(minor1)) {
+        expr minor1 = to_telescope(tc, binding_domain(t1), minor1_args);
-            expr arg = mk_local(ngen.next(), binding_name(minor1), binding_domain(minor1), binding_info(minor1));
-            minor1_args.push_back(arg);
-            minor1   = tc.whnf(instantiate(binding_body(minor1), arg)).first;
-        }
         expr curr_t2  = t2;
         buffer<expr> inner_cases_on_args;
         unsigned idx2 = 0;
         while (is_pi(curr_t2)) {
-            expr minor2 = tc.whnf(binding_domain(curr_t2)).first;
             buffer<expr> minor2_args;
-            while (is_pi(minor2)) {
+            expr minor2 = to_telescope(tc, binding_domain(curr_t2), minor2_args);
-                expr arg = mk_local(ngen.next(), binding_name(minor2), binding_domain(minor2), binding_info(minor2));
-                minor2_args.push_back(arg);
-                minor2   = tc.whnf(instantiate(binding_body(minor2), arg)).first;
-            }
             if (idx1 != idx2) {
                 // infeasible case, constructors do not match
                 inner_cases_on_args.push_back(Fun(minor2_args, P));
@@ -158,11 +144,7 @@ environment mk_no_confusion(environment const & env, name const & n) {
     name heq_refl_name{"heq", "refl"};
     buffer<expr> args;
     expr type = no_confusion_type_type;
-    while (is_pi(type)) {
+    type = to_telescope(ngen, type, args, some(mk_implicit_binder_info()));
-        expr arg = mk_local(ngen.next(), binding_name(type), binding_domain(type), mk_implicit_binder_info());
-        args.push_back(arg);
-        type = instantiate(binding_body(type), arg);
-    }
     lean_assert(args.size() >= nparams + 3);
     unsigned nindices = args.size() - nparams - 3; // 3 is for P v1 v2
     expr range        = mk_app(mk_constant(no_confusion_type_decl.get_name(), ls), args);
@@ -205,13 +187,8 @@ environment mk_no_confusion(environment const & env, name const & n) {
     expr cot       = tc.infer(cases_on).first;
 
     while (is_pi(cot)) {
-        expr minor = tc.whnf(binding_domain(cot)).first;
         buffer<expr> minor_args;
-        while (is_pi(minor)) {
+        expr minor = to_telescope(tc, binding_domain(cot), minor_args);
-            expr arg = mk_local(ngen.next(), binding_name(minor), binding_domain(minor), binding_info(minor));
-            minor_args.push_back(arg);
-            minor   = tc.whnf(instantiate(binding_body(minor), arg)).first;
-        }
         lean_assert(!minor_args.empty());
         expr H  = minor_args.back();
         expr Ht = mlocal_type(H);

src/library/definitional/util.cpp

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include "kernel/find_fn.h"
 #include "kernel/instantiate.h"
+#include "kernel/type_checker.h"
 #include "kernel/inductive/inductive.h"
 
 namespace lean {
@@ -93,4 +94,18 @@ expr to_telescope(name_generator & ngen, expr type, buffer<expr> & telescope, op
     }
     return type;
 }
+
+expr to_telescope(type_checker & tc, expr type, buffer<expr> & telescope, optional<binder_info> const & binfo) {
+    type = tc.whnf(type).first;
+    while (is_pi(type)) {
+        expr local;
+        if (binfo)
+            local = mk_local(tc.mk_fresh_name(), binding_name(type), binding_domain(type), *binfo);
+        else
+            local = mk_local(tc.mk_fresh_name(), binding_name(type), binding_domain(type), binder_info(type));
+        telescope.push_back(local);
+        type = tc.whnf(instantiate(binding_body(type), local)).first;
+    }
+    return type;
+}
 }

src/library/definitional/util.h

@@ -35,6 +35,9 @@ bool is_inductive_predicate(environment const & env, name const & n);
 */
 expr to_telescope(name_generator & ngen, expr type, buffer<expr> & telescope,
                   optional<binder_info> const & binfo = optional<binder_info>());
+/** \brief Similar to previous method, but puts \c type in whnf */
+expr to_telescope(type_checker & tc, expr type, buffer<expr> & telescope,
+                  optional<binder_info> const & binfo = optional<binder_info>());
 
 /** \brief Return the universe where inductive datatype resides
     \pre \c ind_type is of the form <tt>Pi (a_1 : A_1) (a_2 : A_2[a_1]) ..., Type.{lvl}</tt>