-- 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 — Collation body
--
-- Self-contained collation module. Initialize reads allkeys.txt (DUCET)
-- at init time. Requires Normalization to be initialized first.
--
-- Initialize is SPARK_Mode Off: file I/O, string parsing.
--
-- All runtime procedures (Compare, Sort_Key) and their helpers
-- (Produce_CEs, Sort_Key_From_CEs, Implicit_Weight) are SPARK_Mode On.
-------------------------------------------------------------------------------
with Lingenic_Text.File_IO;
with Lingenic_Text.Normalization_Spec;
with Lingenic_Text.UTF8;
package body Lingenic_Text.Collation
with SPARK_Mode,
Refined_State => (Collation_State =>
(Is_Init,
CE_Index, CE_Data, CE_Used,
Contraction_Starter,
Starter_Index, Contraction_Entries, Contraction_Used,
Implicit_Ranges, Implicit_Count,
Init_Buffer, Init_Length))
is
---------------------------------------------------------------------------
-- Constants
---------------------------------------------------------------------------
Max_CE_Data : constant := 250_000;
Max_Contractions : constant := 1024;
Max_Implicit_Ranges : constant := 8;
-- NFD output buffer size. NFD can expand by at most 3x for canonical
-- decompositions. We limit input to Max_Input_CPs codepoints (~1 KB
-- of UTF-8 typically). 3072 bytes is generous.
Max_NFD_Bytes : constant := 3072;
---------------------------------------------------------------------------
-- Data types
---------------------------------------------------------------------------
-- Per-codepoint index into CE_Data.
-- 0 = not in DUCET (compute implicit weight).
-- > 0 = offset: CE_Data(offset) = count, then 4*count entries follow
-- (primary, secondary, tertiary, variable_flag per CE).
type CE_Index_Type is array (0 .. Max_Codepoint) of Natural;
-- Packed CE storage.
type CE_Data_Type is array (1 .. Max_CE_Data) of Natural;
-- Boolean flat array: is this CP a contraction starter?
type Starter_Flag_Type is array (0 .. Max_Codepoint) of Boolean;
-- Contraction entry: starter CP1, CP2, CP3 (0 if 2-CP), CE offset.
type Contraction_Entry is record
CP1 : Natural; -- Starter codepoint (for sorting)
CP2 : Natural; -- Second codepoint of contraction
CP3 : Natural; -- Third codepoint (0 = 2-CP contraction)
CE_Offset : Natural; -- Into CE_Data
end record;
-- Per-starter index into Contraction_Entries.
type Starter_Range is record
Start : Natural; -- 1-based, 0 = no contractions
Count : Natural;
end record;
type Starter_Index_Type is array (0 .. Max_Codepoint) of Starter_Range;
type Contraction_Array is array (1 .. Max_Contractions) of Contraction_Entry;
-- Implicit weight ranges from @implicitweights directives.
-- BBBB_Offset is the minimum First_CP among all ranges sharing the same
-- Base value. UTS #10 §10.1.3 says BBBB = (CP - group_first) | 0x8000,
-- where group_first is the first CP of the entire siniform group, not the
-- individual @implicitweights range.
type Implicit_Range is record
First_CP : Natural;
Last_CP : Natural;
Base : Natural; -- e.g. 16#FB00#
BBBB_Offset : Natural; -- min First_CP among ranges with same Base
end record;
type Implicit_Range_Array is array (1 .. Max_Implicit_Ranges) of Implicit_Range;
-- Work arrays for CE production and sort key building.
type CP_Work_Array is array (1 .. Max_Input_CPs) of Natural;
type CCC_Work_Array is array (1 .. Max_Input_CPs) of Natural;
type CE_Primary_Array is array (1 .. Max_CEs) of Natural;
type CE_Secondary_Array is array (1 .. Max_CEs) of Natural;
type CE_Tertiary_Array is array (1 .. Max_CEs) of Natural;
type CE_Variable_Array is array (1 .. Max_CEs) of Boolean;
---------------------------------------------------------------------------
-- State variables
---------------------------------------------------------------------------
Is_Init : Boolean := False;
CE_Index : CE_Index_Type := [others => 0];
CE_Data : CE_Data_Type := [others => 0];
CE_Used : Natural := 0;
Contraction_Starter : Starter_Flag_Type := [others => False];
Starter_Index : Starter_Index_Type := [others => (Start => 0, Count => 0)];
Contraction_Entries : Contraction_Array :=
[others => (CP1 => 0, CP2 => 0, CP3 => 0, CE_Offset => 0)];
Contraction_Used : Natural := 0;
Implicit_Ranges : Implicit_Range_Array :=
[others => (First_CP => 0, Last_CP => 0, Base => 0, BBBB_Offset => 0)];
Implicit_Count : Natural range 0 .. Max_Implicit_Ranges := 0;
---------------------------------------------------------------------------
-- Init-time temporaries (package-level to avoid stack overflow)
---------------------------------------------------------------------------
Init_Buffer : File_IO.File_Byte_Array := [others => 0];
Init_Length : File_IO.File_Size := 0;
---------------------------------------------------------------------------
-- Initialized
---------------------------------------------------------------------------
function Initialized return Boolean is (Is_Init);
---------------------------------------------------------------------------
-- Implicit_Weight — compute two CEs for a CP not in DUCET
--
-- UTS #10 Section 10.1.3:
-- Returns AAAA and BBBB such that the CE pair is:
-- [.AAAA.0020.0002][.BBBB.0000.0000]
---------------------------------------------------------------------------
procedure Implicit_Weight
(CP : Codepoint;
AAAA : out Natural;
BBBB : out Natural;
Siniform : out Boolean)
with Global => (Input => (Implicit_Ranges, Implicit_Count)),
Post => -- Platinum: non-siniform codepoints match ghost spec
(if not Siniform
then AAAA = Implicit_AAAA (CP)
and then BBBB = Implicit_BBBB (CP))
is
begin
Siniform := False;
-- Check @implicitweights ranges first (siniform scripts).
-- These have their own BBBB formula: (CP - range_first) mod 0x8000 + 0x8000.
-- (Adding 0x8000 to a value in 0..0x7FFF is equivalent to setting bit 15.)
for I in 1 .. Implicit_Count loop
pragma Loop_Invariant (I <= Implicit_Count
and then Implicit_Count <= Max_Implicit_Ranges);
if CP >= Implicit_Ranges (I).First_CP
and then CP <= Implicit_Ranges (I).Last_CP
then
AAAA := Implicit_Ranges (I).Base;
BBBB := ((CP - Implicit_Ranges (I).BBBB_Offset) mod 16#8000#)
+ 16#8000#;
Siniform := True;
return;
end if;
end loop;
-- Core Han: CJK_Unified_Ideographs + CJK_Compatibility_Ideographs
if Is_Core_Han (CP) then
AAAA := Natural (Implicit_Base_Core_Han) + CP / 16#8000#;
BBBB := (CP mod 16#8000#) + 16#8000#;
pragma Assert (AAAA = Implicit_AAAA (CP));
pragma Assert (BBBB = Implicit_BBBB (CP));
return;
end if;
-- Other Han (extensions)
if Is_Other_Han (CP) then
AAAA := Natural (Implicit_Base_Other_Han) + CP / 16#8000#;
BBBB := (CP mod 16#8000#) + 16#8000#;
pragma Assert (AAAA = Implicit_AAAA (CP));
pragma Assert (BBBB = Implicit_BBBB (CP));
return;
end if;
-- Unassigned and all others
AAAA := Natural (Implicit_Base_Unassigned) + CP / 16#8000#;
BBBB := (CP mod 16#8000#) + 16#8000#;
pragma Assert (AAAA = Implicit_AAAA (CP));
pragma Assert (BBBB = Implicit_BBBB (CP));
end Implicit_Weight;
---------------------------------------------------------------------------
-- Append_CEs_From_Data — append CEs stored at a given offset in CE_Data
---------------------------------------------------------------------------
procedure Append_CEs_From_Data
(Offset : Positive;
Primaries : in out CE_Primary_Array;
Seconds : in out CE_Secondary_Array;
Tertiaries : in out CE_Tertiary_Array;
Variables : in out CE_Variable_Array;
CE_Count : in out Natural;
Success : in out Boolean)
with Pre => Offset >= 1
and then Offset <= Max_CE_Data
and then CE_Count <= Max_CEs
and then Success,
Post => CE_Count >= CE_Count'Old
and then CE_Count <= Max_CEs
-- Frame: existing CE entries unchanged
and then
(for all I in 1 .. CE_Count'Old =>
Primaries (I) = Primaries'Old (I)
and then Seconds (I) = Seconds'Old (I)
and then Tertiaries (I) = Tertiaries'Old (I)
and then Variables (I) = Variables'Old (I))
is
N : Natural;
begin
N := CE_Data (Offset);
if N = 0 or else N > 18 then
-- Invalid entry
return;
end if;
-- Check that data fits within CE_Data bounds
if Offset > Max_CE_Data - N * 4 then
Success := False;
return;
end if;
-- Check CE_Count won't overflow
if CE_Count > Max_CEs - N then
Success := False;
return;
end if;
for I in 1 .. N loop
pragma Loop_Invariant (CE_Count >= CE_Count'Loop_Entry
and then CE_Count <= Max_CEs - (N - I + 1)
and then CE_Count < Max_CEs);
-- Frame: entries before the append start are unchanged
pragma Loop_Invariant
(for all J in 1 .. CE_Count'Loop_Entry =>
Primaries (J) = Primaries'Loop_Entry (J)
and then Seconds (J) = Seconds'Loop_Entry (J)
and then Tertiaries (J) = Tertiaries'Loop_Entry (J)
and then Variables (J) = Variables'Loop_Entry (J));
CE_Count := CE_Count + 1;
declare
Base : constant Positive := Offset + (I - 1) * 4;
begin
if Base + 4 <= Max_CE_Data then
Primaries (CE_Count) := CE_Data (Base + 1);
Seconds (CE_Count) := CE_Data (Base + 2);
Tertiaries (CE_Count) := CE_Data (Base + 3);
Variables (CE_Count) := CE_Data (Base + 4) /= 0;
else
-- Shouldn't happen; data was already bounds-checked
Primaries (CE_Count) := 0;
Seconds (CE_Count) := 0;
Tertiaries (CE_Count) := 0;
Variables (CE_Count) := False;
end if;
end;
end loop;
end Append_CEs_From_Data;
---------------------------------------------------------------------------
-- Produce_CEs — convert a codepoint array to a collation element array
--
-- UTS #10 Section 7.1: for each codepoint in the NFD-normalized input,
-- look up its CE(s). Handle contractions and implicit weights.
---------------------------------------------------------------------------
procedure Produce_CEs
(CPs : CP_Work_Array;
CP_Count : Natural;
CCC_Values : CCC_Work_Array;
Primaries : out CE_Primary_Array;
Seconds : out CE_Secondary_Array;
Tertiaries : out CE_Tertiary_Array;
Variables : out CE_Variable_Array;
CE_Count : out Natural;
Success : out Boolean)
with Pre => CP_Count >= 1
and then CP_Count <= Max_Input_CPs,
Post => CE_Count <= Max_CEs
is
I : Natural;
CP : Natural;
Offset : Natural;
AAAA : Natural;
BBBB : Natural;
Unused_Siniform : Boolean;
Matched : Boolean;
-- Consumed flags: True = this CP was consumed by a discontiguous
-- contraction and should be skipped during main-loop processing.
type Consumed_Array is array (1 .. Max_Input_CPs) of Boolean;
Consumed : Consumed_Array := [others => False];
begin
Primaries := [others => 0];
Seconds := [others => 0];
Tertiaries := [others => 0];
Variables := [others => False];
CE_Count := 0;
Success := True;
I := 1;
while I <= CP_Count loop
pragma Loop_Invariant (I >= 1 and then I <= CP_Count);
pragma Loop_Invariant (CP_Count <= Max_Input_CPs);
pragma Loop_Invariant (CE_Count <= Max_CEs);
pragma Loop_Invariant (Success);
-- Skip CPs consumed by discontiguous contractions
if Consumed (I) then
I := I + 1;
else
CP := CPs (I);
Matched := False;
if CP > Max_Codepoint then
-- Out of Unicode range — skip
I := I + 1;
elsif Contraction_Starter (CP)
and then Starter_Index (CP).Count > 0
then
-- UTS #10 S2.1: Two-phase contraction matching.
--
-- Phase 1: Find the longest contiguous prefix match.
-- Phase 2: Extend discontiguously through unblocked non-starters,
-- one non-starter at a time (S2.1.1–S2.1.3).
--
-- WF5 guarantees that if a 3-CP contraction ABC exists with C a
-- non-starter, then the 2-CP prefix AB also exists. This lets the
-- one-at-a-time extension find ABC via: S=A → S=AB → S=ABC.
declare
SR : constant Starter_Range := Starter_Index (CP);
Start : constant Natural := SR.Start;
Cnt : constant Natural := SR.Count;
-- Best match so far.
Best_Offset : Natural := 0; -- 0 = no contraction match
Best_Advance : Natural := 1; -- contiguous CPs to skip
Best_Level : Natural := 1; -- total match length (incl discont.)
Best_CP2 : Natural := 0; -- second CP of best match
begin
if Start >= 1 and then Cnt >= 1
and then Cnt <= Max_Contractions
and then Start <= Max_Contractions - Cnt + 1
then
-- Phase 1: Find longest contiguous match.
-- Try 2-CP first, then 3-CP (greedy longest).
for J in Start .. Start + Cnt - 1 loop
pragma Loop_Invariant
(CE_Count <= Max_CEs and then Success
and then I >= 1 and then I <= CP_Count
and then CP_Count <= Max_Input_CPs
and then Best_Level <= 3
and then Best_Advance <= 3);
declare
CE : constant Contraction_Entry :=
Contraction_Entries (J);
begin
-- 2-CP contiguous match
if CE.CP3 = 0
and then I + 1 <= CP_Count
and then not Consumed (I + 1)
and then CPs (I + 1) = CE.CP2
and then Best_Level < 2
then
Best_Offset := CE.CE_Offset;
Best_Advance := 2;
Best_Level := 2;
Best_CP2 := CE.CP2;
end if;
-- 3-CP contiguous match (overrides 2-CP if found)
if CE.CP3 /= 0
and then I + 2 <= CP_Count
and then not Consumed (I + 1)
and then not Consumed (I + 2)
and then CPs (I + 1) = CE.CP2
and then CPs (I + 2) = CE.CP3
and then Best_Level < 3
then
Best_Offset := CE.CE_Offset;
Best_Advance := 3;
Best_Level := 3;
Best_CP2 := CE.CP2;
end if;
end;
end loop;
-- Phase 2: Discontiguous extension (S2.1.1–S2.1.3).
-- Only attempt if we haven't already found a 3-CP match
-- (max contraction length in DUCET).
if Best_Level < 3 and then I + 1 <= CP_Count then
declare
-- Start scanning after contiguous match, or at I+1
-- if no contiguous match yet.
K_Init : constant Natural :=
(if Best_Advance >= 1 then I + Best_Advance
else I + 1);
K : Natural := K_Init;
Max_CCC : Natural := 0;
Ext_CP2 : Natural := Best_CP2;
Ext_Offset : Natural := Best_Offset;
Ext_Level : Natural := Best_Level;
-- Ext_Level: 1 = starter only, 2 = 2-CP match
Found : Boolean;
begin
while K <= CP_Count and then Ext_Level < 3 loop
pragma Loop_Invariant
(K >= I + 1
and then I >= 1 and then I <= CP_Count
and then CP_Count <= Max_Input_CPs);
pragma Loop_Variant (Increases => K);
-- Skip already-consumed positions
if Consumed (K) then
if K = CP_Count then exit; end if;
K := K + 1;
-- Hit a starter → stop discontiguous scan
elsif CCC_Values (K) = 0 then
exit;
-- Blocked: CCC(K) <= max CCC of intervening
-- non-consumed non-starters → stop scan
elsif Max_CCC /= 0
and then CCC_Values (K) <= Max_CCC
then
exit;
else
-- K is an unblocked non-starter.
-- Try extending the current match S by CPs(K).
Found := False;
if Ext_Level = 1 then
-- S = starter only. Look for 2-CP match:
-- starter + CPs(K)
for J in Start .. Start + Cnt - 1 loop
pragma Loop_Invariant (not Found);
if Contraction_Entries (J).CP3 = 0
and then Contraction_Entries (J).CP2
= CPs (K)
then
Ext_Offset := Contraction_Entries (J)
.CE_Offset;
Ext_CP2 := CPs (K);
Ext_Level := 2;
Consumed (K) := True;
Found := True;
exit;
end if;
end loop;
elsif Ext_Level = 2 then
-- S = starter + Ext_CP2. Look for 3-CP match:
-- starter + Ext_CP2 + CPs(K)
for J in Start .. Start + Cnt - 1 loop
pragma Loop_Invariant (not Found);
if Contraction_Entries (J).CP2 = Ext_CP2
and then Contraction_Entries (J).CP3
= CPs (K)
then
Ext_Offset := Contraction_Entries (J)
.CE_Offset;
Ext_Level := 3;
Consumed (K) := True;
Found := True;
exit;
end if;
end loop;
end if;
if not Found then
-- CPs(K) didn't extend the match.
-- Update Max_CCC for blocking computation
-- and continue to next non-starter.
Max_CCC := CCC_Values (K);
end if;
if K = CP_Count then exit; end if;
K := K + 1;
end if;
end loop;
-- Commit the discontiguous extension result.
-- Best_Advance stays as the contiguous advance;
-- Best_Level tracks the total match length.
if Ext_Level > Best_Level then
Best_Offset := Ext_Offset;
Best_Level := Ext_Level;
end if;
end;
end if;
end if;
-- Apply the best contraction match found.
-- Best_Level >= 2 means a contraction was matched.
-- Best_Advance is the contiguous CPs to skip;
-- discontiguous CPs are already flagged in Consumed.
if Best_Level >= 2
and then Best_Offset >= 1
and then Best_Offset <= Max_CE_Data
then
Append_CEs_From_Data
(Best_Offset,
Primaries, Seconds, Tertiaries, Variables,
CE_Count, Success);
I := I + Best_Advance;
Matched := True;
end if;
end;
end if;
if not Success then exit; end if;
if not Matched and then CP <= Max_Codepoint then
-- Single codepoint lookup
Offset := CE_Index (CP);
if Offset >= 1 and then Offset <= Max_CE_Data then
-- Explicit DUCET entry
Append_CEs_From_Data
(Offset, Primaries, Seconds, Tertiaries, Variables,
CE_Count, Success);
else
-- Implicit weight
Implicit_Weight (CP, AAAA, BBBB, Unused_Siniform);
if CE_Count > Max_CEs - 2 then
Success := False;
exit;
end if;
CE_Count := CE_Count + 1;
Primaries (CE_Count) := AAAA;
Seconds (CE_Count) := 16#0020#;
Tertiaries (CE_Count) := 16#0002#;
Variables (CE_Count) := False;
CE_Count := CE_Count + 1;
Primaries (CE_Count) := BBBB;
Seconds (CE_Count) := 0;
Tertiaries (CE_Count) := 0;
Variables (CE_Count) := False;
end if;
I := I + 1;
end if;
if not Success then exit; end if;
if I > CP_Count then exit; end if;
end if; -- Consumed check
end loop;
if not Success then
CE_Count := 0;
end if;
end Produce_CEs;
---------------------------------------------------------------------------
-- Sort_Key_From_CEs — build a binary sort key from CE arrays
--
-- UTS #10 Section 7.3:
-- Non_Ignorable: L1 primary | 0000 | L2 secondary | 0000 | L3 tertiary
-- Shifted: L1..L3 with variable suppression + L4 shifted weights
--
-- Each weight is written as 2 bytes big-endian.
---------------------------------------------------------------------------
procedure Sort_Key_From_CEs
(Primaries : CE_Primary_Array;
Seconds : CE_Secondary_Array;
Tertiaries : CE_Tertiary_Array;
Variables : CE_Variable_Array;
CE_Count : Natural;
Option : Variable_Weight_Option;
Key : in out Byte_Array;
Last : out Natural;
Success : out Boolean)
with Pre => CE_Count <= Max_CEs
and then Key'Length >= 1
and then Key'Last < Positive'Last,
Post => (if Success then
Last in Key'First .. Key'Last
else
Last = Key'First - 1)
is
Pos : Natural := Key'First;
procedure Write_16 (Val : Natural)
with Pre => Key'First >= 1
and then Key'Last >= Key'First
and then Key'Last < Positive'Last
and then Pos >= Key'First
and then Pos < Key'Last,
Post => Pos = Pos'Old + 2
and then Pos >= Key'First + 2
and then Pos <= Key'Last + 1
is
begin
Key (Pos) := (Val / 256) mod 256;
Key (Pos + 1) := Val mod 256;
Pos := Pos + 2;
end Write_16;
After_Variable : Boolean := False;
begin
Last := Key'First - 1;
Success := True;
if CE_Count = 0 then
-- Empty string: produce minimal sort key
if Pos < Key'Last then
Write_16 (0);
Last := Pos - 1;
else
Success := False;
end if;
return;
end if;
-- === Level 1: Primary weights ===
for I in 1 .. CE_Count loop
pragma Loop_Invariant (Pos >= Key'First and then Pos <= Key'Last + 1);
pragma Loop_Invariant (Success);
if Option = Non_Ignorable then
if Primaries (I) /= 0 then
if Pos >= Key'Last then
Success := False;
Last := Key'First - 1;
return;
end if;
Write_16 (Primaries (I));
end if;
else
-- Shifted: suppress variable CEs and trailing ignorables
if Variables (I) then
After_Variable := True;
-- Skip this primary
elsif Primaries (I) = 0 and then After_Variable then
-- Ignorable after variable: skip
null;
else
After_Variable := False;
if Primaries (I) /= 0 then
if Pos >= Key'Last then
Success := False;
Last := Key'First - 1;
return;
end if;
Write_16 (Primaries (I));
end if;
end if;
end if;
end loop;
-- L1/L2 separator
if Pos >= Key'Last then
Success := False;
Last := Key'First - 1;
return;
end if;
Write_16 (0);
-- === Level 2: Secondary weights ===
After_Variable := False;
for I in 1 .. CE_Count loop
pragma Loop_Invariant (Pos >= Key'First and then Pos <= Key'Last + 1);
pragma Loop_Invariant (Success);
if Option = Non_Ignorable then
if Seconds (I) /= 0 then
if Pos >= Key'Last then
Success := False;
Last := Key'First - 1;
return;
end if;
Write_16 (Seconds (I));
end if;
else
-- Shifted L2: UTS #10 Table 11
if Variables (I) then
After_Variable := True;
-- Variable: suppress secondary
elsif Primaries (I) = 0 and then Seconds (I) = 0
and then Tertiaries (I) = 0
then
null; -- Completely ignorable: always suppress, state unchanged
elsif Primaries (I) = 0 and then After_Variable then
null; -- Ignorable after variable: suppress
else
-- Non-variable primary (P /= 0) or
-- ignorable NOT following variable (P = 0, not After_Variable)
if Primaries (I) /= 0 then
After_Variable := False;
end if;
if Seconds (I) /= 0 then
if Pos >= Key'Last then
Success := False;
Last := Key'First - 1;
return;
end if;
Write_16 (Seconds (I));
end if;
end if;
end if;
end loop;
-- L2/L3 separator
if Pos >= Key'Last then
Success := False;
Last := Key'First - 1;
return;
end if;
Write_16 (0);
-- === Level 3: Tertiary weights ===
After_Variable := False;
for I in 1 .. CE_Count loop
pragma Loop_Invariant (Pos >= Key'First and then Pos <= Key'Last + 1);
pragma Loop_Invariant (Success);
if Option = Non_Ignorable then
if Tertiaries (I) /= 0 then
if Pos >= Key'Last then
Success := False;
Last := Key'First - 1;
return;
end if;
Write_16 (Tertiaries (I));
end if;
else
-- Shifted L3: UTS #10 Table 11
if Variables (I) then
After_Variable := True;
-- Variable: suppress tertiary
elsif Primaries (I) = 0 and then Seconds (I) = 0
and then Tertiaries (I) = 0
then
null; -- Completely ignorable: always suppress, state unchanged
elsif Primaries (I) = 0 and then After_Variable then
null; -- Ignorable after variable: suppress
else
if Primaries (I) /= 0 then
After_Variable := False;
end if;
if Tertiaries (I) /= 0 then
if Pos >= Key'Last then
Success := False;
Last := Key'First - 1;
return;
end if;
Write_16 (Tertiaries (I));
end if;
end if;
end if;
end loop;
-- === Level 4 (Shifted only) ===
if Option = Shifted then
-- L3/L4 separator
if Pos >= Key'Last then
Success := False;
Last := Key'First - 1;
return;
end if;
Write_16 (0);
-- Shifted L4: UTS #10 Table 11
-- Variable → L4 = old primary
-- Completely ignorable → L4 = 0000 (not appended)
-- Ignorable after variable → L4 = 0000 (not appended)
-- Ignorable not after variable → L4 = FFFF
-- Non-variable primary → L4 = FFFF
After_Variable := False;
for I in 1 .. CE_Count loop
pragma Loop_Invariant
(Pos >= Key'First and then Pos <= Key'Last + 1 and then Success);
if Variables (I) then
-- Variable CE: L4 = original primary
After_Variable := True;
if Primaries (I) /= 0 then
if Pos >= Key'Last then
Success := False;
Last := Key'First - 1;
return;
end if;
Write_16 (Primaries (I));
end if;
elsif Primaries (I) = 0 and then Seconds (I) = 0
and then Tertiaries (I) = 0
then
-- Completely ignorable: L4 = 0000, state unchanged
null;
elsif Primaries (I) = 0 and then After_Variable then
-- Ignorable after variable: L4 = 0000, state unchanged
null;
elsif Primaries (I) = 0 then
-- Ignorable NOT following variable: L4 = FFFF
if Pos >= Key'Last then
Success := False;
Last := Key'First - 1;
return;
end if;
Write_16 (16#FFFF#);
else
-- Non-variable primary: L4 = FFFF
After_Variable := False;
if Pos >= Key'Last then
Success := False;
Last := Key'First - 1;
return;
end if;
Write_16 (16#FFFF#);
end if;
end loop;
end if;
if Pos > Key'First then
Last := Pos - 1;
else
Last := Key'First - 1;
Success := False;
end if;
end Sort_Key_From_CEs;
---------------------------------------------------------------------------
-- Process_String — NFD normalize, decode to codepoints, produce CEs,
-- build sort key.
---------------------------------------------------------------------------
procedure Process_String
(Input : Byte_Array;
Option : Variable_Weight_Option;
Key : in out Byte_Array;
Last : out Natural;
Success : out Boolean)
with Pre => Initialized
and then Normalization.Initialized
and then Normalization.Data_All_Terminal
and then Input'Length >= 1
and then Key'Length >= 1
and then Input'Last < Positive'Last
and then Key'Last < Positive'Last,
Post => (if Success then
Last in Key'First .. Key'Last
else
Last = Key'First - 1),
Global => (Proof_In => Is_Init,
Input => (CE_Index, CE_Data,
Contraction_Starter,
Starter_Index, Contraction_Entries,
Implicit_Ranges, Implicit_Count,
Normalization.Norm_State))
is
use type Normalization.Norm_Status;
NFD_Output : Byte_Array (1 .. Max_NFD_Bytes) := [others => 0];
NFD_Last : Natural;
NFD_Status : Normalization.Norm_Status;
CPs : CP_Work_Array := [others => 0];
CCC_Values : CCC_Work_Array := [others => 0];
CP_Count : Natural := 0;
Pos : Natural;
CP_Val : Codepoint;
Len : Positive;
Valid : Boolean;
CE_Prim : CE_Primary_Array;
CE_Sec : CE_Secondary_Array;
CE_Tert : CE_Tertiary_Array;
CE_Var : CE_Variable_Array;
CE_Count : Natural;
CE_OK : Boolean;
begin
Last := Key'First - 1;
Success := False;
-- Step 1: NFD normalize the input
Normalization.Normalize
(Input, Normalization_Spec.NFD, NFD_Output, NFD_Last, NFD_Status);
if NFD_Status /= Normalization.Norm_Status'(Normalization.Success) then
return;
end if;
-- Step 2: Decode NFD output to codepoints with CCC values
Pos := 1;
while Pos <= NFD_Last loop
pragma Loop_Invariant (Pos >= 1 and then Pos <= NFD_Last);
pragma Loop_Invariant (CP_Count <= Max_Input_CPs);
pragma Loop_Variant (Increases => Pos);
UTF8.Decode (NFD_Output, Pos, CP_Val, Len, Valid);
if not Valid then
return;
end if;
if CP_Count >= Max_Input_CPs then
return; -- Input too long
end if;
CP_Count := CP_Count + 1;
CPs (CP_Count) := CP_Val;
CCC_Values (CP_Count) :=
Natural (Normalization.Get_CCC (CP_Val));
exit when Pos > NFD_Last - Len + 1;
Pos := Pos + Len;
end loop;
if CP_Count = 0 then
return;
end if;
-- Step 3: Produce collation elements
Produce_CEs
(CPs, CP_Count, CCC_Values,
CE_Prim, CE_Sec, CE_Tert, CE_Var, CE_Count, CE_OK);
if not CE_OK then
return;
end if;
-- Step 4: Build sort key
Sort_Key_From_CEs
(CE_Prim, CE_Sec, CE_Tert, CE_Var, CE_Count,
Option, Key, Last, Success);
end Process_String;
---------------------------------------------------------------------------
-- Compare_Sort_Keys — Platinum byte-by-byte sort key comparison
--
-- Postcondition: Result = Ghost_Compare_Bytes (Left, Left_Len,
-- Right, Right_Len, 1)
-- Proves the comparison loop matches the recursive ghost specification.
---------------------------------------------------------------------------
procedure Compare_Sort_Keys
(Left : Byte_Array;
Left_Len : Natural;
Right : Byte_Array;
Right_Len : Natural;
Result : out Comparison_Result)
with Pre => Left'First = 1
and then Right'First = 1
and then Left'Last < Positive'Last
and then Right'Last < Positive'Last
and then Left_Len >= 1
and then Left_Len <= Left'Last
and then Right_Len >= 1
and then Right_Len <= Right'Last,
Post => Result = Ghost_Compare_Bytes
(Left, Left_Len, Right, Right_Len, 1)
is
Min_Len : constant Natural := Natural'Min (Left_Len, Right_Len);
begin
for I in 1 .. Min_Len loop
pragma Loop_Invariant
(Ghost_Compare_Bytes (Left, Left_Len, Right, Right_Len, 1) =
Ghost_Compare_Bytes (Left, Left_Len, Right, Right_Len, I));
if Left (I) < Right (I) then
Result := Less;
return;
elsif Left (I) > Right (I) then
Result := Greater;
return;
end if;
end loop;
-- All common bytes are equal; shorter key is less
if Left_Len < Right_Len then
Result := Less;
elsif Left_Len > Right_Len then
Result := Greater;
else
Result := Equal;
end if;
end Compare_Sort_Keys;
---------------------------------------------------------------------------
-- Compare
---------------------------------------------------------------------------
procedure Compare
(Left : Byte_Array;
Right : Byte_Array;
Option : Variable_Weight_Option;
Result : out Comparison_Result;
Success : out Boolean)
is
Left_Key : Byte_Array (1 .. Max_Sort_Key) := [others => 0];
Left_Last : Natural;
Left_OK : Boolean;
Right_Key : Byte_Array (1 .. Max_Sort_Key) := [others => 0];
Right_Last : Natural;
Right_OK : Boolean;
begin
Result := Equal;
Success := False;
Process_String (Left, Option, Left_Key, Left_Last, Left_OK);
if not Left_OK then
return;
end if;
Process_String (Right, Option, Right_Key, Right_Last, Right_OK);
if not Right_OK then
return;
end if;
Success := True;
Compare_Sort_Keys (Left_Key, Left_Last, Right_Key, Right_Last, Result);
end Compare;
---------------------------------------------------------------------------
-- Sort_Key
---------------------------------------------------------------------------
procedure Sort_Key
(Input : Byte_Array;
Option : Variable_Weight_Option;
Key : in out Byte_Array;
Last : out Natural;
Success : out Boolean)
is
begin
Process_String (Input, Option, Key, Last, Success);
end Sort_Key;
---------------------------------------------------------------------------
-- Initialize
--
-- Parse allkeys.txt and populate all data tables.
-- SPARK_Mode Off — uses string parsing and file I/O.
---------------------------------------------------------------------------
procedure Initialize
(UCD_Dir : String;
Success : out Boolean)
with SPARK_Mode => Off
is
OK : Boolean;
-- Hex parsing helper
function Hex_Val (B : Natural) return Natural is
begin
if B in 48 .. 57 then -- '0'..'9'
return B - 48;
elsif B in 65 .. 70 then -- 'A'..'F'
return B - 65 + 10;
elsif B in 97 .. 102 then -- 'a'..'f'
return B - 97 + 10;
else
return 0;
end if;
end Hex_Val;
function Is_Hex (B : Natural) return Boolean is
(B in 48 .. 57 or B in 65 .. 70 or B in 97 .. 102);
-- Parse a hex number starting at position P in Init_Buffer.
-- Advances P past the number. Returns 0 on failure.
procedure Parse_Hex
(P : in out Natural;
Value : out Natural)
is
V : Natural := 0;
begin
Value := 0;
while P <= Init_Length and then Is_Hex (Init_Buffer (P)) loop
V := V * 16 + Hex_Val (Init_Buffer (P));
P := P + 1;
end loop;
Value := V;
end Parse_Hex;
-- Skip whitespace
procedure Skip_Space (P : in out Natural) is
begin
while P <= Init_Length
and then (Init_Buffer (P) = 32 or Init_Buffer (P) = 9)
loop
P := P + 1;
end loop;
end Skip_Space;
-- Find end of line (LF or end of buffer)
function Line_End (From : Natural) return Natural is
P : Natural := From;
begin
while P <= Init_Length
and then Init_Buffer (P) /= 10
and then Init_Buffer (P) /= 13
loop
P := P + 1;
end loop;
return P;
end Line_End;
-- Skip to next line
procedure Next_Line (P : in out Natural) is
begin
while P <= Init_Length
and then Init_Buffer (P) /= 10
loop
P := P + 1;
end loop;
if P <= Init_Length then
P := P + 1; -- skip LF
end if;
end Next_Line;
-- Parse codepoints before ';'
-- Returns number of CPs parsed (0..Max_CPS).
Max_CPS : constant := 4;
type Line_CPs is array (1 .. Max_CPS) of Natural;
procedure Parse_Codepoints
(P : in out Natural;
CPs : out Line_CPs;
Count : out Natural)
is
Val : Natural;
begin
CPs := [others => 0];
Count := 0;
Skip_Space (P);
while P <= Init_Length and then Init_Buffer (P) /= 59 loop -- ';'
if Is_Hex (Init_Buffer (P)) then
Parse_Hex (P, Val);
if Count < Max_CPS then
Count := Count + 1;
CPs (Count) := Val;
end if;
end if;
Skip_Space (P);
end loop;
-- Skip past ';'
if P <= Init_Length and then Init_Buffer (P) = 59 then
P := P + 1;
end if;
end Parse_Codepoints;
-- Parse CE list: [.PPPP.SSSS.TTTT] or [*PPPP.SSSS.TTTT]
-- Store into CE_Data at CE_Used. Returns offset and count.
procedure Parse_CE_List
(P : in out Natural;
Offset : out Natural;
CE_Count : out Natural;
Parse_OK : out Boolean)
is
LE : constant Natural := Line_End (P);
Prim, Sec, Tert : Natural;
Is_Variable : Boolean;
begin
Offset := CE_Used + 1;
CE_Count := 0;
Parse_OK := True;
-- Reserve space for the count
if CE_Used >= Max_CE_Data then
Parse_OK := False;
return;
end if;
CE_Used := CE_Used + 1;
Skip_Space (P);
while P < LE loop
-- Look for '['
if Init_Buffer (P) /= 91 then -- '['
P := P + 1;
-- Stop at '#' (comment)
if P <= Init_Length and then Init_Buffer (P - 1) = 35 then
exit;
end if;
else
P := P + 1; -- skip '['
if P > Init_Length then
Parse_OK := False;
return;
end if;
-- Check variable flag
if Init_Buffer (P) = 42 then -- '*'
Is_Variable := True;
P := P + 1;
elsif Init_Buffer (P) = 46 then -- '.'
Is_Variable := False;
P := P + 1;
else
Parse_OK := False;
return;
end if;
-- Parse PPPP
Parse_Hex (P, Prim);
-- Skip '.'
if P <= Init_Length and then Init_Buffer (P) = 46 then
P := P + 1;
end if;
-- Parse SSSS
Parse_Hex (P, Sec);
-- Skip '.'
if P <= Init_Length and then Init_Buffer (P) = 46 then
P := P + 1;
end if;
-- Parse TTTT
Parse_Hex (P, Tert);
-- Skip to ']'
while P <= Init_Length and then Init_Buffer (P) /= 93 loop
P := P + 1;
end loop;
if P <= Init_Length then
P := P + 1; -- skip ']'
end if;
-- Store CE (4 words: prim, sec, tert, variable flag)
if CE_Used + 4 > Max_CE_Data then
Parse_OK := False;
return;
end if;
CE_Used := CE_Used + 1;
CE_Data (CE_Used) := Prim;
CE_Used := CE_Used + 1;
CE_Data (CE_Used) := Sec;
CE_Used := CE_Used + 1;
CE_Data (CE_Used) := Tert;
CE_Used := CE_Used + 1;
if Is_Variable then
CE_Data (CE_Used) := 1;
else
CE_Data (CE_Used) := 0;
end if;
CE_Count := CE_Count + 1;
end if;
end loop;
-- Write the count at the offset position
CE_Data (Offset) := CE_Count;
end Parse_CE_List;
-- Parse @implicitweights directive
procedure Parse_Implicit_Weights (P : in out Natural) is
First_CP, Last_CP, Base_Val : Natural;
begin
-- Format: @implicitweights HHHH..HHHH; HHHH
-- P is positioned right after "@implicitweights "
Skip_Space (P);
Parse_Hex (P, First_CP);
-- Skip ".."
while P <= Init_Length
and then Init_Buffer (P) = 46
loop
P := P + 1;
end loop;
Parse_Hex (P, Last_CP);
-- Skip "; "
while P <= Init_Length
and then (Init_Buffer (P) = 59 or Init_Buffer (P) = 32)
loop
P := P + 1;
end loop;
Parse_Hex (P, Base_Val);
if Implicit_Count < Max_Implicit_Ranges
and then First_CP <= Max_Codepoint
and then Last_CP <= Max_Codepoint
then
Implicit_Count := Implicit_Count + 1;
Implicit_Ranges (Implicit_Count) :=
(First_CP => First_CP,
Last_CP => Last_CP,
Base => Base_Val,
BBBB_Offset => First_CP);
end if;
end Parse_Implicit_Weights;
P : Natural;
Line_CPs_Arr : Line_CPs;
CP_Count : Natural;
CE_Offset : Natural;
CE_Count : Natural;
Parse_OK : Boolean;
begin
-- Reset all state
Is_Init := False;
CE_Index := [others => 0];
CE_Data := [others => 0];
CE_Used := 0;
Contraction_Starter := [others => False];
Starter_Index := [others => (Start => 0, Count => 0)];
Contraction_Entries :=
[others => (CP1 => 0, CP2 => 0, CP3 => 0, CE_Offset => 0)];
Contraction_Used := 0;
Implicit_Ranges := [others => (First_CP => 0, Last_CP => 0,
Base => 0, BBBB_Offset => 0)];
Implicit_Count := 0;
Success := False;
-- Read allkeys.txt
File_IO.Read_File
(UCD_Dir & "/allkeys.txt", Init_Buffer, Init_Length, OK);
if not OK then
return;
end if;
-- Parse line by line
P := 1;
while P <= Init_Length loop
Skip_Space (P);
if P > Init_Length then
exit;
end if;
-- Skip empty lines and comments
if Init_Buffer (P) = 10 or Init_Buffer (P) = 13 then
Next_Line (P);
elsif Init_Buffer (P) = 35 then -- '#'
Next_Line (P);
elsif Init_Buffer (P) = 64 then -- '@'
-- Directive line
-- Check for "@implicitweights"
declare
Marker : constant String := "@implicitweights";
Match : Boolean := True;
Q : Natural := P;
begin
for I in Marker'Range loop
if Q > Init_Length
or else Character'Pos (Marker (I)) /= Init_Buffer (Q)
then
Match := False;
exit;
end if;
Q := Q + 1;
end loop;
if Match then
P := Q;
Parse_Implicit_Weights (P);
end if;
end;
Next_Line (P);
elsif Is_Hex (Init_Buffer (P)) then
-- Data line: parse codepoints and CE list
Parse_Codepoints (P, Line_CPs_Arr, CP_Count);
if CP_Count >= 1 then
-- Parse CE list
Parse_CE_List (P, CE_Offset, CE_Count, Parse_OK);
if Parse_OK and then CE_Count >= 1 then
if CP_Count = 1 then
-- Single codepoint entry
if Line_CPs_Arr (1) <= Max_Codepoint then
CE_Index (Line_CPs_Arr (1)) := CE_Offset;
end if;
else
-- Contraction (multi-CP entry)
if Line_CPs_Arr (1) <= Max_Codepoint
and then Contraction_Used < Max_Contractions
then
Contraction_Starter (Line_CPs_Arr (1)) := True;
Contraction_Used := Contraction_Used + 1;
Contraction_Entries (Contraction_Used) :=
(CP1 => Line_CPs_Arr (1),
CP2 => Line_CPs_Arr (2),
CP3 => (if CP_Count >= 3
then Line_CPs_Arr (3) else 0),
CE_Offset => CE_Offset);
end if;
end if;
end if;
end if;
Next_Line (P);
else
Next_Line (P);
end if;
end loop;
-- Sort contraction entries by CP1 so that entries for the same
-- starter are contiguous. Simple insertion sort (964 entries max).
for I in 2 .. Contraction_Used loop
declare
Key_Entry : constant Contraction_Entry := Contraction_Entries (I);
J : Natural := I - 1;
begin
while J >= 1
and then Contraction_Entries (J).CP1 > Key_Entry.CP1
loop
Contraction_Entries (J + 1) := Contraction_Entries (J);
J := J - 1;
end loop;
Contraction_Entries (J + 1) := Key_Entry;
end;
end loop;
-- Rebuild Starter_Index from the sorted entries.
Starter_Index := [others => (Start => 0, Count => 0)];
for I in 1 .. Contraction_Used loop
declare
CP1 : constant Natural := Contraction_Entries (I).CP1;
begin
if CP1 <= Max_Codepoint then
if Starter_Index (CP1).Count = 0 then
Starter_Index (CP1).Start := I;
end if;
Starter_Index (CP1).Count :=
Starter_Index (CP1).Count + 1;
end if;
end;
end loop;
-- Compute BBBB_Offset for each implicit weight range: the minimum
-- First_CP among all ranges sharing the same Base value.
-- This ensures that ranges like Tangut (17000..18AFF, FB00) and
-- Tangut Supplement (18D00..18D7F, FB00) use a single offset (17000).
for I in 1 .. Implicit_Count loop
for J in 1 .. Implicit_Count loop
if Implicit_Ranges (J).Base = Implicit_Ranges (I).Base
and then Implicit_Ranges (J).First_CP
< Implicit_Ranges (I).BBBB_Offset
then
Implicit_Ranges (I).BBBB_Offset :=
Implicit_Ranges (J).First_CP;
end if;
end loop;
end loop;
Is_Init := True;
Success := True;
end Initialize;
end Lingenic_Text.Collation;