refactor(library/blast/forward): make sure backward and forward modules use same naming convention

src/frontends/lean/print_cmd.cpp

@@ -30,7 +30,7 @@ Author: Leonardo de Moura
 #include "library/blast/blast.h"
 #include "library/blast/simplifier/simplifier.h"
 #include "library/blast/backward/backward_lemmas.h"
-#include "library/blast/forward/forward_lemma_set.h"
+#include "library/blast/forward/forward_lemmas.h"
 #include "library/blast/forward/pattern.h"
 #include "library/blast/grinder/intro_elim_lemmas.h"
 #include "frontends/lean/parser.h"

src/library/blast/forward/CMakeLists.txt

@@ -1,2 +1,2 @@
 add_library(forward OBJECT init_module.cpp forward_extension.cpp qcf.cpp pattern.cpp
-  ematch.cpp forward_lemma_set.cpp)
+  ematch.cpp forward_lemmas.cpp)

src/library/blast/forward/ematch.cpp

@@ -14,7 +14,7 @@ Author: Leonardo de Moura
 #include "library/blast/options.h"
 #include "library/blast/congruence_closure.h"
 #include "library/blast/forward/pattern.h"
-#include "library/blast/forward/forward_lemma_set.h"
+#include "library/blast/forward/forward_lemmas.h"
 
 namespace lean {
 namespace blast {
@@ -97,7 +97,7 @@ struct ematch_branch_extension : public branch_extension {
     virtual ~ematch_branch_extension() {}
     virtual branch_extension * clone() override { return new ematch_branch_extension(*this); }
     virtual void initialized() override {
-        forward_lemma_set s = get_forward_lemma_set(env());
+        forward_lemmas s = get_forward_lemmas(env());
         s.for_each([&](name const & n, unsigned prio) {
                 try {
                     m_new_lemmas.insert(mk_hi_lemma(n, prio));

src/library/blast/forward/forward_lemmas.cpp

@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 #include <string>
 #include "library/scoped_ext.h"
 #include "library/attribute_manager.h"
-#include "library/blast/forward/forward_lemma_set.h"
+#include "library/blast/forward/forward_lemmas.h"
 #include "library/blast/forward/pattern.h"
 
 namespace lean {
@@ -21,9 +21,9 @@ struct forward_lemma {
     forward_lemma(name const & n, unsigned p):m_name(n), m_priority(p) {}
 };
 
-struct forward_lemma_set_config {
-    typedef forward_lemma     entry;
-    typedef forward_lemma_set state;
+struct forward_lemmas_config {
+    typedef forward_lemma  entry;
+    typedef forward_lemmas state;
 
     static void add_entry(environment const &, io_state const &, state & s, entry const & e) {
         s.insert(e.m_name, e.m_priority);
@@ -52,25 +52,25 @@ struct forward_lemma_set_config {
     }
 };
 
-template class scoped_ext<forward_lemma_set_config>;
-typedef scoped_ext<forward_lemma_set_config> forward_lemma_set_ext;
+template class scoped_ext<forward_lemmas_config>;
+typedef scoped_ext<forward_lemmas_config> forward_lemmas_ext;
 
 environment add_forward_lemma(environment const & env, name const & n, unsigned priority, name const & ns, bool persistent) {
-    return forward_lemma_set_ext::add_entry(env, get_dummy_ios(), forward_lemma(n, priority), ns, persistent);
+    return forward_lemmas_ext::add_entry(env, get_dummy_ios(), forward_lemma(n, priority), ns, persistent);
 }
 
 bool is_forward_lemma(environment const & env, name const & n) {
-    return forward_lemma_set_ext::get_state(env).contains(n);
+    return forward_lemmas_ext::get_state(env).contains(n);
 }
 
-forward_lemma_set get_forward_lemma_set(environment const & env) {
-    return forward_lemma_set_ext::get_state(env);
+forward_lemmas get_forward_lemmas(environment const & env) {
+    return forward_lemmas_ext::get_state(env);
 }
 
-void initialize_forward_lemma_set() {
+void initialize_forward_lemmas() {
     g_name              = new name("forward");
     g_key               = new std::string("FWD");
-    forward_lemma_set_ext::initialize();
+    forward_lemmas_ext::initialize();
 
     register_prio_attribute("forward", "forward chaining",
                             [](environment const & env, io_state const & ios, name const & d, unsigned prio, name const & ns, bool persistent) {
@@ -79,15 +79,15 @@ void initialize_forward_lemma_set() {
                             },
                             is_forward_lemma,
                             [](environment const & env, name const & n) {
-                                if (auto prio = get_forward_lemma_set(env).find(n))
+                                if (auto prio = get_forward_lemmas(env).find(n))
                                     return *prio;
                                 else
                                     return LEAN_DEFAULT_PRIORITY;
                             });
 }
 
-void finalize_forward_lemma_set() {
-    forward_lemma_set_ext::finalize();
+void finalize_forward_lemmas() {
+    forward_lemmas_ext::finalize();
     delete g_name;
     delete g_key;
 }

src/library/blast/forward/forward_lemmas.h

@@ -10,12 +10,12 @@ Author: Leonardo de Moura
 
 namespace lean {
 /** \brief The forward lemma set is actually a mapping from lemma name to priority */
-typedef rb_map<name, unsigned, name_quick_cmp> forward_lemma_set;
+typedef rb_map<name, unsigned, name_quick_cmp> forward_lemmas;
 
 environment add_forward_lemma(environment const & env, name const & n, unsigned priority, name const & ns, bool persistent);
 bool is_forward_lemma(environment const & env, name const & n);
-forward_lemma_set get_forward_lemma_set(environment const & env);
+forward_lemmas get_forward_lemmas(environment const & env);
 
-void initialize_forward_lemma_set();
-void finalize_forward_lemma_set();
+void initialize_forward_lemmas();
+void finalize_forward_lemmas();
 }

src/library/blast/forward/init_module.cpp

@@ -5,7 +5,7 @@ Author: Daniel Selsam
 */
 #include "library/blast/forward/init_module.h"
 #include "library/blast/forward/forward_extension.h"
-#include "library/blast/forward/forward_lemma_set.h"
+#include "library/blast/forward/forward_lemmas.h"
 #include "library/blast/forward/pattern.h"
 #include "library/blast/forward/ematch.h"
 
@@ -15,13 +15,13 @@ namespace blast {
 void initialize_forward_module() {
     initialize_forward_extension();
     initialize_pattern();
-    initialize_forward_lemma_set();
+    initialize_forward_lemmas();
     initialize_ematch();
 }
 
 void finalize_forward_module() {
     finalize_ematch();
-    finalize_forward_lemma_set();
+    finalize_forward_lemmas();
     finalize_pattern();
     finalize_forward_extension();
 }

src/library/blast/forward/pattern.cpp

@@ -23,7 +23,7 @@ Author: Leonardo de Moura
 #include "library/blast/options.h"
 #include "library/blast/blast.h"
 #include "library/blast/forward/pattern.h"
-#include "library/blast/forward/forward_lemma_set.h"
+#include "library/blast/forward/forward_lemmas.h"
 
 namespace lean {
 /*