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

fix(library/unfold_macros): fixes #806

Browse source
This commit is contained in:
Leonardo de Moura 2015-08-18 17:46:47 -07:00
parent 3ce8c5d6f7
commit 2b52198702
2 changed files with 9 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/library/unfold_macros.cpp
View file

@ -110,8 +110,8 @@ public:
expr operator()(expr const & e) { return visit(e); } expr operator()(expr const & e) { return visit(e); }
}; };
static bool contains_untrusted_macro(environment const & env, unsigned trust_lvl, expr const & e) { static bool contains_untrusted_macro(unsigned trust_lvl, expr const & e) {
if (env.trust_lvl() > LEAN_BELIEVER_TRUST_LEVEL) if (trust_lvl > LEAN_BELIEVER_TRUST_LEVEL)
return false; 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;
@ -119,7 +119,7 @@ static bool contains_untrusted_macro(environment const & env, unsigned 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(env, trust_lvl, e)) { if (contains_untrusted_macro(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;
@ -134,16 +134,16 @@ expr unfold_all_macros(environment const & env, expr const & e) {
return unfold_untrusted_macros(env, e, 0); return unfold_untrusted_macros(env, e, 0);
} }
static bool contains_untrusted_macro(environment const & env, unsigned trust_lvl, declaration const & d) { static bool contains_untrusted_macro(unsigned trust_lvl, declaration const & d) {
if (env.trust_lvl() > LEAN_BELIEVER_TRUST_LEVEL) if (trust_lvl > LEAN_BELIEVER_TRUST_LEVEL)
return false; return false;
if (contains_untrusted_macro(env, trust_lvl, d.get_type())) if (contains_untrusted_macro(trust_lvl, d.get_type()))
return true; return true;
return (d.is_definition() || d.is_theorem()) && contains_untrusted_macro(env, trust_lvl, d.get_value()); return (d.is_definition() || d.is_theorem()) && contains_untrusted_macro(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(env, trust_lvl, d)) { if (contains_untrusted_macro(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);

1
src/shell/CMakeLists.txt
View file

@ -26,6 +26,7 @@ add_test(lean_ghash1 "${CMAKE_CURRENT_BINARY_DIR}/lean" -g)
add_test(lean_ghash2 "${CMAKE_CURRENT_BINARY_DIR}/lean" --githash) add_test(lean_ghash2 "${CMAKE_CURRENT_BINARY_DIR}/lean" --githash)
add_test(lean_path1 "${CMAKE_CURRENT_BINARY_DIR}/lean" -p) add_test(lean_path1 "${CMAKE_CURRENT_BINARY_DIR}/lean" -p)
add_test(lean_path2 "${CMAKE_CURRENT_BINARY_DIR}/lean" --path) add_test(lean_path2 "${CMAKE_CURRENT_BINARY_DIR}/lean" --path)
add_test(export_all "${LEAN_SOURCE_DIR}/../bin/lean" --export-all=all.out "${LEAN_SOURCE_DIR}/../library/standard.lean")
add_test(lean_luahook1 "${CMAKE_CURRENT_BINARY_DIR}/lean" --luahook=100 "${LEAN_SOURCE_DIR}/../tests/lua/big.lua") add_test(lean_luahook1 "${CMAKE_CURRENT_BINARY_DIR}/lean" --luahook=100 "${LEAN_SOURCE_DIR}/../tests/lua/big.lua")
add_test(lean_luahook2 "${CMAKE_CURRENT_BINARY_DIR}/lean" -k 100 "${LEAN_SOURCE_DIR}/../tests/lua/big.lua") add_test(lean_luahook2 "${CMAKE_CURRENT_BINARY_DIR}/lean" -k 100 "${LEAN_SOURCE_DIR}/../tests/lua/big.lua")
# add_test(lean_lua1 ${LEAN_SOURCE_DIR}/cmake/redirect.sh "${CMAKE_CURRENT_BINARY_DIR}/lean" "--lua" "${LEAN_SOURCE_DIR}/../tests/lua/single.lua") # add_test(lean_lua1 ${LEAN_SOURCE_DIR}/cmake/redirect.sh "${CMAKE_CURRENT_BINARY_DIR}/lean" "--lua" "${LEAN_SOURCE_DIR}/../tests/lua/single.lua")