max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library,frontends/lean): use is_constructor, is_recursor, is_inductive helper functions

Browse source 
They do not throw exception if the constant is not declared in the environment.
This commit is contained in:
Leonardo de Moura 2018-09-07 20:36:42 -07:00
parent 88d4a1b0cd
commit 13fbd8304e
8 changed files with 11 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/frontends/lean/elaborator.cpp
View file

@ -106,7 +106,7 @@ elaborator_strategy get_elaborator_strategy(environment const & env, name const
if (auto data = get_elaborator_strategy_attribute().get(env, n))
return data->m_status;
if (env.get(n).is_recursor() ||
if (is_recursor(env, n) ||
is_aux_recursor(env, n) ||
is_user_defined_recursor(env, n)) {
return elaborator_strategy::AsEliminator;
@ -395,7 +395,7 @@ static bool is_basic_aux_recursor(environment const & env, name const & n) {
/** See comment at elim_info */
auto elaborator::get_elim_info_for_builtin(name const & fn) -> elim_info {
lean_assert(is_basic_aux_recursor(m_env, fn) || m_env.get(fn).is_recursor());
lean_assert(is_basic_aux_recursor(m_env, fn) || is_recursor(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());
@ -440,7 +440,7 @@ auto elaborator::get_elim_info_for_builtin(name const & fn) -> 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_basic_aux_recursor(m_env, fn) || m_env.get(fn).is_recursor()) {
if (is_basic_aux_recursor(m_env, fn) || is_recursor(m_env, fn)) {
return optional<elim_info>(get_elim_info_for_builtin(fn));
}
type_context_old::tmp_locals locals(m_ctx);

2
src/frontends/lean/parser.cpp
View file

@ -1385,7 +1385,7 @@ struct to_pattern_fn {
/* Return true iff the constant n may occur in a pattern */
bool is_pattern_constant(name const & n) {
if (env().get(n).is_constructor())
if (is_constructor(env(), n))
return true;
if (has_pattern_attribute(env(), n))
return true;

2
src/library/equations_compiler/elim_match.cpp
View file

@ -275,7 +275,7 @@ struct elim_match_fn {
return optional<name>();
}
bool is_inductive(name const & n) const { return m_env.get(n).is_inductive(); }
bool is_inductive(name const & n) const { return ::lean::is_inductive(m_env, n); }
bool is_inductive(expr const & e) const { return is_constant(e) && is_inductive(const_name(e)); }
bool is_inductive_app(expr const & e) const { return is_inductive(get_app_fn(e)); }

4
src/library/equations_compiler/structural_rec.cpp
View file

@ -75,7 +75,7 @@ struct structural_rec_fn {
m_ctx(ctx), m_lhs(lhs), m_fn(fn), m_pattern(pattern), m_arg_idx(arg_idx) {}
bool is_constructor(expr const & e) const {
return is_constant(e) && m_ctx.env().get(const_name(e)).is_constructor();
return is_constant(e) && ::lean::is_constructor(m_ctx.env(), const_name(e));
}
expr whnf(expr const & e) {
@ -220,7 +220,7 @@ struct structural_rec_fn {
expr arg_type = ctx.relaxed_whnf(binding_domain(fn_type));
buffer<expr> I_args;
expr I = get_app_args(arg_type, I_args);
if (!is_constant(I) || !m_env.get(const_name(I)).is_inductive()) {
if (!is_constant(I) || !is_inductive(m_env, const_name(I))) {
trace_struct(tout() << "structural recursion on argument #" << (arg_idx+1) << " was not used "
<< "for '" << fn << "' because type is not inductive\n "
<< arg_type << "\n";);

2
src/library/equations_compiler/util.cpp
View file

@ -322,7 +322,7 @@ bool is_nat_int_char_string_name_value(type_context_old & ctx, expr const & e) {
}
static bool is_inductive(environment const & env, expr const & e) {
return is_constant(e) && env.get(const_name(e)).is_inductive();
return is_constant(e) && is_inductive(env, const_name(e));
}
/* Normalize until head is an inductive datatype */

2
src/library/tactic/cases_tactic.cpp
View file

@ -102,7 +102,7 @@ struct cases_tactic_fn {
expr const & fn = get_app_args(t, args);
if (!is_constant(fn))
return false;
if (!m_env.get(const_name(fn)).is_inductive())
if (!is_inductive(m_env, const_name(fn)))
return false;
if (!m_env.find(name{const_name(fn), "cases_on"}) || !m_env.find(get_eq_name()))
return false;

2
src/library/user_recursors.cpp
View file

@ -333,7 +333,7 @@ typedef scoped_ext<recursor_config> recursor_ext;
environment add_user_recursor(environment const & env, name const & r, optional<unsigned> const & major_pos,
bool persistent) {
if (env.get(r).is_recursor())
if (is_recursor(env, r))
throw exception(sstream() << "invalid user defined recursor, '" << r << "' is a builtin recursor");
recursor_info info = mk_recursor_info(env, r, major_pos);
return recursor_ext::add_entry(env, get_dummy_ios(), info, persistent);

2
src/library/util.cpp
View file

@ -247,7 +247,7 @@ void get_constructor_names(environment const & env, name const & n, buffer<name>
optional<name> is_constructor_app(environment const & env, expr const & e) {
expr const & fn = get_app_fn(e);
if (is_constant(fn)) {
if (env.get(const_name(fn)).is_constructor())
if (is_constructor(env, const_name(fn)))
return optional<name>(const_name(fn));
}
return optional<name>();