From b9a548f67c857a785f6afe7d0cdc1550f73f0b69 Mon Sep 17 00:00:00 2001
From: hatzka <hello@hatzka.is>
Date: Sat, 21 Mar 2026 22:21:21 -0600
Subject: [PATCH 1/2] feat: modularize

---
 Parser.lean               | 15 ++++++++-------
 Parser/Basic.lean         |  9 ++++++---
 Parser/Char.lean          |  7 ++++---
 Parser/Char/Basic.lean    |  6 ++++--
 Parser/Char/Numeric.lean  |  6 ++++--
 Parser/Char/Unicode.lean  |  4 +++-
 Parser/Error.lean         | 10 ++++++----
 Parser/Parser.lean        |  8 ++++++--
 Parser/Prelude.lean       |  7 ++++---
 Parser/RegEx.lean         |  5 +++--
 Parser/RegEx/Basic.lean   |  4 +++-
 Parser/RegEx/Compile.lean |  5 ++++-
 Parser/Stream.lean        |  8 +++++---
 lake-manifest.json        |  2 +-
 14 files changed, 61 insertions(+), 35 deletions(-)

diff --git a/Parser.lean b/Parser.lean
index 44c3621d..4e301a7f 100644
--- a/Parser.lean
+++ b/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
diff --git a/Parser/Basic.lean b/Parser/Basic.lean
index 75d7d125..67787b62 100644
--- a/Parser/Basic.lean
+++ b/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]
diff --git a/Parser/Char.lean b/Parser/Char.lean
index 2fa485b5..70742808 100644
--- a/Parser/Char.lean
+++ b/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
diff --git a/Parser/Char/Basic.lean b/Parser/Char/Basic.lean
index 36fc71d9..9ee07e42 100644
--- a/Parser/Char/Basic.lean
+++ b/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]
 
diff --git a/Parser/Char/Numeric.lean b/Parser/Char/Numeric.lean
index 893735ae..b8ccdf5a 100644
--- a/Parser/Char/Numeric.lean
+++ b/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]
 
diff --git a/Parser/Char/Unicode.lean b/Parser/Char/Unicode.lean
index 37bd7ef7..b55ce237 100644
--- a/Parser/Char/Unicode.lean
+++ b/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]
 
diff --git a/Parser/Error.lean b/Parser/Error.lean
index 3c64e0b6..50b5e119 100644
--- a/Parser/Error.lean
+++ b/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}"
diff --git a/Parser/Parser.lean b/Parser/Parser.lean
index 80b6284c..42e6ce5c 100644
--- a/Parser/Parser.lean
+++ b/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 ε σ α)
 
diff --git a/Parser/Prelude.lean b/Parser/Prelude.lean
index 4ba90a1c..8881c05c 100644
--- a/Parser/Prelude.lean
+++ b/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)
diff --git a/Parser/RegEx.lean b/Parser/RegEx.lean
index 4127337f..260c4980 100644
--- a/Parser/RegEx.lean
+++ b/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
diff --git a/Parser/RegEx/Basic.lean b/Parser/RegEx/Basic.lean
index b0674d11..02fcfc94 100644
--- a/Parser/RegEx/Basic.lean
+++ b/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 -/
diff --git a/Parser/RegEx/Compile.lean b/Parser/RegEx/Compile.lean
index 92e54524..501c4f7a 100644
--- a/Parser/RegEx/Compile.lean
+++ b/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
 
diff --git a/Parser/Stream.lean b/Parser/Stream.lean
index e1ae572d..1d40c197 100644
--- a/Parser/Stream.lean
+++ b/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]
diff --git a/lake-manifest.json b/lake-manifest.json
index bb20d7a3..ebf424d3 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "05954ce1797e6bd6b414c916499fe6dda4a11702",
+   "rev": "603cc6effaf17675bcfc45143fef38130545291d",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

From 34a04b8a9c5e8f0460d41d3f8dff61779925ee65 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20G=2E=20Dorais?= <fgdorais@gmail.com>
Date: Fri, 15 May 2026 00:57:53 -0400
Subject: [PATCH 2/2] chore: style

---
 Parser/Basic.lean         | 2 ++
 Parser/Char/Basic.lean    | 3 +--
 Parser/Char/Unicode.lean  | 1 +
 Parser/Error.lean         | 1 +
 Parser/Parser.lean        | 2 ++
 Parser/RegEx/Basic.lean   | 3 +++
 Parser/RegEx/Compile.lean | 3 ++-
 Parser/Stream.lean        | 2 ++
 8 files changed, 14 insertions(+), 3 deletions(-)

diff --git a/Parser/Basic.lean b/Parser/Basic.lean
index 67787b62..a7e57301 100644
--- a/Parser/Basic.lean
+++ b/Parser/Basic.lean
@@ -422,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
diff --git a/Parser/Char/Basic.lean b/Parser/Char/Basic.lean
index 9ee07e42..07d26ec8 100644
--- a/Parser/Char/Basic.lean
+++ b/Parser/Char/Basic.lean
@@ -8,6 +8,7 @@ public import Parser.Basic
 public import Parser.RegEx.Basic
 
 public section
+
 namespace Parser.Char
 variable {ε σ m} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m]
 
@@ -168,5 +169,3 @@ def hexDigit : ParserT ε σ Char m (Fin 16) :=
               none
 
 end ASCII
-
-end Parser.Char
diff --git a/Parser/Char/Unicode.lean b/Parser/Char/Unicode.lean
index b55ce237..962dfb88 100644
--- a/Parser/Char/Unicode.lean
+++ b/Parser/Char/Unicode.lean
@@ -7,6 +7,7 @@ module
 public import Parser.Char.Basic
 
 public section
+
 namespace Parser.Char.Unicode
 variable {ε σ m} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m]
 
diff --git a/Parser/Error.lean b/Parser/Error.lean
index 50b5e119..39961974 100644
--- a/Parser/Error.lean
+++ b/Parser/Error.lean
@@ -6,6 +6,7 @@ module
 
 import Parser.Prelude
 public import Parser.Stream
+
 public section
 
 /-! # Parser Error
diff --git a/Parser/Parser.lean b/Parser/Parser.lean
index 42e6ce5c..0d6d1c09 100644
--- a/Parser/Parser.lean
+++ b/Parser/Parser.lean
@@ -363,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
diff --git a/Parser/RegEx/Basic.lean b/Parser/RegEx/Basic.lean
index 02fcfc94..2f6271c9 100644
--- a/Parser/RegEx/Basic.lean
+++ b/Parser/RegEx/Basic.lean
@@ -8,6 +8,7 @@ module
 public import Parser.Basic
 
 public section
+
 namespace Parser
 
 /-- Type of regular expressions -/
@@ -111,3 +112,5 @@ where
       return ms.set! lvl (some (start, stop))
 
 end
+
+end Parser.RegEx
diff --git a/Parser/RegEx/Compile.lean b/Parser/RegEx/Compile.lean
index 501c4f7a..d4e8d34a 100644
--- a/Parser/RegEx/Compile.lean
+++ b/Parser/RegEx/Compile.lean
@@ -42,7 +42,6 @@ public section
   `[`, `\`, `]` must be preceded by an escape character `\` within a class.
 -/
 
-
 namespace Parser.RegEx
 open Char
 
@@ -180,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
diff --git a/Parser/Stream.lean b/Parser/Stream.lean
index 1d40c197..3fcfcc48 100644
--- a/Parser/Stream.lean
+++ b/Parser/Stream.lean
@@ -3,7 +3,9 @@ Copyright © 2022-2025 François G. Dorais, Kyrill Serdyuk, Emma Shroyer. All ri
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
 module
+
 public import Parser.Prelude
+
 public section
 
 /-! # Parser Stream