feat(frontends/lean): add ! operator the "dual" of @, closes #220

src/frontends/lean/builtin_exprs.cpp

@@ -340,6 +340,18 @@ static expr parse_explicit_expr(parser & p, unsigned, expr const *, pos_info con
     }
 }
 
+static expr parse_consume_args_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
+    expr e = p.parse_expr(get_max_prec());
+    if (is_choice(e)) {
+        buffer<expr> new_choices;
+        for (unsigned i = 0; i < get_num_choices(e); i++)
+            new_choices.push_back(p.save_pos(mk_consume_args(get_choice(e, i)), pos));
+        return p.save_pos(mk_choice(new_choices.size(), new_choices.data()), pos);
+    } else {
+        return p.save_pos(mk_consume_args(e), pos);
+    }
+}
+
 static expr parse_including_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
     buffer<expr> locals;
     while (!p.curr_is_token(get_comma_tk())) {
@@ -400,6 +412,7 @@ parse_table init_nud_table() {
     r = r.add({transition("calc", mk_ext_action(parse_calc_expr))}, x0);
     r = r.add({transition("#", mk_ext_action(parse_overwrite_notation))}, x0);
     r = r.add({transition("@", mk_ext_action(parse_explicit_expr))}, x0);
+    r = r.add({transition("!", mk_ext_action(parse_consume_args_expr))}, x0);
     r = r.add({transition("begin", mk_ext_action(parse_begin_end))}, x0);
     r = r.add({transition("proof", mk_ext_action(parse_proof_qed))}, x0);
     r = r.add({transition("sorry", mk_ext_action(parse_sorry))}, x0);

src/frontends/lean/elaborator.cpp

@@ -781,7 +781,14 @@ public:
         } else if (is_typed_expr(e)) {
             return visit_typed_expr(e, cs);
         } else if (is_implicit(e)) {
+            // ignore annotation
             return visit_core(get_implicit_arg(e), cs);
+        } else if (is_consume_args(e)) {
+            // ignore annotation
+            return visit_core(get_consume_args_arg(e), cs);
+        } else if (is_explicit(e)) {
+            // ignore annotation
+            return visit_core(get_explicit_arg(e), cs);
         } else if (is_sorry(e)) {
             return visit_sorry(e);
         } else {
@@ -819,11 +826,15 @@ public:
         } else if (is_explicit(get_app_fn(e))) {
             r    = visit_core(e, cs);
         } else {
+            bool consume_args = false;
             if (is_implicit(e)) {
                 r = get_implicit_arg(e);
                 if (is_explicit(r)) r = get_explicit_arg(r);
                 b = r;
                 r = visit_core(r, cs);
+            } else if (is_consume_args(e)) {
+                consume_args = true;
+                r = visit_core(get_consume_args_arg(e), cs);
             } else {
                 r = visit_core(e, cs);
             }
@@ -831,7 +842,7 @@ public:
             expr r_type    = whnf(infer_type(r, cs), cs);
             expr imp_arg;
             bool is_strict = true;
-            while (is_pi(r_type) && binding_info(r_type).is_implicit()) {
+            while (is_pi(r_type) && (consume_args || binding_info(r_type).is_implicit())) {
                 imp_arg = mk_placeholder_meta(some_expr(binding_domain(r_type)), g, is_strict, cs);
                 r       = mk_app(r, imp_arg, g);
                 r_type  = whnf(instantiate(binding_body(r_type), imp_arg), cs);

src/frontends/lean/token_table.cpp

@@ -72,7 +72,7 @@ void init_token_table(token_table & t) {
         {{"fun", 0}, {"Pi", 0}, {"let", 0}, {"in", 0}, {"have", 0}, {"show", 0}, {"obtain", 0}, {"by", 0}, {"then", 0},
          {"from", 0}, {"(", g_max_prec}, {")", 0}, {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec},
          {"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, {"Type", g_max_prec},
-         {"Type'", g_max_prec}, {"using", 0}, {"|", 0}, {"!", 0}, {"with", 0}, {"...", 0}, {",", 0},
+         {"Type'", g_max_prec}, {"using", 0}, {"|", 0}, {"!", g_max_prec}, {"with", 0}, {"...", 0}, {",", 0},
          {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {":=", 0}, {"--", 0}, {"#", 0},
          {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"proof", g_max_prec}, {"qed", 0}, {"@", g_max_prec},
          {"including", 0}, {"sorry", g_max_prec}, {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec},

src/library/explicit.cpp

@@ -13,32 +13,42 @@ namespace lean {
 static name * g_explicit_name = nullptr;
 static name * g_implicit_name = nullptr;
 static name * g_as_is_name    = nullptr;
+static name * g_consume_args_name = nullptr;
 
 expr mk_explicit(expr const & e) { return mk_annotation(*g_explicit_name, e); }
 bool is_explicit(expr const & e) { return is_annotation(e, *g_explicit_name); }
 bool is_nested_explicit(expr const & e) { return is_nested_annotation(e, *g_explicit_name); }
+expr const & get_explicit_arg(expr const & e) { lean_assert(is_explicit(e)); return get_annotation_arg(e); }
+
 expr mk_as_is(expr const & e) { return mk_annotation(*g_as_is_name, e); }
 bool is_as_is(expr const & e) { return is_annotation(e, *g_as_is_name); }
+expr const & get_as_is_arg(expr const & e) { lean_assert(is_as_is(e)); return get_annotation_arg(e); }
+
 expr mk_implicit(expr const & e) { return mk_annotation(*g_implicit_name, e); }
 bool is_implicit(expr const & e) { return is_annotation(e, *g_implicit_name); }
-expr const & get_explicit_arg(expr const & e) { lean_assert(is_explicit(e)); return get_annotation_arg(e); }
-expr const & get_as_is_arg(expr const & e) { lean_assert(is_as_is(e)); return get_annotation_arg(e); }
 expr const & get_implicit_arg(expr const & e) { lean_assert(is_implicit(e)); return get_annotation_arg(e); }
 
+expr mk_consume_args(expr const & e) { return mk_annotation(*g_consume_args_name, e); }
+bool is_consume_args(expr const & e) { return is_annotation(e, *g_consume_args_name); }
+expr const & get_consume_args_arg(expr const & e) { lean_assert(is_consume_args(e)); return get_annotation_arg(e); }
+
 void initialize_explicit() {
-    g_explicit_name = new name("@");
-    g_implicit_name = new name("@^-1");
-    g_as_is_name    = new name("as_is");
+    g_explicit_name     = new name("@");
+    g_implicit_name     = new name("@^-1");
+    g_as_is_name        = new name("as_is");
+    g_consume_args_name = new name("!");
 
     register_annotation(*g_explicit_name);
     register_annotation(*g_implicit_name);
     register_annotation(*g_as_is_name);
+    register_annotation(*g_consume_args_name);
 }
 
 void finalize_explicit() {
     delete g_as_is_name;
     delete g_implicit_name;
     delete g_explicit_name;
+    delete g_consume_args_name;
 }
 
 static int mk_explicit(lua_State * L) { return push_expr(L, mk_explicit(to_expr(L, 1))); }

src/library/explicit.h

@@ -17,30 +17,43 @@ expr mk_explicit(expr const & e);
 bool is_explicit(expr const & e);
 /** \brief See #is_nested_annotation */
 bool is_nested_explicit(expr const & e);
+/** \brief Return the argument of an explicit expression.
+    \pre is_explicit(e)
+*/
+expr const & get_explicit_arg(expr const & e);
+
 /** \brief Create an explicit expression that is accepted as is
     by the elaborator.
 */
 expr mk_as_is(expr const & e);
 /** \brief Return true iff \c e was created with mk_as_is. */
 bool is_as_is(expr const & e);
+/** \brief Return the argument of an expression created using mk_as_is.
+    \pre is_as_is(e)
+*/
+expr const & get_as_is_arg(expr const & e);
+
 /** \brief Create an implicit expression '@^-1 f'.
     This only affects the elaborator behavior. This expression "cancels" the effect of '@'
 */
 expr mk_implicit(expr const & e);
 /** \brief Return true iff \c e is an implicit expression. */
 bool is_implicit(expr const & e);
-/** \brief Return the argument of an explicit expression.
-    \pre is_explicit(e)
-*/
-expr const & get_explicit_arg(expr const & e);
-/** \brief Return the argument of an expression created using mk_as_is.
-    \pre is_as_is(e)
-*/
-expr const & get_as_is_arg(expr const & e);
 /** \brief Return the argument of an implicit expression.
     \pre is_implicit(e)
 */
 expr const & get_implicit_arg(expr const & e);
+
+/** \brief Create the expression '! e'.
+    This only affects the elaborator behavior.
+    It instructs the elaborator to keep adding '_'
+    for \c e arguments.
+*/
+expr mk_consume_args(expr const & e);
+/** \brief Return true iff \c e is an '!f' expression. */
+bool is_consume_args(expr const & e);
+expr const & get_consume_args_arg(expr const & e);
+
 void open_explicit(lua_State * L);
 void initialize_explicit();
 void finalize_explicit();

tests/lean/run/consume.lean

@@ -0,0 +1,11 @@
+import logic
+
+definition pr2 {A : Type} (a b : A) := a
+
+check pr2
+check !pr2
+check !@pr2
+check @pr2
+check @!pr2
+check @@pr2
+check !!pr2