From b08af16d5fbdc65fc2ca629d54b22311a81ea06d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 29 Aug 2016 09:25:01 -0700 Subject: [PATCH] refactor(library/equations_compiler): remove unnecessary abstraction We changed how we are going to process derived inductive datatypes. --- src/library/equations_compiler/elim_match.cpp | 2 +- .../equations_compiler/structural_rec.cpp | 9 ++--- src/library/equations_compiler/util.cpp | 33 ------------------- src/library/equations_compiler/util.h | 21 ------------ 4 files changed, 6 insertions(+), 59 deletions(-) diff --git a/src/library/equations_compiler/elim_match.cpp b/src/library/equations_compiler/elim_match.cpp index 091376a25c..2e3fd260ad 100644 --- a/src/library/equations_compiler/elim_match.cpp +++ b/src/library/equations_compiler/elim_match.cpp @@ -215,7 +215,7 @@ struct elim_match_fn { That is, the fixed parameters used in the inductive declaration. */ unsigned get_constructor_num_params(expr const & n) const { lean_assert(is_constructor(n)); - name I_name = *eqns_env_interface(m_env).is_constructor(n); + name I_name = *inductive::is_intro_rule(m_env, const_name(n)); return get_inductive_num_params(I_name); } diff --git a/src/library/equations_compiler/structural_rec.cpp b/src/library/equations_compiler/structural_rec.cpp index e553c99f7f..98fa8039ae 100644 --- a/src/library/equations_compiler/structural_rec.cpp +++ b/src/library/equations_compiler/structural_rec.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "kernel/instantiate.h" +#include "kernel/inductive/inductive.h" #include "library/trace.h" #include "library/constants.h" #include "library/locals.h" @@ -34,7 +35,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 static_cast(eqns_env_interface(m_ctx).is_constructor(e)); + return is_constant(e) && inductive::is_intro_rule(m_ctx.env(), const_name(e)); } /** \brief Return true iff \c s is structurally smaller than \c t OR equal to \c t */ @@ -156,10 +157,10 @@ struct structural_rec_fn { fn_type = instantiate(binding_body(fn_type), locals.push_local_from_binding(fn_type)); } if (!is_pi(fn_type)) throw_ill_formed_eqns(); - expr arg_type = binding_domain(fn_type); + expr arg_type = m_ctx.relaxed_whnf(binding_domain(fn_type)); buffer I_args; expr I = get_app_args(arg_type, I_args); - if (!eqns_env_interface(m_ctx).is_inductive(I)) { + if (is_constant(I) && !inductive::is_inductive_decl(m_ctx.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";); @@ -171,7 +172,7 @@ struct structural_rec_fn { << arg_type << "\n";); return false; } - unsigned nindices = eqns_env_interface(m_ctx).get_inductive_num_indices(const_name(I)); + unsigned nindices = *inductive::get_num_indices(m_ctx.env(), const_name(I)); if (nindices > 0) { trace_struct(tout() << "structural recursion on argument #" << (arg_idx+1) << " was not used " << "for '" << fn << "' because the inductive type '" << I << "' is an indexed family\n " diff --git a/src/library/equations_compiler/util.cpp b/src/library/equations_compiler/util.cpp index fbbd5adcec..6a853af457 100644 --- a/src/library/equations_compiler/util.cpp +++ b/src/library/equations_compiler/util.cpp @@ -144,39 +144,6 @@ expr unpack_eqn::repack() { return copy_tag(m_src, m_locals.ctx().mk_lambda(m_vars, new_eq)); } -bool eqns_env_interface::is_inductive(name const & n) const { - return static_cast(inductive::is_inductive_decl(m_env, n)); -} - -bool eqns_env_interface::is_inductive(expr const & e) const { - if (!is_constant(e)) return false; - return is_inductive(const_name(e)); -} - -optional eqns_env_interface::is_constructor(name const & n) const { - return inductive::is_intro_rule(m_env, n); -} - -optional eqns_env_interface::is_constructor(expr const & e) const { - if (!is_constant(e)) return optional(); - return is_constructor(const_name(e)); -} - -unsigned eqns_env_interface::get_inductive_num_params(name const & n) const { - lean_assert(is_inductive(n)); - return *inductive::get_num_params(m_env, n); -} - -unsigned eqns_env_interface::get_inductive_num_indices(name const & n) const { - lean_assert(is_inductive(n)); - return *inductive::get_num_indices(m_env, n); -} - -void eqns_env_interface::get_constructors_of(name const & n, buffer & c_names) const { - lean_assert(is_inductive(n)); - get_intro_rule_names(m_env, n, c_names); -} - bool is_recursive_eqns(type_context & ctx, expr const & e) { unpack_eqns ues(ctx, e); for (unsigned fidx = 0; fidx < ues.get_num_fns(); fidx++) { diff --git a/src/library/equations_compiler/util.h b/src/library/equations_compiler/util.h index 65f9374098..165c78e3fa 100644 --- a/src/library/equations_compiler/util.h +++ b/src/library/equations_compiler/util.h @@ -67,27 +67,6 @@ public: expr repack(); }; -/** \brief Interface object for providing extra functionality - required by the equation compiler from the environment. - - For example, it abstracts the inductive datatype API. - So, if we add new forms of inductive datatype, we need - to change this class. */ -class eqns_env_interface { - environment m_env; -public: - eqns_env_interface(environment const & env):m_env(env) {} - eqns_env_interface(type_context const & ctx):m_env(ctx.env()) {} - - bool is_inductive(name const & n) const; - bool is_inductive(expr const & e) const; - optional is_constructor(name const & n) const; - optional is_constructor(expr const & e) const; - unsigned get_inductive_num_params(name const & n) const; - unsigned get_inductive_num_indices(name const & n) const; - void get_constructors_of(name const & n, buffer & c_names) const; -}; - /** \brief Return true iff \c e is recursive. That is, some equation in the rhs has a reference to a function being defined by the equations. */