From 33ae79cd9e64788011adcf90a08b369043b9d973 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 17 May 2014 11:20:24 -0700 Subject: [PATCH] refactor(kernel): move shallow copy function to library Signed-off-by: Leonardo de Moura --- src/kernel/expr.cpp | 16 ---------------- src/kernel/expr.h | 5 ----- src/library/deep_copy.cpp | 16 ++++++++++++++++ src/library/deep_copy.h | 3 +++ 4 files changed, 19 insertions(+), 21 deletions(-) diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index b330bbc99..779b7606b 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -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 -} } diff --git a/src/kernel/expr.h b/src/kernel/expr.h index 7a244809c..8b52d20aa 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -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); diff --git a/src/library/deep_copy.cpp b/src/library/deep_copy.cpp index fbca3d52d..08f1b2539 100644 --- a/src/library/deep_copy.cpp +++ b/src/library/deep_copy.cpp @@ -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 m_cache; diff --git a/src/library/deep_copy.h b/src/library/deep_copy.h index d32b83b93..ac505ad43 100644 --- a/src/library/deep_copy.h +++ b/src/library/deep_copy.h @@ -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.