-- 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 — Graphemes body
--
-- Forward state machine for grapheme cluster boundary detection (UAX #29).
--
-- Decodes UTF-8, looks up GBP/ExtPict/InCB properties, maintains state
-- for GB9c (Indic conjunct), GB11 (ExtPict+ZWJ), GB12/13 (RI pairs),
-- and applies the composite break decision from the ghost spec.
--
-- Invalid UTF-8 bytes are treated as single-byte codepoints with
-- GBP = Other, ExtPict = False, InCB = None.
--
-- SPARK Platinum: the loop invariant connects runtime state to the
-- recursive ghost function Next_GCB, establishing that the returned
-- position equals Next_GCB_From(Text, Pos).
-------------------------------------------------------------------------------
with Lingenic_Text.UTF8;
with Lingenic_Text.UCD_Parser;
package body Lingenic_Text.Graphemes
with SPARK_Mode
is
-- RI counter upper bound. Text'Last < Positive'Last (precondition),
-- so the number of RI codepoints can never exceed Text'Last.
-- We use a generous upper bound to keep the invariant simple.
Max_RI : constant := Natural'Last - 1;
subtype RI_Counter is Natural range 0 .. Max_RI;
procedure Next_Grapheme_Cluster_Break
(Text : Byte_Array;
Pos : Positive;
Next_Pos : out Positive)
is
use Graphemes_Spec;
-- First codepoint in cluster (GB1: always start new cluster)
First_CP : Codepoint;
First_Len : Positive;
First_Valid : Boolean;
First_GBP : UCD_Parser.Property_Index;
First_ExtPict : Boolean;
First_InCB : UCD_Parser.Property_Index;
-- State variables
Prev_GBP : GBP_Value;
Ext_Pict_Seq : Boolean;
Conj_State : Conjunct_State;
RI_Count : RI_Counter;
-- Current position in text
Cur : Positive;
begin
-- Decode first codepoint (GB1: sot ÷)
UTF8.Decode (Text, Pos, First_CP, First_Len, First_Valid);
-- Platinum: First_Len = Ghost_Step_Length (Text, Pos)
-- From UTF8.Decode postcondition:
-- First_Valid = Well_Formed_At(Text, Pos)
-- If valid: First_Len = Lead_Length(Text(Pos))
-- If invalid: First_Len = 1
-- Ghost_Step_Length matches this exactly.
pragma Assert (First_Len = Ghost_Step_Length (Text, Pos));
-- Advance past first codepoint
-- First_Len >= 1, so Pos + First_Len > Pos always.
-- If this reaches or exceeds the end of text, return (GB2: ÷ eot).
if Pos > Text'Last - First_Len + 1 then
Next_Pos := Pos + First_Len;
-- Platinum: Next_Pos = Pos + Ghost_Step_Length(Text, Pos)
-- = Next_GCB_From(Text, Pos) when first CP reaches end.
pragma Assert (Next_Pos = Next_GCB_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_GBP := Properties.Get_GBP (First_CP);
First_ExtPict := Properties.Get_ExtPict (First_CP);
First_InCB := Properties.Get_InCB (First_CP);
else
First_GBP := 0; -- Default -> GBP_Other
First_ExtPict := False;
First_InCB := 0; -- Default -> InCB_None
end if;
-- Initialize state
Prev_GBP := Properties.GBP_To_Abstract (First_GBP);
Ext_Pict_Seq := Next_ExtPict_Seq
(False, Prev_GBP, First_ExtPict);
Conj_State := Next_Conjunct_State
(CS_None, Properties.InCB_To_Abstract (First_InCB));
RI_Count := (if Prev_GBP = GBP_Regional_Indicator then 1 else 0);
-- Platinum: connect runtime decoded CP to ghost decoded CP.
-- UTF8.Decode postcondition: First_Valid = Well_Formed_At(Text, Pos)
-- and if valid: First_CP = Decoded_At(Text, Pos).
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.
-- Each step: runtime lookup via First_CP = ghost lookup via Ghost_CP.
pragma Assert (Prev_GBP = Ghost_GBP (Text, Pos));
pragma Assert (First_ExtPict = Ghost_ExtPict (Text, Pos));
pragma Assert
(Properties.InCB_To_Abstract (First_InCB) = Ghost_InCB (Text, Pos));
-- Platinum: connect composite initial state to ghost Initial_State.
pragma Assert (Ext_Pict_Seq = Initial_State (Text, Pos).Ext_Pict_Seq);
pragma Assert (Conj_State = Initial_State (Text, Pos).Conj_State);
pragma Assert (RI_Count = Initial_State (Text, Pos).RI_Count);
-- Platinum: establish base case for the accumulator invariant.
-- Next_GCB_From unfolds to Next_GCB(Text, Pos + step, Initial_State(..))
-- when Pos <= Text'Last - step + 1.
pragma Assert
(Next_GCB (Text, Cur,
GCB_State'(Prev_GBP, Ext_Pict_Seq, Conj_State, RI_Count))
= Next_GCB_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_GCB (Text, Cur,
GCB_State'(Prev_GBP, Ext_Pict_Seq,
Conj_State, RI_Count))
= Next_GCB_From (Text, Pos));
pragma Loop_Variant (Increases => Cur);
declare
This_CP : Codepoint;
This_Len : Positive;
This_Valid : Boolean;
This_GBP_Idx : UCD_Parser.Property_Index;
This_ExtPict : Boolean;
This_InCB_Idx : UCD_Parser.Property_Index;
This_GBP : GBP_Value;
This_InCB : InCB_Value;
Is_Break : Boolean;
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_GBP_Idx := Properties.Get_GBP (This_CP);
This_ExtPict := Properties.Get_ExtPict (This_CP);
This_InCB_Idx := Properties.Get_InCB (This_CP);
else
This_GBP_Idx := 0;
This_ExtPict := False;
This_InCB_Idx := 0;
end if;
This_GBP := Properties.GBP_To_Abstract (This_GBP_Idx);
This_InCB := Properties.InCB_To_Abstract (This_InCB_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_GBP = Ghost_GBP (Text, Cur));
pragma Assert (This_ExtPict = Ghost_ExtPict (Text, Cur));
pragma Assert (This_InCB = Ghost_InCB (Text, Cur));
-- Apply composite break decision
Is_Break := Is_Grapheme_Break
(A_GBP => Prev_GBP,
B_GBP => This_GBP,
B_ExtPict => This_ExtPict,
B_InCB => This_InCB,
In_ExtPict_Seq => Ext_Pict_Seq,
RI_Count_Odd => RI_Count mod 2 = 1,
In_Conjunct => Conj_State = CS_Linker);
-- Platinum: Is_Break = Ghost_Break with current state.
pragma Assert
(Is_Break = Ghost_Break
(GCB_State'(Prev_GBP, Ext_Pict_Seq,
Conj_State, RI_Count),
Text, Cur));
if Is_Break then
Next_Pos := Cur;
-- Platinum: Next_GCB returns Cur when Ghost_Break is true.
-- Combined with the accumulator invariant, this gives us
-- Next_Pos = Next_GCB_From(Text, Pos).
pragma Assert (Next_Pos = Next_GCB_From (Text, Pos));
return;
end if;
-- No break: update state and continue
-- Update ExtPict sequence state
Ext_Pict_Seq := Next_ExtPict_Seq
(Ext_Pict_Seq, This_GBP, This_ExtPict);
-- Update Indic conjunct state
Conj_State := Next_Conjunct_State
(Conj_State, This_InCB);
-- Update RI count
if This_GBP = GBP_Regional_Indicator then
if RI_Count < Max_RI - 1 then
RI_Count := RI_Count + 1;
end if;
else
RI_Count := 0;
end if;
-- Update previous GBP
Prev_GBP := This_GBP;
-- Advance position
if Cur > Text'Last - This_Len + 1 then
-- This codepoint reaches end of text
Next_Pos := Cur + This_Len;
-- Platinum: Next_GCB returns Cur + step when past end,
-- Ghost_Break is false (checked above).
pragma Assert (Next_Pos = Next_GCB_From (Text, Pos));
return;
end if;
Cur := Cur + This_Len;
end;
end loop;
-- Reached end of text (GB2: ÷ eot)
-- This can happen when Cur = Text'Last + 1 after advancing.
Next_Pos := Text'Last + 1;
-- Platinum: Cur not in Text'Range, so Next_GCB returns Cur
-- (which equals Text'Last + 1).
pragma Assert (Next_Pos = Next_GCB_From (Text, Pos));
end Next_Grapheme_Cluster_Break;
end Lingenic_Text.Graphemes;