-- 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
--
-- Proved Script_Extensions (UAX #24) file parser.
--
-- Reads ScriptExtensions.txt from an in-memory Byte_Array and populates
-- a pool-interned table: every codepoint points to a Script_Set in the
-- pool listing the script indices the file associates with it.
--
-- The file format is the standard UCD property format with one twist:
-- the value field is a space-separated LIST of four-letter ISO 15924
-- script codes, not a single value. Each script code corresponds to
-- an entry in the already-parsed Scripts.txt value-name table
-- (Script_Names), which lives in a DIFFERENT source buffer. The parser
-- therefore takes BOTH buffers explicitly.
--
-- The parser's postcondition references the recursive ghost spec in
-- Lingenic_Text.Scx_Spec. For every codepoint and every script index,
-- the parsed pool membership exactly matches
-- Scx_Spec.Expected_Scx_Has_From, which is a direct encoding of what
-- ScriptExtensions.txt's raw bytes say about that (CP, Script) pair.
--
-- Semantics of ScriptExtensions.txt (per UAX #24):
-- - Each codepoint appears at most once across all data lines.
-- - If a line covers CP, the associated script set is the tokens on
-- that line.
-- - If no line covers CP, the set is the singleton {Get_Script (CP)}
-- — the primary script. This "default fallback" is applied OUTSIDE
-- the parser, in the Is_In_Script_Extensions accessor. The parser
-- itself only characterizes what the FILE explicitly says, mirroring
-- the structure of Scx_Spec.Expected_Scx_Has_From.
--
-- Storage — pool interned:
-- The set of distinct script-sets encountered in ScriptExtensions.txt
-- is small (~300 in Unicode 17.0). Rather than storing a full set
-- per codepoint, we maintain a small pool of Script_Set values and a
-- flat per-codepoint table mapping each codepoint to its pool entry.
-- Pool entry 0 is reserved for "codepoint not covered by the file".
-------------------------------------------------------------------------------
with Lingenic_Text.UCD_Parser;
with Lingenic_Text.Scx_Spec;
package Lingenic_Text.Scx_Parser
with SPARK_Mode, Pure
is
---------------------------------------------------------------------------
-- Script set: a small bounded list of script indices.
--
-- Indices are UCD_Parser.Property_Index values (1 .. 255) referring to
-- entries in the Scripts.txt Script_Names table. The list is packed:
-- positions 1 .. Count hold the valid entries, the rest are 0.
---------------------------------------------------------------------------
Max_Scx_Size : constant := UCD_Parser.Max_Value_Names;
-- Sized to the maximum possible Script_Count so that Build_Line_Set
-- can iterate over all scripts without overflow. Actual per-codepoint
-- script counts never exceed ~24 in Unicode 17.0.
subtype Scx_Member_Count is Natural range 0 .. Max_Scx_Size;
type Scx_Member_Array is
array (Positive range 1 .. Max_Scx_Size) of UCD_Parser.Property_Index;
type Script_Set is record
Count : Scx_Member_Count := 0;
Items : Scx_Member_Array := [others => 0];
end record;
---------------------------------------------------------------------------
-- Pool and table types
---------------------------------------------------------------------------
Max_Unique_Scx : constant := 512;
-- Unicode 17.0 has ~300 distinct script-extension sets — 512 is ample.
subtype Scx_Pool_Id is Natural range 0 .. Max_Unique_Scx;
-- 0 = "codepoint not covered by the file".
type Scx_Pool_Array is
array (Scx_Pool_Id range 1 .. Max_Unique_Scx) of Script_Set;
type Scx_Table_Array is array (Codepoint) of Scx_Pool_Id;
---------------------------------------------------------------------------
-- Ghost membership predicate
--
-- Set_Has (S, Idx) asks: is Script index Idx a member of S?
-- Expressed as a recursive expression function on a bounded range so
-- the solver can unfold it directly.
---------------------------------------------------------------------------
function Set_Has_From
(S : Script_Set;
Idx : UCD_Parser.Property_Index;
From : Positive) return Boolean
is (From <= S.Count
and then (S.Items (From) = Idx
or else (From < S.Count
and then Set_Has_From (S, Idx, From + 1))))
with Ghost,
Pre => From in 1 .. Max_Scx_Size,
Subprogram_Variant => (Decreases => Max_Scx_Size - From);
function Set_Has
(S : Script_Set;
Idx : UCD_Parser.Property_Index) return Boolean
is (Set_Has_From (S, Idx, 1))
with Ghost;
---------------------------------------------------------------------------
-- Pool_Has: does the set at pool position P contain script index Idx?
--
-- Wraps Set_Has for the common "look up by pool id" access pattern.
-- Returns False for the sentinel pool id 0.
---------------------------------------------------------------------------
-- Deliberately NOT an expression function: the solver treats this
-- as opaque and uses the postcondition when it needs to look inside.
-- This prevents cascading Set_Has → Set_Has_From expansion in
-- nested loop invariant VCs where congruence suffices.
function Pool_Has
(Pool : Scx_Pool_Array;
Pool_End : Natural;
P : Scx_Pool_Id;
Script_Idx : UCD_Parser.Property_Index) return Boolean
with Ghost,
Pre => Pool_End <= Max_Unique_Scx,
Post => Pool_Has'Result =
(P >= 1
and then P <= Pool_End
and then P <= Max_Unique_Scx
and then Set_Has (Pool (P), Script_Idx));
---------------------------------------------------------------------------
-- Parse ScriptExtensions.txt.
--
-- Scx_Src : raw bytes of ScriptExtensions.txt (First = 1).
-- Script_Src : raw bytes of Scripts.txt (First = 1), referenced by
-- Script_Names entries.
-- Script_Names : name table previously produced by
-- UCD_Parser.Extract_Value_Names on Script_Src.
-- Script_Count : number of valid entries in Script_Names.
-- Pool : out — small table of distinct script-sets seen.
-- Pool_End : out — number of valid pool entries (1 .. Pool_End).
-- Table : out — flat per-codepoint pool id.
-- Success : out — True when every token on every data line
-- matched a known Script_Names entry.
--
-- Postcondition (Platinum):
-- For every codepoint CP and every script index S in
-- 1 .. Script_Count:
--
-- Pool_Has (Pool, Pool_End, Table (CP), S)
-- = Scx_Spec.Expected_Scx_Has_From
-- (Scx_Src, 1, CP, Script_Src, Script_Names, S)
--
-- i.e. the parsed membership exactly matches what the raw file
-- bytes specify, as characterized recursively by Scx_Spec.
---------------------------------------------------------------------------
procedure Parse_Script_Extensions
(Scx_Src : Byte_Array;
Script_Src : Byte_Array;
Script_Names : UCD_Parser.Value_Name_Array;
Script_Count : UCD_Parser.Property_Index;
Pool : out Scx_Pool_Array;
Pool_End : out Natural;
Table : out Scx_Table_Array;
Success : out Boolean)
with Pre => Scx_Src'First = 1
and then Scx_Src'Last < Positive'Last
and then Scx_Src'Length > 0
and then Script_Src'First = 1
and then Script_Src'Last < Positive'Last
and then Script_Count in 1 .. UCD_Parser.Max_Value_Names,
Post => -- Pool bounds
Pool_End in 0 .. Max_Unique_Scx
-- Table entries are valid pool ids
and then (for all CP in Codepoint =>
Table (CP) in 0 .. Pool_End)
-- Every pool set is well-formed
and then (for all P in 1 .. Pool_End =>
(P in 1 .. Max_Unique_Scx
and then Pool (P).Count in 0 .. Max_Scx_Size))
-- Correctness: parsed membership matches the ghost spec
and then
(if Success then
(for all CP in Codepoint =>
(for all S in UCD_Parser.Property_Index
range 1 .. Script_Count =>
Pool_Has (Pool, Pool_End, Table (CP), S)
= Scx_Spec.Expected_Scx_Has_From
(Scx_Src, 1, CP,
Script_Src, Script_Names, S))));
end Lingenic_Text.Scx_Parser;