From a53098385c682ce9d56311ea847ae05bd99a756a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 21 Jan 2015 17:22:41 -0800
Subject: [PATCH] refactor(frontends/lean/type_util): move
 infer_implicit_params to library

---
 src/frontends/lean/type_util.cpp | 16 ----------------
 src/frontends/lean/type_util.h   |  7 +------
 src/library/util.cpp             | 16 ++++++++++++++++
 src/library/util.h               |  7 +++++++
 4 files changed, 24 insertions(+), 22 deletions(-)

diff --git a/src/frontends/lean/type_util.cpp b/src/frontends/lean/type_util.cpp
index b8b87e76a..bd3f377d1 100644
--- a/src/frontends/lean/type_util.cpp
+++ b/src/frontends/lean/type_util.cpp
@@ -51,20 +51,4 @@ implicit_infer_kind parse_implicit_infer_modifier(parser & p) {
         return implicit_infer_kind::Implicit;
     }
 }
-
-expr infer_implicit_params(expr const & type, unsigned nparams, implicit_infer_kind k) {
-    switch (k) {
-    case implicit_infer_kind::Implicit: {
-        bool strict = true;
-        return infer_implicit(type, nparams, strict);
-    }
-    case implicit_infer_kind::RelaxedImplicit: {
-        bool strict = false;
-        return infer_implicit(type, nparams, strict);
-    }
-    case implicit_infer_kind::None:
-        return type;
-    }
-    lean_unreachable(); // LCOV_EXCL_LINE
-}
 }
diff --git a/src/frontends/lean/type_util.h b/src/frontends/lean/type_util.h
index d5afd1e45..e4d1ef3a2 100644
--- a/src/frontends/lean/type_util.h
+++ b/src/frontends/lean/type_util.h
@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include "library/util.h"
 
 namespace lean {
 class parser;
@@ -35,7 +36,6 @@ public:
 environment add_alias(parser & p, environment env, bool composite,
                       name const & full_id, levels const & ctx_levels, buffer<expr> const & ctx_params);
 
-enum class implicit_infer_kind { Implicit, RelaxedImplicit, None };
 /**
    \brief Parse implicit parameter inference modifiers.
 
@@ -44,9 +44,4 @@ enum class implicit_infer_kind { Implicit, RelaxedImplicit, None };
     Return implicit_infer_kind::Implicit, otherwise.
 */
 implicit_infer_kind parse_implicit_infer_modifier(parser & p);
-
-/** \brief Infer implicit parameter annotations for the first \c nparams using mode
-    specified by \c k.
-*/
-expr infer_implicit_params(expr const & type, unsigned nparams, implicit_infer_kind k);
 }
diff --git a/src/library/util.cpp b/src/library/util.cpp
index 59432134e..ac132a070 100644
--- a/src/library/util.cpp
+++ b/src/library/util.cpp
@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "kernel/type_checker.h"
 #include "kernel/inductive/inductive.h"
 #include "library/locals.h"
+#include "library/util.h"
 
 namespace lean {
 bool is_def_app(environment const & env, expr const & e) {
@@ -504,4 +505,19 @@ expr mk_sigma_mk(type_checker & tc, buffer<expr> const & ts, buffer<expr> const
     return mk_sigma_mk(tc, ts.size(), ts.data(), as.data(), cs);
 }
 
+expr infer_implicit_params(expr const & type, unsigned nparams, implicit_infer_kind k) {
+    switch (k) {
+    case implicit_infer_kind::Implicit: {
+        bool strict = true;
+        return infer_implicit(type, nparams, strict);
+    }
+    case implicit_infer_kind::RelaxedImplicit: {
+        bool strict = false;
+        return infer_implicit(type, nparams, strict);
+    }
+    case implicit_infer_kind::None:
+        return type;
+    }
+    lean_unreachable(); // LCOV_EXCL_LINE
+}
 }
diff --git a/src/library/util.h b/src/library/util.h
index 79576e82f..7be0d0941 100644
--- a/src/library/util.h
+++ b/src/library/util.h
@@ -132,6 +132,13 @@ level mk_max(levels const & ls);
 
 expr mk_sigma_mk(type_checker & tc, buffer<expr> const & ts, buffer<expr> const & as, constraint_seq & cs);
 
+enum class implicit_infer_kind { Implicit, RelaxedImplicit, None };
+
+/** \brief Infer implicit parameter annotations for the first \c nparams using mode
+    specified by \c k.
+*/
+expr infer_implicit_params(expr const & type, unsigned nparams, implicit_infer_kind k);
+
 void initialize_library_util();
 void finalize_library_util();
 }