From 86edc94dbe348244b20344cca583d8a68badfdf1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 18 Jan 2020 20:02:50 -0800
Subject: [PATCH] feat: add support for elaborating raw literals

---
 src/Init/Lean/Elab/Term.lean    | 27 +++++++++++++++++++++------
 tests/lean/run/macro_macro.lean |  8 ++++++--
 2 files changed, 27 insertions(+), 8 deletions(-)

diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean
index d6c23e4355..b45419429e 100644
--- a/src/Init/Lean/Elab/Term.lean
+++ b/src/Init/Lean/Elab/Term.lean
@@ -782,16 +782,24 @@ match result? with
 @[builtinTermElab cdot] def elabBadCDot : TermElab :=
 fun stx _ => throwError stx "invalid occurrence of `·` notation, it must be surrounded by parentheses (e.g. `(· + 1)`)"
 
-@[builtinTermElab str] def elabStr : TermElab :=
+/-
+  A raw literal is not a valid term, but it is nice to have a handler for them because it allows `macros` to insert them into terms.
+
+  TODO: check whether we still need wrapper nodes around literals. -/
+@[builtinTermElab strLit] def elabRawStrLit : TermElab :=
 fun stx _ => do
-  match (stx.getArg 0).isStrLit? with
+  match stx.isStrLit? with
   | some val => pure $ mkStrLit val
   | none     => throwError stx "ill-formed syntax"
 
-@[builtinTermElab num] def elabNum : TermElab :=
+@[builtinTermElab str] def elabStr : TermElab :=
+fun stx expectedType? => elabRawStrLit (stx.getArg 0) expectedType?
+
+/- See `elabRawStrLit` -/
+@[builtinTermElab numLit] def elabRawNumLit : TermElab :=
 fun stx expectedType? => do
   let ref := stx;
-  val ← match (stx.getArg 0).isNatLit? with
+  val ← match stx.isNatLit? with
     | some val => pure (mkNatLit val)
     | none     => throwError stx "ill-formed syntax";
   typeMVar ← mkFreshTypeMVar ref MetavarKind.synthetic;
@@ -804,12 +812,19 @@ fun stx expectedType? => do
   mvar ← mkInstMVar ref (mkApp (Lean.mkConst `HasOfNat [u]) typeMVar);
   pure $ mkApp3 (Lean.mkConst `HasOfNat.ofNat [u]) typeMVar mvar val
 
-@[builtinTermElab char] def elabChar : TermElab :=
+@[builtinTermElab num] def elabNum : TermElab :=
+fun stx expectedType? => elabRawNumLit (stx.getArg 0) expectedType?
+
+/- See `elabRawStrLit` -/
+@[builtinTermElab charLit] def elabRawCharLit : TermElab :=
 fun stx _ => do
-  match (stx.getArg 0).isCharLit? with
+  match stx.isCharLit? with
   | some val => pure $ mkApp (Lean.mkConst `Char.ofNat) (mkNatLit val.toNat)
   | none     => throwError stx "ill-formed syntax"
 
+@[builtinTermElab char] def elabChar : TermElab :=
+fun stx expectedType? => elabRawCharLit (stx.getArg 0) expectedType?
+
 end Term
 
 @[init] private def regTraceClasses : IO Unit := do
diff --git a/tests/lean/run/macro_macro.lean b/tests/lean/run/macro_macro.lean
index 5a81b94e1d..d33ad99e6c 100644
--- a/tests/lean/run/macro_macro.lean
+++ b/tests/lean/run/macro_macro.lean
@@ -1,5 +1,9 @@
 new_frontend
 
-macro mk_m : command => `(macro m : term => `(fun x => x))
+macro mk_m id:ident v:str n:num c:char : command => `(macro $id:ident : term => `(fun (x : String) => x ++ $v ++ (toString $n) ++ (toString $c)))
 
-mk_m
+mk_m foo "bla" 10 'a'
+mk_m boo "hello" 3 'b'
+
+#check foo "world"
+#check boo "boo"