From 506cca0ac11e85e61595be061f948c5ddc804573 Mon Sep 17 00:00:00 2001
From: Soonho Kong <soonhok@cs.cmu.edu>
Date: Sun, 1 Dec 2013 00:58:06 -0500
Subject: [PATCH] feat(library/rewriter): implement depth RW

---
 src/library/rewriter/rewriter.cpp |  8 +++-----
 src/library/rewriter/rewriter.h   | 26 ++++++++++++++++++++++++++
 2 files changed, 29 insertions(+), 5 deletions(-)

diff --git a/src/library/rewriter/rewriter.cpp b/src/library/rewriter/rewriter.cpp
index b70f3293e..772f039df 100644
--- a/src/library/rewriter/rewriter.cpp
+++ b/src/library/rewriter/rewriter.cpp
@@ -11,13 +11,12 @@
 #include "kernel/context.h"
 #include "kernel/environment.h"
 #include "kernel/expr.h"
-#include "kernel/replace.h"
 #include "kernel/printer.h"
+#include "kernel/replace.h"
 #include "library/basic_thms.h"
-#include "library/type_inferer.h"
 #include "library/rewriter/fo_match.h"
 #include "library/rewriter/rewriter.h"
-#include "library/rewriter/apply_rewriter_fn.h"
+#include "library/type_inferer.h"
 #include "util/buffer.h"
 #include "util/trace.h"
 
@@ -967,8 +966,7 @@ ostream & repeat_rewriter_cell::display(ostream & out) const {
 depth_rewriter_cell::depth_rewriter_cell(rewriter const & rw):rewriter_cell(rewriter_kind::Depth), m_rw(rw) { }
 depth_rewriter_cell::~depth_rewriter_cell() { }
 pair<expr, expr> depth_rewriter_cell::operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception) {
-    apply_rewriter_fn f(m_rw);
-    return f.apply(env, ctx, v);
+    return apply_rewriter_fn<decltype(m_rw)>(m_rw)(env, ctx, v);
 }
 ostream & depth_rewriter_cell::display(ostream & out) const {
     out << "Depth_RW(" << m_rw << ")";
diff --git a/src/library/rewriter/rewriter.h b/src/library/rewriter/rewriter.h
index a79a9cd94..3466a4102 100644
--- a/src/library/rewriter/rewriter.h
+++ b/src/library/rewriter/rewriter.h
@@ -380,6 +380,11 @@ class apply_rewriter_fn {
                 results.push_back(apply(env, ctx, arg(v, i)));
             }
             result = rewrite_app(env, ctx, v, results);
+            std::pair<expr, expr> tmp = m_rw(env, ctx, result.first);
+            if (result.first != tmp.first) {
+                tmp.second = Trans(ty_v, v, result.first, tmp.first, result.second, tmp.second);
+                result = tmp;
+            }
         }
             break;
         case expr_kind::Eq: {
@@ -406,6 +411,11 @@ class apply_rewriter_fn {
                     result = std::make_pair(v, Refl(lc(v, ctx), v));
                 }
             }
+            std::pair<expr, expr> tmp = m_rw(env, ctx, result.first);
+            if (result.first != tmp.first) {
+                tmp.second = Trans(ty_v, v, result.first, tmp.first, result.second, tmp.second);
+                result = tmp;
+            }
         }
             break;
         case expr_kind::Lambda: {
@@ -432,6 +442,11 @@ class apply_rewriter_fn {
                     result = std::make_pair(v, Refl(lc(v, ctx), v));
                 }
             }
+            std::pair<expr, expr> tmp = m_rw(env, ctx, result.first);
+            if (result.first != tmp.first) {
+                tmp.second = Trans(ty_v, v, result.first, tmp.first, result.second, tmp.second);
+                result = tmp;
+            }
         }
             break;
 
@@ -459,6 +474,11 @@ class apply_rewriter_fn {
                     result = std::make_pair(v, Refl(lc(v, ctx), v));
                 }
             }
+            std::pair<expr, expr> tmp = m_rw(env, ctx, result.first);
+            if (result.first != tmp.first) {
+                tmp.second = Trans(ty_v, v, result.first, tmp.first, result.second, tmp.second);
+                result = tmp;
+            }
         }
             break;
         case expr_kind::Let: {
@@ -506,6 +526,12 @@ class apply_rewriter_fn {
                 changed = true;
             }
             result = std::make_pair(new_v, pf);
+
+            std::pair<expr, expr> tmp = m_rw(env, ctx, result.first);
+            if (result.first != tmp.first) {
+                tmp.second = Trans(ty_v, v, result.first, tmp.first, result.second, tmp.second);
+                result = tmp;
+            }
         }
             break;
         }