From cc8b5d2d6e0e4728bb88fa0c186c96483bbbebcc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 14 Aug 2015 18:10:19 -0700
Subject: [PATCH] perf(library/unfold_macros): skip contains_untrusted_macro if
 trust level is very high

---
 src/library/unfold_macros.cpp | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/src/library/unfold_macros.cpp b/src/library/unfold_macros.cpp
index 2135ae6eeb..898fbbe747 100644
--- a/src/library/unfold_macros.cpp
+++ b/src/library/unfold_macros.cpp
@@ -110,14 +110,16 @@ public:
     expr operator()(expr const & e) { return visit(e); }
 };
 
-bool contains_untrusted_macro(unsigned trust_lvl, expr const & e) {
+static bool contains_untrusted_macro(environment const & env, unsigned trust_lvl, expr const & e) {
+    if (env.trust_lvl() > LEAN_BELIEVER_TRUST_LEVEL)
+        return false;
     return static_cast<bool>(find(e, [&](expr const & e, unsigned) {
                 return is_macro(e) && macro_def(e).trust_level() >= trust_lvl;
             }));
 }
 
 expr unfold_untrusted_macros(environment const & env, expr const & e, unsigned trust_lvl) {
-    if (contains_untrusted_macro(trust_lvl, e)) {
+    if (contains_untrusted_macro(env, trust_lvl, e)) {
         return unfold_untrusted_macros_fn(env, trust_lvl)(e);
     } else {
         return e;
@@ -132,14 +134,14 @@ expr unfold_all_macros(environment const & env, expr const & e) {
     return unfold_untrusted_macros(env, e, 0);
 }
 
-bool contains_untrusted_macro(unsigned trust_lvl, declaration const & d) {
-    if (contains_untrusted_macro(trust_lvl, d.get_type()))
+static bool contains_untrusted_macro(environment const & env, unsigned trust_lvl, declaration const & d) {
+    if (contains_untrusted_macro(env, trust_lvl, d.get_type()))
         return true;
-    return (d.is_definition() || d.is_theorem()) && contains_untrusted_macro(trust_lvl, d.get_value());
+    return (d.is_definition() || d.is_theorem()) && contains_untrusted_macro(env, trust_lvl, d.get_value());
 }
 
 declaration unfold_untrusted_macros(environment const & env, declaration const & d, unsigned trust_lvl) {
-    if (contains_untrusted_macro(trust_lvl, d)) {
+    if (contains_untrusted_macro(env, trust_lvl, d)) {
         expr new_t = unfold_untrusted_macros(env, d.get_type(), trust_lvl);
         if (d.is_theorem()) {
             expr new_v = unfold_untrusted_macros(env, d.get_value(), trust_lvl);