From 031979cb49de9f44613c5f01429468181cdabc0f Mon Sep 17 00:00:00 2001
From: Daniel Selsam <daniel.selsam@gmail.com>
Date: Thu, 12 Nov 2015 14:14:18 -0800
Subject: [PATCH] feat(library/blast/simplifier): take simp_rule_sets as
 argument

---
 src/frontends/lean/builtin_cmds.cpp |  2 +-
 src/library/blast/simplifier.cpp    | 14 +++++++-------
 src/library/blast/simplifier.h      |  3 ++-
 3 files changed, 10 insertions(+), 9 deletions(-)

diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 04f0ff496..87937c48a 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -1332,7 +1332,7 @@ static environment simplify_cmd(parser & p) {
     std::tie(e, ls) = parse_local_expr(p);
 
     blast::scope_debug scope(p.env(), p.ios());
-    blast::simp::result r = blast::simplify(rel, e);
+    blast::simp::result r = blast::simplify(rel, e, get_simp_rule_sets(p.env()));
 
     flycheck_information info(p.regular_stream());
     if (info.enabled()) {
diff --git a/src/library/blast/simplifier.cpp b/src/library/blast/simplifier.cpp
index 85d8c296d..092b99ee3 100644
--- a/src/library/blast/simplifier.cpp
+++ b/src/library/blast/simplifier.cpp
@@ -95,6 +95,7 @@ class simplifier {
     app_builder                                  m_app_builder;
     name                                         m_rel;
 
+    simp_rule_sets                               m_srss;
     simp_rule_sets                               m_ctx_srss;
 
     /* Logging */
@@ -168,14 +169,14 @@ class simplifier {
                             list<expr> const & emetas, list<bool> const & instances);
 
 public:
-    simplifier(name const & rel);
+    simplifier(name const & rel, simp_rule_sets const & srss);
     result operator()(expr const & e) { return simplify(e); }
 };
 
 /* Constructor */
 
-simplifier::simplifier(name const & rel):
-    m_app_builder(*m_tmp_tctx), m_rel(rel) { }
+simplifier::simplifier(name const & rel, simp_rule_sets const & srss):
+    m_app_builder(*m_tmp_tctx), m_rel(rel), m_srss(srss) { }
 
 /* Cache */
 
@@ -401,7 +402,7 @@ result simplifier::rewrite(expr const & e) {
     result r(e);
     while (true) {
         result r_ctx = rewrite(r.get_new(), m_ctx_srss);
-        result r_new = rewrite(r_ctx.get_new(), get_simp_rule_sets(env()));
+        result r_new = rewrite(r_ctx.get_new(), m_srss);
         if (r_ctx.is_none() && r_new.is_none()) break;
         r = join(join(r, r_ctx), r_new);
     }
@@ -663,9 +664,8 @@ void finalize_simplifier() {
 }
 
 /* Entry point */
-
-result simplify(name const & rel, expr const & e) {
-    return simplifier(rel)(e);
+result simplify(name const & rel, expr const & e, simp_rule_sets const & srss) {
+    return simplifier(rel, srss)(e);    
 }
 
 }}
diff --git a/src/library/blast/simplifier.h b/src/library/blast/simplifier.h
index 21cfc6727..139f33edf 100644
--- a/src/library/blast/simplifier.h
+++ b/src/library/blast/simplifier.h
@@ -6,6 +6,7 @@ Author: Daniel Selsam
 #pragma once
 #include "kernel/expr_pair.h"
 #include "library/blast/state.h"
+#include "library/simplifier/simp_rule_set.h"
 
 namespace lean {
 namespace blast {
@@ -33,7 +34,7 @@ public:
 
 }
 
-simp::result simplify(name const & rel, expr const & e);
+simp::result simplify(name const & rel, expr const & e, simp_rule_sets const & srss);
 
 void initialize_simplifier();
 void finalize_simplifier();