-- 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 BidiBrackets.txt parser.
--
-- Reads BidiBrackets.txt from an in-memory Byte_Array and populates
-- four lookup tables used by the N0 bracket pair algorithm:
--
-- Bracket_Open_Table — opening bracket → closing bracket mapping
-- Bracket_Close_Table — closing bracket → opening bracket mapping
-- Is_Open_Bracket — per-codepoint flag: is opening bracket
-- Is_Close_Bracket — per-codepoint flag: is closing bracket
--
-- The parser's postcondition references the recursive ghost spec in
-- Lingenic_Text.Bidi_Brackets_Spec. For every codepoint, each output
-- table entry matches the corresponding Expected_* function, which is
-- a direct encoding of what BidiBrackets.txt's raw bytes specify.
--
-- This replaces the hand-rolled SPARK_Mode(Off) parser that was
-- previously inside Bidi.Initialize, bringing the BidiBrackets parsing
-- under SPARK verification.
-------------------------------------------------------------------------------
with Lingenic_Text.Bidi_Brackets_Spec;
package Lingenic_Text.Bidi_Brackets_Parser
with SPARK_Mode, Pure
is
use Bidi_Brackets_Spec;
---------------------------------------------------------------------------
-- Output table types
--
-- Bracket_Table maps each codepoint to its paired codepoint (0 if
-- the codepoint is not a bracket).
--
-- Bracket_Flag_Table maps each codepoint to a boolean indicating
-- whether it is an opening or closing bracket.
---------------------------------------------------------------------------
type Bracket_Table is array (Codepoint) of Codepoint;
type Bracket_Flag_Table is array (Codepoint) of Boolean;
---------------------------------------------------------------------------
-- Minimum expected data lines.
--
-- Unicode 17.0 BidiBrackets.txt has 128 data lines (64 bracket pairs).
-- Require at least 120 to detect truncated files. This threshold is
-- checked only for the Success output — correctness of table contents
-- is established by the ghost spec regardless of line count.
---------------------------------------------------------------------------
Min_Expected_Lines : constant := 120;
---------------------------------------------------------------------------
-- Parse BidiBrackets.txt.
--
-- Source: Raw bytes of BidiBrackets.txt (Source'First = 1).
-- Open_Table: Output — opening bracket → paired closing codepoint.
-- Close_Table: Output — closing bracket → paired opening codepoint.
-- Open_Flags: Output — True for opening brackets.
-- Close_Flags: Output — True for closing brackets.
-- Lines_Parsed: Output — count of valid bracket data lines processed.
-- Success: Output — True when parsing completed and at least
-- Min_Expected_Lines valid bracket data lines were found.
--
-- Postcondition (Platinum):
-- For every codepoint CP:
-- Open_Table(CP) = Expected_Open_From(Source, 1, CP)
-- Close_Table(CP) = Expected_Close_From(Source, 1, CP)
-- Open_Flags(CP) = Expected_Is_Open_From(Source, 1, CP)
-- Close_Flags(CP) = Expected_Is_Close_From(Source, 1, CP)
--
-- i.e. the parsed tables exactly match what the raw file bytes
-- specify, as characterized recursively by Bidi_Brackets_Spec.
---------------------------------------------------------------------------
procedure Parse_Brackets_File
(Source : Byte_Array;
Open_Table : out Bracket_Table;
Close_Table : out Bracket_Table;
Open_Flags : out Bracket_Flag_Table;
Close_Flags : out Bracket_Flag_Table;
Lines_Parsed : out Natural;
Success : out Boolean)
with Pre => Source'First = 1
and then Source'Last < Positive'Last
and then Source'Length > 0,
Post =>
-- Range safety: all table values are valid codepoints
(for all CP in Codepoint =>
Open_Table (CP) <= Max_Codepoint
and then Close_Table (CP) <= Max_Codepoint)
-- Correctness: each entry matches the ghost spec
and then
(for all CP in Codepoint =>
Open_Table (CP) =
Expected_Open_From (Source, 1, CP)
and then Close_Table (CP) =
Expected_Close_From (Source, 1, CP)
and then Open_Flags (CP) =
Expected_Is_Open_From (Source, 1, CP)
and then Close_Flags (CP) =
Expected_Is_Close_From (Source, 1, CP))
-- Truncation detection
and then
(if Success then Lines_Parsed >= Min_Expected_Lines);
end Lingenic_Text.Bidi_Brackets_Parser;