refactor(kernel): remove pairs from kernel

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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<expr_cell*> & 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<expr_cell*> & 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<expr_cell*> & 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<expr_cell*> & todelete) {
     dec_ref(m_body, todelete);
@@ -246,13 +220,9 @@ void expr_cell::dealloc() {
             case expr_kind::Local:      static_cast<expr_mlocal*>(it)->dealloc(todo); break;
             case expr_kind::Constant:   delete static_cast<expr_const*>(it); break;
             case expr_kind::Sort:       delete static_cast<expr_sort*>(it); break;
-            case expr_kind::Pair:       static_cast<expr_dep_pair*>(it)->dealloc(todo); break;
-            case expr_kind::Fst:
-            case expr_kind::Snd:        static_cast<expr_proj*>(it)->dealloc(todo); break;
             case expr_kind::App:        static_cast<expr_app*>(it)->dealloc(todo); break;
             case expr_kind::Lambda:
-            case expr_kind::Pi:
+            case expr_kind::Pi:         static_cast<expr_binder*>(it)->dealloc(todo); break;
-            case expr_kind::Sigma:      static_cast<expr_binder*>(it)->dealloc(todo); break;
             case expr_kind::Let:        static_cast<expr_let*>(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::Lambda: case expr_kind::Pi:
-    case expr_kind::Pair:   case expr_kind::Fst:  case expr_kind::Snd:
     case expr_kind::App:    case expr_kind::Let:
         return static_cast<expr_composite*>(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::Lambda:   case expr_kind::Pi:
-    case expr_kind::Pair:     case expr_kind::Fst: case expr_kind::Snd:
         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<expr_macro*>(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<expr, expr_hash_alloc, expr_eqp
                 case expr_kind::Macro:
                     to_macro(a).write(s);
                     break;
-                case expr_kind::Pair:
-                    write_core(pair_first(a)); write_core(pair_second(a)); write_core(pair_type(a));
-                    break;
-                case expr_kind::Fst:  case expr_kind::Snd:
-                    write_core(proj_arg(a));
-                    break;
                 case expr_kind::App:
                     write_core(app_fn(a)); write_core(app_arg(a));
                     break;
-                case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Sigma:
+                case expr_kind::Lambda: case expr_kind::Pi:
                     s << binder_name(a); write_core(binder_domain(a)); write_core(binder_body(a));
                     break;
                 case expr_kind::Let:
@@ -506,20 +445,11 @@ public:
                     break;
                 case expr_kind::Macro:
                     return read_macro(d);
-                case expr_kind::Pair: {
-                    expr f = read();
-                    expr s = read();
-                    return mk_pair(f, s, read());
-                }
-                case expr_kind::Fst:
-                    return mk_fst(read());
-                case expr_kind::Snd:
-                    return mk_snd(read());
                 case expr_kind::App: {
                     expr f = read();
                     return mk_app(f, read());
                 }
-                case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Sigma:
+                case expr_kind::Lambda: case expr_kind::Pi:
                     return read_binder(k);
                 case expr_kind::Let: {
                     name n = read_name(d);

src/kernel/expr.h

@@ -33,17 +33,13 @@ class expr;
           |   Meta          name expr
           |   Local         name expr
           |   App           expr expr
-          |   Pair          expr expr expr
-          |   Fst           expr
-          |   Snd           expr
           |   Lambda        name expr expr
           |   Pi            name expr expr
-          |   Sigma         name expr expr
           |   Let           name expr expr expr
 
           |   Macro         macro
 */
-enum class expr_kind { Var, Sort, Constant, Meta, Local, App, Pair, Fst, Snd, Lambda, Pi, Sigma, Let, Macro };
+enum class expr_kind { Var, Sort, Constant, Meta, Local, App, Lambda, Pi, Let, Macro };
 class expr_cell {
 protected:
     unsigned short     m_kind;
@@ -215,32 +211,6 @@ public:
     expr const & get_arg() const { return m_arg; }
 };
 
-/** \brief dependent pairs */
-class expr_dep_pair : public expr_composite {
-    expr     m_first;
-    expr     m_second;
-    expr     m_type;
-    friend expr mk_pair(expr const & f, expr const & s, expr const & t);
-    friend expr_cell;
-    void dealloc(buffer<expr_cell*> & 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<expr_cell*> & 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_binder(expr_cell * e)      { return is_lambda(e) || is_pi(e); }
-inline bool is_proj(expr_cell * e)        { return is_fst(e) || is_snd(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_binder(expr const & e)     { return is_lambda(e) || is_pi(e); }
-inline bool is_proj(expr const & e)       { return is_fst(e) || is_snd(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<typename T> 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<expr_var*>(e); }
 inline expr_const *       to_constant(expr_cell * e)   { lean_assert(is_constant(e));    return static_cast<expr_const*>(e); }
-inline expr_dep_pair *    to_pair(expr_cell * e)       { lean_assert(is_dep_pair(e));    return static_cast<expr_dep_pair*>(e); }
-inline expr_proj *        to_proj(expr_cell * e)       { lean_assert(is_proj(e));        return static_cast<expr_proj*>(e); }
 inline expr_app *         to_app(expr_cell * e)        { lean_assert(is_app(e));         return static_cast<expr_app*>(e); }
 inline expr_binder *      to_binder(expr_cell * e)     { lean_assert(is_binder(e));      return static_cast<expr_binder*>(e); }
 inline expr_let *         to_let(expr_cell * e)        { lean_assert(is_let(e));         return static_cast<expr_let*>(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<expr_macro*>(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<typename C> 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);

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:
+    case expr_kind::Lambda: case expr_kind::Pi:
-        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:
         return
             apply(binder_domain(a), binder_domain(b)) &&
             apply(binder_body(a), binder_body(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:
+        case expr_kind::Lambda: case expr_kind::Pi:
-            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:
             todo.emplace_back(binder_body(e), offset + 1);
             todo.emplace_back(binder_domain(e), offset);
             goto begin_loop;

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;

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::Lambda: case expr_kind::Pi:
-        case expr_kind::Pair:   case expr_kind::Fst: case expr_kind::Snd:
             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:
+        case expr_kind::Lambda: case expr_kind::Pi:
-            result = apply(proj_arg(e), offset);
-            break;
-        case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Sigma:
             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::Lambda: case expr_kind::Pi:
-        case expr_kind::Pair:   case expr_kind::Fst: case expr_kind::Snd:
             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::Lambda: case expr_kind::Pi:
-        case expr_kind::Pair:   case expr_kind::Fst: case expr_kind::Snd:
             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) {

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:
+          case expr_kind::App:
-            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:
             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:

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<expr> {
                 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;

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))

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);
     }
 

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 &);
 

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;

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:
+    case expr_kind::Lambda: case expr_kind::Pi:
-        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:
         if (binder_domain(a) != binder_domain(b))
             return is_lt(binder_domain(a), binder_domain(b), use_hash);
         else

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() {

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;
 }