-- 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 — Words body
--
-- Forward state machine for word boundary detection (UAX #29).
--
-- Decodes UTF-8, looks up WBP/ExtPict properties, maintains state for
-- WB4 (Extend/Format/ZWJ ignore), lookbehind (WB7, WB7c, WB11),
-- lookahead (WB6, WB7b, WB12), and RI pairing (WB15/16).
--
-- Invalid UTF-8 bytes are treated as single-byte codepoints with
-- WBP = Other, ExtPict = False.
--
-- SPARK Platinum: the loop invariant connects runtime state to the
-- recursive ghost function Next_WB, establishing that the returned
-- position equals Next_WB_From(Text, Pos).
-------------------------------------------------------------------------------
with Lingenic_Text.UTF8;
with Lingenic_Text.UCD_Parser;
package body Lingenic_Text.Words
with SPARK_Mode
is
-- RI counter upper bound.
Max_RI : constant := Natural'Last - 1;
subtype RI_Counter is Natural range 0 .. Max_RI;
---------------------------------------------------------------------------
-- Scan_After_B — body (declaration in spec)
---------------------------------------------------------------------------
procedure Scan_After_B
(Text : Byte_Array;
From : Positive;
Found : out Boolean;
After_WBP : out Words_Spec.WBP_Value)
is
use Words_Spec;
Scan : Positive := From;
Scan_WBP_Idx : UCD_Parser.Property_Index;
begin
Found := False;
After_WBP := WBP_Other;
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);
-- Platinum accumulator invariant: remaining lookahead from Scan
-- equals the full lookahead from From.
pragma Loop_Invariant
(Ghost_After_Found (Text, Scan) = Ghost_After_Found (Text, From));
pragma Loop_Invariant
(Ghost_After_WBP (Text, Scan) = Ghost_After_WBP (Text, From));
pragma Loop_Variant (Increases => Scan);
declare
Scan_CP : Codepoint;
Scan_Len : Positive;
Scan_Valid : Boolean;
Scan_WBP : WBP_Value;
begin
UTF8.Decode (Text, Scan, Scan_CP, Scan_Len, Scan_Valid);
-- Platinum: Scan_Len = Ghost_Step_Length
pragma Assert (Scan_Len = Ghost_Step_Length (Text, Scan));
-- Look up WBP — align computation path with ghost function.
-- Use WBP_To_Abstract(idx) for both valid and invalid bytes
-- so the solver can connect to Ghost_WBP.
if Scan_Valid then
Scan_WBP_Idx := Properties.Get_WBP (Scan_CP);
else
Scan_WBP_Idx := 0;
end if;
Scan_WBP := Properties.WBP_To_Abstract (Scan_WBP_Idx);
-- Platinum: connect runtime WBP to ghost WBP
pragma Assert (Scan_Valid = UTF8_Spec.Well_Formed_At (Text, Scan));
pragma Assert (Scan_CP = Ghost_CP (Text, Scan));
pragma Assert (Scan_WBP = Ghost_WBP (Text, Scan));
if not Is_Ignored (Scan_WBP) then
-- Found a non-ignored character
Found := True;
After_WBP := Scan_WBP;
return;
end if;
-- Skip this ignored character
if Scan > Text'Last - Scan_Len + 1 then
-- Reached end of text
return;
end if;
Scan := Scan + Scan_Len;
end;
end loop;
end Scan_After_B;
---------------------------------------------------------------------------
-- Next_Word_Break
---------------------------------------------------------------------------
procedure Next_Word_Break
(Text : Byte_Array;
Pos : Positive;
Next_Pos : out Positive)
is
use Words_Spec;
-- First codepoint (WB1: always start new segment)
First_CP : Codepoint;
First_Len : Positive;
First_Valid : Boolean;
First_WBP_Idx : UCD_Parser.Property_Index;
First_WBP : WBP_Value;
-- State variables
Prev_Actual : WBP_Value; -- Literal previous char
Prev_Eff : WBP_Value; -- Effective previous (WB4-adjusted)
Before_Prev_Eff : WBP_Value; -- Two effective chars back
RI_Count : RI_Counter;
-- Current position in text
Cur : Positive;
begin
-- Decode first codepoint (WB1: sot ÷)
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
Next_Pos := Pos + First_Len;
pragma Assert (Next_Pos = Next_WB_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 properties of first codepoint
if First_Valid then
First_WBP_Idx := Properties.Get_WBP (First_CP);
else
First_WBP_Idx := 0;
end if;
First_WBP := Properties.WBP_To_Abstract (First_WBP_Idx);
-- Initialize state
Prev_Actual := First_WBP;
Prev_Eff := First_WBP;
Before_Prev_Eff := WBP_Other; -- No char before first
RI_Count := (if First_WBP = WBP_Regional_Indicator then 1 else 0);
-- Platinum: connect runtime decoded CP to ghost decoded CP.
pragma Assert (First_Valid = UTF8_Spec.Well_Formed_At (Text, Pos));
pragma Assert (First_CP = Ghost_CP (Text, Pos));
-- Platinum: connect runtime property lookups to ghost functions.
pragma Assert (First_WBP = Ghost_WBP (Text, Pos));
-- Platinum: connect composite initial state to ghost Initial_State.
pragma Assert (Prev_Eff = Initial_State (Text, Pos).Prev_Eff);
pragma Assert (Before_Prev_Eff = Initial_State (Text, Pos).Before_Prev_Eff);
pragma Assert (RI_Count = Initial_State (Text, Pos).RI_Count);
-- Platinum: establish base case for the accumulator invariant.
pragma Assert
(Next_WB (Text, Cur,
WB_State'(Prev_Actual, Prev_Eff, Before_Prev_Eff, RI_Count))
= Next_WB_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);
pragma Loop_Invariant (RI_Count < Max_RI);
-- Platinum accumulator invariant: the remaining computation from
-- Cur with the current state equals the full computation from Pos.
pragma Loop_Invariant
(Next_WB (Text, Cur,
WB_State'(Prev_Actual, Prev_Eff,
Before_Prev_Eff, RI_Count))
= Next_WB_From (Text, Pos));
pragma Loop_Variant (Increases => Cur);
declare
This_CP : Codepoint;
This_Len : Positive;
This_Valid : Boolean;
This_WBP_Idx : UCD_Parser.Property_Index;
This_WBP : WBP_Value;
This_ExtPict : Boolean;
Is_Break : Boolean;
-- Lookahead result
After_Found : Boolean;
After_WBP : WBP_Value;
-- Ghost: save state before updates for inductive step
Old_St : constant WB_State :=
WB_State'(Prev_Actual, Prev_Eff, Before_Prev_Eff, RI_Count)
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 properties
if This_Valid then
This_WBP_Idx := Properties.Get_WBP (This_CP);
This_ExtPict := Properties.Get_ExtPict (This_CP);
else
This_WBP_Idx := 0;
This_ExtPict := False;
end if;
This_WBP := Properties.WBP_To_Abstract (This_WBP_Idx);
-- Platinum: connect runtime decoded CP to ghost decoded CP.
pragma Assert (This_Valid = UTF8_Spec.Well_Formed_At (Text, Cur));
pragma Assert (This_CP = Ghost_CP (Text, Cur));
-- Platinum: connect runtime properties to ghost functions.
pragma Assert (This_WBP = Ghost_WBP (Text, Cur));
pragma Assert (This_ExtPict = Ghost_ExtPict (Text, Cur));
-- Perform lookahead for rules WB6, WB7b, WB12
-- Only needed when B could be a "mid" character
if Is_MidLetter_Or_MidNumLetQ (This_WBP)
or This_WBP = WBP_Double_Quote
or Is_MidNum_Or_MidNumLetQ (This_WBP)
then
-- Platinum: This_WBP needs lookahead = Ghost_Needs_Lookahead
pragma Assert (Ghost_Needs_Lookahead (This_WBP));
if Cur + This_Len <= Text'Last + 1 then
Scan_After_B (Text, Cur + This_Len, After_Found, After_WBP);
-- Platinum: Scan_After_B postcondition gives us:
-- After_Found = Ghost_After_Found(Text, Cur + This_Len)
-- After_WBP = Ghost_After_WBP(Text, Cur + This_Len)
-- Which equals Ghost_After_Found_At / Ghost_After_WBP_At
-- since Ghost_Needs_Lookahead is true and
-- Cur + step <= Text'Last + 1.
else
After_Found := False;
After_WBP := WBP_Other;
end if;
else
After_Found := False;
After_WBP := WBP_Other;
end if;
-- Platinum: connect lookahead to ghost functions.
pragma Assert (After_Found = Ghost_After_Found_At (Text, Cur));
pragma Assert (After_WBP = Ghost_After_WBP_At (Text, Cur));
-- Apply composite break decision
Is_Break := Is_Word_Break
(A_Actual => Prev_Actual,
A_Eff => Prev_Eff,
B_WBP => This_WBP,
B_ExtPict => This_ExtPict,
Before_A => Before_Prev_Eff,
After_B => After_WBP,
Has_After => After_Found,
RI_Count_Odd => RI_Count mod 2 = 1);
-- Platinum: Is_Break = Ghost_Break with current state.
pragma Assert
(Is_Break = Ghost_Break
(WB_State'(Prev_Actual, Prev_Eff,
Before_Prev_Eff, RI_Count),
Text, Cur));
if Is_Break then
Next_Pos := Cur;
-- Platinum: Next_WB returns Cur when Ghost_Break is true.
-- Combined with the accumulator invariant, this gives us
-- Next_Pos = Next_WB_From(Text, Pos).
pragma Assert (Next_Pos = Next_WB_From (Text, Pos));
return;
end if;
-- No break: update state and continue
--
-- Structure mirrors Updated_State: two-way branch on WB4.
if Is_Ignored (This_WBP)
and not Is_Newline_Or_CRLF (Prev_Eff)
then
-- WB4 transparent: only Prev_Actual changes.
-- Prev_Eff, Before_Prev_Eff, RI_Count unchanged.
Prev_Actual := This_WBP;
else
-- Non-ignored character: shift all effective state.
Before_Prev_Eff := Prev_Eff;
Prev_Eff := This_WBP;
Prev_Actual := This_WBP;
-- Update RI count
if This_WBP = WBP_Regional_Indicator then
if RI_Count < Max_RI - 1 then
RI_Count := RI_Count + 1;
end if;
else
RI_Count := 0;
end if;
end if;
-- Platinum: after all state updates, the runtime state matches
-- the ghost Updated_State applied to the saved old state.
pragma Assert
(WB_State'(Prev_Actual, Prev_Eff, Before_Prev_Eff, RI_Count)
= Updated_State (Old_St, Text, Cur));
-- Advance position
if Cur > Text'Last - This_Len + 1 then
-- This codepoint reaches end of text
Next_Pos := Cur + This_Len;
-- Platinum: Next_WB returns Cur + step when past end,
-- Ghost_Break is false (checked above).
pragma Assert (Next_Pos = Next_WB_From (Text, Pos));
return;
end if;
Cur := Cur + This_Len;
end;
end loop;
-- Reached end of text (WB2: ÷ eot)
Next_Pos := Text'Last + 1;
-- Platinum: Cur not in Text'Range, so Next_WB returns Cur
-- (which equals Text'Last + 1).
pragma Assert (Next_Pos = Next_WB_From (Text, Pos));
end Next_Word_Break;
end Lingenic_Text.Words;