-- Copyright © 2026 Lingenic LLC. All rights reserved.
-- Licensed under the Lingenic Source-Available License v2.3.
-- Production use requires a separate license from Licensor.
-- See LICENSE.md and COPYRIGHT in the project root.
--
-------------------------------------------------------------------------------
-- Lingenic-Text
-- Formally Verified Unicode Text Processing Library
--
-- Unicode Bidirectional Algorithm (UAX #9).
--
-- Implements the full Unicode Bidirectional Algorithm:
-- Resolve_Levels — embedding level resolution for a UTF-8 paragraph
-- Reorder — visual reordering from resolved levels
-- Needs_Mirror — UAX #9 L4 mirrored-glyph decision per codepoint
--
-- Self-contained module with its own Initialize. Reads BidiBrackets.txt
-- at init time for N0/BD16 bracket pair matching. Requires Properties
-- to be initialized first (for Bidi_Class lookup).
--
-- Algorithm phases:
-- P2/P3 — Paragraph level determination
-- X1–X8 — Explicit embedding/override/isolate level resolution
-- X9/X10 — Isolating run sequence computation
-- W1–W7 — Weak type resolution
-- N0 — Bracket pair resolution (BD16)
-- N1–N2 — Neutral type resolution
-- I1–I2 — Implicit level resolution
-- L1 — Whitespace level reset
-- L2 — Visual reordering
-- L4 — Mirrored glyph selection (per-codepoint decision)
--
-- Data tables:
-- Bracket_Open_Table — opening bracket → closing bracket mapping
-- Bracket_Close_Table — closing bracket → opening bracket mapping
-------------------------------------------------------------------------------
with Lingenic_Text.Bidi_Spec;
with Lingenic_Text.Properties;
package Lingenic_Text.Bidi
with SPARK_Mode,
Abstract_State => Bidi_State,
Initializes => Bidi_State
is
use Bidi_Spec;
---------------------------------------------------------------------------
-- Initialization
---------------------------------------------------------------------------
function Initialized return Boolean
with Global => Bidi_State;
procedure Initialize
(UCD_Dir : String;
Success : out Boolean)
with Global => (Output => Bidi_State,
Input => Properties.Property_State),
Pre => Properties.Initialized,
Post => (if Success then Initialized);
---------------------------------------------------------------------------
-- Types
---------------------------------------------------------------------------
subtype Paragraph_Length is Natural range 0 .. Max_Paragraph_CPs;
type Level_Array is array (1 .. Max_Paragraph_CPs) of Embedding_Level;
type Index_Array is array (1 .. Max_Paragraph_CPs) of Natural;
type Paragraph_Direction is (Dir_Auto, Dir_LTR, Dir_RTL);
---------------------------------------------------------------------------
-- Resolve_Levels
--
-- Decode a UTF-8 paragraph, determine paragraph level, and resolve
-- embedding levels for each codepoint.
--
-- Dir selects how the paragraph level is determined:
-- Dir_Auto — P2/P3 (first strong character)
-- Dir_LTR — force level 0
-- Dir_RTL — force level 1
--
-- On success:
-- Num_CPs = number of codepoints decoded
-- Para_Level = determined paragraph level (0 or 1)
-- Levels(1..Num_CPs) = resolved embedding levels
--
-- On failure (invalid UTF-8, too many codepoints, etc.):
-- Num_CPs = 0, Success = False
---------------------------------------------------------------------------
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)
with Pre => Initialized
and then Properties.Initialized
and then Text'Length >= 1
and then Text'Last < Positive'Last,
Post => (if Success then
Num_CPs >= 1
and then Num_CPs <= Max_Paragraph_CPs
and then Para_Level <= 1
-- Paragraph level determination (P2/P3)
and then (if Dir = Dir_LTR then Para_Level = 0)
and then (if Dir = Dir_RTL then Para_Level = 1)
and then (for all I in 1 .. Num_CPs =>
Levels (I) <= Max_Depth + 1)
else
Num_CPs = 0),
Global => (Input => (Bidi_State, Properties.Property_State));
---------------------------------------------------------------------------
-- Reorder
--
-- Compute a visual reordering from resolved embedding levels (L2).
--
-- On success:
-- Order(1..Num_CPs) = visual display order (indices into logical order)
--
-- On failure (should not happen with valid Resolve_Levels output):
-- Success = False
---------------------------------------------------------------------------
procedure Reorder
(Levels : Level_Array;
Num_CPs : Paragraph_Length;
Para_Level : Embedding_Level;
Order : out Index_Array;
Success : out Boolean)
with Pre => Num_CPs >= 1
and then Num_CPs <= Max_Paragraph_CPs
and then Para_Level <= 1
and then (for all I in 1 .. Num_CPs =>
Levels (I) <= Max_Depth + 1),
Post => (if Success then
-- Range: every output index is in bounds
(for all I in 1 .. Num_CPs =>
Order (I) >= 1 and Order (I) <= Num_CPs)
-- Surjectivity: every value appears (permutation)
and then
(for all V in 1 .. Num_CPs =>
(for some I in 1 .. Num_CPs =>
Order (I) = V))),
Global => null;
---------------------------------------------------------------------------
-- Needs_Mirror — UAX #9 rule L4
--
-- Decides whether the output glyph at a given position must be the
-- mirrored form of the input character, per UAX #9 §3.4 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."
--
-- The resolved directionality is derived from the resolved embedding
-- level: odd levels are RTL (R), even levels are LTR (L). The result
-- is therefore a pure function of the codepoint and its resolved
-- level; no auxiliary state is needed beyond the Bidi_Mirrored
-- property exposed by Properties.
--
-- This function returns the decision only — producing the actual
-- mirrored glyph from a mirrored codepoint is a rendering-layer
-- responsibility and is out of scope for text processing.
---------------------------------------------------------------------------
function Needs_Mirror
(CP : Codepoint;
Level : Embedding_Level) return Boolean
with Pre => Properties.Initialized,
Post => Needs_Mirror'Result =
((Level mod 2 = 1)
and then Properties.Get_Bidi_Mirrored (CP)),
Global => (Input => Properties.Property_State);
end Lingenic_Text.Bidi;