feat: modularize

Author: hatzka-nezumi

UnicodeBasic.lean

@@ -2,9 +2,11 @@
 Copyright © 2023-2025 François G. Dorais. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
+module
+public import UnicodeBasic.Types
+public import UnicodeBasic.TableLookup
 
-import UnicodeBasic.Types
-import UnicodeBasic.TableLookup
+public section
 
 /-!
   # General API #
@@ -855,3 +857,4 @@ def isAlphabetic (char : Char) : Bool :=
 abbrev isAlpha := isAlphabetic
 
 end Unicode
+end

UnicodeBasic/CharacterDatabase.lean

@@ -2,8 +2,9 @@
 Copyright © 2023 François G. Dorais. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
-
+module
 namespace Unicode
+public section
 
 /-- Stream type for Unicode Character Database (UCD) files
 
@@ -63,5 +64,5 @@ instance : Std.Stream UCDStream (Array String.Slice) where
   next? := UCDStream.next?
 
 end UCDStream
-
+end
 end Unicode

UnicodeBasic/Hangul.lean

@@ -2,33 +2,34 @@
 Copyright © 2024 François G. Dorais. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
-
+module
 namespace Unicode.Hangul
+public section
 
-private def shortNameL : Array String :=
+def shortNameL : Array String :=
   #["G", "GG", "N", "D", "DD", "R", "M", "B", "BB", "S",
     "SS", "", "J", "JJ", "C", "K", "T", "P", "H"]
 
-private def shortNameV : Array String :=
+def shortNameV : Array String :=
   #["A", "AE", "YA", "YAE", "EO", "E", "YEO", "YE", "O", "WA",
     "WAE", "OE", "YO", "U", "WEO", "WE", "WI", "YU", "EU", "YI",
     "I"]
 
-private def shortNameT : Array String :=
+def shortNameT : Array String :=
   #["", "G", "GG", "GS", "N", "NJ", "NH", "D", "L", "LG",
     "LM", "LB", "LS", "LT", "LP", "LH", "M", "B", "BS", "S",
     "SS", "NG", "J", "C", "K", "T", "P", "H"]
 
-private abbrev sizeL := shortNameL.size -- 19
-private abbrev sizeV := shortNameV.size -- 21
-private abbrev sizeT := shortNameT.size -- 28
-private abbrev sizeLV := sizeL * sizeV -- 399
-private abbrev sizeVT := sizeV * sizeT -- 588
-private abbrev sizeLVT := sizeL * sizeV * sizeT -- 11172
+@[expose] abbrev sizeL := shortNameL.size -- 19
+@[expose] abbrev sizeV := shortNameV.size -- 21
+@[expose] abbrev sizeT := shortNameT.size -- 28
+@[expose] abbrev sizeLV := sizeL * sizeV -- 399
+@[expose] abbrev sizeVT := sizeV * sizeT -- 588
+@[expose] abbrev sizeLVT := sizeL * sizeV * sizeT -- 11172
 
-private abbrev baseL : UInt32 := 0x1100
-private abbrev baseV : UInt32 := 0x1161
-private abbrev baseT : UInt32 := 0x11A7
+@[expose] abbrev baseL : UInt32 := 0x1100
+@[expose] abbrev baseV : UInt32 := 0x1161
+@[expose] abbrev baseT : UInt32 := 0x11A7
 
 /-- Number of Hangul syllables -/
 def Syllable.size := sizeLVT
@@ -113,4 +114,5 @@ def getSyllable! (code : UInt32) : Syllable :=
   | some s => s
   | none => panic! "not a Hangul syllable"
 
+end
 end Unicode.Hangul

UnicodeBasic/TableLookup.lean

@@ -2,10 +2,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.CharacterDatabase
 import UnicodeBasic.Hangul
-import UnicodeBasic.Types
+public import UnicodeBasic.Types
+public section
 
 namespace Unicode
 

UnicodeBasic/Types.lean

@@ -2,7 +2,8 @@
 Copyright © 2023-2025 François G. Dorais. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
-
+module
+public section
 /-- Low-level conversion from `UInt32` to `Char` (*unsafe*)
 
   This function translates to a no-op in the compiler. However, it does not
@@ -204,6 +205,7 @@ deriving DecidableEq
 /-- General category (GC)
 
   Unicode property: `General_Category` -/
+@[expose]
 def GC := UInt32 deriving DecidableEq, Inhabited
 
 namespace GC
@@ -271,22 +273,22 @@ protected def Cn  : GC := (0x20000000 : UInt32)
 protected def C   : GC := .Cc ||| .Cf ||| .Cs ||| .Co ||| .Cn
 
 def mk : (major : MajorGeneralCategory) → Option (MinorGeneralCategory major) → GC
-| .letter, none => .L
+| .letter, .none => .L
 | _, some .casedLetter => .LC
 | _, some .uppercaseLetter => .Lu
 | _, some .lowercaseLetter => .Ll
 | _, some .titlecaseLetter => .Lt
 | _, some .modifierLetter => .Lm
 | _, some .otherLetter => .Lo
-| .mark, none => .M
+| .mark, .none => .M
 | _, some .nonspacingMark => .Mn
 | _, some .spacingMark => .Mc
 | _, some .enclosingMark => .Me
-| .number, none => .N
+| .number, .none => .N
 | _, some .decimalNumber => .Nd
 | _, some .letterNumber => .Nl
 | _, some .otherNumber => .No
-| .punctuation, none => .P
+| .punctuation, .none => .P
 | _, some .connectorPunctuation => .Pc
 | _, some .dashPunctuation => .Pd
 | _, some .groupPunctuation => .PG
@@ -296,16 +298,16 @@ def mk : (major : MajorGeneralCategory) → Option (MinorGeneralCategory major)
 | _, some .initialPunctuation => .Pi
 | _, some .finalPunctuation => .Pf
 | _, some .otherPunctuation => .Po
-| .symbol, none => .S
+| .symbol, .none => .S
 | _, some .mathSymbol => .Sm
 | _, some .currencySymbol => .Sc
 | _, some .modifierSymbol => .Sk
 | _, some .otherSymbol => .So
-| .separator, none => .Z
+| .separator, .none => .Z
 | _, some .spaceSeparator => .Zs
 | _, some .lineSeparator => .Zl
 | _, some .paragraphSeparator => .Zp
-| .other, none => .C
+| .other, .none => .C
 | _, some .control => .Cc
 | _, some .format => .Cf
 | _, some .surrogate => .Cs
@@ -412,11 +414,12 @@ def toAbbrev! (x : GC) : String :=
   | [a] => a
   | _ => panic! "invalid general category"
 
-open Std.Format Repr in instance : Repr GC where
-  reprPrec x := addAppParen (group (joinSep (reprAux x |>.map (text "Unicode.GC." ++ text ·)) (text " |||" ++ line)) .fill)
+open Std.Format Repr in
+  def reprPrec (x : GC) := addAppParen (group (joinSep (reprAux x |>.map (text "Unicode.GC." ++ text ·)) (text " |||" ++ line)) .fill)
+  instance : Repr GC where reprPrec
 
-instance : ToString GC where
-  toString x := " | ".intercalate (reprAux x)
+def toString (x : GC) := " | ".intercalate (reprAux x)
+instance : ToString GC where toString
 
 def ofAbbrev? (s : String.Slice) : Option GC :=
   match s.chars.take 3 |>.toList with
@@ -464,8 +467,8 @@ def ofAbbrev? (s : String.Slice) : Option GC :=
 
 def ofAbbrev! (s : String.Slice) : GC :=
   match ofAbbrev? s with
-  | some c => c
-  | none => panic! "invalid general category"
+  | .some c => c
+  | .none => panic! "invalid general category"
 
 def ofString? (s : String.Slice) : Option GC := do
   let mut c := .none
@@ -475,8 +478,8 @@ def ofString? (s : String.Slice) : Option GC := do
 
 def ofString! (s : String.Slice) : GC :=
   match ofString? s with
-  | some c => c
-  | none => panic! "invalid general category"
+  | .some c => c
+  | .none => panic! "invalid general category"
 
 end GC
 
@@ -1012,3 +1015,4 @@ instance : Repr BidiClass where
   reprPrec bc _ := s!"Unicode.BidiClass.{bc.toAbbrev}"
 
 end Unicode
+end

UnicodeData.lean

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

UnicodeData/Aliases.lean

@@ -3,10 +3,12 @@ Copyright © 2026 François G. Dorais. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
 
-import Std.Data.HashMap
+module
+public import Std.Data.HashMap
 import UnicodeBasic.Types
 import UnicodeBasic.CharacterDatabase
 
+public section
 namespace Unicode
 
 /-- Type for list of aliases -/
@@ -125,3 +127,4 @@ def PropertyValueAliases.getShortName! (prop val : String.Slice) : String.Slice
   getShortName? prop val |>.get!
 
 end Unicode
+end

UnicodeData/Basic.lean

@@ -3,10 +3,12 @@ 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.CharacterDatabase
 import UnicodeBasic.Hangul
-import UnicodeBasic.Types
+public import UnicodeBasic.Types
 
+public section
 namespace Unicode
 
 /-- Structure for data from `UnicodeData.txt` -/
@@ -143,29 +145,8 @@ def UnicodeData.mkTangutIdeograph (c : UInt32) : UnicodeData where
 protected def UnicodeData.txt := include_str "../data/UnicodeData.txt"
 
 /-- Parse `UnicodeData.txt` -/
-private unsafe def UnicodeData.init : IO (Array UnicodeData) := do
-  let stream := UCDStream.ofString UnicodeData.txt
-  let mut arr := #[]
-  for record in stream do
-    arr := arr.push {
-      code := ofHexString! record[0]!
-      name := record[1]!
-      gc := GC.ofAbbrev! record[2]!
-      cc := record[3]!.toNat!
-      bidi := BidiClass.ofAbbrev! record[4]!
-      decomp := getDecompositionMapping? record[5]!
-      numeric := getNumericType? record[6]! record[7]! record[8]!
-      bidiMirrored := record[9]! == "Y"
-      uppercase := if record[12]!.isEmpty then none else some <| Char.mkUnsafe <| ofHexString! record[12]!
-      lowercase := if record[13]!.isEmpty then none else some <| Char.mkUnsafe <| ofHexString! record[13]!
-      titlecase := if record[14]!.isEmpty then none else some <| Char.mkUnsafe <| ofHexString! record[14]!
-    }
-  return arr
-
-where
-
-  /-- Get decomposition mapping -/
-  getDecompositionMapping? (s : String.Slice) : Option DecompositionMapping := do
+unsafe initialize UnicodeData.data : Array UnicodeData ←
+  let getDecompositionMapping? (s : String.Slice) : Option DecompositionMapping := do
     /-
       The value of the `Decomposition_Mapping` property for a character is
       provided in field 5 of `UnicodeData.txt`. This is a string-valued
@@ -218,8 +199,10 @@ where
         some ⟨tag, cs⟩
       | [] => unreachable!
 
-  /-- Get numeric type -/
-  getNumericType? (s₁ s₂ s₃ : String.Slice) : Option NumericType := do
+  let getDigitUnsafe (char : Char) : Fin 10 :=
+    unsafeCast (char.val - '0'.val).toNat
+
+  let getNumericType? (s₁ s₂ s₃ : String.Slice) : Option NumericType := do
     /-
       If the character has the property value `Numeric_Type=Decimal`, then the
       `Numeric_Value` of that digit is represented with an integer value
@@ -263,14 +246,23 @@ where
     else
       return .decimal <| getDigitUnsafe <| s₁.front
 
-  /-- Get decimal digit -/
-  @[inline]
-  getDigitUnsafe (char : Char) : Fin 10 :=
-    unsafeCast (char.val - '0'.val).toNat
-
-/-- Parsed data from `UnicodeData.txt` -/
-@[init UnicodeData.init]
-protected def UnicodeData.data : Array UnicodeData := #[]
+  let stream := UCDStream.ofString UnicodeData.txt
+  let mut arr := #[]
+  for record in stream do
+    arr := arr.push {
+      code := ofHexString! record[0]!
+      name := record[1]!
+      gc := GC.ofAbbrev! record[2]!
+      cc := record[3]!.toNat!
+      bidi := BidiClass.ofAbbrev! record[4]!
+      decomp := getDecompositionMapping? record[5]!
+      numeric := getNumericType? record[6]! record[7]! record[8]!
+      bidiMirrored := record[9]! == "Y"
+      uppercase := if record[12]!.isEmpty then none else some <| Char.mkUnsafe <| ofHexString! record[12]!
+      lowercase := if record[13]!.isEmpty then none else some <| Char.mkUnsafe <| ofHexString! record[13]!
+      titlecase := if record[14]!.isEmpty then none else some <| Char.mkUnsafe <| ofHexString! record[14]!
+    }
+  return arr
 
 /-- Get code point data from `UnicodeData.txt` -/
 partial def getUnicodeData? (code : UInt32) : Option UnicodeData := do
@@ -370,12 +362,12 @@ structure UnicodeDataStream where
   default : UInt32 → UnicodeData := UnicodeData.mkNoncharacter
   deriving Inhabited
 
-private def UnicodeDataStream.next? (s : UnicodeDataStream) : Option (UnicodeData × UnicodeDataStream) := do
+def UnicodeDataStream.next? (s : UnicodeDataStream) : Option (UnicodeData × UnicodeDataStream) := do
   let c := s.code
   let i := s.index
   if c > Unicode.max then
     none
-  else if h : i < UnicodeData.data.size.toUSize then
+  else if h : i.toNat < UnicodeData.data.size then
     let d := UnicodeData.data[i]
     let n := d.name
     if c < d.code then
@@ -412,3 +404,4 @@ instance : Std.Stream UnicodeDataStream UnicodeData where
   next? := UnicodeDataStream.next?
 
 end Unicode
+end

UnicodeData/PropList.lean

@@ -3,9 +3,11 @@ 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.Types
 import UnicodeBasic.CharacterDatabase
 
+public section
 namespace Unicode
 
 /-- Structure containing supported character properties from `PropList.txt` -/
@@ -35,7 +37,7 @@ deriving Inhabited, Repr
 /-- Raw string form `PropList.txt` -/
 protected def PropList.txt := include_str "../data/PropList.txt"
 
-private unsafe def PropList.init : IO PropList := do
+unsafe initialize PropList.data : PropList ←
   let stream := UCDStream.ofString PropList.txt
   let mut list : PropList := {}
   for record in stream do
@@ -66,10 +68,6 @@ private unsafe def PropList.init : IO PropList := do
       list := {list with deprecated := list.deprecated.push val}
   return list
 
-/-- Parsed data from `PropList.txt` -/
-@[init PropList.init]
-protected def PropList.data : PropList := {}
-
 -- TODO: stop reinventing the wheel!
 /-- Binary search -/
 private partial def find (code : UInt32) (data : Array (UInt32 × Option UInt32)) (lo hi : Nat) : Nat :=
@@ -176,3 +174,4 @@ def PropList.isDeprecated (code : UInt32) : Bool :=
     | (_, some top) => code <= top
 
 end Unicode
+end