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

refactor(kernel): move shallow copy function to library

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-17 11:20:24 -07:00
parent d625c9a26c
commit 33ae79cd9e
4 changed files with 19 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/kernel/expr.cpp
View file

@ -481,20 +481,4 @@ bool is_arrow(expr const & t) {
return res;
}
}
expr copy(expr const & a) {
switch (a.kind()) {
case expr_kind::Var: return mk_var(var_idx(a));
case expr_kind::Constant: return mk_constant(const_name(a), const_levels(a));
case expr_kind::Sort: return mk_sort(sort_level(a));
case expr_kind::Macro: return mk_macro(to_macro(a)->m_definition, macro_num_args(a), macro_args(a));
case expr_kind::App: return mk_app(app_fn(a), app_arg(a));
case expr_kind::Lambda: return mk_lambda(binding_name(a), binding_domain(a), binding_body(a), binding_info(a));
case expr_kind::Pi: return mk_pi(binding_name(a), binding_domain(a), binding_body(a), binding_info(a));
case expr_kind::Let: return mk_let(let_name(a), let_type(a), let_value(a), let_body(a));
case expr_kind::Meta: return mk_metavar(mlocal_name(a), mlocal_type(a));
case expr_kind::Local: return mk_local(mlocal_name(a), local_pp_name(a), mlocal_type(a));
}
lean_unreachable(); // LCOV_EXCL_LINE
}
}

5
src/kernel/expr.h
View file

@ -631,11 +631,6 @@ struct expr_cell_offset_hash { unsigned operator()(expr_cell_offset const & p) c
struct expr_cell_offset_eqp { unsigned operator()(expr_cell_offset const & p1, expr_cell_offset const & p2) const { return p1 == p2; } };
// =======================================
/**
\brief Return a shallow copy of \c e
*/
expr copy(expr const & e);
// =======================================
// Update
expr update_app(expr const & e, expr const & new_fn, expr const & new_arg);

16
src/library/deep_copy.cpp
View file

@ -9,6 +9,22 @@ Author: Leonardo de Moura
#include "kernel/expr_maps.h"
namespace lean {
expr copy(expr const & a) {
switch (a.kind()) {
case expr_kind::Var: return mk_var(var_idx(a));
case expr_kind::Constant: return mk_constant(const_name(a), const_levels(a));
case expr_kind::Sort: return mk_sort(sort_level(a));
case expr_kind::Macro: return mk_macro(to_macro(a)->m_definition, macro_num_args(a), macro_args(a));
case expr_kind::App: return mk_app(app_fn(a), app_arg(a));
case expr_kind::Lambda: return mk_lambda(binding_name(a), binding_domain(a), binding_body(a), binding_info(a));
case expr_kind::Pi: return mk_pi(binding_name(a), binding_domain(a), binding_body(a), binding_info(a));
case expr_kind::Let: return mk_let(let_name(a), let_type(a), let_value(a), let_body(a));
case expr_kind::Meta: return mk_metavar(mlocal_name(a), mlocal_type(a));
case expr_kind::Local: return mk_local(mlocal_name(a), local_pp_name(a), mlocal_type(a));
}
lean_unreachable(); // LCOV_EXCL_LINE
}
/** \brief Implements deep copy of kernel expressions. */
class deep_copy_fn {
expr_cell_map<expr> m_cache;

3
src/library/deep_copy.h
View file

@ -8,6 +8,9 @@ Author: Leonardo de Moura
#include "kernel/expr.h"
namespace lean {
/** \brief Return a shallow copy of \c e */
expr copy(expr const & e);
/**
\brief Return a new expression that is equal to the given
argument, but does not share any memory cell with it.