-- 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 Ghost Specification (UTS #10)
--
-- Defines collation element types, variable weight options, comparison
-- result, and structural constants for the Unicode Collation Algorithm.
--
-- All types and expression functions in this package are ghost-eligible
-- (Pure) and can be referenced in postconditions and loop invariants.
-------------------------------------------------------------------------------
package Lingenic_Text.Collation_Spec
with SPARK_Mode, Pure
is
---------------------------------------------------------------------------
-- Weight type: 16-bit collation weight value.
---------------------------------------------------------------------------
type Weight_16 is range 0 .. 16#FFFF#;
---------------------------------------------------------------------------
-- Collation element: three weight levels + variable flag.
--
-- UTS #10 Section 3.2: a collation element consists of a primary weight,
-- a secondary weight, and a tertiary weight. Variable-weight elements
-- (marked with '*' in allkeys.txt) are handled specially in Shifted mode.
---------------------------------------------------------------------------
type Collation_Element is record
Primary : Weight_16;
Secondary : Weight_16;
Tertiary : Weight_16;
Variable : Boolean;
end record;
---------------------------------------------------------------------------
-- Variable weight processing (UTS #10 Section 4)
---------------------------------------------------------------------------
type Variable_Weight_Option is
(Non_Ignorable, -- Variable CEs sort at their assigned weights
Shifted); -- Variable CEs are shifted to a fourth level
---------------------------------------------------------------------------
-- Comparison result
---------------------------------------------------------------------------
type Comparison_Result is (Less, Equal, Greater);
---------------------------------------------------------------------------
-- Implicit weight ranges (UTS #10 §10.1.3, Unicode 17.0)
--
-- Core Han: Unified_Ideograph=True AND
-- (Block=CJK_Unified_Ideographs OR
-- Block=CJK_Compatibility_Ideographs)
-- AAAA = 0xFB40 + (CP >> 15)
--
-- Other Han: Unified_Ideograph=True AND NOT in those two blocks
-- (CJK extensions A, B, C+D, E, F, G, H+J, I)
-- AAAA = 0xFB80 + (CP >> 15)
--
-- Siniform scripts (Tangut, Tangut Components, Nushu, Khitan) use
-- @implicitweights from allkeys.txt with their own AAAA base and BBBB.
--
-- Ranges below are the Unified_Ideograph=True character boundaries
-- from PropList.txt (Unicode 17.0), NOT the block boundaries.
---------------------------------------------------------------------------
-- Core Han: Unified_Ideograph=True in Block=CJK_Unified_Ideographs
-- PropList.txt: 4E00..9FFF
CJK_Core_First : constant := 16#4E00#;
CJK_Core_Last : constant := 16#9FFF#;
-- Core Han: Unified_Ideograph=True in Block=CJK_Compatibility_Ideographs
-- PropList.txt (Unicode 17.0): FA0E..FA0F, FA11, FA13..FA14, FA1F,
-- FA21, FA23..FA24, FA27..FA29. Exact enumeration, not block range.
-- Other Han: Unified_Ideograph=True ranges outside Core Han blocks
-- (from PropList.txt, Unicode 17.0)
-- CJK Ext A: U+3400..U+4DBF
CJK_Ext_A_First : constant := 16#3400#;
CJK_Ext_A_Last : constant := 16#4DBF#;
-- CJK Ext B: U+20000..U+2A6DF
CJK_Ext_B_First : constant := 16#2_0000#;
CJK_Ext_B_Last : constant := 16#2_A6DF#;
-- CJK Ext C+D: U+2A700..U+2B81D (Unified_Ideograph boundary)
CJK_Ext_CD_First : constant := 16#2_A700#;
CJK_Ext_CD_Last : constant := 16#2_B81D#;
-- CJK Ext E: U+2B820..U+2CEAD
CJK_Ext_E_First : constant := 16#2_B820#;
CJK_Ext_E_Last : constant := 16#2_CEAD#;
-- CJK Ext F: U+2CEB0..U+2EBE0
CJK_Ext_F_First : constant := 16#2_CEB0#;
CJK_Ext_F_Last : constant := 16#2_EBE0#;
-- CJK Ext I: U+2EBF0..U+2EE5D
CJK_Ext_I_First : constant := 16#2_EBF0#;
CJK_Ext_I_Last : constant := 16#2_EE5D#;
-- CJK Ext G: U+30000..U+3134A
CJK_Ext_G_First : constant := 16#3_0000#;
CJK_Ext_G_Last : constant := 16#3_134A#;
-- CJK Ext H+J: U+31350..U+33479 (contiguous in Unified_Ideograph)
CJK_Ext_HJ_First : constant := 16#3_1350#;
CJK_Ext_HJ_Last : constant := 16#3_3479#;
---------------------------------------------------------------------------
-- Implicit weight base values (UTS #10 Table 16)
---------------------------------------------------------------------------
Implicit_Base_Core_Han : constant Weight_16 := 16#FB40#;
Implicit_Base_Other_Han : constant Weight_16 := 16#FB80#;
Implicit_Base_Unassigned : constant Weight_16 := 16#FBC0#;
---------------------------------------------------------------------------
-- Predicates for implicit weight categories
---------------------------------------------------------------------------
function Is_Core_Han (CP : Codepoint) return Boolean is
(CP in CJK_Core_First .. CJK_Core_Last
or else CP in 16#FA0E# .. 16#FA0F#
or else CP = 16#FA11#
or else CP in 16#FA13# .. 16#FA14#
or else CP = 16#FA1F#
or else CP = 16#FA21#
or else CP in 16#FA23# .. 16#FA24#
or else CP in 16#FA27# .. 16#FA29#);
function Is_Other_Han (CP : Codepoint) return Boolean is
(CP in CJK_Ext_A_First .. CJK_Ext_A_Last
or else CP in CJK_Ext_B_First .. CJK_Ext_B_Last
or else CP in CJK_Ext_CD_First .. CJK_Ext_CD_Last
or else CP in CJK_Ext_E_First .. CJK_Ext_E_Last
or else CP in CJK_Ext_F_First .. CJK_Ext_F_Last
or else CP in CJK_Ext_I_First .. CJK_Ext_I_Last
or else CP in CJK_Ext_G_First .. CJK_Ext_G_Last
or else CP in CJK_Ext_HJ_First .. CJK_Ext_HJ_Last);
---------------------------------------------------------------------------
-- Sizing constants
---------------------------------------------------------------------------
Max_CEs : constant := 512; -- Max CEs for one comparison string
Max_Sort_Key : constant := 4096; -- Max sort key bytes
Max_Input_CPs : constant := 256; -- Max codepoints in one input string
---------------------------------------------------------------------------
-- Ghost: Implicit weight computation (UTS #10 §10.1.3)
--
-- For codepoints NOT in DUCET and NOT in @implicitweights ranges
-- (siniform scripts), the implicit CE pair is:
-- [.AAAA.0020.0002][.BBBB.0000.0000]
--
-- These ghost functions encode the AAAA/BBBB formulas for Core Han,
-- Other Han, and unassigned codepoints. Siniform ranges are runtime-
-- table-driven and cannot be specified in a Pure ghost package.
---------------------------------------------------------------------------
function Implicit_AAAA (CP : Codepoint) return Natural
is (if Is_Core_Han (CP)
then Natural (Implicit_Base_Core_Han) + CP / 16#8000#
elsif Is_Other_Han (CP)
then Natural (Implicit_Base_Other_Han) + CP / 16#8000#
else Natural (Implicit_Base_Unassigned) + CP / 16#8000#)
with Ghost;
function Implicit_BBBB (CP : Codepoint) return Natural
is ((CP mod 16#8000#) + 16#8000#)
with Ghost;
---------------------------------------------------------------------------
-- Ghost: Lexicographic comparison of sort key byte arrays
--
-- UTS #10 §7.3: sort keys are compared byte-by-byte. The result is
-- determined by the first differing byte, or by length if all common
-- bytes match (shorter key is Less).
---------------------------------------------------------------------------
function Compare_Keys
(Left_Len : Natural;
Right_Len : Natural;
All_Equal : Boolean) return Comparison_Result
is (if All_Equal and then Left_Len < Right_Len then Less
elsif All_Equal and then Left_Len > Right_Len then Greater
elsif All_Equal then Equal
else Equal) -- unreachable: caller asserts All_Equal
with Ghost;
---------------------------------------------------------------------------
-- Ghost: Recursive byte-by-byte comparison
--
-- Models the full lexicographic comparison of two sort key byte arrays.
-- Starting at position Pos, compare Left(Pos) vs Right(Pos):
-- - If Pos exceeds both lengths: Equal
-- - If Pos exceeds Left only: Less (shorter key)
-- - If Pos exceeds Right only: Greater
-- - If bytes differ: Less or Greater
-- - If bytes match: recurse at Pos + 1
--
-- The postcondition on Compare references this function to prove the
-- comparison result is correct for all inputs.
---------------------------------------------------------------------------
function Ghost_Compare_Bytes
(Left : Byte_Array;
Left_Len : Natural;
Right : Byte_Array;
Right_Len : Natural;
Pos : Positive) return Comparison_Result
is (if Pos > Left_Len and then Pos > Right_Len then Equal
elsif Pos > Left_Len then Less
elsif Pos > Right_Len then Greater
elsif Left (Pos) < Right (Pos) then Less
elsif Left (Pos) > Right (Pos) then Greater
else Ghost_Compare_Bytes (Left, Left_Len, Right, Right_Len, Pos + 1))
with Ghost,
Pre => Left'First = 1
and then Right'First = 1
and then Left_Len <= Left'Last
and then Right_Len <= Right'Last
and then Left'Last < Positive'Last
and then Right'Last < Positive'Last
and then Pos >= 1,
Subprogram_Variant => (Decreases =>
Natural'Max (Left_Len, Right_Len) - Pos + 1);
end Lingenic_Text.Collation_Spec;