-- 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 — Line Break body
--
-- Forward state machine for line break detection (UAX #14, Unicode 17.0).
--
-- Decodes UTF-8, looks up resolved LBP properties, maintains state for:
-- LB9/LB10 (CM/ZWJ absorption)
-- SP* indirect breaks (LB8, LB14, LB15a, LB16, LB17)
-- RI pairing (LB30a)
-- Three-character lookbehind (LB21a, LB28a sub-rule 3)
-- Forward lookahead (LB15b, LB15c, LB19a, LB25 PO/PR×OP, LB28a sub-rule 4)
-- NU context tracking (LB25)
-- East Asian Width tracking (LB19a)
--
-- Invalid UTF-8 bytes are treated as single-byte codepoints with
-- LBP = AL (the default resolution for XX).
--
-- SPARK Platinum: the loop invariant connects runtime state to the
-- recursive ghost function Next_LB, establishing that the returned
-- position equals Next_LB_From(Text, Pos).
-------------------------------------------------------------------------------
with Lingenic_Text.UCD_Parser;
with Lingenic_Text.UTF8;
package body Lingenic_Text.Line_Break
with SPARK_Mode
is
---------------------------------------------------------------------------
-- Is_EAW_East_Asian — check if a codepoint has East Asian Width F/W/H
--
-- Expression function so the solver can unfold it and connect to
-- Ghost_Is_EA which uses the same EAW_To_Abstract(Get_EAW(CP)) path.
---------------------------------------------------------------------------
function Is_EAW_East_Asian (CP : Codepoint) return Boolean
is (declare
Val : constant EAW_Spec.EAW_Value :=
Properties.EAW_To_Abstract (Properties.Get_EAW (CP));
begin
Val = EAW_Spec.EAW_Fullwidth
or Val = EAW_Spec.EAW_Wide
or Val = EAW_Spec.EAW_Halfwidth)
with Pre => Properties.Initialized;
---------------------------------------------------------------------------
-- Scan_LB15b — forward lookahead for LB15b
---------------------------------------------------------------------------
procedure Scan_LB15b
(Text : Byte_Array;
From : Positive;
Applies : out Boolean)
with Pre => Text'First = 1
and then Text'Last >= 1
and then Text'Last < Positive'Last
and then From <= Text'Last + 1
and then Properties.Initialized,
Post => Applies = Ghost_LB15b (Text, From)
is
use Line_Break_Spec;
Scan : Positive := From;
begin
-- If From is past end of text → eot → LB15b applies
if From > Text'Last then
Applies := True;
return;
end if;
while Scan in Text'Range loop
pragma Loop_Invariant (Scan >= From);
pragma Loop_Invariant (Scan <= Text'Last);
pragma Loop_Invariant
(Ghost_LB15b (Text, Scan) = Ghost_LB15b (Text, From));
pragma Loop_Variant (Increases => Scan);
declare
Scan_CP : Codepoint;
Scan_Len : Positive;
Scan_Valid : Boolean;
Scan_LBP : LBP_Value;
begin
UTF8.Decode (Text, Scan, Scan_CP, Scan_Len, Scan_Valid);
pragma Assert (Scan_Len = Ghost_Step_Length (Text, Scan));
if Scan_Valid then
Scan_LBP := Properties.Get_LBP (Scan_CP);
else
Scan_LBP := LBP_AL;
end if;
pragma Assert (Scan_Valid = UTF8_Spec.Well_Formed_At (Text, Scan));
pragma Assert (Scan_CP = Ghost_CP (Text, Scan));
pragma Assert (Scan_LBP = Ghost_LBP (Text, Scan));
-- LB9: skip CM/ZWJ to find the effective next character
if Is_CM_ZWJ (Scan_LBP) then
-- Advance past this CM/ZWJ
if Scan > Text'Last - Scan_Len + 1 then
-- Reached end of text — eot counts as right context
Applies := True;
return;
end if;
Scan := Scan + Scan_Len;
else
-- Found effective next character — check right context
Applies := Is_LB15b_After (Scan_LBP);
return;
end if;
end;
end loop;
-- Reached end of text → eot → LB15b applies
Applies := True;
end Scan_LB15b;
---------------------------------------------------------------------------
-- Scan_LB15c — forward lookahead for LB15c
---------------------------------------------------------------------------
procedure Scan_LB15c
(Text : Byte_Array;
From : Positive;
Found : out Boolean)
with Pre => Text'First = 1
and then Text'Last >= 1
and then Text'Last < Positive'Last
and then From <= Text'Last + 1
and then Properties.Initialized,
Post => Found = Ghost_LB15c (Text, From)
is
use Line_Break_Spec;
Scan : Positive := From;
begin
Found := False;
if From > Text'Last then
return;
end if;
while Scan in Text'Range loop
pragma Loop_Invariant (Scan >= From);
pragma Loop_Invariant (Scan <= Text'Last);
pragma Loop_Invariant
(Ghost_LB15c (Text, Scan) = Ghost_LB15c (Text, From));
pragma Loop_Variant (Increases => Scan);
declare
Scan_CP : Codepoint;
Scan_Len : Positive;
Scan_Valid : Boolean;
Scan_LBP : LBP_Value;
begin
UTF8.Decode (Text, Scan, Scan_CP, Scan_Len, Scan_Valid);
pragma Assert (Scan_Len = Ghost_Step_Length (Text, Scan));
if Scan_Valid then
Scan_LBP := Properties.Get_LBP (Scan_CP);
else
Scan_LBP := LBP_AL;
end if;
pragma Assert (Scan_Valid = UTF8_Spec.Well_Formed_At (Text, Scan));
pragma Assert (Scan_CP = Ghost_CP (Text, Scan));
pragma Assert (Scan_LBP = Ghost_LBP (Text, Scan));
-- LB9: skip CM/ZWJ to find the effective next character
if Is_CM_ZWJ (Scan_LBP) then
if Scan > Text'Last - Scan_Len + 1 then
return;
end if;
Scan := Scan + Scan_Len;
else
Found := (Scan_LBP = LBP_NU);
return;
end if;
end;
end loop;
end Scan_LB15c;
---------------------------------------------------------------------------
-- Scan_LB19a — forward lookahead for LB19a right context
---------------------------------------------------------------------------
procedure Scan_LB19a_Non_EA
(Text : Byte_Array;
From : Positive;
Found : out Boolean)
with Pre => Text'First = 1
and then Text'Last >= 1
and then Text'Last < Positive'Last
and then From <= Text'Last + 1
and then Properties.Initialized,
Post => Found = Ghost_LB19a_Non_EA (Text, From)
is
use Line_Break_Spec;
Scan : Positive := From;
begin
Found := True;
-- eot counts as non-EA
if From > Text'Last then
return;
end if;
while Scan in Text'Range loop
pragma Loop_Invariant (Scan >= From);
pragma Loop_Invariant (Scan <= Text'Last);
pragma Loop_Invariant
(Ghost_LB19a_Non_EA (Text, Scan) =
Ghost_LB19a_Non_EA (Text, From));
pragma Loop_Variant (Increases => Scan);
declare
Scan_CP : Codepoint;
Scan_Len : Positive;
Scan_Valid : Boolean;
Scan_LBP : LBP_Value;
begin
UTF8.Decode (Text, Scan, Scan_CP, Scan_Len, Scan_Valid);
pragma Assert (Scan_Len = Ghost_Step_Length (Text, Scan));
if Scan_Valid then
Scan_LBP := Properties.Get_LBP (Scan_CP);
else
Scan_LBP := LBP_AL;
end if;
pragma Assert (Scan_Valid = UTF8_Spec.Well_Formed_At (Text, Scan));
pragma Assert (Scan_CP = Ghost_CP (Text, Scan));
pragma Assert (Scan_LBP = Ghost_LBP (Text, Scan));
-- LB9: skip CM/ZWJ to find the effective next character
if Is_CM_ZWJ (Scan_LBP) then
if Scan > Text'Last - Scan_Len + 1 then
-- eot counts as non-EA
Found := True;
return;
end if;
Scan := Scan + Scan_Len;
else
-- Found effective next character — check if non-EA
if Scan_Valid then
Found := not Is_EAW_East_Asian (Scan_CP);
-- Platinum: connect runtime EA check to ghost
pragma Assert (Ghost_Is_EA (Text, Scan) = not Found);
else
Found := True; -- invalid → non-EA
end if;
return;
end if;
end;
end loop;
-- eot counts as non-EA
Found := True;
end Scan_LB19a_Non_EA;
---------------------------------------------------------------------------
-- Scan_LB25_OP_NU — forward lookahead for LB25 PO/PR × OP rules
---------------------------------------------------------------------------
procedure Scan_LB25_OP_NU
(Text : Byte_Array;
From : Positive;
Found : out Boolean)
with Pre => Text'First = 1
and then Text'Last >= 1
and then Text'Last < Positive'Last
and then From <= Text'Last + 1
and then Properties.Initialized,
Post => Found = Ghost_LB25_OP_NU (Text, From)
is
use Line_Break_Spec;
Scan : Positive := From;
begin
Found := False;
if From > Text'Last then
return;
end if;
-- First non-CM/ZWJ character should be NU or IS
while Scan in Text'Range loop
pragma Loop_Invariant (Scan >= From);
pragma Loop_Invariant (Scan <= Text'Last);
pragma Loop_Invariant
(Ghost_LB25_OP_NU (Text, Scan) = Ghost_LB25_OP_NU (Text, From));
pragma Loop_Variant (Increases => Scan);
declare
Scan_CP : Codepoint;
Scan_Len : Positive;
Scan_Valid : Boolean;
Scan_LBP : LBP_Value;
begin
UTF8.Decode (Text, Scan, Scan_CP, Scan_Len, Scan_Valid);
pragma Assert (Scan_Len = Ghost_Step_Length (Text, Scan));
if Scan_Valid then
Scan_LBP := Properties.Get_LBP (Scan_CP);
else
Scan_LBP := LBP_AL;
end if;
pragma Assert (Scan_Valid = UTF8_Spec.Well_Formed_At (Text, Scan));
pragma Assert (Scan_CP = Ghost_CP (Text, Scan));
pragma Assert (Scan_LBP = Ghost_LBP (Text, Scan));
-- LB9: skip CM/ZWJ
if Is_CM_ZWJ (Scan_LBP) then
if Scan > Text'Last - Scan_Len + 1 then
return;
end if;
Scan := Scan + Scan_Len;
elsif Scan_LBP = LBP_NU then
-- PO/PR × OP NU or PO/PR × OP (CM|ZWJ)* NU
Found := True;
return;
elsif Scan_LBP = LBP_IS then
-- Might be PO/PR × OP IS NU — need to check for NU after IS
-- Skip past IS and its CM/ZWJ, then check for NU
if Scan > Text'Last - Scan_Len + 1 then
return;
end if;
Scan := Scan + Scan_Len;
-- Now look for NU past CM/ZWJ — this is Ghost_LB25_Inner_NU
while Scan in Text'Range loop
pragma Loop_Invariant (Scan >= From);
pragma Loop_Invariant (Scan <= Text'Last);
pragma Loop_Invariant
(Ghost_LB25_Inner_NU (Text, Scan) =
Ghost_LB25_OP_NU (Text, From));
pragma Loop_Variant (Increases => Scan);
declare
S2_CP : Codepoint;
S2_Len : Positive;
S2_Valid : Boolean;
S2_LBP : LBP_Value;
begin
UTF8.Decode (Text, Scan, S2_CP, S2_Len, S2_Valid);
pragma Assert (S2_Len = Ghost_Step_Length (Text, Scan));
if S2_Valid then
S2_LBP := Properties.Get_LBP (S2_CP);
else
S2_LBP := LBP_AL;
end if;
pragma Assert
(S2_Valid = UTF8_Spec.Well_Formed_At (Text, Scan));
pragma Assert (S2_CP = Ghost_CP (Text, Scan));
pragma Assert (S2_LBP = Ghost_LBP (Text, Scan));
if Is_CM_ZWJ (S2_LBP) then
if Scan > Text'Last - S2_Len + 1 then
return;
end if;
Scan := Scan + S2_Len;
else
Found := (S2_LBP = LBP_NU);
return;
end if;
end;
end loop;
return;
else
-- Neither NU nor IS nor CM/ZWJ — doesn't match
return;
end if;
end;
end loop;
end Scan_LB25_OP_NU;
---------------------------------------------------------------------------
-- Scan_LB28a_VF — forward lookahead for LB28a sub-rule 4
---------------------------------------------------------------------------
procedure Scan_LB28a_VF
(Text : Byte_Array;
From : Positive;
Found : out Boolean)
with Pre => Text'First = 1
and then Text'Last >= 1
and then Text'Last < Positive'Last
and then From <= Text'Last + 1
and then Properties.Initialized,
Post => Found = Ghost_LB28a_VF (Text, From)
is
use Line_Break_Spec;
Scan : Positive := From;
begin
Found := False;
if From > Text'Last then
return;
end if;
while Scan in Text'Range loop
pragma Loop_Invariant (Scan >= From);
pragma Loop_Invariant (Scan <= Text'Last);
pragma Loop_Invariant
(Ghost_LB28a_VF (Text, Scan) = Ghost_LB28a_VF (Text, From));
pragma Loop_Variant (Increases => Scan);
declare
Scan_CP : Codepoint;
Scan_Len : Positive;
Scan_Valid : Boolean;
Scan_LBP : LBP_Value;
begin
UTF8.Decode (Text, Scan, Scan_CP, Scan_Len, Scan_Valid);
pragma Assert (Scan_Len = Ghost_Step_Length (Text, Scan));
if Scan_Valid then
Scan_LBP := Properties.Get_LBP (Scan_CP);
else
Scan_LBP := LBP_AL;
end if;
pragma Assert (Scan_Valid = UTF8_Spec.Well_Formed_At (Text, Scan));
pragma Assert (Scan_CP = Ghost_CP (Text, Scan));
pragma Assert (Scan_LBP = Ghost_LBP (Text, Scan));
-- LB9: skip CM/ZWJ to find the effective next character
if Is_CM_ZWJ (Scan_LBP) then
if Scan > Text'Last - Scan_Len + 1 then
return;
end if;
Scan := Scan + Scan_Len;
else
Found := (Scan_LBP = LBP_VF);
return;
end if;
end;
end loop;
end Scan_LB28a_VF;
---------------------------------------------------------------------------
-- Next_Line_Break
---------------------------------------------------------------------------
procedure Next_Line_Break
(Text : Byte_Array;
Pos : Positive;
Next_Pos : out Positive)
is
use Line_Break_Spec;
-- First codepoint (LB2: sot × — never break at start)
First_CP : Codepoint;
First_Len : Positive;
First_Valid : Boolean;
First_LBP : LBP_Value;
-- State variables
Prev_Eff : LBP_Value; -- Effective previous (LB9-adjusted)
Prev_Actual : LBP_Value; -- Literal previous char
Before_Prev_Eff : LBP_Value; -- Two effective chars back (LB21a, LB28a)
Before_SP : LBP_Value; -- Character before current SP run
In_SP_Run : Boolean; -- Currently in SP sequence
RI_Count : Natural; -- Consecutive RI count for LB30a
QU_Pi_Context : Boolean; -- LB15a: QU_Pi after valid context
Prev_ExtPict_Cn : Boolean; -- LB30b: prev is ExtPict AND GC=Cn
Prev_Is_DC : Boolean; -- LB28a: prev eff is U+25CC
Before_Prev_DC : Boolean; -- LB28a: two eff chars back is U+25CC
In_NU_Context : Boolean; -- LB25: in NU (SY|IS)* sequence
Prev_Is_EA : Boolean; -- LB19a: prev char has EAW F/W/H
Before_Prev_EA : Boolean; -- LB19a: two chars back has EAW F/W/H
-- Current position in text
Cur : Positive;
begin
-- Decode first codepoint (LB2: sot × — don't break here)
UTF8.Decode (Text, Pos, First_CP, First_Len, First_Valid);
-- Platinum: First_Len = Ghost_Step_Length (Text, Pos)
pragma Assert (First_Len = Ghost_Step_Length (Text, Pos));
-- Advance past first codepoint
if Pos > Text'Last - First_Len + 1 then
-- First codepoint reaches end of text (LB3: ! eot)
Next_Pos := Pos + First_Len;
pragma Assert (Next_Pos = Next_LB_From (Text, Pos));
return;
end if;
Cur := Pos + First_Len;
pragma Assert (Cur > Pos);
pragma Assert (Cur = Pos + Ghost_Step_Length (Text, Pos));
-- Look up property of first codepoint
if First_Valid then
First_LBP := Properties.Get_LBP (First_CP);
else
First_LBP := LBP_AL; -- Invalid UTF-8 → AL (LB1/LB10)
end if;
-- Platinum: connect runtime decoded CP to ghost
pragma Assert (First_Valid = UTF8_Spec.Well_Formed_At (Text, Pos));
pragma Assert (First_CP = Ghost_CP (Text, Pos));
pragma Assert (First_LBP = Ghost_LBP (Text, Pos));
-- Track whether LB10 applies (CM/ZWJ at sot → AL)
declare
First_Is_LB10 : constant Boolean := Is_CM_ZWJ (First_LBP);
First_Raw_LBP : constant LBP_Value := First_LBP;
First_Eff_LBP : LBP_Value;
begin
if First_Is_LB10 then
First_Eff_LBP := LBP_AL;
else
First_Eff_LBP := First_LBP;
end if;
-- Initialize state
Prev_Eff := First_Eff_LBP;
Prev_Actual := First_Raw_LBP;
Before_Prev_Eff := LBP_Other;
Before_SP := LBP_Other;
In_SP_Run := (First_Eff_LBP = LBP_SP);
QU_Pi_Context := False;
-- LB25: NU context tracking
In_NU_Context := (First_Eff_LBP = LBP_NU);
-- LB19a: East Asian Width tracking
if First_Is_LB10 or else (not First_Valid) then
Prev_Is_EA := False;
else
Prev_Is_EA := Is_EAW_East_Asian (First_CP);
end if;
-- LB19a: track Before_Prev EAW (sot → non-EA)
Before_Prev_EA := False;
-- LB28a: check if first char is U+25CC
Prev_Is_DC := (First_Valid and then First_CP = 16#25CC#);
Before_Prev_DC := False;
-- LB30b: check if first char is ExtPict and GC=Cn
-- When LB10 applies, ghost Initial_State sets this to False.
if First_Is_LB10 then
Prev_ExtPict_Cn := False;
elsif First_Valid
and then Properties.Get_ExtPict (First_CP)
then
declare
GC_Idx : constant UCD_Parser.Property_Index :=
Properties.Get_GC (First_CP);
begin
if GC_Idx >= 1
and then GC_Idx <= Properties.GC_Name_Count
and then Properties.GC_Name (GC_Idx) = "Cn"
then
Prev_ExtPict_Cn := True;
else
Prev_ExtPict_Cn := False;
end if;
end;
else
Prev_ExtPict_Cn := False;
end if;
-- LB15a: if first char is QU_Pi, sot is valid left context
if First_Eff_LBP = LBP_QU_Pi then
QU_Pi_Context := True;
end if;
-- Initialize RI counter
if First_Eff_LBP = LBP_RI then
RI_Count := 1;
else
RI_Count := 0;
end if;
-- Initialize SP tracking
if First_Eff_LBP = LBP_SP then
Before_SP := LBP_Other; -- sot before SP
In_SP_Run := True;
end if;
end;
-- Platinum: bridge for ExtPict_Cn.
-- When LB10, body sets False; ghost Initial_State also returns False.
-- When not LB10, body computes from Get_ExtPict/Get_GC;
-- ghost uses Ghost_ExtPict_Cn which calls same opaque functions.
-- At level 0 the solver can't always substitute through opaque state
-- functions, but at level 1+ it can.
-- Platinum: bridge for Is_EA
pragma Assert
(Prev_Is_EA =
(not Line_Break_Spec.Is_CM_ZWJ (Ghost_LBP (Text, Pos))
and then Ghost_Valid (Text, Pos)
and then Ghost_Is_EA (Text, Pos)));
-- Platinum: connect composite initial state to ghost Initial_State.
pragma Assert (Prev_Eff = Initial_State (Text, Pos).Prev_Eff);
pragma Assert (Prev_Actual = Initial_State (Text, Pos).Prev_Actual);
pragma Assert
(Before_Prev_Eff = Initial_State (Text, Pos).Before_Prev_Eff);
pragma Assert (Before_SP = Initial_State (Text, Pos).Before_SP);
pragma Assert (In_SP_Run = Initial_State (Text, Pos).In_SP_Run);
pragma Assert (RI_Count = Initial_State (Text, Pos).RI_Count);
pragma Assert
(QU_Pi_Context = Initial_State (Text, Pos).QU_Pi_Context);
pragma Assert
(Prev_ExtPict_Cn = Initial_State (Text, Pos).Prev_ExtPict_Cn);
pragma Assert (Prev_Is_DC = Initial_State (Text, Pos).Prev_Is_DC);
pragma Assert
(Before_Prev_DC = Initial_State (Text, Pos).Before_Prev_DC);
pragma Assert
(In_NU_Context = Initial_State (Text, Pos).In_NU_Context);
pragma Assert (Prev_Is_EA = Initial_State (Text, Pos).Prev_Is_EA);
pragma Assert
(Before_Prev_EA = Initial_State (Text, Pos).Before_Prev_EA);
-- Platinum: establish base case for the accumulator invariant.
pragma Assert
(Next_LB (Text, Cur,
LB_State'(Prev_Eff, Prev_Actual, Before_Prev_Eff,
Before_SP, In_SP_Run, RI_Count,
QU_Pi_Context, Prev_ExtPict_Cn,
Prev_Is_DC, Before_Prev_DC,
In_NU_Context, Prev_Is_EA, Before_Prev_EA))
= Next_LB_From (Text, Pos));
-- Scan forward through subsequent codepoints
while Cur in Text'Range loop
pragma Loop_Invariant (Cur > Pos);
pragma Loop_Invariant (Cur <= Text'Last);
-- Platinum accumulator invariant
pragma Loop_Invariant
(Next_LB (Text, Cur,
LB_State'(Prev_Eff, Prev_Actual, Before_Prev_Eff,
Before_SP, In_SP_Run, RI_Count,
QU_Pi_Context, Prev_ExtPict_Cn,
Prev_Is_DC, Before_Prev_DC,
In_NU_Context, Prev_Is_EA, Before_Prev_EA))
= Next_LB_From (Text, Pos));
pragma Loop_Variant (Increases => Cur);
declare
This_CP : Codepoint;
This_Len : Positive;
This_Valid : Boolean;
This_LBP : LBP_Value;
Eff_B : LBP_Value; -- Effective B (after LB9/LB10)
Is_Absorbed : Boolean; -- CM/ZWJ absorbed by LB9?
Allow_Break : Boolean;
-- LB15b lookahead result
LB15b_Result : Boolean;
-- LB15c lookahead result
LB15c_Result : Boolean;
-- LB19a lookahead result
LB19a_Result : Boolean;
-- LB25 PO/PR × OP lookahead result
LB25_OP_Result : Boolean;
-- LB28a sub-rule 4 lookahead result
LB28a_VF_Result : Boolean;
-- LB28a: is current character U+25CC?
This_Is_DC : Boolean;
-- LB19a: is current character East Asian?
This_Is_EA : Boolean;
-- Ghost: save state before updates for inductive step
Old_St : constant LB_State :=
LB_State'(Prev_Eff, Prev_Actual, Before_Prev_Eff,
Before_SP, In_SP_Run, RI_Count,
QU_Pi_Context, Prev_ExtPict_Cn,
Prev_Is_DC, Before_Prev_DC,
In_NU_Context, Prev_Is_EA, Before_Prev_EA)
with Ghost;
begin
-- Decode next codepoint
UTF8.Decode (Text, Cur, This_CP, This_Len, This_Valid);
-- Platinum: This_Len = Ghost_Step_Length (Text, Cur)
pragma Assert (This_Len = Ghost_Step_Length (Text, Cur));
-- Look up resolved LBP
if This_Valid then
This_LBP := Properties.Get_LBP (This_CP);
else
This_LBP := LBP_AL;
end if;
-- Platinum: connect runtime decoded CP to ghost
pragma Assert (This_Valid = UTF8_Spec.Well_Formed_At (Text, Cur));
pragma Assert (This_CP = Ghost_CP (Text, Cur));
pragma Assert (This_LBP = Ghost_LBP (Text, Cur));
-- LB28a: dotted circle check
This_Is_DC := (This_Valid and then This_CP = 16#25CC#);
-- Platinum: connect DC to ghost
pragma Assert (This_Is_DC = Ghost_Is_DC (Text, Cur));
-- LB19a: East Asian check
This_Is_EA := (This_Valid and then Is_EAW_East_Asian (This_CP));
-- Platinum: connect EA to ghost
pragma Assert
(if This_Valid then This_Is_EA = Ghost_Is_EA (Text, Cur)
else not This_Is_EA);
----------------------------------------------------------------
-- LB9: CM/ZWJ absorption
----------------------------------------------------------------
if Is_CM_ZWJ (This_LBP) then
if not Is_LB9_Exception (Prev_Eff) then
-- LB9: absorbed — no break, B takes A's class
Is_Absorbed := True;
Eff_B := Prev_Eff;
else
-- LB10: CM/ZWJ after LB9 exception → treat as AL
Is_Absorbed := False;
Eff_B := LBP_AL;
This_Is_EA := False;
end if;
else
Is_Absorbed := False;
Eff_B := This_LBP;
end if;
-- Platinum: connect absorption to ghost
pragma Assert (Is_Absorbed = Ghost_Is_Absorbed (Old_St, Text, Cur));
pragma Assert (Eff_B = Ghost_Eff_B (Old_St, Text, Cur));
pragma Assert (This_Is_EA = Ghost_This_EA (Old_St, Text, Cur));
----------------------------------------------------------------
-- If CM/ZWJ is absorbed by LB9, no break here.
----------------------------------------------------------------
if Is_Absorbed then
-- No break. CM/ZWJ is transparent.
Prev_Actual := This_LBP;
-- Platinum: connect to Updated_State_Absorbed
pragma Assert
(LB_State'(Prev_Eff, Prev_Actual, Before_Prev_Eff,
Before_SP, In_SP_Run, RI_Count,
QU_Pi_Context, Prev_ExtPict_Cn,
Prev_Is_DC, Before_Prev_DC,
In_NU_Context, Prev_Is_EA, Before_Prev_EA)
= Updated_State (Old_St, Text, Cur));
-- Advance position
if Cur > Text'Last - This_Len + 1 then
Next_Pos := Cur + This_Len;
pragma Assert (Next_Pos = Next_LB_From (Text, Pos));
return;
end if;
Cur := Cur + This_Len;
else
---------------------------------------------------------
-- Pre-compute ALL lookahead results needed by rules
---------------------------------------------------------
-- LB15b: × QU_Pf — look ahead for right context
if Eff_B = LBP_QU_Pf then
if Cur + This_Len <= Text'Last + 1 then
Scan_LB15b (Text, Cur + This_Len, LB15b_Result);
else
LB15b_Result := True; -- eot → applies
end if;
else
LB15b_Result := False;
end if;
-- Platinum: connect LB15b to ghost
pragma Assert
(LB15b_Result = Ghost_LB15b_At (Old_St, Text, Cur));
-- LB15c: SP ÷ IS NU — look ahead for NU after IS
if Prev_Eff = LBP_SP and Eff_B = LBP_IS then
if Cur + This_Len <= Text'Last + 1 then
Scan_LB15c (Text, Cur + This_Len, LB15c_Result);
else
LB15c_Result := False;
end if;
else
LB15c_Result := False;
end if;
-- Platinum: connect LB15c to ghost
pragma Assert
(LB15c_Result = Ghost_LB15c_At (Old_St, Text, Cur));
-- LB19a: look ahead for non-EA after QU
if Is_QU (Eff_B) and Prev_Is_EA then
if Cur + This_Len <= Text'Last + 1 then
Scan_LB19a_Non_EA
(Text, Cur + This_Len, LB19a_Result);
else
LB19a_Result := True; -- eot counts as non-EA
end if;
else
LB19a_Result := False;
end if;
-- Platinum: connect LB19a to ghost
pragma Assert
(LB19a_Result = Ghost_LB19a_At (Old_St, Text, Cur));
-- LB25: PO/PR × OP — look ahead for NU or IS NU
if (Prev_Eff = LBP_PO or Prev_Eff = LBP_PR)
and Is_OP (Eff_B)
then
if Cur + This_Len <= Text'Last + 1 then
Scan_LB25_OP_NU (Text, Cur + This_Len, LB25_OP_Result);
else
LB25_OP_Result := False;
end if;
else
LB25_OP_Result := False;
end if;
-- Platinum: connect LB25 to ghost
pragma Assert
(LB25_OP_Result = Ghost_LB25_OP_At (Old_St, Text, Cur));
-- LB28a sub-rule 4: look ahead for VF
if LB28a_Sub4_Prefix (Prev_Eff, Prev_Is_DC,
Eff_B, This_Is_DC)
then
if Cur + This_Len <= Text'Last + 1 then
Scan_LB28a_VF (Text, Cur + This_Len, LB28a_VF_Result);
else
LB28a_VF_Result := False;
end if;
else
LB28a_VF_Result := False;
end if;
-- Platinum: connect LB28a VF to ghost
pragma Assert
(LB28a_VF_Result = Ghost_LB28a_VF_At (Old_St, Text, Cur));
---------------------------------------------------------
-- Apply rules in priority order.
---------------------------------------------------------
-- LB4/LB5: Mandatory breaks
if LB5_CRLF (Prev_Actual, Eff_B) then
-- CR × LF: no break
Allow_Break := False;
elsif Is_Hard_Break (Prev_Actual) then
-- LB4/LB5: BK !, CR !, LF !, NL ! → mandatory break
-- Platinum: this is a break — Ghost_Break returns True
pragma Assert (not Ghost_Is_Absorbed (Old_St, Text, Cur));
pragma Assert (Is_Hard_Break (Old_St.Prev_Actual));
pragma Assert
(not LB5_CRLF (Old_St.Prev_Actual,
Ghost_Eff_B (Old_St, Text, Cur)));
pragma Assert (Ghost_Break (Old_St, Text, Cur));
Next_Pos := Cur;
pragma Assert (Next_Pos = Next_LB_From (Text, Pos));
return;
-- LB6: × (BK | CR | LF | NL)
elsif LB6_Applies (Eff_B) then
Allow_Break := False;
-- LB7: × SP, × ZW
elsif LB7_Applies (Eff_B) then
Allow_Break := False;
-- LB8: ZW SP* ÷
elsif In_SP_Run and Before_SP = LBP_ZW then
Allow_Break := True;
elsif (not In_SP_Run) and Prev_Eff = LBP_ZW then
Allow_Break := True;
-- LB8a: ZWJ ×
elsif Prev_Actual = LBP_ZWJ then
Allow_Break := False;
-- LB11: × WJ, WJ ×
elsif LB11_Before (Eff_B) then
Allow_Break := False;
elsif LB11_After (Prev_Eff) then
Allow_Break := False;
-- LB12: GL ×
elsif LB12_Applies (Prev_Eff) then
Allow_Break := False;
-- LB12a: [^SP BA HY HH] × GL
elsif LB12a_Applies (Prev_Eff, Eff_B) then
Allow_Break := False;
-- LB13: × CL, × CP, × EX, × SY
elsif LB13_Applies (Eff_B) then
Allow_Break := False;
-- LB14: OP SP* × (indirect via SP tracking)
elsif In_SP_Run and Is_OP (Before_SP) then
Allow_Break := False;
elsif (not In_SP_Run) and Is_OP (Prev_Eff) then
Allow_Break := False;
-- LB15a: QU_Pi_Context SP* ×
elsif In_SP_Run and QU_Pi_Context then
Allow_Break := False;
elsif (not In_SP_Run) and QU_Pi_Context then
Allow_Break := False;
-- LB15b: × QU_Pf (right context check)
elsif LB15b_Result then
Allow_Break := False;
-- LB15c: SP ÷ IS NU (break before decimal mark after space)
elsif Prev_Eff = LBP_SP and Eff_B = LBP_IS then
if LB15c_Result then
Allow_Break := True;
else
Allow_Break := False;
end if;
-- LB15d: × IS (don't break before IS)
elsif LB15d_Applies (Eff_B) then
Allow_Break := False;
-- LB16: (CL | CP) SP* × NS (indirect via SP tracking)
elsif In_SP_Run
and (Before_SP = LBP_CL or Is_CP (Before_SP))
and Eff_B = LBP_NS
then
Allow_Break := False;
elsif (not In_SP_Run)
and (Prev_Eff = LBP_CL or Is_CP (Prev_Eff))
and Eff_B = LBP_NS
then
Allow_Break := False;
-- LB17: B2 SP* × B2 (indirect via SP tracking)
elsif In_SP_Run and Before_SP = LBP_B2
and Eff_B = LBP_B2
then
Allow_Break := False;
elsif (not In_SP_Run) and Prev_Eff = LBP_B2
and Eff_B = LBP_B2
then
Allow_Break := False;
-- LB18: SP ÷
elsif Prev_Eff = LBP_SP then
Allow_Break := True;
-- LB19: × [QU - Pi], [QU - Pf] ×
elsif LB19_Before (Eff_B) then
Allow_Break := False;
elsif LB19_After (Prev_Eff) then
Allow_Break := False;
-- LB19a: East Asian QU context
elsif (not Prev_Is_EA) and Is_QU (Eff_B) then
Allow_Break := False;
elsif Is_QU (Eff_B) then
if LB19a_Result then
Allow_Break := False;
else
Allow_Break := True;
end if;
elsif Is_QU (Prev_Eff) and then (not This_Is_EA) then
Allow_Break := False;
elsif Is_QU (Prev_Eff) then
if Before_Prev_Eff = LBP_Other or (not Before_Prev_EA) then
Allow_Break := False;
else
Allow_Break := True;
end if;
-- LB20: ÷ CB, CB ÷
elsif LB20_Before (Eff_B) then
Allow_Break := True;
elsif LB20_After (Prev_Eff) then
Allow_Break := True;
-- LB20a: (sot|BK|CR|LF|NL|SP|ZW|CB|GL) (HY|HH) × (AL|HL)
elsif LB20a_Applies (Before_Prev_Eff, Prev_Eff, Eff_B) then
Allow_Break := False;
-- LB21: × BA, × HY, × HH, × NS, BB ×
elsif LB21_Applies (Prev_Eff, Eff_B) then
Allow_Break := False;
-- LB21a: HL (HY | HH) × [^HL]
elsif LB21a_Applies (Before_Prev_Eff, Prev_Eff, Eff_B) then
Allow_Break := False;
-- LB21b: SY × HL
elsif LB21b_Applies (Prev_Eff, Eff_B) then
Allow_Break := False;
-- LB22: × IN
elsif LB22_Applies (Eff_B) then
Allow_Break := False;
-- LB23: (AL|HL) × NU, NU × (AL|HL)
elsif LB23_Applies (Prev_Eff, Eff_B) then
Allow_Break := False;
-- LB23a: PR × (ID|EB|EM), (ID|EB|EM) × PO
elsif LB23a_Applies (Prev_Eff, Eff_B) then
Allow_Break := False;
-- LB24: (PR|PO) × (AL|HL), (AL|HL) × (PR|PO)
elsif LB24_Applies (Prev_Eff, Eff_B) then
Allow_Break := False;
-- LB25: Do not break numbers (context-sensitive)
elsif LB25_Simple (Prev_Eff, Eff_B) then
Allow_Break := False;
elsif LB25_NU_Context (Prev_Eff, Eff_B, In_NU_Context) then
Allow_Break := False;
elsif (Prev_Eff = LBP_PO or Prev_Eff = LBP_PR)
and Is_OP (Eff_B)
then
if LB25_OP_Result then
Allow_Break := False;
else
Allow_Break := True;
end if;
-- LB26: Korean syllable
elsif LB26_Applies (Prev_Eff, Eff_B) then
Allow_Break := False;
-- LB27: Korean syllable + PO/PR
elsif LB27_Applies (Prev_Eff, Eff_B) then
Allow_Break := False;
-- LB28: (AL|HL) × (AL|HL)
elsif LB28_Applies (Prev_Eff, Eff_B) then
Allow_Break := False;
-- LB28a: Brahmic orthographic syllable
elsif LB28a_Sub1 (Prev_Eff, Eff_B, This_Is_DC) then
Allow_Break := False;
elsif LB28a_Sub2 (Prev_Eff, Prev_Is_DC, Eff_B) then
Allow_Break := False;
elsif LB28a_Sub3 (Before_Prev_Eff, Before_Prev_DC,
Prev_Eff, Eff_B, This_Is_DC)
then
Allow_Break := False;
elsif LB28a_Sub4_Prefix (Prev_Eff, Prev_Is_DC,
Eff_B, This_Is_DC)
then
if LB28a_VF_Result then
Allow_Break := False;
else
Allow_Break := True;
end if;
-- LB29: IS × (AL|HL)
elsif LB29_Applies (Prev_Eff, Eff_B) then
Allow_Break := False;
-- LB30: (AL|HL|NU) × OP (non-EA), CP (non-EA) × (AL|HL|NU)
elsif LB30_Applies (Prev_Eff, Eff_B) then
Allow_Break := False;
-- LB30a: RI × RI (odd count → no break)
elsif Prev_Eff = LBP_RI and Eff_B = LBP_RI then
if RI_Count mod 2 = 1 then
Allow_Break := False;
else
Allow_Break := True;
end if;
-- LB30b: EB × EM, or (ExtPict ∧ Cn) × EM
elsif LB30b_Applies (Prev_Eff, Eff_B, Prev_ExtPict_Cn) then
Allow_Break := False;
-- LB31: ALL ÷ / ÷ ALL
else
Allow_Break := True;
end if;
---------------------------------------------------------
-- Apply break decision
---------------------------------------------------------
-- Platinum: Allow_Break = Is_Allow_Break with ghost spec
pragma Assert (Allow_Break = Is_Allow_Break
(Prev_Actual => Prev_Actual,
Prev_Eff => Prev_Eff,
Eff_B => Eff_B,
Before_Prev_Eff => Before_Prev_Eff,
In_SP_Run => In_SP_Run,
Before_SP => Before_SP,
QU_Pi_Ctx => QU_Pi_Context,
LB15b_Res => LB15b_Result,
LB15c_Res => LB15c_Result,
In_NU_Ctx => In_NU_Context,
LB25_OP_Res => LB25_OP_Result,
LB28a_VF_Res => LB28a_VF_Result,
Prev_Is_EA => Prev_Is_EA,
This_Is_EA => This_Is_EA,
Before_Prev_EA => Before_Prev_EA,
Prev_Is_DC => Prev_Is_DC,
This_Is_DC => This_Is_DC,
Before_Prev_DC => Before_Prev_DC,
Prev_ExtPict_Cn => Prev_ExtPict_Cn,
RI_Count => RI_Count,
LB19a_Res => LB19a_Result));
-- Platinum: the non-absorbed, non-hard-break case means
-- Ghost_Break = Is_Allow_Break result.
pragma Assert (not Ghost_Is_Absorbed (Old_St, Text, Cur));
pragma Assert
(not (Is_Hard_Break (Old_St.Prev_Actual)
and not LB5_CRLF (Old_St.Prev_Actual,
Ghost_Eff_B (Old_St, Text, Cur)))
or Allow_Break);
pragma Assert (Allow_Break = Ghost_Break (Old_St, Text, Cur));
if Allow_Break then
Next_Pos := Cur;
pragma Assert (Next_Pos = Next_LB_From (Text, Pos));
return;
end if;
---------------------------------------------------------
-- No break: update state and continue.
-- Compute ALL new values from old state, then assign.
-- This matches Updated_State_Normal which uses St (old).
---------------------------------------------------------
declare
New_Before_Prev_Eff : constant LBP_Value := Prev_Eff;
New_Before_Prev_DC : constant Boolean := Prev_Is_DC;
New_Before_Prev_EA : constant Boolean := Prev_Is_EA;
-- SP tracking (computed from old state)
New_In_SP : constant Boolean :=
(Eff_B = LBP_SP);
New_Before_SP : constant LBP_Value :=
(if Eff_B = LBP_SP then
(if not In_SP_Run then Prev_Eff else Before_SP)
else Before_SP);
-- RI counter (computed from old state)
New_RI_Count : constant Natural :=
(if Eff_B = LBP_RI then
(if RI_Count < Natural'Last
then RI_Count + 1 else RI_Count)
else 0);
-- QU_Pi context (computed from OLD In_SP_Run, Before_SP)
New_QU_Pi : constant Boolean :=
(if Eff_B = LBP_QU_Pi then
(if Is_LB15a_Before (Prev_Eff) then True
elsif In_SP_Run and Is_LB15a_Before (Before_SP)
then True
else QU_Pi_Context)
elsif Eff_B /= LBP_SP then False
else QU_Pi_Context);
-- NU context (computed from old state)
New_NU_Ctx : constant Boolean :=
(if Eff_B = LBP_NU then True
elsif In_NU_Context
and then (Eff_B = LBP_SY or Eff_B = LBP_IS)
then True
elsif In_NU_Context
and then (Eff_B = LBP_CL or Is_CP (Eff_B))
then True
else False);
-- ExtPict∧Cn (from current codepoint properties)
New_ExtPict_Cn : Boolean;
begin
-- Compute ExtPict∧Cn
if This_Valid
and then Properties.Get_ExtPict (This_CP)
then
declare
GC_Idx : constant UCD_Parser.Property_Index :=
Properties.Get_GC (This_CP);
begin
New_ExtPict_Cn :=
(GC_Idx >= 1
and then GC_Idx <= Properties.GC_Name_Count
and then Properties.GC_Name (GC_Idx) = "Cn");
end;
else
New_ExtPict_Cn := False;
end if;
-- Platinum: bridge for ExtPict_Cn
pragma Assert
(New_ExtPict_Cn = Ghost_ExtPict_Cn (Text, Cur));
-- Now assign all state at once
Prev_Eff := Eff_B;
Prev_Actual := This_LBP;
Before_Prev_Eff := New_Before_Prev_Eff;
Before_SP := New_Before_SP;
In_SP_Run := New_In_SP;
RI_Count := New_RI_Count;
QU_Pi_Context := New_QU_Pi;
Prev_ExtPict_Cn := New_ExtPict_Cn;
Prev_Is_DC := This_Is_DC;
Before_Prev_DC := New_Before_Prev_DC;
In_NU_Context := New_NU_Ctx;
Prev_Is_EA := This_Is_EA;
Before_Prev_EA := New_Before_Prev_EA;
-- Platinum: after all state updates, runtime matches ghost.
pragma Assert
(LB_State'(Prev_Eff, Prev_Actual, Before_Prev_Eff,
Before_SP, In_SP_Run, RI_Count,
QU_Pi_Context, Prev_ExtPict_Cn,
Prev_Is_DC, Before_Prev_DC,
In_NU_Context, Prev_Is_EA, Before_Prev_EA)
= Updated_State (Old_St, Text, Cur));
end;
-- Advance position
if Cur > Text'Last - This_Len + 1 then
Next_Pos := Cur + This_Len;
pragma Assert (Next_Pos = Next_LB_From (Text, Pos));
return;
end if;
Cur := Cur + This_Len;
end if;
end;
end loop;
-- Reached end of text (LB3: ! eot)
Next_Pos := Text'Last + 1;
pragma Assert (Next_Pos = Next_LB_From (Text, Pos));
end Next_Line_Break;
end Lingenic_Text.Line_Break;