refactor(library/definitional): combine auxiliary functions used by definitional package in a single module

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"

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"

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

src/library/definitional/eq.cpp

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

src/library/definitional/eq.h

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

src/library/definitional/heq.cpp

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

src/library/definitional/heq.h

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

src/library/definitional/unit.cpp

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

src/library/definitional/unit.h

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

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)

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.