diff --git a/src/frontends/lean/calc.cpp b/src/frontends/lean/calc.cpp index 4cc95f02f..e3cece64f 100644 --- a/src/frontends/lean/calc.cpp +++ b/src/frontends/lean/calc.cpp @@ -44,7 +44,7 @@ static pair 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 & arg_types) { diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 303f8b181..41f5bc20d 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -671,7 +671,7 @@ expr elaborator::visit_constant(expr const & e) { buffer 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 diff --git a/src/frontends/lean/find_cmd.cpp b/src/frontends/lean/find_cmd.cpp index 34bd1aff7..29bbcdf29 100644 --- a/src/frontends/lean/find_cmd.cpp +++ b/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 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())); diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp index f1502d2ba..ab3ff8606 100644 --- a/src/frontends/lean/inductive_cmd.cpp +++ b/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 */ diff --git a/src/frontends/lean/server.cpp b/src/frontends/lean/server.cpp index afcf371cc..b664a8ec4 100644 --- a/src/frontends/lean/server.cpp +++ b/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 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())); diff --git a/src/kernel/declaration.cpp b/src/kernel/declaration.cpp index 1b7710c23..95a5c8626 100644 --- a/src/kernel/declaration.cpp +++ b/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; } diff --git a/src/kernel/declaration.h b/src/kernel/declaration.h index 3afb4064f..360d9e5ad 100644 --- a/src/kernel/declaration.h +++ b/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; diff --git a/src/kernel/instantiate.cpp b/src/kernel/instantiate.cpp index d8e01ea0d..9a4f80db1 100644 --- a/src/kernel/instantiate.cpp +++ b/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(); diff --git a/src/kernel/instantiate.h b/src/kernel/instantiate.h index 025668e16..aa4f7e8cf 100644 --- a/src/kernel/instantiate.h +++ b/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); } diff --git a/src/library/definitional/cases_on.cpp b/src/library/definitional/cases_on.cpp index 6ecf5b657..2a2ccb8c0 100644 --- a/src/library/definitional/cases_on.cpp +++ b/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 unit; diff --git a/src/library/definitional/induction_on.cpp b/src/library/definitional/induction_on.cpp index b1c7c499a..6f46fa629 100644 --- a/src/library/definitional/induction_on.cpp +++ b/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 ind_num_univs = length(ind_decl.get_univ_params()); + unsigned rec_on_num_univs = rec_on_decl.get_num_univ_params(); + unsigned ind_num_univs = ind_decl.get_num_univ_params(); bool opaque = false; bool use_conv_opt = true; environment new_env = env; diff --git a/src/library/definitional/no_confusion.cpp b/src/library/definitional/no_confusion.cpp index 7412a2c2c..0995b2735 100644 --- a/src/library/definitional/no_confusion.cpp +++ b/src/library/definitional/no_confusion.cpp @@ -42,7 +42,7 @@ optional 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(); // type does not have only a restricted eliminator // All inductive datatype parameters and indices are arguments buffer args; diff --git a/src/library/definitional/projection.cpp b/src/library/definitional/projection.cpp index c39572c1f..9d4cad375 100644 --- a/src/library/definitional/projection.cpp +++ b/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)); diff --git a/src/library/inductive_unifier_plugin.cpp b/src/library/inductive_unifier_plugin.cpp index 44268964f..5d76c96a5 100644 --- a/src/library/inductive_unifier_plugin.cpp +++ b/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); diff --git a/src/library/tactic/class_instance_synth.cpp b/src/library/tactic/class_instance_synth.cpp index 6c63808a0..470d5ce26 100644 --- a/src/library/tactic/class_instance_synth.cpp +++ b/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 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()); diff --git a/src/library/tactic/inversion_tactic.cpp b/src/library/tactic/inversion_tactic.cpp index 3c84eb6be..4292409ad 100644 --- a/src/library/tactic/inversion_tactic.cpp +++ b/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 { diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index 401a56a06..1a933dc84 100644 --- a/src/library/unifier.cpp +++ b/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;