-- 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 — Emoji body
--
-- Self-contained emoji property module. Initialize reads emoji-data.txt
-- and loads 5 boolean property tables (Emoji, Emoji_Presentation,
-- Emoji_Modifier, Emoji_Modifier_Base, Emoji_Component).
--
-- Initialize is SPARK_Mode Off: file I/O, string parsing, Filter_By_Value.
--
-- All runtime functions (Is_Emoji, Is_Emoji_Presentation, etc. and
-- Classify_Sequence) are SPARK_Mode On.
--
-- SPARK Platinum: Classify_Sequence's loop invariant maintains the
-- accumulator-recursion equivalence with Ghost_Scan, and each return
-- point is connected to Ghost_Scan_Result via bridge assertions.
-------------------------------------------------------------------------------
with Lingenic_Text.File_IO;
with Lingenic_Text.UCD_Parser;
with Lingenic_Text.UTF8;
package body Lingenic_Text.Emoji
with SPARK_Mode,
Refined_State => (Emoji_State =>
(Is_Init,
Emoji_Table, Presentation_Table, Modifier_Table,
Modifier_Base_Table, Component_Table,
Init_Buffer, Init_Length,
Init_Filtered, Init_Filtered_Length))
is
---------------------------------------------------------------------------
-- State variables
---------------------------------------------------------------------------
Is_Init : Boolean := False;
Emoji_Table : UCD_Parser.Property_Table := [others => 0];
Presentation_Table : UCD_Parser.Property_Table := [others => 0];
Modifier_Table : UCD_Parser.Property_Table := [others => 0];
Modifier_Base_Table : UCD_Parser.Property_Table := [others => 0];
Component_Table : UCD_Parser.Property_Table := [others => 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;
Init_Filtered : File_IO.File_Byte_Array := [others => 0];
Init_Filtered_Length : File_IO.File_Size := 0;
---------------------------------------------------------------------------
-- Initialized
---------------------------------------------------------------------------
function Initialized return Boolean is (Is_Init);
---------------------------------------------------------------------------
-- Boolean property lookups (O(1) flat indexed)
---------------------------------------------------------------------------
function Is_Emoji (CP : Codepoint) return Boolean
is (Emoji_Table (CP) /= 0);
function Is_Emoji_Presentation (CP : Codepoint) return Boolean
is (Presentation_Table (CP) /= 0);
function Is_Emoji_Modifier (CP : Codepoint) return Boolean
is (Modifier_Table (CP) /= 0);
function Is_Emoji_Modifier_Base (CP : Codepoint) return Boolean
is (Modifier_Base_Table (CP) /= 0);
function Is_Emoji_Component (CP : Codepoint) return Boolean
is (Component_Table (CP) /= 0);
---------------------------------------------------------------------------
-- Initialize
---------------------------------------------------------------------------
procedure Initialize
(UCD_Dir : String;
Success : out Boolean)
with SPARK_Mode => Off
is
procedure Reset_Buffer (Buf : in out File_IO.File_Byte_Array) is
begin
for I in Buf'Range loop
Buf (I) := 0;
end loop;
end Reset_Buffer;
procedure Reset_Table (T : in out UCD_Parser.Property_Table) is
begin
for CP in T'Range loop
T (CP) := 0;
end loop;
end Reset_Table;
procedure Filter_By_Value
(Src : File_IO.File_Byte_Array;
Src_Len : File_IO.File_Size;
Target : String;
Dst : in out File_IO.File_Byte_Array;
Dst_Len : out File_IO.File_Size)
is
SP : Positive := 1;
DP : Positive := 1;
begin
Reset_Buffer (Dst);
Dst_Len := 0;
if Src_Len = 0 then return; end if;
while SP <= Src_Len loop
declare
Line_End : Positive := SP;
begin
while Line_End <= Src_Len
and then Src (Line_End) /= LF_Byte
and then Src (Line_End) /= CR_Byte
loop
Line_End := Line_End + 1;
end loop;
declare
Semi_Pos : Natural := 0;
Val_Start : Natural := 0;
Match : Boolean := False;
begin
for J in SP .. Line_End - 1 loop
if Src (J) = Semicolon_Byte then
Semi_Pos := J;
exit;
end if;
end loop;
if Semi_Pos > 0 and Semi_Pos < Line_End - 1 then
Val_Start := Semi_Pos + 1;
while Val_Start < Line_End
and then (Src (Val_Start) = Space_Byte
or Src (Val_Start) = Tab_Byte)
loop
Val_Start := Val_Start + 1;
end loop;
if Val_Start + Target'Length - 1 < Line_End then
Match := True;
for K in 0 .. Target'Length - 1 loop
if Character'Pos (Target (Target'First + K))
/= Src (Val_Start + K)
then
Match := False;
exit;
end if;
end loop;
if Match then
declare
After : constant Natural :=
Val_Start + Target'Length;
begin
if After < Line_End
and then Src (After) /= Space_Byte
and then Src (After) /= Tab_Byte
and then Src (After) /= Hash_Byte
and then Src (After) /= LF_Byte
and then Src (After) /= CR_Byte
then
Match := False;
end if;
end;
end if;
end if;
end if;
if Match then
if DP + (Line_End - SP) <= File_IO.Max_File_Size then
for J in SP .. Line_End - 1 loop
Dst (DP) := Src (J);
DP := DP + 1;
end loop;
Dst (DP) := LF_Byte;
DP := DP + 1;
end if;
end if;
end;
SP := Line_End;
if SP <= Src_Len and then Src (SP) = CR_Byte then
SP := SP + 1;
end if;
if SP <= Src_Len and then Src (SP) = LF_Byte then
SP := SP + 1;
end if;
if SP = Line_End then
SP := Src_Len + 1;
end if;
end;
end loop;
if DP > 1 then
Dst_Len := File_IO.File_Size (DP - 1);
end if;
end Filter_By_Value;
procedure Load_Property
(Name : String;
Table : out UCD_Parser.Property_Table;
OK : out Boolean)
is
Names : UCD_Parser.Value_Name_Array := [others => (First => 1, Last => 0)];
Count : UCD_Parser.Property_Index := 0;
E_OK, P_OK : Boolean;
begin
Reset_Table (Table);
OK := False;
Reset_Buffer (Init_Filtered);
Init_Filtered_Length := 0;
Filter_By_Value (Init_Buffer, Init_Length, Name,
Init_Filtered, Init_Filtered_Length);
if Init_Filtered_Length = 0 then return; end if;
UCD_Parser.Extract_Value_Names
(Init_Filtered (1 .. Init_Filtered_Length), Names, Count, E_OK);
if not E_OK or Count = 0 then return; end if;
UCD_Parser.Parse_Property_File
(Init_Filtered (1 .. Init_Filtered_Length), Names, Count, Table, P_OK);
if not P_OK then return; end if;
OK := True;
end Load_Property;
OK : Boolean;
begin
Is_Init := False;
Success := False;
Reset_Table (Emoji_Table);
Reset_Table (Presentation_Table);
Reset_Table (Modifier_Table);
Reset_Table (Modifier_Base_Table);
Reset_Table (Component_Table);
Reset_Buffer (Init_Buffer);
Init_Length := 0;
File_IO.Read_File (UCD_Dir & "/emoji-data.txt",
Init_Buffer, Init_Length, OK);
if not OK or Init_Length = 0 then return; end if;
Load_Property ("Emoji", Emoji_Table, OK);
if not OK then return; end if;
Load_Property ("Emoji_Presentation", Presentation_Table, OK);
if not OK then return; end if;
Load_Property ("Emoji_Modifier", Modifier_Table, OK);
if not OK then return; end if;
Load_Property ("Emoji_Modifier_Base", Modifier_Base_Table, OK);
if not OK then return; end if;
Load_Property ("Emoji_Component", Component_Table, OK);
if not OK then return; end if;
Is_Init := True;
Success := True;
end Initialize;
---------------------------------------------------------------------------
-- Classify_Sequence
--
-- Linear forward scan with boolean flags. The ghost state is constructed
-- inline from runtime variables (St function), following the same pattern
-- as the segmentation modules. No separate ghost variable is needed.
--
-- SPARK Platinum: the loop invariant maintains the accumulator-recursion
-- equivalence Ghost_Scan(Input, Pos, St) = Ghost_Classify_All(Input).
-- At each return point, Ghost_Scan_Result(St) = Ghost_Classify_All(Input)
-- and Result (the runtime classification) = Ghost_Scan_Result(St).
---------------------------------------------------------------------------
function Classify_Sequence
(Input : Byte_Array) return Emoji_Spec.Emoji_Sequence_Type
is
Pos : Positive := Input'First;
CP : Codepoint;
Len : Positive;
Valid : Boolean;
First_CP : Codepoint := 0;
Has_ZWJ : Boolean := False;
Has_VS16 : Boolean := False;
Has_Keycap : Boolean := False;
Has_Mod : Boolean := False;
Tag_Done : Boolean := False;
In_Tag : Boolean := False;
RI_Count : Natural := 0;
CP_Count : Natural := 0;
-- Inline ghost state constructor from runtime variables.
-- The solver sees through this expression function, so
-- Ghost_Scan(Input, Pos, St) references runtime variables directly.
function St return Emoji_Scan_State is
(Emoji_Scan_State'
(First_CP => First_CP,
Has_ZWJ => Has_ZWJ,
Has_VS16 => Has_VS16,
Has_Keycap => Has_Keycap,
Has_Mod => Has_Mod,
Tag_Done => Tag_Done,
In_Tag => In_Tag,
RI_Count => RI_Count,
CP_Count => CP_Count))
with Ghost;
-- Runtime classification from accumulated flags.
-- Structurally identical to Ghost_Scan_Result(St) when
-- Is_Emoji is unfolded to Emoji_Table(CP) /= 0, etc.
function Result return Emoji_Sequence_Type is
(if not Is_Regional_Indicator (First_CP)
and then Emoji_Table (First_CP) = 0
then Not_Emoji
elsif Has_ZWJ then Emoji_ZWJ_Seq
elsif RI_Count >= 2 then Emoji_Flag_Seq
elsif Has_Keycap and then Is_Keycap_Base (First_CP)
then Emoji_Keycap_Seq
elsif Tag_Done then Emoji_Tag_Seq
elsif Has_Mod and then Modifier_Base_Table (First_CP) /= 0
then Emoji_Modifier_Seq
elsif Has_VS16 then Emoji_Presentation_Seq
elsif Emoji_Table (First_CP) /= 0 then Emoji_Character
else Not_Emoji)
with Pre => Initialized;
begin
while Pos <= Input'Last loop
pragma Loop_Invariant (Pos >= Input'First);
pragma Loop_Invariant (Pos <= Input'Last);
pragma Loop_Invariant (CP_Count <= Input'Last - Input'First + 1);
pragma Loop_Invariant (RI_Count <= CP_Count);
-- Accumulator-recursion equivalence:
-- St constructs Emoji_Scan_State inline from runtime variables.
pragma Loop_Invariant
(Ghost_Scan (Input, Pos, St) = Ghost_Classify_All (Input));
pragma Loop_Variant (Increases => Pos);
declare
Old_St : constant Emoji_Scan_State := St with Ghost;
begin
UTF8.Decode (Input, Pos, CP, Len, Valid);
if not Valid then
-- Ghost_Scan at invalid position returns Not_Emoji
pragma Assert (not Ghost_Valid (Input, Pos));
pragma Assert (Ghost_Scan (Input, Pos, Old_St) = Not_Emoji);
return Not_Emoji;
end if;
-- Platinum: connect decoded CP to ghost CP.
pragma Assert (Valid = UTF8_Spec.Well_Formed_At (Input, Pos));
pragma Assert (CP = Ghost_CP (Input, Pos));
pragma Assert (Len = Ghost_Step_Length (Input, Pos));
-- Track codepoint count and first codepoint.
-- Set First_CP BEFORE incrementing CP_Count, so the guard
-- "CP_Count = 0" matches Ghost_Update_Scan's conditional
-- "(if St.CP_Count = 0 then CP else St.First_CP)".
if CP_Count = 0 then
First_CP := CP;
end if;
if CP_Count < Input'Last - Input'First + 1 then
CP_Count := CP_Count + 1;
end if;
-- Set flags based on structural codepoints
if Is_Regional_Indicator (CP) then
if RI_Count < CP_Count then
RI_Count := RI_Count + 1;
end if;
elsif CP = ZWJ then
Has_ZWJ := True;
elsif CP = VS16 then
Has_VS16 := True;
elsif CP = Keycap then
Has_Keycap := True;
elsif Is_Tag_Spec (CP) then
In_Tag := True;
elsif CP = Cancel_Tag and then In_Tag then
Tag_Done := True;
In_Tag := False;
elsif Modifier_Table (CP) /= 0 then
Has_Mod := True;
end if;
-- Platinum: after flag updates, runtime state (St) matches
-- Ghost_Update_Scan applied to the old state (Old_St).
-- Prove field by field so the solver handles one at a time.
declare
GU : constant Emoji_Scan_State :=
Ghost_Update_Scan (Old_St, CP, Input'Length) with Ghost;
begin
pragma Assert (St.CP_Count = GU.CP_Count);
pragma Assert (St.First_CP = GU.First_CP);
pragma Assert (St.Has_ZWJ = GU.Has_ZWJ);
pragma Assert (St.Has_VS16 = GU.Has_VS16);
pragma Assert (St.Has_Keycap = GU.Has_Keycap);
pragma Assert (St.In_Tag = GU.In_Tag);
pragma Assert (St.Tag_Done = GU.Tag_Done);
pragma Assert (St.Has_Mod = GU.Has_Mod);
pragma Assert (St.RI_Count = GU.RI_Count);
pragma Assert (St = GU);
end;
if Pos > Input'Last - Len + 1 then
-- Last codepoint: Ghost_Scan takes the "last cp" branch.
-- Ghost_Scan_Result(St) = Ghost_Classify_All(Input).
pragma Assert (Ghost_Scan_Result (St) =
Ghost_Classify_All (Input));
-- Connect runtime Result to ghost:
pragma Assert (Result = Ghost_Scan_Result (St));
return Result;
end if;
Pos := Pos + Len;
-- Re-establish for next iteration
pragma Assert
(Ghost_Scan (Input, Pos, St) = Ghost_Classify_All (Input));
end;
end loop;
-- Normal exit: last codepoint ended exactly at Input'Last.
-- Pos > Input'Last, so Ghost_Scan returns Ghost_Scan_Result(St).
pragma Assert (Ghost_Scan_Result (St) = Ghost_Classify_All (Input));
pragma Assert (Result = Ghost_Scan_Result (St));
return Result;
end Classify_Sequence;
end Lingenic_Text.Emoji;