diff --git a/src/Lean/Data.lean b/src/Lean/Data.lean index e1af358c3f..7a1854d207 100644 --- a/src/Lean/Data.lean +++ b/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 diff --git a/src/Lean/Data/Json/Parser.lean b/src/Lean/Data/Json/Parser.lean index 3856638792..907e156d18 100644 --- a/src/Lean/Data/Json/Parser.lean +++ b/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 diff --git a/src/Lean/Data/Xml/Parser.lean b/src/Lean/Data/Xml/Parser.lean index 6538224f8e..6a81fedbf2 100644 --- a/src/Lean/Data/Xml/Parser.lean +++ b/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 diff --git a/src/Lean/Elab/Tactic/BVDecide/External.lean b/src/Lean/Elab/Tactic/BVDecide/External.lean index b5ffae8f9a..8af812341f 100644 --- a/src/Lean/Elab/Tactic/BVDecide/External.lean +++ b/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 diff --git a/src/Lean/Elab/Tactic/BVDecide/LRAT/Parser.lean b/src/Lean/Elab/Tactic/BVDecide/LRAT/Parser.lean index b943305109..63f72c7567 100644 --- a/src/Lean/Elab/Tactic/BVDecide/LRAT/Parser.lean +++ b/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 diff --git a/src/Std.lean b/src/Std.lean index 7a0154f6d7..aeee8c6e31 100644 --- a/src/Std.lean +++ b/src/Std.lean @@ -7,3 +7,4 @@ prelude import Std.Data import Std.Sat import Std.Tactic +import Std.Internal diff --git a/src/Std/Internal.lean b/src/Std/Internal.lean new file mode 100644 index 0000000000..44d41356f0 --- /dev/null +++ b/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. +-/ diff --git a/src/Lean/Data/Parsec.lean b/src/Std/Internal/Parsec.lean similarity index 61% rename from src/Lean/Data/Parsec.lean rename to src/Std/Internal/Parsec.lean index 70d807260c..89319bb46b 100644 --- a/src/Lean/Data/Parsec.lean +++ b/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 diff --git a/src/Lean/Data/Parsec/Basic.lean b/src/Std/Internal/Parsec/Basic.lean similarity index 97% rename from src/Lean/Data/Parsec/Basic.lean rename to src/Std/Internal/Parsec/Basic.lean index fad7e0a3e1..6421f3f09d 100644 --- a/src/Lean/Data/Parsec/Basic.lean +++ b/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 diff --git a/src/Lean/Data/Parsec/ByteArray.lean b/src/Std/Internal/Parsec/ByteArray.lean similarity index 98% rename from src/Lean/Data/Parsec/ByteArray.lean rename to src/Std/Internal/Parsec/ByteArray.lean index 895d6f40ca..288a007b60 100644 --- a/src/Lean/Data/Parsec/ByteArray.lean +++ b/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 diff --git a/src/Lean/Data/Parsec/String.lean b/src/Std/Internal/Parsec/String.lean similarity index 97% rename from src/Lean/Data/Parsec/String.lean rename to src/Std/Internal/Parsec/String.lean index b653b521e0..2276f6e65f 100644 --- a/src/Lean/Data/Parsec/String.lean +++ b/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 diff --git a/tests/lean/1363.lean b/tests/lean/1363.lean index 1a431b4e1d..68cd8c6fec 100644 --- a/tests/lean/1363.lean +++ b/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 diff --git a/tests/lean/interactive/run.lean b/tests/lean/interactive/run.lean index 8224dc92c7..589c39b3d3 100644 --- a/tests/lean/interactive/run.lean +++ b/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)