From 8486807eb3b49733e85c24094a75240b6482f98f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20G=2E=20Dorais?= Date: Sun, 21 Dec 2025 15:10:16 -0500 Subject: [PATCH 1/3] chore: modulize `UnicodeBasic` --- UnicodeBasic.lean | 5 +++-- UnicodeBasic/CharacterDatabase.lean | 4 +++- UnicodeBasic/Hangul.lean | 4 +++- UnicodeBasic/TableLookup.lean | 7 ++++--- UnicodeBasic/Types.lean | 5 ++++- 5 files changed, 17 insertions(+), 8 deletions(-) diff --git a/UnicodeBasic.lean b/UnicodeBasic.lean index e587cefb4..1a5321b92 100644 --- a/UnicodeBasic.lean +++ b/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 # diff --git a/UnicodeBasic/CharacterDatabase.lean b/UnicodeBasic/CharacterDatabase.lean index 69a1fa786..0f70b161a 100644 --- a/UnicodeBasic/CharacterDatabase.lean +++ b/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 diff --git a/UnicodeBasic/Hangul.lean b/UnicodeBasic/Hangul.lean index e1b7f9e18..cee6b169f 100644 --- a/UnicodeBasic/Hangul.lean +++ b/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 := diff --git a/UnicodeBasic/TableLookup.lean b/UnicodeBasic/TableLookup.lean index 56131a90f..e06071b3d 100644 --- a/UnicodeBasic/TableLookup.lean +++ b/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 diff --git a/UnicodeBasic/Types.lean b/UnicodeBasic/Types.lean index ca6fd1598..2d0f66656 100644 --- a/UnicodeBasic/Types.lean +++ b/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" From f90e00628973fd06f55ca507286610cc5313d982 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20G=2E=20Dorais?= Date: Sun, 21 Dec 2025 15:13:07 -0500 Subject: [PATCH 2/3] chore: modulize `UnicodeData` --- UnicodeData.lean | 7 ++++--- UnicodeData/Basic.lean | 7 ++++--- UnicodeData/PropList.lean | 7 ++++--- 3 files changed, 12 insertions(+), 9 deletions(-) diff --git a/UnicodeData.lean b/UnicodeData.lean index 99b106182..035196afc 100644 --- a/UnicodeData.lean +++ b/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 diff --git a/UnicodeData/Basic.lean b/UnicodeData/Basic.lean index 3ace8974c..fc825a20d 100644 --- a/UnicodeData/Basic.lean +++ b/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 diff --git a/UnicodeData/PropList.lean b/UnicodeData/PropList.lean index d3672e56a..596eb3b16 100644 --- a/UnicodeData/PropList.lean +++ b/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 From 567ad0b233d09aaa60ddce7aa3cce89b1d302fc0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20G=2E=20Dorais?= Date: Sun, 21 Dec 2025 15:22:58 -0500 Subject: [PATCH 3/3] chore: modulize executables --- lookup.lean | 5 +++-- makeCLib.lean | 11 +++++++++-- makeTables.lean | 6 ++++-- testTables.lean | 7 +++++-- 4 files changed, 21 insertions(+), 8 deletions(-) diff --git a/lookup.lean b/lookup.lean index 5564dc742..d76cabec5 100644 --- a/lookup.lean +++ b/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}" diff --git a/makeCLib.lean b/makeCLib.lean index 0157bdcbc..89c7dabb6 100644 --- a/makeCLib.lean +++ b/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 diff --git a/makeTables.lean b/makeTables.lean index 9d2bbc0b4..e945168a3 100644 --- a/makeTables.lean +++ b/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", diff --git a/testTables.lean b/testTables.lean index 75fdaa406..33251c4e5 100644 --- a/testTables.lean +++ b/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