-- 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 grapheme cluster break rules (UAX #29).
--
-- Defines abstract property values and the break decision function.
-- Each GB rule is a named ghost expression function. The composite
-- Is_Grapheme_Break encodes the full rule priority chain.
-------------------------------------------------------------------------------
package Lingenic_Text.Graphemes_Spec
with SPARK_Mode, Pure
is
---------------------------------------------------------------------------
-- Abstract Grapheme_Cluster_Break property values
--
-- These are abstract constants used in the ghost specification.
-- The Properties package maps runtime-discovered indices to these
-- values at initialization time.
---------------------------------------------------------------------------
GBP_Other : constant := 0;
GBP_CR : constant := 1;
GBP_LF : constant := 2;
GBP_Control : constant := 3;
GBP_Extend : constant := 4;
GBP_ZWJ : constant := 5;
GBP_Regional_Indicator : constant := 6;
GBP_Prepend : constant := 7;
GBP_SpacingMark : constant := 8;
GBP_L : constant := 9;
GBP_V : constant := 10;
GBP_T : constant := 11;
GBP_LV : constant := 12;
GBP_LVT : constant := 13;
subtype GBP_Value is Natural range 0 .. 13;
---------------------------------------------------------------------------
-- Abstract Indic_Conjunct_Break property values
---------------------------------------------------------------------------
InCB_None : constant := 0;
InCB_Consonant : constant := 1;
InCB_Linker : constant := 2;
InCB_Extend : constant := 3;
subtype InCB_Value is Natural range 0 .. 3;
---------------------------------------------------------------------------
-- Indic conjunct state for GB9c
---------------------------------------------------------------------------
type Conjunct_State is (CS_None, CS_Consonant, CS_Linker);
---------------------------------------------------------------------------
-- Individual GB rules
---------------------------------------------------------------------------
-- GB3: CR × LF
function GB3_Applies (A, B : GBP_Value) return Boolean
is (A = GBP_CR and B = GBP_LF);
-- GB4: (Control | CR | LF) ÷
function GB4_Applies (A : GBP_Value) return Boolean
is (A = GBP_Control or A = GBP_CR or A = GBP_LF);
-- GB5: ÷ (Control | CR | LF)
function GB5_Applies (B : GBP_Value) return Boolean
is (B = GBP_Control or B = GBP_CR or B = GBP_LF);
-- GB6: L × (L | V | LV | LVT)
function GB6_Applies (A, B : GBP_Value) return Boolean
is (A = GBP_L and (B = GBP_L or B = GBP_V or B = GBP_LV or B = GBP_LVT));
-- GB7: (LV | V) × (V | T)
function GB7_Applies (A, B : GBP_Value) return Boolean
is ((A = GBP_LV or A = GBP_V) and (B = GBP_V or B = GBP_T));
-- GB8: (LVT | T) × T
function GB8_Applies (A, B : GBP_Value) return Boolean
is ((A = GBP_LVT or A = GBP_T) and B = GBP_T);
-- GB9: × (Extend | ZWJ)
function GB9_Applies (B : GBP_Value) return Boolean
is (B = GBP_Extend or B = GBP_ZWJ);
-- GB9a: × SpacingMark
function GB9a_Applies (B : GBP_Value) return Boolean
is (B = GBP_SpacingMark);
-- GB9b: Prepend ×
function GB9b_Applies (A : GBP_Value) return Boolean
is (A = GBP_Prepend);
-- GB9c: \p{InCB=Consonant} [\p{InCB=Extend}\p{InCB=Linker}]*
-- \p{InCB=Linker} [\p{InCB=Extend}\p{InCB=Linker}]* × \p{InCB=Consonant}
--
-- In_Conjunct is True when the context state is CS_Linker, meaning
-- we have seen Consonant [Ext|Link]* Linker [Ext|Link]*.
function GB9c_Applies
(In_Conjunct : Boolean;
B_InCB : InCB_Value) return Boolean
is (In_Conjunct and B_InCB = InCB_Consonant);
-- GB11: \p{ExtPict} Extend* ZWJ × \p{ExtPict}
--
-- In_ExtPict_Seq is True when we have seen ExtPict followed by
-- zero or more Extend characters. The break point is between
-- the ZWJ (A_GBP = GBP_ZWJ) and an ExtPict codepoint.
function GB11_Applies
(In_ExtPict_Seq : Boolean;
A_GBP : GBP_Value;
B_ExtPict : Boolean) return Boolean
is (In_ExtPict_Seq and A_GBP = GBP_ZWJ and B_ExtPict);
-- GB12/GB13: sot (RI RI)* RI × RI / [^RI] (RI RI)* RI × RI
--
-- No break when the number of preceding RI in the cluster is odd.
function GB12_13_Applies
(A_GBP : GBP_Value;
B_GBP : GBP_Value;
RI_Count_Odd : Boolean) return Boolean
is (A_GBP = GBP_Regional_Indicator
and B_GBP = GBP_Regional_Indicator
and RI_Count_Odd);
---------------------------------------------------------------------------
-- Composite break decision (GB3–GB999 in priority order)
--
-- GB1 (break at sot) and GB2 (break at eot) are handled by the
-- caller — they concern text boundaries, not pair properties.
---------------------------------------------------------------------------
function Is_Grapheme_Break
(A_GBP : GBP_Value;
B_GBP : GBP_Value;
B_ExtPict : Boolean;
B_InCB : InCB_Value;
In_ExtPict_Seq : Boolean;
RI_Count_Odd : Boolean;
In_Conjunct : Boolean) return Boolean
is (if GB3_Applies (A_GBP, B_GBP) then False
elsif GB4_Applies (A_GBP) then True
elsif GB5_Applies (B_GBP) then True
elsif GB6_Applies (A_GBP, B_GBP) then False
elsif GB7_Applies (A_GBP, B_GBP) then False
elsif GB8_Applies (A_GBP, B_GBP) then False
elsif GB9_Applies (B_GBP) then False
elsif GB9a_Applies (B_GBP) then False
elsif GB9b_Applies (A_GBP) then False
elsif GB9c_Applies (In_Conjunct, B_InCB) then False
elsif GB11_Applies (In_ExtPict_Seq, A_GBP, B_ExtPict) then False
elsif GB12_13_Applies (A_GBP, B_GBP, RI_Count_Odd) then False
else True); -- GB999: Otherwise, break everywhere
---------------------------------------------------------------------------
-- State machine transition for ExtPict sequence tracking
--
-- ext_pict_seq tracks whether we are in ExtPict Extend* context.
-- True after seeing ExtPict, stays True through Extend, reset otherwise.
-- After ZWJ it stays True (ExtPict Extend* ZWJ is a valid prefix).
---------------------------------------------------------------------------
function Next_ExtPict_Seq
(Prev : Boolean;
This_GBP : GBP_Value;
This_ExtPict : Boolean) return Boolean
is (if This_ExtPict then True
elsif Prev and (This_GBP = GBP_Extend or This_GBP = GBP_ZWJ) then True
else False);
---------------------------------------------------------------------------
-- State machine transition for Indic conjunct tracking
---------------------------------------------------------------------------
function Next_Conjunct_State
(Prev : Conjunct_State;
This_InCB : InCB_Value) return Conjunct_State
is (case This_InCB is
when InCB_Consonant => CS_Consonant,
when InCB_Linker =>
(if Prev = CS_Consonant or Prev = CS_Linker
then CS_Linker else CS_None),
when InCB_Extend =>
(if Prev = CS_Consonant or Prev = CS_Linker
then Prev else CS_None),
when InCB_None => CS_None);
end Lingenic_Text.Graphemes_Spec;