max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/unfold_macros): add definition for disabling optimization

Browse source
This commit is contained in:
Leonardo de Moura 2016-12-28 19:59:41 -08:00
parent 5b6e81ddb9
commit 7f86ad64eb
1 changed files with 12 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/library/unfold_macros.cpp
View file

@ -15,6 +15,11 @@ Author: Leonardo de Moura
#include "library/replace_visitor.h"
#include "library/exception.h"
/* If the trust level of all macros is < LEAN_BELIEVER_TRUST_LEVEL,
then we skip the unfold_untrusted_macros potentially expensive step.
The following definition is commented because we are currently testing the AC macros. */
// #define LEAN_ALL_MACROS_HAVE_SMALL_TRUST_LVL
namespace lean {
class unfold_untrusted_macros_fn {
typedef expr_bi_struct_map<expr> cache;
@ -119,8 +124,9 @@ public:
};
static bool contains_untrusted_macro(unsigned trust_lvl, expr const & e) {
if (trust_lvl > LEAN_BELIEVER_TRUST_LEVEL)
return false;
#if defined(LEAN_ALL_MACROS_HAVE_SMALL_TRUST_LVL)
if (trust_lvl > LEAN_BELIEVER_TRUST_LEVEL) return false;
#endif
return static_cast<bool>(find(e, [&](expr const & e, unsigned) {
return is_macro(e) && macro_def(e).trust_level() >= trust_lvl;
}));
@ -143,7 +149,10 @@ expr unfold_all_macros(environment const & env, expr const & e) {
}
static bool contains_untrusted_macro(unsigned trust_lvl, declaration const & d) {
if (trust_lvl > LEAN_BELIEVER_TRUST_LEVEL || !d.is_trusted())
#if defined(LEAN_ALL_MACROS_HAVE_SMALL_TRUST_LVL)
if (trust_lvl > LEAN_BELIEVER_TRUST_LEVEL) return false;
#endif
if (!d.is_trusted())
return false;
if (contains_untrusted_macro(trust_lvl, d.get_type()))
return true;