feat(frontends/lean): parse and pretty print pair/tuple projection operators proj1 and proj2, fix bug in the type checker

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

src/frontends/lean/parser_expr.cpp

@@ -891,6 +891,29 @@ expr parser_imp::parse_tuple() {
     }
 }
 
+expr parser_imp::parse_proj(bool first) {
+    auto p = pos();
+    next();
+    unsigned i = 0;
+    if (curr() == scanner::token::IntVal) {
+        i = parse_unsigned("invalid tuple/pair projection, index does not fit in a machine integer");
+        if (i == 0)
+            throw parser_error("invalid tuple/pair projection, optional index must be >= 1", p);
+        if (i > LEAN_MAX_PROJECTION)
+            throw parser_error(sstream() << "invalid tuple/pair projection, optional index is >= "
+                               << LEAN_MAX_PROJECTION << " (internal limit)", p);
+    }
+    expr t = parse_expr();
+    while (i > 0) {
+        --i;
+        t = save(mk_proj2(t), p);
+    }
+    if (first)
+        return save(mk_proj1(t), p);
+    else
+        return save(mk_proj2(t), p);
+}
+
 /** \brief Parse \c _ a hole that must be filled by the elaborator. */
 expr parser_imp::parse_placeholder() {
     auto p = pos();
@@ -1004,6 +1027,8 @@ expr parser_imp::parse_nud() {
     case scanner::token::Type:        return parse_type(false);
     case scanner::token::Have:        return parse_have_expr();
     case scanner::token::Tuple:       return parse_tuple();
+    case scanner::token::Proj1:       return parse_proj(true);
+    case scanner::token::Proj2:       return parse_proj(false);
     case scanner::token::By:          return parse_by_expr();
     default:
         throw parser_error("invalid expression, unexpected token", pos());

src/frontends/lean/parser_imp.h

@@ -25,6 +25,17 @@ Author: Leonardo de Moura
 #include "frontends/lean/operator_info.h"
 #include "frontends/lean/frontend_elaborator.h"
 
+// Lean encodes
+//    proj1 i t
+// as
+//    proj1 (proj2 (proj2 ... t) ...)
+// So, a big \c i may make Lean run out of memory.
+// The default limit is 10000. I don't believe anybody needs to create a tuple with
+// more than 10000 entries
+#ifndef LEAN_MAX_PROJECTION
+#define LEAN_MAX_PROJECTION 10000
+#endif
+
 namespace lean {
 class parser_imp;
 class calc_proof_parser;
@@ -306,6 +317,7 @@ private:
     expr parse_let();
     expr parse_type(bool level_expected);
     expr parse_tuple();
+    expr parse_proj(bool first);
     tactic parse_tactic_macro(name tac_id, pos_info const & p);
     expr parse_have_expr();
     expr parse_calc();

src/frontends/lean/pp.cpp

@@ -77,6 +77,8 @@ static format g_ellipsis_fmt  = highlight(format("..."));
 static format g_let_fmt       = highlight_keyword(format("let"));
 static format g_in_fmt        = highlight_keyword(format("in"));
 static format g_tuple_fmt     = highlight_keyword(format("tuple"));
+static format g_proj1_fmt     = highlight_keyword(format("proj1"));
+static format g_proj2_fmt     = highlight_keyword(format("proj2"));
 static format g_assign_fmt    = highlight_keyword(format(":="));
 static format g_geq_fmt       = format("\u2265");
 static format g_lift_fmt      = highlight_keyword(format("lift"));
@@ -1144,6 +1146,23 @@ class pp_fn {
         return result(group(r_format), r_weight);
     }
 
+    result pp_proj(expr a, unsigned depth) {
+        unsigned i = 0;
+        bool first = proj_first(a);
+        while (is_proj(proj_arg(a)) && !proj_first(proj_arg(a))) {
+            a = proj_arg(a);
+            i++;
+        }
+        auto arg_r = pp_child(proj_arg(a), depth);
+        unsigned indent   = 6;
+        format r_format   = first ? g_proj1_fmt : g_proj2_fmt;
+        unsigned r_weight = 1 + arg_r.second;;
+        if (i > 0)
+            r_format += format{space(), format(i)};
+        r_format += nest(indent, compose(line(), arg_r.first));
+        return result(group(r_format), r_weight);
+    }
+
     result pp(expr const & e, unsigned depth, bool main = false) {
         check_system("pretty printer");
         if (!is_atomic(e) && (m_num_steps > m_max_steps || depth > m_max_depth)) {
@@ -1181,6 +1200,7 @@ class pp_fn {
                 case expr_kind::Let:        r = pp_let(e, depth);         break;
                 case expr_kind::MetaVar:    r = pp_metavar(e, depth);     break;
                 case expr_kind::Pair:       r = pp_tuple(e, depth);       break;
+                case expr_kind::Proj:       r = pp_proj(e, depth);        break;
                 }
             }
             if (!main && m_extra_lets && has_several_occs(e) && r.second > m_alias_min_weight) {

src/frontends/lean/scanner.cpp

@@ -31,7 +31,8 @@ static name g_using_name("using");
 static name g_by_name("by");
 static name g_sig_name("sig");
 static name g_tuple_name("tuple");
-static name g_proj_name("proj");
+static name g_proj1_name("proj1");
+static name g_proj2_name("proj2");
 static name g_cartesian_product_unicode("\u2A2F");
 static name g_cartesian_product("#");
 
@@ -214,8 +215,10 @@ scanner::token scanner::read_a_symbol() {
                 return token::Sig;
             } else if (m_name_val == g_tuple_name) {
                 return token::Tuple;
-            } else if (m_name_val == g_proj_name) {
-                return token::Proj;
+            } else if (m_name_val == g_proj1_name) {
+                return token::Proj1;
+            } else if (m_name_val == g_proj2_name) {
+                return token::Proj2;
             } else if (m_name_val == g_placeholder_name) {
                 return token::Placeholder;
             } else if (m_name_val == g_have_name) {
@@ -460,7 +463,8 @@ std::ostream & operator<<(std::ostream & out, scanner::token const & t) {
     case scanner::token::Assign:            out << ":="; break;
     case scanner::token::Type:              out << "Type"; break;
     case scanner::token::Sig:               out << "sig"; break;
-    case scanner::token::Proj:              out << "proj"; break;
+    case scanner::token::Proj1:             out << "proj1"; break;
+    case scanner::token::Proj2:             out << "proj2"; break;
     case scanner::token::Tuple:             out << "tuple"; break;
     case scanner::token::Placeholder:       out << "_"; break;
     case scanner::token::ScriptBlock:       out << "Script"; break;

src/frontends/lean/scanner.h

@@ -20,7 +20,7 @@ class scanner {
 public:
     enum class token {
         LeftParen, RightParen, LeftCurlyBracket, RightCurlyBracket, Colon, Comma, Period, Lambda, Pi, Arrow,
-        Sig, Tuple, Proj, Let, In, Exists, Id, CommandId, IntVal, DecimalVal, StringVal, Assign, Type, Placeholder,
+        Sig, Tuple, Proj1, Proj2, Let, In, Exists, Id, CommandId, IntVal, DecimalVal, StringVal, Assign, Type, Placeholder,
         Have, By, ScriptBlock, Ellipsis, CartesianProduct, Eof
     };
 protected:

src/kernel/type_checker.cpp

@@ -288,14 +288,14 @@ class type_checker::imp {
             }
         case expr_kind::Proj: {
             expr t = check_sigma(infer_type_core(proj_arg(e), ctx), e, ctx);
-            if (proj_first(t)) {
+            if (proj_first(e)) {
                 return abst_domain(t);
             } else {
                 expr const & b = abst_body(t);
                 if (closed(b))
                     return b;
                 else
-                    return instantiate(b, mk_proj1(e));
+                    return instantiate(b, mk_proj1(proj_arg(e)));
             }
         }
         case expr_kind::Lambda:

tests/lean/sig3.lean

@@ -0,0 +1,3 @@
+check tuple 10, 20
+check tuple 10, 20, 30
+check tuple 10, true, (λ x : Nat, x > 10)

tests/lean/sig3.lean.expected.out

@@ -0,0 +1,5 @@
+  Set: pp::colors
+  Set: pp::unicode
+tuple 10, 20 : ℕ ⨯ ℕ
+tuple 10, 20, 30 : ℕ ⨯ ℕ ⨯ ℕ
+tuple 10, ⊤, (λ x : ℕ, x > 10) : ℕ ⨯ Bool ⨯ (ℕ → Bool)

tests/lean/sig4.lean

@@ -0,0 +1,13 @@
+check proj1 (tuple 10, 20)
+eval proj1 (tuple 10, 20)
+eval proj2 (tuple 10, 20)
+eval proj2 (tuple 10, 20, 30)
+eval proj1 1 (tuple 10, 20, 30, 40)
+eval proj1 2 (tuple 10, 20, 30, 40)
+eval proj2 2 (tuple 10, 20, 30, 40)
+definition NZ : Type := sig x : Nat, 1 ≤ x
+variable t : NZ
+check proj1 t
+check proj2 t
+variable t2 : Nat # Nat # Nat
+check proj2 t2

tests/lean/sig4.lean.expected.out

@@ -0,0 +1,15 @@
+  Set: pp::colors
+  Set: pp::unicode
+proj1 (tuple 10, 20) : ℕ
+10
+20
+tuple 20, 30
+20
+30
+40
+  Defined: NZ
+  Assumed: t
+proj1 t : ℕ
+proj2 t : 1 ≤ proj1 t
+  Assumed: t2
+proj2 t2 : ℕ ⨯ ℕ