From 865ef32e91008aa444f6a5e1ced587cbfcf6882d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 6 Jan 2020 15:10:35 -0800
Subject: [PATCH] feat: add `parser!` and `tparser!` elaborators

@Kha It is not convenient to use because
1- Coercions have not been implemented
2- Autoparams have not been implemented
3- There is bug the `Expr.lit` type checker
4- The new frontend uses a different mechanism for `export`. So,
`export`s in imported files compiled with the old frontend do not work.

I am working on these issues.
---
 src/Init/Lean/Elab/BuiltinNotation.lean | 24 ++++++++++++++++++++++++
 tests/lean/run/frontend1.lean           |  2 ++
 2 files changed, 26 insertions(+)

diff --git a/src/Init/Lean/Elab/BuiltinNotation.lean b/src/Init/Lean/Elab/BuiltinNotation.lean
index 0bf81a2c30..e502678f04 100644
--- a/src/Init/Lean/Elab/BuiltinNotation.lean
+++ b/src/Init/Lean/Elab/BuiltinNotation.lean
@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Lean.Elab.Term
+import Init.Lean.Elab.Quotation
 
 namespace Lean
 namespace Elab
@@ -77,6 +78,29 @@ adaptExpander $ fun stx => match_syntax stx with
     body
 | _                      => throwUnexpectedSyntax stx "where"
 
+@[termElab «parser!»] def elabParserMacro : TermElab :=
+adaptExpander $ fun stx => match_syntax stx with
+| `(parser! $e) => do
+  declName? ← getDeclName?;
+  match declName? with
+  | some declName@(Name.str _ s _) => do
+    let kind := quote declName;
+    let s    := quote s;
+    -- TODO simplify the following quotation as soon as we have coercions and autoparams
+    `(HasOrelse.orelse (Lean.Parser.mkAntiquot $s (some $kind) true) (Lean.Parser.leadingNode $kind $e))
+  | none          => throwError stx "invalid `parser!` macro, it must be used in definitions"
+  | _             => throwError stx "invalid `parser!` macro, unexpected declaration name"
+| _             => throwUnexpectedSyntax stx "parser!"
+
+@[termElab «tparser!»] def elabTParserMacro : TermElab :=
+adaptExpander $ fun stx => match_syntax stx with
+| `(tparser! $e) => do
+  declName? ← getDeclName?;
+  match declName? with
+  | some declName => let kind := quote declName; `(Lean.Parser.trailingNode $kind $e)
+  | none          => throwError stx "invalid `tparser!` macro, it must be used in definitions"
+| _             => throwUnexpectedSyntax stx "tparser!"
+
 def elabInfix (f : Syntax) : TermElab :=
 fun stx expectedType? => do
   -- term `op` term
diff --git a/tests/lean/run/frontend1.lean b/tests/lean/run/frontend1.lean
index 8f4e52d11f..bb7f8269d1 100644
--- a/tests/lean/run/frontend1.lean
+++ b/tests/lean/run/frontend1.lean
@@ -200,3 +200,5 @@ f a
 #eval run "variables {β σ} universes w1 w2 /-- Testing axiom -/ unsafe axiom Nat.aux.{u, v} (γ : Type w1) (v : Nat) : β → (α : Type _) → v = zero /- Nat.zero -/ → Array α #check @Nat.aux"
 #eval run "def x : Nat := Nat.zero #check x"
 #eval run "def x := Nat.zero #check x"
+#eval run "open Lean.Parser def x := parser! symbol \"foo\" Nat.zero #check x"
+#eval run "open Lean.Parser def x := tparser! symbol \"foo\" Nat.zero #check x"