-- 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 — Case Mapping body
--
-- Self-contained case mapping module. Initialize reads UnicodeData.txt
-- (simple case mappings), SpecialCasing.txt (full multi-char mappings),
-- CaseFolding.txt (case fold), and DerivedCoreProperties.txt
-- (Uppercase/Lowercase boolean properties for Is_Cased).
--
-- Initialize is SPARK_Mode Off: file I/O, string parsing.
--
-- All runtime procedures (Uppercase, Lowercase, Titlecase, Casefold,
-- Is_Cased, Is_Case_Ignorable) are SPARK_Mode On.
--
-- Uppercase, Lowercase, and Casefold use the Text_Transform generic.
-- Titlecase is standalone (word-boundary-aware via the Words module).
-------------------------------------------------------------------------------
with Lingenic_Text.File_IO;
with Lingenic_Text.UTF8;
with Lingenic_Text.UCD_Parser;
with Lingenic_Text.Words_Spec;
package body Lingenic_Text.Case_Mapping
with SPARK_Mode,
Refined_State => (Case_State =>
(Is_Init,
Upper_Index, Upper_Data, Upper_Used,
Lower_Index, Lower_Data, Lower_Used,
Title_Index, Title_Data, Title_Used,
Fold_Index, Fold_Data, Fold_Used,
Cased_Table, Case_Ignorable_Table,
Init_UD_Buffer, Init_UD_Length,
Init_SC_Buffer, Init_SC_Length,
Init_CF_Buffer, Init_CF_Length,
Init_DCP_Buffer, Init_DCP_Length,
Init_Upper_Prop, Init_Lower_Prop))
is
use Case_Mapping_Spec;
---------------------------------------------------------------------------
-- Constants
---------------------------------------------------------------------------
Max_Map_Data : constant := 10_000;
---------------------------------------------------------------------------
-- Data types
---------------------------------------------------------------------------
-- Per-codepoint index into packed mapping data.
-- 0 = self-mapping (no change). > 0 = offset into corresponding data
-- array; data at that offset: [length, cp1, cp2, ...].
type Map_Index_Type is array (0 .. Max_Codepoint) of Natural;
-- Packed mapping data. Entries are stored as: length at offset,
-- then length codepoints following.
type Map_Data_Type is array (1 .. Max_Map_Data) of Natural;
-- Boolean property table, one per codepoint.
type Bool_Table_Type is array (0 .. Max_Codepoint) of Boolean;
---------------------------------------------------------------------------
-- State variables
---------------------------------------------------------------------------
Is_Init : Boolean := False;
Upper_Index : Map_Index_Type := [others => 0];
Upper_Data : Map_Data_Type := [others => 0];
Upper_Used : Natural := 0;
Lower_Index : Map_Index_Type := [others => 0];
Lower_Data : Map_Data_Type := [others => 0];
Lower_Used : Natural := 0;
Title_Index : Map_Index_Type := [others => 0];
Title_Data : Map_Data_Type := [others => 0];
Title_Used : Natural := 0;
Fold_Index : Map_Index_Type := [others => 0];
Fold_Data : Map_Data_Type := [others => 0];
Fold_Used : Natural := 0;
Cased_Table : Bool_Table_Type := [others => False];
Case_Ignorable_Table : Bool_Table_Type := [others => False];
---------------------------------------------------------------------------
-- Init-time temporaries (package-level to avoid stack overflow)
---------------------------------------------------------------------------
Init_UD_Buffer : File_IO.File_Byte_Array := [others => 0];
Init_UD_Length : File_IO.File_Size := 0;
Init_SC_Buffer : File_IO.File_Byte_Array := [others => 0];
Init_SC_Length : File_IO.File_Size := 0;
Init_CF_Buffer : File_IO.File_Byte_Array := [others => 0];
Init_CF_Length : File_IO.File_Size := 0;
Init_DCP_Buffer : File_IO.File_Byte_Array := [others => 0];
Init_DCP_Length : File_IO.File_Size := 0;
-- Temporary boolean property arrays for Uppercase/Lowercase
Init_Upper_Prop : Bool_Table_Type := [others => False];
Init_Lower_Prop : Bool_Table_Type := [others => False];
---------------------------------------------------------------------------
-- Initialized
---------------------------------------------------------------------------
function Initialized return Boolean is (Is_Init);
---------------------------------------------------------------------------
-- Is_Cased
---------------------------------------------------------------------------
function Is_Cased (CP : Codepoint) return Boolean is
(Cased_Table (CP));
---------------------------------------------------------------------------
-- Is_Case_Ignorable
---------------------------------------------------------------------------
function Is_Case_Ignorable (CP : Codepoint) return Boolean is
(Case_Ignorable_Table (CP));
---------------------------------------------------------------------------
-- Mapping accessor functions — body implementations
--
-- These expose the internal table structure for ghost specification
-- functions. The logic matches Write_Mapping's table lookup:
-- Index(CP) = 0 → self-mapping (len=1, CP maps to itself)
-- Index(CP) > 0 → Data(Index(CP)) = length, Data(Index(CP)+I) = CPs
--
-- Out-of-range indices fall back to self-mapping (same as Write_Mapping).
---------------------------------------------------------------------------
function Map_Len_From
(CP : Codepoint;
Idx : Map_Index_Type;
Data : Map_Data_Type;
Used : Natural) return Natural
is (if Idx (CP) = 0 then 1
elsif Used > Max_Map_Data
or else Idx (CP) > Used
or else Idx (CP) > Max_Map_Data
then 1
elsif Data (Idx (CP)) < 1 or Data (Idx (CP)) > Max_Mapping_Len
then 1
else Data (Idx (CP)));
function Map_CP_From
(CP : Codepoint;
I : Positive;
Idx : Map_Index_Type;
Data : Map_Data_Type;
Used : Natural) return Codepoint
is (if Idx (CP) = 0 then CP
elsif Used > Max_Map_Data
or else Idx (CP) > Used
or else Idx (CP) > Max_Map_Data
then CP
elsif Data (Idx (CP)) < 1 or Data (Idx (CP)) > Max_Mapping_Len
then CP
elsif Idx (CP) > Max_Map_Data - I
then CP
elsif Data (Idx (CP) + I) > Max_Codepoint
then CP
else Data (Idx (CP) + I));
function Get_Upper_Map_Len (CP : Codepoint) return Natural
is (Map_Len_From (CP, Upper_Index, Upper_Data, Upper_Used));
function Get_Upper_Map_CP (CP : Codepoint; Idx : Positive) return Codepoint
is (Map_CP_From (CP, Idx, Upper_Index, Upper_Data, Upper_Used));
function Get_Fold_Map_Len (CP : Codepoint) return Natural
is (Map_Len_From (CP, Fold_Index, Fold_Data, Fold_Used));
function Get_Fold_Map_CP (CP : Codepoint; Idx : Positive) return Codepoint
is (Map_CP_From (CP, Idx, Fold_Index, Fold_Data, Fold_Used));
function Get_Lower_Map_Len (CP : Codepoint) return Natural
is (Map_Len_From (CP, Lower_Index, Lower_Data, Lower_Used));
function Get_Lower_Map_CP (CP : Codepoint; Idx : Positive) return Codepoint
is (Map_CP_From (CP, Idx, Lower_Index, Lower_Data, Lower_Used));
function Get_Title_Map_Len (CP : Codepoint) return Natural
is (Map_Len_From (CP, Title_Index, Title_Data, Title_Used));
function Get_Title_Map_CP (CP : Codepoint; Idx : Positive) return Codepoint
is (Map_CP_From (CP, Idx, Title_Index, Title_Data, Title_Used));
---------------------------------------------------------------------------
-- CP_Enc_Len — non-ghost UTF-8 encoded byte count
--
-- Identical to UTF8_Spec.Encoded_Length but non-ghost, so it can
-- appear in non-ghost postconditions.
---------------------------------------------------------------------------
function CP_Enc_Len (CP : Codepoint) return Positive
is (if CP <= 16#7F# then 1
elsif CP <= 16#7FF# then 2
elsif CP <= 16#FFFF# then 3
else 4);
---------------------------------------------------------------------------
-- Map_Written_Bytes — compute exact output byte count for one mapping
--
-- This is the body-level version of Ghost_Upper_Out_Bytes/Ghost_Fold_Out_Bytes
-- that works with any Index/Data/Used triple. It mirrors the logic in
-- Write_Mapping exactly: self-mapping produces CP_Enc_Len(CP),
-- table mapping produces the sum of CP_Enc_Len for each mapped CP.
---------------------------------------------------------------------------
function Map_Written_Bytes
(CP : Codepoint;
Index : Map_Index_Type;
Data : Map_Data_Type;
Used : Natural) return Positive
is (case Map_Len_From (CP, Index, Data, Used) is
when 1 =>
CP_Enc_Len (Map_CP_From (CP, 1, Index, Data, Used)),
when 2 =>
CP_Enc_Len (Map_CP_From (CP, 1, Index, Data, Used))
+ CP_Enc_Len (Map_CP_From (CP, 2, Index, Data, Used)),
when 3 =>
CP_Enc_Len (Map_CP_From (CP, 1, Index, Data, Used))
+ CP_Enc_Len (Map_CP_From (CP, 2, Index, Data, Used))
+ CP_Enc_Len (Map_CP_From (CP, 3, Index, Data, Used)),
when others =>
CP_Enc_Len (CP));
---------------------------------------------------------------------------
-- Ghost lemma: CP_Enc_Len = UTF8_Spec.Encoded_Length
--
-- Both are defined identically but the solver sometimes needs a hint
-- that two expression functions with the same body are equal.
---------------------------------------------------------------------------
procedure Lemma_Enc_Len_Eq (CP : Codepoint) with
Ghost,
Post => CP_Enc_Len (CP) = UTF8_Spec.Encoded_Length (CP)
is
begin
null;
end Lemma_Enc_Len_Eq;
---------------------------------------------------------------------------
-- Ghost lemma: Map_Written_Bytes = Ghost_Upper_Out_Bytes
--
-- Bridges the body-level Map_Written_Bytes (which uses CP_Enc_Len and
-- direct table access) to the spec-level Ghost_Upper_Out_Bytes (which
-- uses UTF8_Spec.Encoded_Length and Get_Upper_Map_Len/Get_Upper_Map_CP).
---------------------------------------------------------------------------
procedure Lemma_Upper_Bytes_Eq (CP : Codepoint) with
Ghost,
Pre => Initialized,
Post => Map_Written_Bytes (CP, Upper_Index, Upper_Data, Upper_Used) =
Ghost_Upper_Out_Bytes (CP)
is
L : constant Natural := Get_Upper_Map_Len (CP);
begin
-- Assert accessor equivalence (expression function, solver sees through)
pragma Assert (L = Map_Len_From (CP, Upper_Index, Upper_Data, Upper_Used));
if L = 1 then
declare
MC : constant Codepoint := Get_Upper_Map_CP (CP, 1);
begin
pragma Assert (MC = Map_CP_From (CP, 1, Upper_Index, Upper_Data,
Upper_Used));
Lemma_Enc_Len_Eq (MC);
end;
elsif L = 2 then
declare
MC1 : constant Codepoint := Get_Upper_Map_CP (CP, 1);
MC2 : constant Codepoint := Get_Upper_Map_CP (CP, 2);
begin
pragma Assert (MC1 = Map_CP_From (CP, 1, Upper_Index, Upper_Data,
Upper_Used));
pragma Assert (MC2 = Map_CP_From (CP, 2, Upper_Index, Upper_Data,
Upper_Used));
Lemma_Enc_Len_Eq (MC1);
Lemma_Enc_Len_Eq (MC2);
end;
elsif L = 3 then
declare
MC1 : constant Codepoint := Get_Upper_Map_CP (CP, 1);
MC2 : constant Codepoint := Get_Upper_Map_CP (CP, 2);
MC3 : constant Codepoint := Get_Upper_Map_CP (CP, 3);
begin
pragma Assert (MC1 = Map_CP_From (CP, 1, Upper_Index, Upper_Data,
Upper_Used));
pragma Assert (MC2 = Map_CP_From (CP, 2, Upper_Index, Upper_Data,
Upper_Used));
pragma Assert (MC3 = Map_CP_From (CP, 3, Upper_Index, Upper_Data,
Upper_Used));
Lemma_Enc_Len_Eq (MC1);
Lemma_Enc_Len_Eq (MC2);
Lemma_Enc_Len_Eq (MC3);
end;
else
-- L = 0 or L > 3: "others" branch, both return Encoded_Length(CP)
Lemma_Enc_Len_Eq (CP);
end if;
end Lemma_Upper_Bytes_Eq;
procedure Lemma_Fold_Bytes_Eq (CP : Codepoint) with
Ghost,
Pre => Initialized,
Post => Map_Written_Bytes (CP, Fold_Index, Fold_Data, Fold_Used) =
Ghost_Fold_Out_Bytes (CP)
is
L : constant Natural := Get_Fold_Map_Len (CP);
begin
pragma Assert (L = Map_Len_From (CP, Fold_Index, Fold_Data, Fold_Used));
if L = 1 then
declare
MC : constant Codepoint := Get_Fold_Map_CP (CP, 1);
begin
pragma Assert (MC = Map_CP_From (CP, 1, Fold_Index, Fold_Data,
Fold_Used));
Lemma_Enc_Len_Eq (MC);
end;
elsif L = 2 then
declare
MC1 : constant Codepoint := Get_Fold_Map_CP (CP, 1);
MC2 : constant Codepoint := Get_Fold_Map_CP (CP, 2);
begin
pragma Assert (MC1 = Map_CP_From (CP, 1, Fold_Index, Fold_Data,
Fold_Used));
pragma Assert (MC2 = Map_CP_From (CP, 2, Fold_Index, Fold_Data,
Fold_Used));
Lemma_Enc_Len_Eq (MC1);
Lemma_Enc_Len_Eq (MC2);
end;
elsif L = 3 then
declare
MC1 : constant Codepoint := Get_Fold_Map_CP (CP, 1);
MC2 : constant Codepoint := Get_Fold_Map_CP (CP, 2);
MC3 : constant Codepoint := Get_Fold_Map_CP (CP, 3);
begin
pragma Assert (MC1 = Map_CP_From (CP, 1, Fold_Index, Fold_Data,
Fold_Used));
pragma Assert (MC2 = Map_CP_From (CP, 2, Fold_Index, Fold_Data,
Fold_Used));
pragma Assert (MC3 = Map_CP_From (CP, 3, Fold_Index, Fold_Data,
Fold_Used));
Lemma_Enc_Len_Eq (MC1);
Lemma_Enc_Len_Eq (MC2);
Lemma_Enc_Len_Eq (MC3);
end;
else
Lemma_Enc_Len_Eq (CP);
end if;
end Lemma_Fold_Bytes_Eq;
---------------------------------------------------------------------------
-- Ghost lemma: Map_Written_Bytes = Ghost_Lower_Out_Bytes (non-sigma)
--
-- For non-sigma codepoints, the lower table drives both the runtime
-- and ghost paths. Sigma is handled separately by Lemma_Sigma_Bytes.
---------------------------------------------------------------------------
procedure Lemma_Lower_Bytes_Eq (CP : Codepoint) with
Ghost,
Pre => Initialized
and then CP /= Greek_Capital_Sigma,
Post => Map_Written_Bytes (CP, Lower_Index, Lower_Data, Lower_Used) =
Ghost_Lower_Out_Bytes (CP)
is
L : constant Natural := Get_Lower_Map_Len (CP);
begin
pragma Assert (L = Map_Len_From (CP, Lower_Index, Lower_Data, Lower_Used));
if L = 1 then
declare
MC : constant Codepoint := Get_Lower_Map_CP (CP, 1);
begin
pragma Assert (MC = Map_CP_From (CP, 1, Lower_Index, Lower_Data,
Lower_Used));
Lemma_Enc_Len_Eq (MC);
end;
elsif L = 2 then
declare
MC1 : constant Codepoint := Get_Lower_Map_CP (CP, 1);
MC2 : constant Codepoint := Get_Lower_Map_CP (CP, 2);
begin
pragma Assert (MC1 = Map_CP_From (CP, 1, Lower_Index, Lower_Data,
Lower_Used));
pragma Assert (MC2 = Map_CP_From (CP, 2, Lower_Index, Lower_Data,
Lower_Used));
Lemma_Enc_Len_Eq (MC1);
Lemma_Enc_Len_Eq (MC2);
end;
elsif L = 3 then
declare
MC1 : constant Codepoint := Get_Lower_Map_CP (CP, 1);
MC2 : constant Codepoint := Get_Lower_Map_CP (CP, 2);
MC3 : constant Codepoint := Get_Lower_Map_CP (CP, 3);
begin
pragma Assert (MC1 = Map_CP_From (CP, 1, Lower_Index, Lower_Data,
Lower_Used));
pragma Assert (MC2 = Map_CP_From (CP, 2, Lower_Index, Lower_Data,
Lower_Used));
pragma Assert (MC3 = Map_CP_From (CP, 3, Lower_Index, Lower_Data,
Lower_Used));
Lemma_Enc_Len_Eq (MC1);
Lemma_Enc_Len_Eq (MC2);
Lemma_Enc_Len_Eq (MC3);
end;
else
Lemma_Enc_Len_Eq (CP);
end if;
end Lemma_Lower_Bytes_Eq;
---------------------------------------------------------------------------
-- Ghost lemma: Map_Written_Bytes(Title) = Ghost_Title_Out_Bytes
---------------------------------------------------------------------------
procedure Lemma_Title_Bytes_Eq (CP : Codepoint) with
Ghost,
Pre => Initialized,
Post => Map_Written_Bytes (CP, Title_Index, Title_Data, Title_Used) =
Ghost_Title_Out_Bytes (CP)
is
L : constant Natural := Get_Title_Map_Len (CP);
begin
pragma Assert (L = Map_Len_From (CP, Title_Index, Title_Data, Title_Used));
if L = 1 then
declare
MC : constant Codepoint := Get_Title_Map_CP (CP, 1);
begin
pragma Assert (MC = Map_CP_From (CP, 1, Title_Index, Title_Data,
Title_Used));
Lemma_Enc_Len_Eq (MC);
end;
elsif L = 2 then
declare
MC1 : constant Codepoint := Get_Title_Map_CP (CP, 1);
MC2 : constant Codepoint := Get_Title_Map_CP (CP, 2);
begin
pragma Assert (MC1 = Map_CP_From (CP, 1, Title_Index, Title_Data,
Title_Used));
pragma Assert (MC2 = Map_CP_From (CP, 2, Title_Index, Title_Data,
Title_Used));
Lemma_Enc_Len_Eq (MC1);
Lemma_Enc_Len_Eq (MC2);
end;
elsif L = 3 then
declare
MC1 : constant Codepoint := Get_Title_Map_CP (CP, 1);
MC2 : constant Codepoint := Get_Title_Map_CP (CP, 2);
MC3 : constant Codepoint := Get_Title_Map_CP (CP, 3);
begin
pragma Assert (MC1 = Map_CP_From (CP, 1, Title_Index, Title_Data,
Title_Used));
pragma Assert (MC2 = Map_CP_From (CP, 2, Title_Index, Title_Data,
Title_Used));
pragma Assert (MC3 = Map_CP_From (CP, 3, Title_Index, Title_Data,
Title_Used));
Lemma_Enc_Len_Eq (MC1);
Lemma_Enc_Len_Eq (MC2);
Lemma_Enc_Len_Eq (MC3);
end;
else
Lemma_Enc_Len_Eq (CP);
end if;
end Lemma_Title_Bytes_Eq;
---------------------------------------------------------------------------
-- Ghost lemma: Map_Written_Bytes(Lower) = Ghost_Plain_Lower_Bytes
--
-- Bridges the body-level Map_Written_Bytes with the lower table to
-- Ghost_Plain_Lower_Bytes. Works for ALL codepoints including sigma.
-- Used by Titlecase where the lower table is applied without
-- Final_Sigma context.
---------------------------------------------------------------------------
procedure Lemma_Plain_Lower_Bytes_Eq (CP : Codepoint) with
Ghost,
Pre => Initialized,
Post => Map_Written_Bytes (CP, Lower_Index, Lower_Data, Lower_Used) =
Ghost_Plain_Lower_Bytes (CP)
is
L : constant Natural := Get_Lower_Map_Len (CP);
begin
pragma Assert (L = Map_Len_From (CP, Lower_Index, Lower_Data, Lower_Used));
if L = 1 then
declare
MC : constant Codepoint := Get_Lower_Map_CP (CP, 1);
begin
pragma Assert (MC = Map_CP_From (CP, 1, Lower_Index, Lower_Data,
Lower_Used));
Lemma_Enc_Len_Eq (MC);
end;
elsif L = 2 then
declare
MC1 : constant Codepoint := Get_Lower_Map_CP (CP, 1);
MC2 : constant Codepoint := Get_Lower_Map_CP (CP, 2);
begin
pragma Assert (MC1 = Map_CP_From (CP, 1, Lower_Index, Lower_Data,
Lower_Used));
pragma Assert (MC2 = Map_CP_From (CP, 2, Lower_Index, Lower_Data,
Lower_Used));
Lemma_Enc_Len_Eq (MC1);
Lemma_Enc_Len_Eq (MC2);
end;
elsif L = 3 then
declare
MC1 : constant Codepoint := Get_Lower_Map_CP (CP, 1);
MC2 : constant Codepoint := Get_Lower_Map_CP (CP, 2);
MC3 : constant Codepoint := Get_Lower_Map_CP (CP, 3);
begin
pragma Assert (MC1 = Map_CP_From (CP, 1, Lower_Index, Lower_Data,
Lower_Used));
pragma Assert (MC2 = Map_CP_From (CP, 2, Lower_Index, Lower_Data,
Lower_Used));
pragma Assert (MC3 = Map_CP_From (CP, 3, Lower_Index, Lower_Data,
Lower_Used));
Lemma_Enc_Len_Eq (MC1);
Lemma_Enc_Len_Eq (MC2);
Lemma_Enc_Len_Eq (MC3);
end;
else
Lemma_Enc_Len_Eq (CP);
end if;
end Lemma_Plain_Lower_Bytes_Eq;
---------------------------------------------------------------------------
-- Ghost lemma: sigma variant byte count = Ghost_Lower_Out_Bytes(Sigma)
--
-- Both Greek_Small_Sigma (U+03C3) and Greek_Small_Final (U+03C2) are
-- in the range 0x80..0x7FF, producing 2-byte UTF-8 sequences.
-- Ghost_Lower_Out_Bytes(Greek_Capital_Sigma) also evaluates to 2.
---------------------------------------------------------------------------
procedure Lemma_Sigma_Bytes (Sigma_Variant : Codepoint) with
Ghost,
Pre => Initialized
and then (Sigma_Variant = Greek_Small_Sigma
or Sigma_Variant = Greek_Small_Final),
Post => UTF8_Spec.Encoded_Length (Sigma_Variant) =
Ghost_Lower_Out_Bytes (Greek_Capital_Sigma)
is
begin
null;
end Lemma_Sigma_Bytes;
---------------------------------------------------------------------------
-- Write_CP — encode a single codepoint to UTF-8 output
---------------------------------------------------------------------------
procedure Write_CP
(CP : Codepoint;
Output : in out Byte_Array;
Pos : in out Natural;
OK : in out Boolean)
with Pre => Output'Last < Positive'Last
and then Pos >= Output'First
and then Pos <= Output'Last + 1
and then OK,
Post => Pos >= Pos'Old
and then Pos <= Output'Last + 1
and then (if OK then
Pos = Pos'Old + UTF8_Spec.Encoded_Length (CP))
is
Len : Natural;
begin
-- Determine UTF-8 encoded length
if CP <= 16#7F# then
Len := 1;
elsif CP <= 16#7FF# then
Len := 2;
elsif CP <= 16#FFFF# then
Len := 3;
else
Len := 4;
end if;
-- Check output space
if Pos > Output'Last - Len + 1 then
OK := False;
return;
end if;
-- Encode
if Len = 1 then
Output (Pos) := CP;
Pos := Pos + 1;
elsif Len = 2 then
Output (Pos) := 16#C0# + CP / 64;
Output (Pos + 1) := 16#80# + CP mod 64;
Pos := Pos + 2;
elsif Len = 3 then
Output (Pos) := 16#E0# + CP / 4096;
Output (Pos + 1) := 16#80# + (CP / 64) mod 64;
Output (Pos + 2) := 16#80# + CP mod 64;
Pos := Pos + 3;
else
Output (Pos) := 16#F0# + CP / 262144;
Output (Pos + 1) := 16#80# + (CP / 4096) mod 64;
Output (Pos + 2) := 16#80# + (CP / 64) mod 64;
Output (Pos + 3) := 16#80# + CP mod 64;
Pos := Pos + 4;
end if;
end Write_CP;
---------------------------------------------------------------------------
-- Write_Mapping — look up and encode a case mapping to output
--
-- If Index(CP) = 0, the codepoint maps to itself.
-- Otherwise, Data(Index(CP)) is the length, followed by codepoints.
---------------------------------------------------------------------------
procedure Write_Mapping
(CP : Codepoint;
Index : Map_Index_Type;
Data : Map_Data_Type;
Used : Natural;
Output : in out Byte_Array;
Pos : in out Natural;
OK : in out Boolean)
with Pre => Output'Last < Positive'Last
and then Pos >= Output'First
and then Pos <= Output'Last + 1
and then OK,
Post => Pos >= Pos'Old
and then Pos <= Output'Last + 1
and then (if OK then
Pos - Pos'Old = Map_Written_Bytes
(CP, Index, Data, Used))
is
Idx : constant Natural := Index (CP);
Map_Len : Natural;
begin
if Idx = 0 then
-- Self-mapping: encode CP directly
Write_CP (CP, Output, Pos, OK);
elsif Used > Max_Map_Data
or else Idx > Used
or else Idx > Max_Map_Data
then
-- Invalid index → self-map fallback
Write_CP (CP, Output, Pos, OK);
else
Map_Len := Data (Idx);
if Map_Len < 1 or Map_Len > Max_Mapping_Len then
-- Invalid length → self-map fallback
Write_CP (CP, Output, Pos, OK);
elsif Map_Len = 1 then
-- 1-codepoint mapping
if Idx > Max_Map_Data - 1 then
OK := False; return;
end if;
declare
M : constant Natural := Data (Idx + 1);
begin
if M > Max_Codepoint then
OK := False; return;
end if;
Write_CP (M, Output, Pos, OK);
end;
elsif Map_Len = 2 then
-- 2-codepoint mapping
if Idx > Max_Map_Data - 2 then
OK := False; return;
end if;
declare
M1 : constant Natural := Data (Idx + 1);
M2 : constant Natural := Data (Idx + 2);
begin
if M1 > Max_Codepoint or M2 > Max_Codepoint then
OK := False; return;
end if;
Write_CP (M1, Output, Pos, OK);
if not OK then return; end if;
Write_CP (M2, Output, Pos, OK);
end;
else -- Map_Len = 3
-- 3-codepoint mapping
if Idx > Max_Map_Data - 3 then
OK := False; return;
end if;
declare
M1 : constant Natural := Data (Idx + 1);
M2 : constant Natural := Data (Idx + 2);
M3 : constant Natural := Data (Idx + 3);
begin
if M1 > Max_Codepoint or M2 > Max_Codepoint
or M3 > Max_Codepoint
then
OK := False; return;
end if;
Write_CP (M1, Output, Pos, OK);
if not OK then return; end if;
Write_CP (M2, Output, Pos, OK);
if not OK then return; end if;
Write_CP (M3, Output, Pos, OK);
end;
end if;
end if;
end Write_Mapping;
---------------------------------------------------------------------------
-- Public wrappers
---------------------------------------------------------------------------
procedure Uppercase
(Input : Byte_Array;
Output : in out Byte_Array;
Last : out Natural;
Status : out Case_Status)
is
Pos : Positive := Input'First;
Out_Pos : Natural := Output'First;
CP : Codepoint;
Len : Positive;
Valid : Boolean;
OK : Boolean := True;
begin
while Pos <= Input'Last loop
pragma Loop_Invariant (Pos >= Input'First);
pragma Loop_Invariant (Pos <= Input'Last);
pragma Loop_Invariant (Out_Pos >= Output'First);
pragma Loop_Invariant (Out_Pos <= Output'Last + 1);
pragma Loop_Invariant (Out_Pos - Output'First <= Max_Out_Acc);
pragma Loop_Invariant (OK);
-- Accumulator-recursion equivalence
pragma Loop_Invariant
(Ghost_Upper_Out (Input, Pos, Out_Pos - Output'First) =
Ghost_Upper_Total (Input));
pragma Loop_Variant (Increases => Pos);
UTF8.Decode (Input, Pos, CP, Len, Valid);
if not Valid then
Status := Invalid_Input;
Last := Output'First - 1;
return;
end if;
-- Connect decoded CP to ghost CP
pragma Assert (CP = Ghost_CP (Input, Pos));
pragma Assert (Len = Ghost_Step_Length (Input, Pos));
-- Snapshot output position before writing
declare
Old_Acc : constant Natural := Out_Pos - Output'First with Ghost;
begin
-- Write the uppercase mapping to output
Write_Mapping (CP, Upper_Index, Upper_Data, Upper_Used,
Output, Out_Pos, OK);
if not OK then
Status := Buffer_Overflow;
Last := Output'First - 1;
return;
end if;
-- Bridge: connect body-level Map_Written_Bytes to ghost
Lemma_Upper_Bytes_Eq (CP);
pragma Assert (Out_Pos - Output'First =
Old_Acc + Ghost_Upper_Out_Bytes (CP));
-- Advance past this codepoint and unfold ghost recursion
if Pos > Input'Last - Len + 1 then
-- Last codepoint: terminal branch of Ghost_Upper_Out
-- Ghost_Upper_Out(Input, Pos, Old_Acc) =
-- Old_Acc + Ghost_Upper_Out_Bytes(Ghost_CP(Input, Pos))
pragma Assert (Old_Acc <= Max_Out_Acc);
Pos := Input'Last + 1;
else
-- Recursive branch: Ghost_Upper_Out(Input, Pos, Old_Acc)
-- = Ghost_Upper_Out(Input, Pos + Step, Old_Acc + Bytes)
-- After advancing, Out_Pos - Output'First = Old_Acc + Bytes
-- and the invariant re-establishes at new Pos.
pragma Assert (Old_Acc <= Max_Out_Acc);
Pos := Pos + Len;
end if;
end;
end loop;
-- Post-loop: Pos > Input'Last, so Ghost_Upper_Out returns Acc
pragma Assert (Out_Pos - Output'First = Ghost_Upper_Total (Input));
-- Success
if Out_Pos = Output'First then
Status := Buffer_Overflow;
Last := Output'First - 1;
else
Last := Out_Pos - 1;
Status := Success;
end if;
end Uppercase;
procedure Lowercase
(Input : Byte_Array;
Output : in out Byte_Array;
Last : out Natural;
Status : out Case_Status)
is
Pos : Positive := Input'First;
Out_Pos : Natural := Output'First;
CP : Codepoint;
Len : Positive;
Valid : Boolean;
OK : Boolean := True;
-- Final_Sigma context: tracks whether a Cased character preceded
-- the current position (Case_Ignorable chars are transparent).
Prev_Was_Cased : Boolean := False;
begin
while Pos <= Input'Last loop
pragma Loop_Invariant (Pos >= Input'First);
pragma Loop_Invariant (Pos <= Input'Last);
pragma Loop_Invariant (Out_Pos >= Output'First);
pragma Loop_Invariant (Out_Pos <= Output'Last + 1);
pragma Loop_Invariant (Out_Pos - Output'First <= Max_Out_Acc);
pragma Loop_Invariant (OK);
-- Accumulator-recursion equivalence
pragma Loop_Invariant
(Ghost_Lower_Out (Input, Pos, Out_Pos - Output'First) =
Ghost_Lower_Total (Input));
pragma Loop_Variant (Increases => Pos);
UTF8.Decode (Input, Pos, CP, Len, Valid);
if not Valid then
Status := Invalid_Input;
Last := Output'First - 1;
return;
end if;
-- Connect decoded CP to ghost CP
pragma Assert (CP = Ghost_CP (Input, Pos));
pragma Assert (Len = Ghost_Step_Length (Input, Pos));
-- Snapshot output position before writing
declare
Old_Acc : constant Natural := Out_Pos - Output'First with Ghost;
begin
if CP = Greek_Capital_Sigma then
-- Final_Sigma resolution via forward scan.
-- Scan forward past Case_Ignorable characters to find
-- whether the next non-Case_Ignorable character is Cased.
declare
Followed : Boolean := False;
Sigma_Result : Codepoint;
begin
-- Forward scan (read-only — does not modify Output/Out_Pos)
if Pos <= Input'Last - Len + 1 then
declare
Scan_Pos : Positive := Pos + Len;
Scan_CP : Codepoint;
Scan_Len : Positive;
Scan_OK : Boolean;
begin
while Scan_Pos <= Input'Last loop
pragma Loop_Invariant (Scan_Pos >= Input'First);
pragma Loop_Invariant (Scan_Pos <= Input'Last);
pragma Loop_Invariant (Out_Pos = Out_Pos'Loop_Entry);
pragma Loop_Invariant (OK);
pragma Loop_Variant (Increases => Scan_Pos);
UTF8.Decode (Input, Scan_Pos, Scan_CP,
Scan_Len, Scan_OK);
if not Scan_OK then
exit;
end if;
if Cased_Table (Scan_CP) then
Followed := True;
exit;
elsif not Case_Ignorable_Table (Scan_CP) then
exit;
end if;
if Scan_Pos > Input'Last - Scan_Len + 1 then
exit;
end if;
Scan_Pos := Scan_Pos + Scan_Len;
end loop;
end;
end if;
-- Resolve: Final_Sigma when preceded by Cased and
-- not followed by Cased.
if Prev_Was_Cased and not Followed then
Sigma_Result := Greek_Small_Final;
else
Sigma_Result := Greek_Small_Sigma;
end if;
Write_CP (Sigma_Result, Output, Out_Pos, OK);
if not OK then
Status := Buffer_Overflow;
Last := Output'First - 1;
return;
end if;
-- Bridge: sigma variant byte count = ghost byte count
Lemma_Sigma_Bytes (Sigma_Result);
end;
-- Sigma is Cased: update context for subsequent characters
Prev_Was_Cased := True;
else
-- Non-sigma: standard lowercase table mapping
Write_Mapping (CP, Lower_Index, Lower_Data, Lower_Used,
Output, Out_Pos, OK);
if not OK then
Status := Buffer_Overflow;
Last := Output'First - 1;
return;
end if;
-- Update Final_Sigma context:
-- Case_Ignorable characters are transparent.
if Cased_Table (CP) then
Prev_Was_Cased := True;
elsif not Case_Ignorable_Table (CP) then
Prev_Was_Cased := False;
end if;
-- Bridge: Map_Written_Bytes = Ghost_Lower_Out_Bytes
Lemma_Lower_Bytes_Eq (CP);
end if;
-- Common bridge: both paths produce Ghost_Lower_Out_Bytes bytes
pragma Assert (Out_Pos - Output'First =
Old_Acc + Ghost_Lower_Out_Bytes (CP));
-- Advance past this codepoint and unfold ghost recursion
if Pos > Input'Last - Len + 1 then
pragma Assert (Old_Acc <= Max_Out_Acc);
Pos := Input'Last + 1;
else
pragma Assert (Old_Acc <= Max_Out_Acc);
Pos := Pos + Len;
end if;
end;
end loop;
-- Post-loop: Pos > Input'Last, so Ghost_Lower_Out returns Acc
pragma Assert (Out_Pos - Output'First = Ghost_Lower_Total (Input));
-- Success
if Out_Pos = Output'First then
Status := Buffer_Overflow;
Last := Output'First - 1;
else
Last := Out_Pos - 1;
Status := Success;
end if;
end Lowercase;
procedure Casefold
(Input : Byte_Array;
Output : in out Byte_Array;
Last : out Natural;
Status : out Case_Status)
is
Pos : Positive := Input'First;
Out_Pos : Natural := Output'First;
CP : Codepoint;
Len : Positive;
Valid : Boolean;
OK : Boolean := True;
begin
while Pos <= Input'Last loop
pragma Loop_Invariant (Pos >= Input'First);
pragma Loop_Invariant (Pos <= Input'Last);
pragma Loop_Invariant (Out_Pos >= Output'First);
pragma Loop_Invariant (Out_Pos <= Output'Last + 1);
pragma Loop_Invariant (Out_Pos - Output'First <= Max_Out_Acc);
pragma Loop_Invariant (OK);
-- Accumulator-recursion equivalence
pragma Loop_Invariant
(Ghost_Fold_Out (Input, Pos, Out_Pos - Output'First) =
Ghost_Fold_Total (Input));
pragma Loop_Variant (Increases => Pos);
UTF8.Decode (Input, Pos, CP, Len, Valid);
if not Valid then
Status := Invalid_Input;
Last := Output'First - 1;
return;
end if;
pragma Assert (CP = Ghost_CP (Input, Pos));
pragma Assert (Len = Ghost_Step_Length (Input, Pos));
declare
Old_Acc : constant Natural := Out_Pos - Output'First with Ghost;
begin
Write_Mapping (CP, Fold_Index, Fold_Data, Fold_Used,
Output, Out_Pos, OK);
if not OK then
Status := Buffer_Overflow;
Last := Output'First - 1;
return;
end if;
-- Bridge: connect body-level Map_Written_Bytes to ghost
Lemma_Fold_Bytes_Eq (CP);
pragma Assert (Out_Pos - Output'First =
Old_Acc + Ghost_Fold_Out_Bytes (CP));
if Pos > Input'Last - Len + 1 then
pragma Assert (Old_Acc <= Max_Out_Acc);
Pos := Input'Last + 1;
else
pragma Assert (Old_Acc <= Max_Out_Acc);
Pos := Pos + Len;
end if;
end;
end loop;
pragma Assert (Out_Pos - Output'First = Ghost_Fold_Total (Input));
if Out_Pos = Output'First then
Status := Buffer_Overflow;
Last := Output'First - 1;
else
Last := Out_Pos - 1;
Status := Success;
end if;
end Casefold;
---------------------------------------------------------------------------
-- Titlecase — single-loop with inline word break detection
--
-- Platinum postcondition: output byte count = Ghost_Title_Total(Input).
--
-- Ghost structure:
-- Ghost_Title_Scan processes codepoints one at a time, checking
-- Ghost_Break at each position to detect word boundaries and reset
-- Found_Cased.
--
-- The first codepoint is handled separately (WB1: always a word start).
-- Then the main loop processes subsequent codepoints, tracking WB state
-- and Found_Cased inline.
---------------------------------------------------------------------------
procedure Titlecase
(Input : Byte_Array;
Output : in out Byte_Array;
Last : out Natural;
Status : out Case_Status)
is
use Words_Spec;
use type Words.WB_State;
Pos : Positive := Input'First;
Out_Pos : Natural := Output'First;
CP : Codepoint;
Len : Positive;
Valid : Boolean;
OK : Boolean := True;
-- Word break state machine (mirrors Words module)
Prev_Actual : WBP_Value;
Prev_Eff : WBP_Value;
Before_Prev_Eff : WBP_Value;
RI_Count : Natural;
-- Per-word state
Found_Cased : Boolean;
-- Max RI counter (same as Words module)
WB_Max_RI : constant := Natural'Last - 1;
begin
-- Process the first codepoint (WB1: always a word start)
UTF8.Decode (Input, Pos, CP, Len, Valid);
if not Valid then
Status := Invalid_Input;
Last := Output'First - 1;
return;
end if;
pragma Assert (CP = Ghost_CP (Input, Pos));
pragma Assert (Len = Ghost_Step_Length (Input, Pos));
-- First CP is always start of first word → Found_Cased = False
-- Process based on case status
declare
Old_Acc : constant Natural := Out_Pos - Output'First with Ghost;
begin
if Cased_Table (CP) then
-- First cased character: titlecase mapping
Write_Mapping (CP, Title_Index, Title_Data, Title_Used,
Output, Out_Pos, OK);
if not OK then
Status := Buffer_Overflow;
Last := Output'First - 1;
return;
end if;
Lemma_Title_Bytes_Eq (CP);
Found_Cased := True;
else
-- Uncased: pass through
Write_CP (CP, Output, Out_Pos, OK);
if not OK then
Status := Buffer_Overflow;
Last := Output'First - 1;
return;
end if;
Lemma_Enc_Len_Eq (CP);
Found_Cased := False;
end if;
pragma Assert (Out_Pos - Output'First =
Old_Acc + Ghost_Title_CP_Bytes (CP, False));
pragma Assert (Out_Pos - Output'First =
Ghost_Title_First_Bytes (Input));
end;
-- Check for single-codepoint input
if Pos > Input'Last - Len + 1 then
-- Only one codepoint: output the first CP's bytes
Last := Out_Pos - 1;
Status := Success;
return;
end if;
-- Initialize WB state from first codepoint
declare
First_WBP_Idx : UCD_Parser.Property_Index;
First_WBP : WBP_Value;
begin
if Valid then
First_WBP_Idx := Properties.Get_WBP (CP);
else
First_WBP_Idx := 0;
end if;
First_WBP := Properties.WBP_To_Abstract (First_WBP_Idx);
Prev_Actual := First_WBP;
Prev_Eff := First_WBP;
Before_Prev_Eff := WBP_Other;
RI_Count := (if First_WBP = WBP_Regional_Indicator then 1 else 0);
-- Connect to ghost Initial_State
pragma Assert (First_WBP = Words.Ghost_WBP (Input, Input'First));
pragma Assert (Prev_Eff = Words.Initial_State (Input, Input'First).Prev_Eff);
pragma Assert (Before_Prev_Eff =
Words.Initial_State (Input, Input'First).Before_Prev_Eff);
pragma Assert (RI_Count =
Words.Initial_State (Input, Input'First).RI_Count);
end;
Pos := Pos + Len;
-- Main loop: process subsequent codepoints
while Pos <= Input'Last loop
pragma Loop_Invariant (Pos >= Input'First + 1);
pragma Loop_Invariant (Pos <= Input'Last);
pragma Loop_Invariant (Out_Pos >= Output'First);
pragma Loop_Invariant (Out_Pos <= Output'Last + 1);
pragma Loop_Invariant (Out_Pos - Output'First <= Max_Out_Acc);
pragma Loop_Invariant (OK);
pragma Loop_Invariant (RI_Count < WB_Max_RI);
-- Accumulator-recursion equivalence
pragma Loop_Invariant
(Ghost_Title_Scan
(Input, Pos, Found_Cased,
Words.WB_State'(Prev_Actual, Prev_Eff,
Before_Prev_Eff, RI_Count),
Out_Pos - Output'First) =
Ghost_Title_Total (Input));
pragma Loop_Variant (Increases => Pos);
-- Decode current codepoint
UTF8.Decode (Input, Pos, CP, Len, Valid);
if not Valid then
Status := Invalid_Input;
Last := Output'First - 1;
return;
end if;
pragma Assert (CP = Ghost_CP (Input, Pos));
pragma Assert (Len = Ghost_Step_Length (Input, Pos));
-- Look up WBP and ExtPict for word break detection
declare
WBP_Idx : UCD_Parser.Property_Index;
This_WBP : WBP_Value;
This_EP : Boolean;
Is_Break : Boolean;
-- Lookahead
After_Found : Boolean;
After_WBP : WBP_Value;
-- Ghost state snapshot
Old_St : constant Words.WB_State :=
Words.WB_State'(Prev_Actual, Prev_Eff,
Before_Prev_Eff, RI_Count)
with Ghost;
begin
if Valid then
WBP_Idx := Properties.Get_WBP (CP);
This_EP := Properties.Get_ExtPict (CP);
else
WBP_Idx := 0;
This_EP := False;
end if;
This_WBP := Properties.WBP_To_Abstract (WBP_Idx);
pragma Assert (This_WBP = Words.Ghost_WBP (Input, Pos));
pragma Assert (This_EP = Words.Ghost_ExtPict (Input, Pos));
-- Lookahead for WB6, WB7b, WB12
if Is_MidLetter_Or_MidNumLetQ (This_WBP)
or This_WBP = WBP_Double_Quote
or Is_MidNum_Or_MidNumLetQ (This_WBP)
then
if Pos + Len <= Input'Last + 1 then
Words.Scan_After_B
(Input, Pos + Len, After_Found, After_WBP);
else
After_Found := False;
After_WBP := WBP_Other;
end if;
else
After_Found := False;
After_WBP := WBP_Other;
end if;
pragma Assert (After_Found =
Words.Ghost_After_Found_At (Input, Pos));
pragma Assert (After_WBP =
Words.Ghost_After_WBP_At (Input, Pos));
-- Break decision
Is_Break := Is_Word_Break
(A_Actual => Prev_Actual,
A_Eff => Prev_Eff,
B_WBP => This_WBP,
B_ExtPict => This_EP,
Before_A => Before_Prev_Eff,
After_B => After_WBP,
Has_After => After_Found,
RI_Count_Odd => RI_Count mod 2 = 1);
pragma Assert (Is_Break = Words.Ghost_Break (Old_St, Input, Pos));
-- Reset Found_Cased at word boundaries
if Is_Break then
Found_Cased := False;
end if;
-- Snapshot for proof bridge
declare
Old_Acc : constant Natural :=
Out_Pos - Output'First with Ghost;
Was_Found : constant Boolean :=
Found_Cased with Ghost;
begin
-- Process CP based on case status within current word
if not Found_Cased and then Cased_Table (CP) then
-- First cased in word: titlecase mapping
Write_Mapping (CP, Title_Index, Title_Data, Title_Used,
Output, Out_Pos, OK);
if not OK then
Status := Buffer_Overflow;
Last := Output'First - 1;
return;
end if;
Lemma_Title_Bytes_Eq (CP);
Found_Cased := True;
elsif Found_Cased then
-- Subsequent in word: lowercase mapping
Write_Mapping (CP, Lower_Index, Lower_Data, Lower_Used,
Output, Out_Pos, OK);
if not OK then
Status := Buffer_Overflow;
Last := Output'First - 1;
return;
end if;
Lemma_Plain_Lower_Bytes_Eq (CP);
else
-- Uncased before first cased: pass through
Write_CP (CP, Output, Out_Pos, OK);
if not OK then
Status := Buffer_Overflow;
Last := Output'First - 1;
return;
end if;
Lemma_Enc_Len_Eq (CP);
end if;
-- Bridge: all paths produce Ghost_Title_CP_Bytes bytes
pragma Assert (Out_Pos - Output'First =
Old_Acc + Ghost_Title_CP_Bytes (CP, Was_Found));
end;
-- Update WB state (same logic as Words module)
if Is_Ignored (This_WBP)
and not Is_Newline_Or_CRLF (Prev_Eff)
then
Prev_Actual := This_WBP;
else
Before_Prev_Eff := Prev_Eff;
Prev_Eff := This_WBP;
Prev_Actual := This_WBP;
if This_WBP = WBP_Regional_Indicator then
if RI_Count < WB_Max_RI - 1 then
RI_Count := RI_Count + 1;
end if;
else
RI_Count := 0;
end if;
end if;
-- Connect runtime state to ghost Updated_State
pragma Assert
(Words.WB_State'(Prev_Actual, Prev_Eff,
Before_Prev_Eff, RI_Count)
= Words.Updated_State (Old_St, Input, Pos));
-- Advance past this codepoint
if Pos > Input'Last - Len + 1 then
Pos := Input'Last + 1;
else
Pos := Pos + Len;
end if;
end;
end loop;
-- Post-loop: Pos > Input'Last, so Ghost_Title_Scan returns Acc
pragma Assert (Out_Pos - Output'First = Ghost_Title_Total (Input));
-- Success
if Out_Pos = Output'First then
Status := Buffer_Overflow;
Last := Output'First - 1;
else
Last := Out_Pos - 1;
Status := Success;
end if;
end Titlecase;
---------------------------------------------------------------------------
-- Initialize
---------------------------------------------------------------------------
procedure Initialize
(UCD_Dir : String;
Success : out Boolean)
with SPARK_Mode => Off
is
File_OK : Boolean;
-- Helper: parse hex codepoint from ASCII bytes at position P.
-- Advances P past the hex digits. Sets Result to 0 on failure.
procedure Parse_Hex
(Buf : File_IO.File_Byte_Array;
Len : File_IO.File_Size;
P : in out Natural;
Result : out Natural)
is
Digit_Count : Natural := 0;
begin
Result := 0;
while P <= Len
and then Is_Hex_Digit (Buf (P))
loop
if Result > 16#10_FFFF# then
Result := 0;
return;
end if;
Result := Result * 16 + Hex_Value (Buf (P));
Digit_Count := Digit_Count + 1;
P := P + 1;
end loop;
if Digit_Count = 0 then
Result := 0;
end if;
end Parse_Hex;
-- Helper: skip spaces in buffer at position P
procedure Skip_Spaces
(Buf : File_IO.File_Byte_Array;
Len : File_IO.File_Size;
P : in out Natural)
is
begin
while P <= Len and then Buf (P) = Space_Byte loop
P := P + 1;
end loop;
end Skip_Spaces;
-- Helper: add a mapping entry to an index+data table
procedure Add_Mapping
(CP : Natural;
CPs : in out Map_Data_Type;
Idx : in out Map_Index_Type;
Used : in out Natural;
Targets : Map_Data_Type;
T_Count : Natural;
T_Start : Natural)
is
begin
if CP > Max_Codepoint then
return;
end if;
if T_Count < 1 or T_Count > Max_Mapping_Len then
return;
end if;
if Used + T_Count + 1 > Max_Map_Data then
return;
end if;
Used := Used + 1;
Idx (CP) := Used;
CPs (Used) := T_Count;
for I in 0 .. T_Count - 1 loop
Used := Used + 1;
CPs (Used) := Targets (T_Start + I);
end loop;
end Add_Mapping;
-- Helper: add a single-codepoint mapping
procedure Add_Simple
(CP : Natural;
Target : Natural;
CPs : in out Map_Data_Type;
Idx : in out Map_Index_Type;
Used : in out Natural)
is
begin
if CP > Max_Codepoint or Target > Max_Codepoint then
return;
end if;
if Idx (CP) /= 0 then
-- Already has a mapping (e.g. from SpecialCasing override)
return;
end if;
if Used + 2 > Max_Map_Data then
return;
end if;
Used := Used + 1;
Idx (CP) := Used;
CPs (Used) := 1;
Used := Used + 1;
CPs (Used) := Target;
end Add_Simple;
-- Helper: get the Nth semicolon-delimited field from a line in
-- UnicodeData.txt. Returns the start position and length.
-- Field 0 is the first field before the first semicolon.
procedure Get_UD_Field
(Buf : File_IO.File_Byte_Array;
Start : Natural;
Eol : Natural;
Field : Natural;
F_Start : out Natural;
F_Len : out Natural)
is
P : Natural := Start;
Count : Natural := 0;
begin
F_Start := Start;
F_Len := 0;
-- Skip to the right field
while Count < Field and P <= Eol loop
if Buf (P) = Semicolon_Byte then
Count := Count + 1;
end if;
P := P + 1;
end loop;
F_Start := P;
F_Len := 0;
-- Measure field length
while P <= Eol and then Buf (P) /= Semicolon_Byte loop
F_Len := F_Len + 1;
P := P + 1;
end loop;
end Get_UD_Field;
-- Parse UnicodeData.txt for simple case mappings (fields 12, 13, 14)
procedure Parse_UnicodeData is
P : Natural := 1;
Eol : Natural;
F_Start : Natural;
F_Len : Natural;
CP : Natural;
HP : Natural;
Target : Natural;
begin
while P <= Init_UD_Length loop
-- Find end of line
Eol := P;
while Eol <= Init_UD_Length
and then not Is_Line_End (Init_UD_Buffer (Eol))
loop
Eol := Eol + 1;
end loop;
Eol := Eol - 1;
-- Skip empty/comment lines
if Eol >= P and then Init_UD_Buffer (P) /= Hash_Byte then
-- Field 0: codepoint
HP := P;
Parse_Hex (Init_UD_Buffer, Init_UD_Length, HP, CP);
if CP <= Max_Codepoint then
-- Field 12: Simple_Uppercase_Mapping
Get_UD_Field (Init_UD_Buffer, P, Eol, 12,
F_Start, F_Len);
if F_Len > 0 then
HP := F_Start;
Parse_Hex (Init_UD_Buffer, Init_UD_Length, HP, Target);
if Target > 0 and Target <= Max_Codepoint then
Add_Simple (CP, Target, Upper_Data, Upper_Index,
Upper_Used);
-- Titlecase defaults to uppercase if not specified
end if;
end if;
-- Field 13: Simple_Lowercase_Mapping
Get_UD_Field (Init_UD_Buffer, P, Eol, 13,
F_Start, F_Len);
if F_Len > 0 then
HP := F_Start;
Parse_Hex (Init_UD_Buffer, Init_UD_Length, HP, Target);
if Target > 0 and Target <= Max_Codepoint then
Add_Simple (CP, Target, Lower_Data, Lower_Index,
Lower_Used);
end if;
end if;
-- Field 14: Simple_Titlecase_Mapping
Get_UD_Field (Init_UD_Buffer, P, Eol, 14,
F_Start, F_Len);
if F_Len > 0 then
HP := F_Start;
Parse_Hex (Init_UD_Buffer, Init_UD_Length, HP, Target);
if Target > 0 and Target <= Max_Codepoint then
Add_Simple (CP, Target, Title_Data, Title_Index,
Title_Used);
end if;
else
-- If no titlecase mapping, use uppercase mapping
if Upper_Index (CP) /= 0 then
-- Copy the uppercase entry to titlecase
declare
UI : constant Natural := Upper_Index (CP);
begin
if UI <= Upper_Used and then
Upper_Data (UI) = 1 and then
UI + 1 <= Upper_Used
then
Add_Simple (CP, Upper_Data (UI + 1),
Title_Data, Title_Index, Title_Used);
end if;
end;
end if;
end if;
end if;
end if;
-- Advance to next line
while P <= Init_UD_Length
and then not Is_Line_End (Init_UD_Buffer (P))
loop
P := P + 1;
end loop;
-- Skip line ending
if P <= Init_UD_Length and then Init_UD_Buffer (P) = CR_Byte then
P := P + 1;
end if;
if P <= Init_UD_Length and then Init_UD_Buffer (P) = LF_Byte then
P := P + 1;
end if;
end loop;
end Parse_UnicodeData;
-- Parse SpecialCasing.txt for unconditional full mappings.
-- Format: code; lower; title; upper; (condition_list)? # comment
-- We only parse entries WITHOUT a condition_list.
procedure Parse_SpecialCasing is
P : Natural := 1;
Eol : Natural;
HP : Natural;
CP : Natural;
SC_Num : Natural;
-- Temporary for parsing a multi-CP field
Tmp : Map_Data_Type := [others => 0];
Tmp_Count : Natural;
-- Helper: count semicolons before hash or eol
function Count_Semicolons return Natural is
S : Natural := P;
N : Natural := 0;
begin
while S <= Eol loop
if Init_SC_Buffer (S) = Hash_Byte then
exit;
end if;
if Init_SC_Buffer (S) = Semicolon_Byte then
N := N + 1;
end if;
S := S + 1;
end loop;
return N;
end Count_Semicolons;
-- Helper: parse a field of space-separated hex codepoints.
-- Starts at HP, reads until semicolon.
-- Stores codepoints in Tmp starting at Tmp_Start.
procedure Parse_CP_Field
(Tmp_Start : Natural;
Count : out Natural)
is
T : Natural := HP;
begin
Count := 0;
Skip_Spaces (Init_SC_Buffer, Init_SC_Length, T);
while T <= Eol
and then Init_SC_Buffer (T) /= Semicolon_Byte
loop
if Is_Hex_Digit (Init_SC_Buffer (T)) then
declare
Val : Natural;
begin
Parse_Hex (Init_SC_Buffer, Init_SC_Length, T, Val);
if Val <= Max_Codepoint
and then Count < Max_Mapping_Len
then
Count := Count + 1;
Tmp (Tmp_Start + Count - 1) := Val;
end if;
end;
end if;
Skip_Spaces (Init_SC_Buffer, Init_SC_Length, T);
end loop;
HP := T;
end Parse_CP_Field;
-- Helper: advance HP past the next semicolon
procedure Skip_Past_Semi is
begin
while HP <= Eol
and then Init_SC_Buffer (HP) /= Semicolon_Byte
loop
HP := HP + 1;
end loop;
if HP <= Eol then
HP := HP + 1; -- skip the semicolon
end if;
end Skip_Past_Semi;
begin
while P <= Init_SC_Length loop
-- Find end of line
Eol := P;
while Eol <= Init_SC_Length
and then not Is_Line_End (Init_SC_Buffer (Eol))
loop
Eol := Eol + 1;
end loop;
Eol := Eol - 1;
-- Skip comment/empty lines
if Eol >= P
and then Init_SC_Buffer (P) /= Hash_Byte
and then Init_SC_Buffer (P) /= LF_Byte
and then Init_SC_Buffer (P) /= CR_Byte
then
-- Count semicolons: unconditional entries have exactly 4
-- (code; lower; title; upper; # comment).
-- Conditional entries have 5+ (extra condition field).
SC_Num := Count_Semicolons;
if SC_Num = 4 then
-- Unconditional entry
HP := P;
Skip_Spaces (Init_SC_Buffer, Init_SC_Length, HP);
Parse_Hex (Init_SC_Buffer, Init_SC_Length, HP, CP);
if CP > 0 and CP <= Max_Codepoint then
-- Skip past first semicolon (after code field)
Skip_Past_Semi;
-- Field 2: lowercase mapping
Tmp_Count := 0;
Parse_CP_Field (1, Tmp_Count);
if Tmp_Count >= 1 then
-- Override existing mapping
Lower_Index (CP) := 0; -- clear old
Add_Mapping (CP, Lower_Data, Lower_Index,
Lower_Used, Tmp, Tmp_Count, 1);
end if;
Skip_Past_Semi;
-- Field 3: titlecase mapping
Tmp_Count := 0;
Parse_CP_Field (1, Tmp_Count);
if Tmp_Count >= 1 then
Title_Index (CP) := 0;
Add_Mapping (CP, Title_Data, Title_Index,
Title_Used, Tmp, Tmp_Count, 1);
end if;
Skip_Past_Semi;
-- Field 4: uppercase mapping
Tmp_Count := 0;
Parse_CP_Field (1, Tmp_Count);
if Tmp_Count >= 1 then
Upper_Index (CP) := 0;
Add_Mapping (CP, Upper_Data, Upper_Index,
Upper_Used, Tmp, Tmp_Count, 1);
end if;
end if;
end if;
end if;
-- Advance to next line
while P <= Init_SC_Length
and then not Is_Line_End (Init_SC_Buffer (P))
loop
P := P + 1;
end loop;
if P <= Init_SC_Length and then Init_SC_Buffer (P) = CR_Byte then
P := P + 1;
end if;
if P <= Init_SC_Length and then Init_SC_Buffer (P) = LF_Byte then
P := P + 1;
end if;
end loop;
end Parse_SpecialCasing;
-- Parse CaseFolding.txt for status C and F entries.
-- Format: codepoint; status; mapping(s); # comment
procedure Parse_CaseFolding is
P : Natural := 1;
Eol : Natural;
HP : Natural;
CP : Natural;
Status_Byte : Natural;
Tmp : Map_Data_Type := [others => 0];
Tmp_Count : Natural;
begin
while P <= Init_CF_Length loop
-- Find end of line
Eol := P;
while Eol <= Init_CF_Length
and then not Is_Line_End (Init_CF_Buffer (Eol))
loop
Eol := Eol + 1;
end loop;
Eol := Eol - 1;
-- Skip comment/empty lines
if Eol >= P
and then Init_CF_Buffer (P) /= Hash_Byte
and then Init_CF_Buffer (P) /= LF_Byte
and then Init_CF_Buffer (P) /= CR_Byte
then
-- Parse codepoint
HP := P;
Skip_Spaces (Init_CF_Buffer, Init_CF_Length, HP);
Parse_Hex (Init_CF_Buffer, Init_CF_Length, HP, CP);
-- Skip past semicolon
while HP <= Eol
and then Init_CF_Buffer (HP) /= Semicolon_Byte
loop
HP := HP + 1;
end loop;
if HP <= Eol then
HP := HP + 1;
end if;
-- Parse status (single letter after spaces)
Skip_Spaces (Init_CF_Buffer, Init_CF_Length, HP);
if HP <= Eol then
Status_Byte := Init_CF_Buffer (HP);
HP := HP + 1;
else
Status_Byte := 0;
end if;
-- Only process C (Common) and F (Full) entries
-- C = 67, F = 70
if (Status_Byte = 67 or Status_Byte = 70)
and CP > 0 and CP <= Max_Codepoint
then
-- Skip past semicolon to mapping field
while HP <= Eol
and then Init_CF_Buffer (HP) /= Semicolon_Byte
loop
HP := HP + 1;
end loop;
if HP <= Eol then
HP := HP + 1;
end if;
-- Parse mapping codepoints
Tmp_Count := 0;
Skip_Spaces (Init_CF_Buffer, Init_CF_Length, HP);
while HP <= Eol
and then Init_CF_Buffer (HP) /= Semicolon_Byte
and then Init_CF_Buffer (HP) /= Hash_Byte
loop
if Is_Hex_Digit (Init_CF_Buffer (HP)) then
declare
Val : Natural;
begin
Parse_Hex (Init_CF_Buffer,
Init_CF_Length, HP, Val);
if Val <= Max_Codepoint
and then Tmp_Count < Max_Mapping_Len
then
Tmp_Count := Tmp_Count + 1;
Tmp (Tmp_Count) := Val;
end if;
end;
end if;
Skip_Spaces (Init_CF_Buffer, Init_CF_Length, HP);
end loop;
if Tmp_Count >= 1 then
-- Override any existing fold mapping
Fold_Index (CP) := 0;
if Tmp_Count = 1 then
Add_Simple (CP, Tmp (1), Fold_Data, Fold_Index,
Fold_Used);
else
Add_Mapping (CP, Fold_Data, Fold_Index,
Fold_Used, Tmp, Tmp_Count, 1);
end if;
end if;
end if;
end if;
-- Advance to next line
while P <= Init_CF_Length
and then not Is_Line_End (Init_CF_Buffer (P))
loop
P := P + 1;
end loop;
if P <= Init_CF_Length and then Init_CF_Buffer (P) = CR_Byte then
P := P + 1;
end if;
if P <= Init_CF_Length and then Init_CF_Buffer (P) = LF_Byte then
P := P + 1;
end if;
end loop;
end Parse_CaseFolding;
-- Parse DerivedCoreProperties.txt for Uppercase and Lowercase properties.
-- Format: codepoint(.codepoint)? ; property_name # comment
procedure Parse_DerivedCoreProps is
P : Natural := 1;
Eol : Natural;
HP : Natural;
CP1 : Natural;
CP2 : Natural;
Prop_Start : Natural;
Prop_Len : Natural;
-- Helper: extract trimmed property name between semicolon and hash
procedure Get_Prop_Name is
begin
-- Skip to semicolon
while HP <= Eol
and then Init_DCP_Buffer (HP) /= Semicolon_Byte
loop
HP := HP + 1;
end loop;
if HP <= Eol then
HP := HP + 1; -- skip semicolon
end if;
Skip_Spaces (Init_DCP_Buffer, Init_DCP_Length, HP);
Prop_Start := HP;
Prop_Len := 0;
while HP <= Eol
and then Init_DCP_Buffer (HP) /= Hash_Byte
and then Init_DCP_Buffer (HP) /= Space_Byte
and then not Is_Line_End (Init_DCP_Buffer (HP))
loop
Prop_Len := Prop_Len + 1;
HP := HP + 1;
end loop;
end Get_Prop_Name;
-- Helper: check if property name matches a given string
function Prop_Is (S : String) return Boolean is
begin
if Prop_Len /= S'Length then
return False;
end if;
for I in 0 .. S'Length - 1 loop
if Prop_Start + I > Init_DCP_Length then
return False;
end if;
if Init_DCP_Buffer (Prop_Start + I) /=
Character'Pos (S (S'First + I))
then
return False;
end if;
end loop;
return True;
end Prop_Is;
begin
while P <= Init_DCP_Length loop
-- Find end of line
Eol := P;
while Eol <= Init_DCP_Length
and then not Is_Line_End (Init_DCP_Buffer (Eol))
loop
Eol := Eol + 1;
end loop;
Eol := Eol - 1;
-- Skip comment/empty lines
if Eol >= P
and then Init_DCP_Buffer (P) /= Hash_Byte
and then Init_DCP_Buffer (P) /= LF_Byte
and then Init_DCP_Buffer (P) /= CR_Byte
then
-- Parse codepoint or range
HP := P;
Skip_Spaces (Init_DCP_Buffer, Init_DCP_Length, HP);
Parse_Hex (Init_DCP_Buffer, Init_DCP_Length, HP, CP1);
-- Check for range (..)
CP2 := CP1;
if HP + 1 <= Eol
and then Init_DCP_Buffer (HP) = Dot_Byte
and then Init_DCP_Buffer (HP + 1) = Dot_Byte
then
HP := HP + 2;
Parse_Hex (Init_DCP_Buffer, Init_DCP_Length, HP, CP2);
end if;
-- Get property name
Get_Prop_Name;
if CP1 <= Max_Codepoint and CP2 <= Max_Codepoint
and CP2 >= CP1
then
if Prop_Is ("Uppercase") then
for C in CP1 .. CP2 loop
Init_Upper_Prop (C) := True;
end loop;
elsif Prop_Is ("Lowercase") then
for C in CP1 .. CP2 loop
Init_Lower_Prop (C) := True;
end loop;
end if;
end if;
end if;
-- Advance to next line
while P <= Init_DCP_Length
and then not Is_Line_End (Init_DCP_Buffer (P))
loop
P := P + 1;
end loop;
if P <= Init_DCP_Length
and then Init_DCP_Buffer (P) = CR_Byte
then
P := P + 1;
end if;
if P <= Init_DCP_Length
and then Init_DCP_Buffer (P) = LF_Byte
then
P := P + 1;
end if;
end loop;
end Parse_DerivedCoreProps;
-- Build Is_Cased and Is_Case_Ignorable tables
procedure Build_Context_Tables is
GC_Idx : UCD_Parser.Property_Index;
WBP_Idx : UCD_Parser.Property_Index;
begin
for CP in 0 .. Max_Codepoint loop
-- Is_Cased (D135):
-- has Uppercase property OR has Lowercase property OR GC = Lt
if Init_Upper_Prop (CP) or Init_Lower_Prop (CP) then
Cased_Table (CP) := True;
else
GC_Idx := Properties.Get_GC (CP);
if GC_Idx >= 1 and then GC_Idx <= Properties.GC_Name_Count then
declare
N : constant String := Properties.GC_Name (GC_Idx);
begin
if N = "Lt" then
Cased_Table (CP) := True;
end if;
end;
end if;
end if;
-- Is_Case_Ignorable (D136):
-- WBP in {MidLetter, MidNumLet, Single_Quote}
-- OR GC in {Mn, Me, Cf, Lm, Sk}
GC_Idx := Properties.Get_GC (CP);
if GC_Idx >= 1 and then GC_Idx <= Properties.GC_Name_Count then
declare
N : constant String := Properties.GC_Name (GC_Idx);
begin
if N = "Mn" or N = "Me" or N = "Cf"
or N = "Lm" or N = "Sk"
then
Case_Ignorable_Table (CP) := True;
end if;
end;
end if;
if not Case_Ignorable_Table (CP) then
WBP_Idx := Properties.Get_WBP (CP);
if WBP_Idx >= 1
and then WBP_Idx <= Properties.WBP_Name_Count
then
declare
N : constant String := Properties.WBP_Name (WBP_Idx);
begin
if N = "MidLetter" or N = "MidNumLet"
or N = "Single_Quote"
then
Case_Ignorable_Table (CP) := True;
end if;
end;
end if;
end if;
end loop;
end Build_Context_Tables;
begin -- Initialize
Is_Init := False;
Success := False;
-- Reset all tables
Upper_Index := [others => 0];
Upper_Data := [others => 0];
Upper_Used := 0;
Lower_Index := [others => 0];
Lower_Data := [others => 0];
Lower_Used := 0;
Title_Index := [others => 0];
Title_Data := [others => 0];
Title_Used := 0;
Fold_Index := [others => 0];
Fold_Data := [others => 0];
Fold_Used := 0;
Cased_Table := [others => False];
Case_Ignorable_Table := [others => False];
Init_Upper_Prop := [others => False];
Init_Lower_Prop := [others => False];
-- 1. Read and parse UnicodeData.txt (simple case mappings)
File_IO.Read_File (UCD_Dir & "/UnicodeData.txt",
Init_UD_Buffer, Init_UD_Length, File_OK);
if not File_OK then
return;
end if;
Parse_UnicodeData;
-- 2. Read and parse SpecialCasing.txt (unconditional full mappings)
-- These OVERRIDE the simple mappings from UnicodeData.txt.
-- Parse SpecialCasing AFTER UnicodeData so overrides work.
-- Actually, we need to clear existing entries before overriding.
-- The Parse_SpecialCasing procedure handles this by clearing
-- the index entry before adding the new mapping.
File_IO.Read_File (UCD_Dir & "/SpecialCasing.txt",
Init_SC_Buffer, Init_SC_Length, File_OK);
if not File_OK then
return;
end if;
Parse_SpecialCasing;
-- 3. Read and parse CaseFolding.txt (C+F entries)
File_IO.Read_File (UCD_Dir & "/CaseFolding.txt",
Init_CF_Buffer, Init_CF_Length, File_OK);
if not File_OK then
return;
end if;
Parse_CaseFolding;
-- 4. Read and parse DerivedCoreProperties.txt (Uppercase/Lowercase)
File_IO.Read_File (UCD_Dir & "/DerivedCoreProperties.txt",
Init_DCP_Buffer, Init_DCP_Length, File_OK);
if not File_OK then
return;
end if;
Parse_DerivedCoreProps;
-- 5. Build Is_Cased and Is_Case_Ignorable tables
Build_Context_Tables;
Is_Init := True;
Success := True;
end Initialize;
end Lingenic_Text.Case_Mapping;