Skip to content

Commit d97721f

Browse files
fgdoraisfgdorais
committed
chore: cleanup executables
1 parent 6b0500d commit d97721f

2 files changed

Lines changed: 60 additions & 60 deletions

File tree

‎makeTables.lean‎

Lines changed: 59 additions & 59 deletions
Original file line numberDiff line numberDiff line change
@@ -144,9 +144,9 @@ def mkDecompositionMapping : IO <| Array (UInt32 × String) := do
144144
for data in UnicodeData.data do
145145
match data.decomp with
146146
| some ⟨none, l⟩ =>
147-
t := t.push (data.code, ";" ++ ";".intercalate (l.map (toHexStringAux <| Char.val .)))
147+
t := t.push (data.code, ";" ++ ";".intercalate (l.map (toHexStringRaw <| Char.val .)))
148148
| some ⟨some k, l⟩ =>
149-
t := t.push (data.code, s!"{k};" ++ ";".intercalate (l.map (toHexStringAux <| Char.val ·)))
149+
t := t.push (data.code, s!"{k};" ++ ";".intercalate (l.map (toHexStringRaw <| Char.val ·)))
150150
| _ => continue
151151
return t
152152

@@ -548,278 +548,278 @@ def main (args : List String) : IO UInt32 := do
548548
IO.FS.withFile (tableDir/(arg ++ ".txt")) .write fun file => do
549549
for (c₀, c₁) in table do
550550
if c₀ == c₁ then
551-
file.putStrLn <| toHexStringAux c₀ ++ ";"
551+
file.putStrLn <| toHexStringRaw c₀ ++ ";"
552552
else
553-
file.putStrLn <| toHexStringAux c₀ ++ ";" ++ toHexStringAux c₁
553+
file.putStrLn <| toHexStringRaw c₀ ++ ";" ++ toHexStringRaw c₁
554554
IO.println s!"Size: {(statsProp table).1} + {(statsProp table).2}"
555555
| "Bidi_Class" =>
556556
IO.println s!"Generating table {arg}"
557557
let table ← mkBidiClass
558558
IO.FS.withFile (tableDir/(arg ++ ".txt")) .write fun file => do
559559
for (c₀, c₁, bc) in table do
560560
if c₀ == c₁ then
561-
file.putStrLn <| toHexStringAux c₀ ++ ";;" ++ bc.toAbbrev
561+
file.putStrLn <| toHexStringRaw c₀ ++ ";;" ++ bc.toAbbrev
562562
else
563-
file.putStrLn <| toHexStringAux c₀ ++ ";" ++ toHexStringAux c₁ ++ ";" ++ bc.toAbbrev
563+
file.putStrLn <| toHexStringRaw c₀ ++ ";" ++ toHexStringRaw c₁ ++ ";" ++ bc.toAbbrev
564564
IO.println s!"Size: {(statsData table).1} + {(statsData table).2}"
565565
| "Bidi_Mirrored" =>
566566
IO.println s!"Generating table {arg}"
567567
let table ← mkBidiMirrored
568568
IO.FS.withFile (tableDir/(arg ++ ".txt")) .write fun file => do
569569
for (c₀, c₁) in table do
570570
if c₀ == c₁ then
571-
file.putStrLn <| toHexStringAux c₀ ++ ";"
571+
file.putStrLn <| toHexStringRaw c₀ ++ ";"
572572
else
573-
file.putStrLn <| toHexStringAux c₀ ++ ";" ++ toHexStringAux c₁
573+
file.putStrLn <| toHexStringRaw c₀ ++ ";" ++ toHexStringRaw c₁
574574
IO.println s!"Size: {(statsProp table).1} + {(statsProp table).2}"
575575
| "Canonical_Combining_Class" =>
576576
IO.println s!"Generating table {arg}"
577577
let table ← mkCanonicalCombiningClass
578578
IO.FS.withFile (tableDir/(arg ++ ".txt")) .write fun file => do
579579
for (c₀, c₁, cc) in table do
580580
if c₀ == c₁ then
581-
file.putStrLn <| ";".intercalate [toHexStringAux c₀, "", toString cc]
581+
file.putStrLn <| ";".intercalate [toHexStringRaw c₀, "", toString cc]
582582
else
583-
file.putStrLn <| ";".intercalate [toHexStringAux c₀, toHexStringAux c₁, toString cc]
583+
file.putStrLn <| ";".intercalate [toHexStringRaw c₀, toHexStringRaw c₁, toString cc]
584584
IO.println s!"Size: {(statsData table).1} + {(statsData table).2}"
585585
| "Canonical_Decomposition_Mapping" =>
586586
IO.println s!"Generating table {arg}"
587587
let table ← mkCanonicalDecompositionMapping
588588
IO.FS.withFile (tableDir/(arg ++ ".txt")) .write fun file => do
589589
for (c, l) in table do
590-
file.putStrLn <| toHexStringAux c ++ ";" ++ ";".intercalate (l.map fun c => toHexStringAux c.val)
590+
file.putStrLn <| toHexStringRaw c ++ ";" ++ ";".intercalate (l.map fun c => toHexStringRaw c.val)
591591
IO.println s!"Size: {table.size}"
592592
| "Case_Mapping" =>
593593
IO.println s!"Generating table {arg}"
594594
let table ← mkCaseMapping
595595
IO.FS.withFile (tableDir/(arg ++ ".txt")) .write fun file => do
596596
for (c₀, c₁, uc, lc, tc) in table do
597597
if c₀ == c₁ then
598-
file.putStr <| toHexStringAux c₀ ++ ";"
598+
file.putStr <| toHexStringRaw c₀ ++ ";"
599599
if c₀ == uc then
600600
file.putStr <| ";"
601601
else
602-
file.putStr <| ";" ++ toHexStringAux uc
602+
file.putStr <| ";" ++ toHexStringRaw uc
603603
if c₀ == lc then
604604
file.putStr <| ";"
605605
else
606-
file.putStr <| ";" ++ toHexStringAux lc
606+
file.putStr <| ";" ++ toHexStringRaw lc
607607
else
608-
file.putStr <| ";".intercalate <| [c₀, c₁, uc, lc].map toHexStringAux
608+
file.putStr <| ";".intercalate <| [c₀, c₁, uc, lc].map toHexStringRaw
609609
if uc == tc then
610610
file.putStrLn ";"
611611
else
612-
file.putStrLn <| ";" ++ toHexStringAux tc
612+
file.putStrLn <| ";" ++ toHexStringRaw tc
613613
IO.println s!"Size: {(statsData table).1} + {(statsData table).2}"
614614
| "Cased" =>
615615
IO.println s!"Generating table {arg}"
616616
let table ← mkCased
617617
IO.FS.withFile (tableDir/(arg ++ ".txt")) .write fun file => do
618618
for (c₀, c₁) in table do
619619
if c₀ == c₁ then
620-
file.putStrLn <| toHexStringAux c₀ ++ ";"
620+
file.putStrLn <| toHexStringRaw c₀ ++ ";"
621621
else
622-
file.putStrLn <| toHexStringAux c₀ ++ ";" ++ toHexStringAux c₁
622+
file.putStrLn <| toHexStringRaw c₀ ++ ";" ++ toHexStringRaw c₁
623623
IO.println s!"Size: {(statsProp table).1} + {(statsProp table).2}"
624624
| "Decomposition_Mapping" =>
625625
IO.println s!"Generating table {arg}"
626626
let table ← mkDecompositionMapping
627627
IO.FS.withFile (tableDir/(arg ++ ".txt")) .write fun file => do
628628
for (c, s) in table do
629-
file.putStrLn <| toHexStringAux c ++ ";" ++ s
629+
file.putStrLn <| toHexStringRaw c ++ ";" ++ s
630630
IO.println s!"Size: {table.size}"
631631
| "Default_Ignorable_Code_Point" =>
632632
IO.println s!"Generating table {arg}"
633633
let table ← mkDefaultIgnorableCodePoint
634634
IO.FS.withFile (tableDir/(arg ++ ".txt")) .write fun file => do
635635
for (c₀, c₁) in table do
636636
if c₀ == c₁ then
637-
file.putStrLn <| toHexStringAux c₀ ++ ";"
637+
file.putStrLn <| toHexStringRaw c₀ ++ ";"
638638
else
639-
file.putStrLn <| toHexStringAux c₀ ++ ";" ++ toHexStringAux c₁
639+
file.putStrLn <| toHexStringRaw c₀ ++ ";" ++ toHexStringRaw c₁
640640
IO.println s!"Size: {(statsProp table).1} + {(statsProp table).2}"
641641
| "General_Category" =>
642642
IO.println s!"Generating table {arg}"
643643
let table ← mkGC
644644
IO.FS.withFile (tableDir/(arg ++ ".txt")) .write fun file => do
645645
for (c₀, c₁, v) in table do
646646
if c₀ == c₁ then
647-
file.putStrLn <| ";".intercalate [toHexStringAux c₀, "", toString v]
647+
file.putStrLn <| ";".intercalate [toHexStringRaw c₀, "", toString v]
648648
else
649-
file.putStrLn <| ";".intercalate [toHexStringAux c₀, toHexStringAux c₁, toString v]
649+
file.putStrLn <| ";".intercalate [toHexStringRaw c₀, toHexStringRaw c₁, toString v]
650650
IO.println s!"Size: {(statsData table).1} + {(statsData table).2}"
651651
| "Lowercase" =>
652652
IO.println s!"Generating table {arg}"
653653
let table ← mkLowercase
654654
IO.FS.withFile (tableDir/(arg ++ ".txt")) .write fun file => do
655655
for (c₀, c₁) in table do
656656
if c₀ == c₁ then
657-
file.putStrLn <| toHexStringAux c₀ ++ ";"
657+
file.putStrLn <| toHexStringRaw c₀ ++ ";"
658658
else
659-
file.putStrLn <| toHexStringAux c₀ ++ ";" ++ toHexStringAux c₁
659+
file.putStrLn <| toHexStringRaw c₀ ++ ";" ++ toHexStringRaw c₁
660660
IO.println s!"Size: {(statsProp table).1} + {(statsProp table).2}"
661661
| "Math" =>
662662
IO.println s!"Generating table {arg}"
663663
let table ← mkMath
664664
IO.FS.withFile (tableDir/(arg ++ ".txt")) .write fun file => do
665665
for (c₀, c₁) in table do
666666
if c₀ == c₁ then
667-
file.putStrLn <| toHexStringAux c₀ ++ ";"
667+
file.putStrLn <| toHexStringRaw c₀ ++ ";"
668668
else
669-
file.putStrLn <| toHexStringAux c₀ ++ ";" ++ toHexStringAux c₁
669+
file.putStrLn <| toHexStringRaw c₀ ++ ";" ++ toHexStringRaw c₁
670670
IO.println s!"Size: {(statsProp table).1} + {(statsProp table).2}"
671671
| "Name" =>
672672
IO.println s!"Generating table {arg}"
673673
let table ← mkName
674674
IO.FS.withFile (tableDir/(arg ++ ".txt")) .write fun file => do
675675
for (c₀, c₁, n) in table do
676676
if c₀ == c₁ then
677-
file.putStrLn <| ";".intercalate [toHexStringAux c₀, "", n]
677+
file.putStrLn <| ";".intercalate [toHexStringRaw c₀, "", n]
678678
else
679-
file.putStrLn <| ";".intercalate [toHexStringAux c₀, toHexStringAux c₁, n]
679+
file.putStrLn <| ";".intercalate [toHexStringRaw c₀, toHexStringRaw c₁, n]
680680
IO.println s!"Size: {(statsData table).1} + {(statsData table).2}"
681681
| "Noncharacter_Code_Point" =>
682682
IO.println s!"Generating table {arg}"
683683
let table := mkNoncharacterCodePoint
684684
IO.FS.withFile (tableDir/(arg ++ ".txt")) .write fun file => do
685685
for (c₀, c₁) in table do
686686
if c₀ == c₁ then
687-
file.putStrLn <| toHexStringAux c₀ ++ ";"
687+
file.putStrLn <| toHexStringRaw c₀ ++ ";"
688688
else
689-
file.putStrLn <| toHexStringAux c₀ ++ ";" ++ toHexStringAux c₁
689+
file.putStrLn <| toHexStringRaw c₀ ++ ";" ++ toHexStringRaw c₁
690690
IO.println s!"Size: {(statsProp table).1} + {(statsProp table).2}"
691691
| "Numeric_Value" =>
692692
IO.println s!"Generating table {arg}"
693693
let table ← mkNumericValue
694694
IO.FS.withFile (tableDir/(arg ++ ".txt")) .write fun file => do
695695
for (c₀, c₁, n) in table do
696696
match n with
697-
| .decimal _ => file.putStrLn <| ";".intercalate [toHexStringAux c₀, toHexStringAux c₁, "decimal"]
697+
| .decimal _ => file.putStrLn <| ";".intercalate [toHexStringRaw c₀, toHexStringRaw c₁, "decimal"]
698698
| .digit v =>
699699
if c₀ == c₁ then
700-
file.putStrLn <| ";".intercalate [toHexStringAux c₀, "", s!"digit {v.val}"]
700+
file.putStrLn <| ";".intercalate [toHexStringRaw c₀, "", s!"digit {v.val}"]
701701
else
702702
let last := v.val + c₁.toNat - c₀.toNat
703-
file.putStrLn <| ";".intercalate [toHexStringAux c₀, toHexStringAux c₁, s!"digit {v.val}-{last}"]
704-
| .numeric v none => file.putStrLn <| ";".intercalate [toHexStringAux c₀, "", s!"numeric {v}"]
705-
| .numeric v (some d) => file.putStrLn <| ";".intercalate [toHexStringAux c₀, "", s!"numeric {v}/{d}"]
703+
file.putStrLn <| ";".intercalate [toHexStringRaw c₀, toHexStringRaw c₁, s!"digit {v.val}-{last}"]
704+
| .numeric v none => file.putStrLn <| ";".intercalate [toHexStringRaw c₀, "", s!"numeric {v}"]
705+
| .numeric v (some d) => file.putStrLn <| ";".intercalate [toHexStringRaw c₀, "", s!"numeric {v}/{d}"]
706706
IO.println s!"Size: {(statsData table).1} + {(statsData table).2}"
707707
| "Other_Alphabetic" =>
708708
IO.println s!"Generating table {arg}"
709709
let table := mkOtherAlphabetic
710710
IO.FS.withFile (tableDir/(arg ++ ".txt")) .write fun file => do
711711
for (c₀, c₁) in table do
712712
if c₀ == c₁ then
713-
file.putStrLn <| toHexStringAux c₀ ++ ";"
713+
file.putStrLn <| toHexStringRaw c₀ ++ ";"
714714
else
715-
file.putStrLn <| toHexStringAux c₀ ++ ";" ++ toHexStringAux c₁
715+
file.putStrLn <| toHexStringRaw c₀ ++ ";" ++ toHexStringRaw c₁
716716
IO.println s!"Size: {(statsProp table).1} + {(statsProp table).2}"
717717
| "Other_Default_Ignorable_Code_Point" =>
718718
IO.println s!"Generating table {arg}"
719719
let table := mkOtherDefaultIgnorableCodePoint
720720
IO.FS.withFile (tableDir/(arg ++ ".txt")) .write fun file => do
721721
for (c₀, c₁) in table do
722722
if c₀ == c₁ then
723-
file.putStrLn <| toHexStringAux c₀ ++ ";"
723+
file.putStrLn <| toHexStringRaw c₀ ++ ";"
724724
else
725-
file.putStrLn <| toHexStringAux c₀ ++ ";" ++ toHexStringAux c₁
725+
file.putStrLn <| toHexStringRaw c₀ ++ ";" ++ toHexStringRaw c₁
726726
IO.println s!"Size: {(statsProp table).1} + {(statsProp table).2}"
727727
| "Other_Lowercase" =>
728728
IO.println s!"Generating table {arg}"
729729
let table := mkOtherLowercase
730730
IO.FS.withFile (tableDir/(arg ++ ".txt")) .write fun file => do
731731
for (c₀, c₁) in table do
732732
if c₀ == c₁ then
733-
file.putStrLn <| toHexStringAux c₀ ++ ";"
733+
file.putStrLn <| toHexStringRaw c₀ ++ ";"
734734
else
735-
file.putStrLn <| toHexStringAux c₀ ++ ";" ++ toHexStringAux c₁
735+
file.putStrLn <| toHexStringRaw c₀ ++ ";" ++ toHexStringRaw c₁
736736
IO.println s!"Size: {(statsProp table).1} + {(statsProp table).2}"
737737
| "Other_Math" =>
738738
IO.println s!"Generating table {arg}"
739739
let table := mkOtherMath
740740
IO.FS.withFile (tableDir/(arg ++ ".txt")) .write fun file => do
741741
for (c₀, c₁) in table do
742742
if c₀ == c₁ then
743-
file.putStrLn <| toHexStringAux c₀ ++ ";"
743+
file.putStrLn <| toHexStringRaw c₀ ++ ";"
744744
else
745-
file.putStrLn <| toHexStringAux c₀ ++ ";" ++ toHexStringAux c₁
745+
file.putStrLn <| toHexStringRaw c₀ ++ ";" ++ toHexStringRaw c₁
746746
IO.println s!"Size: {(statsProp table).1} + {(statsProp table).2}"
747747
| "Other_Uppercase" =>
748748
IO.println s!"Generating table {arg}"
749749
let table := mkOtherUppercase
750750
IO.FS.withFile (tableDir/(arg ++ ".txt")) .write fun file => do
751751
for (c₀, c₁) in table do
752752
if c₀ == c₁ then
753-
file.putStrLn <| toHexStringAux c₀ ++ ";"
753+
file.putStrLn <| toHexStringRaw c₀ ++ ";"
754754
else
755-
file.putStrLn <| toHexStringAux c₀ ++ ";" ++ toHexStringAux c₁
755+
file.putStrLn <| toHexStringRaw c₀ ++ ";" ++ toHexStringRaw c₁
756756
IO.println s!"Size: {(statsProp table).1} + {(statsProp table).2}"
757757
| "Other" =>
758758
IO.println s!"Generating table {arg}"
759759
let table := mkOther
760760
IO.FS.withFile (tableDir/(arg ++ ".txt")) .write fun file => do
761761
for (c₀, c₁, v) in table do
762762
if c₀ == c₁ then
763-
file.putStrLn <| toHexStringAux c₀ ++ ";;" ++ toString v
763+
file.putStrLn <| toHexStringRaw c₀ ++ ";;" ++ toString v
764764
else
765-
file.putStrLn <| toHexStringAux c₀ ++ ";" ++ toHexStringAux c₁ ++ ";" ++ toString v
765+
file.putStrLn <| toHexStringRaw c₀ ++ ";" ++ toHexStringRaw c₁ ++ ";" ++ toString v
766766
IO.println s!"Size: {(statsData table).1} + {(statsData table).2}"
767767
| "Prepended_Concatenation_Mark" =>
768768
IO.println s!"Generating table {arg}"
769769
let table := mkPrependedConcatenationMark
770770
IO.FS.withFile (tableDir/(arg ++ ".txt")) .write fun file => do
771771
for (c₀, c₁) in table do
772772
if c₀ == c₁ then
773-
file.putStrLn <| toHexStringAux c₀ ++ ";"
773+
file.putStrLn <| toHexStringRaw c₀ ++ ";"
774774
else
775-
file.putStrLn <| toHexStringAux c₀ ++ ";" ++ toHexStringAux c₁
775+
file.putStrLn <| toHexStringRaw c₀ ++ ";" ++ toHexStringRaw c₁
776776
IO.println s!"Size: {(statsProp table).1} + {(statsProp table).2}"
777777
| "Script_Name" =>
778778
IO.println s!"Generating table {arg}"
779779
let table := mkScriptName
780780
IO.FS.withFile (tableDir/(arg ++ ".txt")) .write fun file => do
781781
for (c, name) in table do
782-
file.putStrLn <| toHexStringAux c ++ ";" ++ name
782+
file.putStrLn <| toHexStringRaw c ++ ";" ++ name
783783
IO.println s!"Size: {table.size}"
784784
| "Titlecase" =>
785785
IO.println s!"Generating table {arg}"
786786
let table ← mkTitlecase
787787
IO.FS.withFile (tableDir/(arg ++ ".txt")) .write fun file => do
788788
for (c₀, c₁) in table do
789789
if c₀ == c₁ then
790-
file.putStrLn <| toHexStringAux c₀ ++ ";"
790+
file.putStrLn <| toHexStringRaw c₀ ++ ";"
791791
else
792-
file.putStrLn <| toHexStringAux c₀ ++ ";" ++ toHexStringAux c₁
792+
file.putStrLn <| toHexStringRaw c₀ ++ ";" ++ toHexStringRaw c₁
793793
IO.println s!"Size: {(statsProp table).1} + {(statsProp table).2}"
794794
| "Uppercase" =>
795795
IO.println s!"Generating table {arg}"
796796
let table ← mkUppercase
797797
IO.FS.withFile (tableDir/(arg ++ ".txt")) .write fun file => do
798798
for (c₀, c₁) in table do
799799
if c₀ == c₁ then
800-
file.putStrLn <| toHexStringAux c₀ ++ ";"
800+
file.putStrLn <| toHexStringRaw c₀ ++ ";"
801801
else
802-
file.putStrLn <| toHexStringAux c₀ ++ ";" ++ toHexStringAux c₁
802+
file.putStrLn <| toHexStringRaw c₀ ++ ";" ++ toHexStringRaw c₁
803803
IO.println s!"Size: {(statsProp table).1} + {(statsProp table).2}"
804804
| "Variation_Selector" =>
805805
IO.println s!"Generating table {arg}"
806806
let table := mkVariationSelector
807807
IO.FS.withFile (tableDir/(arg ++ ".txt")) .write fun file => do
808808
for (c₀, c₁) in table do
809809
if c₀ == c₁ then
810-
file.putStrLn <| toHexStringAux c₀ ++ ";"
810+
file.putStrLn <| toHexStringRaw c₀ ++ ";"
811811
else
812-
file.putStrLn <| toHexStringAux c₀ ++ ";" ++ toHexStringAux c₁
812+
file.putStrLn <| toHexStringRaw c₀ ++ ";" ++ toHexStringRaw c₁
813813
IO.println s!"Size: {(statsProp table).1} + {(statsProp table).2}"
814814
| "White_Space" =>
815815
IO.println s!"Generating table {arg}"
816816
let table := mkWhiteSpace
817817
IO.FS.withFile (tableDir/(arg ++ ".txt")) .write fun file => do
818818
for (c₀, c₁) in table do
819819
if c₀ == c₁ then
820-
file.putStrLn <| toHexStringAux c₀ ++ ";"
820+
file.putStrLn <| toHexStringRaw c₀ ++ ";"
821821
else
822-
file.putStrLn <| toHexStringAux c₀ ++ ";" ++ toHexStringAux c₁
822+
file.putStrLn <| toHexStringRaw c₀ ++ ";" ++ toHexStringRaw c₁
823823
IO.println s!"Size: {(statsProp table).1} + {(statsProp table).2}"
824824
| _ => IO.println s!"Unknown property {arg}"
825825
return 0

‎testTables.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -140,5 +140,5 @@ def main (args : List String) : IO UInt32 := do
140140
for t in tests do
141141
if t.1 ∈ args && !t.2 d then
142142
err := 1
143-
IO.println s!"Error: {t.1} {toHexStringAux d.code}"
143+
IO.println s!"Error: {t.1} {toHexStringRaw d.code}"
144144
return err

0 commit comments

Comments
 (0)