From 88bbae29fedc7fdb5f4e0423a8958aeff7c40853 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 11 Dec 2019 15:30:54 +0100
Subject: [PATCH] refactor: use TermElab in quotation expander, polish
 Unhygienic story

---
 src/Init/Lean/Elab.lean           |  1 +
 src/Init/Lean/Elab/Quotation.lean | 60 +++++++++++++++++++------------
 src/Init/Lean/Elab/Term.lean      |  6 ----
 3 files changed, 39 insertions(+), 28 deletions(-)

diff --git a/src/Init/Lean/Elab.lean b/src/Init/Lean/Elab.lean
index 564d2ccfee..4710733a2b 100644
--- a/src/Init/Lean/Elab.lean
+++ b/src/Init/Lean/Elab.lean
@@ -9,5 +9,6 @@ import Init.Lean.Elab.Exception
 import Init.Lean.Elab.ElabStrategyAttrs
 import Init.Lean.Elab.Command
 import Init.Lean.Elab.Term
+import Init.Lean.Elab.Quotation
 import Init.Lean.Elab.Frontend
 import Init.Lean.Elab.BuiltinNotation
diff --git a/src/Init/Lean/Elab/Quotation.lean b/src/Init/Lean/Elab/Quotation.lean
index 98a5909693..5b7bd938d7 100644
--- a/src/Init/Lean/Elab/Quotation.lean
+++ b/src/Init/Lean/Elab/Quotation.lean
@@ -6,6 +6,7 @@ Authors: Sebastian Ullrich
 prelude
 import Init.Lean.Syntax
 import Init.Lean.Elab.ResolveName
+import Init.Lean.Elab.Term
 import Init.Lean.Parser -- TODO: remove after removing old elaborator
 
 namespace Lean
@@ -16,32 +17,40 @@ class MonadQuotation (m : Type → Type) :=
 -- Get the fresh scope of the current macro invocation
 (getCurrMacroScope : m Nat)
 
-/-- Simplistic MonadQuotation that does not guarantee fresh names. -/
+/-- Simplistic MonadQuotation that does not guarantee fresh names. It is only safe
+    if the syntax quotations do not introduce bindings around antiquotations, and
+    if references to globals are prefixed with `_root_.`. -/
 abbrev Unhygienic := Id
 namespace Unhygienic
 instance MonadQuotation : MonadQuotation Unhygienic := ⟨pure 0⟩
 def run {α : Type} : Unhygienic α → α := Id.run
 end Unhygienic
 
+namespace Term
+
+instance TermElabM.MonadQuotation : MonadQuotation TermElabM :=
+-- FIXME: actually allocate macro scopes when we actually make use of them
+⟨pure 0⟩
+
 private def appN (fn : Syntax) (args : Array Syntax) : Syntax :=
 args.foldl (fun fn arg => Unhygienic.run `(%%fn %%arg)) fn
 
 -- TODO: unclear if the following functions could also be useful to other code
 private def quoteName : Name → Syntax
-| Name.anonymous => Unhygienic.run `(Lean.Name.anonymous)
-| Name.str n s _ => Unhygienic.run `(Lean.mkNameStr %%(quoteName n) %%(Lean.mkStxStrLit s))
-| Name.num n i _ => Unhygienic.run `(Lean.mkNameStr %%(quoteName n) %%(Lean.mkStxNumLit (HasToString.toString i)))
+| Name.anonymous => Unhygienic.run `(_root_.Lean.Name.anonymous)
+| Name.str n s _ => Unhygienic.run `(_root_.Lean.mkNameStr %%(quoteName n) %%(Lean.mkStxStrLit s))
+| Name.num n i _ => Unhygienic.run `(_root_.Lean.mkNameStr %%(quoteName n) %%(Lean.mkStxNumLit (HasToString.toString i)))
 
 private def quoteList : List Syntax → Syntax
-| [] =>      Unhygienic.run `(List.nil)
-| (x::xs) => Unhygienic.run `(List.cons %%x %%(quoteList xs))
+| [] =>      Unhygienic.run `(_root_.List.nil)
+| (x::xs) => Unhygienic.run `(_root_.List.cons %%x %%(quoteList xs))
 
 private def quoteArray : Array Syntax → Syntax
 | xs =>
   let stx := quoteList xs.toList;
-  Unhygienic.run `(List.toArray %%stx)
+  Unhygienic.run `(_root_.List.toArray %%stx)
 
-private partial def quote (env : Environment) (msc : Syntax) : Syntax → Syntax
+private partial def quote {m : Type → Type} [Monad m] [MonadQuotation m] (env : Environment) (msc : Syntax) : Syntax → m Syntax
 | Syntax.ident info rawVal val preresolved =>
   -- TODO: pass scope information
   let ns := Name.anonymous;
@@ -50,22 +59,28 @@ private partial def quote (env : Environment) (msc : Syntax) : Syntax → Syntax
   -- TODO: hygiene
   -- `(Name.mkNumeral %%val %%msc)
   let val := quoteName val;
-  let args := quoteList $ preresolved.map $ fun ⟨n, ss⟩ => appN (Unhygienic.run `(Prod.mk)) #[quoteName n, quoteList $ ss.map mkStxStrLit];
-  Unhygienic.run `(Lean.Syntax.ident Option.none (String.toSubstring %%(Lean.mkStxStrLit (HasToString.toString rawVal))) %%val %%args)
-| Syntax.node `Lean.Parser.Term.antiquot args => args.get! 1
-| Syntax.node k args =>
+  let args := quoteList $ preresolved.map $ fun ⟨n, ss⟩ => appN (Unhygienic.run `(_root_.Prod.mk)) #[quoteName n, quoteList $ ss.map mkStxStrLit];
+  `(Lean.Syntax.ident Option.none (String.toSubstring %%(Lean.mkStxStrLit (HasToString.toString rawVal))) %%val %%args)
+| Syntax.node `Lean.Parser.Term.antiquot args => pure $ args.get! 1
+| Syntax.node k args => do
   let k := quoteName k;
-  let args := quoteArray $ args.map quote;
-  Unhygienic.run `(Lean.Syntax.node %%k %%args)
+  args ← quoteArray <$> args.mapM quote;
+  `(Lean.Syntax.node %%k %%args)
 | Syntax.atom info val =>
-  Unhygienic.run `(Lean.Syntax.atom Option.none %%(Lean.mkStxStrLit val))
+  `(Lean.Syntax.atom Option.none %%(Lean.mkStxStrLit val))
 | Syntax.missing => unreachable!
 
-def stxQuot.expand (env : Environment) (stx : Syntax) : Syntax :=
--- TODO: hygiene
--- `(do msc ← getCurMacroScope; pure %(quote `(msc) quoted))
-let stx := quote env Syntax.missing $ stx.getArg 1;
-Unhygienic.run `(HasPure.pure %%stx)
+def stxQuot.expand {m : Type → Type} [Monad m] [MonadQuotation m] (env : Environment) (stx : Syntax) : m Syntax := do
+  -- TODO: hygiene
+  -- `(do msc ← getCurMacroScope; pure %(quote `(msc) quoted))
+  stx ← quote env Syntax.missing $ stx.getArg 1;
+  `(HasPure.pure %%stx)
+
+@[builtinTermElab stxQuot] def elabStxQuot : TermElab :=
+fun stx expectedType? => do
+  env ← getEnv;
+  stx ← stxQuot.expand env (stx.getArg 1);
+  elabTerm stx expectedType?
 
 -- REMOVE with old frontend
 private partial def toPreterm (env : Environment) : Syntax → Except String Expr
@@ -80,7 +95,7 @@ private partial def toPreterm (env : Environment) : Syntax → Except String Exp
       let openDecls := [];
       let resolved := resolveGlobalName env ns openDecls val <|> preresolved;
       match resolved with
-      | (pre,[])::_ => pure $ mkConst pre
+      | (pre,[])::_ => pure $ Lean.mkConst pre
       | [] => pure $ mkFVar val
       | _ => throw "stxQuot: unimplemented: projection notation"
     | _ => unreachable!
@@ -101,7 +116,7 @@ let s := Parser.mkParserState c.input;
 let s := s.setPos pos;
 let s := (Parser.termParser : Parser.Parser).fn (0 : Nat) c s;
 let stx := s.stxStack.back;
-let stx := quote env Syntax.missing stx;
+let stx := Unhygienic.run $ quote env Syntax.missing stx;
 let stx := Unhygienic.run `(HasPure.pure %%stx);
 expr ← toPreterm env stx;
 match s.errorMsg with
@@ -110,5 +125,6 @@ match s.errorMsg with
 | none =>
   Except.ok (expr, s.pos)
 
+end Term
 end Elab
 end Lean
diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean
index 6668f0c565..6d693acd54 100644
--- a/src/Init/Lean/Elab/Term.lean
+++ b/src/Init/Lean/Elab/Term.lean
@@ -10,7 +10,6 @@ import Init.Lean.Meta
 import Init.Lean.Elab.Log
 import Init.Lean.Elab.Alias
 import Init.Lean.Elab.ResolveName
-import Init.Lean.Elab.Quotation
 
 namespace Lean
 namespace Elab
@@ -314,11 +313,6 @@ fun _ _ => pure $ mkSort levelOne
 @[builtinTermElab «hole»] def elabHole : TermElab :=
 fun stx expectedType? => mkFreshExprMVar stx.val expectedType?
 
-@[builtinTermElab stxQuot] def elabStxQuot : TermElab :=
-fun stx expectedType? => do
-  env ← getEnv;
-  elabTerm (stxQuot.expand env (stx.getArg 1)) expectedType?
-
 /--
   Given syntax of the forms
     a) (`:` term)?