From 99aca85ac7282e786704251d0b053a59d77ea2f3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 15 Jan 2020 12:02:02 -0800 Subject: [PATCH] refactor: move declarations used at `macro` command to `LeanInit` --- src/Init/Lean/Data/Name.lean | 9 ------ src/Init/Lean/Syntax.lean | 37 ---------------------- src/Init/LeanInit.lean | 59 ++++++++++++++++++++++++++++++++++++ 3 files changed, 59 insertions(+), 46 deletions(-) diff --git a/src/Init/Lean/Data/Name.lean b/src/Init/Lean/Data/Name.lean index 1670948cbc..e1dff24002 100644 --- a/src/Init/Lean/Data/Name.lean +++ b/src/Init/Lean/Data/Name.lean @@ -42,15 +42,6 @@ def components' : Name → List Name def components (n : Name) : List Name := n.components'.reverse -@[extern "lean_name_eq"] -protected def beq : (@& Name) → (@& Name) → Bool -| anonymous, anonymous => true -| str p₁ s₁ _, str p₂ s₂ _ => s₁ == s₂ && beq p₁ p₂ -| num p₁ n₁ _, num p₂ n₂ _ => n₁ == n₂ && beq p₁ p₂ -| _, _ => false - -instance : HasBeq Name := ⟨Name.beq⟩ - def eqStr : Name → String → Bool | str anonymous s _, s' => s == s' | _, _ => false diff --git a/src/Init/Lean/Syntax.lean b/src/Init/Lean/Syntax.lean index 55ab07b8b6..6f0d54d41d 100644 --- a/src/Init/Lean/Syntax.lean +++ b/src/Init/Lean/Syntax.lean @@ -9,13 +9,6 @@ import Init.Lean.Data.Name import Init.Lean.Data.Format namespace Lean -structure SourceInfo := -/- Will be inferred after parsing by `Syntax.updateLeading`. During parsing, - it is not at all clear what the preceding token was, especially with backtracking. -/ -(leading : Substring) -(pos : String.Pos) -(trailing : Substring) - namespace SourceInfo def updateTrailing (info : SourceInfo) (trailing : Substring) : SourceInfo := @@ -36,8 +29,6 @@ end SourceInfo /- Node kind generation -/ -abbrev SyntaxNodeKind := Name - @[matchPattern] def choiceKind : SyntaxNodeKind := `choice @[matchPattern] def nullKind : SyntaxNodeKind := `null def strLitKind : SyntaxNodeKind := `strLit @@ -47,15 +38,6 @@ def fieldIdxKind : SyntaxNodeKind := `fieldIdx /- Syntax AST -/ -inductive Syntax -| missing {} : Syntax -| node (kind : SyntaxNodeKind) (args : Array Syntax) : Syntax -| atom {} (info : Option SourceInfo) (val : String) : Syntax -| ident {} (info : Option SourceInfo) (rawVal : Substring) (val : Name) (preresolved : List (Name × List String)) : Syntax - -instance stxInh : Inhabited Syntax := -⟨Syntax.missing⟩ - def Syntax.isMissing : Syntax → Bool | Syntax.missing => true | _ => false @@ -138,12 +120,6 @@ def asNode : Syntax → SyntaxNode def getNumArgs (stx : Syntax) : Nat := stx.asNode.getNumArgs -def getArgs (stx : Syntax) : Array Syntax := -stx.asNode.getArgs - -def getArg (stx : Syntax) (i : Nat) : Syntax := -stx.asNode.getArg i - def setArgs (stx : Syntax) (args : Array Syntax) : Syntax := match stx with | node k _ => node k args @@ -167,16 +143,6 @@ match stx with def getIdAt (stx : Syntax) (i : Nat) : Name := (stx.getArg i).getId -def getKind (stx : Syntax) : SyntaxNodeKind := -match stx with -| Syntax.node k args => k --- We use these "pseudo kinds" for antiquotation kinds. --- For example, an antiquotation `$id:ident` (using Lean.Parser.Term.ident) --- is compiled to ``if stx.isOfKind `ident ...`` -| Syntax.missing => `missing -| Syntax.atom _ v => v -| Syntax.ident _ _ _ _ => `ident - @[specialize] partial def mreplace {m : Type → Type} [Monad m] (fn : Syntax → m (Option Syntax)) : Syntax → m (Syntax) | stx@(node kind args) => do o ← fn stx; @@ -185,9 +151,6 @@ match stx with | none => do args ← args.mapM mreplace; pure (node kind args) | stx => do o ← fn stx; pure $ o.getD stx -def isOfKind : Syntax → SyntaxNodeKind → Bool -| stx, k => stx.getKind == k - @[specialize] partial def mrewriteBottomUp {m : Type → Type} [Monad m] (fn : Syntax → m (Syntax)) : Syntax → m (Syntax) | node kind args => do args ← args.mapM mrewriteBottomUp; diff --git a/src/Init/LeanInit.lean b/src/Init/LeanInit.lean index 186d06c93d..06c6e70893 100644 --- a/src/Init/LeanInit.lean +++ b/src/Init/LeanInit.lean @@ -5,6 +5,7 @@ Authors: Leonardo de Moura -/ prelude import Init.Data.String.Basic +import Init.Data.Array.Basic import Init.Data.UInt import Init.Data.Hashable @@ -47,6 +48,15 @@ Name.num p v $ mixHash (hash p) (hash v) def mkNameSimple (s : String) : Name := mkNameStr Name.anonymous s +@[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 + +instance : HasBeq Name := ⟨Name.beq⟩ + inductive ParserKind | leading | trailing @@ -97,4 +107,53 @@ abbrev TrailingParserDescr := ParserDescrCore ParserKind.trailing @[matchPattern] abbrev ParserDescr.pushLeading := @ParserDescrCore.pushLeading @[matchPattern] abbrev ParserDescr.parser := @ParserDescrCore.parser +/- Syntax -/ + +structure SourceInfo := +/- Will be inferred after parsing by `Syntax.updateLeading`. During parsing, + it is not at all clear what the preceding token was, especially with backtracking. -/ +(leading : Substring) +(pos : String.Pos) +(trailing : Substring) + +abbrev SyntaxNodeKind := Name + +/- Syntax AST -/ + +inductive Syntax +| missing {} : Syntax +| node (kind : SyntaxNodeKind) (args : Array Syntax) : Syntax +| atom {} (info : Option SourceInfo) (val : String) : Syntax +| ident {} (info : Option SourceInfo) (rawVal : Substring) (val : Name) (preresolved : List (Name × List String)) : Syntax + +instance Syntax.inhabited : Inhabited Syntax := +⟨Syntax.missing⟩ + +namespace Syntax + +def getKind (stx : Syntax) : SyntaxNodeKind := +match stx with +| Syntax.node k args => k +-- We use these "pseudo kinds" for antiquotation kinds. +-- For example, an antiquotation `$id:ident` (using Lean.Parser.Term.ident) +-- is compiled to ``if stx.isOfKind `ident ...`` +| Syntax.missing => `missing +| Syntax.atom _ v => mkNameSimple v +| Syntax.ident _ _ _ _ => `ident + +def isOfKind : Syntax → SyntaxNodeKind → Bool +| stx, k => stx.getKind == k + +def getArg (stx : Syntax) (i : Nat) : Syntax := +match stx with +| Syntax.node _ args => args.get! i +| _ => arbitrary _ + +def getArgs (stx : Syntax) : Array Syntax := +match stx with +| Syntax.node _ args => args +| _ => #[] + +end Syntax + end Lean