Skip to content

Commit f767e5c

Browse files
srghmasrghma
committed
feat: implement bidi
1 parent 3669c3e commit f767e5c

22 files changed

Lines changed: 11434 additions & 55 deletions

File tree

‎UnicodeBasic.lean‎

Lines changed: 98 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
-/
55
module
66
public import UnicodeBasic.Types
7+
public import UnicodeBasic.Bidi
78
import UnicodeData.Core.BidiBrackets
89
import UnicodeData.Core.BidiMirroring
910
import UnicodeData.Core.Blocks
@@ -531,6 +532,103 @@ public def isBidiControl (char : Char) : Bool :=
531532
|| char.val <= 0x202E && char.val >= 0x202A
532533
|| char.val <= 0x2069 && char.val >= 0x2066
533534

535+
/-- Check whether a character has a specific bidi class. -/
536+
@[inline]
537+
public def isBidiClass (bc : BidiClass) (char : Char) : Bool :=
538+
getBidiClass char == bc
539+
540+
/-- Check if bidirectional left-to-right character -/
541+
@[inline]
542+
public def isBidiLeftToRight (char : Char) : Bool := isBidiClass .L char
543+
544+
/-- Check if bidirectional right-to-left character -/
545+
@[inline]
546+
public def isBidiRightToLeft (char : Char) : Bool := isBidiClass .R char
547+
548+
/-- Check if bidirectional arabic letter character -/
549+
@[inline]
550+
public def isBidiArabicLetter (char : Char) : Bool := isBidiClass .AL char
551+
552+
/-- Check if bidirectional european number character -/
553+
@[inline]
554+
public def isBidiEuropeanNumber (char : Char) : Bool := isBidiClass .EN char
555+
556+
/-- Check if bidirectional arabic number character -/
557+
@[inline]
558+
public def isBidiArabicNumber (char : Char) : Bool := isBidiClass .AN char
559+
560+
/-- Check if bidirectional european separator character -/
561+
@[inline]
562+
public def isBidiEuropeanSeparator (char : Char) : Bool := isBidiClass .ES char
563+
564+
/-- Check if bidirectional european terminator character -/
565+
@[inline]
566+
public def isBidiEuropeanTerminator (char : Char) : Bool := isBidiClass .ET char
567+
568+
/-- Check if bidirectional common separator character -/
569+
@[inline]
570+
public def isBidiCommonSeparator (char : Char) : Bool := isBidiClass .CS char
571+
572+
/-- Check if bidirectional nonspacing mark character -/
573+
@[inline]
574+
public def isBidiNonspacingMark (char : Char) : Bool := isBidiClass .NSM char
575+
576+
/-- Check if bidirectional boundary neutral character -/
577+
@[inline]
578+
public def isBidiBoundaryNeutral (char : Char) : Bool := isBidiClass .BN char
579+
580+
/-- Check if bidirectional paragraph separator character -/
581+
@[inline]
582+
public def isBidiParagraphSeparator (char : Char) : Bool := isBidiClass .B char
583+
584+
/-- Check if bidirectional segment separator character -/
585+
@[inline]
586+
public def isBidiSegmentSeparator (char : Char) : Bool := isBidiClass .S char
587+
588+
/-- Check if bidirectional white space character -/
589+
@[inline]
590+
public def isBidiWhiteSpace (char : Char) : Bool := isBidiClass .WS char
591+
592+
/-- Check if bidirectional other neutral character -/
593+
@[inline]
594+
public def isBidiOtherNeutral (char : Char) : Bool := isBidiClass .ON char
595+
596+
/-- Check if bidirectional left-to-right embedding character -/
597+
@[inline]
598+
public def isBidiLeftToRightEmbedding (char : Char) : Bool := isBidiClass .LRE char
599+
600+
/-- Check if bidirectional left-to-right override character -/
601+
@[inline]
602+
public def isBidiLeftToRightOverride (char : Char) : Bool := isBidiClass .LRO char
603+
604+
/-- Check if bidirectional right-to-left embedding character -/
605+
@[inline]
606+
public def isBidiRightToLeftEmbedding (char : Char) : Bool := isBidiClass .RLE char
607+
608+
/-- Check if bidirectional right-to-left override character -/
609+
@[inline]
610+
public def isBidiRightToLeftOverride (char : Char) : Bool := isBidiClass .RLO char
611+
612+
/-- Check if bidirectional pop directional format character -/
613+
@[inline]
614+
public def isBidiPopDirectionalFormat (char : Char) : Bool := isBidiClass .PDF char
615+
616+
/-- Check if bidirectional left-to-right isolate character -/
617+
@[inline]
618+
public def isBidiLeftToRightIsolate (char : Char) : Bool := isBidiClass .LRI char
619+
620+
/-- Check if bidirectional right-to-left isolate character -/
621+
@[inline]
622+
public def isBidiRightToLeftIsolate (char : Char) : Bool := isBidiClass .RLI char
623+
624+
/-- Check if bidirectional first strong isolate character -/
625+
@[inline]
626+
public def isBidiFirstStrongIsolate (char : Char) : Bool := isBidiClass .FSI char
627+
628+
/-- Check if bidirectional pop directional isolate character -/
629+
@[inline]
630+
public def isBidiPopDirectionalIsolate (char : Char) : Bool := isBidiClass .PDI char
631+
534632
/-!
535633
## General Category ##
536634
-/

‎UnicodeBasic/Bidi.lean‎

Lines changed: 113 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,113 @@
1+
/-
2+
Copyright © 2026 François G. Dorais. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
-/
5+
module
6+
public import UnicodeBasic.Types
7+
8+
namespace Unicode
9+
10+
/-- Paragraph direction used for bidi resolution. -/
11+
public inductive BidiParagraphDirection where
12+
| ltr
13+
| rtl
14+
| autoLtr
15+
deriving Inhabited, DecidableEq, Repr
16+
17+
public instance : ToString BidiParagraphDirection where
18+
toString
19+
| .ltr => "ltr"
20+
| .rtl => "rtl"
21+
| .autoLtr => "autoLtr"
22+
23+
/-- Result of a bidi resolution query. -/
24+
public structure BidiResolution where
25+
paragraphLevel : Nat
26+
resolvedLevels : Array (Option Nat)
27+
visualOrder : Array Nat
28+
deriving Inhabited, DecidableEq, Repr
29+
30+
namespace CLib
31+
32+
@[extern "unicode_bidi_query_case"]
33+
protected opaque queryCase (text : Array UInt32) (paragraphDirection : UInt32) (fileFormat : UInt32) : String
34+
35+
end CLib
36+
37+
private def paragraphDirectionCode : BidiParagraphDirection → UInt32
38+
| .ltr => 0
39+
| .rtl => 1
40+
| .autoLtr => 2
41+
42+
private def encodeBidiClass : BidiClass → UInt32
43+
| .leftToRight => 2
44+
| .otherNeutral => 3
45+
| .rightToLeft => 4
46+
| .europeanNumber => 5
47+
| .europeanSeparator => 6
48+
| .europeanTerminator => 7
49+
| .arabicNumber => 8
50+
| .commonSeparator => 9
51+
| .paragraphSeparator => 10
52+
| .segmentSeparator => 11
53+
| .whiteSpace => 12
54+
| .arabicLetter => 13
55+
| .nonspacingMark => 14
56+
| .boundaryNeutral => 15
57+
| .popDirectionalFormat => 16
58+
| .leftToRightEmbedding => 17
59+
| .leftToRightOverride => 18
60+
| .rightToLeftEmbeding => 19
61+
| .rightToLeftOverride => 20
62+
| .leftToRightIsolate => 21
63+
| .rightToLeftIsolate => 22
64+
| .firstStrongIsolate => 23
65+
| .popDirectionalIsolate => 24
66+
67+
private def parseNatArray (s : String) : Option (Array Nat) := do
68+
let mut out := #[]
69+
for part in s.splitOn " " do
70+
if part.isEmpty then
71+
continue
72+
out := out.push (← part.toNat?)
73+
return out
74+
75+
private def parseOptNatArray (s : String) : Option (Array (Option Nat)) := do
76+
let mut out := #[]
77+
for part in s.splitOn " " do
78+
if part.isEmpty then
79+
continue
80+
if part == "x" then
81+
out := out.push none
82+
else
83+
out := out.push (some (← part.toNat?))
84+
return out
85+
86+
private def parseQueryOutput (raw : String) : Option BidiResolution := do
87+
let parts := raw.splitOn ";" |>.toArray
88+
if parts.size ≠ 3 then
89+
none
90+
else
91+
let paragraphLevel ← parts[0]!.toNat?
92+
let resolvedLevels ← parseOptNatArray parts[1]!
93+
let visualOrder ← parseNatArray parts[2]!
94+
return { paragraphLevel, resolvedLevels, visualOrder }
95+
96+
private def resolveRaw (text : Array UInt32) (paragraphDirection : BidiParagraphDirection) (fileFormat : UInt32) : Except String BidiResolution :=
97+
let raw := CLib.queryCase text (paragraphDirectionCode paragraphDirection) fileFormat
98+
if raw.startsWith "ERR:" then
99+
.error raw
100+
else
101+
match parseQueryOutput raw with
102+
| some out => .ok out
103+
| none => .error raw
104+
105+
/-- Resolve bidi levels and order for a code-point sequence. -/
106+
public def resolveBidiText (text : Array UInt32) (paragraphDirection : BidiParagraphDirection) : Except String BidiResolution :=
107+
resolveRaw text paragraphDirection 0
108+
109+
/-- Resolve bidi levels and order for a sequence of bidi classes. -/
110+
public def resolveBidiClasses (classes : Array BidiClass) (paragraphDirection : BidiParagraphDirection) : Except String BidiResolution :=
111+
resolveRaw (classes.map encodeBidiClass) paragraphDirection 1
112+
113+
end Unicode

‎UnicodeCLib/bidi.c‎

Lines changed: 63 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,63 @@
1+
#include <lean/lean.h>
2+
#include <stdio.h>
3+
#include <stdlib.h>
4+
5+
#include "bidiref/brutils.c"
6+
#include "bidiref/brtable.c"
7+
#include "bidiref/brrule.c"
8+
#include "bidiref/brtest.c"
9+
10+
static int unicode_bidi_initialized = 0;
11+
12+
static int unicode_bidi_init(void) {
13+
if (!unicode_bidi_initialized) {
14+
int rc = br_InitWithPath(UBACUR, "data/ucd/core/");
15+
if (rc != BR_TESTOK) {
16+
return rc;
17+
}
18+
unicode_bidi_initialized = 1;
19+
}
20+
return BR_TESTOK;
21+
}
22+
23+
static uint32_t unicode_bidi_class_code(lean_obj_arg v) {
24+
return lean_unbox_uint32(v);
25+
}
26+
27+
LEAN_EXPORT lean_obj_res unicode_bidi_query_case(
28+
lean_obj_arg text,
29+
uint32_t paragraphDirection,
30+
uint32_t fileFormat) {
31+
int rc = unicode_bidi_init();
32+
if (rc != BR_TESTOK) {
33+
return lean_mk_string("ERR:init");
34+
}
35+
36+
SetFileFormat((int)fileFormat);
37+
38+
size_t len = lean_array_size(text);
39+
U_Int_32 *buf = (U_Int_32 *)malloc(len * sizeof(U_Int_32));
40+
if (buf == NULL) {
41+
return lean_mk_string("ERR:alloc");
42+
}
43+
44+
for (size_t i = 0; i < len; i++) {
45+
lean_object *v = lean_array_uget_borrowed(text, i);
46+
buf[i] = unicode_bidi_class_code(v);
47+
}
48+
49+
int embeddingLevel = -1;
50+
char levels[4096];
51+
char order[4096];
52+
int qrc = br_QueryOneTestCase(buf, (int)len, (int)paragraphDirection,
53+
&embeddingLevel, levels, (int)sizeof(levels), order, (int)sizeof(order));
54+
free(buf);
55+
56+
if (qrc != BR_TESTOK && qrc != BR_OUTPUTERR && qrc != BR_TESTERR) {
57+
return lean_mk_string("ERR:query");
58+
}
59+
60+
char out[8192];
61+
snprintf(out, sizeof(out), "%d;%s;%s", embeddingLevel, levels, order);
62+
return lean_mk_string(out);
63+
}

0 commit comments

Comments
 (0)