-- 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
-- Formally Verified Unicode Text Processing Library
--
-- Property lookup API.
--
-- Provides O(1) indexed lookup for Unicode character properties.
-- Tables are populated at runtime by reading UCD files from disk and
-- parsing them with the proved UCD parser.
--
-- Usage:
-- Initialize ("ucd", Success);
-- if Success then
-- Idx := Get_Script (CP);
-- Name := Script_Name (Idx);
-- GBP := Get_GBP (CP);
-- end if;
-------------------------------------------------------------------------------
with Lingenic_Text.UCD_Parser;
with Lingenic_Text.Scx_Parser;
with Lingenic_Text.Graphemes_Spec;
with Lingenic_Text.Words_Spec;
with Lingenic_Text.Sentences_Spec;
with Lingenic_Text.EAW_Spec;
with Lingenic_Text.Line_Break_Spec;
with Lingenic_Text.Bidi_Spec;
with Lingenic_Text.Properties_Spec;
package Lingenic_Text.Properties
with SPARK_Mode,
Abstract_State => Property_State,
Initializes => Property_State
is
---------------------------------------------------------------------------
-- Initialization
---------------------------------------------------------------------------
function Initialized return Boolean
with Global => Property_State;
procedure Initialize
(UCD_Dir : String;
Success : out Boolean)
with Global => (Output => Property_State),
Post => (if Success then Initialized);
---------------------------------------------------------------------------
-- Script property (UAX #24)
---------------------------------------------------------------------------
function Get_Script (CP : Codepoint) return UCD_Parser.Property_Index
with Global => Property_State,
Pre => Initialized;
function Script_Name_Count return UCD_Parser.Property_Index
with Global => Property_State,
Pre => Initialized;
function Script_Name
(Idx : UCD_Parser.Property_Index) return String
with Global => Property_State,
Pre => Initialized
and then Idx >= 1
and then Idx <= Script_Name_Count;
---------------------------------------------------------------------------
-- Script_Extensions property (UAX #24)
--
-- Is_In_Script_Extensions implements the full UAX #24 semantics:
-- - If ScriptExtensions.txt covers CP, the result is membership in
-- the script-set from that file.
-- - If CP is not covered by any line, the result is
-- (Script_Idx = Get_Script (CP)) — the singleton primary script.
--
-- Get_Script_Extension_Count returns the number of scripts in the
-- extension set. For CPs not in ScriptExtensions.txt, this is 1
-- (the primary script).
---------------------------------------------------------------------------
function Is_In_Script_Extensions
(CP : Codepoint;
Script_Idx : UCD_Parser.Property_Index) return Boolean
with Global => Property_State,
Pre => Initialized
and then Script_Idx >= 1
and then Script_Idx <= Script_Name_Count;
function Get_Script_Extension_Count
(CP : Codepoint) return Scx_Parser.Scx_Member_Count
with Global => Property_State,
Pre => Initialized;
function Get_Script_Extension
(CP : Codepoint;
K : Positive) return UCD_Parser.Property_Index
with Global => Property_State,
Pre => Initialized
and then K >= 1
and then K <= Get_Script_Extension_Count (CP);
---------------------------------------------------------------------------
-- Grapheme_Cluster_Break property (UAX #29)
---------------------------------------------------------------------------
function Get_GBP (CP : Codepoint) return UCD_Parser.Property_Index
with Global => Property_State,
Pre => Initialized;
function GBP_Name_Count return UCD_Parser.Property_Index
with Global => Property_State,
Pre => Initialized;
function GBP_Name
(Idx : UCD_Parser.Property_Index) return String
with Global => Property_State,
Pre => Initialized
and then Idx >= 1
and then Idx <= GBP_Name_Count;
-- Map a runtime GBP index to the abstract GBP_Value used by the
-- ghost specification. Returns GBP_Other for unrecognized indices.
function GBP_To_Abstract
(Idx : UCD_Parser.Property_Index) return Graphemes_Spec.GBP_Value
with Global => Property_State,
Pre => Initialized;
---------------------------------------------------------------------------
-- Extended_Pictographic property (UTS #51 / emoji-data.txt)
---------------------------------------------------------------------------
function Get_ExtPict (CP : Codepoint) return Boolean
with Global => Property_State,
Pre => Initialized;
---------------------------------------------------------------------------
-- Indic_Conjunct_Break property (UAX #44)
---------------------------------------------------------------------------
function Get_InCB (CP : Codepoint) return UCD_Parser.Property_Index
with Global => Property_State,
Pre => Initialized;
function InCB_Name_Count return UCD_Parser.Property_Index
with Global => Property_State,
Pre => Initialized;
-- Map a runtime InCB index to the abstract InCB_Value used by the
-- ghost specification. Returns InCB_None for unrecognized indices.
function InCB_To_Abstract
(Idx : UCD_Parser.Property_Index) return Graphemes_Spec.InCB_Value
with Global => Property_State,
Pre => Initialized;
---------------------------------------------------------------------------
-- Word_Break property (UAX #29)
---------------------------------------------------------------------------
function Get_WBP (CP : Codepoint) return UCD_Parser.Property_Index
with Global => Property_State,
Pre => Initialized;
function WBP_Name_Count return UCD_Parser.Property_Index
with Global => Property_State,
Pre => Initialized;
function WBP_Name
(Idx : UCD_Parser.Property_Index) return String
with Global => Property_State,
Pre => Initialized
and then Idx >= 1
and then Idx <= WBP_Name_Count;
-- Map a runtime WBP index to the abstract WBP_Value used by the
-- ghost specification. Returns WBP_Other for unrecognized indices.
function WBP_To_Abstract
(Idx : UCD_Parser.Property_Index) return Words_Spec.WBP_Value
with Global => Property_State,
Pre => Initialized;
---------------------------------------------------------------------------
-- Sentence_Break property (UAX #29)
---------------------------------------------------------------------------
function Get_SBP (CP : Codepoint) return UCD_Parser.Property_Index
with Global => Property_State,
Pre => Initialized;
function SBP_Name_Count return UCD_Parser.Property_Index
with Global => Property_State,
Pre => Initialized;
function SBP_Name
(Idx : UCD_Parser.Property_Index) return String
with Global => Property_State,
Pre => Initialized
and then Idx >= 1
and then Idx <= SBP_Name_Count;
-- Map a runtime SBP index to the abstract SBP_Value used by the
-- ghost specification. Returns SBP_Other for unrecognized indices.
function SBP_To_Abstract
(Idx : UCD_Parser.Property_Index) return Sentences_Spec.SBP_Value
with Global => Property_State,
Pre => Initialized;
---------------------------------------------------------------------------
-- East_Asian_Width property (UAX #11)
---------------------------------------------------------------------------
function Get_EAW (CP : Codepoint) return UCD_Parser.Property_Index
with Global => Property_State,
Pre => Initialized;
function EAW_Name_Count return UCD_Parser.Property_Index
with Global => Property_State,
Pre => Initialized;
function EAW_Name
(Idx : UCD_Parser.Property_Index) return String
with Global => Property_State,
Pre => Initialized
and then Idx >= 1
and then Idx <= EAW_Name_Count;
-- Map a runtime EAW index to the abstract EAW_Value used by the
-- ghost specification. Returns EAW_Neutral for unrecognized indices.
function EAW_To_Abstract
(Idx : UCD_Parser.Property_Index) return EAW_Spec.EAW_Value
with Global => Property_State,
Pre => Initialized;
---------------------------------------------------------------------------
-- XID_Start / XID_Continue properties (UAX #31)
---------------------------------------------------------------------------
function Get_XID_Start (CP : Codepoint) return Boolean
with Global => Property_State,
Pre => Initialized;
function Get_XID_Continue (CP : Codepoint) return Boolean
with Global => Property_State,
Pre => Initialized;
---------------------------------------------------------------------------
-- Line_Break property — resolved (UAX #14)
--
-- Returns the resolved LBP class directly (after LB1 resolution,
-- QU/OP/CP splits). The raw LB index is not exposed.
---------------------------------------------------------------------------
function Get_LBP (CP : Codepoint) return Line_Break_Spec.LBP_Value
with Global => Property_State,
Pre => Initialized;
---------------------------------------------------------------------------
-- General_Category property (UAX #44)
---------------------------------------------------------------------------
function Get_GC (CP : Codepoint) return UCD_Parser.Property_Index
with Global => Property_State,
Pre => Initialized;
function GC_Name_Count return UCD_Parser.Property_Index
with Global => Property_State,
Pre => Initialized;
function GC_Name
(Idx : UCD_Parser.Property_Index) return String
with Global => Property_State,
Pre => Initialized
and then Idx >= 1
and then Idx <= GC_Name_Count;
---------------------------------------------------------------------------
-- Bidi_Class property — resolved (UAX #9)
--
-- Returns the resolved BC_Value directly (with block-specific @missing
-- defaults applied for RTL scripts, Arabic, and Currency Symbols).
---------------------------------------------------------------------------
function Get_BC (CP : Codepoint) return Bidi_Spec.BC_Value
with Global => Property_State,
Pre => Initialized;
---------------------------------------------------------------------------
-- Joining_Type property — resolved (UAX #44 / DerivedJoiningType.txt)
--
-- Returns the JT_Value directly. Default is JT_U (Non_Joining).
---------------------------------------------------------------------------
function Get_JT (CP : Codepoint) return Properties_Spec.JT_Value
with Global => Property_State,
Pre => Initialized;
---------------------------------------------------------------------------
-- Bidi_Mirrored property — UAX #9 rule L4 / UnicodeData.txt field 9
--
-- True when the character's depicted glyph should be mirrored in a
-- right-to-left rendering context, per the Bidi_Mirrored property.
--
-- The L4 rule is: "A character is depicted by a mirrored glyph if and
-- only if (a) the resolved directionality of that character is R, and
-- (b) the Bidi_Mirrored property value of that character is Yes."
--
-- This function exposes the (b) part — the Unicode property. The full
-- L4 decision (combining level parity with the property) is provided
-- as Bidi.Needs_Mirror. Producing the actual mirrored glyph from the
-- decision is the rendering layer's obligation, not text processing.
---------------------------------------------------------------------------
function Get_Bidi_Mirrored (CP : Codepoint) return Boolean
with Global => Property_State,
Pre => Initialized;
end Lingenic_Text.Properties;