BIDIRECTIONAL ALGORITHM MODULE
==============================
Standard: UAX #9 (Unicode Bidirectional Algorithm)
Files: src/lingenic_text-bidi_spec.ads (ghost specification)
src/lingenic_text-bidi.ads (public API)
src/lingenic_text-bidi.adb (implementation)
PURPOSE
-------
The Bidi module implements the full Unicode Bidirectional Algorithm for
mixed left-to-right and right-to-left text. It resolves embedding
levels for each codepoint in a paragraph, computes visual reordering,
and determines mirrored-glyph requirements.
GHOST SPECIFICATION (Bidi_Spec)
-------------------------------
Bidi Class Values (BC_Value, 23 classes):
Strong: L, R, AL
Weak: EN, ES, ET, AN, CS, NSM, BN
Neutral: B, S, WS, ON
Explicit: LRE, RLE, LRO, RLO, PDF
Isolate: LRI, RLI, FSI, PDI
Types:
subtype Embedding_Level is Natural range 0 .. 126;
0-125: explicit levels
126: Max_Depth + 1 (implicit overflow level)
type Override_Status is (Neutral, Left_To_Right, Right_To_Left);
type Stack_Entry is record
Level : Embedding_Level;
Override : Override_Status;
Isolate : Boolean;
end record;
Constants:
Max_Depth = 125 Maximum embedding depth
Max_Paragraph_CPs = 4096 Maximum codepoints per paragraph
Max_Stack = 127 Directional status stack depth
Max_Bracket_Stack = 63 Bracket pair stack depth (BD16)
Classification Predicates:
Is_Strong(BC) L, R, or AL
Is_Weak(BC) EN, ES, ET, AN, CS, NSM, BN
Is_Neutral(BC) B, S, WS, ON
Is_Isolate_Initiator(BC) LRI, RLI, FSI
Direction_From_Level(L) Even -> L, Odd -> R
Next_Odd_Level(L) Next higher odd level
Next_Even_Level(L) Next higher even level
INITIALIZATION
--------------
procedure Initialize
(UCD_Dir : String;
Success : out Boolean);
Pre: Properties.Initialized
Post: if Success then Initialized
Reads from UCD_Dir:
BidiBrackets.txt Bracket pair mappings for N0/BD16
Maps opening brackets to closing brackets
and vice versa
Builds internal data tables:
Bracket_Open_Table Opening bracket -> closing bracket mapping
Bracket_Close_Table Closing bracket -> opening bracket mapping
PUBLIC API
----------
Resolve_Levels:
procedure Resolve_Levels
(Text : Byte_Array;
Dir : Paragraph_Direction;
Levels : out Level_Array;
Num_CPs : out Paragraph_Length;
Para_Level : out Embedding_Level;
Success : out Boolean);
Pre: Initialized, Properties.Initialized
Text'Length >= 1, Text'Last < Positive'Last
Post: if Success then
Num_CPs >= 1, Num_CPs <= Max_Paragraph_CPs
Para_Level <= 1
if Dir = Dir_LTR then Para_Level = 0
if Dir = Dir_RTL then Para_Level = 1
for all I in 1..Num_CPs => Levels(I) <= Max_Depth + 1
else
Num_CPs = 0
Paragraph_Direction:
Dir_Auto P2/P3 (first strong character determines level)
Dir_LTR Force paragraph level 0 (left-to-right)
Dir_RTL Force paragraph level 1 (right-to-left)
Algorithm Phases:
P2/P3: Determine paragraph embedding level.
Scan for first L, AL, or R (ignoring isolate pairs).
L -> level 0; AL or R -> level 1; none found -> level 0.
X1-X8: Process explicit directional formatting characters.
Build directional status stack (level, override, isolate).
LRE/RLE: push new level (next even/odd).
LRO/RLO: push new level with override.
LRI/RLI/FSI: push isolate initiator.
PDF: pop non-isolate entry.
PDI: pop back to matching isolate.
Stack depth bounded by Max_Depth (125).
X9/X10: Compute isolating run sequences.
Remove BN/explicit controls from consideration.
Group runs with matching isolate pairs.
W1-W7: Resolve weak types within each isolating run sequence.
W1: NSM -> type of previous (or sos).
W2: EN after AL -> AN.
W3: AL -> R.
W4: ES between EN -> EN; CS between EN -> EN; CS between AN -> AN.
W5: ET adjacent to EN -> EN.
W6: Remaining ES/CS/ET -> ON.
W7: EN after L (in run context) -> L.
N0: Bracket pair resolution (BD16).
Find matching bracket pairs using a bracket stack.
Assign strong type to paired brackets based on enclosed content
and embedding direction.
N1-N2: Resolve neutrals.
N1: Neutrals between strong types -> that strong type,
or direction from embedding level at boundaries.
N2: Remaining neutrals -> embedding direction.
I1-I2: Assign implicit levels.
I1: Even level: R -> level+1; AN/EN -> level+2.
I2: Odd level: L/AN/EN -> level+1.
L1: Reset whitespace/isolate/control levels.
Trailing WS, isolate controls, and paragraph separators
reset to paragraph level.
Reorder:
procedure Reorder
(Levels : Level_Array;
Num_CPs : Paragraph_Length;
Para_Level : Embedding_Level;
Order : out Index_Array;
Success : out Boolean);
Pre: Num_CPs >= 1, Num_CPs <= Max_Paragraph_CPs
Para_Level <= 1
for all I in 1..Num_CPs => Levels(I) <= Max_Depth + 1
Post: if Success then
Range: for all I => Order(I) in 1..Num_CPs
Surjection: for all V in 1..Num_CPs =>
(for some I => Order(I) = V)
Computes visual display order from resolved embedding levels (L2).
Algorithm:
1. Find the highest level among all characters
2. Starting from the highest level down to the paragraph level:
For each level, reverse the subsequences of characters at that
level or higher
3. The resulting Order array maps visual positions to logical positions
The postcondition proves that Order is a valid permutation: every
output index is in bounds, and every value from 1 to Num_CPs appears
at least once (surjectivity, which combined with the finite domain
implies bijectivity).
Needs_Mirror:
function Needs_Mirror
(CP : Codepoint;
Level : Embedding_Level) return Boolean;
Pre: Properties.Initialized
Post: Result = ((Level mod 2 = 1) and then
Properties.Get_Bidi_Mirrored(CP))
Determines if the output glyph for CP at the given resolved level
should be the mirrored form (UAX #9, Section 3.4, rule L4):
"A character is depicted by a mirrored glyph if and only if
(a) the resolved directionality of that character is R, and
(b) the Bidi_Mirrored property value of that character is Yes."
Odd levels are RTL. The function returns the decision only --
producing the actual mirrored glyph is a rendering-layer concern.
USAGE PATTERN
-------------
-- 1. Resolve levels for the paragraph
Resolve_Levels (Text, Dir_Auto, Levels, Num_CPs, Para_Level, Success);
if not Success then
-- Handle error (invalid UTF-8, too many codepoints, etc.)
return;
end if;
-- 2. Compute visual reordering
Reorder (Levels, Num_CPs, Para_Level, Order, Reorder_OK);
-- 3. Display in visual order
for Visual_Pos in 1 .. Num_CPs loop
Logical_Pos := Order (Visual_Pos);
CP := Codepoints (Logical_Pos);
-- 4. Check mirroring
if Needs_Mirror (CP, Levels (Logical_Pos)) then
-- Render mirrored glyph
else
-- Render normal glyph
end if;
end loop;
LIMITS
------
Max_Paragraph_CPs = 4096
Paragraphs longer than 4096 codepoints must be split.
Max_Stack = 127
Matches the Unicode standard's maximum embedding depth plus margins.
Max_Bracket_Stack = 63
Matches the Unicode standard's BD16 bracket pair stack limit.