-- 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 Properties and Sequence Classification (UTS #51)
--
-- Self-contained module with its own Initialize. Reads emoji-data.txt
-- and loads 5 boolean property tables:
-- Emoji, Emoji_Presentation, Emoji_Modifier, Emoji_Modifier_Base,
-- Emoji_Component
--
-- Provides:
-- - O(1) boolean property lookups for each emoji property
-- - Classify_Sequence: classify a UTF-8 byte array as an emoji type
--
-- Does NOT depend on Properties.Initialized. The 5 emoji properties
-- are loaded independently from emoji-data.txt.
--
-- Extended_Pictographic remains in the Properties module (needed by
-- grapheme segmentation at Properties init time).
--
-- SPARK Platinum: the postcondition on Classify_Sequence references the
-- recursive ghost function Ghost_Classify_All, which simulates the forward
-- scan as an expression function. GNATprove verifies the implementation
-- matches this specification.
-------------------------------------------------------------------------------
with Lingenic_Text.Emoji_Spec;
with Lingenic_Text.UTF8_Spec;
package Lingenic_Text.Emoji
with SPARK_Mode,
Abstract_State => Emoji_State,
Initializes => Emoji_State
is
use Emoji_Spec;
---------------------------------------------------------------------------
-- Initialization
---------------------------------------------------------------------------
function Initialized return Boolean
with Global => Emoji_State;
procedure Initialize
(UCD_Dir : String;
Success : out Boolean)
with Global => (Output => Emoji_State),
Post => (if Success then Initialized);
---------------------------------------------------------------------------
-- Boolean property lookups (O(1) flat indexed by codepoint)
---------------------------------------------------------------------------
function Is_Emoji (CP : Codepoint) return Boolean
with Pre => Initialized,
Global => Emoji_State;
function Is_Emoji_Presentation (CP : Codepoint) return Boolean
with Pre => Initialized,
Global => Emoji_State;
function Is_Emoji_Modifier (CP : Codepoint) return Boolean
with Pre => Initialized,
Global => Emoji_State;
function Is_Emoji_Modifier_Base (CP : Codepoint) return Boolean
with Pre => Initialized,
Global => Emoji_State;
function Is_Emoji_Component (CP : Codepoint) return Boolean
with Pre => Initialized,
Global => Emoji_State;
---------------------------------------------------------------------------
-- Ghost state record for the emoji scan state machine
--
-- Tracks all accumulated flags during the forward scan of the input.
-- Plain record (not "with Ghost") because GNAT 15 rejects ghost types
-- as parameters. Used only in ghost expression functions.
---------------------------------------------------------------------------
type Emoji_Scan_State is record
First_CP : Codepoint;
Has_ZWJ : Boolean;
Has_VS16 : Boolean;
Has_Keycap : Boolean;
Has_Mod : Boolean;
Tag_Done : Boolean;
In_Tag : Boolean;
RI_Count : Natural;
CP_Count : Natural;
end record;
Ghost_Initial_State : constant Emoji_Scan_State :=
(First_CP => 0,
Has_ZWJ => False,
Has_VS16 => False,
Has_Keycap => False,
Has_Mod => False,
Tag_Done => False,
In_Tag => False,
RI_Count => 0,
CP_Count => 0);
---------------------------------------------------------------------------
-- Ghost helper functions
--
-- These mirror the runtime decode + property lookup logic as expression
-- functions so the solver can unfold them.
---------------------------------------------------------------------------
-- Step length at position Cur: how many bytes the codepoint consumes.
-- Mirrors UTF8.Decode: well-formed → Lead_Length, invalid → 1.
function Ghost_Step_Length
(Input : Byte_Array;
Cur : Positive) return Positive
is (if UTF8_Spec.Well_Formed_At (Input, Cur)
then UTF8_Spec.Lead_Length (Input (Cur))
else 1)
with Ghost,
Pre => Input'Last < Positive'Last
and then Cur in Input'Range;
-- Is the codepoint at Cur well-formed?
function Ghost_Valid
(Input : Byte_Array;
Cur : Positive) return Boolean
is (UTF8_Spec.Well_Formed_At (Input, Cur))
with Ghost,
Pre => Input'Last < Positive'Last
and then Cur in Input'Range;
-- Decoded codepoint at Cur.
-- Well-formed → Decoded_At, invalid → 0 (but we'll return Not_Emoji).
function Ghost_CP
(Input : Byte_Array;
Cur : Positive) return Codepoint
is (if UTF8_Spec.Well_Formed_At (Input, Cur)
then UTF8_Spec.Decoded_At (Input, Cur)
else 0)
with Ghost,
Pre => Input'Last < Positive'Last
and then Cur in Input'Range;
---------------------------------------------------------------------------
-- Ghost_Update_Scan — update scan state for one codepoint
--
-- Mirrors the flag-setting logic in the body's loop (lines 353-370).
-- The CP parameter is the decoded codepoint at the current position.
---------------------------------------------------------------------------
function Ghost_Update_Scan
(St : Emoji_Scan_State;
CP : Codepoint;
Max_CP : Natural) return Emoji_Scan_State
is (Emoji_Scan_State'
(First_CP => (if St.CP_Count = 0 then CP else St.First_CP),
Has_ZWJ => St.Has_ZWJ
or else (not Is_Regional_Indicator (CP)
and then CP = ZWJ),
Has_VS16 => St.Has_VS16
or else (not Is_Regional_Indicator (CP)
and then CP /= ZWJ
and then CP = VS16),
Has_Keycap => St.Has_Keycap
or else (not Is_Regional_Indicator (CP)
and then CP /= ZWJ
and then CP /= VS16
and then CP = Keycap),
Has_Mod => St.Has_Mod
or else (not Is_Regional_Indicator (CP)
and then CP /= ZWJ
and then CP /= VS16
and then CP /= Keycap
and then not Is_Tag_Spec (CP)
and then not (CP = Cancel_Tag
and then St.In_Tag)
and then Is_Emoji_Modifier (CP)),
Tag_Done => St.Tag_Done
or else (not Is_Regional_Indicator (CP)
and then CP /= ZWJ
and then CP /= VS16
and then CP /= Keycap
and then not Is_Tag_Spec (CP)
and then CP = Cancel_Tag
and then St.In_Tag),
In_Tag => (if Is_Tag_Spec (CP)
and then not Is_Regional_Indicator (CP)
and then CP /= ZWJ
and then CP /= VS16
and then CP /= Keycap
then True
elsif not Is_Regional_Indicator (CP)
and then CP /= ZWJ
and then CP /= VS16
and then CP /= Keycap
and then not Is_Tag_Spec (CP)
and then CP = Cancel_Tag
and then St.In_Tag
then False
else St.In_Tag),
RI_Count => (if Is_Regional_Indicator (CP)
and then St.RI_Count
< (if St.CP_Count < Max_CP
then St.CP_Count + 1
else St.CP_Count)
then St.RI_Count + 1
else St.RI_Count),
CP_Count => (if St.CP_Count < Max_CP
then St.CP_Count + 1
else St.CP_Count)))
with Ghost,
Global => Emoji_State,
Pre => Initialized
and then Max_CP <= Max_Sequence_Bytes
and then St.CP_Count <= Max_CP
and then St.RI_Count <= St.CP_Count;
---------------------------------------------------------------------------
-- Ghost_Scan_Result — final classification from accumulated state
--
-- Mirrors the classification logic after the loop (lines 382-450).
-- Calls Classify_From_Flags with booleans derived from First_CP.
---------------------------------------------------------------------------
function Ghost_Scan_Result
(St : Emoji_Scan_State) return Emoji_Sequence_Type
is (Classify_From_Flags
(Is_Emoji_CP => Is_Emoji (St.First_CP),
Is_Keycap_B => Is_Keycap_Base (St.First_CP),
Is_Mod_Base => Is_Emoji_Modifier_Base (St.First_CP),
Is_RI_First => Is_Regional_Indicator (St.First_CP),
Has_ZWJ => St.Has_ZWJ,
RI_Count => St.RI_Count,
Has_Keycap => St.Has_Keycap,
Tag_Done => St.Tag_Done,
Has_Mod => St.Has_Mod,
Has_VS16 => St.Has_VS16))
with Ghost,
Global => Emoji_State,
Pre => Initialized;
---------------------------------------------------------------------------
-- Recursive ghost function: simulates the forward scan loop.
--
-- Given Input, current position Cur, and accumulated state St,
-- returns the emoji sequence classification.
--
-- Invalid UTF-8 at any position → Not_Emoji.
-- At end of input → Ghost_Scan_Result(St).
-- Otherwise → decode, update state, recurse.
--
-- The recursion decreases Input'Last - Cur + 1 at each step because
-- Ghost_Step_Length >= 1, so Cur strictly increases.
---------------------------------------------------------------------------
function Ghost_Scan
(Input : Byte_Array;
Cur : Positive;
St : Emoji_Scan_State) return Emoji_Sequence_Type
is (if Cur not in Input'Range then
-- Past end of input: classify from accumulated state
Ghost_Scan_Result (St)
elsif not Ghost_Valid (Input, Cur) then
-- Invalid UTF-8: Not_Emoji
Not_Emoji
elsif Cur > Input'Last - Ghost_Step_Length (Input, Cur) + 1 then
-- Last codepoint: update state and classify
Ghost_Scan_Result
(Ghost_Update_Scan (St, Ghost_CP (Input, Cur), Input'Length))
else
-- More codepoints: update state and recurse
Ghost_Scan
(Input,
Cur + Ghost_Step_Length (Input, Cur),
Ghost_Update_Scan (St, Ghost_CP (Input, Cur), Input'Length)))
with Ghost,
Global => Emoji_State,
Pre => Input'Last < Positive'Last
and then Input'Length >= 1
and then Input'Length <= Max_Sequence_Bytes
and then Cur > 0
and then St.CP_Count <= Input'Length
and then St.RI_Count <= St.CP_Count
and then Initialized,
Subprogram_Variant => (Decreases => Input'Last - Cur + 1);
---------------------------------------------------------------------------
-- Top-level wrapper: classifies the entire input.
---------------------------------------------------------------------------
function Ghost_Classify_All
(Input : Byte_Array) return Emoji_Sequence_Type
is (Ghost_Scan (Input, Input'First, Ghost_Initial_State))
with Ghost,
Global => Emoji_State,
Pre => Input'Last < Positive'Last
and then Input'Length >= 1
and then Input'Length <= Max_Sequence_Bytes
and then Initialized;
---------------------------------------------------------------------------
-- Classify_Sequence
--
-- Given a UTF-8 byte array (typically one grapheme cluster as returned
-- by Next_Grapheme_Cluster_Break), classify the emoji sequence type.
--
-- The classifier implements the UTS #51 EBNF grammar:
-- possible_emoji := zwj_element (\x{200D} zwj_element)*
-- flag_sequence := \p{RI} \p{RI}
-- zwj_element := \p{Emoji} emoji_modification?
-- | flag_sequence
-- emoji_modification := \p{EMod}
-- | \x{FE0F} \x{20E3}?
-- | tag_modifier
-- tag_modifier := [\x{E0020}-\x{E007E}]+ \x{E007F}
--
-- Invalid UTF-8 or non-emoji input returns Not_Emoji.
--
-- SPARK Platinum postcondition: the result matches the recursive ghost
-- specification Ghost_Classify_All.
---------------------------------------------------------------------------
function Classify_Sequence
(Input : Byte_Array) return Emoji_Spec.Emoji_Sequence_Type
with Pre => Initialized
and then Input'Length >= 1
and then Input'Length <= Emoji_Spec.Max_Sequence_Bytes
and then Input'Last < Positive'Last,
Post => Classify_Sequence'Result = Ghost_Classify_All (Input),
Global => Emoji_State;
end Lingenic_Text.Emoji;