-- 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 word break rules (UAX #29).
--
-- Defines abstract property values and the break decision function.
-- Each WB rule is a named expression function. The composite
-- Is_Word_Break encodes the full rule priority chain.
--
-- WB4 (ignore rule) makes Extend/Format/ZWJ transparent for rules
-- WB5–WB999. The state machine tracks "effective" previous characters
-- (the last non-Extend/Format/ZWJ char) for those rules.
-- Rules WB3–WB3d are evaluated before WB4 and use actual characters.
-------------------------------------------------------------------------------
package Lingenic_Text.Words_Spec
with SPARK_Mode, Pure
is
---------------------------------------------------------------------------
-- Abstract Word_Break property values
--
-- These are abstract constants used in the specification.
-- The Properties package maps runtime-discovered indices to these
-- values at initialization time.
---------------------------------------------------------------------------
WBP_Other : constant := 0;
WBP_CR : constant := 1;
WBP_LF : constant := 2;
WBP_Newline : constant := 3;
WBP_Extend : constant := 4;
WBP_ZWJ : constant := 5;
WBP_Regional_Indicator : constant := 6;
WBP_Format : constant := 7;
WBP_Katakana : constant := 8;
WBP_Hebrew_Letter : constant := 9;
WBP_ALetter : constant := 10;
WBP_Single_Quote : constant := 11;
WBP_Double_Quote : constant := 12;
WBP_MidNumLet : constant := 13;
WBP_MidLetter : constant := 14;
WBP_MidNum : constant := 15;
WBP_Numeric : constant := 16;
WBP_ExtendNumLet : constant := 17;
WBP_WSegSpace : constant := 18;
subtype WBP_Value is Natural range 0 .. 18;
---------------------------------------------------------------------------
-- Macro predicates
---------------------------------------------------------------------------
-- AHLetter = ALetter | Hebrew_Letter
function Is_AHLetter (V : WBP_Value) return Boolean
is (V = WBP_ALetter or V = WBP_Hebrew_Letter);
-- MidNumLetQ = MidNumLet | Single_Quote
function Is_MidNumLetQ (V : WBP_Value) return Boolean
is (V = WBP_MidNumLet or V = WBP_Single_Quote);
-- Characters ignored by WB4
function Is_Ignored (V : WBP_Value) return Boolean
is (V = WBP_Extend or V = WBP_Format or V = WBP_ZWJ);
-- Characters after which WB4 does NOT apply
-- (sot is handled separately by the caller)
function Is_Newline_Or_CRLF (V : WBP_Value) return Boolean
is (V = WBP_CR or V = WBP_LF or V = WBP_Newline);
-- MidLetter or MidNumLetQ (for WB6/WB7)
function Is_MidLetter_Or_MidNumLetQ (V : WBP_Value) return Boolean
is (V = WBP_MidLetter or Is_MidNumLetQ (V));
-- MidNum or MidNumLetQ (for WB11/WB12)
function Is_MidNum_Or_MidNumLetQ (V : WBP_Value) return Boolean
is (V = WBP_MidNum or Is_MidNumLetQ (V));
---------------------------------------------------------------------------
-- Individual WB rules
--
-- Parameters use these conventions:
-- A = actual previous character WBP (for rules before WB4)
-- A_Eff = effective previous character WBP (WB4-adjusted)
-- B = current character WBP
-- Bef = effective character before A (two effective chars back)
-- Aft = effective character after B (lookahead past ignored)
---------------------------------------------------------------------------
-- WB3: CR × LF
function WB3_Applies (A, B : WBP_Value) return Boolean
is (A = WBP_CR and B = WBP_LF);
-- WB3a: (Newline | CR | LF) ÷
function WB3a_Applies (A : WBP_Value) return Boolean
is (A = WBP_Newline or A = WBP_CR or A = WBP_LF);
-- WB3b: ÷ (Newline | CR | LF)
function WB3b_Applies (B : WBP_Value) return Boolean
is (B = WBP_Newline or B = WBP_CR or B = WBP_LF);
-- WB3c: ZWJ × \p{Extended_Pictographic}
-- Uses actual A (ZWJ), not effective A.
function WB3c_Applies (A : WBP_Value; B_ExtPict : Boolean) return Boolean
is (A = WBP_ZWJ and B_ExtPict);
-- WB3d: WSegSpace × WSegSpace
-- Uses actual A and B (listed before WB4).
function WB3d_Applies (A, B : WBP_Value) return Boolean
is (A = WBP_WSegSpace and B = WBP_WSegSpace);
-- WB5: AHLetter × AHLetter
function WB5_Applies (A_Eff, B : WBP_Value) return Boolean
is (Is_AHLetter (A_Eff) and Is_AHLetter (B));
-- WB6: AHLetter × (MidLetter | MidNumLetQ) AHLetter
-- B is a mid character, Aft (lookahead) must be AHLetter.
function WB6_Applies
(A_Eff, B : WBP_Value;
Aft : WBP_Value;
Has_Aft : Boolean) return Boolean
is (Is_AHLetter (A_Eff)
and Is_MidLetter_Or_MidNumLetQ (B)
and Has_Aft and Is_AHLetter (Aft));
-- WB7: AHLetter (MidLetter | MidNumLetQ) × AHLetter
-- A_Eff is a mid character, Bef (lookbehind) must be AHLetter.
function WB7_Applies
(Bef, A_Eff, B : WBP_Value) return Boolean
is (Is_AHLetter (Bef)
and Is_MidLetter_Or_MidNumLetQ (A_Eff)
and Is_AHLetter (B));
-- WB7a: Hebrew_Letter × Single_Quote
function WB7a_Applies (A_Eff, B : WBP_Value) return Boolean
is (A_Eff = WBP_Hebrew_Letter and B = WBP_Single_Quote);
-- WB7b: Hebrew_Letter × Double_Quote Hebrew_Letter
-- B is Double_Quote, Aft (lookahead) must be Hebrew_Letter.
function WB7b_Applies
(A_Eff, B : WBP_Value;
Aft : WBP_Value;
Has_Aft : Boolean) return Boolean
is (A_Eff = WBP_Hebrew_Letter
and B = WBP_Double_Quote
and Has_Aft and Aft = WBP_Hebrew_Letter);
-- WB7c: Hebrew_Letter Double_Quote × Hebrew_Letter
-- A_Eff is Double_Quote, Bef (lookbehind) must be Hebrew_Letter.
function WB7c_Applies
(Bef, A_Eff, B : WBP_Value) return Boolean
is (Bef = WBP_Hebrew_Letter
and A_Eff = WBP_Double_Quote
and B = WBP_Hebrew_Letter);
-- WB8: Numeric × Numeric
function WB8_Applies (A_Eff, B : WBP_Value) return Boolean
is (A_Eff = WBP_Numeric and B = WBP_Numeric);
-- WB9: AHLetter × Numeric
function WB9_Applies (A_Eff, B : WBP_Value) return Boolean
is (Is_AHLetter (A_Eff) and B = WBP_Numeric);
-- WB10: Numeric × AHLetter
function WB10_Applies (A_Eff, B : WBP_Value) return Boolean
is (A_Eff = WBP_Numeric and Is_AHLetter (B));
-- WB11: Numeric (MidNum | MidNumLetQ) × Numeric
-- A_Eff is a mid character, Bef (lookbehind) must be Numeric.
function WB11_Applies
(Bef, A_Eff, B : WBP_Value) return Boolean
is (Bef = WBP_Numeric
and Is_MidNum_Or_MidNumLetQ (A_Eff)
and B = WBP_Numeric);
-- WB12: Numeric × (MidNum | MidNumLetQ) Numeric
-- B is a mid character, Aft (lookahead) must be Numeric.
function WB12_Applies
(A_Eff, B : WBP_Value;
Aft : WBP_Value;
Has_Aft : Boolean) return Boolean
is (A_Eff = WBP_Numeric
and Is_MidNum_Or_MidNumLetQ (B)
and Has_Aft and Aft = WBP_Numeric);
-- WB13: Katakana × Katakana
function WB13_Applies (A_Eff, B : WBP_Value) return Boolean
is (A_Eff = WBP_Katakana and B = WBP_Katakana);
-- WB13a: (AHLetter | Numeric | Katakana | ExtendNumLet) × ExtendNumLet
function WB13a_Applies (A_Eff, B : WBP_Value) return Boolean
is ((Is_AHLetter (A_Eff)
or A_Eff = WBP_Numeric
or A_Eff = WBP_Katakana
or A_Eff = WBP_ExtendNumLet)
and B = WBP_ExtendNumLet);
-- WB13b: ExtendNumLet × (AHLetter | Numeric | Katakana)
function WB13b_Applies (A_Eff, B : WBP_Value) return Boolean
is (A_Eff = WBP_ExtendNumLet
and (Is_AHLetter (B)
or B = WBP_Numeric
or B = WBP_Katakana));
-- WB15/WB16: RI pairing — same pattern as GB12/13
-- sot (RI RI)* RI × RI / [^RI] (RI RI)* RI × RI
-- No break when the number of preceding RI is odd.
function WB15_16_Applies
(A_Eff : WBP_Value;
B : WBP_Value;
RI_Count_Odd : Boolean) return Boolean
is (A_Eff = WBP_Regional_Indicator
and B = WBP_Regional_Indicator
and RI_Count_Odd);
---------------------------------------------------------------------------
-- Composite break decision (WB3–WB999 in priority order)
--
-- WB1 (break at sot) and WB2 (break at eot) are handled by the
-- caller — they concern text boundaries, not pair properties.
--
-- A_Actual = literal previous character (for WB3, WB3a, WB3c, WB3d)
-- A_Eff = effective previous character after WB4 (for WB5+)
-- B_WBP = current character
-- B_ExtPict = is current character Extended_Pictographic?
-- Before_A = effective character before A (for WB7, WB7c, WB11)
-- After_B = effective character after B (for WB6, WB7b, WB12)
-- Has_After = was lookahead successful?
-- RI_Count_Odd = odd # of preceding RI in cluster
---------------------------------------------------------------------------
function Is_Word_Break
(A_Actual : WBP_Value;
A_Eff : WBP_Value;
B_WBP : WBP_Value;
B_ExtPict : Boolean;
Before_A : WBP_Value;
After_B : WBP_Value;
Has_After : Boolean;
RI_Count_Odd : Boolean) return Boolean
is (if WB3_Applies (A_Actual, B_WBP) then False
elsif WB3a_Applies (A_Actual) then True
elsif WB3b_Applies (B_WBP) then True
elsif WB3c_Applies (A_Actual, B_ExtPict) then False
elsif WB3d_Applies (A_Actual, B_WBP) then False
-- WB4: Extend/Format/ZWJ are ignored after non-newline chars.
-- Effect: no break before Extend/Format/ZWJ (unless after CRLF).
elsif Is_Ignored (B_WBP) and not Is_Newline_Or_CRLF (A_Eff)
then False
elsif WB5_Applies (A_Eff, B_WBP) then False
elsif WB6_Applies (A_Eff, B_WBP, After_B, Has_After) then False
elsif WB7_Applies (Before_A, A_Eff, B_WBP) then False
elsif WB7a_Applies (A_Eff, B_WBP) then False
elsif WB7b_Applies (A_Eff, B_WBP, After_B, Has_After) then False
elsif WB7c_Applies (Before_A, A_Eff, B_WBP) then False
elsif WB8_Applies (A_Eff, B_WBP) then False
elsif WB9_Applies (A_Eff, B_WBP) then False
elsif WB10_Applies (A_Eff, B_WBP) then False
elsif WB11_Applies (Before_A, A_Eff, B_WBP) then False
elsif WB12_Applies (A_Eff, B_WBP, After_B, Has_After) then False
elsif WB13_Applies (A_Eff, B_WBP) then False
elsif WB13a_Applies (A_Eff, B_WBP) then False
elsif WB13b_Applies (A_Eff, B_WBP) then False
elsif WB15_16_Applies (A_Eff, B_WBP, RI_Count_Odd) then False
else True); -- WB999: Otherwise, break everywhere
end Lingenic_Text.Words_Spec;