From cc4608a392d207684459a9e51d686f14a5c70049 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 13 Nov 2015 14:03:43 -0800
Subject: [PATCH] feat(library/blast): add "revert" auxiliary action

---
 src/library/blast/CMakeLists.txt |  2 +-
 src/library/blast/revert.cpp     | 48 ++++++++++++++++++++++++++++++++
 src/library/blast/revert.h       | 15 ++++++++++
 src/library/blast/state.cpp      |  9 ++++++
 src/library/blast/state.h        |  7 ++++-
 5 files changed, 79 insertions(+), 2 deletions(-)
 create mode 100644 src/library/blast/revert.cpp
 create mode 100644 src/library/blast/revert.h

diff --git a/src/library/blast/CMakeLists.txt b/src/library/blast/CMakeLists.txt
index 79e80259c..11ad170ad 100644
--- a/src/library/blast/CMakeLists.txt
+++ b/src/library/blast/CMakeLists.txt
@@ -1,4 +1,4 @@
 add_library(blast OBJECT expr.cpp state.cpp blast.cpp blast_tactic.cpp
   init_module.cpp simplifier.cpp simple_actions.cpp intros.cpp proof_expr.cpp
   options.cpp choice_point.cpp simple_strategy.cpp backward.cpp util.cpp
-  gexpr.cpp)
+  gexpr.cpp revert.cpp)
diff --git a/src/library/blast/revert.cpp b/src/library/blast/revert.cpp
new file mode 100644
index 000000000..936440980
--- /dev/null
+++ b/src/library/blast/revert.cpp
@@ -0,0 +1,48 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "library/blast/revert.h"
+#include "library/blast/blast.h"
+
+namespace lean {
+namespace blast {
+struct revert_proof_step_cell : public proof_step_cell {
+    list<expr> m_hs;
+    revert_proof_step_cell(list<expr> const & hs):m_hs(hs) {}
+
+    virtual ~revert_proof_step_cell() {}
+
+    virtual action_result resolve(expr const & pr) const {
+        expr new_pr = mk_app(pr, m_hs);
+        return action_result::solved(new_pr);
+    }
+
+    virtual bool is_silent() const override { return true; }
+};
+
+unsigned revert(buffer<hypothesis_idx> & hidxs, hypothesis_idx_set & hidxs_set) {
+    lean_assert(hidxs.size() == hidxs_set.size());
+    state & s = curr_state();
+    unsigned hidxs_size = hidxs.size();
+    for (unsigned i = 0; i < hidxs_size; i++) {
+        s.collect_forward_deps(hidxs[i], hidxs, hidxs_set);
+    }
+    s.sort_hypotheses(hidxs);
+    buffer<expr> hs;
+    s.to_hrefs(hidxs, hs);
+    expr target     = s.get_target();
+    expr new_target = s.mk_pi(hs, target);
+    s.set_target(new_target);
+    s.push_proof_step(new revert_proof_step_cell(to_list(hs)));
+    lean_verify(s.del_hypotheses(hidxs));
+    return hidxs.size();
+}
+
+unsigned revert(buffer<hypothesis_idx> & hidxs) {
+    hypothesis_idx_set hidxs_set(hidxs);
+    return revert(hidxs, hidxs_set);
+}
+}}
diff --git a/src/library/blast/revert.h b/src/library/blast/revert.h
new file mode 100644
index 000000000..e55e540b1
--- /dev/null
+++ b/src/library/blast/revert.h
@@ -0,0 +1,15 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "library/blast/hypothesis.h"
+
+namespace lean {
+namespace blast {
+/** \brief Revert the given hypotheses and their dependencies.
+    Return the total number of hypotheses reverted. */
+unsigned revert(buffer<hypothesis_idx> & hidxs);
+}}
diff --git a/src/library/blast/state.cpp b/src/library/blast/state.cpp
index 2b2427c0a..15f9f4d44 100644
--- a/src/library/blast/state.cpp
+++ b/src/library/blast/state.cpp
@@ -356,9 +356,18 @@ void state::get_sorted_hypotheses(hypothesis_idx_buffer & r) const {
             if (!h.is_dead())
                 r.push_back(hidx);
         });
+    sort_hypotheses(r);
+}
+
+void state::sort_hypotheses(hypothesis_idx_buffer & r) const {
     std::sort(r.begin(), r.end(), hypothesis_dep_depth_lt(*this));
 }
 
+void state::to_hrefs(hypothesis_idx_buffer const & hidxs, buffer<expr> & r) const {
+    for (hypothesis_idx hidx : hidxs)
+        r.push_back(get_hypothesis_decl(hidx)->get_self());
+}
+
 void state::add_forward_dep(unsigned hidx_user, unsigned hidx_provider) {
     if (auto s = m_branch.m_forward_deps.find(hidx_provider)) {
         if (!s->contains(hidx_user)) {
diff --git a/src/library/blast/state.h b/src/library/blast/state.h
index 92a76726f..f479a93b3 100644
--- a/src/library/blast/state.h
+++ b/src/library/blast/state.h
@@ -168,7 +168,6 @@ class state {
     void remove_from_indices(hypothesis const & h, hypothesis_idx hidx);
 
     void del_hypotheses(buffer<hypothesis_idx> const & to_delete, hypothesis_idx_set const & to_delete_set);
-    void collect_forward_deps(hypothesis_idx hidx, buffer<hypothesis_idx> & result, hypothesis_idx_set & already_found);
     bool safe_to_delete(buffer<hypothesis_idx> const & to_delete);
 
     void display_active(output_channel & out) const;
@@ -222,6 +221,7 @@ public:
 
     /** \brief Collect all hypothesis in \c result that depend directly or indirectly on hidx */
     void collect_forward_deps(hypothesis_idx hidx, buffer<hypothesis_idx> & result);
+    void collect_forward_deps(hypothesis_idx hidx, buffer<hypothesis_idx> & result, hypothesis_idx_set & already_found);
 
     /** \brief Return true iff the hypothesis with index \c hidx_user depends on the hypothesis with index
         \c hidx_provider. */
@@ -242,6 +242,11 @@ public:
 
     /** \brief Store in \c r the hypotheses in this branch sorted by dependency depth */
     void get_sorted_hypotheses(hypothesis_idx_buffer & r) const;
+    /** \brief Sort hypotheses in r */
+    void sort_hypotheses(hypothesis_idx_buffer & r) const;
+
+    /** \brief Convert hypotheses indices into hrefs */
+    void to_hrefs(hypothesis_idx_buffer const & hidxs, buffer<expr> & r) const;
 
     expr expand_hrefs(expr const & e, list<expr> const & hrefs) const;