-- 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 line break rules (UAX #14).
--
-- Defines resolved Line_Break property values (after LB1 resolution),
-- macro predicates, and the break decision function.
--
-- LB1 resolution is performed at init time:
-- AI, SG, XX → AL; CJ → NS; SA + Mn/Mc → CM, SA + other → AL
-- QU split into QU, QU_Pi, QU_Pf based on General_Category
-- OP split into OP, OP_EA based on East_Asian_Width ∈ {F,W,H}
-- CP split into CP, CP_EA based on East_Asian_Width ∈ {F,W,H}
--
-- LB9 (combining mark absorption) makes CM and ZWJ transparent:
-- X (CM|ZWJ)* → X (where X ∉ {BK, CR, LF, NL, SP, ZW})
-- LB10: remaining CM/ZWJ → AL
--
-- Rules with SP* patterns (LB8, LB14, LB15a, LB16, LB17) use
-- Before_SP state tracking. LB15b and LB28a use forward lookahead.
-------------------------------------------------------------------------------
package Lingenic_Text.Line_Break_Spec
with SPARK_Mode, Pure
is
---------------------------------------------------------------------------
-- Resolved Line_Break property values
--
-- These values incorporate LB1 resolution and the QU/OP/CP splits.
-- The state machine works exclusively with these resolved values.
---------------------------------------------------------------------------
LBP_Other : constant := 0; -- Default / unrecognized
-- Mandatory breaks and control
LBP_BK : constant := 1; -- Mandatory Break
LBP_CR : constant := 2; -- Carriage Return
LBP_LF : constant := 3; -- Line Feed
LBP_NL : constant := 4; -- Next Line
LBP_CM : constant := 5; -- Combining Mark (includes SA→CM)
LBP_WJ : constant := 6; -- Word Joiner
LBP_ZW : constant := 7; -- Zero Width Space
LBP_GL : constant := 8; -- Non-breaking "Glue"
LBP_SP : constant := 9; -- Space
LBP_ZWJ : constant := 10; -- Zero Width Joiner
-- Break opportunities
LBP_B2 : constant := 11; -- Break Opportunity Before and After
LBP_BA : constant := 12; -- Break After
LBP_BB : constant := 13; -- Break Before
LBP_HY : constant := 14; -- Hyphen
LBP_CB : constant := 15; -- Contingent Break
-- Closing/opening punctuation
LBP_CL : constant := 16; -- Close Punctuation
LBP_CP : constant := 17; -- Close Parenthesis (non-EA)
LBP_CP_EA : constant := 18; -- Close Parenthesis (EA F/W/H)
LBP_EX : constant := 19; -- Exclamation/Interrogation
LBP_IN : constant := 20; -- Inseparable
LBP_NS : constant := 21; -- Nonstarter (includes CJ→NS)
LBP_OP : constant := 22; -- Open Punctuation (non-EA)
LBP_OP_EA : constant := 23; -- Open Punctuation (EA F/W/H)
LBP_QU : constant := 24; -- Quotation (neither Pi nor Pf)
LBP_QU_Pi : constant := 25; -- Quotation + Initial Punctuation
LBP_QU_Pf : constant := 26; -- Quotation + Final Punctuation
-- Numeric context
LBP_IS : constant := 27; -- Infix Numeric Separator
LBP_NU : constant := 28; -- Numeric
LBP_PO : constant := 29; -- Postfix Numeric
LBP_PR : constant := 30; -- Prefix Numeric
LBP_SY : constant := 31; -- Symbols Allowing Break After
-- Alphabetic
LBP_AL : constant := 32; -- Alphabetic (includes AI/SG/XX/SA→AL)
LBP_HL : constant := 33; -- Hebrew Letter
-- Brahmic scripts
LBP_AK : constant := 34; -- Aksara
LBP_AP : constant := 35; -- Aksara Pre-Base
LBP_AS : constant := 36; -- Aksara Start
LBP_VF : constant := 37; -- Virama Final
LBP_VI : constant := 38; -- Virama
-- Emoji
LBP_EB : constant := 39; -- Emoji Base
LBP_EM : constant := 40; -- Emoji Modifier
-- Hangul
LBP_H2 : constant := 41; -- Hangul LV Syllable
LBP_H3 : constant := 42; -- Hangul LVT Syllable
LBP_JL : constant := 43; -- Hangul L Jamo
LBP_JV : constant := 44; -- Hangul V Jamo
LBP_JT : constant := 45; -- Hangul T Jamo
-- Other
LBP_RI : constant := 46; -- Regional Indicator
LBP_ID : constant := 47; -- Ideographic
LBP_HH : constant := 48; -- Unambiguous Hyphen (Unicode 17.0)
subtype LBP_Value is Natural range 0 .. 48;
---------------------------------------------------------------------------
-- Macro predicates
---------------------------------------------------------------------------
-- Characters that cause mandatory breaks (LB4/LB5)
function Is_Hard_Break (V : LBP_Value) return Boolean
is (V = LBP_BK or V = LBP_CR or V = LBP_LF or V = LBP_NL);
-- CM or ZWJ (absorbed by LB9)
function Is_CM_ZWJ (V : LBP_Value) return Boolean
is (V = LBP_CM or V = LBP_ZWJ);
-- Characters where CM/ZWJ is NOT absorbed (LB9 exception)
function Is_LB9_Exception (V : LBP_Value) return Boolean
is (V = LBP_BK or V = LBP_CR or V = LBP_LF
or V = LBP_NL or V = LBP_SP or V = LBP_ZW);
-- AL or HL (alphabetic)
function Is_Alpha (V : LBP_Value) return Boolean
is (V = LBP_AL or V = LBP_HL);
-- Any QU variant
function Is_QU (V : LBP_Value) return Boolean
is (V = LBP_QU or V = LBP_QU_Pi or V = LBP_QU_Pf);
-- Any OP variant
function Is_OP (V : LBP_Value) return Boolean
is (V = LBP_OP or V = LBP_OP_EA);
-- Any CP variant
function Is_CP (V : LBP_Value) return Boolean
is (V = LBP_CP or V = LBP_CP_EA);
-- Aksara-like for LB28a: AK or AS
function Is_AK_AS (V : LBP_Value) return Boolean
is (V = LBP_AK or V = LBP_AS);
-- LB15a: valid context before QU_Pi
-- sot | BK | CR | LF | NL | OP | QU | GL | SP | ZW
function Is_LB15a_Before (V : LBP_Value) return Boolean
is (Is_Hard_Break (V) or Is_OP (V) or Is_QU (V)
or V = LBP_GL or V = LBP_SP or V = LBP_ZW);
-- LB15b: valid context after QU_Pf
-- SP | GL | WJ | CL | QU | CP | EX | IS | SY | BK | CR | LF | NL | ZW
function Is_LB15b_After (V : LBP_Value) return Boolean
is (V = LBP_SP or V = LBP_GL or V = LBP_WJ
or V = LBP_CL or Is_QU (V) or Is_CP (V)
or V = LBP_EX or V = LBP_IS or V = LBP_SY
or Is_Hard_Break (V) or V = LBP_ZW);
---------------------------------------------------------------------------
-- The state machine evaluates rules procedurally in priority order
-- using these individual rule predicates. This spec provides the
-- predicates; the implementation applies them in sequence.
--
-- The composite Is_Allow_Break ghost function at the end of this
-- package encodes the full if-elsif chain, enabling Platinum proofs.
---------------------------------------------------------------------------
-- LB4/LB5: Always break after hard line breaks.
-- CR × LF (LB5 first clause), then CR/LF/NL/BK cause break.
function LB5_CRLF (A, B : LBP_Value) return Boolean
is (A = LBP_CR and B = LBP_LF);
-- LB6: × (BK | CR | LF | NL)
function LB6_Applies (B : LBP_Value) return Boolean
is (Is_Hard_Break (B));
-- LB7: × SP, × ZW
function LB7_Applies (B : LBP_Value) return Boolean
is (B = LBP_SP or B = LBP_ZW);
-- LB11: × WJ, WJ ×
function LB11_Before (B : LBP_Value) return Boolean
is (B = LBP_WJ);
function LB11_After (A : LBP_Value) return Boolean
is (A = LBP_WJ);
-- LB12: GL ×
function LB12_Applies (A : LBP_Value) return Boolean
is (A = LBP_GL);
-- LB12a: [^SP BA HY HH] × GL
function LB12a_Applies (A, B : LBP_Value) return Boolean
is (B = LBP_GL
and then A /= LBP_SP
and then A /= LBP_BA
and then A /= LBP_HY
and then A /= LBP_HH);
-- LB13: × CL, × CP, × EX, × SY
-- (IS was moved to LB15d in Unicode 16.0; SY added)
function LB13_Applies (B : LBP_Value) return Boolean
is (B = LBP_CL or Is_CP (B) or B = LBP_EX or B = LBP_SY);
-- LB15c: SP ÷ IS NU (break before decimal mark after space)
-- Checked in state machine via lookahead: if A=SP and B=IS,
-- look ahead to see if next effective char is NU.
-- LB15d: × IS (don't break before IS, unless LB15c applies)
function LB15d_Applies (B : LBP_Value) return Boolean
is (B = LBP_IS);
-- LB19: × [QU - Pi], [QU - Pf] ×
-- Don't break before non-initial QU (QU or QU_Pf), and
-- don't break after non-final QU (QU only — QU_Pi × is handled
-- context-sensitively by LB19a).
--
-- × [QU - Pi] = × QU ∪ × QU_Pf (unconditional)
-- [QU - Pf] × = QU × (QU_Pi is handled by LB19a, not here)
function LB19_Before (B : LBP_Value) return Boolean
is (B = LBP_QU or B = LBP_QU_Pf);
function LB19_After (A : LBP_Value) return Boolean
is (A = LBP_QU);
-- LB19a: East Asian QU context
-- [^$EA] × QU, × QU ([^$EA] | eot), QU × [^$EA], (sot | [^$EA]) QU ×
-- A_Is_EA and B_Is_EA are the East Asian Width flags for A and B.
-- Applied in state machine as four sub-checks.
-- LB20: ÷ CB, CB ÷
function LB20_Before (B : LBP_Value) return Boolean
is (B = LBP_CB);
function LB20_After (A : LBP_Value) return Boolean
is (A = LBP_CB);
-- LB20a: (sot|BK|CR|LF|NL|SP|ZW|CB|GL) (HY|HH) × (AL|HL)
-- Before_A is the context before A; A = HY or HH; B = AL or HL
function Is_LB20a_Before (V : LBP_Value) return Boolean
is (V = LBP_Other -- sot
or Is_Hard_Break (V) or V = LBP_SP or V = LBP_ZW
or V = LBP_CB or V = LBP_GL);
function LB20a_Applies (Before_A, A, B : LBP_Value) return Boolean
is (Is_LB20a_Before (Before_A)
and then (A = LBP_HY or A = LBP_HH)
and then Is_Alpha (B));
-- LB21: × BA, × HY, × HH, × NS, BB ×
function LB21_Applies (A, B : LBP_Value) return Boolean
is (B = LBP_BA or B = LBP_HY or B = LBP_HH or B = LBP_NS
or A = LBP_BB);
-- LB21a: HL (HY | HH) × [^HL]
-- Before_A = HL, A = HY or HH, B ≠ HL → no break
function LB21a_Applies (Before_A, A, B : LBP_Value) return Boolean
is (Before_A = LBP_HL
and then (A = LBP_HY or A = LBP_HH)
and then B /= LBP_HL);
-- LB21b: SY × HL
function LB21b_Applies (A, B : LBP_Value) return Boolean
is (A = LBP_SY and B = LBP_HL);
-- LB22: × IN
function LB22_Applies (B : LBP_Value) return Boolean
is (B = LBP_IN);
-- LB23: (AL|HL) × NU, NU × (AL|HL)
function LB23_Applies (A, B : LBP_Value) return Boolean
is ((Is_Alpha (A) and B = LBP_NU)
or (A = LBP_NU and Is_Alpha (B)));
-- LB23a: PR × (ID|EB|EM), (ID|EB|EM) × PO
function LB23a_Applies (A, B : LBP_Value) return Boolean
is ((A = LBP_PR and (B = LBP_ID or B = LBP_EB or B = LBP_EM))
or ((A = LBP_ID or A = LBP_EB or A = LBP_EM) and B = LBP_PO));
-- LB24: (PR|PO) × (AL|HL), (AL|HL) × (PR|PO)
function LB24_Applies (A, B : LBP_Value) return Boolean
is (((A = LBP_PR or A = LBP_PO) and Is_Alpha (B))
or (Is_Alpha (A) and (B = LBP_PR or B = LBP_PO)));
-- LB25: Do not break numbers (Unicode 16.0+ context-sensitive rules)
--
-- The state machine tracks In_NU_Context = True when in NU (SY|IS)*.
-- Rules use this context plus pair checks and forward lookahead.
--
-- NU (SY|IS)* CL × PO — In_NU_Context ∧ A∈{CL} ∧ B=PO
-- NU (SY|IS)* CP × PO — In_NU_Context ∧ A∈{CP} ∧ B=PO
-- NU (SY|IS)* CL × PR — In_NU_Context ∧ A∈{CL} ∧ B=PR
-- NU (SY|IS)* CP × PR — In_NU_Context ∧ A∈{CP} ∧ B=PR
-- NU (SY|IS)* × PO — In_NU_Context ∧ B=PO
-- NU (SY|IS)* × PR — In_NU_Context ∧ B=PR
-- PO × OP NU — A=PO ∧ B∈{OP} ∧ lookahead NU
-- PO × OP IS NU — A=PO ∧ B∈{OP} ∧ lookahead IS NU
-- PO × NU — A=PO ∧ B=NU
-- PR × OP NU — A=PR ∧ B∈{OP} ∧ lookahead NU
-- PR × OP IS NU — A=PR ∧ B∈{OP} ∧ lookahead IS NU
-- PR × NU — A=PR ∧ B=NU
-- HY × NU — A=HY ∧ B=NU
-- IS × NU — A=IS ∧ B=NU
-- NU (SY|IS)* × NU — In_NU_Context ∧ B=NU
--
-- Simplified: the state machine checks these procedurally.
-- Context-independent pair rules (no lookbehind/lookahead needed):
function LB25_Simple (A, B : LBP_Value) return Boolean
is ((A = LBP_PO and B = LBP_NU)
or (A = LBP_PR and B = LBP_NU)
or (A = LBP_HY and B = LBP_NU)
or (A = LBP_IS and B = LBP_NU));
-- Context-dependent rules needing In_NU_Context:
function LB25_NU_Context (A, B : LBP_Value;
In_NU : Boolean) return Boolean
is (In_NU
and then ((A = LBP_CL and (B = LBP_PO or B = LBP_PR))
or (Is_CP (A) and (B = LBP_PO or B = LBP_PR))
or B = LBP_PO
or B = LBP_PR
or B = LBP_NU));
-- PO/PR × OP rules need lookahead for NU (or IS NU).
-- Checked in state machine via forward scan.
-- LB26: Korean syllable rules
function LB26_Applies (A, B : LBP_Value) return Boolean
is ((A = LBP_JL and (B = LBP_JL or B = LBP_JV or B = LBP_H2 or B = LBP_H3))
or ((A = LBP_JV or A = LBP_H2) and (B = LBP_JV or B = LBP_JT))
or ((A = LBP_JT or A = LBP_H3) and B = LBP_JT));
-- LB27: Korean syllable + PO/PR
function LB27_Applies (A, B : LBP_Value) return Boolean
is (((A = LBP_JL or A = LBP_JV or A = LBP_JT
or A = LBP_H2 or A = LBP_H3) and B = LBP_PO)
or (A = LBP_PR and (B = LBP_JL or B = LBP_JV or B = LBP_JT
or B = LBP_H2 or B = LBP_H3)));
-- LB28: (AL|HL) × (AL|HL)
function LB28_Applies (A, B : LBP_Value) return Boolean
is (Is_Alpha (A) and Is_Alpha (B));
-- LB28a: Brahmic orthographic syllable rules
-- The spec uses [◌] (U+25CC DOTTED CIRCLE) alongside AK and AS.
-- Since ◌ has LB class AL, it needs explicit DC (dotted circle) flags.
--
-- Sub-rule 1: AP × (AK | ◌ | AS)
-- Sub-rule 2: (AK | ◌ | AS) × (VF | VI)
-- Sub-rule 3: (AK | ◌ | AS) VI × (AK | ◌)
-- Sub-rule 4: (AK | ◌ | AS) × (AK | ◌ | AS) VF
function LB28a_Sub1 (A : LBP_Value;
B : LBP_Value; B_DC : Boolean) return Boolean
is (A = LBP_AP and (Is_AK_AS (B) or B_DC));
function LB28a_Sub2 (A : LBP_Value; A_DC : Boolean;
B : LBP_Value) return Boolean
is ((Is_AK_AS (A) or A_DC) and (B = LBP_VF or B = LBP_VI));
function LB28a_Sub3 (Before_A : LBP_Value; Before_A_DC : Boolean;
A, B : LBP_Value; B_DC : Boolean) return Boolean
is ((Is_AK_AS (Before_A) or Before_A_DC)
and A = LBP_VI and (B = LBP_AK or B_DC));
-- Sub-rule 4: (AK|◌|AS) × (AK|◌|AS) VF — requires lookahead for VF
function LB28a_Sub4_Prefix (A : LBP_Value; A_DC : Boolean;
B : LBP_Value; B_DC : Boolean) return Boolean
is ((Is_AK_AS (A) or A_DC) and (Is_AK_AS (B) or B_DC));
-- LB29: IS × (AL|HL)
function LB29_Applies (A, B : LBP_Value) return Boolean
is (A = LBP_IS and Is_Alpha (B));
-- LB30: (AL|HL|NU) × OP (non-EA), CP (non-EA) × (AL|HL|NU)
function LB30_Applies (A, B : LBP_Value) return Boolean
is (((Is_Alpha (A) or A = LBP_NU) and B = LBP_OP)
or (A = LBP_CP and (Is_Alpha (B) or B = LBP_NU)));
-- LB30a: RI pairing (even count → no break)
function LB30a_Applies (A, B : LBP_Value;
RI_Count_Odd : Boolean) return Boolean
is (A = LBP_RI and B = LBP_RI and RI_Count_Odd);
-- LB30b: EB × EM, or (ExtPict ∪ Cn) × EM
-- ExtPict_Or_Cn is computed at runtime from ExtPict table + GC
function LB30b_Applies (A, B : LBP_Value;
A_ExtPict_Or_Cn : Boolean) return Boolean
is (B = LBP_EM and then (A = LBP_EB or A_ExtPict_Or_Cn));
---------------------------------------------------------------------------
-- Composite ghost function: Allow_Break decision
--
-- Encodes the full if-elsif rule chain from the state machine body.
-- Given all state variables and pre-computed lookahead results, returns
-- True when the rules allow a break (LB31 default or explicit ÷).
--
-- Mandatory breaks (LB4/LB5) are handled separately — this function
-- is only called when Prev_Actual is NOT a hard break (or is CR+LF).
--
-- Parameters match the local variables at the decision point in the body.
---------------------------------------------------------------------------
function Is_Allow_Break
(Prev_Actual : LBP_Value;
Prev_Eff : LBP_Value;
Eff_B : LBP_Value;
Before_Prev_Eff : LBP_Value;
In_SP_Run : Boolean;
Before_SP : LBP_Value;
QU_Pi_Ctx : Boolean;
LB15b_Res : Boolean;
LB15c_Res : Boolean;
In_NU_Ctx : Boolean;
LB25_OP_Res : Boolean;
LB28a_VF_Res : Boolean;
Prev_Is_EA : Boolean;
This_Is_EA : Boolean;
Before_Prev_EA : Boolean;
Prev_Is_DC : Boolean;
This_Is_DC : Boolean;
Before_Prev_DC : Boolean;
Prev_ExtPict_Cn : Boolean;
RI_Count : Natural;
LB19a_Res : Boolean) return Boolean
is (-- LB5: CR × LF → no break
if LB5_CRLF (Prev_Actual, Eff_B) then False
-- LB6: × (BK | CR | LF | NL)
elsif LB6_Applies (Eff_B) then False
-- LB7: × SP, × ZW
elsif LB7_Applies (Eff_B) then False
-- LB8: ZW SP* ÷
elsif In_SP_Run and Before_SP = LBP_ZW then True
elsif (not In_SP_Run) and Prev_Eff = LBP_ZW then True
-- LB8a: ZWJ ×
elsif Prev_Actual = LBP_ZWJ then False
-- LB11: × WJ, WJ ×
elsif LB11_Before (Eff_B) then False
elsif LB11_After (Prev_Eff) then False
-- LB12: GL ×
elsif LB12_Applies (Prev_Eff) then False
-- LB12a: [^SP BA HY HH] × GL
elsif LB12a_Applies (Prev_Eff, Eff_B) then False
-- LB13: × CL, × CP, × EX, × SY
elsif LB13_Applies (Eff_B) then False
-- LB14: OP SP* ×
elsif In_SP_Run and Is_OP (Before_SP) then False
elsif (not In_SP_Run) and Is_OP (Prev_Eff) then False
-- LB15a: QU_Pi_Context SP* ×
elsif In_SP_Run and QU_Pi_Ctx then False
elsif (not In_SP_Run) and QU_Pi_Ctx then False
-- LB15b: × QU_Pf (right context)
elsif LB15b_Res then False
-- LB15c/LB15d: SP × IS when followed by NU → break, else no break
elsif Prev_Eff = LBP_SP and Eff_B = LBP_IS then LB15c_Res
-- LB15d: × IS
elsif LB15d_Applies (Eff_B) then False
-- LB16: (CL | CP) SP* × NS
elsif In_SP_Run
and (Before_SP = LBP_CL or Is_CP (Before_SP))
and Eff_B = LBP_NS
then False
elsif (not In_SP_Run)
and (Prev_Eff = LBP_CL or Is_CP (Prev_Eff))
and Eff_B = LBP_NS
then False
-- LB17: B2 SP* × B2
elsif In_SP_Run and Before_SP = LBP_B2 and Eff_B = LBP_B2 then False
elsif (not In_SP_Run) and Prev_Eff = LBP_B2
and Eff_B = LBP_B2
then False
-- LB18: SP ÷
elsif Prev_Eff = LBP_SP then True
-- LB19: × [QU - Pi], [QU - Pf] ×
elsif LB19_Before (Eff_B) then False
elsif LB19_After (Prev_Eff) then False
-- LB19a: East Asian QU context (4 sub-checks)
-- [^$EA] × QU
elsif (not Prev_Is_EA) and Is_QU (Eff_B) then False
-- × QU ([^$EA] | eot) — Prev_Is_EA is true here
elsif Is_QU (Eff_B) then
(if LB19a_Res then False else True)
-- QU × [^$EA]
elsif Is_QU (Prev_Eff) and then (not This_Is_EA) then False
-- (sot | [^$EA]) QU ×
elsif Is_QU (Prev_Eff) then
(if Before_Prev_Eff = LBP_Other or (not Before_Prev_EA) then False
else True)
-- LB20: ÷ CB, CB ÷
elsif LB20_Before (Eff_B) then True
elsif LB20_After (Prev_Eff) then True
-- LB20a: (sot|BK|CR|LF|NL|SP|ZW|CB|GL) (HY|HH) × (AL|HL)
elsif LB20a_Applies (Before_Prev_Eff, Prev_Eff, Eff_B) then False
-- LB21: × BA, × HY, × HH, × NS, BB ×
elsif LB21_Applies (Prev_Eff, Eff_B) then False
-- LB21a: HL (HY | HH) × [^HL]
elsif LB21a_Applies (Before_Prev_Eff, Prev_Eff, Eff_B) then False
-- LB21b: SY × HL
elsif LB21b_Applies (Prev_Eff, Eff_B) then False
-- LB22: × IN
elsif LB22_Applies (Eff_B) then False
-- LB23: (AL|HL) × NU, NU × (AL|HL)
elsif LB23_Applies (Prev_Eff, Eff_B) then False
-- LB23a: PR × (ID|EB|EM), (ID|EB|EM) × PO
elsif LB23a_Applies (Prev_Eff, Eff_B) then False
-- LB24: (PR|PO) × (AL|HL), (AL|HL) × (PR|PO)
elsif LB24_Applies (Prev_Eff, Eff_B) then False
-- LB25: simple pair rules
elsif LB25_Simple (Prev_Eff, Eff_B) then False
-- LB25: NU-context rules
elsif LB25_NU_Context (Prev_Eff, Eff_B, In_NU_Ctx) then False
-- LB25: PO/PR × OP (lookahead for NU)
elsif (Prev_Eff = LBP_PO or Prev_Eff = LBP_PR)
and Is_OP (Eff_B)
then (if LB25_OP_Res then False else True)
-- LB26: Korean syllable
elsif LB26_Applies (Prev_Eff, Eff_B) then False
-- LB27: Korean syllable + PO/PR
elsif LB27_Applies (Prev_Eff, Eff_B) then False
-- LB28: (AL|HL) × (AL|HL)
elsif LB28_Applies (Prev_Eff, Eff_B) then False
-- LB28a: Brahmic sub-rules
elsif LB28a_Sub1 (Prev_Eff, Eff_B, This_Is_DC) then False
elsif LB28a_Sub2 (Prev_Eff, Prev_Is_DC, Eff_B) then False
elsif LB28a_Sub3 (Before_Prev_Eff, Before_Prev_DC,
Prev_Eff, Eff_B, This_Is_DC) then False
elsif LB28a_Sub4_Prefix (Prev_Eff, Prev_Is_DC,
Eff_B, This_Is_DC)
then (if LB28a_VF_Res then False else True)
-- LB29: IS × (AL|HL)
elsif LB29_Applies (Prev_Eff, Eff_B) then False
-- LB30: (AL|HL|NU) × OP (non-EA), CP (non-EA) × (AL|HL|NU)
elsif LB30_Applies (Prev_Eff, Eff_B) then False
-- LB30a: RI × RI (odd count → no break, even → break)
elsif Prev_Eff = LBP_RI and Eff_B = LBP_RI then
(if RI_Count mod 2 = 1 then False else True)
-- LB30b: EB × EM, or (ExtPict ∧ Cn) × EM
elsif LB30b_Applies (Prev_Eff, Eff_B, Prev_ExtPict_Cn) then False
-- LB31: ALL ÷ / ÷ ALL
else True)
with Ghost;
end Lingenic_Text.Line_Break_Spec;