From 8e3ac023bb2e664770549dd5fb4853da9b415177 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 23 Oct 2014 13:09:59 -0700
Subject: [PATCH] feat(library/reducible): expose 'memoize' flag

---
 src/library/reducible.cpp | 7 ++++---
 src/library/reducible.h   | 3 ++-
 2 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/src/library/reducible.cpp b/src/library/reducible.cpp
index e84d514282..6e120214d6 100644
--- a/src/library/reducible.cpp
+++ b/src/library/reducible.cpp
@@ -116,7 +116,8 @@ bool is_reducible_off(environment const & env, name const & n) {
 }
 
 std::unique_ptr<type_checker> mk_type_checker(environment const & env, name_generator const & ngen,
-                                              bool relax_main_opaque, bool only_main_reducible) {
+                                              bool relax_main_opaque, bool only_main_reducible,
+                                              bool memoize) {
     reducible_state const & s = reducible_ext::get_state(env);
     if (only_main_reducible) {
         name_set reducible_on  = s.m_reducible_on;
@@ -127,12 +128,12 @@ std::unique_ptr<type_checker> mk_type_checker(environment const & env, name_gene
                     (!reducible_on.contains(n));
             });
         return std::unique_ptr<type_checker>(new type_checker(env, ngen, mk_default_converter(env, relax_main_opaque,
-                                                                                              true, pred)));
+                                                                                              memoize, pred)));
     } else {
         name_set reducible_off = s.m_reducible_off;
         extra_opaque_pred pred([=](name const & n) { return reducible_off.contains(n); });
         return std::unique_ptr<type_checker>(new type_checker(env, ngen, mk_default_converter(env, relax_main_opaque,
-                                                                                              true, pred)));
+                                                                                              memoize, pred)));
     }
 }
 std::unique_ptr<type_checker> mk_type_checker(environment const & env, bool relax_main_opaque, bool only_main_reducible) {
diff --git a/src/library/reducible.h b/src/library/reducible.h
index ecb808e96c..b915a8bf76 100644
--- a/src/library/reducible.h
+++ b/src/library/reducible.h
@@ -35,7 +35,8 @@ bool is_reducible_off(environment const & env, name const & n);
 
 /** \brief Create a type checker that takes the "reducibility" hints into account. */
 std::unique_ptr<type_checker> mk_type_checker(environment const & env, name_generator const & ngen,
-                                              bool relax_main_opaque = true, bool only_main_reducible = false);
+                                              bool relax_main_opaque = true, bool only_main_reducible = false,
+                                              bool memoize = true);
 std::unique_ptr<type_checker> mk_type_checker(environment const & env, bool relax_main_opaque, bool only_main_reducible = false);
 
 void initialize_reducible();