From 6774377d194a61350dbcb4e190cee8d5445c2ba1 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 10 Dec 2019 15:32:14 +0100
Subject: [PATCH] feat: elaborate quotation terms

---
 src/Init/Lean/Elab/Quotation.lean | 69 +++++++++++++++++++++++++++++++
 src/Init/Lean/Elab/Term.lean      |  6 +++
 2 files changed, 75 insertions(+)
 create mode 100644 src/Init/Lean/Elab/Quotation.lean

diff --git a/src/Init/Lean/Elab/Quotation.lean b/src/Init/Lean/Elab/Quotation.lean
new file mode 100644
index 0000000000..e1b59f9f54
--- /dev/null
+++ b/src/Init/Lean/Elab/Quotation.lean
@@ -0,0 +1,69 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Ullrich
+-/
+prelude
+import Init.Lean.Syntax
+import Init.Lean.Elab.ResolveName
+
+namespace Lean
+namespace Elab
+
+-- TODO: replace with quotations where possible
+private def const (n : Name) : Syntax :=
+Syntax.node `Lean.Parser.Term.id #[Syntax.ident none n.toString.toSubstring n [(n, [])]]
+
+private def app (fn arg : Syntax) : Syntax :=
+Syntax.node `Lean.Parser.Term.app #[fn, arg]
+
+private def appN (fn : Syntax) (args : Array Syntax) : Syntax :=
+args.foldl app fn
+
+-- TODO: unclear if the following functions could also be useful to other code
+private def quoteName : Name → Syntax
+| Name.anonymous => const `Lean.Name.anonymous
+| Name.str n s _ => appN (const `Lean.mkNameStr) #[quoteName n, mkStxStrLit s]
+| Name.num n i _ => appN (const `Lean.mkNameNum) #[quoteName n, mkStxNumLit $ toString i]
+
+private def quoteList : List Syntax → Syntax
+| [] => const `List.nil
+| (x::xs) => appN (const `List.cons) #[x, quoteList xs]
+
+private def quoteArray : Array Syntax → Syntax
+| xs => app (const `List.toArray) $ quoteList xs.toList
+
+private partial def quote (env : Environment) (msc : Syntax) : Syntax → Syntax
+| Syntax.ident info rawVal val preresolved =>
+  -- TODO: pass scope information
+  let ns := Name.anonymous;
+  let openDecls := [];
+  let preresolved := resolveGlobalName env ns openDecls val <|> preresolved;
+  --`(Syntax.ident none (String.toSubstring %(rawVal.toString)) (Name.mkNumeral %val %msc))
+  appN (const `Lean.Syntax.ident) #[
+    const `Option.none,
+    app (const `String.toSubstring) (mkStxStrLit rawVal.toString),
+    --appN (const `Lean.Name.mkNumeral) #[quoteName val, msc]
+    -- TODO: hygiene
+    quoteName val,
+    quoteList $ preresolved.map $ fun ⟨n, ss⟩ => appN (const `Prod.mk) #[quoteName n, quoteList $ ss.map mkStxStrLit]
+  ]
+| Syntax.node `Lean.Parser.Term.antiquot args => args.get! 1
+| Syntax.node k args =>
+  --`(Syntax.node %k %args...)
+  let args := quoteArray $ args.map quote;
+  appN (const `Lean.Syntax.node) $ #[quoteName k, args]
+| Syntax.atom info val => --`(Syntax.atom none %val)
+  appN (const `Lean.Syntax.atom) #[
+    const `Option.none,
+    mkStxStrLit val
+  ]
+| Syntax.missing => unreachable!
+
+-- TODO: hygiene
+def stxQuot.expand (env : Environment) (stx : Syntax) : Syntax :=
+-- `(do msc ← getCurMacroScope; pure %(quote `(msc) quoted))
+app (const `HasPure.pure) $ quote env Syntax.missing $ stx.getArg 1
+
+end Elab
+end Lean
diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean
index b49530b55b..49e61174bb 100644
--- a/src/Init/Lean/Elab/Term.lean
+++ b/src/Init/Lean/Elab/Term.lean
@@ -8,6 +8,7 @@ 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
@@ -164,6 +165,11 @@ fun _ expectedType? =>
   | some expectedType => mkFreshExprMVar expectedType
   | none              => do u ← mkFreshLevelMVar; mkFreshExprMVar (mkSort u)
 
+@[builtinTermElab stxQuot] def elabStxQuot : TermElab :=
+fun stx expectedType? => do
+  env ← getEnv;
+  elabTerm (stxQuot.expand env (stx.getArg 1)) expectedType?
+
 private def mkFreshAnonymousName : TermElabM Name :=
 do s ← get;
    let anonymousIdx := s.anonymousIdx;