lean2/src/library/deep_copy.cpp

78 lines
2.9 KiB
C++
Raw Normal View History

/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "util/buffer.h"
#include "kernel/expr.h"
#include "kernel/expr_maps.h"
namespace lean {
/** \brief Implements deep copy of kernel expressions. */
class deep_copy_fn {
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) {
bool sh = false;
if (is_shared(a)) {
auto r = m_cache.find(a.raw());
if (r != m_cache.end())
return r->second;
sh = true;
}
switch (a.kind()) {
case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value:
return save_result(a, copy(a), sh);
case expr_kind::App: {
buffer<expr> new_args;
for (expr const & old_arg : args(a))
new_args.push_back(apply(old_arg));
return save_result(a, mk_app(new_args), sh);
}
refactor(kernel): add heterogeneous equality back to expr The main motivation is that we will be able to move equalities between universes. For example, suppose we have A : (Type i) B : (Type i) H : @eq (Type j) A B where j > i We didn't find any trick for deducing (@eq (Type i) A B) from H. Before this commit, heterogeneous equality as a constant with type heq : {A B : (Type U)} : A -> B -> Bool So, from H, we would only be able to deduce (@heq (Type j) (Type j) A B) Not being able to move the equality back to a smaller universe is problematic in several cases. I list some instances in the end of the commit message. With this commit, Heterogeneous equality is a special kind of expression. It is not a constant anymore. From H, we can deduce H1 : A == B That is, we are essentially "erasing" the universes when we move to heterogeneous equality. Now, since A and B have (Type i), we can deduce (@eq (Type i) A B) from H1. The proof term is (to_eq (Type i) A B (to_heq (Type j) A B H)) : (@eq (Type i) A B) So, it remains to explain why we need this feature. For example, suppose we want to state the Pi extensionality axiom. axiom hpiext {A A' : (Type U)} {B : A → (Type U)} {B' : A' → (Type U)} : A = A' → (∀ x x', x == x' → B x == B' x') → (∀ x, B x) == (∀ x, B' x) This axiom produces an "inflated" equality at (Type U) when we treat heterogeneous equality as a constant. The conclusion (∀ x, B x) == (∀ x, B' x) is syntax sugar for (@heq (Type U) (Type U) (∀ x : A, B x) (∀ x : A', B' x)) Even if A, A', B, B' live in a much smaller universe. As I described above, it doesn't seem to be a way to move this equality back to a smaller universe. So, if we wanted to keep the heterogeneous equality as a constant, it seems we would have to support axiom schemas. That is, hpiext would be parametrized by the universes where A, A', B and B'. Another possibility would be to have universe polymorphism like Agda. None of the solutions seem attractive. So, we decided to have heterogeneous equality as a special kind of expression. And use the trick above to move equalities back to the right universe. BTW, the parser is not creating the new heterogeneous equalities yet. Moreover, kernel.lean still contains a constant name heq2 that is the heterogeneous equality as a constant. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-07 18:07:08 +00:00
case expr_kind::HEq: return save_result(a, mk_heq(apply(heq_lhs(a)), apply(heq_rhs(a))), sh);
case expr_kind::Pair: return save_result(a, mk_pair(apply(pair_first(a)), apply(pair_second(a)), apply(pair_type(a))), sh);
case expr_kind::Proj: return save_result(a, mk_proj(proj_first(a), apply(proj_arg(a))), sh);
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:
/**
\brief Return a new expression that is equal to the given
argument, but does not share any memory cell with it.
*/
expr operator()(expr const & a) { return apply(a); }
};
expr deep_copy(expr const & e) {
return deep_copy_fn()(e);
}
}