chore: modulize

UnicodeBasic.lean

@@ -3,8 +3,9 @@ Copyright © 2023-2025 François G. Dorais. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
 
-import UnicodeBasic.Types
-import UnicodeBasic.TableLookup
+module
+public import UnicodeBasic.Types
+import all UnicodeBasic.TableLookup
 
 /-!
   # General API #

UnicodeBasic/CharacterDatabase.lean

@@ -1,8 +1,10 @@
 /-
-Copyright © 2023 François G. Dorais. All rights reserved.
+Copyright © 2023-2025 François G. Dorais. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
 
+module
+
 namespace Unicode
 
 /-- Stream type for Unicode Character Database (UCD) files

UnicodeBasic/Hangul.lean

@@ -1,8 +1,10 @@
 /-
-Copyright © 2024 François G. Dorais. All rights reserved.
+Copyright © 2024-2025 François G. Dorais. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
 
+module
+
 namespace Unicode.Hangul
 
 private def shortNameL : Array String :=

UnicodeBasic/TableLookup.lean

@@ -3,9 +3,10 @@ Copyright © 2024-2025 François G. Dorais. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
 
-import UnicodeBasic.CharacterDatabase
-import UnicodeBasic.Hangul
-import UnicodeBasic.Types
+module
+public import UnicodeBasic.Types
+import all UnicodeBasic.CharacterDatabase
+import all UnicodeBasic.Hangul
 
 namespace Unicode
 

UnicodeBasic/Types.lean

@@ -3,6 +3,9 @@ Copyright © 2023-2025 François G. Dorais. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
 
+module
+@[expose] public section
+
 /-- Low-level conversion from `UInt32` to `Char` (*unsafe*)
 
   This function translates to a no-op in the compiler. However, it does not
@@ -312,7 +315,7 @@ def mk : (major : MajorGeneralCategory) → Option (MinorGeneralCategory major)
 | _, some .privateUse => .Co
 | _, some .unassigned => .Cn
 
-private def reprAux (x : GC) (extra := false) : List String := Id.run do
+def reprAux (x : GC) (extra := false) : List String := Id.run do
   let mut c := #[]
   if .L ⊆ x then
     c := c.push "L"

UnicodeData.lean

@@ -1,7 +1,8 @@
 /-
-Copyright © 2023-2024 François G. Dorais. All rights reserved.
+Copyright © 2023-2025 François G. Dorais. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
 
-import UnicodeData.Basic
-import UnicodeData.PropList
+module
+public import UnicodeData.Basic
+public import UnicodeData.PropList

UnicodeData/Basic.lean

@@ -3,9 +3,10 @@ Copyright © 2023-2025 François G. Dorais. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
 
-import UnicodeBasic.CharacterDatabase
-import UnicodeBasic.Hangul
-import UnicodeBasic.Types
+module
+public import UnicodeBasic.Types
+import all UnicodeBasic.CharacterDatabase
+import all UnicodeBasic.Hangul
 
 namespace Unicode
 

UnicodeData/PropList.lean

@@ -1,10 +1,11 @@
 /-
-Copyright © 2023-2024 François G. Dorais. All rights reserved.
+Copyright © 2023-2025 François G. Dorais. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
 
-import UnicodeBasic.Types
-import UnicodeBasic.CharacterDatabase
+module
+public import UnicodeBasic.Types
+import all UnicodeBasic.CharacterDatabase
 
 namespace Unicode
 

lookup.lean

@@ -3,12 +3,13 @@ Copyright © 2023-2025 François G. Dorais. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
 
+module
 import UnicodeBasic
-import UnicodeData
+import all UnicodeData.Basic
 
 open Unicode
 
-def main (args : List String) : IO Unit := do
+public def main (args : List String) : IO Unit := do
   for a in args do
     match getArg? a with
     | none => IO.println s!"invalid argument: {a}"

makeCLib.lean

@@ -1,4 +1,11 @@
-import UnicodeData
+/-
+Copyright © 2025 François G. Dorais. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+-/
+
+module
+import all UnicodeData.Basic
+import all UnicodeData.PropList
 
 open Unicode
 
@@ -191,7 +198,7 @@ static const unicode_data_t table[] = {"
       file.putStrLn s!"\{UINT32_C({c₀}),UINT32_C({c₁}),UINT64_C({d})},"
     file.putStrLn "};"
 
-def main : IO UInt32 := do
+public def main : IO UInt32 := do
   makeCaseC
   makePropC
   return 0

makeTables.lean

@@ -3,7 +3,9 @@ Copyright © 2024-2025 François G. Dorais. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
 
-import UnicodeData
+module
+import all UnicodeData.Basic
+import all UnicodeData.PropList
 
 open Unicode
 
@@ -483,7 +485,7 @@ def mkWhiteSpace : Array (UInt32 × UInt32) :=
     | (c₀, some c₁) => (c₀, c₁)
     | (c₀, none) => (c₀, c₀)
 
-def main (args : List String) : IO UInt32 := do
+public def main (args : List String) : IO UInt32 := do
   let args := if args != [] then args else [
     "Bidi_Class",
     "Bidi_Mirrored",

testTables.lean

@@ -3,8 +3,11 @@ Copyright © 2024-2025 François G. Dorais. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
 
+module
 import UnicodeBasic
-import UnicodeData
+import all UnicodeBasic.TableLookup
+import all UnicodeData.Basic
+import all UnicodeData.PropList
 
 open Unicode
 
@@ -115,7 +118,7 @@ def tests : Array (String × (UnicodeData → Bool)) := #[
   ("General_Category", testGeneralCategory),
   ("White_Space", testWhiteSpace)]
 
-def main (args : List String) : IO UInt32 := do
+public def main (args : List String) : IO UInt32 := do
   let args := if args.isEmpty then tests.map Prod.fst else args.toArray
   let stream : UnicodeDataStream := {}
   let mut err : UInt32 := 0