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

refactor(library/unfold_macros): use replace_visitor_with_tc to implement unfold_macros

Browse source 
This commit also fixes a potential peformance problem at
unfold_macros (it was eagerly expanding let-expressions).
This commit is contained in:
Leonardo de Moura 2016-12-29 18:11:33 -08:00
parent 73bf232fea
commit a500059672
2 changed files with 11 additions and 89 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/library/type_context.h
View file

@ -376,6 +376,8 @@ public:
bool is_prop(expr const & e);
bool is_proof(expr const & e);
optional<expr> expand_macro(expr const & e);
optional<name> is_class(expr const & type);
optional<expr> mk_class_instance(expr const & type);
optional<expr> mk_subsingleton_instance(expr const & type);
@ -471,7 +473,6 @@ private:
optional<expr> unfold_definition(expr const & e);
optional<expr> try_unfold_definition(expr const & e);
bool should_unfold_macro(expr const & e);
optional<expr> expand_macro(expr const & e);
expr whnf_core(expr const & e);
optional<declaration> is_transparent(transparency_mode m, name const & n);
optional<declaration> is_transparent(name const & n);

97
src/library/unfold_macros.cpp
View file

@ -5,14 +5,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "util/interrupt.h"
#include "util/fresh_name.h"
#include "kernel/type_checker.h"
#include "kernel/find_fn.h"
#include "kernel/expr_maps.h"
#include "kernel/instantiate.h"
#include "kernel/abstract.h"
#include "library/type_context.h"
#include "library/unfold_macros.h"
#include "library/replace_visitor.h"
#include "library/replace_visitor_with_tc.h"
#include "library/exception.h"
/* If the trust level of all macros is < LEAN_BELIEVER_TRUST_LEVEL,
@ -21,26 +18,17 @@ Author: Leonardo de Moura
// #define LEAN_ALL_MACROS_HAVE_SMALL_TRUST_LVL
namespace lean {
class unfold_untrusted_macros_fn {
typedef expr_bi_struct_map<expr> cache;
type_checker m_tc;
class unfold_untrusted_macros_fn : public replace_visitor_with_tc {
unsigned m_trust_lvl;
cache m_cache;
expr save_result(expr const & e, expr && r) {
m_cache.insert(std::make_pair(e, r));
return r;
}
expr visit_macro(expr const & e) {
virtual expr visit_macro(expr const & e) override {
buffer<expr> new_args;
for (unsigned i = 0; i < macro_num_args(e); i++)
new_args.push_back(visit(macro_arg(e, i)));
auto def = macro_def(e);
expr r = update_macro(e, new_args.size(), new_args.data());
if (def.trust_level() >= m_trust_lvl) {
if (optional<expr> new_r = m_tc.expand_macro(r)) {
if (optional<expr> new_r = m_ctx.expand_macro(r)) {
return *new_r;
} else {
throw generic_exception(e, "failed to expand macro");
@ -50,77 +38,9 @@ class unfold_untrusted_macros_fn {
}
}
expr visit_app(expr const & e) {
expr new_f = visit(app_fn(e));
expr new_v = visit(app_arg(e));
return update_app(e, new_f, new_v);
}
expr visit_binding(expr e) {
expr_kind k = e.kind();
buffer<expr> es;
buffer<expr> ls;
while (e.kind() == k) {
expr d = visit(instantiate_rev(binding_domain(e), ls.size(), ls.data()));
expr l = mk_local(mk_fresh_name(), binding_name(e), d, binding_info(e));
ls.push_back(l);
es.push_back(e);
e = binding_body(e);
}
e = visit(instantiate_rev(e, ls.size(), ls.data()));
expr r = abstract_locals(e, ls.size(), ls.data());
while (!ls.empty()) {
expr d = mlocal_type(ls.back());
ls.pop_back();
d = abstract_locals(d, ls.size(), ls.data());
r = update_binding(es.back(), d, r);
es.pop_back();
}
return r;
}
expr visit_let(expr const & e) {
// TODO(Leo): improve
return visit(instantiate(let_body(e), let_value(e)));
}
expr visit(expr const & e) {
switch (e.kind()) {
case expr_kind::Sort: case expr_kind::Constant:
case expr_kind::Var: case expr_kind::Meta:
case expr_kind::Local:
return e;
default:
break;
}
check_system("unfold macros");
auto it = m_cache.find(e);
if (it != m_cache.end())
return it->second;
switch (e.kind()) {
case expr_kind::Sort: case expr_kind::Constant:
case expr_kind::Var: case expr_kind::Meta:
case expr_kind::Local:
lean_unreachable();
case expr_kind::Macro:
return save_result(e, visit_macro(e));
case expr_kind::App:
return save_result(e, visit_app(e));
case expr_kind::Lambda: case expr_kind::Pi:
return save_result(e, visit_binding(e));
case expr_kind::Let:
return save_result(e, visit_let(e));
}
lean_unreachable();
}
public:
unfold_untrusted_macros_fn(environment const & env, unsigned lvl):
m_tc(env), m_trust_lvl(lvl) {}
expr operator()(expr const & e) { return visit(e); }
unfold_untrusted_macros_fn(type_context & ctx, unsigned lvl):
replace_visitor_with_tc(ctx), m_trust_lvl(lvl) {}
};
static bool contains_untrusted_macro(unsigned trust_lvl, expr const & e) {
@ -134,7 +54,8 @@ static bool contains_untrusted_macro(unsigned trust_lvl, expr const & e) {
expr unfold_untrusted_macros(environment const & env, expr const & e, unsigned trust_lvl) {
if (contains_untrusted_macro(trust_lvl, e)) {
return unfold_untrusted_macros_fn(env, trust_lvl)(e);
type_context ctx(env, transparency_mode::All);
return unfold_untrusted_macros_fn(ctx, trust_lvl)(e);
} else {
return e;
}