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

@@ -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);
     }
 

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<bool>(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<expr> 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  "

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<bool>(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<name> eqns_env_interface::is_constructor(name const & n) const {
-    return inductive::is_intro_rule(m_env, n);
-}
-
-optional<name> eqns_env_interface::is_constructor(expr const & e) const {
-    if (!is_constant(e)) return optional<name>();
-    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<name> & 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++) {

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<name> is_constructor(name const & n) const;
-    optional<name> 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<name> & 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. */