chore: use modules

Author: fgdorais

UnicodeBasic.lean

@@ -3,8 +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.Types
-import UnicodeBasic.TableLookup
+module
+
+public import UnicodeBasic.TableLookup
+public import UnicodeBasic.Types
 
 /-!
   # General API #
@@ -40,7 +42,7 @@ import UnicodeBasic.TableLookup
   non-titlecase letter or a separator.
 -/
 
-namespace Unicode
+public section namespace Unicode
 
 /-!
   ## Name ##

UnicodeBasic/CharacterDatabase.lean

@@ -3,6 +3,8 @@ Copyright © 2023 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
@@ -12,24 +14,24 @@ namespace Unicode
   around field values are not significant. Line comments are prefixed with a
   number sign `#` (U+0023).
 -/
-structure UCDStream extends Substring.Raw where
+public structure UCDStream extends Substring.Raw where
   /-- `isUnihan` is true if the records are tab separated -/
   isUnihan := false
 deriving Inhabited
 
 namespace UCDStream
 
 /-- Make a `UCDStream` from a substring -/
-def ofSubstring (str : Substring.Raw) : UCDStream := { str with }
+public def ofSubstring (str : Substring.Raw) : UCDStream := { str with }
 
 /-- Make a `UCDStream` from a string -/
-def ofString (str : String) : UCDStream where
+public def ofString (str : String) : UCDStream where
   str := str
   startPos := 0
   stopPos := str.rawEndPos
 
 /-- Make a `UCDStream` from a file -/
-def ofFile (path : System.FilePath) : IO UCDStream :=
+public def ofFile (path : System.FilePath) : IO UCDStream :=
   ofString <$> IO.FS.readFile path
 
 /-- Get the next line from the `UCDStream`
@@ -60,7 +62,3 @@ protected def next? (stream : UCDStream) : Option (Array Substring.Raw × UCDStr
 
 instance : Std.Stream UCDStream (Array Substring.Raw) where
   next? := UCDStream.next?
-
-end UCDStream
-
-end Unicode

UnicodeBasic/Hangul.lean

@@ -3,32 +3,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
 
-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
+abbrev sizeL := shortNameL.size -- 19
+abbrev sizeV := shortNameV.size -- 21
+abbrev sizeT := shortNameT.size -- 28
+abbrev sizeLV := sizeL * sizeV -- 399
+abbrev sizeVT := sizeV * sizeT -- 588
+abbrev sizeLVT := sizeL * sizeV * sizeT -- 11172
 
-private abbrev baseL : UInt32 := 0x1100
-private abbrev baseV : UInt32 := 0x1161
-private abbrev baseT : UInt32 := 0x11A7
+abbrev baseL : UInt32 := 0x1100
+abbrev baseV : UInt32 := 0x1161
+abbrev baseT : UInt32 := 0x11A7
 
 /-- Number of Hangul syllables -/
 def Syllable.size := sizeLVT
@@ -112,5 +114,3 @@ def getSyllable! (code : UInt32) : Syllable :=
   match getSyllable? code with
   | some s => s
   | none => panic! "not a Hangul syllable"
-
-end Unicode.Hangul

UnicodeBasic/TableLookup.lean

@@ -3,24 +3,28 @@ 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
+
+import all UnicodeBasic.CharacterDatabase
+import all UnicodeBasic.Hangul
+import all UnicodeBasic.Types
+
+public import UnicodeBasic.Types
 
 namespace Unicode
 
 namespace CLib
 
 @[extern "unicode_case_lookup"]
-protected opaque lookupCase (c : UInt32) : UInt64
+public protected opaque lookupCase (c : UInt32) : UInt64
 
 protected abbrev oUpper : UInt64 := 0x100000000
 protected abbrev oLower : UInt64 := 0x200000000
 protected abbrev oAlpha : UInt64 := 0x400000000
 protected abbrev oMath  : UInt64 := 0x800000000
 
 @[extern "unicode_prop_lookup"]
-protected opaque lookupProp (c : UInt32) : UInt64
+public protected opaque lookupProp (c : UInt32) : UInt64
 
 end CLib
 
@@ -69,7 +73,7 @@ private def parsePropTable (s : String) : Thunk <| Array (UInt32 × UInt32) := I
 /-- Get bidirectional class using lookup table
 
   Unicode property: `Bidi_Class` -/
-def lookupBidiClass (c : UInt32) : BidiClass :=
+public def lookupBidiClass (c : UInt32) : BidiClass :=
   let table := table.get
   if c < table[0]!.1 then .BN else
     match table[find c (fun i => table[i]!.1) 0 table.size.toUSize]! with
@@ -82,7 +86,7 @@ where
 /-- Get canonical combining class using lookup table
 
   Unicode property: `Canonical_Combining_Class` -/
-def lookupCanonicalCombiningClass (c : UInt32) : Nat :=
+public def lookupCanonicalCombiningClass (c : UInt32) : Nat :=
   let t := table.get
   if c < t[0]!.1 then 0 else
     match t[find c (fun i => t[i]!.1) 0 t.size.toUSize]! with
@@ -97,7 +101,7 @@ where
   Unicode properties:
     `Decomposition_Mapping`
     `Decomposition_Type=Canonical` -/
-def lookupCanonicalDecompositionMapping (c : UInt32) : List UInt32 :=
+public def lookupCanonicalDecompositionMapping (c : UInt32) : List UInt32 :=
   -- Hangul syllables
   if Hangul.Syllable.base ≤ c && c ≤ Hangul.Syllable.last then
     let s := Hangul.getSyllable! c
@@ -120,7 +124,7 @@ where
     `Simple_Lowercase_Mapping`
     `Simple_Uppercase_Mapping`
     `Simple_Titlecase_Mapping` -/
-def lookupCaseMapping (c : UInt32) : UInt32 × UInt32 × UInt32 :=
+public def lookupCaseMapping (c : UInt32) : UInt32 × UInt32 × UInt32 :=
   let v : UInt64 := CLib.lookupCase c
   if v == 0 then (c, c, c) else
     let cu : UInt32 := v.toUInt32 &&& 0x001FFFFF
@@ -133,7 +137,7 @@ def lookupCaseMapping (c : UInt32) : UInt32 × UInt32 × UInt32 :=
   Unicode properties:
     `Decomposition_Mapping`
     `Decomposition_Type` -/
-def lookupDecompositionMapping? (c : UInt32) : Option DecompositionMapping :=
+public def lookupDecompositionMapping? (c : UInt32) : Option DecompositionMapping :=
   -- Hangul syllables
   if Hangul.Syllable.base ≤ c && c ≤ Hangul.Syllable.last then
     let s := Hangul.getSyllable! c
@@ -178,12 +182,12 @@ where
 
   Unicode property: `General_Category` -/
 @[inline]
-def lookupGC (c : UInt32) : GC := CLib.lookupProp c |>.toUInt32
+public def lookupGC (c : UInt32) : GC := CLib.lookupProp c |>.toUInt32
 
 /-- Get name of a code point using lookup table
 
   Unicode property: `Name` -/
-def lookupName (c : UInt32) : String :=
+public def lookupName (c : UInt32) : String :=
   let table := table.get
   if c < table[0]!.1 then unreachable! else
     match table[find c (fun i => table[i]!.1) 0 table.size.toUSize]! with
@@ -235,7 +239,7 @@ where
   Unicode properties:
     `Numeric_Type`
     `Numeric_Value` -/
-def lookupNumericValue (c : UInt32) : Option NumericType :=
+public def lookupNumericValue (c : UInt32) : Option NumericType :=
   let table := table.get
   if c < table[0]!.1 then none else
     match table[find c (fun i => table[i]!.1) 0 table.size.toUSize]! with
@@ -292,15 +296,16 @@ def lookupOther (c : UInt32) : UInt32 :=
 
   Unicode property: `Alphabetic` -/
 @[inline]
-def lookupAlphabetic (c : UInt32) : Bool :=
+public def lookupAlphabetic (c : UInt32) : Bool :=
   let m := CLib.oAlpha ||| (GC.L ||| GC.Nl).toUInt64
   CLib.lookupProp c &&& m != 0
 
 /-- Check if code point is bidi mirrored using lookup table
 
   Unicode property: `Bidi_Mirrored`
 -/
-def lookupBidiMirrored (c : UInt32) : Bool :=
+@[inline]
+public def lookupBidiMirrored (c : UInt32) : Bool :=
   let table := table.get
   if c < table[0]!.1 then false else
     match table[find c (fun i => table[i]!.1) 0 table.size.toUSize]! with
@@ -313,15 +318,15 @@ where
 
   Unicode property: `Cased` -/
 @[inline]
-def lookupCased (c : UInt32 ) : Bool :=
+public def lookupCased (c : UInt32 ) : Bool :=
   let m := CLib.oUpper ||| CLib.oLower ||| GC.LC.toUInt64
   CLib.lookupProp c &&& m != 0
 
 /-- Check if code point is a lowercase letter using lookup table
 
   Unicode property: `Lowercase` -/
 @[inline]
-def lookupLowercase (c : UInt32) : Bool :=
+public def lookupLowercase (c : UInt32) : Bool :=
   let m := CLib.oLower ||| GC.Ll.toUInt64
   CLib.lookupProp c &&& m != 0
 
@@ -330,35 +335,33 @@ def lookupLowercase (c : UInt32) : Bool :=
 
   Unicode property: `Math` -/
 @[inline]
-def lookupMath (c : UInt32) : Bool :=
+public def lookupMath (c : UInt32) : Bool :=
   let m := CLib.oMath ||| GC.Sm.toUInt64
   CLib.lookupProp c &&& m != 0
 
 /-- Check if code point is a titlecase letter using lookup table
 
   Unicode property: `Titlecase` -/
 @[inline]
-def lookupTitlecase (c : UInt32) : Bool :=
+public def lookupTitlecase (c : UInt32) : Bool :=
   lookupGC c == GC.Lt
 
 /-- Check if code point is a uppercase letter using lookup table
 
   Unicode property: `Uppercase` -/
 @[inline]
-def lookupUppercase (c : UInt32) : Bool :=
+public def lookupUppercase (c : UInt32) : Bool :=
   let m := CLib.oUpper ||| GC.Lu.toUInt64
   CLib.lookupProp c &&& m != 0
 
 /-- Check if code point is a white space character using lookup table
 
   Unicode property: `White_Space` -/
-def lookupWhiteSpace (c : UInt32) : Bool :=
+public def lookupWhiteSpace (c : UInt32) : Bool :=
   let table := table.get
   if c < table[0]!.1 then false else
     match table[find c (fun i => table[i]!.1) 0 table.size.toUSize]! with
     | (_, v) => c ≤ v
 where
   str : String := include_str "../data/table/White_Space.txt"
   table : Thunk <| Array (UInt32 × UInt32) := parsePropTable str
-
-end Unicode