-- 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
--
-- Unicode collation (UTS #10).
--
-- Implements the Default Unicode Collation Element Table (DUCET) for
-- the Unicode Collation Algorithm:
-- Compare — multi-level comparison of two UTF-8 strings
-- Sort_Key — build a binary sort key for byte-by-byte comparison
--
-- Self-contained module with its own Initialize. Reads allkeys.txt
-- (DUCET) at init time. Requires Normalization to be initialized
-- first (NFD normalization is applied internally before collation).
--
-- Data tables:
-- CE_Index/CE_Data — per-codepoint collation element lookup
-- Contraction_Starter — flat Boolean array for contraction starters
-- Starter_Index/Entries — contraction matching tables
-- Implicit_Ranges — @implicitweights ranges from allkeys.txt
--
-- Supports Non-Ignorable and Shifted variable weighting.
-------------------------------------------------------------------------------
with Lingenic_Text.Collation_Spec;
with Lingenic_Text.Normalization;
package Lingenic_Text.Collation
with SPARK_Mode,
Abstract_State => Collation_State,
Initializes => Collation_State
is
use Collation_Spec;
---------------------------------------------------------------------------
-- Initialization
---------------------------------------------------------------------------
function Initialized return Boolean
with Global => Collation_State;
procedure Initialize
(UCD_Dir : String;
Success : out Boolean)
with Global => (Output => Collation_State,
Input => Normalization.Norm_State),
Pre => Normalization.Initialized,
Post => (if Success then Initialized);
---------------------------------------------------------------------------
-- Compare
--
-- Compare two UTF-8 strings using DUCET collation.
-- Both inputs are NFD-normalized internally before CE production.
-- Returns Less, Equal, or Greater in Result.
-- Success is False if either input is invalid UTF-8, too long, or
-- an internal buffer overflows.
---------------------------------------------------------------------------
procedure Compare
(Left : Byte_Array;
Right : Byte_Array;
Option : Variable_Weight_Option;
Result : out Comparison_Result;
Success : out Boolean)
with Pre => Initialized
and then Normalization.Initialized
and then Normalization.Data_All_Terminal
and then Left'Length >= 1
and then Right'Length >= 1
and then Left'Last < Positive'Last
and then Right'Last < Positive'Last,
Global => (Input => (Collation_State, Normalization.Norm_State));
---------------------------------------------------------------------------
-- Sort_Key
--
-- Build a binary sort key from a UTF-8 string.
-- Sort keys can be compared byte-by-byte (memcmp) for correct ordering.
-- The sort key is written into Key (Key'First .. Last).
-- On failure, Last = Key'First - 1.
---------------------------------------------------------------------------
procedure Sort_Key
(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 => (Input => (Collation_State, Normalization.Norm_State));
end Lingenic_Text.Collation;