refactor(*): add method get_num_univ_params

src/frontends/lean/calc.cpp

@@ -44,7 +44,7 @@ static pair<expr, unsigned> extract_arg_types_core(environment const & env, name
         arg_types.push_back(binding_domain(f_type));
         f_type = binding_body(f_type);
     }
-    return mk_pair(f_type, length(d.get_univ_params()));
+    return mk_pair(f_type, d.get_num_univ_params());
 }
 
 static expr extract_arg_types(environment const & env, name const & f, buffer<expr> & arg_types) {

src/frontends/lean/elaborator.cpp

@@ -671,7 +671,7 @@ expr elaborator::visit_constant(expr const & e) {
     buffer<level> ls;
     for (level const & l : const_levels(e))
         ls.push_back(replace_univ_placeholder(l));
-    unsigned num_univ_params = length(d.get_univ_params());
+    unsigned num_univ_params = d.get_num_univ_params();
     if (num_univ_params < ls.size())
         throw_kernel_exception(env(), sstream() << "incorrect number of universe levels parameters for '"
                                << const_name(e) << "', #" << num_univ_params

src/frontends/lean/find_cmd.cpp

@@ -54,7 +54,7 @@ bool get_find_expensive(options const & opts) {
 bool match_pattern(type_checker & tc, expr const & pattern, declaration const & d, unsigned max_steps, bool cheap) {
     name_generator ngen = tc.mk_ngen();
      buffer<level> ls;
-    unsigned num_ls = length(d.get_univ_params());
+    unsigned num_ls = d.get_num_univ_params();
     for (unsigned i = 0; i < num_ls; i++)
         ls.push_back(mk_meta_univ(ngen.next()));
     expr dt        = instantiate_type_univ_params(d, to_list(ls.begin(), ls.end()));

src/frontends/lean/inductive_cmd.cpp

@@ -663,7 +663,7 @@ struct inductive_cmd_fn {
     bool has_general_eliminator(environment const & env, name const & d_name) {
         declaration d = env.get(d_name);
         declaration r = env.get(mk_rec_name(d_name));
-        return length(d.get_univ_params()) != length(r.get_univ_params());
+        return d.get_num_univ_params() != r.get_num_univ_params();
     }
 
     /** \brief Add aliases for the inductive datatype, introduction and elimination rules */

src/frontends/lean/server.cpp

@@ -719,7 +719,7 @@ bool match_type(type_checker & tc, expr const & meta, expr const & expected_type
     name_generator ngen = tc.mk_ngen();
     goal g(meta, expected_type);
     buffer<level> ls;
-    unsigned num_ls = length(d.get_univ_params());
+    unsigned num_ls = d.get_num_univ_params();
     for (unsigned i = 0; i < num_ls; i++)
         ls.push_back(mk_meta_univ(ngen.next()));
     expr dt        = instantiate_type_univ_params(d, to_list(ls.begin(), ls.end()));

src/kernel/declaration.cpp

@@ -56,6 +56,7 @@ bool declaration::is_theorem() const       { return is_definition() && m_ptr->m_
 
 name const & declaration::get_name() const { return m_ptr->m_name; }
 level_param_names const & declaration::get_univ_params() const { return m_ptr->m_params; }
+unsigned declaration::get_num_univ_params() const { return length(get_univ_params()); }
 expr const & declaration::get_type() const { return m_ptr->m_type; }
 
 bool declaration::is_opaque() const { return m_ptr->m_opaque; }

src/kernel/declaration.h

@@ -61,6 +61,7 @@ public:
 
     name const & get_name() const;
     level_param_names const & get_univ_params() const;
+    unsigned get_num_univ_params() const;
     expr const & get_type() const;
 
     expr const & get_value() const;

src/kernel/instantiate.cpp

@@ -193,7 +193,7 @@ MK_THREAD_LOCAL_GET_DEF(instantiate_univ_cache, get_type_univ_cache);
 MK_THREAD_LOCAL_GET_DEF(instantiate_univ_cache, get_value_univ_cache);
 
 expr instantiate_type_univ_params(declaration const & d, levels const & ls) {
-    lean_assert(length(d.get_univ_params()) == length(ls));
+    lean_assert(d.get_num_univ_params() == length(ls));
     if (is_nil(ls) || !has_param_univ(d.get_type()))
         return d.get_type();
     instantiate_univ_cache & cache = get_type_univ_cache();
@@ -205,7 +205,7 @@ expr instantiate_type_univ_params(declaration const & d, levels const & ls) {
 }
 
 expr instantiate_value_univ_params(declaration const & d, levels const & ls) {
-    lean_assert(length(d.get_univ_params()) == length(ls));
+    lean_assert(d.get_num_univ_params() == length(ls));
     if (is_nil(ls) || !has_param_univ(d.get_value()))
         return d.get_value();
     instantiate_univ_cache & cache = get_value_univ_cache();

src/kernel/instantiate.h

@@ -33,11 +33,11 @@ expr instantiate_univ_params(expr const & e, level_param_names const & ps, level
 
 class declaration;
 /** \brief Instantiate the universe level parameters of the type of the given declaration.
-    \pre length(d.get_univ_params()) == length(ls)
+    \pre d.get_num_univ_params() == length(ls)
 */
 expr instantiate_type_univ_params(declaration const & d, levels const & ls);
 /** \brief Instantiate the universe level parameters of the value of the given declaration.
-    \pre length(d.get_univ_params()) == length(ls)
+    \pre d.get_num_univ_params() == length(ls)
 */
 expr instantiate_value_univ_params(declaration const & d, levels const & ls);
 }

src/library/definitional/cases_on.cpp

@@ -75,7 +75,7 @@ environment mk_cases_on(environment const & env, name const & n) {
     }
 
     levels lvls       = param_names_to_levels(rec_decl.get_univ_params());
-    bool elim_to_prop = length(rec_decl.get_univ_params()) == length(ind_decl.get_univ_params());
+    bool elim_to_prop = rec_decl.get_num_univ_params() == ind_decl.get_num_univ_params();
     level elim_univ   = elim_to_prop ? mk_level_zero() : head(lvls);
 
     optional<expr> unit;

src/library/definitional/induction_on.cpp

@@ -22,8 +22,8 @@ environment mk_induction_on(environment const & env, name const & n) {
     name induction_on_name(n, "induction_on");
     declaration rec_on_decl   = env.get(rec_on_name);
     declaration ind_decl      = env.get(n);
-    unsigned rec_on_num_univs = length(rec_on_decl.get_univ_params());
+    unsigned rec_on_num_univs = rec_on_decl.get_num_univ_params();
-    unsigned ind_num_univs    = length(ind_decl.get_univ_params());
+    unsigned ind_num_univs    = ind_decl.get_num_univ_params();
     bool opaque               = false;
     bool use_conv_opt         = true;
     environment new_env       = env;

src/library/definitional/no_confusion.cpp

@@ -42,7 +42,7 @@ optional<environment> mk_no_confusion_type(environment const & env, name const &
         rlvl = plvl;
     else
         rlvl = mk_max(plvl, ind_lvl);
-    if (length(ilvls) != length(ind_decl.get_univ_params()))
+    if (length(ilvls) != ind_decl.get_num_univ_params())
         return optional<environment>(); // type does not have only a restricted eliminator
     // All inductive datatype parameters and indices are arguments
     buffer<expr> args;

src/library/definitional/projection.cpp

@@ -127,7 +127,7 @@ public:
         expr const & I = get_app_args(s_t, I_args);
         if (is_constant(I)) {
             declaration proj_decl = env.get(m_proj_name);
-            if (length(const_levels(I)) != length(proj_decl.get_univ_params()))
+            if (length(const_levels(I)) != proj_decl.get_num_univ_params())
                 throw_kernel_exception(env, sstream() << "invalid projection application '" << m_proj_name
                                        << "', incorrect number of universe parameters", m);
             expr t = instantiate_type_univ_params(proj_decl, const_levels(I));

src/library/inductive_unifier_plugin.cpp

@@ -62,10 +62,10 @@ class inductive_unifier_plugin_cell : public unifier_plugin_cell {
             name const & intro_name = inductive::intro_rule_name(intro);
             declaration intro_decl  = env.get(intro_name);
             levels intro_lvls;
-            if (length(intro_decl.get_univ_params()) == elim_num_lvls) {
+            if (intro_decl.get_num_univ_params() == elim_num_lvls) {
                 intro_lvls = elim_lvls;
             } else {
-                lean_assert(length(intro_decl.get_univ_params()) == elim_num_lvls - 1);
+                lean_assert(intro_decl.get_num_univ_params() == elim_num_lvls - 1);
                 intro_lvls = tail(elim_lvls);
             }
             expr intro_fn   = mk_constant(inductive::intro_rule_name(intro), intro_lvls);

src/library/tactic/class_instance_synth.cpp

@@ -238,7 +238,7 @@ struct class_instance_elaborator : public choice_iterator {
         if (auto decl = env.find(inst)) {
             name_generator & ngen = m_C->m_ngen;
             buffer<level> ls_buffer;
-            unsigned num_univ_ps = length(decl->get_univ_params());
+            unsigned num_univ_ps = decl->get_num_univ_params();
             for (unsigned i = 0; i < num_univ_ps; i++)
                 ls_buffer.push_back(mk_meta_univ(ngen.next()));
             levels ls = to_list(ls_buffer.begin(), ls_buffer.end());

src/library/tactic/inversion_tactic.cpp

@@ -365,7 +365,7 @@ class inversion_tac {
         name const & I_name = const_name(I);
         expr g_type         = g.get_type();
         expr cases_on;
-        if (length(m_cases_on_decl.get_univ_params()) != length(m_I_decl.get_univ_params())) {
+        if (m_cases_on_decl.get_num_univ_params() != m_I_decl.get_num_univ_params()) {
             level g_lvl  = sort_level(m_tc.ensure_type(g_type).first);
             cases_on     = mk_constant({I_name, "cases_on"}, cons(g_lvl, const_levels(I)));
         } else {

src/library/unifier.cpp

@@ -1330,7 +1330,7 @@ struct unifier_fn {
         levels lhs_lvls = const_levels(lhs_fn);
         levels rhs_lvls = const_levels(lhs_fn);
         if (length(lhs_lvls) != length(rhs_lvls) ||
-            length(d.get_univ_params()) != length(lhs_lvls)) {
+            d.get_num_univ_params() != length(lhs_lvls)) {
             // the constraint is not well-formed, this can happen when users are abusing the API
             set_conflict(j);
             return false;