From e57d3431eeaa6c235583bd111f30583ca8dccb2f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 19 Jan 2020 14:44:03 -0800
Subject: [PATCH] refactor: move basic `Syntax` API to `LeanInit`

We want to make them available for `macro`-building
---
 src/Init/Lean/Data/Name.lean   |  24 +-----
 src/Init/Lean/Elab/Syntax.lean |   2 +-
 src/Init/Lean/Parser/Term.lean |  34 ---------
 src/Init/Lean/Syntax.lean      |  58 ---------------
 src/Init/LeanInit.lean         | 131 +++++++++++++++++++++++++++++++--
 5 files changed, 128 insertions(+), 121 deletions(-)

diff --git a/src/Init/Lean/Data/Name.lean b/src/Init/Lean/Data/Name.lean
index 7dcebb0220..7560b0c86b 100644
--- a/src/Init/Lean/Data/Name.lean
+++ b/src/Init/Lean/Data/Name.lean
@@ -19,6 +19,9 @@ instance stringToName : HasCoe String Name :=
 
 namespace Name
 
+@[export lean_name_hash] def hashEx : Name → USize :=
+Name.hash
+
 def getPrefix : Name → Name
 | anonymous => anonymous
 | str p s _ => p
@@ -46,14 +49,6 @@ def eqStr : Name → String → Bool
 | str anonymous s _, s' => s == s'
 | _,                 _  => false
 
-protected def append : Name → Name → Name
-| n, anonymous => n
-| n, str p s _ => mkNameStr (append n p) s
-| n, num p d _ => mkNameNum (append n p) d
-
-instance : HasAppend Name :=
-⟨Name.append⟩
-
 def replacePrefix : Name → Name → Name → Name
 | anonymous,     anonymous, newP => newP
 | anonymous,     _,         _    => anonymous
@@ -100,19 +95,6 @@ else quickLtAux n₁ n₂
 @[inline] instance : DecidableRel (@HasLess.Less Name Name.hasLtQuick) :=
 inferInstanceAs (DecidableRel (fun a b => Name.quickLt a b = true))
 
-def toStringWithSep (sep : String) : Name → String
-| anonymous         => "[anonymous]"
-| str anonymous s _ => s
-| num anonymous v _ => toString v
-| str n s _         => toStringWithSep n ++ sep ++ s
-| num n v _         => toStringWithSep n ++ sep ++ repr v
-
-protected def toString : Name → String :=
-toStringWithSep "."
-
-instance : HasToString Name :=
-⟨Name.toString⟩
-
 def appendAfter : Name → String → Name
 | str p s _, suffix => mkNameStr p (s ++ suffix)
 | n,         suffix => mkNameStr n suffix
diff --git a/src/Init/Lean/Elab/Syntax.lean b/src/Init/Lean/Elab/Syntax.lean
index e955383881..228bd4cb8c 100644
--- a/src/Init/Lean/Elab/Syntax.lean
+++ b/src/Init/Lean/Elab/Syntax.lean
@@ -180,7 +180,7 @@ adaptExpander $ fun stx => match_syntax stx with
   | `(`($quot)) => pure quot.getKind
   | stx         => throwUnsupportedSyntax;
   -- TODO: meaningful, unhygienic def name for selective macro `open`ing?
-  `(@[macro $(Lean.mkSimpleIdent k)] def myMacro : Macro := fun stx => match_syntax stx with $alts* | _ => throw ())
+  `(@[macro $(Lean.mkIdent k)] def myMacro : Macro := fun stx => match_syntax stx with $alts* | _ => throw ())
 | _ => throwUnsupportedSyntax
 
 /- We just ignore Lean3 notation declaration commands. -/
diff --git a/src/Init/Lean/Parser/Term.lean b/src/Init/Lean/Parser/Term.lean
index dd2484340f..a0345e61ea 100644
--- a/src/Init/Lean/Parser/Term.lean
+++ b/src/Init/Lean/Parser/Term.lean
@@ -179,40 +179,6 @@ end Parser
 
 open Parser
 
-def mkAppStx (fn : Syntax) (args : Array Syntax) : Syntax :=
-Syntax.node `Lean.Parser.Term.app #[fn, mkNullNode args]
--- args.foldl (fun fn arg => Syntax.node `Lean.Parser.Term.app #[fn, arg]) fn
-
-def mkHole (ref : Syntax) := mkNode `Lean.Parser.Term.hole #[mkAtomFrom ref "_"]
-
-/-- Convert a `Syntax.ident` into a `Lean.Parser.Term.id` node -/
-def mkTermIdFromIdent (ident : Syntax) : Syntax :=
-match ident with
-| Syntax.ident _ _ _ _ => mkNode `Lean.Parser.Term.id #[ident, mkNullNode]
-| _                    => unreachable!
-
-/--
-  Create a simple `Lean.Parser.Term.id` syntax using position
-  information from `ref` and name `n`. By simple, we mean that
-  `optional (explicitUniv <|> namedPattern)` is none.
-  To refer to a specific constant, use `mkCTermIdFrom` instead. -/
-def mkTermIdFrom (ref : Syntax) (n : Name) : Syntax :=
-mkTermIdFromIdent (mkIdentFrom ref n)
-
-/-- Variant of `mkTermIdFrom` that makes sure that the identifier cannot accidentally
-    be captured. -/
-def mkCTermIdFrom (ref : Syntax) (c : Name) : Syntax :=
-mkTermIdFromIdent (mkCIdentFrom ref c)
-
-def mkTermId (n : Name) : Syntax :=
-mkTermIdFrom Syntax.missing n
-
-def mkCTermId (c : Name) : Syntax :=
-mkCTermIdFrom Syntax.missing c
-
-def mkCAppStx (fn : Name) (args : Array Syntax) : Syntax :=
-mkAppStx (mkCTermId fn) args
-
 def Syntax.isTermId? (stx : Syntax) : Option (Syntax × Syntax) :=
 stx.ifNode
  (fun node =>
diff --git a/src/Init/Lean/Syntax.lean b/src/Init/Lean/Syntax.lean
index 4c810b098c..a6b091ce22 100644
--- a/src/Init/Lean/Syntax.lean
+++ b/src/Init/Lean/Syntax.lean
@@ -27,15 +27,6 @@ def appendToLeading (info₁ info₂ : SourceInfo) : SourceInfo :=
 
 end SourceInfo
 
-/- Node kind generation -/
-
-@[matchPattern] def choiceKind : SyntaxNodeKind := `choice
-@[matchPattern] def nullKind : SyntaxNodeKind := `null
-def strLitKind : SyntaxNodeKind := `strLit
-def charLitKind : SyntaxNodeKind := `charLit
-def numLitKind : SyntaxNodeKind := `numLit
-def fieldIdxKind : SyntaxNodeKind := `fieldIdx
-
 /- Syntax AST -/
 
 def Syntax.isMissing : Syntax → Bool
@@ -206,13 +197,6 @@ partial def updateTrailing (trailing : Substring) : Syntax → Syntax
    Syntax.node k args
 | s => s
 
-/-- Retrieve the left-most leaf's info in the Syntax tree. -/
-partial def getHeadInfo : Syntax → Option SourceInfo
-| atom info _      => info
-| ident info _ _ _ => info
-| node _ args      => args.find? getHeadInfo
-| _                => none
-
 def getPos (stx : Syntax) : Option String.Pos :=
 SourceInfo.pos <$> stx.getHeadInfo
 
@@ -314,10 +298,6 @@ end SyntaxNode
 def mkSimpleAtom (val : String) : Syntax :=
 Syntax.atom none val
 
-@[export lean_mk_syntax_ident]
-def mkSimpleIdent (val : Name) : Syntax :=
-Syntax.ident none (toString val).toSubstring val []
-
 @[export lean_mk_syntax_list]
 def mkListNode (args : Array Syntax) : Syntax :=
 Syntax.node nullKind args
@@ -328,26 +308,6 @@ Syntax.atom none val
 @[inline] def mkNode (k : SyntaxNodeKind) (args : Array Syntax) : Syntax :=
 Syntax.node k args
 
-@[inline] def mkNullNode (args : Array Syntax := #[]) : Syntax :=
-Syntax.node nullKind args
-
-def mkOptionalNode (arg : Option Syntax) : Syntax :=
-match arg with
-| some arg => Syntax.node nullKind #[arg]
-| none     => Syntax.node nullKind #[]
-
-/- Helper functions for creating string and numeric literals -/
-
-def mkStxLit (kind : SyntaxNodeKind) (val : String) (info : Option SourceInfo := none) : Syntax :=
-let atom : Syntax := Syntax.atom info val;
-Syntax.node kind #[atom]
-
-def mkStxStrLit (val : String) (info : Option SourceInfo := none) : Syntax :=
-mkStxLit strLitKind (repr val) info
-
-def mkStxNumLit (val : String) (info : Option SourceInfo := none) : Syntax :=
-mkStxLit numLitKind val info
-
 @[export lean_mk_syntax_str_lit]
 def mkStxStrLitAux (val : String) : Syntax :=
 mkStxStrLit val
@@ -517,22 +477,4 @@ def hasArgs : Syntax → Bool
 | _                  => false
 
 end Syntax
-
-/-- Create an identifier using `SourceInfo` from `src`.
-    To refer to a specific constant, use `mkCIdentFrom` instead. -/
-def mkIdentFrom (src : Syntax) (val : Name) : Syntax :=
-let info := src.getHeadInfo;
-Syntax.ident info (toString val).toSubstring val []
-
-/-- Create an identifier referring to a constant `c` using `SourceInfo` from `src`.
-    This variant of `mkIdentFrom` makes sure that the identifier cannot accidentally
-    be captured. -/
-def mkCIdentFrom (src : Syntax) (c : Name) : Syntax :=
-let info := src.getHeadInfo;
-Syntax.ident info (toString c).toSubstring (`_root_ ++ c) [(c, [])]
-
-def mkAtomFrom (src : Syntax) (val : String) : Syntax :=
-let info := src.getHeadInfo;
-Syntax.atom info val
-
 end Lean
diff --git a/src/Init/LeanInit.lean b/src/Init/LeanInit.lean
index 78a8c61eb7..9b39f6e0a1 100644
--- a/src/Init/LeanInit.lean
+++ b/src/Init/LeanInit.lean
@@ -30,15 +30,13 @@ inductive Name
 instance Name.inhabited : Inhabited Name :=
 ⟨Name.anonymous⟩
 
-def Name.hash : Name → USize
+protected def Name.hash : Name → USize
 | Name.anonymous => 1723
 | Name.str p s h => h
 | Name.num p v h => h
 
 instance Name.hashable : Hashable Name := ⟨Name.hash⟩
 
-@[export lean_name_hash] def Name.hashEx : Name → USize := Name.hash
-
 @[export lean_name_mk_string]
 def mkNameStr (p : Name) (s : String) : Name :=
 Name.str p s $ mixHash (hash p) (hash s)
@@ -50,15 +48,40 @@ Name.num p v $ mixHash (hash p) (hash v)
 def mkNameSimple (s : String) : Name :=
 mkNameStr Name.anonymous s
 
+namespace Name
+
 @[extern "lean_name_eq"]
 protected def Name.beq : (@& Name) → (@& Name) → Bool
-| Name.anonymous,   Name.anonymous   => true
-| Name.str p₁ s₁ _, Name.str p₂ s₂ _ => s₁ == s₂ && Name.beq p₁ p₂
-| Name.num p₁ n₁ _, Name.num p₂ n₂ _ => n₁ == n₂ && Name.beq p₁ p₂
-| _,                _                => false
+| anonymous,   anonymous   => true
+| str p₁ s₁ _, str p₂ s₂ _ => s₁ == s₂ && Name.beq p₁ p₂
+| num p₁ n₁ _, num p₂ n₂ _ => n₁ == n₂ && Name.beq p₁ p₂
+| _,           _           => false
 
 instance : HasBeq Name := ⟨Name.beq⟩
 
+def toStringWithSep (sep : String) : Name → String
+| anonymous         => "[anonymous]"
+| str anonymous s _ => s
+| num anonymous v _ => toString v
+| str n s _         => toStringWithSep n ++ sep ++ s
+| num n v _         => toStringWithSep n ++ sep ++ repr v
+
+protected def toString : Name → String :=
+toStringWithSep "."
+
+instance : HasToString Name :=
+⟨Name.toString⟩
+
+protected def append : Name → Name → Name
+| n, anonymous => n
+| n, str p s _ => mkNameStr (append n p) s
+| n, num p d _ => mkNameNum (append n p) d
+
+instance : HasAppend Name :=
+⟨Name.append⟩
+
+end Name
+
 inductive ParserKind
 | leading | trailing
 
@@ -156,6 +179,13 @@ match stx with
 | Syntax.node _ args => args
 | _                  => #[]
 
+/-- Retrieve the left-most leaf's info in the Syntax tree. -/
+partial def getHeadInfo : Syntax → Option SourceInfo
+| atom info _      => info
+| ident info _ _ _ => info
+| node _ args      => args.find? getHeadInfo
+| _                => none
+
 end Syntax
 
 /-
@@ -204,6 +234,93 @@ instance MacroM.monadQuotation : MonadQuotation MacroM :=
 
 abbrev Macro := Syntax → MacroM Syntax
 
+/- Builtin kinds -/
+
+@[matchPattern] def choiceKind : SyntaxNodeKind := `choice
+@[matchPattern] def nullKind : SyntaxNodeKind := `null
+def strLitKind : SyntaxNodeKind := `strLit
+def charLitKind : SyntaxNodeKind := `charLit
+def numLitKind : SyntaxNodeKind := `numLit
+def fieldIdxKind : SyntaxNodeKind := `fieldIdx
+
+/- Helper functions for processing Syntax programmatically -/
+
+/--
+  Create an identifier using `SourceInfo` from `src`.
+  To refer to a specific constant, use `mkCIdentFrom` instead. -/
+def mkIdentFrom (src : Syntax) (val : Name) : Syntax :=
+let info := src.getHeadInfo;
+Syntax.ident info (toString val).toSubstring val []
+
+/--
+  Create an identifier referring to a constant `c` using `SourceInfo` from `src`.
+  This variant of `mkIdentFrom` makes sure that the identifier cannot accidentally
+  be captured. -/
+def mkCIdentFrom (src : Syntax) (c : Name) : Syntax :=
+let info := src.getHeadInfo;
+Syntax.ident info (toString c).toSubstring (`_root_ ++ c) [(c, [])]
+
+def mkAtomFrom (src : Syntax) (val : String) : Syntax :=
+let info := src.getHeadInfo;
+Syntax.atom info val
+
+@[export lean_mk_syntax_ident]
+def mkIdent (val : Name) : Syntax :=
+Syntax.ident none (toString val).toSubstring val []
+
+@[inline] def mkNullNode (args : Array Syntax := #[]) : Syntax :=
+Syntax.node nullKind args
+
+def mkOptionalNode (arg : Option Syntax) : Syntax :=
+match arg with
+| some arg => Syntax.node nullKind #[arg]
+| none     => Syntax.node nullKind #[]
+
+/-- Create syntax representing a Lean term application -/
+def mkAppStx (fn : Syntax) (args : Array Syntax) : Syntax :=
+Syntax.node `Lean.Parser.Term.app #[fn, mkNullNode args]
+
+def mkHole (ref : Syntax) : Syntax :=
+Syntax.node `Lean.Parser.Term.hole #[mkAtomFrom ref "_"]
+
+/-- Convert a `Syntax.ident` into a `Lean.Parser.Term.id` node -/
+def mkTermIdFromIdent (ident : Syntax) : Syntax :=
+match ident with
+| Syntax.ident _ _ _ _ => Syntax.node `Lean.Parser.Term.id #[ident, mkNullNode]
+| _                    => unreachable!
+
+/--
+  Create a simple `Lean.Parser.Term.id` syntax using position
+  information from `ref` and name `n`. By simple, we mean that
+  `optional (explicitUniv <|> namedPattern)` is none.
+  To refer to a specific constant, use `mkCTermIdFrom` instead. -/
+def mkTermIdFrom (ref : Syntax) (n : Name) : Syntax :=
+mkTermIdFromIdent (mkIdentFrom ref n)
+
+/-- Variant of `mkTermIdFrom` that makes sure that the identifier cannot accidentally
+    be captured. -/
+def mkCTermIdFrom (ref : Syntax) (c : Name) : Syntax :=
+mkTermIdFromIdent (mkCIdentFrom ref c)
+
+def mkTermId (n : Name) : Syntax :=
+mkTermIdFrom Syntax.missing n
+
+def mkCTermId (c : Name) : Syntax :=
+mkCTermIdFrom Syntax.missing c
+
+def mkCAppStx (fn : Name) (args : Array Syntax) : Syntax :=
+mkAppStx (mkCTermId fn) args
+
+def mkStxLit (kind : SyntaxNodeKind) (val : String) (info : Option SourceInfo := none) : Syntax :=
+let atom : Syntax := Syntax.atom info val;
+Syntax.node kind #[atom]
+
+def mkStxStrLit (val : String) (info : Option SourceInfo := none) : Syntax :=
+mkStxLit strLitKind (repr val) info
+
+def mkStxNumLit (val : String) (info : Option SourceInfo := none) : Syntax :=
+mkStxLit numLitKind val info
+
 end Lean
 
 abbrev Array.getSepElems := @Array.getEvenElems