From 1079d6b320c74ac1a3b34956d1c3ccef6f247522 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 11 Nov 2014 13:46:36 -0800
Subject: [PATCH] refactor(library/definitional): combine auxiliary functions
 used by definitional package in a single module

---
 src/frontends/lean/inductive_cmd.cpp    |  4 +--
 src/frontends/lean/structure_cmd.cpp    |  2 +-
 src/library/definitional/CMakeLists.txt |  2 +-
 src/library/definitional/eq.cpp         | 24 -------------
 src/library/definitional/eq.h           | 12 -------
 src/library/definitional/heq.cpp        | 27 ---------------
 src/library/definitional/heq.h          | 12 -------
 src/library/definitional/unit.cpp       | 21 ------------
 src/library/definitional/unit.h         | 11 ------
 src/library/definitional/util.cpp       | 45 +++++++++++++++++++++++++
 src/library/definitional/util.h         |  3 ++
 11 files changed, 51 insertions(+), 112 deletions(-)
 delete mode 100644 src/library/definitional/eq.cpp
 delete mode 100644 src/library/definitional/eq.h
 delete mode 100644 src/library/definitional/heq.cpp
 delete mode 100644 src/library/definitional/heq.h
 delete mode 100644 src/library/definitional/unit.cpp
 delete mode 100644 src/library/definitional/unit.h

diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp
index 995cf5458..4c56023a3 100644
--- a/src/frontends/lean/inductive_cmd.cpp
+++ b/src/frontends/lean/inductive_cmd.cpp
@@ -25,9 +25,7 @@ Author: Leonardo de Moura
 #include "library/definitional/induction_on.h"
 #include "library/definitional/cases_on.h"
 #include "library/definitional/no_confusion.h"
-#include "library/definitional/eq.h"
-#include "library/definitional/heq.h"
-#include "library/definitional/unit.h"
+#include "library/definitional/util.h"
 #include "frontends/lean/decl_cmds.h"
 #include "frontends/lean/util.h"
 #include "frontends/lean/class.h"
diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp
index f0bbd07ee..aad29c957 100644
--- a/src/frontends/lean/structure_cmd.cpp
+++ b/src/frontends/lean/structure_cmd.cpp
@@ -28,7 +28,7 @@ Author: Leonardo de Moura
 #include "library/definitional/rec_on.h"
 #include "library/definitional/induction_on.h"
 #include "library/definitional/cases_on.h"
-#include "library/definitional/eq.h"
+#include "library/definitional/util.h"
 #include "library/definitional/projection.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/util.h"
diff --git a/src/library/definitional/CMakeLists.txt b/src/library/definitional/CMakeLists.txt
index d0187d191..50e61c799 100644
--- a/src/library/definitional/CMakeLists.txt
+++ b/src/library/definitional/CMakeLists.txt
@@ -1,4 +1,4 @@
-add_library(definitional rec_on.cpp induction_on.cpp cases_on.cpp unit.cpp eq.cpp heq.cpp
+add_library(definitional rec_on.cpp induction_on.cpp cases_on.cpp
   no_confusion.cpp util.cpp projection.cpp)
 
 target_link_libraries(definitional ${LEAN_LIBS})
diff --git a/src/library/definitional/eq.cpp b/src/library/definitional/eq.cpp
deleted file mode 100644
index f4dc59802..000000000
--- a/src/library/definitional/eq.cpp
+++ /dev/null
@@ -1,24 +0,0 @@
-/*
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "kernel/environment.h"
-
-namespace lean {
-bool has_eq_decls(environment const & env) {
-    auto d = env.find(name({"eq", "refl"}));
-    if (!d)
-        return false;
-    if (length(d->get_univ_params()) != 1)
-        return false;
-    expr type = d->get_type();
-    if (!is_pi(type) || !is_pi(binding_body(type)))
-        return false;
-    type = get_app_fn(binding_body(binding_body(type)));
-    if (!is_constant(type))
-        return false;
-    return const_name(type) == "eq";
-}
-}
diff --git a/src/library/definitional/eq.h b/src/library/definitional/eq.h
deleted file mode 100644
index c1534c47c..000000000
--- a/src/library/definitional/eq.h
+++ /dev/null
@@ -1,12 +0,0 @@
-/*
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "kernel/environment.h"
-
-namespace lean {
-bool has_eq_decls(environment const & env);
-}
diff --git a/src/library/definitional/heq.cpp b/src/library/definitional/heq.cpp
deleted file mode 100644
index 7ba9b3d4e..000000000
--- a/src/library/definitional/heq.cpp
+++ /dev/null
@@ -1,27 +0,0 @@
-/*
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "kernel/environment.h"
-
-namespace lean {
-bool has_heq_decls(environment const & env) {
-    auto d = env.find(name({"heq", "refl"}));
-    if (!d)
-        return false;
-    if (length(d->get_univ_params()) != 1)
-        return false;
-    expr type = d->get_type();
-    for (unsigned i = 0; i < 2; i++) {
-        if (!is_pi(type))
-            return type;
-        type = binding_body(type);
-    }
-    type = get_app_fn(type);
-    if (!is_constant(type))
-        return false;
-    return const_name(type) == "heq";
-}
-}
diff --git a/src/library/definitional/heq.h b/src/library/definitional/heq.h
deleted file mode 100644
index fe3fa8302..000000000
--- a/src/library/definitional/heq.h
+++ /dev/null
@@ -1,12 +0,0 @@
-/*
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "kernel/environment.h"
-
-namespace lean {
-bool has_heq_decls(environment const & env);
-}
diff --git a/src/library/definitional/unit.cpp b/src/library/definitional/unit.cpp
deleted file mode 100644
index a42cbf310..000000000
--- a/src/library/definitional/unit.cpp
+++ /dev/null
@@ -1,21 +0,0 @@
-/*
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "kernel/environment.h"
-
-namespace lean {
-bool has_unit_decls(environment const & env) {
-    auto d = env.find(name({"unit", "star"}));
-    if (!d)
-        return false;
-    if (length(d->get_univ_params()) != 1)
-        return false;
-    expr const & type = d->get_type();
-    if (!is_constant(type))
-        return false;
-    return const_name(type) == "unit";
-}
-}
diff --git a/src/library/definitional/unit.h b/src/library/definitional/unit.h
deleted file mode 100644
index 3e36381df..000000000
--- a/src/library/definitional/unit.h
+++ /dev/null
@@ -1,11 +0,0 @@
-/*
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "kernel/environment.h"
-namespace lean {
-bool has_unit_decls(environment const & env);
-}
diff --git a/src/library/definitional/util.cpp b/src/library/definitional/util.cpp
index 48b963398..b8721ec9a 100644
--- a/src/library/definitional/util.cpp
+++ b/src/library/definitional/util.cpp
@@ -8,6 +8,51 @@ Author: Leonardo de Moura
 #include "kernel/inductive/inductive.h"
 
 namespace lean {
+bool has_unit_decls(environment const & env) {
+    auto d = env.find(name({"unit", "star"}));
+    if (!d)
+        return false;
+    if (length(d->get_univ_params()) != 1)
+        return false;
+    expr const & type = d->get_type();
+    if (!is_constant(type))
+        return false;
+    return const_name(type) == "unit";
+}
+
+bool has_eq_decls(environment const & env) {
+    auto d = env.find(name({"eq", "refl"}));
+    if (!d)
+        return false;
+    if (length(d->get_univ_params()) != 1)
+        return false;
+    expr type = d->get_type();
+    if (!is_pi(type) || !is_pi(binding_body(type)))
+        return false;
+    type = get_app_fn(binding_body(binding_body(type)));
+    if (!is_constant(type))
+        return false;
+    return const_name(type) == "eq";
+}
+
+bool has_heq_decls(environment const & env) {
+    auto d = env.find(name({"heq", "refl"}));
+    if (!d)
+        return false;
+    if (length(d->get_univ_params()) != 1)
+        return false;
+    expr type = d->get_type();
+    for (unsigned i = 0; i < 2; i++) {
+        if (!is_pi(type))
+            return type;
+        type = binding_body(type);
+    }
+    type = get_app_fn(type);
+    if (!is_constant(type))
+        return false;
+    return const_name(type) == "heq";
+}
+
 bool is_recursive_datatype(environment const & env, name const & n) {
     optional<inductive::inductive_decls> decls = inductive::is_inductive_decl(env, n);
     if (!decls)
diff --git a/src/library/definitional/util.h b/src/library/definitional/util.h
index 3d6100d02..f276907eb 100644
--- a/src/library/definitional/util.h
+++ b/src/library/definitional/util.h
@@ -8,6 +8,9 @@ Author: Leonardo de Moura
 #include "kernel/environment.h"
 
 namespace lean {
+bool has_unit_decls(environment const & env);
+bool has_eq_decls(environment const & env);
+bool has_heq_decls(environment const & env);
 /** \brief Return true iff \c n is the name of a recursive datatype in \c env.
     That is, it must be an inductive datatype AND contain a recursive constructor.