chore: move Lean.Data.Parsec to Std.Internal.Parsec (#5115)

Again as discussed for bootstrapping reasons.

src/Lean/Data.lean

@@ -18,7 +18,6 @@ import Lean.Data.Name
 import Lean.Data.NameMap
 import Lean.Data.OpenDecl
 import Lean.Data.Options
-import Lean.Data.Parsec
 import Lean.Data.PersistentArray
 import Lean.Data.PersistentHashMap
 import Lean.Data.PersistentHashSet

src/Lean/Data/Json/Parser.lean

@@ -6,13 +6,13 @@ Authors: Gabriel Ebner, Marc Huisinga
 -/
 prelude
 import Lean.Data.Json.Basic
-import Lean.Data.Parsec
 import Lean.Data.RBMap
+import Std.Internal.Parsec
 
 namespace Lean.Json.Parser
 
-open Lean.Parsec
-open Lean.Parsec.String
+open Std.Internal.Parsec
+open Std.Internal.Parsec.String
 
 @[inline]
 def hexChar : Parser Nat := do
@@ -216,8 +216,8 @@ namespace Json
 
 def parse (s : String) : Except String Lean.Json :=
   match Json.Parser.any s.mkIterator with
-  | Parsec.ParseResult.success _ res => Except.ok res
-  | Parsec.ParseResult.error it err  => Except.error s!"offset {repr it.i.byteIdx}: {err}"
+  | .success _ res => Except.ok res
+  | .error it err  => Except.error s!"offset {repr it.i.byteIdx}: {err}"
 
 end Json
 

src/Lean/Data/Xml/Parser.lean

@@ -4,8 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Dany Fabian
 -/
 prelude
-import Lean.Data.Parsec
+import Std.Internal.Parsec
 import Lean.Data.Xml.Basic
+
 open System
 open Lean
 
@@ -14,8 +15,8 @@ namespace Xml
 
 namespace Parser
 
-open Lean.Parsec
-open Lean.Parsec.String
+open Std.Internal.Parsec
+open Std.Internal.Parsec.String
 
 abbrev LeanChar := Char
 

src/Lean/Elab/Tactic/BVDecide/External.lean

@@ -6,7 +6,7 @@ Authors: Henrik Böving
 prelude
 import Lean.Elab.Tactic.BVDecide.LRAT.Parser
 import Lean.CoreM
-import Lean.Data.Parsec
+import Std.Internal.Parsec
 
 /-!
 This module implements the logic to call CaDiCal (or CLI interface compatible SAT solvers) and
@@ -32,14 +32,14 @@ inductive SolverResult where
 
 namespace ModelParser
 
-open Lean.Parsec
-open Lean.Parsec.ByteArray
+open Std.Internal.Parsec
+open Std.Internal.Parsec.ByteArray
 
 def parsePartialAssignment : Parser (Bool × (Array (Bool × Nat))) := do
   skipByteChar 'v'
   let idents ← many (attempt wsLit)
   let idents := idents.map (fun i => if i > 0 then (true, i.natAbs) else (false, i.natAbs))
-  Parsec.tryCatch
+  tryCatch
     (skipString " 0")
     (csuccess := fun _ => pure (true, idents))
     (cerror := fun _ => do

src/Lean/Elab/Tactic/BVDecide/LRAT/Parser.lean

@@ -6,7 +6,7 @@ Authors: Henrik Böving
 prelude
 import Init.System.IO
 import Std.Tactic.BVDecide.LRAT.Actions
-import Lean.Data.Parsec
+import Std.Internal.Parsec
 
 /-!
 This module implements parsers and serializers for both the binary and non-binary LRAT format.
@@ -28,8 +28,8 @@ private def getPivot (clause : Array Int) : Literal Nat :=
     (pivotInt.natAbs, false)
 
 
-open Lean.Parsec
-open Lean.Parsec.ByteArray
+open Std.Internal.Parsec
+open Std.Internal.Parsec.ByteArray
 
 namespace Text
 

src/Std.lean

@@ -7,3 +7,4 @@ prelude
 import Std.Data
 import Std.Sat
 import Std.Tactic
+import Std.Internal

src/Std/Internal.lean

@@ -0,0 +1,12 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+prelude
+import Std.Internal.Parsec
+
+/-!
+This directory is used for components of the standard library that are either considered
+implementation details or not yet ready for public consumption.
+-/

src/Std/Internal/Parsec.lean

@@ -4,6 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Dany Fabian
 -/
 prelude
-import Lean.Data.Parsec.Basic
-import Lean.Data.Parsec.String
-import Lean.Data.Parsec.ByteArray
+import Std.Internal.Parsec.Basic
+import Std.Internal.Parsec.String
+import Std.Internal.Parsec.ByteArray

src/Std/Internal/Parsec/Basic.lean

@@ -7,7 +7,7 @@ prelude
 import Init.NotationExtra
 import Init.Data.ToString.Macro
 
-namespace Lean
+namespace Std.Internal
 
 namespace Parsec
 
@@ -18,7 +18,7 @@ inductive ParseResult (α : Type) (ι : Type) where
 
 end Parsec
 
-def Parsec (ι : Type) (α : Type) : Type := ι → Lean.Parsec.ParseResult α ι
+def Parsec (ι : Type) (α : Type) : Type := ι → Parsec.ParseResult α ι
 
 namespace Parsec
 
@@ -144,5 +144,6 @@ def manyChars (p : Parsec ι Char) : Parsec ι String := manyCharsCore p ""
 @[inline]
 def many1Chars (p : Parsec ι Char) : Parsec ι String := do manyCharsCore p (← p).toString
 
-
 end Parsec
+
+end Std.Internal

src/Std/Internal/Parsec/ByteArray.lean

@@ -4,11 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
 prelude
-import Lean.Data.Parsec.Basic
+import Std.Internal.Parsec.Basic
 import Init.Data.ByteArray.Basic
 import Init.Data.String.Extra
 
-namespace Lean
+namespace Std.Internal
 namespace Parsec
 namespace ByteArray
 
@@ -129,4 +129,4 @@ def take (n : Nat) : Parser ByteArray := fun it =>
 
 end ByteArray
 end Parsec
-end Lean
+end Std.Internal

src/Std/Internal/Parsec/String.lean

@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Dany Fabian, Henrik Böving
 -/
 prelude
-import Lean.Data.Parsec.Basic
+import Std.Internal.Parsec.Basic
 
-namespace Lean
+namespace Std.Internal
 namespace Parsec
 namespace String
 
@@ -110,4 +110,4 @@ def take (n : Nat) : Parser String := fun it =>
 
 end String
 end Parsec
-end Lean
+end Std.Internal

tests/lean/1363.lean

@@ -1,5 +1,5 @@
-import Lean.Data.Parsec
-open Lean Parsec String
+import Std.Internal.Parsec
+open Std Internal Parsec String
 
 @[macro_inline] -- Error
 def f : Nat → Nat

tests/lean/interactive/run.lean

@@ -57,13 +57,13 @@ def Lean.Widget.GetWidgetsResponse.debugJson (r : Widget.GetWidgetsResponse) : J
     )
   ]
 
-open Parsec in
-open Parsec.String in
+open Std.Internal.Parsec in
+open Std.Internal.Parsec.String in
 def word : Parser String :=
   many1Chars <| digit <|> asciiLetter <|> pchar '_'
 
-open Parsec in
-open Parsec.String in
+open Std.Internal.Parsec in
+open Std.Internal.Parsec.String in
 def ident : Parser Name := do
   let head ← word
   let xs ← many1 (pchar '.' *> word)