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]
@@ -419,3 +422,5 @@ trailing `sep`, returns the array of values returned by `p`. This parser never f
 @[inline]
 def sepEndBy1 (sep : ParserT ε σ τ m β) (p : ParserT ε σ τ m α) : ParserT ε σ τ m (Array α) :=
   sepBy1 sep p <* optional sep
+
+end Parser

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,9 +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]
@@ -166,5 +169,3 @@ def hexDigit : ParserT ε σ Char m (Fin 16) :=
               none
 
 end ASCII
-
-end Parser.Char

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,8 +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,12 @@
 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 +87,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 +105,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 +115,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 ε σ α)
 
@@ -359,3 +363,5 @@ where
       p s >>= fun
       | .ok s v => return .ok s v
       | .error s f => go ps (combine e f) (Stream.setPosition s savePos)
+
+end Parser

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,8 +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
 
@@ -109,3 +112,5 @@ where
       return ms.set! lvl (some (start, stop))
 
 end
+
+end Parser.RegEx

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
 
@@ -39,7 +42,6 @@ import Parser.RegEx.Basic
   `[`, `\`, `]` must be preceded by an escape character `\` within a class.
 -/
 
-
 namespace Parser.RegEx
 open Char
 
@@ -177,3 +179,5 @@ protected def compile! (s : String) : RegEx Char :=
   match RegEx.compile? s with
   | some r => r
   | none => panic! "invalid regular expression"
+
+end Parser.RegEx

Parser/Stream.lean

@@ -2,8 +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
+public import Parser.Prelude
+
+public section
 
 /-! # Parser Stream
 
@@ -42,6 +45,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 +59,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]

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "05954ce1797e6bd6b414c916499fe6dda4a11702",
+   "rev": "603cc6effaf17675bcfc45143fef38130545291d",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",