-- 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
--
-- Ghost specification for sentence break rules (UAX #29).
--
-- Defines abstract property values, the SA_State type for tracking
-- SATerm Close* Sp* lookbehind sequences, and the break decision function.
-- Each SB rule is a named expression function. The composite
-- Is_Sentence_Break encodes the full rule priority chain.
--
-- SB5 (ignore rule) makes Extend/Format transparent for rules
-- SB6–SB998. The state machine tracks "effective" previous characters
-- (the last non-Extend/Format char) for those rules.
-- Rules SB3–SB4 are evaluated before SB5 and use actual characters.
--
-- SB8–SB11 use SA_State lookbehind to track whether the effective
-- history matches the pattern SATerm Close* Sp*.
-------------------------------------------------------------------------------
package Lingenic_Text.Sentences_Spec
with SPARK_Mode, Pure
is
---------------------------------------------------------------------------
-- Abstract Sentence_Break property values
--
-- These are abstract constants used in the specification.
-- The Properties package maps runtime-discovered indices to these
-- values at initialization time.
---------------------------------------------------------------------------
SBP_Other : constant := 0;
SBP_CR : constant := 1;
SBP_LF : constant := 2;
SBP_Sep : constant := 3;
SBP_Extend : constant := 4;
SBP_Format : constant := 5;
SBP_Sp : constant := 6;
SBP_Lower : constant := 7;
SBP_Upper : constant := 8;
SBP_OLetter : constant := 9;
SBP_Numeric : constant := 10;
SBP_ATerm : constant := 11;
SBP_STerm : constant := 12;
SBP_SContinue : constant := 13;
SBP_Close : constant := 14;
subtype SBP_Value is Natural range 0 .. 14;
---------------------------------------------------------------------------
-- SA_State — tracks SATerm Close* Sp* lookbehind sequence
--
-- Used by rules SB8, SB8a, SB9, SB10, SB11 which all require
-- knowing whether the effective history matches this pattern.
---------------------------------------------------------------------------
type SA_State is (SA_None, SA_Term, SA_Close, SA_Sp);
---------------------------------------------------------------------------
-- Macro predicates
---------------------------------------------------------------------------
-- ParaSep = Sep | CR | LF
function Is_ParaSep (V : SBP_Value) return Boolean
is (V = SBP_Sep or V = SBP_CR or V = SBP_LF);
-- SATerm = ATerm | STerm
function Is_SATerm (V : SBP_Value) return Boolean
is (V = SBP_ATerm or V = SBP_STerm);
-- Characters ignored by SB5
function Is_Ignored (V : SBP_Value) return Boolean
is (V = SBP_Extend or V = SBP_Format);
-- SB8 stoppers: characters that block the SB8 lookahead scan.
-- If any of these appear before a Lower, SB8 does not apply.
function Is_SB8_Stopper (V : SBP_Value) return Boolean
is (V = SBP_OLetter or V = SBP_Upper
or Is_ParaSep (V) or Is_SATerm (V));
---------------------------------------------------------------------------
-- Individual SB rules
--
-- Parameters use these conventions:
-- A = actual previous character SBP (for rules before SB5)
-- A_Eff = effective previous character SBP (SB5-adjusted)
-- B = current character SBP
-- Bef = effective character before A (two effective chars back)
-- SA = SATerm sequence state (lookbehind for SB8-SB11)
-- SA_ATerm = whether the SATerm was ATerm (vs STerm)
-- SB8_Found = SB8 lookahead found a Lower character
---------------------------------------------------------------------------
-- SB3: CR × LF
function SB3_Applies (A, B : SBP_Value) return Boolean
is (A = SBP_CR and B = SBP_LF);
-- SB4: ParaSep ÷
function SB4_Applies (A : SBP_Value) return Boolean
is (Is_ParaSep (A));
-- SB5 is handled inline in Is_Sentence_Break:
-- Extend/Format are ignored (no break before them) when not after ParaSep.
-- SB6: ATerm × Numeric
function SB6_Applies (A_Eff, B : SBP_Value) return Boolean
is (A_Eff = SBP_ATerm and B = SBP_Numeric);
-- SB7: (Upper | Lower) ATerm × Upper
-- A_Eff is ATerm, Bef (lookbehind) must be Upper or Lower.
function SB7_Applies (Bef, A_Eff, B : SBP_Value) return Boolean
is ((Bef = SBP_Upper or Bef = SBP_Lower)
and A_Eff = SBP_ATerm
and B = SBP_Upper);
-- SB8: ATerm Close* Sp* × (¬(OLetter|Upper|Lower|ParaSep|SATerm))* Lower
-- Uses SA_State to check "ATerm Close* Sp*" lookbehind.
-- SA_ATerm distinguishes ATerm from STerm.
-- SB8_Found is the lookahead result (or B = Lower for immediate match).
function SB8_Applies
(SA : SA_State;
SA_ATerm : Boolean;
B : SBP_Value;
SB8_Found : Boolean) return Boolean
is (SA in SA_Term | SA_Close | SA_Sp
and then SA_ATerm
and then (B = SBP_Lower
or else (not Is_SB8_Stopper (B) and then SB8_Found)));
-- SB8a: SATerm Close* Sp* × (SContinue | SATerm)
function SB8a_Applies (SA : SA_State; B : SBP_Value) return Boolean
is (SA in SA_Term | SA_Close | SA_Sp
and then (B = SBP_SContinue or Is_SATerm (B)));
-- SB9: SATerm Close* × (Close | Sp | ParaSep)
-- Note: SA_Sp is NOT included — only SA_Term and SA_Close.
function SB9_Applies (SA : SA_State; B : SBP_Value) return Boolean
is (SA in SA_Term | SA_Close
and then (B = SBP_Close or B = SBP_Sp or Is_ParaSep (B)));
-- SB10: SATerm Close* Sp* × (Sp | ParaSep)
function SB10_Applies (SA : SA_State; B : SBP_Value) return Boolean
is (SA in SA_Term | SA_Close | SA_Sp
and then (B = SBP_Sp or Is_ParaSep (B)));
-- SB11: SATerm Close* Sp* ParaSep? ÷
-- The ParaSep? part is handled by SB9/SB10 absorbing ParaSep,
-- then SB4 breaking after it. SB11 fires when in the SATerm
-- sequence and no earlier rule prevented the break.
function SB11_Applies (SA : SA_State) return Boolean
is (SA in SA_Term | SA_Close | SA_Sp);
---------------------------------------------------------------------------
-- Composite break decision (SB3–SB998 in priority order)
--
-- SB1 (break at sot) and SB2 (break at eot) are handled by the
-- caller — they concern text boundaries, not pair properties.
--
-- A_Actual = literal previous character (for SB3, SB4)
-- A_Eff = effective previous character after SB5 (for SB6+)
-- B_SBP = current character
-- Before_A = effective character before A (for SB7)
-- SA = SATerm sequence state (for SB8–SB11)
-- SA_ATerm = was the SATerm specifically ATerm? (for SB8)
-- SB8_Found = SB8 lookahead found Lower
---------------------------------------------------------------------------
function Is_Sentence_Break
(A_Actual : SBP_Value;
A_Eff : SBP_Value;
B_SBP : SBP_Value;
Before_A : SBP_Value;
SA : SA_State;
SA_ATerm : Boolean;
SB8_Found : Boolean) return Boolean
is (if SB3_Applies (A_Actual, B_SBP) then False
elsif SB4_Applies (A_Actual) then True
-- SB5: Extend/Format are ignored (transparent) after non-ParaSep.
elsif Is_Ignored (B_SBP) and not Is_ParaSep (A_Eff) then False
elsif SB6_Applies (A_Eff, B_SBP) then False
elsif SB7_Applies (Before_A, A_Eff, B_SBP) then False
elsif SB8_Applies (SA, SA_ATerm, B_SBP, SB8_Found) then False
elsif SB8a_Applies (SA, B_SBP) then False
elsif SB9_Applies (SA, B_SBP) then False
elsif SB10_Applies (SA, B_SBP) then False
elsif SB11_Applies (SA) then True
else False); -- SB998: Otherwise, do not break
end Lingenic_Text.Sentences_Spec;