feat: modularize

Parser.lean

@@ -2,11 +2,12 @@
 Copyright © 2022 François G. Dorais, Kyrill Serdyuk, Emma Shroyer. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
+module
 
-import Parser.Basic
-import Parser.Char
-import Parser.Error
-import Parser.Parser
-import Parser.Prelude
-import Parser.RegEx
-import Parser.Stream
+public import Parser.Basic
+public import Parser.Char
+public import Parser.Error
+public import Parser.Parser
+public import Parser.Prelude
+public import Parser.RegEx
+public import Parser.Stream

Parser/Basic.lean

@@ -2,11 +2,14 @@
 Copyright © 2022-2024 François G. Dorais, Kyrill Serdyuk, Emma Shroyer. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
+module
 
 import Parser.Prelude
-import Parser.Error
-import Parser.Parser
-import Parser.Stream
+public import Parser.Error
+public import Parser.Parser
+public import Parser.Stream
+
+public section
 
 namespace Parser
 variable [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m]

Parser/Char.lean

@@ -2,7 +2,8 @@
 Copyright © 2022-2023 François G. Dorais, Kyrill Serdyuk, Emma Shroyer. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
+module
 
-import Parser.Char.Basic
-import Parser.Char.Numeric
-import Parser.Char.Unicode
+public import Parser.Char.Basic
+public import Parser.Char.Numeric
+public import Parser.Char.Unicode

Parser/Char/Basic.lean

@@ -2,10 +2,12 @@
 Copyright © 2022 François G. Dorais, Kyrill Serdyuk, Emma Shroyer. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
+module
 
-import Parser.Basic
-import Parser.RegEx.Basic
+public import Parser.Basic
+public import Parser.RegEx.Basic
 
+public section
 namespace Parser.Char
 variable {ε σ m} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m]
 

Parser/Char/Numeric.lean

@@ -2,10 +2,12 @@
 Copyright © 2022-2023 François G. Dorais, Kyrill Serdyuk, Emma Shroyer. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
+module
 
-import Parser.Basic
-import Parser.Char.Basic
+public import Parser.Basic
+public import Parser.Char.Basic
 
+public section
 namespace Parser.Char.ASCII
 variable {ε σ m} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m]
 

Parser/Char/Unicode.lean

@@ -2,9 +2,11 @@
 Copyright © 2022 François G. Dorais, Kyrill Serdyuk, Emma Shroyer. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
+module
 
-import Parser.Char.Basic
+public import Parser.Char.Basic
 
+public section
 namespace Parser.Char.Unicode
 variable {ε σ m} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m]
 

Parser/Error.lean

@@ -2,9 +2,11 @@
 Copyright © 2022-2025 François G. Dorais, Kyrill Serdyuk, Emma Shroyer. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
+module
 
 import Parser.Prelude
-import Parser.Stream
+public import Parser.Stream
+public section
 
 /-! # Parser Error
 
@@ -84,7 +86,7 @@ inductive Simple (σ τ) [Parser.Stream σ τ]
   | addMessage : Simple σ τ → Stream.Position σ → String → Simple σ τ
 
 -- The derive handler for `Repr` fails, this is a workaround.
-private def Simple.reprPrec {σ τ} [Parser.Stream σ τ] [Repr τ] [Repr (Stream.Position σ)] :
+protected def Simple.reprPrec {σ τ} [Parser.Stream σ τ] [Repr τ] [Repr (Stream.Position σ)] :
   Simple σ τ → Nat → Std.Format
   | unexpected pos a, prec =>
     Repr.addAppParen
@@ -102,7 +104,7 @@ private def Simple.reprPrec {σ τ} [Parser.Stream σ τ] [Repr τ] [Repr (Strea
         (Std.Format.nest (if prec >= max_prec then 1 else 2)
           (Std.Format.text "Parser.Error.Simple.addMessage" ++
             Std.Format.line ++
-            reprPrec e max_prec ++
+            Simple.reprPrec e max_prec ++
             Std.Format.line ++
             reprArg pos ++
             Std.Format.line ++
@@ -112,7 +114,7 @@ private def Simple.reprPrec {σ τ} [Parser.Stream σ τ] [Repr τ] [Repr (Strea
 instance (σ τ) [Parser.Stream σ τ] [Repr τ] [Repr (Stream.Position σ)] : Repr (Simple σ τ) where
   reprPrec := Simple.reprPrec
 
-private def Simple.toString {σ τ} [Repr τ] [Parser.Stream σ τ] [Repr (Parser.Stream.Position σ)] :
+protected def Simple.toString {σ τ} [Repr τ] [Parser.Stream σ τ] [Repr (Parser.Stream.Position σ)] :
   Simple σ τ → String
   | unexpected pos (some tok) => s!"unexpected token {repr tok} at {repr pos}"
   | unexpected pos none => s!"unexpected token at {repr pos}"

Parser/Parser.lean

@@ -2,10 +2,13 @@
 Copyright © 2022-2024 François G. Dorais, Kyrill Serdyuk, Emma Shroyer. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
+module
 
 import Parser.Prelude
-import Parser.Error
-import Parser.Stream
+public import Parser.Error
+public import Parser.Stream
+
+public section
 
 /-- Parser result type. -/
 protected inductive Parser.Result.{u} (ε σ α : Type u) : Type u
@@ -19,6 +22,7 @@ protected inductive Parser.Result.{u} (ε σ α : Type u) : Type u
 `ParserT ε σ τ` is a monad transformer to parse tokens of type `τ` from the stream type `σ` with
 error type `ε`.
 -/
+@[expose]
 def ParserT (ε σ τ : Type _) [Parser.Stream σ τ] [Parser.Error ε σ τ] (m : Type _ → Type _)
   (α : Type _) : Type _ := σ → m (Parser.Result ε σ α)
 

Parser/Prelude.lean

@@ -3,8 +3,9 @@ Copyright © 2022 François G. Dorais, Kyrill Serdyuk, Emma Shroyer. All rights
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
 
-import Batteries
-import UnicodeBasic
+module
+public import Batteries
+public import UnicodeBasic
 
-instance : Std.Stream String.Slice Char where
+public instance : Std.Stream String.Slice Char where
   next? s := s.front? >>= fun c => return (c, s.drop 1)

Parser/RegEx.lean

@@ -2,6 +2,7 @@
 Copyright © 2022-2023 François G. Dorais, Kyrill Serdyuk, Emma Shroyer. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
+module
 
-import Parser.RegEx.Basic
-import Parser.RegEx.Compile
+public import Parser.RegEx.Basic
+public import Parser.RegEx.Compile

Parser/RegEx/Basic.lean

@@ -3,9 +3,11 @@
 Copyright © 2022-2023 François G. Dorais, Kyrill Serdyuk, Emma Shroyer. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
+module
 
-import Parser.Basic
+public import Parser.Basic
 
+public section
 namespace Parser
 
 /-- Type of regular expressions -/

Parser/RegEx/Compile.lean

@@ -2,10 +2,13 @@
 Copyright © 2022-2023 François G. Dorais, Kyrill Serdyuk, Emma Shroyer. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
+module
 
 import Parser.Char
 import Parser.Char.Numeric
-import Parser.RegEx.Basic
+public import Parser.RegEx.Basic
+
+public section
 
 /-! ## RegEx Syntax
 

Parser/Stream.lean

@@ -2,8 +2,9 @@
 Copyright © 2022-2025 François G. Dorais, Kyrill Serdyuk, Emma Shroyer. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
-
-import Parser.Prelude
+module
+public import Parser.Prelude
+public section
 
 /-! # Parser Stream
 
@@ -42,6 +43,7 @@ attribute [inherit_doc Parser.Stream] Parser.Stream.getPosition Parser.Stream.se
 namespace Parser.Stream
 
 /-- Stream segment type. -/
+@[expose]
 def Segment (σ) [Parser.Stream σ τ] := Stream.Position σ × Stream.Position σ
 
 /-- Start position of stream segment. -/
@@ -55,7 +57,7 @@ abbrev Segment.stop [Parser.Stream σ τ] (s : Segment σ) := s.2
 This wrapper uses the entire stream state as position information; this is not efficient. Always
 prefer tailored `Parser.Stream` instances to this default.
 -/
-@[nolint unusedArguments]
+@[expose]
 def mkDefault (σ τ) [Std.Stream σ τ] := σ
 
 @[reducible]