From 46e60abda6105bba91a21dd7512c73387eb5ac4d Mon Sep 17 00:00:00 2001
From: Daniel Selsam <daniel.selsam@gmail.com>
Date: Mon, 23 Nov 2015 13:15:04 -0800
Subject: [PATCH] feat(library/blast/forward): branch extension

---
 src/CMakeLists.txt                            |  2 +
 src/library/blast/forward/CMakeLists.txt      |  1 +
 src/library/blast/forward/forward_actions.h   | 15 ++++
 .../blast/forward/forward_extension.cpp       | 72 +++++++++++++++++++
 src/library/blast/forward/forward_extension.h | 32 +++++++++
 src/library/blast/forward/init_module.cpp     | 19 +++++
 src/library/blast/forward/init_module.h       | 13 ++++
 src/library/blast/forward/qcf.cpp             | 26 +++++++
 src/library/blast/init_module.cpp             |  3 +
 src/library/blast/simple_strategy.cpp         |  2 +
 10 files changed, 185 insertions(+)
 create mode 100644 src/library/blast/forward/CMakeLists.txt
 create mode 100644 src/library/blast/forward/forward_actions.h
 create mode 100644 src/library/blast/forward/forward_extension.cpp
 create mode 100644 src/library/blast/forward/forward_extension.h
 create mode 100644 src/library/blast/forward/init_module.cpp
 create mode 100644 src/library/blast/forward/init_module.h
 create mode 100644 src/library/blast/forward/qcf.cpp

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index a0944f68f..de7f62391 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -351,6 +351,8 @@ add_subdirectory(library/blast/backward)
 set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:backward>)
 add_subdirectory(library/blast/unit)
 set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:unit>)
+add_subdirectory(library/blast/forward)
+set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:forward>)
 add_subdirectory(library/blast/simplifier)
 set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:simplifier>)
 add_subdirectory(library/error_handling)
diff --git a/src/library/blast/forward/CMakeLists.txt b/src/library/blast/forward/CMakeLists.txt
new file mode 100644
index 000000000..59b760ef0
--- /dev/null
+++ b/src/library/blast/forward/CMakeLists.txt
@@ -0,0 +1 @@
+add_library(forward OBJECT init_module.cpp forward_extension.cpp qcf.cpp)
diff --git a/src/library/blast/forward/forward_actions.h b/src/library/blast/forward/forward_actions.h
new file mode 100644
index 000000000..a00978757
--- /dev/null
+++ b/src/library/blast/forward/forward_actions.h
@@ -0,0 +1,15 @@
+/*
+Copyright (c) 2015 Daniel Selsam. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Daniel Selsam
+*/
+#pragma once
+#include "library/blast/action_result.h"
+#include "library/blast/gexpr.h"
+
+namespace lean {
+namespace blast {
+
+action_result qfc_action(list<gexpr> const & lemmas);
+
+}}
diff --git a/src/library/blast/forward/forward_extension.cpp b/src/library/blast/forward/forward_extension.cpp
new file mode 100644
index 000000000..bf05b60b9
--- /dev/null
+++ b/src/library/blast/forward/forward_extension.cpp
@@ -0,0 +1,72 @@
+/*
+Copyright (c) 2015 Daniel Selsam. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Daniel Selsam
+*/
+#include "library/blast/blast.h"
+#include "library/blast/forward/forward_extension.h"
+#include "library/blast/hypothesis.h"
+#include "library/blast/util.h"
+
+namespace lean {
+namespace blast {
+
+static unsigned g_ext_id = 0;
+static optional<head_index> to_head_index(expr type) {
+    // TODO(dhs): we will want to filter this set,
+    // because some constants are treated specially by this module
+    // (e.g. [eq] and [not])
+    expr const & f = get_app_fn(type);
+    if (is_constant(f) || is_local(f))
+        return optional<head_index>(head_index(f));
+    else
+        return optional<head_index>();
+}
+
+void forward_branch_extension::initialized() { }
+
+void forward_branch_extension::hypothesis_activated(hypothesis const & h, hypothesis_idx ) {
+    index_expr(h.get_type());
+}
+
+void forward_branch_extension::hypothesis_deleted(hypothesis const & , hypothesis_idx ) {
+    // TODO(dhs): remove from indices
+}
+
+void forward_branch_extension::index_expr(expr const & e) {
+    // TODO(dhs): index the target when it gets updated
+
+    if (auto head_idx = to_head_index(e)) {
+        m_index.insert(head_index(e), e);
+    }
+    switch (e.kind()) {
+    case expr_kind::Var:
+        lean_unreachable();  // LCOV_EXCL_LINE
+    case expr_kind::Local:
+    case expr_kind::Meta:
+    case expr_kind::Sort:
+    case expr_kind::Constant:
+    case expr_kind::Macro: // TODO(dhs): do I unfold macros?
+        break;
+    case expr_kind::Lambda:
+    case expr_kind::Pi:
+        // TODO(dhs): confirm that I only index quantified-free hypotheses
+        break;
+    case expr_kind::App:
+        index_expr(app_fn(e));
+        index_expr(app_arg(e));
+        break;
+    }
+}
+
+void initialize_forward_extension() {
+    g_ext_id = register_branch_extension(new forward_branch_extension());
+}
+
+void finalize_forward_extension() { }
+
+forward_branch_extension & get_extension() {
+    return static_cast<forward_branch_extension&>(curr_state().get_extension(g_ext_id));
+}
+
+}}
diff --git a/src/library/blast/forward/forward_extension.h b/src/library/blast/forward/forward_extension.h
new file mode 100644
index 000000000..c7dbe4c64
--- /dev/null
+++ b/src/library/blast/forward/forward_extension.h
@@ -0,0 +1,32 @@
+/*
+Copyright (c) 2015 Daniel Selsam. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Daniel Selsam
+*/
+#pragma once
+#include "library/blast/action_result.h"
+#include "library/blast/gexpr.h"
+#include "library/blast/blast.h"
+
+namespace lean {
+namespace blast {
+
+struct forward_branch_extension : public branch_extension {
+    head_map<expr> m_index;
+    forward_branch_extension() {}
+    forward_branch_extension(forward_branch_extension const & b): m_index(b.m_index) {}
+    virtual ~forward_branch_extension() {}
+    virtual branch_extension * clone() override { return new forward_branch_extension(*this); }
+    virtual void initialized() override;
+    virtual void hypothesis_activated(hypothesis const & h, hypothesis_idx hidx) override;
+    virtual void hypothesis_deleted(hypothesis const & , hypothesis_idx ) override;
+    void index_expr(expr const & e);
+public:
+    head_map<expr> const & get_index() { return m_index; }
+};
+
+forward_branch_extension & get_extension();
+
+void initialize_forward_extension();
+void finalize_forward_extension();
+}}
diff --git a/src/library/blast/forward/init_module.cpp b/src/library/blast/forward/init_module.cpp
new file mode 100644
index 000000000..25f2e7ac5
--- /dev/null
+++ b/src/library/blast/forward/init_module.cpp
@@ -0,0 +1,19 @@
+/*
+Copyright (c) 2015 Daniel Selsam. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Daniel Selsam
+*/
+#include "library/blast/forward/init_module.h"
+#include "library/blast/forward/forward_extension.h"
+
+namespace lean {
+namespace blast {
+
+void initialize_forward_module() {
+    initialize_forward_extension();
+}
+
+void finalize_forward_module() {
+    finalize_forward_extension();
+}
+}}
diff --git a/src/library/blast/forward/init_module.h b/src/library/blast/forward/init_module.h
new file mode 100644
index 000000000..e2ffd2bb9
--- /dev/null
+++ b/src/library/blast/forward/init_module.h
@@ -0,0 +1,13 @@
+/*
+Copyright (c) 2015 Daniel Selsam. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Daniel Selsam
+*/
+#pragma once
+
+namespace lean {
+namespace blast {
+void initialize_forward_module();
+void finalize_forward_module();
+}
+}
diff --git a/src/library/blast/forward/qcf.cpp b/src/library/blast/forward/qcf.cpp
new file mode 100644
index 000000000..b6cc0f430
--- /dev/null
+++ b/src/library/blast/forward/qcf.cpp
@@ -0,0 +1,26 @@
+/*
+Copyright (c) 2015 Daniel Selsam. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Daniel Selsam
+*/
+#include "kernel/instantiate.h"
+#include "kernel/abstract.h"
+#include "kernel/inductive/inductive.h"
+#include "library/blast/blast.h"
+#include "library/blast/action_result.h"
+#include "library/blast/forward/forward_actions.h"
+#include "library/blast/proof_expr.h"
+#include "library/blast/choice_point.h"
+#include "library/blast/hypothesis.h"
+#include "library/blast/util.h"
+#include "library/expr_lt.h"
+#include "library/head_map.h"
+
+namespace lean {
+namespace blast {
+
+action_result qfc_action(list<gexpr> const & lemmas) {
+    return action_result::failed();
+}
+
+}}
diff --git a/src/library/blast/init_module.cpp b/src/library/blast/init_module.cpp
index 9782eae40..47a9659d9 100644
--- a/src/library/blast/init_module.cpp
+++ b/src/library/blast/init_module.cpp
@@ -14,6 +14,7 @@ Author: Leonardo de Moura
 #include "library/blast/assert_cc_action.h"
 #include "library/blast/simplifier/init_module.h"
 #include "library/blast/backward/init_module.h"
+#include "library/blast/forward/init_module.h"
 #include "library/blast/unit/init_module.h"
 
 namespace lean {
@@ -24,6 +25,7 @@ void initialize_blast_module() {
     initialize_blast();
     blast::initialize_simplifier_module();
     blast::initialize_backward_module();
+    blast::initialize_forward_module();
     blast::initialize_unit_module();
     initialize_blast_tactic();
     blast::initialize_recursor_action();
@@ -36,6 +38,7 @@ void finalize_blast_module() {
     blast::finalize_recursor_action();
     finalize_blast_tactic();
     blast::finalize_unit_module();
+    blast::finalize_forward_module();
     blast::finalize_backward_module();
     blast::finalize_simplifier_module();
     finalize_blast();
diff --git a/src/library/blast/simple_strategy.cpp b/src/library/blast/simple_strategy.cpp
index 3bf550e9f..e0d9e2e0e 100644
--- a/src/library/blast/simple_strategy.cpp
+++ b/src/library/blast/simple_strategy.cpp
@@ -13,6 +13,7 @@ Author: Leonardo de Moura
 #include "library/blast/subst_action.h"
 #include "library/blast/backward/backward_action.h"
 #include "library/blast/backward/backward_strategy.h"
+#include "library/blast/forward/forward_actions.h"
 #include "library/blast/unit/unit_action.h"
 #include "library/blast/no_confusion_action.h"
 #include "library/blast/simplifier/simplifier_actions.h"
@@ -68,6 +69,7 @@ class simple_strategy : public strategy {
         Try(constructor_action());
 
         TryStrategy(apply_backward_strategy());
+        Try(qfc_action(list<gexpr>()));
 
         // TODO(Leo): add more actions...