-- 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 — Sentences body
--
-- Forward state machine for sentence boundary detection (UAX #29).
--
-- Decodes UTF-8, looks up SBP properties, maintains state for
-- SB5 (Extend/Format ignore), lookbehind (SB7, SB8–SB11 via SA_State),
-- and SB8 lookahead (Scan_For_SB8_Lower).
--
-- Invalid UTF-8 bytes are treated as single-byte codepoints with
-- SBP = Other.
--
-- SPARK Platinum: the loop invariant connects runtime state to the
-- recursive ghost function Next_SB, establishing that the returned
-- position equals Next_SB_From(Text, Pos).
-------------------------------------------------------------------------------
with Lingenic_Text.UTF8;
with Lingenic_Text.UCD_Parser;
package body Lingenic_Text.Sentences
with SPARK_Mode
is
---------------------------------------------------------------------------
-- Scan_For_SB8_Lower — specialized SB8 lookahead
--
-- Starting from byte position From in Text, decode codepoints and
-- skip those whose SBP is Extend or Format (SB5 transparent).
-- For each non-ignored character:
-- - Lower → Found := True, return
-- - OLetter, Upper, ParaSep, SATerm → Found := False (stopper)
-- - Otherwise → continue scanning (gap character)
-- End of text → Found := False
--
-- Platinum postcondition: Found matches Ghost_SB8_Lower.
---------------------------------------------------------------------------
procedure Scan_For_SB8_Lower
(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_SB8_Lower (Text, From)
is
use Sentences_Spec;
Scan : Positive := From;
Scan_SBP_Idx : UCD_Parser.Property_Index;
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);
-- Platinum accumulator invariant
pragma Loop_Invariant
(Ghost_SB8_Lower (Text, Scan) = Ghost_SB8_Lower (Text, From));
pragma Loop_Variant (Increases => Scan);
declare
Scan_CP : Codepoint;
Scan_Len : Positive;
Scan_Valid : Boolean;
Scan_SBP : SBP_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 SBP — use SBP_To_Abstract(idx) for both paths
if Scan_Valid then
Scan_SBP_Idx := Properties.Get_SBP (Scan_CP);
else
Scan_SBP_Idx := 0;
end if;
Scan_SBP := Properties.SBP_To_Abstract (Scan_SBP_Idx);
-- Platinum: connect runtime SBP to ghost SBP
pragma Assert (Scan_Valid = UTF8_Spec.Well_Formed_At (Text, Scan));
pragma Assert (Scan_CP = Ghost_CP (Text, Scan));
pragma Assert (Scan_SBP = Ghost_SBP (Text, Scan));
if not Is_Ignored (Scan_SBP) then
-- Non-ignored character found
if Scan_SBP = SBP_Lower then
Found := True;
return;
elsif Is_SB8_Stopper (Scan_SBP) then
Found := False;
return;
end if;
-- Gap character — continue scanning
end if;
-- Advance past this 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_For_SB8_Lower;
---------------------------------------------------------------------------
-- Next_Sentence_Break
---------------------------------------------------------------------------
procedure Next_Sentence_Break
(Text : Byte_Array;
Pos : Positive;
Next_Pos : out Positive)
is
use Sentences_Spec;
-- First codepoint (SB1: always start new segment)
First_CP : Codepoint;
First_Len : Positive;
First_Valid : Boolean;
First_SBP_Idx : UCD_Parser.Property_Index;
First_SBP : SBP_Value;
-- State variables
Prev_Actual : SBP_Value; -- Literal previous char
Prev_Eff : SBP_Value; -- Effective previous (SB5-adjusted)
Before_Prev_Eff : SBP_Value; -- Two effective chars back
SA_St : SA_State; -- SATerm sequence state
SA_ATerm_Flag : Boolean; -- Was the SATerm an ATerm?
-- Current position in text
Cur : Positive;
begin
-- Decode first codepoint (SB1: 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_SB_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_SBP_Idx := Properties.Get_SBP (First_CP);
else
First_SBP_Idx := 0;
end if;
First_SBP := Properties.SBP_To_Abstract (First_SBP_Idx);
-- Initialize state
Prev_Actual := First_SBP;
Prev_Eff := First_SBP;
Before_Prev_Eff := SBP_Other; -- No char before first
-- Initialize SA_State based on first codepoint
if First_SBP = SBP_ATerm then
SA_St := SA_Term;
SA_ATerm_Flag := True;
elsif First_SBP = SBP_STerm then
SA_St := SA_Term;
SA_ATerm_Flag := False;
else
SA_St := SA_None;
SA_ATerm_Flag := False;
end if;
-- 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_SBP = Ghost_SBP (Text, Pos));
-- Platinum: connect SA_State initialization to ghost functions.
pragma Assert (SA_St = Ghost_Next_SA (SA_None, First_SBP));
pragma Assert (SA_ATerm_Flag = Ghost_Next_ATerm_Flag (False, First_SBP));
-- 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 (SA_St = Initial_State (Text, Pos).SA_St);
pragma Assert (SA_ATerm_Flag = Initial_State (Text, Pos).SA_ATerm_Flag);
-- Platinum: establish base case for the accumulator invariant.
pragma Assert
(Next_SB (Text, Cur,
SB_State'(Prev_Actual, Prev_Eff, Before_Prev_Eff,
SA_St, SA_ATerm_Flag))
= Next_SB_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_SB (Text, Cur,
SB_State'(Prev_Actual, Prev_Eff, Before_Prev_Eff,
SA_St, SA_ATerm_Flag))
= Next_SB_From (Text, Pos));
pragma Loop_Variant (Increases => Cur);
declare
This_CP : Codepoint;
This_Len : Positive;
This_Valid : Boolean;
This_SBP_Idx : UCD_Parser.Property_Index;
This_SBP : SBP_Value;
Is_Break : Boolean;
-- SB8 lookahead result
SB8_Found : Boolean;
-- Ghost: save state before updates for inductive step
Old_St : constant SB_State :=
SB_State'(Prev_Actual, Prev_Eff, Before_Prev_Eff,
SA_St, SA_ATerm_Flag)
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_SBP_Idx := Properties.Get_SBP (This_CP);
else
This_SBP_Idx := 0;
end if;
This_SBP := Properties.SBP_To_Abstract (This_SBP_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_SBP = Ghost_SBP (Text, Cur));
-- Perform SB8 lookahead when needed
if SA_St in SA_Term | SA_Close | SA_Sp
and then SA_ATerm_Flag
and then This_SBP /= SBP_Lower
and then not Is_SB8_Stopper (This_SBP)
and then not Is_Ignored (This_SBP)
then
pragma Assert (Ghost_SB8_Needed (Old_St, This_SBP));
if Cur + This_Len <= Text'Last + 1 then
Scan_For_SB8_Lower (Text, Cur + This_Len, SB8_Found);
else
SB8_Found := False;
end if;
else
SB8_Found := False;
end if;
-- Platinum: connect SB8 lookahead to ghost function.
pragma Assert (SB8_Found = Ghost_SB8_At (Old_St, Text, Cur));
-- Apply composite break decision
Is_Break := Is_Sentence_Break
(A_Actual => Prev_Actual,
A_Eff => Prev_Eff,
B_SBP => This_SBP,
Before_A => Before_Prev_Eff,
SA => SA_St,
SA_ATerm => SA_ATerm_Flag,
SB8_Found => SB8_Found);
-- Platinum: Is_Break = Ghost_Break with current state.
pragma Assert
(Is_Break = Ghost_Break (Old_St, Text, Cur));
if Is_Break then
Next_Pos := Cur;
pragma Assert (Next_Pos = Next_SB_From (Text, Pos));
return;
end if;
-- No break: update state and continue
-- Structure mirrors Updated_State: two-way branch on SB5.
if Is_Ignored (This_SBP)
and not Is_ParaSep (Prev_Eff)
then
-- SB5 transparent: only Prev_Actual changes
Prev_Actual := This_SBP;
else
-- Non-ignored character: shift effective state
Before_Prev_Eff := Prev_Eff;
Prev_Eff := This_SBP;
Prev_Actual := This_SBP;
-- Update SA_State
if This_SBP = SBP_ATerm then
SA_St := SA_Term;
SA_ATerm_Flag := True;
elsif This_SBP = SBP_STerm then
SA_St := SA_Term;
SA_ATerm_Flag := False;
elsif This_SBP = SBP_Close
and SA_St in SA_Term | SA_Close
then
SA_St := SA_Close;
elsif This_SBP = SBP_Sp
and SA_St in SA_Term | SA_Close | SA_Sp
then
SA_St := SA_Sp;
else
SA_St := SA_None;
end if;
end if;
-- Platinum: after all state updates, runtime state matches ghost.
pragma Assert
(SB_State'(Prev_Actual, Prev_Eff, Before_Prev_Eff,
SA_St, SA_ATerm_Flag)
= 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;
pragma Assert (Next_Pos = Next_SB_From (Text, Pos));
return;
end if;
Cur := Cur + This_Len;
end;
end loop;
-- Reached end of text (SB2: ÷ eot)
Next_Pos := Text'Last + 1;
pragma Assert (Next_Pos = Next_SB_From (Text, Pos));
end Next_Sentence_Break;
end Lingenic_Text.Sentences;