-- 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
--
-- Line break segmentation (UAX #14).
--
-- Implements the Unicode Line Breaking Algorithm as a forward state
-- machine over UTF-8 text. Each call to Next_Line_Break returns the
-- byte position of the next line break opportunity.
--
-- The algorithm uses resolved LBP values (after LB1 resolution and
-- QU/OP/CP splits) from the Properties module. The ghost specification
-- in Line_Break_Spec encodes the individual rule predicates.
--
-- LB9 (combining mark absorption) makes CM/ZWJ transparent by
-- treating the sequence X (CM|ZWJ)* as X, except after BK/CR/LF/NL/SP/ZW.
-- LB10 treats remaining CM/ZWJ as AL.
--
-- SP* indirect break tracking (LB8, LB14, LB15a, LB16, LB17) uses
-- Before_SP state to remember the character before an SP run.
--
-- LB15b and LB28a sub-rule 4 use forward lookahead procedures.
--
-- Invalid UTF-8 bytes are treated as single-byte codepoints with
-- LBP = AL (via LB1 default for XX).
--
-- SPARK Platinum: the postcondition references the recursive ghost function
-- Next_LB_From, which simulates the algorithm as an expression function.
-- GNATprove verifies the implementation matches this specification.
-------------------------------------------------------------------------------
with Lingenic_Text.Properties;
with Lingenic_Text.Line_Break_Spec;
with Lingenic_Text.EAW_Spec;
with Lingenic_Text.UTF8_Spec;
package Lingenic_Text.Line_Break
with SPARK_Mode
is
---------------------------------------------------------------------------
-- Ghost state record for line break state machine
---------------------------------------------------------------------------
type LB_State is record
Prev_Eff : Line_Break_Spec.LBP_Value;
Prev_Actual : Line_Break_Spec.LBP_Value;
Before_Prev_Eff : Line_Break_Spec.LBP_Value;
Before_SP : Line_Break_Spec.LBP_Value;
In_SP_Run : Boolean;
RI_Count : Natural;
QU_Pi_Context : Boolean;
Prev_ExtPict_Cn : Boolean;
Prev_Is_DC : Boolean;
Before_Prev_DC : Boolean;
In_NU_Context : Boolean;
Prev_Is_EA : Boolean;
Before_Prev_EA : 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;
function Ghost_Valid
(Text : Byte_Array;
Cur : Positive) return Boolean
is (UTF8_Spec.Well_Formed_At (Text, Cur))
with Ghost,
Pre => Text'First = 1
and then Text'Last >= 1
and then Text'Last < Positive'Last
and then Cur in Text'Range;
-- LBP value at Cur (invalid → LBP_AL per LB1/LB10).
function Ghost_LBP
(Text : Byte_Array;
Cur : Positive) return Line_Break_Spec.LBP_Value
is (if UTF8_Spec.Well_Formed_At (Text, Cur)
then Properties.Get_LBP (UTF8_Spec.Decoded_At (Text, Cur))
else Line_Break_Spec.LBP_AL)
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;
-- Is dotted circle (U+25CC)?
function Ghost_Is_DC
(Text : Byte_Array;
Cur : Positive) return Boolean
is (Ghost_Valid (Text, Cur) and then Ghost_CP (Text, Cur) = 16#25CC#)
with Ghost,
Pre => Text'First = 1
and then Text'Last >= 1
and then Text'Last < Positive'Last
and then Cur in Text'Range;
-- Is East Asian (EAW ∈ {F,W,H})?
function Ghost_Is_EA
(Text : Byte_Array;
Cur : Positive) return Boolean
is (if Ghost_Valid (Text, Cur) then
(declare
Val : constant EAW_Spec.EAW_Value :=
Properties.EAW_To_Abstract
(Properties.Get_EAW (Ghost_CP (Text, Cur)));
begin
Val = EAW_Spec.EAW_Fullwidth
or Val = EAW_Spec.EAW_Wide
or Val = EAW_Spec.EAW_Halfwidth)
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;
-- Is ExtPict AND GC=Cn?
function Ghost_ExtPict_Cn
(Text : Byte_Array;
Cur : Positive) return Boolean
is (Ghost_Valid (Text, Cur)
and then Properties.Get_ExtPict (Ghost_CP (Text, Cur))
and then Properties.Get_GC (Ghost_CP (Text, Cur)) >= 1
and then Properties.Get_GC (Ghost_CP (Text, Cur))
<= Properties.GC_Name_Count
and then Properties.GC_Name
(Properties.Get_GC (Ghost_CP (Text, Cur))) = "Cn")
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 functions
---------------------------------------------------------------------------
-- LB15b: scan past CM/ZWJ for right context or eot
function Ghost_LB15b
(Text : Byte_Array;
From : Positive) return Boolean
is (if From not in Text'Range then True -- eot → applies
elsif not Line_Break_Spec.Is_CM_ZWJ (Ghost_LBP (Text, From))
then Line_Break_Spec.Is_LB15b_After (Ghost_LBP (Text, From))
elsif From > Text'Last - Ghost_Step_Length (Text, From) + 1 then True
else Ghost_LB15b (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);
-- LB15c: scan past CM/ZWJ for NU
function Ghost_LB15c
(Text : Byte_Array;
From : Positive) return Boolean
is (if From not in Text'Range then False
elsif not Line_Break_Spec.Is_CM_ZWJ (Ghost_LBP (Text, From))
then Ghost_LBP (Text, From) = Line_Break_Spec.LBP_NU
elsif From > Text'Last - Ghost_Step_Length (Text, From) + 1 then False
else Ghost_LB15c (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);
-- LB19a: scan past CM/ZWJ for non-EA or eot
function Ghost_LB19a_Non_EA
(Text : Byte_Array;
From : Positive) return Boolean
is (if From not in Text'Range then True -- eot → non-EA
elsif not Line_Break_Spec.Is_CM_ZWJ (Ghost_LBP (Text, From))
then (if Ghost_Valid (Text, From)
then not Ghost_Is_EA (Text, From)
else True) -- invalid → non-EA
elsif From > Text'Last - Ghost_Step_Length (Text, From) + 1 then True
else Ghost_LB19a_Non_EA
(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);
-- LB25 OP NU: scan past CM/ZWJ for NU or IS NU
-- Inner scan: after IS, skip CM/ZWJ and check for NU
function Ghost_LB25_Inner_NU
(Text : Byte_Array;
From : Positive) return Boolean
is (if From not in Text'Range then False
elsif not Line_Break_Spec.Is_CM_ZWJ (Ghost_LBP (Text, From))
then Ghost_LBP (Text, From) = Line_Break_Spec.LBP_NU
elsif From > Text'Last - Ghost_Step_Length (Text, From) + 1 then False
else Ghost_LB25_Inner_NU
(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);
-- Outer scan: past CM/ZWJ, check for NU or IS (then inner scan for NU)
function Ghost_LB25_OP_NU
(Text : Byte_Array;
From : Positive) return Boolean
is (if From not in Text'Range then False
elsif Line_Break_Spec.Is_CM_ZWJ (Ghost_LBP (Text, From)) then
(if From > Text'Last - Ghost_Step_Length (Text, From) + 1 then False
else Ghost_LB25_OP_NU
(Text, From + Ghost_Step_Length (Text, From)))
elsif Ghost_LBP (Text, From) = Line_Break_Spec.LBP_NU then True
elsif Ghost_LBP (Text, From) = Line_Break_Spec.LBP_IS then
(if From > Text'Last - Ghost_Step_Length (Text, From) + 1 then False
else Ghost_LB25_Inner_NU
(Text, From + Ghost_Step_Length (Text, From)))
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 From > 0
and then Properties.Initialized,
Subprogram_Variant => (Decreases => Text'Last - From + 1);
-- LB28a VF: scan past CM/ZWJ for VF
function Ghost_LB28a_VF
(Text : Byte_Array;
From : Positive) return Boolean
is (if From not in Text'Range then False
elsif not Line_Break_Spec.Is_CM_ZWJ (Ghost_LBP (Text, From))
then Ghost_LBP (Text, From) = Line_Break_Spec.LBP_VF
elsif From > Text'Last - Ghost_Step_Length (Text, From) + 1 then False
else Ghost_LB28a_VF (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: compute all lookahead results at Cur
---------------------------------------------------------------------------
-- Effective B after LB9/LB10
function Ghost_Eff_B
(St : LB_State;
Text : Byte_Array;
Cur : Positive) return Line_Break_Spec.LBP_Value
is (if Line_Break_Spec.Is_CM_ZWJ (Ghost_LBP (Text, Cur)) then
(if not Line_Break_Spec.Is_LB9_Exception (St.Prev_Eff)
then St.Prev_Eff -- LB9: absorbed
else Line_Break_Spec.LBP_AL) -- LB10: treat as AL
else Ghost_LBP (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;
-- Is LB9-absorbed?
function Ghost_Is_Absorbed
(St : LB_State;
Text : Byte_Array;
Cur : Positive) return Boolean
is (Line_Break_Spec.Is_CM_ZWJ (Ghost_LBP (Text, Cur))
and then not Line_Break_Spec.Is_LB9_Exception (St.Prev_Eff))
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;
-- This_Is_EA after LB10 override
function Ghost_This_EA
(St : LB_State;
Text : Byte_Array;
Cur : Positive) return Boolean
is (if Line_Break_Spec.Is_CM_ZWJ (Ghost_LBP (Text, Cur)) then
(if Line_Break_Spec.Is_LB9_Exception (St.Prev_Eff) then False
else Ghost_Is_EA (Text, Cur)) -- absorbed: keep EA
else Ghost_Is_EA (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 LB15b result at Cur
function Ghost_LB15b_At
(St : LB_State;
Text : Byte_Array;
Cur : Positive) return Boolean
is (if Ghost_Eff_B (St, Text, Cur) = Line_Break_Spec.LBP_QU_Pf then
(if Cur + Ghost_Step_Length (Text, Cur) <= Text'Last + 1
then Ghost_LB15b (Text, Cur + Ghost_Step_Length (Text, Cur))
else True)
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 LB15c result at Cur
function Ghost_LB15c_At
(St : LB_State;
Text : Byte_Array;
Cur : Positive) return Boolean
is (if St.Prev_Eff = Line_Break_Spec.LBP_SP
and Ghost_Eff_B (St, Text, Cur) = Line_Break_Spec.LBP_IS
then (if Cur + Ghost_Step_Length (Text, Cur) <= Text'Last + 1
then Ghost_LB15c (Text, Cur + Ghost_Step_Length (Text, Cur))
else False)
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 LB19a result at Cur
function Ghost_LB19a_At
(St : LB_State;
Text : Byte_Array;
Cur : Positive) return Boolean
is (if Line_Break_Spec.Is_QU (Ghost_Eff_B (St, Text, Cur))
and St.Prev_Is_EA
then (if Cur + Ghost_Step_Length (Text, Cur) <= Text'Last + 1
then Ghost_LB19a_Non_EA
(Text, Cur + Ghost_Step_Length (Text, Cur))
else True)
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 LB25 OP result at Cur
function Ghost_LB25_OP_At
(St : LB_State;
Text : Byte_Array;
Cur : Positive) return Boolean
is (if (St.Prev_Eff = Line_Break_Spec.LBP_PO
or St.Prev_Eff = Line_Break_Spec.LBP_PR)
and Line_Break_Spec.Is_OP (Ghost_Eff_B (St, Text, Cur))
then (if Cur + Ghost_Step_Length (Text, Cur) <= Text'Last + 1
then Ghost_LB25_OP_NU
(Text, Cur + Ghost_Step_Length (Text, Cur))
else False)
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 LB28a VF result at Cur
function Ghost_LB28a_VF_At
(St : LB_State;
Text : Byte_Array;
Cur : Positive) return Boolean
is (if Line_Break_Spec.LB28a_Sub4_Prefix
(St.Prev_Eff, St.Prev_Is_DC,
Ghost_Eff_B (St, Text, Cur), Ghost_Is_DC (Text, Cur))
then (if Cur + Ghost_Step_Length (Text, Cur) <= Text'Last + 1
then Ghost_LB28a_VF
(Text, Cur + Ghost_Step_Length (Text, Cur))
else False)
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
---------------------------------------------------------------------------
function Ghost_Break
(St : LB_State;
Text : Byte_Array;
Cur : Positive) return Boolean
is (if Ghost_Is_Absorbed (St, Text, Cur) then False
elsif Line_Break_Spec.Is_Hard_Break (St.Prev_Actual)
and then not Line_Break_Spec.LB5_CRLF
(St.Prev_Actual, Ghost_Eff_B (St, Text, Cur))
then True
else Line_Break_Spec.Is_Allow_Break
(Prev_Actual => St.Prev_Actual,
Prev_Eff => St.Prev_Eff,
Eff_B => Ghost_Eff_B (St, Text, Cur),
Before_Prev_Eff => St.Before_Prev_Eff,
In_SP_Run => St.In_SP_Run,
Before_SP => St.Before_SP,
QU_Pi_Ctx => St.QU_Pi_Context,
LB15b_Res => Ghost_LB15b_At (St, Text, Cur),
LB15c_Res => Ghost_LB15c_At (St, Text, Cur),
In_NU_Ctx => St.In_NU_Context,
LB25_OP_Res => Ghost_LB25_OP_At (St, Text, Cur),
LB28a_VF_Res => Ghost_LB28a_VF_At (St, Text, Cur),
Prev_Is_EA => St.Prev_Is_EA,
This_Is_EA => Ghost_This_EA (St, Text, Cur),
Before_Prev_EA => St.Before_Prev_EA,
Prev_Is_DC => St.Prev_Is_DC,
This_Is_DC => Ghost_Is_DC (Text, Cur),
Before_Prev_DC => St.Before_Prev_DC,
Prev_ExtPict_Cn => St.Prev_ExtPict_Cn,
RI_Count => St.RI_Count,
LB19a_Res => Ghost_LB19a_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
---------------------------------------------------------------------------
-- Ghost QU_Pi context update
function Ghost_Next_QU_Pi
(St : LB_State;
Eff_B : Line_Break_Spec.LBP_Value) return Boolean
is (if Eff_B = Line_Break_Spec.LBP_QU_Pi then
(if Line_Break_Spec.Is_LB15a_Before (St.Prev_Eff) then True
elsif St.In_SP_Run
and Line_Break_Spec.Is_LB15a_Before (St.Before_SP)
then True
else St.QU_Pi_Context)
elsif Eff_B /= Line_Break_Spec.LBP_SP then False
else St.QU_Pi_Context)
with Ghost;
-- Ghost NU context update
function Ghost_Next_NU_Ctx
(St : LB_State;
Eff_B : Line_Break_Spec.LBP_Value) return Boolean
is (if Eff_B = Line_Break_Spec.LBP_NU then True
elsif St.In_NU_Context
and (Eff_B = Line_Break_Spec.LBP_SY
or Eff_B = Line_Break_Spec.LBP_IS)
then True
elsif St.In_NU_Context
and (Eff_B = Line_Break_Spec.LBP_CL
or Line_Break_Spec.Is_CP (Eff_B))
then True
else False)
with Ghost;
-- Ghost SP tracking update
function Ghost_Next_In_SP
(Eff_B : Line_Break_Spec.LBP_Value) return Boolean
is (Eff_B = Line_Break_Spec.LBP_SP)
with Ghost;
function Ghost_Next_Before_SP
(St : LB_State;
Eff_B : Line_Break_Spec.LBP_Value) return Line_Break_Spec.LBP_Value
is (if Eff_B = Line_Break_Spec.LBP_SP then
(if not St.In_SP_Run then St.Prev_Eff else St.Before_SP)
else St.Before_SP)
with Ghost;
-- Full state update for absorbed case (LB9)
function Updated_State_Absorbed
(St : LB_State;
Text : Byte_Array;
Cur : Positive) return LB_State
is (LB_State'
(Prev_Eff => St.Prev_Eff,
Prev_Actual => Ghost_LBP (Text, Cur),
Before_Prev_Eff => St.Before_Prev_Eff,
Before_SP => St.Before_SP,
In_SP_Run => St.In_SP_Run,
RI_Count => St.RI_Count,
QU_Pi_Context => St.QU_Pi_Context,
Prev_ExtPict_Cn => St.Prev_ExtPict_Cn,
Prev_Is_DC => St.Prev_Is_DC,
Before_Prev_DC => St.Before_Prev_DC,
In_NU_Context => St.In_NU_Context,
Prev_Is_EA => St.Prev_Is_EA,
Before_Prev_EA => St.Before_Prev_EA))
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;
-- Full state update for non-absorbed case
function Updated_State_Normal
(St : LB_State;
Text : Byte_Array;
Cur : Positive) return LB_State
is (declare
Eff_B : constant Line_Break_Spec.LBP_Value :=
Ghost_Eff_B (St, Text, Cur);
begin
LB_State'
(Prev_Eff => Eff_B,
Prev_Actual => Ghost_LBP (Text, Cur),
Before_Prev_Eff => St.Prev_Eff,
Before_SP => Ghost_Next_Before_SP (St, Eff_B),
In_SP_Run => Ghost_Next_In_SP (Eff_B),
RI_Count =>
(if Eff_B = Line_Break_Spec.LBP_RI
then (if St.RI_Count < Natural'Last
then St.RI_Count + 1 else St.RI_Count)
else 0),
QU_Pi_Context => Ghost_Next_QU_Pi (St, Eff_B),
Prev_ExtPict_Cn => Ghost_ExtPict_Cn (Text, Cur),
Prev_Is_DC => Ghost_Is_DC (Text, Cur),
Before_Prev_DC => St.Prev_Is_DC,
In_NU_Context => Ghost_Next_NU_Ctx (St, Eff_B),
Prev_Is_EA => Ghost_This_EA (St, Text, Cur),
Before_Prev_EA => St.Prev_Is_EA))
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;
-- Combined update
function Updated_State
(St : LB_State;
Text : Byte_Array;
Cur : Positive) return LB_State
is (if Ghost_Is_Absorbed (St, Text, Cur)
then Updated_State_Absorbed (St, Text, Cur)
else Updated_State_Normal (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;
-- Initial state after first codepoint at Pos
function Initial_State
(Text : Byte_Array;
Pos : Positive) return LB_State
is (LB_State'
(Prev_Eff =>
(if Line_Break_Spec.Is_CM_ZWJ (Ghost_LBP (Text, Pos))
then Line_Break_Spec.LBP_AL
else Ghost_LBP (Text, Pos)),
Prev_Actual => Ghost_LBP (Text, Pos),
Before_Prev_Eff => Line_Break_Spec.LBP_Other,
Before_SP => Line_Break_Spec.LBP_Other,
In_SP_Run =>
(not Line_Break_Spec.Is_CM_ZWJ (Ghost_LBP (Text, Pos))
and then Ghost_LBP (Text, Pos) = Line_Break_Spec.LBP_SP),
RI_Count =>
(if Line_Break_Spec.Is_CM_ZWJ (Ghost_LBP (Text, Pos)) then 0
elsif Ghost_LBP (Text, Pos) = Line_Break_Spec.LBP_RI
then 1 else 0),
QU_Pi_Context =>
(not Line_Break_Spec.Is_CM_ZWJ (Ghost_LBP (Text, Pos))
and then Ghost_LBP (Text, Pos) = Line_Break_Spec.LBP_QU_Pi),
Prev_ExtPict_Cn =>
(if Line_Break_Spec.Is_CM_ZWJ (Ghost_LBP (Text, Pos))
then False
else Ghost_ExtPict_Cn (Text, Pos)),
Prev_Is_DC =>
(Ghost_Valid (Text, Pos)
and then Ghost_CP (Text, Pos) = 16#25CC#),
Before_Prev_DC => False,
In_NU_Context =>
(not Line_Break_Spec.Is_CM_ZWJ (Ghost_LBP (Text, Pos))
and then Ghost_LBP (Text, Pos) = Line_Break_Spec.LBP_NU),
Prev_Is_EA =>
(not Line_Break_Spec.Is_CM_ZWJ (Ghost_LBP (Text, Pos))
and then Ghost_Valid (Text, Pos)
and then Ghost_Is_EA (Text, Pos)),
Before_Prev_EA => False))
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_LB
(Text : Byte_Array;
Cur : Positive;
St : LB_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_LB (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
---------------------------------------------------------------------------
function Next_LB_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_LB (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_Line_Break — True Platinum postcondition
---------------------------------------------------------------------------
procedure Next_Line_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_LB_From (Text, Pos)
and then Next_Pos > Pos
and then Next_Pos <= Text'Last + 1;
end Lingenic_Text.Line_Break;