michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

perf(library/unfold_macros): skip contains_untrusted_macro if trust level is very high

Browse source
This commit is contained in:
Leonardo de Moura 2015-08-14 18:10:19 -07:00
parent 849b99d244
commit cc8b5d2d6e
1 changed files with 8 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/library/unfold_macros.cpp
View file

@ -110,14 +110,16 @@ public:
expr operator()(expr const & e) { return visit(e); } 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 static_cast<bool>(find(e, [&](expr const & e, unsigned) {
return is_macro(e) && macro_def(e).trust_level() >= trust_lvl; return is_macro(e) && macro_def(e).trust_level() >= trust_lvl;
})); }));
} }
expr unfold_untrusted_macros(environment const & env, expr const & e, unsigned 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); return unfold_untrusted_macros_fn(env, trust_lvl)(e);
} else { } else {
return e; return e;
@ -132,14 +134,14 @@ expr unfold_all_macros(environment const & env, expr const & e) {
return unfold_untrusted_macros(env, e, 0); return unfold_untrusted_macros(env, e, 0);
} }
bool contains_untrusted_macro(unsigned trust_lvl, declaration const & d) { static bool contains_untrusted_macro(environment const & env, unsigned trust_lvl, declaration const & d) {
if (contains_untrusted_macro(trust_lvl, d.get_type())) if (contains_untrusted_macro(env, trust_lvl, d.get_type()))
return true; 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) { 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); expr new_t = unfold_untrusted_macros(env, d.get_type(), trust_lvl);
if (d.is_theorem()) { if (d.is_theorem()) {
expr new_v = unfold_untrusted_macros(env, d.get_value(), trust_lvl); expr new_v = unfold_untrusted_macros(env, d.get_value(), trust_lvl);