From 6db265e7abe43d411a013f2c0f64cff8ddc9ec80 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 16 Jun 2014 10:41:08 -0700
Subject: [PATCH] feat(frontends/lean/builtin_exprs): parse '_' placeholder

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/builtin_exprs.cpp | 5 +++++
 src/frontends/lean/token_table.cpp   | 2 +-
 tests/lean/run/t7.lean               | 3 +++
 3 files changed, 9 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/t7.lean

diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index 546f7b064..74b2848e9 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -85,6 +85,10 @@ static expr parse_let_expr(parser & p, unsigned, expr const *) {
     return parse_let(p);
 }
 
+static expr parse_placeholder(parser &, unsigned, expr const *) {
+    return mk_expr_placeholder();
+}
+
 parse_table init_nud_table() {
     action Expr(mk_expr_action());
     action Skip(mk_skip_action());
@@ -92,6 +96,7 @@ parse_table init_nud_table() {
     expr x0 = mk_var(0);
     parse_table r;
     r = r.add({transition("Bool", Skip)}, mk_Bool());
+    r = r.add({transition("_", mk_ext_action(parse_placeholder))}, x0);
     r = r.add({transition("(", Expr), transition(")", Skip)}, x0);
     r = r.add({transition("fun", Binders), transition(",", mk_scoped_expr_action(x0))}, x0);
     r = r.add({transition("Pi", Binders), transition(",", mk_scoped_expr_action(x0, 0, false))}, x0);
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index 2bb527737..3d216b13b 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -55,7 +55,7 @@ token_table init_token_table() {
     token_table t;
     std::pair<char const *, unsigned> builtin[] =
         {{"fun", 0}, {"Pi", 0}, {"let", 0}, {"in", 0}, {"have", 0}, {"show", 0}, {"by", 0},
-         {"from", 0}, {"(", g_max_prec}, {")", 0}, {"{", g_max_prec}, {"}", 0},
+         {"from", 0}, {"(", g_max_prec}, {")", 0}, {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec},
          {"[", g_max_prec}, {"]", 0}, {".{", 0}, {"Type", g_max_prec},
          {"...", 0}, {",", 0}, {".", 0}, {":", 0}, {"calc", 0}, {":=", 0}, {"--", 0},
          {"(*", 0}, {"(--", 0}, {"proof", 0}, {"qed", 0}, {"raw", 0}, {"Bool", g_max_prec},
diff --git a/tests/lean/run/t7.lean b/tests/lean/run/t7.lean
new file mode 100644
index 000000000..7f1684146
--- /dev/null
+++ b/tests/lean/run/t7.lean
@@ -0,0 +1,3 @@
+variable A : Type.{1}
+variable f : A → A → A
+print raw f _ (f _ _)
\ No newline at end of file