From c7b4e00bbfd152f12de361f3b168b22833342811 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 7 May 2016 18:19:19 -0700
Subject: [PATCH] refactor(compiler): move is_comp_irrelevant predicate to util

---
 src/compiler/comp_irrelevant.cpp | 6 +-----
 src/compiler/util.cpp            | 6 ++++++
 src/compiler/util.h              | 7 +++++--
 3 files changed, 12 insertions(+), 7 deletions(-)

diff --git a/src/compiler/comp_irrelevant.cpp b/src/compiler/comp_irrelevant.cpp
index 13e4989c81..9f5f9a34bb 100644
--- a/src/compiler/comp_irrelevant.cpp
+++ b/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) {
diff --git a/src/compiler/util.cpp b/src/compiler/util.cpp
index ae9a0df193..d6915e3107 100644
--- a/src/compiler/util.cpp
+++ b/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))
diff --git a/src/compiler/util.h b/src/compiler/util.h
index 760020c235..b2867f3cf3 100644
--- a/src/compiler/util.h
+++ b/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);