-- 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 — Bidi Ghost Specification (UAX #9)
--
-- Defines Bidi_Class values, embedding level types, directional status
-- types, and expression functions encoding every rule of the Unicode
-- Bidirectional Algorithm.
--
-- All types and expression functions in this package are ghost-eligible
-- (Pure) and can be referenced in postconditions and loop invariants.
-- The ghost spec IS the rules.
-------------------------------------------------------------------------------
package Lingenic_Text.Bidi_Spec
with SPARK_Mode, Pure
is
---------------------------------------------------------------------------
-- Abstract Bidi_Class values (UAX #9 Table 4)
--
-- 22 classes + default (0 = unmapped).
---------------------------------------------------------------------------
-- Strong types
BC_L : constant := 1; -- Left-to-Right
BC_R : constant := 2; -- Right-to-Left
BC_AL : constant := 3; -- Right-to-Left Arabic
-- Weak types
BC_EN : constant := 4; -- European Number
BC_ES : constant := 5; -- European Number Separator
BC_ET : constant := 6; -- European Number Terminator
BC_AN : constant := 7; -- Arabic Number
BC_CS : constant := 8; -- Common Number Separator
BC_NSM : constant := 9; -- Nonspacing Mark
BC_BN : constant := 10; -- Boundary Neutral
-- Neutral types
BC_B : constant := 11; -- Paragraph Separator
BC_S : constant := 12; -- Segment Separator
BC_WS : constant := 13; -- Whitespace
BC_ON : constant := 14; -- Other Neutral
-- Explicit formatting types
BC_LRE : constant := 15; -- Left-to-Right Embedding
BC_LRO : constant := 16; -- Left-to-Right Override
BC_RLE : constant := 17; -- Right-to-Left Embedding
BC_RLO : constant := 18; -- Right-to-Left Override
BC_PDF : constant := 19; -- Pop Directional Format
BC_LRI : constant := 20; -- Left-to-Right Isolate
BC_RLI : constant := 21; -- Right-to-Left Isolate
BC_FSI : constant := 22; -- First Strong Isolate
BC_PDI : constant := 23; -- Pop Directional Isolate
BC_Default : constant := 0;
subtype BC_Value is Natural range 0 .. 23;
---------------------------------------------------------------------------
-- Embedding levels (UAX #9 BD2)
--
-- Max embedding depth = 125. Explicit levels are 0..125.
-- Implicit levels (after I1/I2) can reach 126 (= Max_Depth + 1).
---------------------------------------------------------------------------
Max_Depth : constant := 125;
subtype Embedding_Level is Natural range 0 .. Max_Depth + 1;
subtype Explicit_Level is Natural range 0 .. Max_Depth;
---------------------------------------------------------------------------
-- Paragraph size limit
---------------------------------------------------------------------------
Max_Paragraph_CPs : constant := 4096;
---------------------------------------------------------------------------
-- Directional status (UAX #9 X1)
---------------------------------------------------------------------------
type Override_Status is (Neutral, Left_To_Right, Right_To_Left);
type Stack_Entry is record
Level : Explicit_Level;
Override : Override_Status;
Isolate : Boolean;
end record;
Max_Stack : constant := Max_Depth + 2; -- 127
---------------------------------------------------------------------------
-- BD16 bracket pair stack limit
---------------------------------------------------------------------------
Max_Bracket_Stack : constant := 63;
---------------------------------------------------------------------------
-- Classification predicates
---------------------------------------------------------------------------
-- BD3: Direction implied by embedding level
function Direction_From_Level (Level : Embedding_Level) return BC_Value
is (if Level mod 2 = 0 then BC_L else BC_R);
-- Next greater odd level (X2/X4/X5a)
function Next_Odd (Level : Explicit_Level) return Natural
is (if Level mod 2 = 0 then Level + 1 else Level + 2);
-- Next greater even level (X3/X5/X5b)
function Next_Even (Level : Explicit_Level) return Natural
is (if Level mod 2 = 0 then Level + 2 else Level + 1);
-- Is this a strong type?
function Is_Strong (T : BC_Value) return Boolean
is (T = BC_L or T = BC_R or T = BC_AL);
-- Is this an isolate initiator? (LRI, RLI, FSI)
function Is_Isolate_Initiator (T : BC_Value) return Boolean
is (T = BC_LRI or T = BC_RLI or T = BC_FSI);
-- Is this an explicit embedding or override? (LRE, RLE, LRO, RLO)
function Is_Explicit_Directional (T : BC_Value) return Boolean
is (T = BC_LRE or T = BC_RLE or T = BC_LRO or T = BC_RLO);
-- X9: Characters removed from further processing
function Is_X9_Removed (T : BC_Value) return Boolean
is (T = BC_RLE or T = BC_LRE or T = BC_RLO
or T = BC_LRO or T = BC_PDF or T = BC_BN);
-- NI: Neutral or isolate formatting (used in N1/N2)
function Is_NI (T : BC_Value) return Boolean
is (T = BC_B or T = BC_S or T = BC_WS or T = BC_ON
or T = BC_FSI or T = BC_LRI or T = BC_RLI or T = BC_PDI);
-- L1: Types whose level is reset to paragraph level
function Is_L1_Reset_Type (T : BC_Value) return Boolean
is (T = BC_S or T = BC_B or T = BC_WS
or Is_Isolate_Initiator (T) or T = BC_PDI);
---------------------------------------------------------------------------
-- P rules: Paragraph level determination (UAX #9 Section 3.3.1)
---------------------------------------------------------------------------
-- P3: First strong character determines paragraph level
-- AL or R → 1, L or no strong → 0
function P3_Level (First_Strong : BC_Value) return Embedding_Level
is (if First_Strong = BC_AL or First_Strong = BC_R then 1 else 0);
---------------------------------------------------------------------------
-- W rules: Weak type resolution (UAX #9 Section 3.3.4)
--
-- Each rule is an expression function encoding the exact UAX #9 rule.
-- "Prev" / "Next" mean effective adjacent characters after X9 removal.
-- "Prev_Strong" means nearest preceding strong type (L, R, or AL),
-- or sos if none found.
---------------------------------------------------------------------------
-- W1: Examine each nonspacing mark (NSM) in the isolating run sequence,
-- and change the type of the NSM to Other Neutral if it is at the start
-- of the isolating run sequence or the previous character is an isolate
-- initiator or PDI; otherwise, change it to the type of the previous
-- character.
function W1_Resolved
(T : BC_Value; Prev : BC_Value; At_SOS : Boolean) return BC_Value
is (if T /= BC_NSM then T
elsif At_SOS then BC_ON
elsif Is_Isolate_Initiator (Prev) or Prev = BC_PDI then BC_ON
else Prev);
-- W2: Search backward from each instance of a European number until the
-- first strong type (R, L, AL, or sos) is found. If an AL is found,
-- change the type of the European number to Arabic number.
function W2_Applies (T : BC_Value; Prev_Strong : BC_Value) return Boolean
is (T = BC_EN and Prev_Strong = BC_AL);
-- W3: Change all ALs to R.
function W3_Resolved (T : BC_Value) return BC_Value
is (if T = BC_AL then BC_R else T);
-- W4: A single European separator between two European numbers changes
-- to a European number. A single common separator between two numbers
-- of the same type changes to that type.
function W4_Resolved
(T : BC_Value; Prev : BC_Value; Next : BC_Value) return BC_Value
is (if T = BC_ES and Prev = BC_EN and Next = BC_EN then BC_EN
elsif T = BC_CS and Prev = BC_EN and Next = BC_EN then BC_EN
elsif T = BC_CS and Prev = BC_AN and Next = BC_AN then BC_AN
else T);
-- W5: A sequence of European terminators adjacent to European numbers
-- changes to all European numbers.
function W5_Applies (T : BC_Value; Adjacent_EN : Boolean) return Boolean
is (T = BC_ET and Adjacent_EN);
-- W6: Otherwise, separators and terminators change to Other Neutral.
function W6_Resolved (T : BC_Value) return BC_Value
is (if T = BC_ES or T = BC_ET or T = BC_CS then BC_ON else T);
-- W7: Search backward from each instance of a European number until the
-- first strong type (R, L, or sos) is found. If an L is found, then
-- change the type of the European number to L.
function W7_Applies (T : BC_Value; Prev_Strong : BC_Value) return Boolean
is (T = BC_EN and Prev_Strong = BC_L);
---------------------------------------------------------------------------
-- N rules: Neutral type resolution (UAX #9 Section 3.3.5)
---------------------------------------------------------------------------
-- For neutral resolution, EN and AN are treated as R
function Neutral_Type (T : BC_Value) return BC_Value
is (if T = BC_EN or T = BC_AN then BC_R
elsif T = BC_L or T = BC_R then T
else BC_ON);
-- N1: A sequence of NIs takes the direction of the surrounding strong
-- text if the text on both sides has the same direction.
-- (EN and AN are treated as R for this purpose.)
function N1_Applies
(T : BC_Value; Leading : BC_Value; Trailing : BC_Value) return Boolean
is (Is_NI (T)
and then Neutral_Type (Leading) = Neutral_Type (Trailing)
and then (Neutral_Type (Leading) = BC_L
or Neutral_Type (Leading) = BC_R));
function N1_Resolved (Leading : BC_Value) return BC_Value
is (Neutral_Type (Leading));
-- N2: Any remaining NIs take the embedding direction.
function N2_Resolved
(T : BC_Value; Level : Embedding_Level) return BC_Value
is (if Is_NI (T) then Direction_From_Level (Level) else T);
---------------------------------------------------------------------------
-- N0: Bracket pair resolution (UAX #9 BD16 + N0a/N0b/N0c)
---------------------------------------------------------------------------
-- N0(a): Strong type matching embedding direction found inside pair
-- → set both brackets to embedding direction
function N0a_Applies
(Embed_Dir : BC_Value; Inner_Strong : BC_Value) return Boolean
is (Inner_Strong = Embed_Dir);
-- N0(b): Opposite strong type found inside, no matching strong type.
-- Check preceding context. If context matches embedding direction,
-- set to embedding direction. Otherwise set to opposite direction.
function N0b_Resolved
(Embed_Dir : BC_Value; Context_Dir : BC_Value) return BC_Value
is (if Context_Dir = Embed_Dir then Embed_Dir
else (if Embed_Dir = BC_L then BC_R else BC_L));
---------------------------------------------------------------------------
-- I rules: Implicit level resolution (UAX #9 Section 3.3.6)
---------------------------------------------------------------------------
-- I1: For all characters with an even (left-to-right) embedding level:
-- R → level + 1; AN, EN → level + 2
function I1_Level
(Level : Embedding_Level; T : BC_Value) return Embedding_Level
is (if T = BC_R then Level + 1
elsif T = BC_AN or T = BC_EN then Level + 2
else Level)
with Pre => Level mod 2 = 0 and Level <= Max_Depth;
-- I2: For all characters with an odd (right-to-left) embedding level:
-- L, EN, AN → level + 1
function I2_Level
(Level : Embedding_Level; T : BC_Value) return Embedding_Level
is (if T = BC_L or T = BC_EN or T = BC_AN then Level + 1
else Level)
with Pre => Level mod 2 = 1 and Level <= Max_Depth;
-- Combined implicit level resolution
function Implicit_Level
(Level : Embedding_Level; T : BC_Value) return Embedding_Level
is (if Level mod 2 = 0 and Level <= Max_Depth then I1_Level (Level, T)
elsif Level mod 2 = 1 and Level <= Max_Depth then I2_Level (Level, T)
else Level);
---------------------------------------------------------------------------
-- P2/P3 ghost specification: First strong character determination
--
-- UAX #9 P2: In each paragraph, find the first character of type L, AL,
-- or R while skipping over any characters between an isolate initiator
-- and its matching PDI or the end of the paragraph.
--
-- Ghost_First_Strong scans Types(Pos..Num) with an isolate nesting
-- counter, returning the BC_Value of the first strong type found at
-- isolate level 0, or BC_Default if none is found.
---------------------------------------------------------------------------
type Ghost_BC_Array is array (1 .. Max_Paragraph_CPs) of BC_Value;
type Ghost_Seq_Array is array (1 .. Max_Paragraph_CPs) of Natural;
---------------------------------------------------------------------------
-- N0 ghost: Bracket pair resolution specification
--
-- These ghost expression functions specify the N0a/N0b/N0c resolution
-- for a given bracket pair. The pair itself is identified by its
-- sequence indices (Open_S, Close_S). The functions scan Types between
-- the pair boundaries and compute the resolved direction.
--
-- Ghost_N0_Has_Embed_Dir: scan Seq(From..To) for a strong type matching
-- the embedding direction. (EN and AN count as R via Neutral_Type.)
--
-- Ghost_N0_Has_Opposite: scan Seq(From..To) for a strong type opposite
-- to the embedding direction.
--
-- Ghost_N0_Context_Dir: backward scan from S-1 for preceding strong
-- type (N0b context). Returns SOS if none found.
--
-- Ghost_N0_Pair_Dir: composed result — N0a/N0b/N0c for a given pair.
---------------------------------------------------------------------------
-- Scan From_S..To_S for a strong type matching Embed_Dir.
-- Recurses by shrinking To_S so that:
-- Has_Embed(From, S+1) = check(S+1) OR Has_Embed(From, S)
-- This matches forward loop accumulation.
function Ghost_N0_Has_Embed_Dir
(Types : Ghost_BC_Array;
Seq : Ghost_Seq_Array;
From_S : Natural;
To_S : Natural;
Embed_Dir : BC_Value) return Boolean
is (if From_S > To_S then False
elsif Seq (To_S) >= 1
and then Seq (To_S) <= Max_Paragraph_CPs
and then Neutral_Type (Types (Seq (To_S))) = Embed_Dir then
True
else Ghost_N0_Has_Embed_Dir (Types, Seq, From_S, To_S - 1, Embed_Dir))
with Ghost,
Pre => From_S >= 1
and then To_S <= Max_Paragraph_CPs,
Subprogram_Variant => (Decreases => To_S);
-- Scan From_S..To_S for a strong type opposite to Embed_Dir.
-- Same backward-recursion structure as Ghost_N0_Has_Embed_Dir.
function Ghost_N0_Has_Opposite
(Types : Ghost_BC_Array;
Seq : Ghost_Seq_Array;
From_S : Natural;
To_S : Natural;
Embed_Dir : BC_Value) return Boolean
is (if From_S > To_S then False
elsif Seq (To_S) >= 1
and then Seq (To_S) <= Max_Paragraph_CPs
and then Neutral_Type (Types (Seq (To_S))) /= BC_ON
and then Neutral_Type (Types (Seq (To_S))) /= Embed_Dir then
True
else Ghost_N0_Has_Opposite (Types, Seq, From_S, To_S - 1, Embed_Dir))
with Ghost,
Pre => From_S >= 1
and then To_S <= Max_Paragraph_CPs,
Subprogram_Variant => (Decreases => To_S);
-- Backward scan from S-1 for preceding strong type (N0b context).
-- Returns Neutral_Type of the first strong (L or R) found, or SOS.
function Ghost_N0_Context_Dir
(Types : Ghost_BC_Array;
Seq : Ghost_Seq_Array;
S : Natural;
SOS : BC_Value) return BC_Value
is (if S <= 1 then SOS
elsif Seq (S - 1) < 1
or else Seq (S - 1) > Max_Paragraph_CPs then
Ghost_N0_Context_Dir (Types, Seq, S - 1, SOS)
elsif Neutral_Type (Types (Seq (S - 1))) = BC_L
or else Neutral_Type (Types (Seq (S - 1))) = BC_R then
Neutral_Type (Types (Seq (S - 1)))
else Ghost_N0_Context_Dir (Types, Seq, S - 1, SOS))
with Ghost,
Pre => S <= Max_Paragraph_CPs + 1,
Subprogram_Variant => (Decreases => S);
-- Composed N0 result for a bracket pair at (Open_S, Close_S).
-- Returns BC_L or BC_R if N0a or N0b applies, BC_Default for N0c.
function Ghost_N0_Pair_Dir
(Types : Ghost_BC_Array;
Seq : Ghost_Seq_Array;
Open_S : Natural;
Close_S : Natural;
Embed_Dir : BC_Value;
SOS : BC_Value) return BC_Value
is (if Ghost_N0_Has_Embed_Dir
(Types, Seq, Open_S + 1, Close_S - 1, Embed_Dir)
then Embed_Dir
elsif Ghost_N0_Has_Opposite
(Types, Seq, Open_S + 1, Close_S - 1, Embed_Dir)
then N0b_Resolved (Embed_Dir,
Ghost_N0_Context_Dir (Types, Seq, Open_S, SOS))
else BC_Default)
with Ghost,
Pre => Open_S >= 1
and then Close_S >= 2
and then Close_S <= Max_Paragraph_CPs
and then Open_S < Close_S;
---------------------------------------------------------------------------
-- W2 ghost: Accumulated previous strong type
--
-- Scans Seq(1..S-1), tracking the most recent strong type (L, R, AL).
-- Returns the Prev_Strong that Apply_W2 would have at position S.
---------------------------------------------------------------------------
function Ghost_W2_Prev_Strong
(Types : Ghost_BC_Array;
Seq : Ghost_Seq_Array;
S : Natural;
SOS : BC_Value) return BC_Value
is (if S <= 1 then
SOS
elsif Seq (S - 1) < 1 or else Seq (S - 1) > Max_Paragraph_CPs then
Ghost_W2_Prev_Strong (Types, Seq, S - 1, SOS)
elsif Is_Strong (Types (Seq (S - 1))) then
Types (Seq (S - 1))
else
Ghost_W2_Prev_Strong (Types, Seq, S - 1, SOS))
with Ghost,
Pre => S <= Max_Paragraph_CPs + 1,
Subprogram_Variant => (Decreases => S);
---------------------------------------------------------------------------
-- W4 ghost: Forward-recursive effective type after W4 processing
--
-- W4 processes positions 2..Len-1 left-to-right. At position S, the
-- effective Prev is the W4 result at S-1 (already processed), while
-- Next is the original type at S+1 (not yet processed).
--
-- Ghost_W4_Result(Types, Seq, S, Len) gives the type at position S
-- after W4 has processed positions 2..S.
---------------------------------------------------------------------------
function Ghost_W4_Result
(Types : Ghost_BC_Array;
Seq : Ghost_Seq_Array;
S : Natural;
Len : Natural) return BC_Value
is (if S < 2 or else S > Len - 1
or else Seq (S) < 1 or else Seq (S) > Max_Paragraph_CPs
then
-- Not processed by W4: return original type
(if Seq (S) >= 1 and then Seq (S) <= Max_Paragraph_CPs
then Types (Seq (S))
else BC_Default)
elsif Seq (S - 1) < 1 or else Seq (S - 1) > Max_Paragraph_CPs
or else Seq (S + 1) < 1 or else Seq (S + 1) > Max_Paragraph_CPs
then
-- Neighbors out of range: W4 doesn't fire
Types (Seq (S))
else
W4_Resolved
(Types (Seq (S)),
Ghost_W4_Result (Types, Seq, S - 1, Len),
Types (Seq (S + 1))))
with Ghost,
Pre => S >= 1 and then S <= Max_Paragraph_CPs
and then Len <= Max_Paragraph_CPs,
Subprogram_Variant => (Decreases => S);
---------------------------------------------------------------------------
-- W5 ghost: ET adjacent to EN through chain of ET
--
-- W5 changes ET→EN when there's an EN reachable leftward or rightward
-- through a contiguous chain of ET types in the sequence.
--
-- Ghost_W5_Has_EN_Left(Types, Seq, S): scans leftward from S through
-- positions with BC_ET until finding BC_EN (True) or non-ET/EN (False).
-- Ghost_W5_Has_EN_Right(Types, Seq, S, Len): same, scanning rightward.
-- Ghost_W5_Result: the effective type at position S after W5.
---------------------------------------------------------------------------
function Ghost_W5_Has_EN_Left
(Types : Ghost_BC_Array;
Seq : Ghost_Seq_Array;
S : Natural) return Boolean
is (if S < 1 then False
elsif Seq (S) < 1 or else Seq (S) > Max_Paragraph_CPs then False
elsif Types (Seq (S)) = BC_EN then True
elsif Types (Seq (S)) /= BC_ET then False
else Ghost_W5_Has_EN_Left (Types, Seq, S - 1))
with Ghost,
Pre => S <= Max_Paragraph_CPs,
Subprogram_Variant => (Decreases => S);
function Ghost_W5_Has_EN_Right
(Types : Ghost_BC_Array;
Seq : Ghost_Seq_Array;
S : Natural;
Len : Natural) return Boolean
is (if S < 1 or else S > Len then False
elsif Seq (S) < 1 or else Seq (S) > Max_Paragraph_CPs then False
elsif Types (Seq (S)) = BC_EN then True
elsif Types (Seq (S)) /= BC_ET then False
else Ghost_W5_Has_EN_Right (Types, Seq, S + 1, Len))
with Ghost,
Pre => Len <= Max_Paragraph_CPs
and then S <= Max_Paragraph_CPs + 1,
Subprogram_Variant => (Decreases => Len - S + 1);
-- Forward-pass-only result: ET→EN if Has_EN_Left, else original.
function Ghost_W5_Fwd_Result
(Types : Ghost_BC_Array;
Seq : Ghost_Seq_Array;
S : Natural) return BC_Value
is (if S < 1 or else Seq (S) < 1 or else Seq (S) > Max_Paragraph_CPs
then BC_Default
elsif Types (Seq (S)) = BC_ET
and then Ghost_W5_Has_EN_Left (Types, Seq, S)
then BC_EN
else Types (Seq (S)))
with Ghost,
Pre => S <= Max_Paragraph_CPs;
-- Backward-pass Has_Adjacent_EN: scans right in the post-forward state.
-- ET positions remain ET only when Has_EN_Left = False, so this function
-- sees Fwd_Result = ET for those. EN positions (original or converted by
-- forward pass) appear as BC_EN.
function Ghost_W5_Bwd_Has_EN
(Types : Ghost_BC_Array;
Seq : Ghost_Seq_Array;
S : Natural;
Len : Natural) return Boolean
is (if S < 1 or else S > Len then False
elsif Seq (S) < 1 or else Seq (S) > Max_Paragraph_CPs then False
elsif Ghost_W5_Fwd_Result (Types, Seq, S) = BC_EN then True
elsif Ghost_W5_Fwd_Result (Types, Seq, S) = BC_ET then
Ghost_W5_Bwd_Has_EN (Types, Seq, S + 1, Len)
else False)
with Ghost,
Pre => Len <= Max_Paragraph_CPs
and then S <= Max_Paragraph_CPs + 1,
Subprogram_Variant => (Decreases => Len - S + 1);
-- Combined two-pass result
function Ghost_W5_Result
(Types : Ghost_BC_Array;
Seq : Ghost_Seq_Array;
S : Natural;
Len : Natural) return BC_Value
is (if S < 1 or else S > Len
or else Seq (S) < 1 or else Seq (S) > Max_Paragraph_CPs
then BC_Default
elsif Types (Seq (S)) = BC_ET
and then (Ghost_W5_Has_EN_Left (Types, Seq, S)
or else Ghost_W5_Has_EN_Right (Types, Seq, S, Len))
then BC_EN
else Types (Seq (S)))
with Ghost,
Pre => S <= Max_Paragraph_CPs
and then Len <= Max_Paragraph_CPs;
---------------------------------------------------------------------------
-- W7 ghost: helpers and accumulated previous strong type
--
-- W7 tracks only L and R (not AL, since W3 has already converted AL→R).
-- This models the ACTUAL W7 pass: it applies W7 (EN→L when PS=L) at
-- each position, and the changed type feeds into Prev_Strong tracking.
---------------------------------------------------------------------------
-- Effective type at a position after W7: if original is EN and PS = L,
-- the type becomes L. Otherwise unchanged.
function W7_Effective_Type
(T_Orig : BC_Value; PS : BC_Value) return BC_Value
is (if T_Orig = BC_EN and then PS = BC_L then BC_L else T_Orig);
-- Update Prev_Strong after seeing an effective type:
-- If the effective type is L or R, Prev_Strong becomes that type.
-- Otherwise Prev_Strong is unchanged.
function W7_PS_Update
(T_After : BC_Value; PS : BC_Value) return BC_Value
is (if T_After = BC_L or T_After = BC_R then T_After else PS);
-- Accumulated Prev_Strong before position S in the W7 pass.
-- Recursive: processes positions 1..S-1, applying W7 at each step.
function Ghost_W7_Prev_Strong
(Types : Ghost_BC_Array;
Seq : Ghost_Seq_Array;
S : Natural;
SOS : BC_Value) return BC_Value
is (if S <= 1 then
SOS
elsif Seq (S - 1) < 1 or else Seq (S - 1) > Max_Paragraph_CPs then
Ghost_W7_Prev_Strong (Types, Seq, S - 1, SOS)
else
W7_PS_Update
(W7_Effective_Type
(Types (Seq (S - 1)),
Ghost_W7_Prev_Strong (Types, Seq, S - 1, SOS)),
Ghost_W7_Prev_Strong (Types, Seq, S - 1, SOS)))
with Ghost,
Pre => S <= Max_Paragraph_CPs + 1,
Subprogram_Variant => (Decreases => S);
---------------------------------------------------------------------------
-- W1 ghost: Accumulated previous type for NSM resolution
--
-- W1 changes NSM to the type of the preceding character, or to ON
-- if at the start of the run or after an isolate initiator/PDI.
-- The "previous type" is the result of W1 applied to the preceding
-- position, which makes this mutually recursive with the W1 result.
--
-- We model this as: Ghost_W1_Result gives the result type at position S,
-- and Ghost_W1_Prev is the previous type seen before position S.
---------------------------------------------------------------------------
function Ghost_W1_Prev
(Types : Ghost_BC_Array;
Seq : Ghost_Seq_Array;
S : Natural;
SOS : BC_Value) return BC_Value
is (if S <= 1 then
SOS
elsif Seq (S - 1) < 1 or else Seq (S - 1) > Max_Paragraph_CPs then
Ghost_W1_Prev (Types, Seq, S - 1, SOS)
else
W1_Resolved (Types (Seq (S - 1)),
Ghost_W1_Prev (Types, Seq, S - 1, SOS),
S - 1 = 1))
with Ghost,
Pre => S <= Max_Paragraph_CPs + 1,
Subprogram_Variant => (Decreases => S);
---------------------------------------------------------------------------
-- P2/P3 ghost specification: First strong character determination
---------------------------------------------------------------------------
function Ghost_First_Strong
(Types : Ghost_BC_Array;
Num : Natural;
Pos : Natural;
Iso_Count : Natural) return BC_Value
is (if Pos < 1 or else Pos > Num then
BC_Default
elsif Is_Isolate_Initiator (Types (Pos)) then
Ghost_First_Strong (Types, Num, Pos + 1,
(if Iso_Count < Max_Paragraph_CPs
then Iso_Count + 1 else Iso_Count))
elsif Types (Pos) = BC_PDI then
Ghost_First_Strong (Types, Num, Pos + 1,
(if Iso_Count > 0 then Iso_Count - 1 else 0))
elsif Iso_Count = 0 and then Is_Strong (Types (Pos)) then
Types (Pos)
else
Ghost_First_Strong (Types, Num, Pos + 1, Iso_Count))
with Ghost,
Pre => Num <= Max_Paragraph_CPs
and then Iso_Count <= Max_Paragraph_CPs,
Subprogram_Variant => (Decreases => Num - Pos + 1);
-- Top-level wrapper: scan from position 1 with zero isolate nesting
function Ghost_First_Strong_All
(Types : Ghost_BC_Array;
Num : Natural) return BC_Value
is (Ghost_First_Strong (Types, Num, 1, 0))
with Ghost,
Pre => Num <= Max_Paragraph_CPs;
---------------------------------------------------------------------------
-- N1/N2 ghost specification: neutral type resolution
--
-- Ghost_N_Leading scans backward from S-1 to find the first strong type
-- (Neutral_Type returns L or R). Returns SOS if none found.
--
-- Ghost_N_Trailing scans forward from S+1 to find the first strong type.
-- Returns EOS if none found.
--
-- Ghost_N_Result gives the resolved type at position S.
---------------------------------------------------------------------------
function Ghost_N_Leading
(Types : Ghost_BC_Array;
Seq : Ghost_Seq_Array;
S : Natural;
SOS : BC_Value) return BC_Value
is (if S <= 1 then
SOS
elsif Seq (S - 1) < 1 or else Seq (S - 1) > Max_Paragraph_CPs then
Ghost_N_Leading (Types, Seq, S - 1, SOS)
elsif Neutral_Type (Types (Seq (S - 1))) = BC_L
or else Neutral_Type (Types (Seq (S - 1))) = BC_R
then
Neutral_Type (Types (Seq (S - 1)))
else
Ghost_N_Leading (Types, Seq, S - 1, SOS))
with Ghost,
Pre => S <= Max_Paragraph_CPs + 1,
Subprogram_Variant => (Decreases => S);
function Ghost_N_Trailing
(Types : Ghost_BC_Array;
Seq : Ghost_Seq_Array;
S : Natural;
Len : Natural;
EOS : BC_Value) return BC_Value
is (if S >= Len then
EOS
elsif Seq (S + 1) < 1 or else Seq (S + 1) > Max_Paragraph_CPs then
Ghost_N_Trailing (Types, Seq, S + 1, Len, EOS)
elsif Neutral_Type (Types (Seq (S + 1))) = BC_L
or else Neutral_Type (Types (Seq (S + 1))) = BC_R
then
Neutral_Type (Types (Seq (S + 1)))
else
Ghost_N_Trailing (Types, Seq, S + 1, Len, EOS))
with Ghost,
Pre => Len <= Max_Paragraph_CPs
and then S <= Max_Paragraph_CPs,
Subprogram_Variant => (Decreases => Len - S);
-- Combined N1/N2 result at position S
function Ghost_N_Result
(Types : Ghost_BC_Array;
Seq : Ghost_Seq_Array;
S : Natural;
Len : Natural;
SOS : BC_Value;
EOS : BC_Value;
Level : Embedding_Level) return BC_Value
is (if S < 1 or else S > Len
or else Seq (S) < 1 or else Seq (S) > Max_Paragraph_CPs
then BC_Default
elsif not Is_NI (Types (Seq (S)))
then Types (Seq (S)) -- not NI → unchanged
elsif N1_Applies (Types (Seq (S)),
Ghost_N_Leading (Types, Seq, S, SOS),
Ghost_N_Trailing (Types, Seq, S, Len, EOS))
then N1_Resolved (Ghost_N_Leading (Types, Seq, S, SOS))
else N2_Resolved (Types (Seq (S)), Level))
with Ghost,
Pre => S <= Max_Paragraph_CPs
and then Len <= Max_Paragraph_CPs;
---------------------------------------------------------------------------
-- L1 ghost specification: trailing whitespace/isolate level reset
--
-- Ghost_L1_Should_Reset(Types, I, Num) returns True when position I
-- should have its level reset to the paragraph level. This is the case
-- when:
-- (a) Orig_Types(I) is S or B (always reset), OR
-- (b) Is_L1_Reset_Type(Orig_Types(I)) and all non-X9-removed positions
-- from I+1 to the next non-L1-reset-type (or end of paragraph)
-- are L1 reset types, S, or B.
--
-- Equivalently: scan forward from I+1, skipping X9-removed. If the
-- first non-X9-removed, non-L1-reset-type position is S or B (or end),
-- return True. Otherwise False.
--
-- Ghost_L1_Reset_After scans from position Pos forward and captures
-- the state of the Reset flag after processing position Pos..Num in
-- the backward pass (i.e., whether position Pos-1 would see Reset=True).
---------------------------------------------------------------------------
-- Does the backward scan have Reset=True at position I?
-- That is, should a L1-reset-type character at position I be reset?
--
-- Scan forward from I+1: skip X9-removed; if next non-X9 is S/B, True.
-- If next non-X9 is another L1 reset type, recurse. If other, False.
-- If past end, True (end of paragraph ≡ paragraph separator).
function Ghost_L1_Trailing
(Types : Ghost_BC_Array;
I : Natural;
Num : Natural) return Boolean
is (if I >= Num then
True -- at or past end of paragraph
elsif Is_X9_Removed (Types (I + 1)) then
Ghost_L1_Trailing (Types, I + 1, Num)
elsif Types (I + 1) = BC_S or Types (I + 1) = BC_B then
True
elsif Is_L1_Reset_Type (Types (I + 1)) then
Ghost_L1_Trailing (Types, I + 1, Num)
else
False)
with Ghost,
Pre => Num <= Max_Paragraph_CPs
and then I >= 1
and then I <= Num,
Subprogram_Variant => (Decreases => Num - I);
-- Overall L1 result for position I: should the level be reset to PL?
function Ghost_L1_Should_Reset
(Types : Ghost_BC_Array;
I : Natural;
Num : Natural) return Boolean
is (if Is_X9_Removed (Types (I)) then
False -- X9-removed positions are skipped
elsif Types (I) = BC_S or Types (I) = BC_B then
True -- S and B are always reset
elsif Is_L1_Reset_Type (Types (I)) then
Ghost_L1_Trailing (Types, I, Num)
else
False)
with Ghost,
Pre => Num <= Max_Paragraph_CPs
and then I >= 1
and then I <= Num;
end Lingenic_Text.Bidi_Spec;