-- 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
--
-- C language binding (specification).
--
-- This package exports the full public API surface as C functions with
-- the "lt_" prefix. The companion header is include/lingenic_text.h.
--
-- The binding is a thin validation shim over the proved SPARK core:
-- - every precondition of the underlying SPARK subprogram is checked
-- here at runtime; violations return LT_ERR (-1) instead of calling
-- the core with invalid arguments;
-- - byte buffers are copied between C uint8_t* memory and the
-- library's Byte_Array representation (32-bit components);
-- - positions and indices are 0-based on the C side, 1-based inside.
--
-- This unit is intentionally SPARK_Mode => Off: it manipulates raw C
-- addresses and heap allocations, which are outside SPARK. All proved
-- guarantees apply to the core library it calls into.
--
-- Usage from C:
-- lingenic_text_cinit(); /* Ada elaboration (generated) */
-- lt_init("path/to/ucd"); /* load UCD data tables */
-- ... call lt_* functions ...
-------------------------------------------------------------------------------
with Interfaces.C;
with Interfaces.C.Strings;
with System;
package Lingenic_Text_C
with SPARK_Mode => Off
is
subtype int is Interfaces.C.int;
subtype size_t is Interfaces.C.size_t;
subtype u8 is Interfaces.Unsigned_8;
subtype u32 is Interfaces.Unsigned_32;
type Size_Ptr is access all size_t with Convention => C;
type U32_Ptr is access all u32 with Convention => C;
type U8_Ptr is access all u8 with Convention => C;
type Int_Ptr is access all int with Convention => C;
---------------------------------------------------------------------------
-- Initialization
---------------------------------------------------------------------------
-- Initialize all modules from the UCD directory.
-- Returns 0 on success, or the number of the stage that failed:
-- 1 = properties, 2 = normalization, 3 = emoji, 4 = idna,
-- 5 = bidi, 6 = case mapping, 7 = collation.
-- Returns -1 on invalid argument.
function LT_Init
(UCD_Dir : Interfaces.C.Strings.chars_ptr) return int
with Export, Convention => C, External_Name => "lt_init";
-- 1 if all modules are initialized, 0 otherwise.
function LT_Initialized return int
with Export, Convention => C, External_Name => "lt_initialized";
---------------------------------------------------------------------------
-- UTF-8 (RFC 3629)
---------------------------------------------------------------------------
-- Decode one UTF-8 sequence at 0-based offset Pos.
-- Returns 1 if valid (CP and Seq_Len set), 0 if invalid at Pos
-- (Seq_Len set to 1), -1 on bad arguments.
function LT_UTF8_Decode
(Buf : System.Address;
Len : size_t;
Pos : size_t;
CP : U32_Ptr;
Seq_Len : Size_Ptr) return int
with Export, Convention => C, External_Name => "lt_utf8_decode";
-- Encode codepoint CP into Buf (capacity Cap). Writes 1..4 bytes.
-- Returns 0 on success (Len set), -1 if CP is not a Unicode scalar
-- value or the buffer is too small.
function LT_UTF8_Encode
(CP : u32;
Buf : System.Address;
Cap : size_t;
Len : Size_Ptr) return int
with Export, Convention => C, External_Name => "lt_utf8_encode";
---------------------------------------------------------------------------
-- Segmentation (UAX #29, UAX #14)
--
-- Positions are 0-based byte offsets. On success *Next_Pos is the
-- offset of the next boundary (Pos < *Next_Pos <= Len).
-- Returns 0 on success, -1 on bad arguments / not initialized.
---------------------------------------------------------------------------
function LT_Next_Grapheme_Break
(Text : System.Address;
Len : size_t;
Pos : size_t;
Next_Pos : Size_Ptr) return int
with Export, Convention => C, External_Name => "lt_next_grapheme_break";
function LT_Next_Word_Break
(Text : System.Address;
Len : size_t;
Pos : size_t;
Next_Pos : Size_Ptr) return int
with Export, Convention => C, External_Name => "lt_next_word_break";
function LT_Next_Sentence_Break
(Text : System.Address;
Len : size_t;
Pos : size_t;
Next_Pos : Size_Ptr) return int
with Export, Convention => C, External_Name => "lt_next_sentence_break";
function LT_Next_Line_Break
(Text : System.Address;
Len : size_t;
Pos : size_t;
Next_Pos : Size_Ptr) return int
with Export, Convention => C, External_Name => "lt_next_line_break";
---------------------------------------------------------------------------
-- Normalization (UAX #15)
--
-- Form: 0 = NFD, 1 = NFC, 2 = NFKD, 3 = NFKC.
---------------------------------------------------------------------------
-- Returns 0 = success, 1 = output buffer too small, 2 = invalid
-- UTF-8 input, -1 = bad arguments / not initialized.
function LT_Normalize
(Form : int;
In_Buf : System.Address;
In_Len : size_t;
Out_Buf : System.Address;
Out_Cap : size_t;
Out_Len : Size_Ptr) return int
with Export, Convention => C, External_Name => "lt_normalize";
-- Returns 0 = yes, 1 = no, 2 = maybe, -1 = error.
function LT_Quick_Check
(Form : int;
In_Buf : System.Address;
In_Len : size_t) return int
with Export, Convention => C, External_Name => "lt_quick_check";
-- Returns 1 = normalized, 0 = not normalized, -1 = error.
function LT_Is_Normalized
(Form : int;
In_Buf : System.Address;
In_Len : size_t) return int
with Export, Convention => C, External_Name => "lt_is_normalized";
-- Canonical Combining Class (0..254), -1 on error.
function LT_CCC (CP : u32) return int
with Export, Convention => C, External_Name => "lt_ccc";
---------------------------------------------------------------------------
-- Case mapping (Unicode Section 3.13)
--
-- Full case mappings; output may be up to 3x the input length.
-- Returns 0 = success, 1 = output buffer too small, 2 = invalid
-- UTF-8 input, -1 = bad arguments / not initialized.
---------------------------------------------------------------------------
function LT_Uppercase
(In_Buf : System.Address;
In_Len : size_t;
Out_Buf : System.Address;
Out_Cap : size_t;
Out_Len : Size_Ptr) return int
with Export, Convention => C, External_Name => "lt_uppercase";
function LT_Lowercase
(In_Buf : System.Address;
In_Len : size_t;
Out_Buf : System.Address;
Out_Cap : size_t;
Out_Len : Size_Ptr) return int
with Export, Convention => C, External_Name => "lt_lowercase";
function LT_Titlecase
(In_Buf : System.Address;
In_Len : size_t;
Out_Buf : System.Address;
Out_Cap : size_t;
Out_Len : Size_Ptr) return int
with Export, Convention => C, External_Name => "lt_titlecase";
function LT_Casefold
(In_Buf : System.Address;
In_Len : size_t;
Out_Buf : System.Address;
Out_Cap : size_t;
Out_Len : Size_Ptr) return int
with Export, Convention => C, External_Name => "lt_casefold";
-- D135 Cased / D136 Case_Ignorable. 1/0, -1 on error.
function LT_Is_Cased (CP : u32) return int
with Export, Convention => C, External_Name => "lt_is_cased";
function LT_Is_Case_Ignorable (CP : u32) return int
with Export, Convention => C, External_Name => "lt_is_case_ignorable";
---------------------------------------------------------------------------
-- Collation (UTS #10, DUCET)
--
-- Option: 0 = non-ignorable, 1 = shifted.
---------------------------------------------------------------------------
-- Compare two UTF-8 strings. *Result is -1 (less), 0 (equal),
-- 1 (greater). Returns 0 on success, 1 if either input is invalid
-- UTF-8 / too long, -1 on bad arguments / not initialized.
function LT_Collate
(A : System.Address;
A_Len : size_t;
B : System.Address;
B_Len : size_t;
Option : int;
Result : Int_Ptr) return int
with Export, Convention => C, External_Name => "lt_collate";
-- Build a binary sort key (memcmp-comparable).
-- Returns 0 on success, 1 on failure (invalid input or key buffer
-- too small), -1 on bad arguments / not initialized.
function LT_Sort_Key
(In_Buf : System.Address;
In_Len : size_t;
Option : int;
Key : System.Address;
Key_Cap : size_t;
Key_Len : Size_Ptr) return int
with Export, Convention => C, External_Name => "lt_sort_key";
---------------------------------------------------------------------------
-- Bidirectional algorithm (UAX #9)
--
-- Direction: 0 = auto (rule P2/P3), 1 = LTR, 2 = RTL.
-- Paragraphs are limited to 4096 codepoints.
---------------------------------------------------------------------------
-- Resolve embedding levels for a UTF-8 paragraph.
-- Levels receives one level (0..126) per codepoint; Levels_Cap must
-- be >= the number of codepoints (Len is always sufficient).
-- Returns 0 on success, 1 if the algorithm rejects the input
-- (e.g. too many codepoints), -1 on bad arguments.
function LT_Bidi_Resolve
(Text : System.Address;
Len : size_t;
Direction : int;
Levels : System.Address;
Levels_Cap : size_t;
Num_CPs : Size_Ptr;
Para_Level : U8_Ptr) return int
with Export, Convention => C, External_Name => "lt_bidi_resolve";
-- Compute the visual order (rule L2). Order receives Num_CPs
-- 0-based logical indices: Order[i] is the logical index of the
-- codepoint at visual position i.
-- Returns 0 on success, 1 on failure, -1 on bad arguments.
function LT_Bidi_Reorder
(Levels : System.Address;
Num_CPs : size_t;
Para_Level : u8;
Order : System.Address;
Order_Cap : size_t) return int
with Export, Convention => C, External_Name => "lt_bidi_reorder";
-- Rule L4: 1 if the codepoint should be depicted mirrored at the
-- given embedding level, 0 if not, -1 on error.
function LT_Bidi_Needs_Mirror (CP : u32; Level : u8) return int
with Export, Convention => C, External_Name => "lt_bidi_needs_mirror";
---------------------------------------------------------------------------
-- East Asian Width (UAX #11)
---------------------------------------------------------------------------
-- Display width in fixed-pitch cells: 1 or 2. -1 on error.
function LT_Display_Width (CP : u32) return int
with Export, Convention => C, External_Name => "lt_display_width";
---------------------------------------------------------------------------
-- Emoji (UTS #51)
---------------------------------------------------------------------------
function LT_Is_Emoji (CP : u32) return int
with Export, Convention => C, External_Name => "lt_is_emoji";
function LT_Is_Emoji_Presentation (CP : u32) return int
with Export, Convention => C, External_Name => "lt_is_emoji_presentation";
function LT_Is_Emoji_Modifier (CP : u32) return int
with Export, Convention => C, External_Name => "lt_is_emoji_modifier";
function LT_Is_Emoji_Modifier_Base (CP : u32) return int
with Export, Convention => C,
External_Name => "lt_is_emoji_modifier_base";
function LT_Is_Emoji_Component (CP : u32) return int
with Export, Convention => C, External_Name => "lt_is_emoji_component";
-- Classify a UTF-8 sequence (max 256 bytes):
-- 0 = not emoji, 1 = emoji character, 2 = presentation sequence,
-- 3 = keycap sequence, 4 = modifier sequence, 5 = flag sequence,
-- 6 = tag sequence, 7 = ZWJ sequence. -1 on error.
function LT_Emoji_Classify
(In_Buf : System.Address;
In_Len : size_t) return int
with Export, Convention => C, External_Name => "lt_emoji_classify";
---------------------------------------------------------------------------
-- Identifiers (UAX #31)
---------------------------------------------------------------------------
function LT_Is_Identifier_Start (CP : u32) return int
with Export, Convention => C, External_Name => "lt_is_identifier_start";
function LT_Is_Identifier_Part (CP : u32) return int
with Export, Convention => C, External_Name => "lt_is_identifier_part";
---------------------------------------------------------------------------
-- IDNA (UTS #46)
--
-- Options is a bitmask: bit 0 = CheckHyphens, bit 1 = CheckBidi,
-- bit 2 = CheckJoiners, bit 3 = UseSTD3ASCIIRules,
-- bit 4 = VerifyDnsLength. Default options = 0x1F (all on).
--
-- Returns the IDNA result code (0 = success, see header for the
-- full list), or -1 on bad arguments / not initialized.
---------------------------------------------------------------------------
function LT_IDNA_To_ASCII
(In_Buf : System.Address;
In_Len : size_t;
Options : u32;
Out_Buf : System.Address;
Out_Cap : size_t;
Out_Len : Size_Ptr) return int
with Export, Convention => C, External_Name => "lt_idna_to_ascii";
function LT_IDNA_To_Unicode
(In_Buf : System.Address;
In_Len : size_t;
Options : u32;
Out_Buf : System.Address;
Out_Cap : size_t;
Out_Len : Size_Ptr) return int
with Export, Convention => C, External_Name => "lt_idna_to_unicode";
---------------------------------------------------------------------------
-- Character properties
--
-- Script and General_Category values are runtime indices into name
-- tables (use the *_name functions). All other properties return
-- the stable values listed in the C header.
---------------------------------------------------------------------------
-- Script property (UAX #24). Index into the script name table.
function LT_Script (CP : u32) return int
with Export, Convention => C, External_Name => "lt_script";
function LT_Script_Count return int
with Export, Convention => C, External_Name => "lt_script_count";
-- Copies the NUL-terminated script name into Buf (capacity Cap).
-- Returns the name length, or -1 if Idx is out of range or the
-- buffer is too small.
function LT_Script_Name
(Idx : int;
Buf : System.Address;
Cap : size_t) return int
with Export, Convention => C, External_Name => "lt_script_name";
-- Script_Extensions (UAX #24).
function LT_Script_Extension_Count (CP : u32) return int
with Export, Convention => C,
External_Name => "lt_script_extension_count";
-- K is 0-based; returns the K-th script index of CP's extension set.
function LT_Script_Extension (CP : u32; K : int) return int
with Export, Convention => C, External_Name => "lt_script_extension";
-- 1 if Script_Idx is in CP's Script_Extensions set, 0 if not.
function LT_In_Script_Extensions (CP : u32; Script_Idx : int) return int
with Export, Convention => C, External_Name => "lt_in_script_extensions";
-- General_Category (UAX #44). Index into the GC name table.
function LT_General_Category (CP : u32) return int
with Export, Convention => C, External_Name => "lt_general_category";
function LT_General_Category_Count return int
with Export, Convention => C, External_Name => "lt_general_category_count";
function LT_General_Category_Name
(Idx : int;
Buf : System.Address;
Cap : size_t) return int
with Export, Convention => C, External_Name => "lt_general_category_name";
-- Grapheme_Cluster_Break (LT_GBP_* values in the header).
function LT_Grapheme_Break_Property (CP : u32) return int
with Export, Convention => C,
External_Name => "lt_grapheme_break_property";
-- Word_Break (LT_WBP_* values).
function LT_Word_Break_Property (CP : u32) return int
with Export, Convention => C, External_Name => "lt_word_break_property";
-- Sentence_Break (LT_SBP_* values).
function LT_Sentence_Break_Property (CP : u32) return int
with Export, Convention => C,
External_Name => "lt_sentence_break_property";
-- Line_Break, resolved per LB1 (LT_LBP_* values).
function LT_Line_Break_Property (CP : u32) return int
with Export, Convention => C, External_Name => "lt_line_break_property";
-- East_Asian_Width category (LT_EAW_* values).
function LT_East_Asian_Width (CP : u32) return int
with Export, Convention => C, External_Name => "lt_east_asian_width";
-- Bidi_Class, resolved with @missing defaults (LT_BC_* values).
function LT_Bidi_Class (CP : u32) return int
with Export, Convention => C, External_Name => "lt_bidi_class";
-- Joining_Type (LT_JT_* values).
function LT_Joining_Type (CP : u32) return int
with Export, Convention => C, External_Name => "lt_joining_type";
-- Indic_Conjunct_Break (LT_INCB_* values).
function LT_Indic_Conjunct_Break (CP : u32) return int
with Export, Convention => C,
External_Name => "lt_indic_conjunct_break";
-- Extended_Pictographic. 1/0, -1 on error.
function LT_Extended_Pictographic (CP : u32) return int
with Export, Convention => C,
External_Name => "lt_extended_pictographic";
-- Bidi_Mirrored property (UnicodeData field 9). 1/0, -1 on error.
function LT_Bidi_Mirrored (CP : u32) return int
with Export, Convention => C, External_Name => "lt_bidi_mirrored";
end Lingenic_Text_C;