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

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

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"