-- 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
--
-- Word break segmentation (UAX #29).
--
-- Implements the Unicode Word Boundary algorithm as a forward state machine
-- over UTF-8 text. Each call to Next_Word_Break returns the byte position
-- of the next word boundary.
--
-- The algorithm references the ghost specification in Words_Spec,
-- which encodes WB rules 3 through 999 as expression functions.
--
-- WB4 (ignore rule) makes Extend/Format/ZWJ characters transparent when
-- evaluating rules WB5–WB999. The state machine tracks "effective"
-- previous characters (the last non-Extend/Format/ZWJ) for those rules.
--
-- Lookahead rules (WB6, WB7b, WB12) scan forward past ignored characters
-- to find the next effective character.
--
-- Invalid UTF-8 bytes are treated as single-byte codepoints with
-- WBP = Other, ExtPict = False.
--
-- SPARK Platinum: the postcondition references the recursive ghost function
-- Next_WB_From, which simulates the algorithm as an expression function.
-- GNATprove verifies the implementation matches this specification.
-------------------------------------------------------------------------------
with Lingenic_Text.Properties;
with Lingenic_Text.Words_Spec;
with Lingenic_Text.UTF8_Spec;
package Lingenic_Text.Words
with SPARK_Mode
is
---------------------------------------------------------------------------
-- Ghost state record for word break state machine
---------------------------------------------------------------------------
type WB_State is record
Prev_Actual : Words_Spec.WBP_Value;
Prev_Eff : Words_Spec.WBP_Value;
Before_Prev_Eff : Words_Spec.WBP_Value;
RI_Count : Natural;
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;
-- WBP value at Cur (uses WBP_To_Abstract(0) for invalid bytes).
function Ghost_WBP
(Text : Byte_Array;
Cur : Positive) return Words_Spec.WBP_Value
is (if UTF8_Spec.Well_Formed_At (Text, Cur)
then Properties.WBP_To_Abstract
(Properties.Get_WBP (UTF8_Spec.Decoded_At (Text, Cur)))
else Properties.WBP_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;
-- ExtPict flag at Cur.
function Ghost_ExtPict
(Text : Byte_Array;
Cur : Positive) return Boolean
is (if UTF8_Spec.Well_Formed_At (Text, Cur)
then Properties.Get_ExtPict (UTF8_Spec.Decoded_At (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 lookahead: first non-ignored WBP after position From
--
-- Recursive function that mirrors Scan_After_B.
-- Returns (True, WBP) if found, (False, WBP_Other) if end of text.
---------------------------------------------------------------------------
function Ghost_After_Found
(Text : Byte_Array;
From : Positive) return Boolean
is (if From not in Text'Range then False
elsif not Words_Spec.Is_Ignored (Ghost_WBP (Text, From)) then True
elsif From > Text'Last - Ghost_Step_Length (Text, From) + 1 then False
else Ghost_After_Found
(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);
function Ghost_After_WBP
(Text : Byte_Array;
From : Positive) return Words_Spec.WBP_Value
is (if From not in Text'Range then Words_Spec.WBP_Other
elsif not Words_Spec.Is_Ignored (Ghost_WBP (Text, From))
then Ghost_WBP (Text, From)
elsif From > Text'Last - Ghost_Step_Length (Text, From) + 1
then Words_Spec.WBP_Other
else Ghost_After_WBP
(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 break decision at Cur given state St.
--
-- Performs lookahead when B is a mid-character.
---------------------------------------------------------------------------
Ghost_Max_RI : constant := Natural'Last - 1;
function Ghost_Needs_Lookahead
(B_WBP : Words_Spec.WBP_Value) return Boolean
is (Words_Spec.Is_MidLetter_Or_MidNumLetQ (B_WBP)
or B_WBP = Words_Spec.WBP_Double_Quote
or Words_Spec.Is_MidNum_Or_MidNumLetQ (B_WBP))
with Ghost;
function Ghost_After_Found_At
(Text : Byte_Array;
Cur : Positive) return Boolean
is (if Ghost_Needs_Lookahead (Ghost_WBP (Text, Cur))
and then Cur + Ghost_Step_Length (Text, Cur) <= Text'Last + 1
then Ghost_After_Found
(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;
function Ghost_After_WBP_At
(Text : Byte_Array;
Cur : Positive) return Words_Spec.WBP_Value
is (if Ghost_Needs_Lookahead (Ghost_WBP (Text, Cur))
and then Cur + Ghost_Step_Length (Text, Cur) <= Text'Last + 1
then Ghost_After_WBP
(Text, Cur + Ghost_Step_Length (Text, Cur))
else Words_Spec.WBP_Other)
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 Ghost_Break
(St : WB_State;
Text : Byte_Array;
Cur : Positive) return Boolean
is (Words_Spec.Is_Word_Break
(A_Actual => St.Prev_Actual,
A_Eff => St.Prev_Eff,
B_WBP => Ghost_WBP (Text, Cur),
B_ExtPict => Ghost_ExtPict (Text, Cur),
Before_A => St.Before_Prev_Eff,
After_B => Ghost_After_WBP_At (Text, Cur),
Has_After => Ghost_After_Found_At (Text, Cur),
RI_Count_Odd => St.RI_Count mod 2 = 1))
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 Updated_State
(St : WB_State;
Text : Byte_Array;
Cur : Positive) return WB_State
is (if Words_Spec.Is_Ignored (Ghost_WBP (Text, Cur))
and not Words_Spec.Is_Newline_Or_CRLF (St.Prev_Eff)
then
-- WB4 transparent: only Prev_Actual changes
WB_State'
(Prev_Actual => Ghost_WBP (Text, Cur),
Prev_Eff => St.Prev_Eff,
Before_Prev_Eff => St.Before_Prev_Eff,
RI_Count => St.RI_Count)
else
-- Non-ignored: shift effective state
WB_State'
(Prev_Actual => Ghost_WBP (Text, Cur),
Prev_Eff => Ghost_WBP (Text, Cur),
Before_Prev_Eff => St.Prev_Eff,
RI_Count =>
(if Ghost_WBP (Text, Cur) = Words_Spec.WBP_Regional_Indicator
then (if St.RI_Count < Ghost_Max_RI - 1
then St.RI_Count + 1
else St.RI_Count)
else 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;
function Initial_State
(Text : Byte_Array;
Pos : Positive) return WB_State
is (WB_State'
(Prev_Actual => Ghost_WBP (Text, Pos),
Prev_Eff => Ghost_WBP (Text, Pos),
Before_Prev_Eff => Words_Spec.WBP_Other,
RI_Count =>
(if Ghost_WBP (Text, Pos) = Words_Spec.WBP_Regional_Indicator
then 1 else 0)))
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_WB
(Text : Byte_Array;
Cur : Positive;
St : WB_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_WB (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 (WB1), then recurses.
---------------------------------------------------------------------------
function Next_WB_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_WB (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;
---------------------------------------------------------------------------
-- Scan_After_B — lookahead past Extend/Format/ZWJ
--
-- Starting from byte position From in Text, decode codepoints and
-- skip those whose WBP is Extend, Format, or ZWJ. Return the WBP
-- of the first non-ignored character found, or Found = False if
-- end of text is reached.
---------------------------------------------------------------------------
procedure Scan_After_B
(Text : Byte_Array;
From : Positive;
Found : out Boolean;
After_WBP : out Words_Spec.WBP_Value)
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_After_Found (Text, From)
and then After_WBP = Ghost_After_WBP (Text, From);
---------------------------------------------------------------------------
-- Next_Word_Break — True Platinum postcondition
---------------------------------------------------------------------------
procedure Next_Word_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_WB_From (Text, Pos)
and then Next_Pos > Pos
and then Next_Pos <= Text'Last + 1;
end Lingenic_Text.Words;