-- 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 Ghost Specification (UTS #51)
--
-- Defines emoji sequence classification types and structural codepoint
-- constants. The classifier state machine matches the EBNF grammar from
-- UTS #51 Section 1.4.1.
--
-- All expression functions in this package are ghost-eligible (Pure) and
-- can be referenced in postconditions and loop invariants.
-------------------------------------------------------------------------------
package Lingenic_Text.Emoji_Spec
with SPARK_Mode, Pure
is
---------------------------------------------------------------------------
-- Emoji sequence classification
---------------------------------------------------------------------------
type Emoji_Sequence_Type is
(Not_Emoji,
Emoji_Character, -- Single emoji codepoint (Emoji=Yes)
Emoji_Presentation_Seq, -- emoji_character + VS16 (U+FE0F)
Emoji_Keycap_Seq, -- keycap_base + VS16 + U+20E3
Emoji_Modifier_Seq, -- emoji_modifier_base + emoji_modifier
Emoji_Flag_Seq, -- RI + RI
Emoji_Tag_Seq, -- tag_base + tag_spec+ + cancel_tag
Emoji_ZWJ_Seq); -- elements joined by ZWJ (U+200D)
---------------------------------------------------------------------------
-- Structural codepoint constants
---------------------------------------------------------------------------
VS16 : constant := 16#FE0F#; -- Variation Selector-16
Keycap : constant := 16#20E3#; -- Combining Enclosing Keycap
ZWJ : constant := 16#200D#; -- Zero Width Joiner
Cancel_Tag : constant := 16#E007F#; -- Tag Cancel
-- Regional Indicator range
RI_First : constant := 16#1F1E6#;
RI_Last : constant := 16#1F1FF#;
-- Tag specification range
Tag_First : constant := 16#E0020#;
Tag_Last : constant := 16#E007E#;
---------------------------------------------------------------------------
-- Structural predicates
---------------------------------------------------------------------------
-- Keycap base characters: # * 0..9
function Is_Keycap_Base (CP : Codepoint) return Boolean is
(CP = 16#0023# -- #
or else CP = 16#002A# -- *
or else CP in 16#0030# .. 16#0039#); -- 0..9
-- Regional Indicator
function Is_Regional_Indicator (CP : Codepoint) return Boolean is
(CP in RI_First .. RI_Last);
-- Tag specification character
function Is_Tag_Spec (CP : Codepoint) return Boolean is
(CP in Tag_First .. Tag_Last);
---------------------------------------------------------------------------
-- Classify_From_Flags — ghost classification decision
--
-- Given the accumulated flags from a linear scan, return the emoji
-- sequence type. The priority order matches UTS #51 Section 1.4.1.
-- This is the specification of what Classify_Sequence computes.
---------------------------------------------------------------------------
function Classify_From_Flags
(Is_Emoji_CP : Boolean; -- Emoji_Table(First_CP) /= 0
Is_Keycap_B : Boolean; -- Is_Keycap_Base(First_CP)
Is_Mod_Base : Boolean; -- Modifier_Base_Table(First_CP) /= 0
Is_RI_First : Boolean; -- Is_Regional_Indicator(First_CP)
Has_ZWJ : Boolean;
RI_Count : Natural;
Has_Keycap : Boolean;
Tag_Done : Boolean;
Has_Mod : Boolean;
Has_VS16 : Boolean) return Emoji_Sequence_Type
is (if not Is_RI_First and not Is_Emoji_CP then Not_Emoji
elsif Has_ZWJ then Emoji_ZWJ_Seq
elsif RI_Count >= 2 then Emoji_Flag_Seq
elsif Has_Keycap and Is_Keycap_B then Emoji_Keycap_Seq
elsif Tag_Done then Emoji_Tag_Seq
elsif Has_Mod and Is_Mod_Base then Emoji_Modifier_Seq
elsif Has_VS16 then Emoji_Presentation_Seq
elsif Is_Emoji_CP then Emoji_Character
else Not_Emoji)
with Ghost;
---------------------------------------------------------------------------
-- Input size limit for Classify_Sequence.
-- 256 bytes covers any conformant emoji sequence (the longest RGI ZWJ
-- sequences are about 75 bytes).
---------------------------------------------------------------------------
Max_Sequence_Bytes : constant := 256;
end Lingenic_Text.Emoji_Spec;