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

refactor(library): deep_copy procedure

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-02-22 22:53:34 -08:00
parent 41782c0894
commit 8cd78e00f1
3 changed files with 26 additions and 49 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/CMakeLists.txt
View file

@ -213,8 +213,8 @@ add_subdirectory(util/interval)
set(LEAN_LIBS ${LEAN_LIBS} interval) set(LEAN_LIBS ${LEAN_LIBS} interval)
add_subdirectory(kernel) add_subdirectory(kernel)
set(LEAN_LIBS ${LEAN_LIBS} kernel) set(LEAN_LIBS ${LEAN_LIBS} kernel)
# add_subdirectory(library) add_subdirectory(library)
# set(LEAN_LIBS ${LEAN_LIBS} library) set(LEAN_LIBS ${LEAN_LIBS} library)
# add_subdirectory(library/arith) # add_subdirectory(library/arith)
# set(LEAN_LIBS ${LEAN_LIBS} arithlib) # set(LEAN_LIBS ${LEAN_LIBS} arithlib)
# add_subdirectory(library/rewriter) # add_subdirectory(library/rewriter)

9
src/library/CMakeLists.txt
View file

@ -1,6 +1,7 @@
add_library(library kernel_bindings.cpp deep_copy.cpp add_library(library deep_copy.cpp)
context_to_lambda.cpp placeholder.cpp expr_lt.cpp substitution.cpp # kernel_bindings.cpp deep_copy.cpp
fo_unify.cpp bin_op.cpp equality.cpp io_state_stream.cpp printer.cpp # context_to_lambda.cpp placeholder.cpp expr_lt.cpp substitution.cpp
hop_match.cpp) # fo_unify.cpp bin_op.cpp equality.cpp io_state_stream.cpp printer.cpp
# hop_match.cpp)
target_link_libraries(library ${LEAN_LIBS}) target_link_libraries(library ${LEAN_LIBS})

62
src/library/deep_copy.cpp
View file

@ -13,19 +13,6 @@ namespace lean {
class deep_copy_fn { class deep_copy_fn {
expr_cell_map<expr> m_cache; expr_cell_map<expr> m_cache;
expr save_result(expr const & a, expr && r, bool shared) {
if (shared)
m_cache.insert(std::make_pair(a.raw(), r));
return r;
}
optional<expr> apply(optional<expr> const & a) {
if (a)
return some_expr(apply(*a));
else
return a;
}
expr apply(expr const & a) { expr apply(expr const & a) {
bool sh = false; bool sh = false;
if (is_shared(a)) { if (is_shared(a)) {
@ -34,33 +21,26 @@ class deep_copy_fn {
return r->second; return r->second;
sh = true; sh = true;
} }
expr r;
switch (a.kind()) { switch (a.kind()) {
case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: case expr_kind::Var:
return save_result(a, copy(a), sh); case expr_kind::Constant:
case expr_kind::App: { case expr_kind::Sort:
buffer<expr> new_args; case expr_kind::Macro: r = copy(a); break;
for (expr const & old_arg : args(a)) case expr_kind::App: r = mk_app(apply(app_fn(a)), apply(app_arg(a))); break;
new_args.push_back(apply(old_arg)); case expr_kind::Pair: r = mk_pair(apply(pair_first(a)), apply(pair_second(a)), apply(pair_type(a))); break;
return save_result(a, mk_app(new_args), sh); case expr_kind::Fst: r = mk_fst(apply(proj_arg(a))); break;
case expr_kind::Snd: r = mk_snd(apply(proj_arg(a))); break;
case expr_kind::Lambda: r = mk_lambda(binder_name(a), apply(binder_domain(a)), apply(binder_body(a))); break;
case expr_kind::Pi: r = mk_pi(binder_name(a), apply(binder_domain(a)), apply(binder_body(a))); break;
case expr_kind::Sigma: r = mk_sigma(binder_name(a), apply(binder_domain(a)), apply(binder_body(a))); break;
case expr_kind::Let: r = mk_let(let_name(a), apply(let_type(a)), apply(let_value(a)), apply(let_body(a))); break;
case expr_kind::Meta: r = mk_metavar(mlocal_name(a), apply(mlocal_type(a))); break;
case expr_kind::Local: r = mk_local(mlocal_name(a), apply(mlocal_type(a))); break;
} }
case expr_kind::HEq: return save_result(a, mk_heq(apply(heq_lhs(a)), apply(heq_rhs(a))), sh); if (sh)
case expr_kind::Pair: return save_result(a, mk_pair(apply(pair_first(a)), apply(pair_second(a)), apply(pair_type(a))), sh); m_cache.insert(std::make_pair(a.raw(), r));
case expr_kind::Proj: return save_result(a, mk_proj(proj_first(a), apply(proj_arg(a))), sh); return r;
case expr_kind::Lambda: return save_result(a, mk_lambda(abst_name(a), apply(abst_domain(a)), apply(abst_body(a))), sh);
case expr_kind::Pi: return save_result(a, mk_pi(abst_name(a), apply(abst_domain(a)), apply(abst_body(a))), sh);
case expr_kind::Sigma: return save_result(a, mk_sigma(abst_name(a), apply(abst_domain(a)), apply(abst_body(a))), sh);
case expr_kind::Let: return save_result(a, mk_let(let_name(a), apply(let_type(a)), apply(let_value(a)), apply(let_body(a))), sh);
case expr_kind::MetaVar:
return save_result(a,
update_metavar(a, [&](local_entry const & e) -> local_entry {
if (e.is_inst())
return mk_inst(e.s(), apply(e.v()));
else
return e;
}),
sh);
}
lean_unreachable(); // LCOV_EXCL_LINE
} }
public: public:
/** /**
@ -69,9 +49,5 @@ public:
*/ */
expr operator()(expr const & a) { return apply(a); } expr operator()(expr const & a) { return apply(a); }
}; };
expr deep_copy(expr const & e) { return deep_copy_fn()(e); }
expr deep_copy(expr const & e) {
return deep_copy_fn()(e);
}
} }