From bc8379256afa55ad197cb9dde89a14dc51a4dacd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 17 Apr 2014 10:52:07 -0700 Subject: [PATCH] refactor(kernel): remove pairs from kernel Signed-off-by: Leonardo de Moura --- src/kernel/expr.cpp | 84 +++------------------------------ src/kernel/expr.h | 67 ++------------------------ src/kernel/expr_eq_fn.cpp | 9 +--- src/kernel/for_each_fn.cpp | 10 +--- src/kernel/formatter.cpp | 19 -------- src/kernel/free_vars.cpp | 33 +++---------- src/kernel/max_sharing.cpp | 10 +--- src/kernel/normalizer.cpp | 23 +-------- src/kernel/replace_fn.cpp | 18 +------ src/kernel/replace_visitor.cpp | 15 ------ src/kernel/replace_visitor.h | 5 -- src/library/deep_copy.cpp | 4 -- src/library/expr_lt.cpp | 11 +---- src/tests/kernel/expr.cpp | 30 +----------- src/tests/kernel/normalizer.cpp | 6 +-- 15 files changed, 26 insertions(+), 318 deletions(-) diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index a5682f3bb..95e18c53f 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -102,32 +102,6 @@ expr_composite::expr_composite(expr_kind k, unsigned h, bool has_mv, bool has_lo expr_cell(k, h, has_mv, has_local, has_param_univ), m_depth(d) {} -// Expr dependent pairs -expr_dep_pair::expr_dep_pair(expr const & f, expr const & s, expr const & t): - expr_composite(expr_kind::Pair, ::lean::hash(f.hash(), s.hash()), - f.has_metavar() || s.has_metavar() || t.has_metavar(), - f.has_local() || s.has_local() || t.has_local(), - f.has_param_univ() || s.has_param_univ() || t.has_param_univ(), - std::max(get_depth(f), get_depth(s))+1), - m_first(f), m_second(s), m_type(t) { -} -void expr_dep_pair::dealloc(buffer & todelete) { - dec_ref(m_first, todelete); - dec_ref(m_second, todelete); - dec_ref(m_type, todelete); - delete(this); -} - -// Expr pair projection -expr_proj::expr_proj(bool f, expr const & e): - expr_composite(f ? expr_kind::Fst : expr_kind::Snd, ::lean::hash(17, e.hash()), e.has_metavar(), e.has_local(), e.has_param_univ(), - get_depth(e)+1), - m_expr(e) {} -void expr_proj::dealloc(buffer & todelete) { - dec_ref(m_expr, todelete); - delete(this); -} - // Expr applications expr_app::expr_app(expr const & fn, expr const & arg): expr_composite(expr_kind::App, ::lean::hash(fn.hash(), arg.hash()), @@ -142,7 +116,7 @@ void expr_app::dealloc(buffer & todelete) { delete(this); } -// Expr binders (Lambda, Pi and Sigma) +// Expr binders (Lambda, Pi) expr_binder::expr_binder(expr_kind k, name const & n, expr const & t, expr const & b): expr_composite(k, ::lean::hash(t.hash(), b.hash()), t.has_metavar() || b.has_metavar(), @@ -152,7 +126,7 @@ expr_binder::expr_binder(expr_kind k, name const & n, expr const & t, expr const m_name(n), m_domain(t), m_body(b) { - lean_assert(k == expr_kind::Lambda || k == expr_kind::Pi || k == expr_kind::Sigma); + lean_assert(k == expr_kind::Lambda || k == expr_kind::Pi); } void expr_binder::dealloc(buffer & todelete) { dec_ref(m_body, todelete); @@ -246,13 +220,9 @@ void expr_cell::dealloc() { case expr_kind::Local: static_cast(it)->dealloc(todo); break; case expr_kind::Constant: delete static_cast(it); break; case expr_kind::Sort: delete static_cast(it); break; - case expr_kind::Pair: static_cast(it)->dealloc(todo); break; - case expr_kind::Fst: - case expr_kind::Snd: static_cast(it)->dealloc(todo); break; case expr_kind::App: static_cast(it)->dealloc(todo); break; case expr_kind::Lambda: - case expr_kind::Pi: - case expr_kind::Sigma: static_cast(it)->dealloc(todo); break; + case expr_kind::Pi: static_cast(it)->dealloc(todo); break; case expr_kind::Let: static_cast(it)->dealloc(todo); break; } } @@ -293,7 +263,6 @@ expr mk_rev_app(unsigned num_args, expr const * args) { static name g_default_var_name("a"); bool is_default_var_name(name const & n) { return n == g_default_var_name; } expr mk_arrow(expr const & t, expr const & e) { return mk_pi(g_default_var_name, t, e); } -expr mk_cartesian_product(expr const & t, expr const & e) { return mk_sigma(g_default_var_name, t, e); } expr Bool = mk_sort(mk_level_zero()); expr Type = mk_sort(mk_level_one()); @@ -305,8 +274,7 @@ unsigned get_depth(expr const & e) { case expr_kind::Var: case expr_kind::Constant: case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local: case expr_kind::Macro: return 1; - case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Sigma: - case expr_kind::Pair: case expr_kind::Fst: case expr_kind::Snd: + case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::App: case expr_kind::Let: return static_cast(e.raw())->m_depth; } @@ -334,20 +302,6 @@ expr update_rev_app(expr const & e, unsigned num, expr const * new_args) { return e; } -expr update_proj(expr const & e, expr const & new_arg) { - if (!is_eqp(proj_arg(e), new_arg)) - return mk_proj(is_fst(e), new_arg); - else - return e; -} - -expr update_pair(expr const & e, expr const & new_first, expr const & new_second, expr const & new_type) { - if (!is_eqp(pair_first(e), new_first) || !is_eqp(pair_second(e), new_second) || !is_eqp(pair_type(e), new_type)) - return mk_pair(new_first, new_second, new_type); - else - return e; -} - expr update_binder(expr const & e, expr const & new_domain, expr const & new_body) { if (!is_eqp(binder_domain(e), new_domain) || !is_eqp(binder_body(e), new_body)) return mk_binder(e.kind(), binder_name(e), new_domain, new_body); @@ -390,8 +344,7 @@ bool is_atomic(expr const & e) { return true; case expr_kind::App: case expr_kind::Let: case expr_kind::Meta: case expr_kind::Local: - case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Sigma: - case expr_kind::Pair: case expr_kind::Fst: case expr_kind::Snd: + case expr_kind::Lambda: case expr_kind::Pi: return false; } lean_unreachable(); // LCOV_EXCL_LINE @@ -408,23 +361,15 @@ bool is_arrow(expr const & t) { } } -bool is_cartesian(expr const & t) { - return is_sigma(t) && !has_free_var(binder_body(t), 0); -} - 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_level_params(a)); case expr_kind::Sort: return mk_sort(sort_level(a)); case expr_kind::Macro: return mk_macro(static_cast(a.raw())->m_macro); - case expr_kind::Pair: return mk_pair(pair_first(a), pair_second(a), pair_type(a)); - case expr_kind::Fst: return mk_fst(proj_arg(a)); - case expr_kind::Snd: return mk_snd(proj_arg(a)); case expr_kind::App: return mk_app(app_fn(a), app_arg(a)); case expr_kind::Lambda: return mk_lambda(binder_name(a), binder_domain(a), binder_body(a)); case expr_kind::Pi: return mk_pi(binder_name(a), binder_domain(a), binder_body(a)); - case expr_kind::Sigma: return mk_sigma(binder_name(a), binder_domain(a), binder_body(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), mlocal_type(a)); @@ -453,16 +398,10 @@ class expr_serializer : public object_serializer & todelete); -public: - expr_dep_pair(expr const & f, expr const & s, expr const & t); - expr const & get_first() const { return m_first; } - expr const & get_second() const { return m_second; } - expr const & get_type() const { return m_type; } -}; - -/** \brief dependent pair projection */ -class expr_proj : public expr_composite { - expr m_expr; - friend expr_cell; - friend expr mk_proj(unsigned idx, expr const & t); - void dealloc(buffer & todelete); -public: - expr_proj(bool first, expr const & e); - expr const & get_arg() const { return m_expr; } -}; - /** \brief Super class for lambda, pi and sigma */ class expr_binder : public expr_composite { name m_name; @@ -334,17 +304,12 @@ inline bool is_constant(expr_cell * e) { return e->kind() == expr_kind::Const inline bool is_local(expr_cell * e) { return e->kind() == expr_kind::Local; } inline bool is_metavar(expr_cell * e) { return e->kind() == expr_kind::Meta; } inline bool is_macro(expr_cell * e) { return e->kind() == expr_kind::Macro; } -inline bool is_dep_pair(expr_cell * e) { return e->kind() == expr_kind::Pair; } -inline bool is_fst(expr_cell * e) { return e->kind() == expr_kind::Fst; } -inline bool is_snd(expr_cell * e) { return e->kind() == expr_kind::Snd; } inline bool is_app(expr_cell * e) { return e->kind() == expr_kind::App; } inline bool is_lambda(expr_cell * e) { return e->kind() == expr_kind::Lambda; } inline bool is_pi(expr_cell * e) { return e->kind() == expr_kind::Pi; } -inline bool is_sigma(expr_cell * e) { return e->kind() == expr_kind::Sigma; } inline bool is_sort(expr_cell * e) { return e->kind() == expr_kind::Sort; } inline bool is_let(expr_cell * e) { return e->kind() == expr_kind::Let; } -inline bool is_binder(expr_cell * e) { return is_lambda(e) || is_pi(e) || is_sigma(e); } -inline bool is_proj(expr_cell * e) { return is_fst(e) || is_snd(e); } +inline bool is_binder(expr_cell * e) { return is_lambda(e) || is_pi(e); } inline bool is_mlocal(expr_cell * e) { return is_metavar(e) || is_local(e); } inline bool is_var(expr const & e) { return e.kind() == expr_kind::Var; } @@ -352,22 +317,16 @@ inline bool is_constant(expr const & e) { return e.kind() == expr_kind::Consta inline bool is_local(expr const & e) { return e.kind() == expr_kind::Local; } inline bool is_metavar(expr const & e) { return e.kind() == expr_kind::Meta; } inline bool is_macro(expr const & e) { return e.kind() == expr_kind::Macro; } -inline bool is_dep_pair(expr const & e) { return e.kind() == expr_kind::Pair; } -inline bool is_fst(expr const & e) { return e.kind() == expr_kind::Fst; } -inline bool is_snd(expr const & e) { return e.kind() == expr_kind::Snd; } inline bool is_app(expr const & e) { return e.kind() == expr_kind::App; } inline bool is_lambda(expr const & e) { return e.kind() == expr_kind::Lambda; } inline bool is_pi(expr const & e) { return e.kind() == expr_kind::Pi; } -inline bool is_sigma(expr const & e) { return e.kind() == expr_kind::Sigma; } inline bool is_sort(expr const & e) { return e.kind() == expr_kind::Sort; } inline bool is_let(expr const & e) { return e.kind() == expr_kind::Let; } -inline bool is_binder(expr const & e) { return is_lambda(e) || is_pi(e) || is_sigma(e); } -inline bool is_proj(expr const & e) { return is_fst(e) || is_snd(e); } +inline bool is_binder(expr const & e) { return is_lambda(e) || is_pi(e); } inline bool is_mlocal(expr const & e) { return is_metavar(e) || is_local(e); } bool is_atomic(expr const & e); bool is_arrow(expr const & t); -bool is_cartesian(expr const & t); // ======================================= // ======================================= @@ -381,10 +340,6 @@ inline expr mk_macro(macro * m) { return expr(new expr_macro(m)); } inline expr mk_mlocal(bool is_meta, name const & n, expr const & t) { return expr(new expr_mlocal(is_meta, n, t)); } inline expr mk_metavar(name const & n, expr const & t) { return mk_mlocal(true, n, t); } inline expr mk_local(name const & n, expr const & t) { return mk_mlocal(false, n, t); } -inline expr mk_pair(expr const & f, expr const & s, expr const & t) { return expr(new expr_dep_pair(f, s, t)); } -inline expr mk_proj(bool first, expr const & a) { return expr(new expr_proj(first, a)); } -inline expr mk_fst(expr const & a) { return mk_proj(true, a); } -inline expr mk_snd(expr const & a) { return mk_proj(false, a); } inline expr mk_app(expr const & f, expr const & a) { return expr(new expr_app(f, a)); } expr mk_app(expr const & f, unsigned num_args, expr const * args); expr mk_app(unsigned num_args, expr const * args); @@ -396,7 +351,6 @@ template expr mk_rev_app(T const & args) { return mk_rev_app(args.si inline expr mk_binder(expr_kind k, name const & n, expr const & t, expr const & e) { return expr(new expr_binder(k, n, t, e)); } inline expr mk_lambda(name const & n, expr const & t, expr const & e) { return mk_binder(expr_kind::Lambda, n, t, e); } inline expr mk_pi(name const & n, expr const & t, expr const & e) { return mk_binder(expr_kind::Pi, n, t, e); } -inline expr mk_sigma(name const & n, expr const & t, expr const & e) { return mk_binder(expr_kind::Sigma, n, t, e); } inline expr mk_let(name const & n, expr const & t, expr const & v, expr const & e) { return expr(new expr_let(n, t, v, e)); } inline expr mk_sort(level const & l) { return expr(new expr_sort(l)); } @@ -407,7 +361,6 @@ extern expr Bool; bool is_default_var_name(name const & n); expr mk_arrow(expr const & t, expr const & e); -expr mk_cartesian_product(expr const & t, expr const & e); inline expr operator>>(expr const & t, expr const & e) { return mk_arrow(t, e); } // Auxiliary @@ -443,8 +396,6 @@ inline expr expr::operator()(expr const & a1, expr const & a2, expr const & a3, // Casting (these functions are only needed for low-level code) inline expr_var * to_var(expr_cell * e) { lean_assert(is_var(e)); return static_cast(e); } inline expr_const * to_constant(expr_cell * e) { lean_assert(is_constant(e)); return static_cast(e); } -inline expr_dep_pair * to_pair(expr_cell * e) { lean_assert(is_dep_pair(e)); return static_cast(e); } -inline expr_proj * to_proj(expr_cell * e) { lean_assert(is_proj(e)); return static_cast(e); } inline expr_app * to_app(expr_cell * e) { lean_assert(is_app(e)); return static_cast(e); } inline expr_binder * to_binder(expr_cell * e) { lean_assert(is_binder(e)); return static_cast(e); } inline expr_let * to_let(expr_cell * e) { lean_assert(is_let(e)); return static_cast(e); } @@ -455,8 +406,6 @@ inline expr_mlocal * to_metavar(expr_cell * e) { lean_assert(is_metavar( inline expr_var * to_var(expr const & e) { return to_var(e.raw()); } inline expr_const * to_constant(expr const & e) { return to_constant(e.raw()); } -inline expr_dep_pair * to_pair(expr const & e) { return to_pair(e.raw()); } -inline expr_proj * to_proj(expr const & e) { return to_proj(e.raw()); } inline expr_app * to_app(expr const & e) { return to_app(e.raw()); } inline expr_binder * to_binder(expr const & e) { return to_binder(e.raw()); } inline expr_let * to_let(expr const & e) { return to_let(e.raw()); } @@ -475,10 +424,6 @@ inline unsigned var_idx(expr_cell * e) { return to_var(e)->ge inline bool is_var(expr_cell * e, unsigned i) { return is_var(e) && var_idx(e) == i; } inline name const & const_name(expr_cell * e) { return to_constant(e)->get_name(); } inline levels const & const_level_params(expr_cell * e) { return to_constant(e)->get_level_params(); } -inline expr const & pair_first(expr_cell * e) { return to_pair(e)->get_first(); } -inline expr const & pair_second(expr_cell * e) { return to_pair(e)->get_second(); } -inline expr const & pair_type(expr_cell * e) { return to_pair(e)->get_type(); } -inline expr const & proj_arg(expr_cell * e) { return to_proj(e)->get_arg(); } inline macro const & to_macro(expr_cell * e) { lean_assert(is_macro(e)); return static_cast(e)->get_macro(); } inline expr const & app_fn(expr_cell * e) { return to_app(e)->get_fn(); } @@ -500,10 +445,6 @@ inline unsigned var_idx(expr const & e) { return to_var(e)->g inline bool is_var(expr const & e, unsigned i) { return is_var(e) && var_idx(e) == i; } inline name const & const_name(expr const & e) { return to_constant(e)->get_name(); } inline levels const & const_level_params(expr const & e) { return to_constant(e)->get_level_params(); } -inline expr const & pair_first(expr const & e) { return to_pair(e)->get_first(); } -inline expr const & pair_second(expr const & e) { return to_pair(e)->get_second(); } -inline expr const & pair_type(expr const & e) { return to_pair(e)->get_type(); } -inline expr const & proj_arg(expr const & e) { return to_proj(e)->get_arg(); } inline macro const & to_macro(expr const & e) { return to_macro(e.raw()); } inline expr const & app_fn(expr const & e) { return to_app(e)->get_fn(); } inline expr const & app_arg(expr const & e) { return to_app(e)->get_arg(); } @@ -569,8 +510,6 @@ expr copy(expr const & e); expr update_app(expr const & e, expr const & new_fn, expr const & new_arg); expr update_rev_app(expr const & e, unsigned num, expr const * new_args); template expr update_rev_app(expr const & e, C const & c) { return update_rev_app(e, c.size(), c.data()); } -expr update_proj(expr const & e, expr const & new_arg); -expr update_pair(expr const & e, expr const & new_first, expr const & new_second, expr const & new_type); expr update_binder(expr const & e, expr const & new_domain, expr const & new_body); expr update_let(expr const & e, expr const & new_type, expr const & new_val, expr const & new_body); expr update_mlocal(expr const & e, expr const & new_type); diff --git a/src/kernel/expr_eq_fn.cpp b/src/kernel/expr_eq_fn.cpp index c216970a6..f4a7f8e48 100644 --- a/src/kernel/expr_eq_fn.cpp +++ b/src/kernel/expr_eq_fn.cpp @@ -36,14 +36,7 @@ bool expr_eq_fn::apply(expr const & a, expr const & b) { return apply(app_fn(a), app_fn(b)) && apply(app_arg(a), app_arg(b)); - case expr_kind::Pair: - return - apply(pair_first(a), pair_first(b)) && - apply(pair_second(a), pair_second(b)) && - apply(pair_type(a), pair_type(b)); - case expr_kind::Fst: case expr_kind::Snd: - return apply(proj_arg(a), proj_arg(b)); - case expr_kind::Sigma: case expr_kind::Lambda: case expr_kind::Pi: + case expr_kind::Lambda: case expr_kind::Pi: return apply(binder_domain(a), binder_domain(b)) && apply(binder_body(a), binder_body(b)); diff --git a/src/kernel/for_each_fn.cpp b/src/kernel/for_each_fn.cpp index 2c49d8a9b..3162eb874 100644 --- a/src/kernel/for_each_fn.cpp +++ b/src/kernel/for_each_fn.cpp @@ -52,15 +52,7 @@ void for_each_fn::apply(expr const & e, unsigned offset) { todo.emplace_back(app_arg(e), offset); todo.emplace_back(app_fn(e), offset); goto begin_loop; - case expr_kind::Pair: - todo.emplace_back(pair_type(e), offset); - todo.emplace_back(pair_second(e), offset); - todo.emplace_back(pair_first(e), offset); - goto begin_loop; - case expr_kind::Fst: case expr_kind::Snd: - todo.emplace_back(proj_arg(e), offset); - goto begin_loop; - case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Sigma: + case expr_kind::Lambda: case expr_kind::Pi: todo.emplace_back(binder_body(e), offset + 1); todo.emplace_back(binder_domain(e), offset); goto begin_loop; diff --git a/src/kernel/formatter.cpp b/src/kernel/formatter.cpp index 909996c39..48c858641 100644 --- a/src/kernel/formatter.cpp +++ b/src/kernel/formatter.cpp @@ -58,15 +58,6 @@ struct print_expr_fn { return print_child(a, c); } - void print_pair(expr const & e, context const & c) { - out() << "pair "; - print_child(pair_first(e), c); - out() << " "; - print_child(pair_second(e), c); - out() << " "; - print_child(pair_type(e), c); - } - void print_binder(char const * bname, expr const & e, context const & c) { out() << bname << " " << binder_name(e) << " : "; print_child(binder_domain(e), c); @@ -93,16 +84,6 @@ struct print_expr_fn { case expr_kind::App: print_app(a, c); break; - case expr_kind::Pair: - print_pair(a, c); - break; - case expr_kind::Fst: case expr_kind::Snd: - out() << (is_fst(a) ? "fst" : "snd") << " "; - print_child(proj_arg(a), c); - break; - case expr_kind::Sigma: - print_binder("sig", a, c); - break; case expr_kind::Lambda: print_binder("fun", a, c); break; diff --git a/src/kernel/free_vars.cpp b/src/kernel/free_vars.cpp index 2b434818d..4ee956673 100644 --- a/src/kernel/free_vars.cpp +++ b/src/kernel/free_vars.cpp @@ -31,8 +31,7 @@ protected: return var_idx(e) >= offset; case expr_kind::App: case expr_kind::Let: case expr_kind::Meta: case expr_kind::Local: - case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Sigma: - case expr_kind::Pair: case expr_kind::Fst: case expr_kind::Snd: + case expr_kind::Lambda: case expr_kind::Pi: break; } @@ -69,18 +68,12 @@ protected: case expr_kind::App: result = apply(app_fn(e), offset) || apply(app_arg(e), offset); break; - case expr_kind::Fst: case expr_kind::Snd: - result = apply(proj_arg(e), offset); - break; - case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Sigma: + case expr_kind::Lambda: case expr_kind::Pi: result = apply(binder_domain(e), offset) || apply(binder_body(e), offset + 1); break; case expr_kind::Let: result = apply(let_type(e), offset) || apply(let_value(e), offset) || apply(let_body(e), offset + 1); break; - case expr_kind::Pair: - result = apply(pair_first(e), offset) || apply(pair_second(e), offset) || apply(pair_type(e), offset); - break; } if (!result) { @@ -119,8 +112,7 @@ class free_var_range_fn { return var_idx(e) + 1; case expr_kind::App: case expr_kind::Let: case expr_kind::Meta: case expr_kind::Local: - case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Sigma: - case expr_kind::Pair: case expr_kind::Fst: case expr_kind::Snd: + case expr_kind::Lambda: case expr_kind::Pi: break; } @@ -147,18 +139,12 @@ class free_var_range_fn { case expr_kind::App: result = std::max(apply(app_fn(e)), apply(app_arg(e))); break; - case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Sigma: + case expr_kind::Lambda: case expr_kind::Pi: result = std::max(apply(binder_domain(e)), dec(apply(binder_body(e)))); break; case expr_kind::Let: result = std::max({apply(let_type(e)), apply(let_value(e)), dec(apply(let_body(e)))}); break; - case expr_kind::Fst: case expr_kind::Snd: - result = apply(proj_arg(e)); - break; - case expr_kind::Pair: - result = std::max({apply(pair_first(e)), apply(pair_second(e)), apply(pair_type(e))}); - break; } if (shared) @@ -215,8 +201,7 @@ protected: return in_interval(var_idx(e), offset); case expr_kind::App: case expr_kind::Let: case expr_kind::Meta: case expr_kind::Local: - case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Sigma: - case expr_kind::Pair: case expr_kind::Fst: case expr_kind::Snd: + case expr_kind::Lambda: case expr_kind::Pi: break; } @@ -243,18 +228,12 @@ protected: case expr_kind::App: result = apply(app_fn(e), offset) || apply(app_arg(e), offset); break; - case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Sigma: + case expr_kind::Lambda: case expr_kind::Pi: result = apply(binder_domain(e), offset) || apply(binder_body(e), offset + 1); break; case expr_kind::Let: result = apply(let_type(e), offset) || apply(let_value(e), offset) || apply(let_body(e), offset + 1); break; - case expr_kind::Fst: case expr_kind::Snd: - result = apply(proj_arg(e), offset); - break; - case expr_kind::Pair: - result = apply(pair_first(e), offset) || apply(pair_second(e), offset) || apply(pair_type(e), offset); - break; } if (!result && shared) { diff --git a/src/kernel/max_sharing.cpp b/src/kernel/max_sharing.cpp index d95e72a6f..0e88dac5b 100644 --- a/src/kernel/max_sharing.cpp +++ b/src/kernel/max_sharing.cpp @@ -43,16 +43,10 @@ struct max_sharing_fn::imp { case expr_kind::Sort: case expr_kind::Macro: res = a; break; - case expr_kind::Pair: - res = update_pair(a, apply(pair_first(a)), apply(pair_second(a)), apply(pair_type(a))); - break; - case expr_kind::Fst: case expr_kind::Snd: - res = update_proj(a, apply(proj_arg(a))); - break; - case expr_kind::App: + case expr_kind::App: res = update_app(a, apply(app_fn(a)), apply(app_arg(a))); break; - case expr_kind::Sigma: case expr_kind::Lambda: case expr_kind::Pi: + case expr_kind::Lambda: case expr_kind::Pi: res = update_binder(a, apply(binder_domain(a)), apply(binder_body(a))); break; case expr_kind::Let: diff --git a/src/kernel/normalizer.cpp b/src/kernel/normalizer.cpp index cb5be6dc2..4b82dc2fb 100644 --- a/src/kernel/normalizer.cpp +++ b/src/kernel/normalizer.cpp @@ -97,7 +97,7 @@ class normalizer::imp { expr reify(expr const & v, unsigned k) { return replace(v, [&](expr const & e, unsigned DEBUG_CODE(offset)) -> optional { lean_assert(offset == 0); - lean_assert(!is_lambda(e) && !is_pi(e) && !is_sigma(e) && !is_let(e)); + lean_assert(!is_lambda(e) && !is_pi(e) && !is_let(e)); if (is_var(e)) { // de Bruijn level --> de Bruijn index return some_expr(mk_var(k - var_idx(e) - 1)); @@ -137,7 +137,7 @@ class normalizer::imp { expr r; switch (a.kind()) { - case expr_kind::Sigma: case expr_kind::Pi: case expr_kind::Lambda: + case expr_kind::Pi: case expr_kind::Lambda: r = mk_closure(a, s); break; case expr_kind::Var: @@ -154,25 +154,6 @@ class normalizer::imp { } break; } - case expr_kind::Pair: { - expr new_first = normalize(pair_first(a), s, k); - expr new_second = normalize(pair_second(a), s, k); - expr new_type = normalize(pair_type(a), s, k); - r = update_pair(a, new_first, new_second, new_type); - break; - } - case expr_kind::Fst: case expr_kind::Snd: { - expr new_arg = normalize(proj_arg(a), s, k); - if (is_dep_pair(new_arg)) { - if (is_fst(a)) - r = pair_first(new_arg); - else - r = pair_second(new_arg); - } else { - r = update_proj(a, new_arg); - } - break; - } case expr_kind::Sort: case expr_kind::Macro: case expr_kind::Local: case expr_kind::Meta: r = a; break; diff --git a/src/kernel/replace_fn.cpp b/src/kernel/replace_fn.cpp index 818b48909..dbfa35f98 100644 --- a/src/kernel/replace_fn.cpp +++ b/src/kernel/replace_fn.cpp @@ -85,22 +85,6 @@ expr replace_fn::operator()(expr const & e) { r = update_mlocal(e, rs(-1)); pop_rs(1); break; - case expr_kind::Pair: - if (check_index(f, 0) && !visit(pair_first(e), offset)) - goto begin_loop; - if (check_index(f, 1) && !visit(pair_second(e), offset)) - goto begin_loop; - if (check_index(f, 2) && !visit(pair_type(e), offset)) - goto begin_loop; - r = update_pair(e, rs(-3), rs(-2), rs(-1)); - pop_rs(3); - break; - case expr_kind::Fst: case expr_kind::Snd: - if (check_index(f, 0) && !visit(proj_arg(e), offset)) - goto begin_loop; - r = update_proj(e, rs(-1)); - pop_rs(1); - break; case expr_kind::App: if (check_index(f, 0) && !visit(app_fn(e), offset)) goto begin_loop; @@ -109,7 +93,7 @@ expr replace_fn::operator()(expr const & e) { r = update_app(e, rs(-2), rs(-1)); pop_rs(2); break; - case expr_kind::Sigma: case expr_kind::Pi: case expr_kind::Lambda: + case expr_kind::Pi: case expr_kind::Lambda: if (check_index(f, 0) && !visit(binder_domain(e), offset)) goto begin_loop; if (check_index(f, 1) && !visit(binder_body(e), offset + 1)) diff --git a/src/kernel/replace_visitor.cpp b/src/kernel/replace_visitor.cpp index b7e11fc7d..8f97f24ea 100644 --- a/src/kernel/replace_visitor.cpp +++ b/src/kernel/replace_visitor.cpp @@ -20,16 +20,6 @@ expr replace_visitor::visit_mlocal(expr const & e, context const & ctx) { } expr replace_visitor::visit_meta(expr const & e, context const & ctx) { return visit_mlocal(e, ctx); } expr replace_visitor::visit_local(expr const & e, context const & ctx) { return visit_mlocal(e, ctx); } -expr replace_visitor::visit_pair(expr const & e, context const & ctx) { - lean_assert(is_dep_pair(e)); - return update_pair(e, visit(pair_first(e), ctx), visit(pair_second(e), ctx), visit(pair_type(e), ctx)); -} -expr replace_visitor::visit_proj(expr const & e, context const & ctx) { - lean_assert(is_proj(e)); - return update_proj(e, visit(proj_arg(e), ctx)); -} -expr replace_visitor::visit_fst(expr const & e, context const & ctx) { return visit_proj(e, ctx); } -expr replace_visitor::visit_snd(expr const & e, context const & ctx) { return visit_proj(e, ctx); } expr replace_visitor::visit_app(expr const & e, context const & ctx) { lean_assert(is_app(e)); return update_app(e, visit(app_fn(e), ctx), visit(app_arg(e), ctx)); @@ -43,7 +33,6 @@ expr replace_visitor::visit_binder(expr const & e, context const & ctx) { } expr replace_visitor::visit_lambda(expr const & e, context const & ctx) { return visit_binder(e, ctx); } expr replace_visitor::visit_pi(expr const & e, context const & ctx) { return visit_binder(e, ctx); } -expr replace_visitor::visit_sigma(expr const & e, context const & ctx) { return visit_binder(e, ctx); } expr replace_visitor::visit_let(expr const & e, context const & ctx) { lean_assert(is_let(e)); expr new_t = visit(let_type(e), ctx); @@ -74,13 +63,9 @@ expr replace_visitor::visit(expr const & e, context const & ctx) { case expr_kind::Var: return save_result(e, visit_var(e, ctx), shared); case expr_kind::Meta: return save_result(e, visit_meta(e, ctx), shared); case expr_kind::Local: return save_result(e, visit_local(e, ctx), shared); - case expr_kind::Pair: return save_result(e, visit_pair(e, ctx), shared); - case expr_kind::Fst: return save_result(e, visit_fst(e, ctx), shared); - case expr_kind::Snd: return save_result(e, visit_snd(e, ctx), shared); case expr_kind::App: return save_result(e, visit_app(e, ctx), shared); case expr_kind::Lambda: return save_result(e, visit_lambda(e, ctx), shared); case expr_kind::Pi: return save_result(e, visit_pi(e, ctx), shared); - case expr_kind::Sigma: return save_result(e, visit_sigma(e, ctx), shared); case expr_kind::Let: return save_result(e, visit_let(e, ctx), shared); } diff --git a/src/kernel/replace_visitor.h b/src/kernel/replace_visitor.h index 82682ec47..5b9a36cfb 100644 --- a/src/kernel/replace_visitor.h +++ b/src/kernel/replace_visitor.h @@ -31,15 +31,10 @@ protected: virtual expr visit_mlocal(expr const &, context const &); virtual expr visit_meta(expr const &, context const &); virtual expr visit_local(expr const &, context const &); - virtual expr visit_pair(expr const &, context const &); - virtual expr visit_proj(expr const &, context const &); - virtual expr visit_fst(expr const &, context const &); - virtual expr visit_snd(expr const &, context const &); virtual expr visit_app(expr const &, context const &); virtual expr visit_binder(expr const &, context const &); virtual expr visit_lambda(expr const &, context const &); virtual expr visit_pi(expr const &, context const &); - virtual expr visit_sigma(expr const &, context const &); virtual expr visit_let(expr const &, context const &); virtual expr visit(expr const &, context const &); diff --git a/src/library/deep_copy.cpp b/src/library/deep_copy.cpp index 30a250148..7325c0fd9 100644 --- a/src/library/deep_copy.cpp +++ b/src/library/deep_copy.cpp @@ -28,12 +28,8 @@ class deep_copy_fn { case expr_kind::Sort: case expr_kind::Macro: r = copy(a); break; case expr_kind::App: r = mk_app(apply(app_fn(a)), apply(app_arg(a))); break; - case expr_kind::Pair: r = mk_pair(apply(pair_first(a)), apply(pair_second(a)), apply(pair_type(a))); break; - 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; diff --git a/src/library/expr_lt.cpp b/src/library/expr_lt.cpp index da5da3932..cabc8990b 100644 --- a/src/library/expr_lt.cpp +++ b/src/library/expr_lt.cpp @@ -71,16 +71,7 @@ bool is_lt(expr const & a, expr const & b, bool use_hash) { return is_lt(app_fn(a), app_fn(b), use_hash); else return is_lt(app_arg(a), app_arg(b), use_hash); - case expr_kind::Pair: - if (pair_first(a) != pair_first(b)) - return is_lt(pair_first(a), pair_first(b), use_hash); - else if (pair_second(a) != pair_second(b)) - return is_lt(pair_second(a), pair_second(b), use_hash); - else - return is_lt(pair_type(a), pair_type(b), use_hash); - case expr_kind::Fst: case expr_kind::Snd: - return is_lt(proj_arg(a), proj_arg(b), use_hash); - case expr_kind::Sigma: case expr_kind::Lambda: case expr_kind::Pi: + case expr_kind::Lambda: case expr_kind::Pi: if (binder_domain(a) != binder_domain(b)) return is_lt(binder_domain(a), binder_domain(b), use_hash); else diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp index ee49b07f9..dcac5f47e 100644 --- a/src/tests/kernel/expr.cpp +++ b/src/tests/kernel/expr.cpp @@ -110,14 +110,10 @@ static unsigned count_core(expr const & a, expr_set & s) { return 1; case expr_kind::App: return count_core(app_fn(a), s) + count_core(app_arg(a), s) + 1; - case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Sigma: + case expr_kind::Lambda: case expr_kind::Pi: return count_core(binder_domain(a), s) + count_core(binder_body(a), s) + 1; case expr_kind::Let: return count_core(let_value(a), s) + count_core(let_body(a), s) + 1; - case expr_kind::Fst: case expr_kind::Snd: - return count_core(proj_arg(a), s) + 1; - case expr_kind::Pair: - return count_core(pair_first(a), s) + count_core(pair_second(a), s) + count_core(pair_type(a), s) + 1; } return 0; } @@ -303,15 +299,6 @@ static void tst15() { lean_assert(has_metavar(f(a, a, m))); lean_assert(has_metavar(f(a, m, a, a))); lean_assert(!has_metavar(f(a, a, a, a))); - lean_assert(!has_metavar(mk_fst(a))); - lean_assert(!has_metavar(mk_snd(a))); - lean_assert(has_metavar(mk_fst(m))); - lean_assert(has_metavar(mk_snd(m))); - lean_assert(!has_metavar(mk_pair(a, x, x))); - lean_assert(has_metavar(mk_pair(f(m), x, x))); - lean_assert(has_metavar(mk_pair(f(a), m, x))); - lean_assert(has_metavar(mk_pair(f(a), a, m))); - lean_assert(has_metavar(mk_pair(f(a), a, f(m)))); } static void check_copy(expr const & e) { @@ -376,21 +363,6 @@ static void tst18() { lean_assert(has_local(f(a, a, l))); lean_assert(has_local(f(a, l, a, a))); lean_assert(!has_local(f(a, a, a, a))); - lean_assert(!has_local(mk_fst(a))); - lean_assert(!has_local(mk_snd(a))); - lean_assert(has_local(mk_fst(l))); - lean_assert(has_local(mk_snd(l))); - lean_assert(!has_local(mk_fst(m))); - lean_assert(!has_local(mk_snd(m))); - lean_assert(!has_local(mk_pair(a, x, x))); - lean_assert(has_local(mk_pair(f(l), x, x))); - lean_assert(has_local(mk_pair(f(a), l, x))); - lean_assert(has_local(mk_pair(f(a), a, l))); - lean_assert(has_local(mk_pair(f(a), a, f(l)))); - lean_assert(!has_local(mk_pair(f(m), x, x))); - lean_assert(!has_local(mk_pair(f(a), m, x))); - lean_assert(!has_local(mk_pair(f(a), a, m))); - lean_assert(!has_local(mk_pair(f(a), a, f(m)))); } int main() { diff --git a/src/tests/kernel/normalizer.cpp b/src/tests/kernel/normalizer.cpp index e0cfee19e..3f6ad2a2a 100644 --- a/src/tests/kernel/normalizer.cpp +++ b/src/tests/kernel/normalizer.cpp @@ -68,14 +68,10 @@ unsigned count_core(expr const & a, expr_set & s) { return 1; case expr_kind::App: return count_core(app_fn(a), s) + count_core(app_arg(a), s) + 1; - case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Sigma: + case expr_kind::Lambda: case expr_kind::Pi: return count_core(binder_domain(a), s) + count_core(binder_body(a), s) + 1; case expr_kind::Let: return count_core(let_value(a), s) + count_core(let_body(a), s) + 1; - case expr_kind::Fst: case expr_kind::Snd: - return count_core(proj_arg(a), s) + 1; - case expr_kind::Pair: - return count_core(pair_first(a), s) + count_core(pair_second(a), s) + count_core(pair_type(a), s) + 1; } return 0; }