-- 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 — Bidi_Brackets_Parser body
--
-- Proved parser for BidiBrackets.txt.
--
-- Architecture follows UCD_Parser.Parse_Property_File:
-- - Line-by-line scan of the source buffer
-- - Per-line field extraction using UCD_Parser runtime helpers
-- - Two-part correctness invariant linking table state to ghost spec
-- - Lemma procedures bridging per-line updates to the recursive spec
--
-- Key simplification vs UCD_Parser: BidiBrackets.txt has no range lines
-- (each data line covers exactly one codepoint), so no inner CP loop is
-- needed and frame conditions are trivial.
--
-- Semantic note: The ghost spec (Expected_Open_Mapping) uses
-- "last non-zero writer wins" semantics — when a covering line has
-- Line_Paired_CP = 0, the spec does NOT override a non-zero value from
-- an earlier line. The parser matches this by only writing to the mapping
-- tables when Line_Paired_CP > 0. In practice, BidiBrackets.txt never
-- has a bracket pair mapping to U+0000, so this is purely for proof
-- completeness.
-------------------------------------------------------------------------------
with Lingenic_Text.UCD_Format_Spec;
with Lingenic_Text.UCD_Parser;
package body Lingenic_Text.Bidi_Brackets_Parser
with SPARK_Mode
is
use UCD_Format_Spec;
use UCD_Parser;
pragma Warnings (Off, "is not referenced");
---------------------------------------------------------------------------
-- Ghost lemma: advance the Open_Table invariant over one line.
--
-- Unfolds Expected_Open_Mapping one level at Pos via the expression
-- function body, then reconnects through the opaque Expected_Open_From
-- wrapper at Next_Line_Start(Pos).
--
-- The table update rule includes Line_Paired_CP > 0 to match the spec's
-- "last non-zero writer wins" semantics.
---------------------------------------------------------------------------
procedure Lemma_Invariant_Step_Open
(Source : Byte_Array;
Pos : Positive;
CP : Codepoint;
New_Val : Codepoint;
Old_Val : Codepoint)
with Ghost,
Always_Terminates,
Pre =>
Source'First = 1
and then Source'Last < Positive'Last
and then Pos in Source'Range
-- Old invariant at Pos:
and then
Expected_Open_From (Source, 1, CP) =
(if Expected_Open_From (Source, Pos, CP) /= 0
then Expected_Open_From (Source, Pos, CP)
else Old_Val)
-- Table update rule (only for non-zero LPC):
and then
(if Is_Open_Line (Source, Pos)
and then Line_First_CP (Source, Pos) = CP
and then Line_Paired_CP (Source, Pos) <= Max_Codepoint
and then Line_Paired_CP (Source, Pos) > 0
then New_Val = Line_Paired_CP (Source, Pos)
else New_Val = Old_Val),
Post =>
(declare
NL : constant Positive := Next_Line_Start (Source, Pos);
begin
Expected_Open_From (Source, 1, CP) =
(if Expected_Open_From (Source, NL, CP) /= 0
then Expected_Open_From (Source, NL, CP)
else New_Val))
is
NL : constant Positive := Next_Line_Start (Source, Pos) with Ghost;
Rest : constant Natural :=
Expected_Open_From (Source, NL, CP) with Ghost;
begin
-- Bridge from opaque wrapper to expression function at Pos
pragma Assert
(Expected_Open_From (Source, Pos, CP) =
Expected_Open_Mapping (Source, Pos, CP));
-- Bridge from opaque wrapper to expression function at NL
pragma Assert
(Rest =
(if NL > Source'Last then 0
else Expected_Open_Mapping (Source, NL, CP)));
if Is_Open_Line (Source, Pos)
and then Line_First_CP (Source, Pos) = CP
and then Line_Paired_CP (Source, Pos) <= Max_Codepoint
then
-- Data line covers CP with open bracket.
-- EOM(S, Pos, CP) = if Rest /= 0 then Rest
-- else Line_Paired_CP(S, Pos)
declare
LPC : constant Natural := Line_Paired_CP (Source, Pos);
begin
pragma Assert
(Expected_Open_Mapping (Source, Pos, CP) =
(if Rest /= 0 then Rest else LPC));
if LPC > 0 then
-- LPC > 0: New_Val = LPC (from Pre).
-- EOM /= 0 (since if Rest /= 0 then Rest > 0, else LPC > 0).
-- Old invariant Part A: EOF(1,CP) = EOM.
-- Target: if Rest /= 0 then Rest else New_Val
-- Case Rest /= 0: EOM = Rest, EOF(1) = Rest. Target = Rest. ✓
-- Case Rest = 0: EOM = LPC = NV. EOF(1) = NV. Target = NV. ✓
null;
else
-- LPC = 0: New_Val = Old_Val (from Pre, "else" branch).
-- EOM = if Rest /= 0 then Rest else 0
-- Case Rest /= 0: EOM = Rest /= 0.
-- EOF(1) = EOM = Rest. Target: Rest. ✓
-- Case Rest = 0: EOM = 0. EOF(Pos) = 0.
-- Old invariant Part B: EOF(1) = Old_Val = NV.
-- Target: if 0 /= 0 then ... else NV → NV. ✓
null;
end if;
end;
else
-- Non-covering line: EOM(S, Pos, CP) = EOF(S, NL, CP) = Rest.
-- New_Val = Old_Val (from Pre, "else" branch).
-- Case Rest /= 0: EOF(Pos) /= 0. EOF(1) = EOF(Pos) = Rest.
-- Target: Rest. ✓
-- Case Rest = 0: EOF(Pos) = 0. EOF(1) = Old_Val = NV.
-- Target: NV. ✓
null;
end if;
end Lemma_Invariant_Step_Open;
---------------------------------------------------------------------------
-- Ghost lemma: advance the Close_Table invariant over one line.
---------------------------------------------------------------------------
procedure Lemma_Invariant_Step_Close
(Source : Byte_Array;
Pos : Positive;
CP : Codepoint;
New_Val : Codepoint;
Old_Val : Codepoint)
with Ghost,
Always_Terminates,
Pre =>
Source'First = 1
and then Source'Last < Positive'Last
and then Pos in Source'Range
and then
Expected_Close_From (Source, 1, CP) =
(if Expected_Close_From (Source, Pos, CP) /= 0
then Expected_Close_From (Source, Pos, CP)
else Old_Val)
and then
(if Is_Close_Line (Source, Pos)
and then Line_First_CP (Source, Pos) = CP
and then Line_Paired_CP (Source, Pos) <= Max_Codepoint
and then Line_Paired_CP (Source, Pos) > 0
then New_Val = Line_Paired_CP (Source, Pos)
else New_Val = Old_Val),
Post =>
(declare
NL : constant Positive := Next_Line_Start (Source, Pos);
begin
Expected_Close_From (Source, 1, CP) =
(if Expected_Close_From (Source, NL, CP) /= 0
then Expected_Close_From (Source, NL, CP)
else New_Val))
is
NL : constant Positive := Next_Line_Start (Source, Pos) with Ghost;
Rest : constant Natural :=
Expected_Close_From (Source, NL, CP) with Ghost;
begin
pragma Assert
(Expected_Close_From (Source, Pos, CP) =
Expected_Close_Mapping (Source, Pos, CP));
pragma Assert
(Rest =
(if NL > Source'Last then 0
else Expected_Close_Mapping (Source, NL, CP)));
if Is_Close_Line (Source, Pos)
and then Line_First_CP (Source, Pos) = CP
and then Line_Paired_CP (Source, Pos) <= Max_Codepoint
then
declare
LPC : constant Natural := Line_Paired_CP (Source, Pos);
begin
pragma Assert
(Expected_Close_Mapping (Source, Pos, CP) =
(if Rest /= 0 then Rest else LPC));
if LPC > 0 then
null;
else
null;
end if;
end;
else
null;
end if;
end Lemma_Invariant_Step_Close;
---------------------------------------------------------------------------
-- Ghost lemma: advance the Open_Flags invariant over one line.
---------------------------------------------------------------------------
procedure Lemma_Invariant_Step_Is_Open
(Source : Byte_Array;
Pos : Positive;
CP : Codepoint;
New_Flag : Boolean;
Old_Flag : Boolean)
with Ghost,
Always_Terminates,
Pre =>
Source'First = 1
and then Source'Last < Positive'Last
and then Pos in Source'Range
and then
Expected_Is_Open_From (Source, 1, CP) =
(Expected_Is_Open_From (Source, Pos, CP) or else Old_Flag)
and then
(if Is_Open_Line (Source, Pos)
and then Line_First_CP (Source, Pos) = CP
then New_Flag
else New_Flag = Old_Flag),
Post =>
(declare
NL : constant Positive := Next_Line_Start (Source, Pos);
begin
Expected_Is_Open_From (Source, 1, CP) =
(Expected_Is_Open_From (Source, NL, CP) or else New_Flag))
is
NL : constant Positive := Next_Line_Start (Source, Pos) with Ghost;
begin
pragma Assert
(Expected_Is_Open_From (Source, Pos, CP) =
Expected_Is_Open (Source, Pos, CP));
pragma Assert
(Expected_Is_Open_From (Source, NL, CP) =
(if NL > Source'Last then False
else Expected_Is_Open (Source, NL, CP)));
if Is_Open_Line (Source, Pos)
and then Line_First_CP (Source, Pos) = CP
then
-- Expected_Is_Open(S, Pos, CP) = True
-- EOF(1,CP) = True or Old_Flag = True
-- New_Flag = True (from Pre)
-- Target: True = (anything or True) ✓
pragma Assert (Expected_Is_Open (Source, Pos, CP));
null;
else
-- Expected_Is_Open(S, Pos, CP) = EIOF(S, NL, CP)
-- New_Flag = Old_Flag
-- EOF(1,CP) = EIOF(Pos) or Old_Flag = EIOF(NL) or Old_Flag
-- Target: EIOF(NL) or New_Flag = EIOF(NL) or Old_Flag ✓
null;
end if;
end Lemma_Invariant_Step_Is_Open;
---------------------------------------------------------------------------
-- Ghost lemma: advance the Close_Flags invariant over one line.
---------------------------------------------------------------------------
procedure Lemma_Invariant_Step_Is_Close
(Source : Byte_Array;
Pos : Positive;
CP : Codepoint;
New_Flag : Boolean;
Old_Flag : Boolean)
with Ghost,
Always_Terminates,
Pre =>
Source'First = 1
and then Source'Last < Positive'Last
and then Pos in Source'Range
and then
Expected_Is_Close_From (Source, 1, CP) =
(Expected_Is_Close_From (Source, Pos, CP) or else Old_Flag)
and then
(if Is_Close_Line (Source, Pos)
and then Line_First_CP (Source, Pos) = CP
then New_Flag
else New_Flag = Old_Flag),
Post =>
(declare
NL : constant Positive := Next_Line_Start (Source, Pos);
begin
Expected_Is_Close_From (Source, 1, CP) =
(Expected_Is_Close_From (Source, NL, CP) or else New_Flag))
is
NL : constant Positive := Next_Line_Start (Source, Pos) with Ghost;
begin
pragma Assert
(Expected_Is_Close_From (Source, Pos, CP) =
Expected_Is_Close (Source, Pos, CP));
pragma Assert
(Expected_Is_Close_From (Source, NL, CP) =
(if NL > Source'Last then False
else Expected_Is_Close (Source, NL, CP)));
if Is_Close_Line (Source, Pos)
and then Line_First_CP (Source, Pos) = CP
then
pragma Assert (Expected_Is_Close (Source, Pos, CP));
null;
else
null;
end if;
end Lemma_Invariant_Step_Is_Close;
---------------------------------------------------------------------------
-- Process_Line: per-line field extraction and table update.
--
-- Extracts all three fields from the line at Line_Pos, validates them,
-- and updates the appropriate output tables. The postcondition
-- characterizes what changed in terms of the ghost spec predicates.
--
-- The mapping tables (Open_Table, Close_Table) are only updated when
-- Line_Paired_CP > 0, matching the ghost spec's "last non-zero writer
-- wins" semantics in Expected_Open_Mapping / Expected_Close_Mapping.
---------------------------------------------------------------------------
procedure Process_Line
(Source : Byte_Array;
Line_Pos : Positive;
Open_Table : in out Bracket_Table;
Close_Table : in out Bracket_Table;
Open_Flags : in out Bracket_Flag_Table;
Close_Flags : in out Bracket_Flag_Table;
Lines_Parsed : in out Natural)
with Pre =>
Source'First = 1
and then Source'Last < Positive'Last
and then Line_Pos in Source'Range
and then Lines_Parsed < Natural'Last
and then (for all CP in Codepoint =>
Open_Table (CP) <= Max_Codepoint
and then Close_Table (CP) <= Max_Codepoint),
Post =>
-- Range safety preserved
(for all CP in Codepoint =>
Open_Table (CP) <= Max_Codepoint
and then Close_Table (CP) <= Max_Codepoint)
-- Lines_Parsed incremented at most by 1
and then Lines_Parsed in Lines_Parsed'Old .. Lines_Parsed'Old + 1
-- Per-codepoint update characterization:
and then
(for all CP in Codepoint =>
-- Open_Table update (only for non-zero LPC)
(if Is_Open_Line (Source, Line_Pos)
and then Line_First_CP (Source, Line_Pos) = CP
and then Line_Paired_CP (Source, Line_Pos) <= Max_Codepoint
and then Line_Paired_CP (Source, Line_Pos) > 0
then Open_Table (CP) = Line_Paired_CP (Source, Line_Pos)
else Open_Table (CP) = Open_Table'Old (CP))
-- Close_Table update (only for non-zero LPC)
and then
(if Is_Close_Line (Source, Line_Pos)
and then Line_First_CP (Source, Line_Pos) = CP
and then Line_Paired_CP (Source, Line_Pos) <= Max_Codepoint
and then Line_Paired_CP (Source, Line_Pos) > 0
then Close_Table (CP) = Line_Paired_CP (Source, Line_Pos)
else Close_Table (CP) = Close_Table'Old (CP))
-- Open_Flags update (unconditional on covering)
and then
(if Is_Open_Line (Source, Line_Pos)
and then Line_First_CP (Source, Line_Pos) = CP
then Open_Flags (CP)
else Open_Flags (CP) = Open_Flags'Old (CP))
-- Close_Flags update (unconditional on covering)
and then
(if Is_Close_Line (Source, Line_Pos)
and then Line_First_CP (Source, Line_Pos) = CP
then Close_Flags (CP)
else Close_Flags (CP) = Close_Flags'Old (CP)))
is
F0 : Natural;
Semi1 : Natural;
CP1_N : Natural;
Hex_Len : Natural;
F1 : Natural;
CP2_N : Natural;
Hex_Len2 : Natural;
Semi2 : Natural;
TP : Natural;
Type_Byte : Byte;
begin
-- Step 1: Check if this is at least a UCD data line (field 0)
F0 := Skip_WS (Source, Line_Pos);
if F0 = 0 or else not Is_Hex_Digit (Source (F0)) then
return;
end if;
Semi1 := Find_Semi (Source, Line_Pos);
if Semi1 = 0 then
return;
end if;
-- Parse field 0: first codepoint
Parse_CP (Source, F0, CP1_N, Hex_Len);
if Hex_Len < 4 then
return;
end if;
-- Handle > 6 hex digits: Parse_CP caps at 6, but if the 7th byte
-- is also hex, Hex_Digit_Count > 6 → not Is_Data_Line.
if Hex_Len > 5 then
if F0 + Hex_Len <= Source'Last
and then Is_Hex_Digit (Source (F0 + Hex_Len))
then
Lemma_HDC_GT_6 (Source, F0);
return;
end if;
end if;
Lemma_Hex_Digit_Count (Source, F0, Hex_Len);
pragma Assert (UCD_Format_Spec.Is_Data_Line (Source, Line_Pos));
if CP1_N > Max_Codepoint then
pragma Assert
(CP1_N = UCD_Format_Spec.Line_First_CP (Source, Line_Pos));
return;
end if;
pragma Assert
(CP1_N = UCD_Format_Spec.Line_First_CP (Source, Line_Pos));
-- Step 2: Parse field 1 (paired codepoint)
if Semi1 >= Source'Last then
return;
end if;
F1 := Skip_WS (Source, Semi1 + 1);
if F1 = 0 or else not Is_Hex_Digit (Source (F1)) then
return;
end if;
Parse_CP (Source, F1, CP2_N, Hex_Len2);
if Hex_Len2 < 4 then
return;
end if;
-- Handle > 6 hex digits for field 1
if Hex_Len2 > 5 then
if F1 + Hex_Len2 <= Source'Last
and then Is_Hex_Digit (Source (F1 + Hex_Len2))
then
Lemma_HDC_GT_6 (Source, F1);
return;
end if;
end if;
Lemma_Hex_Digit_Count (Source, F1, Hex_Len2);
-- Note: when CP2_N > Max_Codepoint, we do NOT return here.
-- The flag postconditions (Open_Flags, Close_Flags) require flags
-- to be set whenever Is_Open_Line/Is_Close_Line and Line_First_CP = CP,
-- regardless of Line_Paired_CP. Fall through to process type field.
-- Step 3: Find second semicolon and parse type field
if Source'Last - F1 < Hex_Len2 then
return;
end if;
Semi2 := Find_Semi (Source, F1 + Hex_Len2);
if Semi2 = 0 or else Semi2 >= Source'Last then
return;
end if;
TP := Skip_WS (Source, Semi2 + 1);
if TP = 0 then
return;
end if;
Type_Byte := Source (TP);
-- Bridge assertions: connect runtime values to ghost spec functions.
pragma Assert
(F1 = UCD_Format_Spec.Skip_Spaces (Source, Semi1 + 1));
pragma Assert
(Semi1 = UCD_Format_Spec.Find_Semicolon (Source, Line_Pos));
pragma Assert (Bidi_Brackets_Spec.Field1_Start (Source, Line_Pos) = F1);
pragma Assert
(Bidi_Brackets_Spec.Field1_Hex_Count (Source, Line_Pos) = Hex_Len2);
pragma Assert
(Semi2 = UCD_Format_Spec.Find_Semicolon (Source, F1 + Hex_Len2));
pragma Assert
(Bidi_Brackets_Spec.Find_Second_Semi (Source, Line_Pos) = Semi2);
pragma Assert
(TP = UCD_Format_Spec.Skip_Spaces (Source, Semi2 + 1));
pragma Assert
(Bidi_Brackets_Spec.Type_Field_Pos (Source, Line_Pos) = TP);
if Type_Byte = Lower_O_Byte then
-- Open bracket line.
pragma Assert
(Bidi_Brackets_Spec.Is_Bracket_Data_Line (Source, Line_Pos));
pragma Assert
(Bidi_Brackets_Spec.Is_Open_Line (Source, Line_Pos));
pragma Assert
(not Bidi_Brackets_Spec.Is_Close_Line (Source, Line_Pos));
pragma Assert
(UCD_Format_Spec.Line_First_CP (Source, Line_Pos) = CP1_N);
pragma Assert
(Bidi_Brackets_Spec.Line_Paired_CP (Source, Line_Pos) = CP2_N);
-- Only update mapping table when paired CP is non-zero and in range
if CP2_N <= Max_Codepoint and then CP2_N > 0 then
Open_Table (CP1_N) := CP2_N;
end if;
Open_Flags (CP1_N) := True;
Lines_Parsed := Lines_Parsed + 1;
elsif Type_Byte = Lower_C_Byte then
-- Close bracket line.
pragma Assert
(Bidi_Brackets_Spec.Is_Bracket_Data_Line (Source, Line_Pos));
pragma Assert
(Bidi_Brackets_Spec.Is_Close_Line (Source, Line_Pos));
pragma Assert
(not Bidi_Brackets_Spec.Is_Open_Line (Source, Line_Pos));
pragma Assert
(UCD_Format_Spec.Line_First_CP (Source, Line_Pos) = CP1_N);
pragma Assert
(Bidi_Brackets_Spec.Line_Paired_CP (Source, Line_Pos) = CP2_N);
-- Only update mapping table when paired CP is non-zero and in range
if CP2_N <= Max_Codepoint and then CP2_N > 0 then
Close_Table (CP1_N) := CP2_N;
end if;
Close_Flags (CP1_N) := True;
Lines_Parsed := Lines_Parsed + 1;
else
-- Type byte is neither 'o' nor 'c': not Is_Bracket_Data_Line.
pragma Assert
(not Bidi_Brackets_Spec.Is_Bracket_Data_Line (Source, Line_Pos));
null;
end if;
end Process_Line;
---------------------------------------------------------------------------
-- Parse_Brackets_File
---------------------------------------------------------------------------
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)
is
Line_Pos : Positive := 1;
begin
Open_Table := [others => 0];
Close_Table := [others => 0];
Open_Flags := [others => False];
Close_Flags := [others => False];
Lines_Parsed := 0;
while Line_Pos <= Source'Last loop
-- Lines_Parsed < Line_Pos <= Source'Last < Positive'Last = Natural'Last
-- so Lines_Parsed < Natural'Last, satisfying Process_Line's Pre.
Process_Line (Source, Line_Pos,
Open_Table, Close_Table,
Open_Flags, Close_Flags,
Lines_Parsed);
pragma Assert
(for all CP in Codepoint =>
Open_Table (CP) <= Max_Codepoint
and then Close_Table (CP) <= Max_Codepoint);
Line_Pos := Next_Line (Source, Line_Pos);
pragma Loop_Invariant (Line_Pos in 2 .. Source'Last + 1);
-- Lines_Parsed < Line_Pos: each iteration increments Lines_Parsed
-- by at most 1 and Line_Pos by at least 1.
pragma Loop_Invariant (Lines_Parsed < Line_Pos);
pragma Loop_Invariant
(for all CP in Codepoint =>
Open_Table (CP) <= Max_Codepoint
and then Close_Table (CP) <= Max_Codepoint);
-- Correctness invariant, Part A: if future lines will still
-- assign a non-zero value, the Expected_From at start equals
-- Expected_From at the current position.
pragma Loop_Invariant
(for all CP in Codepoint =>
(if Expected_Open_From (Source, Line_Pos, CP) /= 0
then
Expected_Open_From (Source, 1, CP) =
Expected_Open_From (Source, Line_Pos, CP)));
pragma Loop_Invariant
(for all CP in Codepoint =>
(if Expected_Close_From (Source, Line_Pos, CP) /= 0
then
Expected_Close_From (Source, 1, CP) =
Expected_Close_From (Source, Line_Pos, CP)));
-- Correctness invariant, Part B: if future lines won't assign,
-- the table already holds the correct value.
pragma Loop_Invariant
(for all CP in Codepoint =>
(if Expected_Open_From (Source, Line_Pos, CP) = 0
then
Expected_Open_From (Source, 1, CP) =
Open_Table (CP)));
pragma Loop_Invariant
(for all CP in Codepoint =>
(if Expected_Close_From (Source, Line_Pos, CP) = 0
then
Expected_Close_From (Source, 1, CP) =
Close_Table (CP)));
-- Boolean flag invariants use OR semantics.
pragma Loop_Invariant
(for all CP in Codepoint =>
Expected_Is_Open_From (Source, 1, CP) =
(Expected_Is_Open_From (Source, Line_Pos, CP)
or else Open_Flags (CP)));
pragma Loop_Invariant
(for all CP in Codepoint =>
Expected_Is_Close_From (Source, 1, CP) =
(Expected_Is_Close_From (Source, Line_Pos, CP)
or else Close_Flags (CP)));
pragma Loop_Variant (Increases => Line_Pos);
end loop;
-- After the loop: Line_Pos > Source'Last.
-- The opaque wrapper postconditions give us:
-- Expected_Open_From(S, Line_Pos, CP) = 0 (since Line_Pos > S'Last)
-- Expected_Close_From(S, Line_Pos, CP) = 0
-- Expected_Is_Open_From(S, Line_Pos, CP) = False
-- Expected_Is_Close_From(S, Line_Pos, CP) = False
--
-- Part B of each invariant then gives the postcondition:
-- Open_Table(CP) = Expected_Open_From(S, 1, CP)
-- Boolean: Expected_Is_Open_From(S, 1, CP) = (False or Open_Flags(CP))
-- = Open_Flags(CP)
pragma Assert
(for all CP in Codepoint =>
Expected_Open_From (Source, Line_Pos, CP) = 0);
pragma Assert
(for all CP in Codepoint =>
Expected_Close_From (Source, Line_Pos, CP) = 0);
pragma Assert
(for all CP in Codepoint =>
Expected_Is_Open_From (Source, Line_Pos, CP) = False);
pragma Assert
(for all CP in Codepoint =>
Expected_Is_Close_From (Source, Line_Pos, CP) = False);
-- Combine Part B invariant with the defaulting assertions above
-- to establish the postcondition.
pragma Assert
(for all CP in Codepoint =>
Open_Table (CP) = Expected_Open_From (Source, 1, CP));
pragma Assert
(for all CP in Codepoint =>
Close_Table (CP) = Expected_Close_From (Source, 1, CP));
pragma Assert
(for all CP in Codepoint =>
Open_Flags (CP) = Expected_Is_Open_From (Source, 1, CP));
pragma Assert
(for all CP in Codepoint =>
Close_Flags (CP) = Expected_Is_Close_From (Source, 1, CP));
Success := Lines_Parsed >= Min_Expected_Lines;
end Parse_Brackets_File;
end Lingenic_Text.Bidi_Brackets_Parser;