TEXT SEGMENTATION MODULES
=========================
Standards: UAX #29 (Graphemes, Words, Sentences), UAX #14 (Line Break)
OVERVIEW
--------
Four modules implement Unicode text segmentation as forward state
machines over UTF-8 text. Each finds the next boundary position in
a byte array:
Graphemes Next_Grapheme_Cluster_Break UAX #29 grapheme clusters
Words Next_Word_Break UAX #29 word boundaries
Sentences Next_Sentence_Break UAX #29 sentence boundaries
Line_Break Next_Line_Break UAX #14 line break opportunities
All four follow the same architecture:
1. Ghost _Spec encodes individual rules as expression functions
2. Ghost recursive function simulates the complete algorithm
3. Implementation is a forward state machine
4. Postcondition: implementation output = ghost recursive function
None require their own Initialize -- they use Properties directly.
Properties.Initialized is a precondition on each public procedure.
COMMON PATTERN
--------------
Each module has:
*_spec.ads Ghost specification (Pure, Ghost):
Abstract property value constants
Individual rule functions (GB3, WB5, SB8, LB14, etc.)
Composite decision function (Is_Grapheme_Break, etc.)
State transition functions
*.ads Public API:
State record for the state machine
Ghost helper functions (Ghost_CP, Ghost_GBP, etc.)
Recursive ghost function (Next_GCB, Next_WB, etc.)
Top-level ghost wrapper (Next_GCB_From, etc.)
Public procedure with Platinum postcondition
*.adb Implementation:
Forward loop over bytes
UTF-8 decode at each position
Property lookup + abstract value mapping
State update + break decision
Loop invariant connecting to ghost function
GRAPHEME CLUSTERS (UAX #29)
----------------------------
Files: src/lingenic_text-graphemes_spec.ads
src/lingenic_text-graphemes.ads
src/lingenic_text-graphemes.adb
Abstract Property Values:
GBP_Value (0..13):
GBP_Other (0), GBP_CR (1), GBP_LF (2), GBP_Control (3),
GBP_Extend (4), GBP_ZWJ (5), GBP_Regional_Indicator (6),
GBP_Prepend (7), GBP_SpacingMark (8), GBP_L (9), GBP_V (10),
GBP_T (11), GBP_LV (12), GBP_LVT (13)
InCB_Value (0..3):
InCB_None (0), InCB_Consonant (1), InCB_Linker (2), InCB_Extend (3)
Conjunct_State: CS_None, CS_Consonant, CS_Linker
Rules Encoded:
GB3: CR x LF (no break between CR and LF)
GB4: (Control|CR|LF) / (break after control)
GB5: / (Control|CR|LF) (break before control)
GB6-GB8: Hangul syllable jamo sequences
GB9: x (Extend|ZWJ) (no break before extending)
GB9a: x SpacingMark
GB9b: Prepend x
GB9c: Indic conjunct sequences (Consonant [Ext|Link]* Linker ... x Consonant)
GB11: ExtPict Extend* ZWJ x ExtPict (emoji ZWJ sequences)
GB12/13: RI x RI (regional indicator pairs)
GB999: Otherwise, break everywhere
Composite Decision:
Is_Grapheme_Break(A_GBP, B_GBP, B_ExtPict, B_InCB,
In_ExtPict_Seq, RI_Count_Odd, In_Conjunct)
Evaluates rules in priority order. Returns True = break.
State Record (GCB_State):
Prev_GBP Previous codepoint's GBP value
Ext_Pict_Seq In ExtPict Extend* sequence (for GB11)
Conj_State Indic conjunct tracking (for GB9c)
RI_Count Count of consecutive Regional_Indicators (for GB12/13)
State Transitions:
Next_ExtPict_Seq(Prev, This_GBP, This_ExtPict)
True after ExtPict, stays True through Extend/ZWJ, resets otherwise.
Next_Conjunct_State(Prev, This_InCB)
Consonant -> CS_Consonant; Linker (if in consonant/linker) -> CS_Linker;
Extend (if in consonant/linker) -> keep; otherwise -> CS_None.
Public API:
procedure Next_Grapheme_Cluster_Break
(Text : Byte_Array;
Pos : Positive;
Next_Pos : out Positive);
Pre: Text'First = 1, Text'Last >= 1, Text'Last < Positive'Last,
Pos in Text'Range, Properties.Initialized
Post: Next_Pos = Next_GCB_From(Text, Pos)
Next_Pos > Pos
Next_Pos <= Text'Last + 1
Text(Pos .. Next_Pos - 1) is a complete grapheme cluster.
Invalid UTF-8 bytes are treated as single-codepoint clusters with
GBP = Other.
WORD SEGMENTATION (UAX #29)
-----------------------------
Files: src/lingenic_text-words_spec.ads
src/lingenic_text-words.ads
src/lingenic_text-words.adb
Abstract Property Values:
WBP_Value (0..18):
WBP_Other (0), WBP_CR (1), WBP_LF (2), WBP_Newline (3),
WBP_Extend (4), WBP_ZWJ (5), WBP_Regional_Indicator (6),
WBP_Format (7), WBP_Katakana (8), WBP_Hebrew_Letter (9),
WBP_ALetter (10), WBP_Single_Quote (11), WBP_Double_Quote (12),
WBP_MidNumLet (13), WBP_MidLetter (14), WBP_MidNum (15),
WBP_Numeric (16), WBP_ExtendNumLet (17), WBP_WSegSpace (18)
Key Complexity:
WB4 makes Extend/Format/ZWJ transparent: rules WB5-WB999 use the
"effective" previous character (the last non-transparent character).
The state machine tracks both Prev_Actual and Prev_Eff.
Lookahead rules (WB6, WB7, WB7b, WB12) scan forward past ignored
characters. Ghost_After_Found and Ghost_After_WBP encode these as
recursive ghost functions.
State Record (WB_State):
Prev_Actual Actual previous WBP value
Prev_Eff Effective previous WBP value (skipping Extend/Format/ZWJ)
Before_Prev_Eff Effective WBP before the effective previous
RI_Count Consecutive Regional_Indicator count
Public API:
procedure Next_Word_Break
(Text : Byte_Array;
Pos : Positive;
Next_Pos : out Positive);
Post: Next_Pos = Next_WB_From(Text, Pos)
SENTENCE SEGMENTATION (UAX #29)
---------------------------------
Files: src/lingenic_text-sentences_spec.ads
src/lingenic_text-sentences.ads
src/lingenic_text-sentences.adb
Abstract Property Values:
SBP_Value (0..14):
SBP_Other (0), SBP_CR (1), SBP_LF (2), SBP_Sep (3),
SBP_Extend (4), SBP_Format (5), SBP_Sp (6), SBP_Lower (7),
SBP_Upper (8), SBP_OLetter (9), SBP_Numeric (10), SBP_ATerm (11),
SBP_STerm (12), SBP_SContinue (13), SBP_Close (14)
Key Complexity:
SA_State tracks the "SATerm Close* Sp*" lookbehind context needed
for rules SB8-SB11. States: SA_None, SA_Term, SA_Close, SA_Sp.
SB8 requires lookahead: scan forward past non-stopper characters
looking for a Lower. Ghost_SB8_Lower encodes this as a recursive
ghost function.
State Record (SB_State):
Prev_Actual Actual previous SBP value
Prev_Eff Effective previous (skipping Extend/Format)
Before_Prev_Eff Effective SBP before the effective previous
SA_St SATerm context state
SA_ATerm_Flag True if the SATerm was ATerm (not STerm)
Public API:
procedure Next_Sentence_Break
(Text : Byte_Array;
Pos : Positive;
Next_Pos : out Positive);
Post: Next_Pos = Next_SB_From(Text, Pos)
LINE BREAKING (UAX #14)
-------------------------
Files: src/lingenic_text-line_break_spec.ads
src/lingenic_text-line_break.ads
src/lingenic_text-line_break.adb
This is the most complex segmentation module.
Resolved LBP Values:
49 distinct classes after LB1 resolution:
Mandatory: BK, CR, LF, NL
Attached: CM, WJ, ZW
Closing: CL, CP, CP_EA, EX
Opening: OP, OP_EA
Quoting: QU, QU_Pi, QU_Pf
Numeric: IS, NU, PO, PR, SY
Alpha: AL, HL
Brahmic: AK, AP, AS, VF, VI
Emoji: EB, EM
Hangul: H2, H3, JL, JV, JT
Other: RI, ID, HH, SP, GL, B2, BA, BB, HY, CB, IN, NS, SA
LB1 resolution: AI/SG/XX -> AL, CJ -> NS, SA with Mn/Mc -> CM.
QU/OP/CP split by General_Category and East_Asian_Width.
Key Complexity:
LB9 absorption: CM/ZWJ transparent after most classes (X (CM|ZWJ)* -> X),
except after BK/CR/LF/NL/SP/ZW where remaining CM/ZWJ -> AL (LB10).
Rules with SP* tracking (LB8, LB14, LB15a, LB16, LB17): the
Before_SP state tracks the class before a run of SP characters.
NU context (LB25): tracks whether we're in a numeric context
(PR|PO OP? NU ... NU CL? CP? PR|PO).
Lookahead rules: LB15b, LB28a sub-rule 4.
State Record (LB_State):
Prev_Eff Effective previous LBP
Prev_Actual Actual previous LBP
Before_Prev_Eff Effective before effective previous
Before_SP Class before SP run
In_SP_Run Currently in a run of SP characters
RI_Count Consecutive RI count
QU_Pi_Context Tracking QU of type Pi
Prev_ExtPict_Cn Previous was ExtPict for LB30a context
Prev_Is_DC Dotted_Circle context
Before_Prev_DC DC context before previous
In_NU_Context In numeric context for LB25
Prev_Is_EA Previous was East_Asian for LB30
Before_Prev_EA EA context before previous
Public API:
procedure Next_Line_Break
(Text : Byte_Array;
Pos : Positive;
Next_Pos : out Positive);
Post: Next_Pos = Next_LB_From(Text, Pos)
USAGE PATTERN
-------------
To iterate over grapheme clusters in a UTF-8 byte array:
Pos := Text'First;
while Pos <= Text'Last loop
Next_Grapheme_Cluster_Break (Text, Pos, Next_Pos);
-- Text(Pos .. Next_Pos - 1) is one grapheme cluster
Pos := Next_Pos;
end loop;
The same pattern applies to all four segmentation modules.