-- 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
--
-- Sentence break segmentation (UAX #29).
--
-- Implements the Unicode Sentence Boundary algorithm as a forward state
-- machine over UTF-8 text. Each call to Next_Sentence_Break returns the
-- byte position of the next sentence boundary.
--
-- The algorithm references the ghost specification in Sentences_Spec,
-- which encodes SB rules 3 through 998 as expression functions.
--
-- SB5 (ignore rule) makes Extend/Format characters transparent when
-- evaluating rules SB6–SB998. The state machine tracks "effective"
-- previous characters (the last non-Extend/Format) for those rules.
--
-- SB8–SB11 use SA_State lookbehind to track SATerm Close* Sp* sequences.
-- SB8 uses a specialized forward scan (Scan_For_SB8_Lower) to find
-- a Lower character past gap characters.
--
-- Invalid UTF-8 bytes are treated as single-byte codepoints with
-- SBP = Other.
--
-- SPARK Platinum: the postcondition references the recursive ghost function
-- Next_SB_From, which simulates the algorithm as an expression function.
-- GNATprove verifies the implementation matches this specification.
-------------------------------------------------------------------------------
with Lingenic_Text.Properties;
with Lingenic_Text.Sentences_Spec;
with Lingenic_Text.UTF8_Spec;
package Lingenic_Text.Sentences
with SPARK_Mode
is
---------------------------------------------------------------------------
-- Ghost state record for sentence break state machine
---------------------------------------------------------------------------
type SB_State is record
Prev_Actual : Sentences_Spec.SBP_Value;
Prev_Eff : Sentences_Spec.SBP_Value;
Before_Prev_Eff : Sentences_Spec.SBP_Value;
SA_St : Sentences_Spec.SA_State;
SA_ATerm_Flag : Boolean;
end record;
---------------------------------------------------------------------------
-- Ghost helper functions
---------------------------------------------------------------------------
function Ghost_Step_Length
(Text : Byte_Array;
Cur : Positive) return Positive
is (if UTF8_Spec.Well_Formed_At (Text, Cur)
then UTF8_Spec.Lead_Length (Text (Cur))
else 1)
with Ghost,
Pre => Text'First = 1
and then Text'Last >= 1
and then Text'Last < Positive'Last
and then Cur in Text'Range;
function Ghost_CP
(Text : Byte_Array;
Cur : Positive) return Codepoint
is (if UTF8_Spec.Well_Formed_At (Text, Cur)
then UTF8_Spec.Decoded_At (Text, Cur)
else 0)
with Ghost,
Pre => Text'First = 1
and then Text'Last >= 1
and then Text'Last < Positive'Last
and then Cur in Text'Range;
-- SBP value at Cur (uses SBP_To_Abstract(0) for invalid bytes).
function Ghost_SBP
(Text : Byte_Array;
Cur : Positive) return Sentences_Spec.SBP_Value
is (if UTF8_Spec.Well_Formed_At (Text, Cur)
then Properties.SBP_To_Abstract
(Properties.Get_SBP (UTF8_Spec.Decoded_At (Text, Cur)))
else Properties.SBP_To_Abstract (0))
with Ghost,
Global => Properties.Property_State,
Pre => Text'First = 1
and then Text'Last >= 1
and then Text'Last < Positive'Last
and then Cur in Text'Range
and then Properties.Initialized;
---------------------------------------------------------------------------
-- Ghost SB8 lookahead: scan for Lower past gap characters
--
-- Recursive function that mirrors Scan_For_SB8_Lower.
-- Returns True if a Lower is found before a stopper or end of text.
---------------------------------------------------------------------------
function Ghost_SB8_Lower
(Text : Byte_Array;
From : Positive) return Boolean
is (if From not in Text'Range then False
elsif not Sentences_Spec.Is_Ignored (Ghost_SBP (Text, From)) then
-- Non-ignored character: check if Lower or stopper
(if Ghost_SBP (Text, From) = Sentences_Spec.SBP_Lower then True
elsif Sentences_Spec.Is_SB8_Stopper (Ghost_SBP (Text, From))
then False
-- Gap character: continue scanning
elsif From > Text'Last - Ghost_Step_Length (Text, From) + 1
then False
else Ghost_SB8_Lower
(Text, From + Ghost_Step_Length (Text, From)))
elsif From > Text'Last - Ghost_Step_Length (Text, From) + 1 then False
else Ghost_SB8_Lower
(Text, From + Ghost_Step_Length (Text, From)))
with Ghost,
Global => Properties.Property_State,
Pre => Text'First = 1
and then Text'Last >= 1
and then Text'Last < Positive'Last
and then From > 0
and then Properties.Initialized,
Subprogram_Variant => (Decreases => Text'Last - From + 1);
---------------------------------------------------------------------------
-- Ghost SB8 lookahead at Cur (convenience wrapper)
--
-- Only performs the scan when the SB8 context conditions are met.
---------------------------------------------------------------------------
function Ghost_SB8_Needed
(St : SB_State;
B_SBP : Sentences_Spec.SBP_Value) return Boolean
is (St.SA_St in Sentences_Spec.SA_Term
| Sentences_Spec.SA_Close
| Sentences_Spec.SA_Sp
and then St.SA_ATerm_Flag
and then B_SBP /= Sentences_Spec.SBP_Lower
and then not Sentences_Spec.Is_SB8_Stopper (B_SBP)
and then not Sentences_Spec.Is_Ignored (B_SBP))
with Ghost;
function Ghost_SB8_At
(St : SB_State;
Text : Byte_Array;
Cur : Positive) return Boolean
is (if Ghost_SB8_Needed (St, Ghost_SBP (Text, Cur))
and then Cur + Ghost_Step_Length (Text, Cur) <= Text'Last + 1
then Ghost_SB8_Lower
(Text, Cur + Ghost_Step_Length (Text, Cur))
else False)
with Ghost,
Global => Properties.Property_State,
Pre => Text'First = 1
and then Text'Last >= 1
and then Text'Last < Positive'Last
and then Cur in Text'Range
and then Properties.Initialized;
---------------------------------------------------------------------------
-- Ghost break decision at Cur given state St.
---------------------------------------------------------------------------
function Ghost_Break
(St : SB_State;
Text : Byte_Array;
Cur : Positive) return Boolean
is (Sentences_Spec.Is_Sentence_Break
(A_Actual => St.Prev_Actual,
A_Eff => St.Prev_Eff,
B_SBP => Ghost_SBP (Text, Cur),
Before_A => St.Before_Prev_Eff,
SA => St.SA_St,
SA_ATerm => St.SA_ATerm_Flag,
SB8_Found => Ghost_SB8_At (St, Text, Cur)))
with Ghost,
Global => Properties.Property_State,
Pre => Text'First = 1
and then Text'Last >= 1
and then Text'Last < Positive'Last
and then Cur in Text'Range
and then Properties.Initialized;
---------------------------------------------------------------------------
-- Ghost state transitions
---------------------------------------------------------------------------
function Ghost_Next_SA
(SA_St : Sentences_Spec.SA_State;
B_SBP : Sentences_Spec.SBP_Value)
return Sentences_Spec.SA_State
is (if B_SBP = Sentences_Spec.SBP_ATerm then Sentences_Spec.SA_Term
elsif B_SBP = Sentences_Spec.SBP_STerm then Sentences_Spec.SA_Term
elsif B_SBP = Sentences_Spec.SBP_Close
and SA_St in Sentences_Spec.SA_Term | Sentences_Spec.SA_Close
then Sentences_Spec.SA_Close
elsif B_SBP = Sentences_Spec.SBP_Sp
and SA_St in Sentences_Spec.SA_Term
| Sentences_Spec.SA_Close
| Sentences_Spec.SA_Sp
then Sentences_Spec.SA_Sp
else Sentences_Spec.SA_None)
with Ghost;
function Ghost_Next_ATerm_Flag
(SA_ATerm_Flag : Boolean;
B_SBP : Sentences_Spec.SBP_Value)
return Boolean
is (if B_SBP = Sentences_Spec.SBP_ATerm then True
elsif B_SBP = Sentences_Spec.SBP_STerm then False
else SA_ATerm_Flag)
with Ghost;
function Updated_State
(St : SB_State;
Text : Byte_Array;
Cur : Positive) return SB_State
is (if Sentences_Spec.Is_Ignored (Ghost_SBP (Text, Cur))
and not Sentences_Spec.Is_ParaSep (St.Prev_Eff)
then
-- SB5 transparent: only Prev_Actual changes
SB_State'
(Prev_Actual => Ghost_SBP (Text, Cur),
Prev_Eff => St.Prev_Eff,
Before_Prev_Eff => St.Before_Prev_Eff,
SA_St => St.SA_St,
SA_ATerm_Flag => St.SA_ATerm_Flag)
else
-- Non-ignored: shift effective state
SB_State'
(Prev_Actual => Ghost_SBP (Text, Cur),
Prev_Eff => Ghost_SBP (Text, Cur),
Before_Prev_Eff => St.Prev_Eff,
SA_St => Ghost_Next_SA
(St.SA_St, Ghost_SBP (Text, Cur)),
SA_ATerm_Flag => Ghost_Next_ATerm_Flag
(St.SA_ATerm_Flag,
Ghost_SBP (Text, Cur))))
with Ghost,
Global => Properties.Property_State,
Pre => Text'First = 1
and then Text'Last >= 1
and then Text'Last < Positive'Last
and then Cur in Text'Range
and then Properties.Initialized;
function Initial_State
(Text : Byte_Array;
Pos : Positive) return SB_State
is (SB_State'
(Prev_Actual => Ghost_SBP (Text, Pos),
Prev_Eff => Ghost_SBP (Text, Pos),
Before_Prev_Eff => Sentences_Spec.SBP_Other,
SA_St => Ghost_Next_SA
(Sentences_Spec.SA_None,
Ghost_SBP (Text, Pos)),
SA_ATerm_Flag => Ghost_Next_ATerm_Flag
(False, Ghost_SBP (Text, Pos))))
with Ghost,
Global => Properties.Property_State,
Pre => Text'First = 1
and then Text'Last >= 1
and then Text'Last < Positive'Last
and then Pos in Text'Range
and then Properties.Initialized;
---------------------------------------------------------------------------
-- Recursive ghost function: simulates the forward loop.
---------------------------------------------------------------------------
function Next_SB
(Text : Byte_Array;
Cur : Positive;
St : SB_State) return Positive
is (if Cur not in Text'Range then
(if Cur <= Text'Last + 1 then Cur else Text'Last + 1)
elsif Ghost_Break (St, Text, Cur) then
Cur
elsif Cur > Text'Last - Ghost_Step_Length (Text, Cur) + 1 then
Cur + Ghost_Step_Length (Text, Cur)
else
Next_SB (Text,
Cur + Ghost_Step_Length (Text, Cur),
Updated_State (St, Text, Cur)))
with Ghost,
Global => Properties.Property_State,
Pre => Text'First = 1
and then Text'Last >= 1
and then Text'Last < Positive'Last
and then Cur > 0
and then Properties.Initialized,
Subprogram_Variant => (Decreases => Text'Last - Cur + 1);
---------------------------------------------------------------------------
-- Top-level wrapper: handles first codepoint (SB1), then recurses.
---------------------------------------------------------------------------
function Next_SB_From
(Text : Byte_Array;
Pos : Positive) return Positive
is (if Pos > Text'Last - Ghost_Step_Length (Text, Pos) + 1 then
Pos + Ghost_Step_Length (Text, Pos)
else
Next_SB (Text,
Pos + Ghost_Step_Length (Text, Pos),
Initial_State (Text, Pos)))
with Ghost,
Global => Properties.Property_State,
Pre => Text'First = 1
and then Text'Last >= 1
and then Text'Last < Positive'Last
and then Pos in Text'Range
and then Properties.Initialized;
---------------------------------------------------------------------------
-- Next_Sentence_Break — True Platinum postcondition
---------------------------------------------------------------------------
procedure Next_Sentence_Break
(Text : Byte_Array;
Pos : Positive;
Next_Pos : out Positive)
with Pre => Text'First = 1
and then Text'Last >= 1
and then Text'Last < Positive'Last
and then Pos in Text'Range
and then Properties.Initialized,
Post => Next_Pos = Next_SB_From (Text, Pos)
and then Next_Pos > Pos
and then Next_Pos <= Text'Last + 1;
end Lingenic_Text.Sentences;