refactor(compiler): move is_comp_irrelevant predicate to util

src/compiler/comp_irrelevant.cpp

@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "library/annotation.h"
+#include "compiler/util.h"
 #include "compiler/compiler_step_visitor.h"
 
 namespace lean {
@@ -18,11 +19,6 @@ bool is_marked_as_comp_irrelevant(expr const & e) {
     return is_annotation(e, *g_comp_irrel);
 }
 
-bool is_comp_irrelevant(type_context & ctx, expr const & e) {
-    expr type = ctx.whnf(ctx.infer(e));
-    return is_sort(type) || ctx.is_prop(type);
-}
-
 class mark_comp_irrelevant_fn : public compiler_step_visitor {
 protected:
     optional<expr> mark_if_irrel_core(expr const & e) {

src/compiler/util.cpp

@@ -10,8 +10,14 @@ Author: Leonardo de Moura
 #include "kernel/inductive/inductive.h"
 #include "library/aux_recursors.h"
 #include "library/util.h"
+#include "library/type_context.h"
 
 namespace lean {
+bool is_comp_irrelevant(type_context & ctx, expr const & e) {
+    expr type = ctx.whnf(ctx.infer(e));
+    return is_sort(type) || ctx.is_prop(type);
+}
+
 static bool is_typeformer_app(buffer<name> const & typeformer_names, expr const & e) {
     expr const & fn = get_app_fn(e);
     if (!is_local(fn))

src/compiler/util.h

@@ -7,11 +7,14 @@ Author: Leonardo de Moura
 #pragma once
 #include "kernel/environment.h"
 namespace lean {
+class type_context;
+/** \brief Return true iff \c e is computationally irrelevant */
+bool is_comp_irrelevant(type_context & ctx, expr const & e);
+
 /** \brief Given an inductive datatype \c n, store in \c r a "bitvector" s.t.
     r[i][j] is true iff the j-th argument of the i-th minor premise of the recursor \c n.rec
     is a recursive argument.
-    \pre inductive::is_inductive_decl(env, n)
-*/
+    \pre inductive::is_inductive_decl(env, n) */
 void get_rec_args(environment const & env, name const & n, buffer<buffer<bool>> & r);
 
 unsigned get_constructor_arity(environment const & env, name const & n);