-- 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 body
--
-- Full Unicode Bidirectional Algorithm (UAX #9).
--
-- Initialize is SPARK_Mode Off because it calls File_IO.Read_File
-- and performs custom BidiBrackets.txt parsing.
-- Everything else is proved SPARK.
-------------------------------------------------------------------------------
with Lingenic_Text.File_IO;
with Lingenic_Text.UTF8;
package body Lingenic_Text.Bidi
with SPARK_Mode,
Refined_State => (Bidi_State =>
(Is_Init,
Bracket_Open_Table, Bracket_Close_Table,
Is_Open_Bracket, Is_Close_Bracket,
Init_Buffer, Init_Length))
is
Is_Init : Boolean := False;
-- Bracket pair lookup tables (O(1) by codepoint).
-- Bracket_Open_Table(CP) = paired closing CP, or No_Bracket sentinel.
-- Bracket_Close_Table(CP) = paired opening CP, or No_Bracket sentinel.
-- Sentinel value: Codepoint'Last + 1 = 16#11_0000# doesn't fit in
-- Codepoint, so we use a separate Boolean table instead.
type Bracket_Table is array (Codepoint) of Codepoint;
type Bracket_Flag_Table is array (Codepoint) of Boolean;
Bracket_Open_Table : Bracket_Table := [others => 0];
pragma Warnings (Off, Bracket_Open_Table);
-- Part of Bidi_State; populated during Initialize but only consumed
-- via Is_Open_Bracket at runtime (the table provides closing-bracket
-- values that are not needed by the current N0 algorithm).
Bracket_Close_Table : Bracket_Table := [others => 0];
Is_Open_Bracket : Bracket_Flag_Table := [others => False];
Is_Close_Bracket : Bracket_Flag_Table := [others => False];
-- File buffer for reading BidiBrackets.txt
Init_Buffer : File_IO.File_Byte_Array := [others => 0];
Init_Length : File_IO.File_Size := 0;
---------------------------------------------------------------------------
-- Initialized
---------------------------------------------------------------------------
function Initialized return Boolean
is (Is_Init);
---------------------------------------------------------------------------
-- Initialize
--
-- Read BidiBrackets.txt and populate bracket pair tables.
-- Format: "HHHH; HHHH; o/c"
-- SPARK_Mode Off: calls File_IO.Read_File.
---------------------------------------------------------------------------
procedure Initialize
(UCD_Dir : String;
Success : out Boolean)
with SPARK_Mode => Off
is
OK : Boolean;
function Hex_Value (B : Natural) return Natural is
begin
if B >= Character'Pos ('0') and B <= Character'Pos ('9') then
return B - Character'Pos ('0');
elsif B >= Character'Pos ('A') and B <= Character'Pos ('F') then
return B - Character'Pos ('A') + 10;
elsif B >= Character'Pos ('a') and B <= Character'Pos ('f') then
return B - Character'Pos ('a') + 10;
else
return 16; -- invalid
end if;
end Hex_Value;
Pos : Positive := 1;
CP1, CP2 : Natural;
Digit : Natural;
Bracket_Type_Byte : Natural;
begin
-- Reset state
Is_Init := False;
for CP in Codepoint loop
Bracket_Open_Table (CP) := 0;
Bracket_Close_Table (CP) := 0;
Is_Open_Bracket (CP) := False;
Is_Close_Bracket (CP) := False;
end loop;
for I in Init_Buffer'Range loop
Init_Buffer (I) := 0;
end loop;
Init_Length := 0;
Success := False;
-- Read BidiBrackets.txt
File_IO.Read_File
(UCD_Dir & "/BidiBrackets.txt", Init_Buffer, Init_Length, OK);
if not OK or Init_Length = 0 then return; end if;
-- Parse line by line
Pos := 1;
while Pos <= Init_Length loop
-- Skip comment lines and blank lines
if Init_Buffer (Pos) = Character'Pos ('#')
or Init_Buffer (Pos) = Character'Pos (ASCII.LF)
or Init_Buffer (Pos) = Character'Pos (ASCII.CR)
then
-- Skip to end of line
while Pos <= Init_Length
and then Init_Buffer (Pos) /= Character'Pos (ASCII.LF)
loop
Pos := Pos + 1;
end loop;
if Pos <= Init_Length then Pos := Pos + 1; end if;
else
-- Parse: "HHHH; HHHH; o/c"
-- Field 0: hex codepoint
CP1 := 0;
while Pos <= Init_Length
and then Hex_Value (Init_Buffer (Pos)) < 16
loop
Digit := Hex_Value (Init_Buffer (Pos));
CP1 := CP1 * 16 + Digit;
Pos := Pos + 1;
end loop;
-- Skip "; "
while Pos <= Init_Length
and then (Init_Buffer (Pos) = Character'Pos (';')
or Init_Buffer (Pos) = Character'Pos (' '))
loop
Pos := Pos + 1;
end loop;
-- Field 1: paired codepoint
CP2 := 0;
while Pos <= Init_Length
and then Hex_Value (Init_Buffer (Pos)) < 16
loop
Digit := Hex_Value (Init_Buffer (Pos));
CP2 := CP2 * 16 + Digit;
Pos := Pos + 1;
end loop;
-- Skip "; "
while Pos <= Init_Length
and then (Init_Buffer (Pos) = Character'Pos (';')
or Init_Buffer (Pos) = Character'Pos (' '))
loop
Pos := Pos + 1;
end loop;
-- Field 2: bracket type (o or c)
if Pos <= Init_Length then
Bracket_Type_Byte := Init_Buffer (Pos);
Pos := Pos + 1;
else
Bracket_Type_Byte := 0;
end if;
-- Store in tables
if CP1 <= Codepoint'Last and CP2 <= Codepoint'Last then
if Bracket_Type_Byte = Character'Pos ('o') then
-- Opening bracket: CP1 maps to its closing pair CP2
Bracket_Open_Table (CP1) := CP2;
Is_Open_Bracket (CP1) := True;
elsif Bracket_Type_Byte = Character'Pos ('c') then
-- Closing bracket: CP1 maps to its opening pair CP2
Bracket_Close_Table (CP1) := CP2;
Is_Close_Bracket (CP1) := True;
end if;
end if;
-- Skip to end of line
while Pos <= Init_Length
and then Init_Buffer (Pos) /= Character'Pos (ASCII.LF)
loop
Pos := Pos + 1;
end loop;
if Pos <= Init_Length then Pos := Pos + 1; end if;
end if;
end loop;
Is_Init := True;
Success := True;
end Initialize;
---------------------------------------------------------------------------
-- Internal types
---------------------------------------------------------------------------
subtype Para_Index is Positive range 1 .. Max_Paragraph_CPs;
type CP_Array is array (Para_Index) of Codepoint;
type BC_Array is array (Para_Index) of BC_Value;
type Level_Work_Array is array (Para_Index) of Embedding_Level;
-- Directional status stack (X1)
type Stack_Array is array (1 .. Max_Stack) of Stack_Entry;
-- Match arrays for isolate pairing
type Match_Array is array (Para_Index) of Natural;
---------------------------------------------------------------------------
-- Resolve_Levels
---------------------------------------------------------------------------
procedure Resolve_Levels
(Text : Byte_Array;
Dir : Paragraph_Direction;
Levels : out Level_Array;
Num_CPs : out Paragraph_Length;
Para_Level : out Embedding_Level;
Success : out Boolean)
is
-- Work arrays
CPs : CP_Array := [others => 0];
Types : BC_Array := [others => BC_L];
Orig_Types : BC_Array := [others => BC_L];
Work_Levels : Level_Work_Array;
Embed_Levels : Level_Work_Array := [others => 0]; -- X1-X8 levels (before I1/I2)
Match_PDI : Match_Array := [others => 0]; -- isolate → PDI index
Num : Natural := 0;
-- Current paragraph level (determined by P2/P3 or forced)
PL : Embedding_Level;
-- Ghost type conversion: BC_Array → Ghost_BC_Array (top-level scope)
function To_GBC_Outer (Src : BC_Array) return Ghost_BC_Array
with Ghost,
Post => (for all I in 1 .. Max_Paragraph_CPs =>
To_GBC_Outer'Result (I) = Src (I))
is
Result : Ghost_BC_Array := [others => BC_Default];
begin
for I in 1 .. Max_Paragraph_CPs loop
Result (I) := Src (I);
pragma Loop_Invariant
(for all J in 1 .. I =>
Result (J) = Src (J));
end loop;
return Result;
end To_GBC_Outer;
-----------------------------------------------------------------------
-- Phase 1: Decode paragraph (UTF-8 → codepoints + Bidi_Class)
-----------------------------------------------------------------------
procedure Decode_Paragraph
(OK : out Boolean)
with Global => (Input => (Text, Properties.Property_State),
In_Out => (Num, CPs, Types, Orig_Types)),
Pre => Properties.Initialized
and then Text'Length >= 1
and then Text'Last < Positive'Last
and then Num = 0,
Post => (if OK then
Num >= 1
and then Num <= Max_Paragraph_CPs
else
Num = 0)
is
Pos : Positive := Text'First;
CP : Codepoint;
Len : Positive;
Valid : Boolean;
BC : BC_Value;
begin
OK := False;
Num := 0;
while Pos <= Text'Last loop
UTF8.Decode (Text, Pos, CP, Len, Valid);
if not Valid then
-- Invalid UTF-8
Num := 0;
return;
end if;
Num := Num + 1;
if Num > Max_Paragraph_CPs then
Num := 0;
return;
end if;
CPs (Num) := CP;
BC := Properties.Get_BC (CP);
Types (Num) := BC;
Orig_Types (Num) := BC;
Pos := Pos + Len;
pragma Loop_Variant (Increases => Pos);
pragma Loop_Invariant (Num >= 1 and Num <= Max_Paragraph_CPs);
pragma Loop_Invariant (Pos >= Text'First);
end loop;
if Num >= 1 then
OK := True;
end if;
end Decode_Paragraph;
-----------------------------------------------------------------------
-- Phase 2: Determine paragraph level (P2/P3)
--
-- P2: Find the first character of type L, AL, or R while
-- skipping any characters between an isolate initiator and
-- its matching PDI or the end of the paragraph.
-- P3: If a character is found in P2, set paragraph level per
-- P3_Level; otherwise set to 0.
-----------------------------------------------------------------------
function To_Ghost_BC (Src : BC_Array) return Ghost_BC_Array
with Ghost,
Post => (for all I in 1 .. Max_Paragraph_CPs =>
To_Ghost_BC'Result (I) = Src (I))
is
Result : Ghost_BC_Array := [others => BC_Default];
begin
for I in 1 .. Max_Paragraph_CPs loop
Result (I) := Src (I);
pragma Loop_Invariant
(for all J in 1 .. I =>
Result (J) = Src (J));
end loop;
return Result;
end To_Ghost_BC;
procedure Determine_Para_Level
with Global => (Input => (Dir, Types, Num),
Output => PL),
Pre => Num >= 1 and Num <= Max_Paragraph_CPs,
Post => PL <= 1
and then
(if Dir = Dir_LTR then PL = 0
elsif Dir = Dir_RTL then PL = 1
else PL = P3_Level (Ghost_First_Strong_All
(To_Ghost_BC (Types), Num)))
is
Isolate_Count : Natural := 0;
First_Strong : BC_Value := BC_Default;
Types_G : constant Ghost_BC_Array := To_Ghost_BC (Types)
with Ghost;
begin
case Dir is
when Dir_LTR =>
PL := 0;
return;
when Dir_RTL =>
PL := 1;
return;
when Dir_Auto =>
null;
end case;
-- P2: scan for first strong character, skipping isolate pairs
for I in 1 .. Num loop
pragma Loop_Invariant (Isolate_Count <= I);
pragma Loop_Invariant (Isolate_Count <= Max_Paragraph_CPs);
pragma Loop_Invariant (First_Strong = BC_Default);
pragma Loop_Invariant
(Ghost_First_Strong (Types_G, Num, I, Isolate_Count) =
Ghost_First_Strong_All (Types_G, Num));
if Is_Isolate_Initiator (Types (I)) then
Isolate_Count := Isolate_Count + 1;
elsif Types (I) = BC_PDI then
if Isolate_Count > 0 then
Isolate_Count := Isolate_Count - 1;
end if;
elsif Isolate_Count = 0 and then Is_Strong (Types (I)) then
First_Strong := Types (I);
pragma Assert
(First_Strong = Ghost_First_Strong (Types_G, Num, I, Isolate_Count));
pragma Assert
(First_Strong = Ghost_First_Strong_All (Types_G, Num));
exit;
end if;
end loop;
-- P3
PL := P3_Level (First_Strong);
pragma Assert
(PL = P3_Level (Ghost_First_Strong_All (Types_G, Num)));
end Determine_Para_Level;
-----------------------------------------------------------------------
-- Phase 3: Resolve explicit levels (X1–X8)
--
-- Builds the directional status stack and resolves embedding
-- levels. Also builds the Match_PDI array for isolate
-- pairing (used by X9/X10 to identify isolating run sequences).
-----------------------------------------------------------------------
procedure Resolve_Explicit_Levels
with Global => (Input => (PL, Num, Orig_Types),
In_Out => (Types, Work_Levels, Match_PDI)),
Pre => Num >= 1
and then Num <= Max_Paragraph_CPs
and then PL <= 1,
Post => (for all I in 1 .. Num =>
Work_Levels (I) <= Max_Depth)
is
-- Directional status stack (X1)
DS_Stack : Stack_Array :=
[others => (Level => 0, Override => Neutral, Isolate => False)];
Stack_Top : Natural;
Overflow_Isolate : Natural;
Overflow_Embedding : Natural;
Valid_Isolate : Natural;
New_Level : Natural;
begin
-- X1: Initialize stack with paragraph level entry
Stack_Top := 1;
DS_Stack (1) := (Level => PL,
Override => Neutral,
Isolate => False);
Overflow_Isolate := 0;
Overflow_Embedding := 0;
Valid_Isolate := 0;
for I in 1 .. Num loop
declare
T : constant BC_Value := Types (I);
Cur_Level : constant Explicit_Level := DS_Stack (Stack_Top).Level;
begin
-- X2: RLE
if T = BC_RLE then
New_Level := Next_Odd (Cur_Level);
if New_Level <= Max_Depth
and then Overflow_Isolate = 0
and then Overflow_Embedding = 0
then
if Stack_Top < Max_Stack then
Stack_Top := Stack_Top + 1;
DS_Stack (Stack_Top) :=
(Level => New_Level,
Override => Neutral,
Isolate => False);
else
Overflow_Embedding := Overflow_Embedding + 1;
end if;
else
if Overflow_Isolate = 0 then
Overflow_Embedding := Overflow_Embedding + 1;
end if;
end if;
Work_Levels (I) := Cur_Level;
-- X3: LRE
elsif T = BC_LRE then
New_Level := Next_Even (Cur_Level);
if New_Level <= Max_Depth
and then Overflow_Isolate = 0
and then Overflow_Embedding = 0
then
if Stack_Top < Max_Stack then
Stack_Top := Stack_Top + 1;
DS_Stack (Stack_Top) :=
(Level => New_Level,
Override => Neutral,
Isolate => False);
else
Overflow_Embedding := Overflow_Embedding + 1;
end if;
else
if Overflow_Isolate = 0 then
Overflow_Embedding := Overflow_Embedding + 1;
end if;
end if;
Work_Levels (I) := Cur_Level;
-- X4: RLO
elsif T = BC_RLO then
New_Level := Next_Odd (Cur_Level);
if New_Level <= Max_Depth
and then Overflow_Isolate = 0
and then Overflow_Embedding = 0
then
if Stack_Top < Max_Stack then
Stack_Top := Stack_Top + 1;
DS_Stack (Stack_Top) :=
(Level => New_Level,
Override => Right_To_Left,
Isolate => False);
else
Overflow_Embedding := Overflow_Embedding + 1;
end if;
else
if Overflow_Isolate = 0 then
Overflow_Embedding := Overflow_Embedding + 1;
end if;
end if;
Work_Levels (I) := Cur_Level;
-- X5: LRO
elsif T = BC_LRO then
New_Level := Next_Even (Cur_Level);
if New_Level <= Max_Depth
and then Overflow_Isolate = 0
and then Overflow_Embedding = 0
then
if Stack_Top < Max_Stack then
Stack_Top := Stack_Top + 1;
DS_Stack (Stack_Top) :=
(Level => New_Level,
Override => Left_To_Right,
Isolate => False);
else
Overflow_Embedding := Overflow_Embedding + 1;
end if;
else
if Overflow_Isolate = 0 then
Overflow_Embedding := Overflow_Embedding + 1;
end if;
end if;
Work_Levels (I) := Cur_Level;
-- X5a: RLI
elsif T = BC_RLI then
Work_Levels (I) := Cur_Level;
if DS_Stack (Stack_Top).Override = Right_To_Left then
Types (I) := BC_R;
elsif DS_Stack (Stack_Top).Override = Left_To_Right then
Types (I) := BC_L;
end if;
New_Level := Next_Odd (Cur_Level);
if New_Level <= Max_Depth
and then Overflow_Isolate = 0
and then Overflow_Embedding = 0
then
Valid_Isolate := Valid_Isolate + 1;
if Stack_Top < Max_Stack then
Stack_Top := Stack_Top + 1;
DS_Stack (Stack_Top) :=
(Level => New_Level,
Override => Neutral,
Isolate => True);
end if;
else
Overflow_Isolate := Overflow_Isolate + 1;
end if;
-- X5b: LRI
elsif T = BC_LRI then
Work_Levels (I) := Cur_Level;
if DS_Stack (Stack_Top).Override = Right_To_Left then
Types (I) := BC_R;
elsif DS_Stack (Stack_Top).Override = Left_To_Right then
Types (I) := BC_L;
end if;
New_Level := Next_Even (Cur_Level);
if New_Level <= Max_Depth
and then Overflow_Isolate = 0
and then Overflow_Embedding = 0
then
Valid_Isolate := Valid_Isolate + 1;
if Stack_Top < Max_Stack then
Stack_Top := Stack_Top + 1;
DS_Stack (Stack_Top) :=
(Level => New_Level,
Override => Neutral,
Isolate => True);
end if;
else
Overflow_Isolate := Overflow_Isolate + 1;
end if;
-- X5c: FSI — determine embedding direction, then act as
-- RLI or LRI
elsif T = BC_FSI then
-- Determine the direction the same way as P2/P3 but
-- scanning from the next character to the matching PDI
declare
FSI_Level : Embedding_Level := 0;
Depth : Natural := 1;
begin
for J in I + 1 .. Num loop
if Is_Isolate_Initiator (Types (J)) then
Depth := Depth + 1;
elsif Types (J) = BC_PDI then
if Depth > 1 then
Depth := Depth - 1;
else
exit;
end if;
elsif Depth = 1 and then Is_Strong (Types (J)) then
FSI_Level := P3_Level (Types (J));
exit;
end if;
pragma Loop_Invariant (Depth <= J - I + 1);
end loop;
-- Now act as RLI (if level=1) or LRI (if level=0)
Work_Levels (I) := Cur_Level;
if DS_Stack (Stack_Top).Override = Right_To_Left then
Types (I) := BC_R;
elsif DS_Stack (Stack_Top).Override = Left_To_Right then
Types (I) := BC_L;
end if;
if FSI_Level = 1 then
New_Level := Next_Odd (Cur_Level);
else
New_Level := Next_Even (Cur_Level);
end if;
if New_Level <= Max_Depth
and then Overflow_Isolate = 0
and then Overflow_Embedding = 0
then
Valid_Isolate := Valid_Isolate + 1;
if Stack_Top < Max_Stack then
Stack_Top := Stack_Top + 1;
DS_Stack (Stack_Top) :=
(Level => New_Level,
Override => Neutral,
Isolate => True);
end if;
else
Overflow_Isolate := Overflow_Isolate + 1;
end if;
end;
-- X6a: PDI
elsif T = BC_PDI then
if Overflow_Isolate > 0 then
Overflow_Isolate := Overflow_Isolate - 1;
elsif Valid_Isolate > 0 then
Overflow_Embedding := 0;
-- Pop stack until we find the isolate entry
while Stack_Top > 1
and then not DS_Stack (Stack_Top).Isolate
loop
Stack_Top := Stack_Top - 1;
pragma Loop_Invariant (Stack_Top >= 1
and Stack_Top <= Max_Stack);
end loop;
-- Pop the isolate entry itself
if Stack_Top > 1 then
Stack_Top := Stack_Top - 1;
end if;
Valid_Isolate := Valid_Isolate - 1;
end if;
Work_Levels (I) := DS_Stack (Stack_Top).Level;
if DS_Stack (Stack_Top).Override = Right_To_Left then
Types (I) := BC_R;
elsif DS_Stack (Stack_Top).Override = Left_To_Right then
Types (I) := BC_L;
end if;
-- X7: PDF
elsif T = BC_PDF then
if Overflow_Isolate > 0 then
null; -- do nothing
elsif Overflow_Embedding > 0 then
Overflow_Embedding := Overflow_Embedding - 1;
elsif Stack_Top > 1
and then not DS_Stack (Stack_Top).Isolate
then
Stack_Top := Stack_Top - 1;
end if;
Work_Levels (I) := DS_Stack (Stack_Top).Level;
-- X8: B (paragraph separator) — end of paragraph
elsif T = BC_B then
Work_Levels (I) := PL;
-- X6: All other types
else
Work_Levels (I) := DS_Stack (Stack_Top).Level;
if DS_Stack (Stack_Top).Override = Right_To_Left then
Types (I) := BC_R;
elsif DS_Stack (Stack_Top).Override = Left_To_Right then
Types (I) := BC_L;
end if;
end if;
end;
pragma Loop_Invariant (Stack_Top >= 1 and Stack_Top <= Max_Stack);
pragma Loop_Invariant (Overflow_Embedding <= I);
pragma Loop_Invariant (Overflow_Isolate <= I);
pragma Loop_Invariant (Valid_Isolate <= I);
pragma Loop_Invariant
(for all J in 1 .. I =>
Work_Levels (J) <= Max_Depth);
end loop;
-- Build Match_PDI array
-- (map each isolate initiator to its matching PDI)
declare
Depth : Natural;
begin
for I in 1 .. Num loop
Match_PDI (I) := 0;
end loop;
for I in 1 .. Num loop
if Is_Isolate_Initiator (Orig_Types (I))
or Orig_Types (I) = BC_FSI
then
Depth := 1;
for J in I + 1 .. Num loop
if Is_Isolate_Initiator (Orig_Types (J))
or Orig_Types (J) = BC_FSI
then
Depth := Depth + 1;
elsif Orig_Types (J) = BC_PDI then
if Depth > 0 then
Depth := Depth - 1;
if Depth = 0 then
Match_PDI (I) := J;
exit;
end if;
end if;
end if;
pragma Loop_Invariant (Depth <= J - I + 1);
end loop;
end if;
end loop;
end;
end Resolve_Explicit_Levels;
-----------------------------------------------------------------------
-- Phase 4: Process isolating run sequences
--
-- X9: Remove RLE, LRE, RLO, LRO, PDF, BN from consideration
-- X10: Compute isolating run sequences, determine sos/eos
-- W1–W7: Weak type resolution
-- N0: Bracket pair resolution (BD16)
-- N1–N2: Neutral type resolution
-- I1–I2: Implicit level resolution
-----------------------------------------------------------------------
procedure Process_Run_Sequences
with Global => (Input => (PL, Num, CPs, Orig_Types,
Match_PDI,
Embed_Levels,
Bracket_Close_Table,
Is_Open_Bracket,
Is_Close_Bracket),
In_Out => (Types, Work_Levels)),
Pre => Num >= 1
and then Num <= Max_Paragraph_CPs
and then PL <= 1
and then (for all I in 1 .. Num =>
Work_Levels (I) <= Max_Depth)
and then (for all I in 1 .. Num =>
Embed_Levels (I) <= Max_Depth),
Post => (for all I in 1 .. Num =>
Work_Levels (I) <= Max_Depth + 1)
is
-- Sequence members: indices into the paragraph that form one
-- isolating run sequence (X9 removed characters are skipped)
type Seq_Index_Array is array (Para_Index) of Natural;
Seq : Seq_Index_Array := [others => 0];
Seq_Len : Natural;
-- Track which positions have been visited (to avoid re-processing)
type Visited_Array is array (Para_Index) of Boolean;
Visited : Visited_Array := [others => False];
-- sos (start of sequence) and eos (end of sequence)
SOS, EOS : BC_Value;
-- Get the embedding level of a position (treating X9-removed as
-- inheriting the preceding level). Uses Embed_Levels (the X1-X8
-- output, before I1/I2) so that sos/eos computation is not affected
-- by implicit level adjustments from earlier run sequences.
function Effective_Level (Idx : Para_Index) return Embedding_Level
is
begin
if not Is_X9_Removed (Orig_Types (Idx)) then
return Embed_Levels (Idx);
end if;
-- Walk backward to find a non-removed level
for K in reverse 1 .. Idx - 1 loop
if not Is_X9_Removed (Orig_Types (K)) then
return Embed_Levels (K);
end if;
end loop;
return PL;
end Effective_Level;
-- Ghost conversion: Seq_Index_Array → Ghost_Seq_Array
function To_Ghost_Seq (Src : Seq_Index_Array) return Ghost_Seq_Array
with Ghost,
Post => (for all I in 1 .. Max_Paragraph_CPs =>
To_Ghost_Seq'Result (I) = Src (I))
is
Result : Ghost_Seq_Array := [others => 0];
begin
for I in 1 .. Max_Paragraph_CPs loop
Result (I) := Src (I);
pragma Loop_Invariant
(for all J in 1 .. I =>
Result (J) = Src (J));
end loop;
return Result;
end To_Ghost_Seq;
-- Ghost conversion: BC_Array → Ghost_BC_Array (local copy for W rules)
function To_GBC (Src : BC_Array) return Ghost_BC_Array
with Ghost,
Post => (for all I in 1 .. Max_Paragraph_CPs =>
To_GBC'Result (I) = Src (I))
is
Result : Ghost_BC_Array := [others => BC_Default];
begin
for I in 1 .. Max_Paragraph_CPs loop
Result (I) := Src (I);
pragma Loop_Invariant
(for all J in 1 .. I =>
Result (J) = Src (J));
end loop;
return Result;
end To_GBC;
-- ---------------------------------------------------------------
-- W rules: operate on Types array for positions in Seq(1..Seq_Len)
-- ---------------------------------------------------------------
function Seq_Unique return Boolean
is (Seq_Len <= Max_Paragraph_CPs
and then
(for all I in 1 .. Seq_Len =>
Seq (I) >= 1
and then Seq (I) <= Max_Paragraph_CPs)
and then
(for all A in 1 .. Seq_Len =>
(for all B in A + 1 .. Seq_Len =>
Seq (A) /= Seq (B))))
with Ghost,
Global => (Input => (Seq, Seq_Len));
procedure Apply_W1
with Global => (Input => (Seq, Seq_Len, SOS),
In_Out => Types),
Pre => Seq_Len >= 1
and then Seq_Len <= Max_Paragraph_CPs
and then Seq_Unique,
Post => (for all S in 1 .. Seq_Len =>
(if Seq (S) >= 1
and then Seq (S) <= Max_Paragraph_CPs
then Types (Seq (S)) =
W1_Resolved (Types'Old (Seq (S)),
Ghost_W1_Prev
(To_GBC (Types'Old),
To_Ghost_Seq (Seq),
S, SOS),
S = 1)))
-- Frame: positions not in the sequence are unchanged
and then
(for all I in 1 .. Max_Paragraph_CPs =>
(if (for all S in 1 .. Seq_Len => Seq (S) /= I)
then Types (I) = Types'Old (I)))
is
Prev : BC_Value := SOS;
Idx : Natural;
Types_Orig : constant BC_Array := Types with Ghost;
Types_G : constant Ghost_BC_Array := To_GBC (Types) with Ghost;
Seq_G : constant Ghost_Seq_Array := To_Ghost_Seq (Seq) with Ghost;
W1_Done : array (1 .. Max_Paragraph_CPs) of Boolean :=
[others => False] with Ghost;
begin
for S in 1 .. Seq_Len loop
Idx := Seq (S);
if Idx >= 1 and Idx <= Max_Paragraph_CPs then
-- Uniqueness: no earlier K < S has Seq(K) = Idx.
pragma Assert
(for all K in 1 .. S - 1 => Seq (K) /= Seq (S));
pragma Assert (not W1_Done (Idx));
-- Therefore Types(Idx) = original.
pragma Assert (Types (Idx) = Types_G (Idx));
-- The ghost Prev matches the runtime Prev:
pragma Assert
(Prev = Ghost_W1_Prev (Types_G, Seq_G, S, SOS));
Types (Idx) := W1_Resolved (Types (Idx), Prev, S = 1);
Prev := Types (Idx);
W1_Done (Idx) := True;
end if;
pragma Loop_Invariant
(for all I in 1 .. Max_Paragraph_CPs =>
(if W1_Done (I) then
(for some K in 1 .. S => Seq (K) = I)));
pragma Loop_Invariant
(for all K in 1 .. S =>
(if Seq (K) >= 1 and then Seq (K) <= Max_Paragraph_CPs
then W1_Done (Seq (K))));
pragma Loop_Invariant
(for all I in 1 .. Max_Paragraph_CPs =>
(if not W1_Done (I)
then Types (I) = Types_Orig (I)));
pragma Loop_Invariant (Seq_Len <= Max_Paragraph_CPs);
pragma Loop_Invariant
(Prev = Ghost_W1_Prev (Types_G, Seq_G, S + 1, SOS));
pragma Loop_Invariant
(for all K in 1 .. S =>
(if Seq (K) >= 1
and then Seq (K) <= Max_Paragraph_CPs
then Types (Seq (K)) =
W1_Resolved (Types_G (Seq (K)),
Ghost_W1_Prev
(Types_G, Seq_G, K, SOS),
K = 1)));
end loop;
end Apply_W1;
procedure Apply_W2
with Global => (Input => (Seq, Seq_Len, SOS),
In_Out => Types),
Pre => Seq_Len >= 1
and then Seq_Len <= Max_Paragraph_CPs
and then Seq_Unique,
Post => (for all S in 1 .. Seq_Len =>
(if Seq (S) >= 1
and then Seq (S) <= Max_Paragraph_CPs
and then W2_Applies (Types'Old (Seq (S)),
Ghost_W2_Prev_Strong
(To_GBC (Types'Old),
To_Ghost_Seq (Seq),
S, SOS))
then Types (Seq (S)) = BC_AN))
-- Frame: positions not in the sequence are unchanged
and then
(for all I in 1 .. Max_Paragraph_CPs =>
(if (for all S in 1 .. Seq_Len => Seq (S) /= I)
then Types (I) = Types'Old (I)))
is
Prev_Strong : BC_Value := SOS;
Idx : Natural;
Types_Orig : constant BC_Array := Types with Ghost;
Types_G : constant Ghost_BC_Array := To_GBC (Types) with Ghost;
Seq_G : constant Ghost_Seq_Array := To_Ghost_Seq (Seq) with Ghost;
W2_Done : array (1 .. Max_Paragraph_CPs) of Boolean :=
[others => False] with Ghost;
begin
for S in 1 .. Seq_Len loop
Idx := Seq (S);
if Idx >= 1 and Idx <= Max_Paragraph_CPs then
-- Uniqueness: no earlier K < S has Seq(K) = Idx.
pragma Assert
(for all K in 1 .. S - 1 => Seq (K) /= Seq (S));
pragma Assert (not W2_Done (Idx));
-- W2 only changes EN→AN. Neither is strong.
-- So the ghost Prev_Strong (which reads original types)
-- matches the runtime Prev_Strong (which reads current).
-- Key: W2 never modifies a strong type.
pragma Assert (Types_G (Idx) = Types_Orig (Idx));
pragma Assert
(Prev_Strong =
Ghost_W2_Prev_Strong (Types_G, Seq_G, S, SOS));
if W2_Applies (Types (Idx), Prev_Strong) then
Types (Idx) := BC_AN;
end if;
-- After potential W2 change: Types(Idx) is either
-- unchanged (not EN or Prev_Strong /= AL) or BC_AN.
-- In either case, if Is_Strong, it equals the original.
if Types (Idx) = BC_R or Types (Idx) = BC_L
or Types (Idx) = BC_AL
then
-- Strong type: W2 didn't change it (W2 only touches EN)
pragma Assert (Types (Idx) = Types_Orig (Idx));
pragma Assert (Is_Strong (Types_G (Idx)));
Prev_Strong := Types (Idx);
-- Now Prev_Strong = Types(Idx) = Types_G(Idx)
-- Ghost unfolds: Ghost_W2_Prev_Strong(S+1) =
-- Types_G(Seq(S)) when Is_Strong
pragma Assert
(Prev_Strong = Types_G (Idx));
else
-- Not strong: Prev_Strong unchanged.
-- Types(Idx) is either Types_Orig(Idx) or BC_AN.
-- If it was Types_Orig, and Types_Orig was strong,
-- then Types(Idx) would be strong — contradiction.
-- If it was BC_AN, then not strong, and Types_Orig
-- was EN (which W2 changed), also not strong.
-- Either way, Types_G(Idx) is not strong.
null;
end if;
W2_Done (Idx) := True;
end if;
-- Frame tracking: Done ↔ sequence membership
pragma Loop_Invariant
(for all I in 1 .. Max_Paragraph_CPs =>
(if W2_Done (I) then
(for some K in 1 .. S => Seq (K) = I)));
pragma Loop_Invariant
(for all K in 1 .. S =>
(if Seq (K) >= 1 and then Seq (K) <= Max_Paragraph_CPs
then W2_Done (Seq (K))));
pragma Loop_Invariant
(for all I in 1 .. Max_Paragraph_CPs =>
(if not W2_Done (I)
then Types (I) = Types_Orig (I)));
-- Invariant 1: Every position is either original or BC_AN.
pragma Loop_Invariant
(for all I in 1 .. Max_Paragraph_CPs =>
Types (I) = Types_Orig (I)
or else Types (I) = BC_AN);
-- Invariant 1b: Strong types are never modified by W2.
-- (W2 only changes EN→AN; EN is not strong.)
pragma Loop_Invariant
(for all I in 1 .. Max_Paragraph_CPs =>
(if Is_Strong (Types_Orig (I))
then Types (I) = Types_Orig (I)));
-- Invariant 2: Prev_Strong tracks the ghost function.
pragma Loop_Invariant (Seq_Len <= Max_Paragraph_CPs);
pragma Loop_Invariant
(Prev_Strong =
Ghost_W2_Prev_Strong (Types_G, Seq_G, S + 1, SOS));
-- Invariant 3: All processed positions where W2 applied = BC_AN.
pragma Loop_Invariant
(for all K in 1 .. S =>
(if Seq (K) >= 1
and then Seq (K) <= Max_Paragraph_CPs
and then W2_Applies (Types_G (Seq (K)),
Ghost_W2_Prev_Strong
(Types_G, Seq_G, K, SOS))
then Types (Seq (K)) = BC_AN));
end loop;
end Apply_W2;
procedure Apply_W3
with Global => (Input => (Seq, Seq_Len),
In_Out => Types),
Pre => Seq_Len >= 1
and then Seq_Len <= Max_Paragraph_CPs
and then Seq_Unique,
Post => (for all S in 1 .. Seq_Len =>
(if Seq (S) >= 1 and then Seq (S) <= Max_Paragraph_CPs
then Types (Seq (S)) =
W3_Resolved (Types'Old (Seq (S)))))
-- Frame: positions not in the sequence are unchanged
and then
(for all I in 1 .. Max_Paragraph_CPs =>
(if (for all S in 1 .. Seq_Len => Seq (S) /= I)
then Types (I) = Types'Old (I)))
is
Idx : Natural;
Types_Orig : constant BC_Array := Types with Ghost;
W3_Done : array (1 .. Max_Paragraph_CPs) of Boolean :=
[others => False] with Ghost;
begin
for S in 1 .. Seq_Len loop
Idx := Seq (S);
if Idx >= 1 and Idx <= Max_Paragraph_CPs then
pragma Assert
(for all K in 1 .. S - 1 => Seq (K) /= Seq (S));
pragma Assert (not W3_Done (Idx));
Types (Idx) := W3_Resolved (Types (Idx));
W3_Done (Idx) := True;
end if;
-- Frame tracking: Done ↔ sequence membership
pragma Loop_Invariant
(for all I in 1 .. Max_Paragraph_CPs =>
(if W3_Done (I) then
(for some K in 1 .. S => Seq (K) = I)));
pragma Loop_Invariant
(for all K in 1 .. S =>
(if Seq (K) >= 1 and then Seq (K) <= Max_Paragraph_CPs
then W3_Done (Seq (K))));
pragma Loop_Invariant
(for all I in 1 .. Max_Paragraph_CPs =>
(if not W3_Done (I)
then Types (I) = Types_Orig (I)));
-- Every position in Types is either:
-- (a) untouched: Types(I) = Types_Orig(I), or
-- (b) resolved: Types(I) = W3_Resolved(Types_Orig(I))
pragma Loop_Invariant
(for all I in 1 .. Max_Paragraph_CPs =>
Types (I) = Types_Orig (I)
or else Types (I) = W3_Resolved (Types_Orig (I)));
pragma Loop_Invariant
(for all K in 1 .. S =>
(if Seq (K) >= 1 and then Seq (K) <= Max_Paragraph_CPs
then Types (Seq (K)) =
W3_Resolved (Types_Orig (Seq (K)))));
end loop;
end Apply_W3;
procedure Apply_W4
with Global => (Input => (Seq, Seq_Len),
In_Out => Types),
Pre => Seq_Len >= 1
and then Seq_Len <= Max_Paragraph_CPs
and then Seq_Unique,
Post => (for all S in 1 .. Seq_Len =>
(if Seq (S) >= 1
and then Seq (S) <= Max_Paragraph_CPs
then Types (Seq (S)) =
Ghost_W4_Result
(To_GBC (Types'Old),
To_Ghost_Seq (Seq),
S, Seq_Len)))
-- Frame: positions not in the sequence are unchanged
and then
(for all I in 1 .. Max_Paragraph_CPs =>
(if (for all S in 1 .. Seq_Len => Seq (S) /= I)
then Types (I) = Types'Old (I)))
is
Prev_T, Cur_T, Next_T : BC_Value;
Idx : Natural;
Types_Orig : constant BC_Array := Types with Ghost;
Types_G : constant Ghost_BC_Array := To_GBC (Types) with Ghost;
Seq_G : constant Ghost_Seq_Array := To_Ghost_Seq (Seq) with Ghost;
W4_Done : array (1 .. Max_Paragraph_CPs) of Boolean :=
[others => False] with Ghost;
begin
if Seq_Len < 3 then return; end if;
for S in 2 .. Seq_Len - 1 loop
Idx := Seq (S);
if (Idx >= 1 and Idx <= Max_Paragraph_CPs)
and then (Seq (S - 1) >= 1
and then Seq (S - 1) <= Max_Paragraph_CPs)
and then (Seq (S + 1) >= 1
and then Seq (S + 1) <= Max_Paragraph_CPs)
then
-- Uniqueness: position S not yet visited.
pragma Assert
(for all K in 1 .. S - 1 => Seq (K) /= Seq (S));
pragma Assert (not W4_Done (Idx));
pragma Assert (Types (Idx) = Types_G (Idx));
Prev_T := Types (Seq (S - 1));
Cur_T := Types (Idx);
Next_T := Types (Seq (S + 1));
-- Prev: either S-1 = 1 (original) or S-1 in 2..S-1 (from invariant).
pragma Assert
(Prev_T = Ghost_W4_Result
(Types_G, Seq_G, S - 1, Seq_Len));
-- Next is not yet processed (S+1 > S), so equals original.
pragma Assert
(for all K in 2 .. S => Seq (K) /= Seq (S + 1));
pragma Assert (not W4_Done (Seq (S + 1)));
pragma Assert (Next_T = Types_G (Seq (S + 1)));
Types (Idx) := W4_Resolved (Cur_T, Prev_T, Next_T);
W4_Done (Idx) := True;
end if;
pragma Loop_Invariant
(for all I in 1 .. Max_Paragraph_CPs =>
(if W4_Done (I) then
(for some K in 2 .. S => Seq (K) = I)));
pragma Loop_Invariant
(for all K in 2 .. S =>
(if Seq (K) >= 1 and then Seq (K) <= Max_Paragraph_CPs
then W4_Done (Seq (K))));
pragma Loop_Invariant
(for all I in 1 .. Max_Paragraph_CPs =>
(if not W4_Done (I)
then Types (I) = Types_Orig (I)));
pragma Loop_Invariant (Seq_Len <= Max_Paragraph_CPs);
-- Main result: all processed positions match ghost W4:
pragma Loop_Invariant
(for all K in 2 .. S =>
(if Seq (K) >= 1
and then Seq (K) <= Max_Paragraph_CPs
then Types (Seq (K)) =
Ghost_W4_Result
(Types_G, Seq_G, K, Seq_Len)));
-- Unprocessed positions still match ghost W4:
-- (Ghost_W4_Result returns Types_G for S < 2 or S > Len-1)
pragma Loop_Invariant
(if Seq (1) >= 1 and then Seq (1) <= Max_Paragraph_CPs
then Types (Seq (1)) =
Ghost_W4_Result
(Types_G, Seq_G, 1, Seq_Len));
end loop;
end Apply_W4;
procedure Apply_W5
with Global => (Input => (Seq, Seq_Len),
In_Out => Types),
Pre => Seq_Len >= 1
and then Seq_Len <= Max_Paragraph_CPs
and then Seq_Unique,
Post => (for all S in 1 .. Seq_Len =>
(if Seq (S) >= 1
and then Seq (S) <= Max_Paragraph_CPs
then Types (Seq (S)) =
Ghost_W5_Result
(To_GBC (Types'Old),
To_Ghost_Seq (Seq),
S, Seq_Len)))
-- Frame: positions not in the sequence are unchanged
and then
(for all I in 1 .. Max_Paragraph_CPs =>
(if (for all S in 1 .. Seq_Len => Seq (S) /= I)
then Types (I) = Types'Old (I)))
is
Idx : Natural;
Has_Adjacent_EN : Boolean;
Types_Orig : constant BC_Array := Types with Ghost;
Types_G : constant Ghost_BC_Array := To_GBC (Types) with Ghost;
Seq_G : constant Ghost_Seq_Array := To_Ghost_Seq (Seq) with Ghost;
-- Track which positions have been processed (forward pass)
W5_Fwd_Done : array (1 .. Max_Paragraph_CPs) of Boolean :=
[others => False] with Ghost;
-- Ghost lemma: Ghost_W5_Bwd_Has_EN = Ghost_W5_Has_EN_Right
-- when the position is ET without left-EN.
--
-- Proof: When orig(S) = ET without left-EN, all rightward ETs
-- in the same chain also have no left-EN, so their Fwd_Result
-- is also ET. Both Bwd_Has_EN and Has_EN_Right recurse through
-- the same chain, reaching EN or non-ET at the same point.
procedure Lemma_Bwd_Equals_Right
(S : Natural)
with Ghost,
Pre => S >= 1
and then S <= Seq_Len
and then Seq_Len <= Max_Paragraph_CPs
and then (for all I in 1 .. Seq_Len =>
Seq_G (I) = Seq (I))
and then Seq (S) >= 1
and then Seq (S) <= Max_Paragraph_CPs
and then Types_G (Seq_G (S)) = BC_ET
and then not Ghost_W5_Has_EN_Left
(Types_G, Seq_G, S),
Subprogram_Variant => (Decreases => Seq_Len - S),
Post => Ghost_W5_Bwd_Has_EN
(Types_G, Seq_G, S, Seq_Len) =
Ghost_W5_Has_EN_Right
(Types_G, Seq_G, S, Seq_Len);
procedure Lemma_Bwd_Equals_Right
(S : Natural)
is
begin
-- Fwd_Result(S) = ET (because orig=ET and no left-EN)
pragma Assert
(Ghost_W5_Fwd_Result (Types_G, Seq_G, S) = BC_ET);
if S >= Seq_Len then
-- S+1 > Len: both functions return False at S+1.
-- One-step: both reduce at S to their S+1 value = False.
null;
else
-- S < Seq_Len, so S+1 in 1..Seq_Len.
-- From precondition: Seq_G(I) = Seq(I) for I in 1..Seq_Len.
pragma Assert (Seq_G (S + 1) = Seq (S + 1));
if Seq_G (S + 1) < 1 or else Seq_G (S + 1) > Max_Paragraph_CPs
then
-- Seq out of range at S+1: both return False.
null;
elsif Types_G (Seq_G (S + 1)) = BC_EN then
-- S+1 is orig EN.
-- Fwd_Result(S+1) = EN (orig EN stays EN).
pragma Assert
(Ghost_W5_Fwd_Result (Types_G, Seq_G, S + 1) = BC_EN);
-- Bwd_Has_EN(S+1) = True, Has_EN_Right(S+1) = True.
null;
elsif Types_G (Seq_G (S + 1)) = BC_ET then
-- S+1 is orig ET. Has_EN_Left at S scans left through ET
-- chain; at S+1 it scans through S which is also ET, so
-- if S had no left-EN, neither does S+1.
pragma Assert
(not Ghost_W5_Has_EN_Left (Types_G, Seq_G, S + 1));
-- Inductive step.
Lemma_Bwd_Equals_Right (S + 1);
else
-- S+1 is other (not ET, not EN): both return False.
null;
end if;
end if;
end Lemma_Bwd_Equals_Right;
begin
----------------------------------------------------------------
-- Forward pass: ET → EN if preceded by EN through ET chain
----------------------------------------------------------------
Has_Adjacent_EN := False;
for S in 1 .. Seq_Len loop
Idx := Seq (S);
if Idx >= 1 and Idx <= Max_Paragraph_CPs then
-- Key: this position hasn't been written by any prior
-- iteration (Seq_Unique ensures all prior Seq positions
-- differ from Seq(S)), so Types(Idx) = Types_Orig(Idx).
pragma Assert (not W5_Fwd_Done (Idx));
pragma Assert (Types (Idx) = Types_Orig (Idx));
-- Connect runtime Types to ghost original:
pragma Assert (Types (Idx) = Types_G (Seq_G (S)));
-- Ghost_W5_Has_EN_Left one-step unfolding:
-- Since Types_G(Seq_G(S)) is known, the ghost function
-- evaluates based on this value and the prior Has_Adjacent_EN.
if Types (Idx) = BC_EN then
Has_Adjacent_EN := True;
-- Ghost: Types_G(Seq_G(S)) = BC_EN → True
pragma Assert
(Ghost_W5_Has_EN_Left (Types_G, Seq_G, S) = True);
elsif Types (Idx) = BC_ET then
-- Ghost: Types_G(Seq_G(S)) = BC_ET → recurse to S-1
-- Has_Adjacent_EN = Ghost_W5_Has_EN_Left at S-1
-- (from loop invariant or initial value)
pragma Assert
(Ghost_W5_Has_EN_Left (Types_G, Seq_G, S) =
(if S >= 2
then Ghost_W5_Has_EN_Left (Types_G, Seq_G, S - 1)
else False));
if Has_Adjacent_EN then
Types (Idx) := BC_EN;
end if;
else
Has_Adjacent_EN := False;
-- Ghost: not EN, not ET → False
pragma Assert
(Ghost_W5_Has_EN_Left (Types_G, Seq_G, S) = False);
end if;
W5_Fwd_Done (Idx) := True;
end if;
-- Link Has_Adjacent_EN to ghost function
pragma Assert
(if Seq (S) >= 1 and then Seq (S) <= Max_Paragraph_CPs
then Has_Adjacent_EN =
Ghost_W5_Has_EN_Left (Types_G, Seq_G, S));
-- Current position matches forward ghost result
pragma Assert
(if Seq (S) >= 1 and then Seq (S) <= Max_Paragraph_CPs
then Types (Seq (S)) =
Ghost_W5_Fwd_Result (Types_G, Seq_G, S));
-- W5_Fwd_Done tracks exactly which indices have been processed
pragma Loop_Invariant
(for all K in 1 .. S =>
(if Seq (K) >= 1 and then Seq (K) <= Max_Paragraph_CPs
then W5_Fwd_Done (Seq (K))));
pragma Loop_Invariant
(for all I in 1 .. Max_Paragraph_CPs =>
(if W5_Fwd_Done (I) then
(for some K in 1 .. S => Seq (K) = I)));
pragma Loop_Invariant
(for all K in S + 1 .. Seq_Len =>
(if Seq (K) >= 1 and then Seq (K) <= Max_Paragraph_CPs
then not W5_Fwd_Done (Seq (K))));
-- Unvisited paragraph positions retain original type
pragma Loop_Invariant
(for all I in 1 .. Max_Paragraph_CPs =>
(if not W5_Fwd_Done (I) then Types (I) = Types_Orig (I)));
pragma Loop_Invariant (Seq_Len <= Max_Paragraph_CPs);
-- All processed positions match forward ghost
pragma Loop_Invariant
(for all K in 1 .. S =>
(if Seq (K) >= 1 and then Seq (K) <= Max_Paragraph_CPs
then Types (Seq (K)) =
Ghost_W5_Fwd_Result (Types_G, Seq_G, K)));
-- Has_Adjacent_EN corresponds to left-scan
pragma Loop_Invariant
(if Seq (S) >= 1 and then Seq (S) <= Max_Paragraph_CPs
then Has_Adjacent_EN =
Ghost_W5_Has_EN_Left (Types_G, Seq_G, S));
end loop;
-- After forward pass: all positions match forward ghost result
pragma Assert
(for all S in 1 .. Seq_Len =>
(if Seq (S) >= 1 and then Seq (S) <= Max_Paragraph_CPs
then Types (Seq (S)) =
Ghost_W5_Fwd_Result (Types_G, Seq_G, S)));
----------------------------------------------------------------
-- Backward pass: ET → EN if followed by EN through ET chain
----------------------------------------------------------------
Has_Adjacent_EN := False;
for S in reverse 1 .. Seq_Len loop
Idx := Seq (S);
if Idx >= 1 and Idx <= Max_Paragraph_CPs then
-- Pre-backward value = forward result
pragma Assert
(Types (Idx) =
Ghost_W5_Fwd_Result (Types_G, Seq_G, S));
if Types (Idx) = BC_EN then
Has_Adjacent_EN := True;
-- Ghost_W5_Bwd_Has_EN: Fwd_Result = EN → True
pragma Assert
(Ghost_W5_Bwd_Has_EN
(Types_G, Seq_G, S, Seq_Len) = True);
-- EN in post-forward means either:
-- (a) original EN → Ghost_W5_Result = EN
-- (b) original ET with left-EN → Ghost_W5_Result = EN
pragma Assert
(Ghost_W5_Result (Types_G, Seq_G, S, Seq_Len) = BC_EN);
elsif Types (Idx) = BC_ET then
-- ET in post-forward means original ET without left-EN.
pragma Assert (Types_G (Seq_G (S)) = BC_ET);
pragma Assert
(not Ghost_W5_Has_EN_Left (Types_G, Seq_G, S));
-- Ghost_W5_Bwd_Has_EN one-step: Fwd_Result=ET → recurse S+1
pragma Assert
(Ghost_W5_Bwd_Has_EN (Types_G, Seq_G, S, Seq_Len) =
Ghost_W5_Bwd_Has_EN
(Types_G, Seq_G, S + 1, Seq_Len));
-- Lemma: Bwd_Has_EN = Has_EN_Right for this position
pragma Assert
(for all I in 1 .. Seq_Len =>
Seq_G (I) = Seq (I));
Lemma_Bwd_Equals_Right (S);
-- Now connect: Has_Adjacent_EN = Bwd_Has_EN(S+1)
-- = Bwd_Has_EN(S) [one-step] = Has_EN_Right(S) [lemma]
if Has_Adjacent_EN then
Types (Idx) := BC_EN;
pragma Assert
(Ghost_W5_Has_EN_Right
(Types_G, Seq_G, S, Seq_Len));
pragma Assert
(Ghost_W5_Result (Types_G, Seq_G, S, Seq_Len)
= BC_EN);
else
pragma Assert
(not Ghost_W5_Has_EN_Right
(Types_G, Seq_G, S, Seq_Len));
pragma Assert
(Ghost_W5_Result (Types_G, Seq_G, S, Seq_Len)
= BC_ET);
end if;
else
Has_Adjacent_EN := False;
-- Fwd_Result is other → Bwd_Has_EN = False
pragma Assert
(Ghost_W5_Bwd_Has_EN
(Types_G, Seq_G, S, Seq_Len) = False);
-- Not ET, not EN → Ghost_W5_Result = original = current
pragma Assert
(Types_G (Seq_G (S)) /= BC_ET);
pragma Assert
(Ghost_W5_Result (Types_G, Seq_G, S, Seq_Len)
= Types_G (Seq_G (S)));
end if;
end if;
-- Current position matches final ghost result
pragma Assert
(if Seq (S) >= 1 and then Seq (S) <= Max_Paragraph_CPs
then Types (Seq (S)) =
Ghost_W5_Result (Types_G, Seq_G, S, Seq_Len));
-- All positions S..Seq_Len match final ghost result
pragma Loop_Invariant
(for all K in S .. Seq_Len =>
(if Seq (K) >= 1 and then Seq (K) <= Max_Paragraph_CPs
then Types (Seq (K)) =
Ghost_W5_Result (Types_G, Seq_G, K, Seq_Len)));
-- Positions 1..S-1 still match forward result (untouched)
pragma Loop_Invariant
(for all K in 1 .. S - 1 =>
(if Seq (K) >= 1 and then Seq (K) <= Max_Paragraph_CPs
then Types (Seq (K)) =
Ghost_W5_Fwd_Result (Types_G, Seq_G, K)));
-- Frame: non-sequence positions are unchanged
pragma Loop_Invariant
(for all I in 1 .. Max_Paragraph_CPs =>
(if not W5_Fwd_Done (I)
then Types (I) = Types_Orig (I)));
pragma Loop_Invariant (Seq_Len <= Max_Paragraph_CPs);
-- Track Has_Adjacent_EN correspondence with ghost
pragma Loop_Invariant
(if Seq (S) >= 1 and then Seq (S) <= Max_Paragraph_CPs
then Has_Adjacent_EN =
Ghost_W5_Bwd_Has_EN
(Types_G, Seq_G, S, Seq_Len));
end loop;
end Apply_W5;
procedure Apply_W6
with Global => (Input => (Seq, Seq_Len),
In_Out => Types),
Pre => Seq_Len >= 1
and then Seq_Len <= Max_Paragraph_CPs
and then Seq_Unique,
Post => (for all S in 1 .. Seq_Len =>
(if Seq (S) >= 1 and then Seq (S) <= Max_Paragraph_CPs
then Types (Seq (S)) =
W6_Resolved (Types'Old (Seq (S)))))
-- Frame: positions not in the sequence are unchanged
and then
(for all I in 1 .. Max_Paragraph_CPs =>
(if (for all S in 1 .. Seq_Len => Seq (S) /= I)
then Types (I) = Types'Old (I)))
is
Idx : Natural;
Types_Orig : constant BC_Array := Types with Ghost;
W6_Done : array (1 .. Max_Paragraph_CPs) of Boolean :=
[others => False] with Ghost;
begin
for S in 1 .. Seq_Len loop
Idx := Seq (S);
if Idx >= 1 and Idx <= Max_Paragraph_CPs then
pragma Assert
(for all K in 1 .. S - 1 => Seq (K) /= Seq (S));
pragma Assert (not W6_Done (Idx));
Types (Idx) := W6_Resolved (Types (Idx));
W6_Done (Idx) := True;
end if;
-- Frame tracking: Done ↔ sequence membership
pragma Loop_Invariant
(for all I in 1 .. Max_Paragraph_CPs =>
(if W6_Done (I) then
(for some K in 1 .. S => Seq (K) = I)));
pragma Loop_Invariant
(for all K in 1 .. S =>
(if Seq (K) >= 1 and then Seq (K) <= Max_Paragraph_CPs
then W6_Done (Seq (K))));
pragma Loop_Invariant
(for all I in 1 .. Max_Paragraph_CPs =>
(if not W6_Done (I)
then Types (I) = Types_Orig (I)));
pragma Loop_Invariant
(for all I in 1 .. Max_Paragraph_CPs =>
Types (I) = Types_Orig (I)
or else Types (I) = W6_Resolved (Types_Orig (I)));
pragma Loop_Invariant
(for all K in 1 .. S =>
(if Seq (K) >= 1 and then Seq (K) <= Max_Paragraph_CPs
then Types (Seq (K)) =
W6_Resolved (Types_Orig (Seq (K)))));
end loop;
end Apply_W6;
procedure Apply_W7
with Global => (Input => (Seq, Seq_Len, SOS),
In_Out => Types),
Pre => Seq_Len >= 1
and then Seq_Len <= Max_Paragraph_CPs
and then Seq_Unique,
Post => (for all S in 1 .. Seq_Len =>
(if Seq (S) >= 1
and then Seq (S) <= Max_Paragraph_CPs
and then W7_Applies (Types'Old (Seq (S)),
Ghost_W7_Prev_Strong
(To_GBC (Types'Old),
To_Ghost_Seq (Seq),
S, SOS))
then Types (Seq (S)) = BC_L))
-- Frame: positions not in the sequence are unchanged
and then
(for all I in 1 .. Max_Paragraph_CPs =>
(if (for all S in 1 .. Seq_Len => Seq (S) /= I)
then Types (I) = Types'Old (I)))
is
Prev_Strong : BC_Value := SOS;
Idx : Natural;
Types_Orig : constant BC_Array := Types with Ghost;
Types_G : constant Ghost_BC_Array := To_GBC (Types) with Ghost;
Seq_G : constant Ghost_Seq_Array := To_Ghost_Seq (Seq) with Ghost;
-- Ghost: track which positions W7 has already modified.
-- Positions not yet visited still equal their original type.
W7_Done : array (1 .. Max_Paragraph_CPs) of Boolean :=
[others => False] with Ghost;
begin
for S in 1 .. Seq_Len loop
Idx := Seq (S);
if Idx >= 1 and Idx <= Max_Paragraph_CPs then
pragma Assert (Seq_G (S) = Seq (S));
-- Uniqueness: for all K < S, Seq(K) /= Seq(S) = Idx.
-- (from Seq_Unique: for all A in 1..Seq_Len,
-- B in A+1..Seq_Len => Seq(A) /= Seq(B))
pragma Assert
(for all K in 1 .. S - 1 =>
Seq (K) /= Seq (S));
-- Combined with W7_Done invariant: W7_Done(I) implies
-- some K <= S-1 has Seq(K) = I. Since no such K has
-- Seq(K) = Idx, W7_Done(Idx) must be False.
pragma Assert (not W7_Done (Idx));
-- Therefore Types(Idx) = original.
pragma Assert (Types (Idx) = Types_G (Idx));
declare
PS_Before : constant BC_Value :=
Prev_Strong with Ghost;
begin
if W7_Applies (Types (Idx), Prev_Strong) then
Types (Idx) := BC_L;
end if;
if Types (Idx) = BC_L or Types (Idx) = BC_R then
Prev_Strong := Types (Idx);
end if;
-- Runtime = W7_PS_Update(W7_Effective_Type(orig, PS_Before), PS_Before)
pragma Assert
(Prev_Strong =
W7_PS_Update
(W7_Effective_Type (Types_G (Idx), PS_Before),
PS_Before));
-- Ghost(S+1) unfolds to same expression:
pragma Assert
(Ghost_W7_Prev_Strong
(Types_G, Seq_G, S + 1, SOS) =
W7_PS_Update
(W7_Effective_Type (Types_G (Idx), PS_Before),
PS_Before));
-- Therefore:
pragma Assert
(Prev_Strong =
Ghost_W7_Prev_Strong
(Types_G, Seq_G, S + 1, SOS));
end;
W7_Done (Idx) := True;
end if;
-- W7_Done(I) = True iff I was a Seq(K) for some K <= S.
-- This is needed to prove not W7_Done(Idx) for future S.
pragma Loop_Invariant
(for all I in 1 .. Max_Paragraph_CPs =>
(if W7_Done (I) then
(for some K in 1 .. S =>
Seq (K) = I)));
pragma Loop_Invariant
(for all K in 1 .. S =>
(if Seq (K) >= 1 and then Seq (K) <= Max_Paragraph_CPs
then W7_Done (Seq (K))));
-- Positions not marked done are still at their original value.
pragma Loop_Invariant
(for all I in 1 .. Max_Paragraph_CPs =>
(if not W7_Done (I) then Types (I) = Types_Orig (I)));
-- Positions that are done are either original or BC_L.
pragma Loop_Invariant
(for all I in 1 .. Max_Paragraph_CPs =>
Types (I) = Types_Orig (I) or else Types (I) = BC_L);
pragma Loop_Invariant (Seq_Len <= Max_Paragraph_CPs);
pragma Loop_Invariant
(Prev_Strong =
Ghost_W7_Prev_Strong (Types_G, Seq_G, S + 1, SOS));
pragma Loop_Invariant
(for all K in 1 .. S =>
(if Seq (K) >= 1
and then Seq (K) <= Max_Paragraph_CPs
and then W7_Applies (Types_G (Seq (K)),
Ghost_W7_Prev_Strong
(Types_G, Seq_G, K, SOS))
then Types (Seq (K)) = BC_L));
end loop;
end Apply_W7;
-- ---------------------------------------------------------------
-- N0: Bracket pair resolution (BD16)
-- ---------------------------------------------------------------
procedure Apply_N0
with Global => (Input => (Seq, Seq_Len, CPs, Orig_Types,
Embed_Levels, PL, SOS,
Bracket_Close_Table,
Is_Open_Bracket,
Is_Close_Bracket),
In_Out => Types),
Pre => (Seq_Len >= 1 and Seq_Len <= Max_Paragraph_CPs)
and then PL <= 1
and then Seq_Unique
is
-- BD16 bracket stack
type Bracket_Stack_Entry is record
Open_Pos : Natural; -- sequence index (1..Seq_Len)
Open_CP : Codepoint;
end record;
type Bracket_Stack_Array is
array (1 .. Max_Bracket_Stack) of Bracket_Stack_Entry;
Br_Stack : Bracket_Stack_Array :=
[others => (Open_Pos => 0, Open_CP => 0)];
Br_Top : Natural := 0;
-- Collected bracket pairs (sorted by opening position)
type Pair_Record is record
Open_Pos : Natural;
Close_Pos : Natural;
end record;
type Pair_Array is array (1 .. Max_Bracket_Stack) of Pair_Record;
Pairs : Pair_Array := [others => (Open_Pos => 0, Close_Pos => 0)];
Num_Pairs : Natural := 0;
-- BD16 canonical equivalence for bracket matching.
-- Only two bracket pairs have canonical decompositions:
-- U+2329 → U+3008 and U+232A → U+3009.
function Canonical_Bracket (CP : Codepoint) return Codepoint
is (case CP is
when 16#2329# => 16#3008#,
when 16#232A# => 16#3009#,
when others => CP);
Idx : Natural;
CP_Val : Codepoint;
Embed_Dir : BC_Value;
Run_Level : Embedding_Level;
-- N0 helper: scan Seq(From_S..To_S) for strong types.
-- Sets FE = True iff a strong type matching Ed found.
-- Sets FO = True iff a strong type opposite to Ed found.
procedure N0_Scan_Inner
(From_S : Natural;
To_S : Natural;
Ed : BC_Value;
FE : out Boolean;
FO : out Boolean)
with Global => (Input => (Types, Seq),
Proof_In => Seq_Len),
Pre => From_S >= 1
and then To_S <= Max_Paragraph_CPs
and then To_S < Seq_Len
and then Seq_Len >= 1
and then Seq_Len <= Max_Paragraph_CPs
and then Seq_Unique,
Post => FE = Ghost_N0_Has_Embed_Dir
(To_GBC (Types), To_Ghost_Seq (Seq),
From_S, To_S, Ed)
and then
FO = Ghost_N0_Has_Opposite
(To_GBC (Types), To_Ghost_Seq (Seq),
From_S, To_S, Ed)
is
S_Idx : Natural;
Types_G : constant Ghost_BC_Array :=
To_GBC (Types) with Ghost;
Seq_G : constant Ghost_Seq_Array :=
To_Ghost_Seq (Seq) with Ghost;
Check_E : Boolean;
Check_O : Boolean;
begin
FE := False;
FO := False;
for S in From_S .. To_S loop
-- All S in From_S..To_S are within 1..Seq_Len (from Pre)
-- Seq_Unique ensures Seq(S) >= 1 and Seq(S) <= Max_Paragraph_CPs
S_Idx := Seq (S);
-- Bridge: ghost arrays match runtime
pragma Assert (Seq_G (S) = S_Idx);
pragma Assert
(if S_Idx >= 1 and then S_Idx <= Max_Paragraph_CPs
then Types_G (S_Idx) = Types (S_Idx));
-- Compute the exact checks that the ghost functions test
Check_E :=
S_Idx >= 1
and then S_Idx <= Max_Paragraph_CPs
and then Neutral_Type (Types (S_Idx)) = Ed;
Check_O :=
S_Idx >= 1
and then S_Idx <= Max_Paragraph_CPs
and then Neutral_Type (Types (S_Idx)) /= BC_ON
and then Neutral_Type (Types (S_Idx)) /= Ed;
-- Update accumulators via explicit OR
FE := FE or Check_E;
FO := FO or Check_O;
-- One-step unfolding of the ghost recursive definition
pragma Assert
(Ghost_N0_Has_Embed_Dir (Types_G, Seq_G, From_S, S, Ed) =
(Check_E
or else Ghost_N0_Has_Embed_Dir
(Types_G, Seq_G, From_S, S - 1, Ed)));
pragma Assert
(Ghost_N0_Has_Opposite (Types_G, Seq_G, From_S, S, Ed) =
(Check_O
or else Ghost_N0_Has_Opposite
(Types_G, Seq_G, From_S, S - 1, Ed)));
pragma Loop_Invariant
(FE = Ghost_N0_Has_Embed_Dir
(Types_G, Seq_G, From_S, S, Ed));
pragma Loop_Invariant
(FO = Ghost_N0_Has_Opposite
(Types_G, Seq_G, From_S, S, Ed));
end loop;
end N0_Scan_Inner;
-- N0 helper: backward scan from Open_S-1 for preceding strong.
-- Returns the Neutral_Type of the first strong (L or R), or SOS_V.
function N0_Find_Context
(Open_S : Natural;
SOS_V : BC_Value) return BC_Value
with Global => (Input => (Types, Seq),
Proof_In => Seq_Len),
Pre => Open_S >= 1
and then Open_S <= Seq_Len
and then Seq_Len >= 1
and then Seq_Len <= Max_Paragraph_CPs
and then Seq_Unique,
Post => N0_Find_Context'Result =
Ghost_N0_Context_Dir
(To_GBC (Types), To_Ghost_Seq (Seq),
Open_S, SOS_V)
is
Types_G : constant Ghost_BC_Array :=
To_GBC (Types) with Ghost;
Seq_G : constant Ghost_Seq_Array :=
To_Ghost_Seq (Seq) with Ghost;
S_Idx : Natural;
NT : BC_Value;
Is_Strong : Boolean;
begin
for S in reverse 1 .. Open_S - 1 loop
-- S is in 1..Seq_Len-1 since Open_S <= Seq_Len
S_Idx := Seq (S);
-- Bridge: ghost arrays match runtime
pragma Assert (Seq_G (S) = S_Idx);
pragma Assert
(if S_Idx >= 1 and then S_Idx <= Max_Paragraph_CPs
then Types_G (S_Idx) = Types (S_Idx));
-- Is this position a strong type?
NT := BC_ON;
Is_Strong := False;
if S_Idx >= 1 and S_Idx <= Max_Paragraph_CPs then
NT := Neutral_Type (Types (S_Idx));
if NT = BC_L or NT = BC_R then
Is_Strong := True;
end if;
end if;
-- Unfold: Context_Dir(S+1) checks Seq_G(S).
-- If strong at S → Context_Dir(S+1) = that strong type.
-- Otherwise → Context_Dir(S+1) = Context_Dir(S).
pragma Assert
(if Is_Strong
then Ghost_N0_Context_Dir
(Types_G, Seq_G, S + 1, SOS_V) = NT
else Ghost_N0_Context_Dir
(Types_G, Seq_G, S + 1, SOS_V) =
Ghost_N0_Context_Dir
(Types_G, Seq_G, S, SOS_V));
if Is_Strong then
return NT;
end if;
-- Didn't find strong at S, so Context_Dir(S+1) = Context_Dir(S)
-- Combined with the previous invariant, gives:
-- Context_Dir(Open_S) = Context_Dir(S)
pragma Loop_Invariant
(Ghost_N0_Context_Dir (Types_G, Seq_G, Open_S, SOS_V) =
Ghost_N0_Context_Dir (Types_G, Seq_G, S, SOS_V));
end loop;
return SOS_V;
end N0_Find_Context;
begin
-- Determine the embedding direction for this run sequence
-- (use the embedding level of the first member, before I1/I2)
if Seq (1) >= 1 and Seq (1) <= Max_Paragraph_CPs then
Run_Level := Embed_Levels (Seq (1));
else
Run_Level := PL;
end if;
Embed_Dir := Direction_From_Level (Run_Level);
-- Phase 1: Find bracket pairs using BD16 algorithm.
-- Per BD14/BD15, only characters whose current type is ON
-- are considered as opening/closing paired brackets.
for S in 1 .. Seq_Len loop
Idx := Seq (S);
if Idx >= 1 and Idx <= Max_Paragraph_CPs then
CP_Val := CPs (Idx);
-- BD14/BD15: bracket must have current type ON
if Types (Idx) /= BC_ON then
null; -- not a bracket candidate
-- Is this an opening bracket?
elsif Is_Open_Bracket (CP_Val) then
if Br_Top < Max_Bracket_Stack then
Br_Top := Br_Top + 1;
-- Store canonical equivalent for BD16 matching
Br_Stack (Br_Top) :=
(Open_Pos => S,
Open_CP => Canonical_Bracket (CP_Val));
else
-- Stack overflow: stop looking for pairs
exit;
end if;
-- Is this a closing bracket?
elsif Is_Close_Bracket (CP_Val) then
declare
-- Get the opening bracket that this closer maps to,
-- normalized to canonical equivalent for BD16
Paired_Open : constant Codepoint :=
Canonical_Bracket (Bracket_Close_Table (CP_Val));
begin
-- Search stack from top for matching open bracket
for K in reverse 1 .. Br_Top loop
if Br_Stack (K).Open_CP = Paired_Open then
-- Found a match
if Num_Pairs < Max_Bracket_Stack then
Num_Pairs := Num_Pairs + 1;
Pairs (Num_Pairs) :=
(Open_Pos => Br_Stack (K).Open_Pos,
Close_Pos => S);
end if;
-- Pop everything above the matched entry
Br_Top := K - 1;
exit;
end if;
end loop;
end;
end if;
end if;
pragma Loop_Invariant (Br_Top <= Max_Bracket_Stack);
pragma Loop_Invariant (Num_Pairs <= Max_Bracket_Stack);
end loop;
-- Sort pairs by opening position (simple insertion sort)
if Num_Pairs >= 2 then
for I in 2 .. Num_Pairs loop
declare
Key_Open : constant Natural := Pairs (I).Open_Pos;
Key_Close : constant Natural := Pairs (I).Close_Pos;
J : Natural := I - 1;
begin
while J >= 1
and then Pairs (J).Open_Pos > Key_Open
loop
Pairs (J + 1) := Pairs (J);
J := J - 1;
pragma Loop_Invariant (J + 1 >= 1);
pragma Loop_Invariant (J + 1 <= Max_Bracket_Stack);
end loop;
Pairs (J + 1) :=
(Open_Pos => Key_Open, Close_Pos => Key_Close);
end;
pragma Loop_Invariant (Num_Pairs <= Max_Bracket_Stack);
end loop;
end if;
-- Phase 2: Resolve bracket types per N0a/N0b/N0c.
-- Each pair is resolved using the current Types state (which
-- may reflect modifications from earlier pair resolutions).
-- Per-pair ghost assertions verify that the resolved direction
-- matches Ghost_N0_Pair_Dir evaluated against the current state.
for P in 1 .. Num_Pairs loop
declare
O : constant Natural := Pairs (P).Open_Pos;
C : constant Natural := Pairs (P).Close_Pos;
Found_Embed : Boolean;
Found_Opposite : Boolean;
Context_Dir : BC_Value;
Resolved_Dir : BC_Value;
O_Idx, C_Idx : Natural;
begin
if O >= 1 and then O <= Seq_Len
and then C >= 1 and then C <= Seq_Len
and then O < C
then
O_Idx := Seq (O);
C_Idx := Seq (C);
-- Scan between the brackets for strong types.
-- Postcondition links to ghost spec on current Types.
N0_Scan_Inner
(From_S => O + 1,
To_S => C - 1,
Ed => Embed_Dir,
FE => Found_Embed,
FO => Found_Opposite);
-- N0a: Embedding direction found inside
if Found_Embed then
Resolved_Dir := Embed_Dir;
elsif Found_Opposite then
-- N0b: Only opposite direction found, check context
Context_Dir :=
N0_Find_Context (Open_S => O, SOS_V => SOS);
Resolved_Dir :=
N0b_Resolved (Embed_Dir, Context_Dir);
else
-- N0c: No strong types inside — leave as is
Resolved_Dir := BC_Default;
end if;
-- Ghost: verify resolved direction matches spec
pragma Assert
(Resolved_Dir =
Ghost_N0_Pair_Dir
(To_GBC (Types), To_Ghost_Seq (Seq),
O, C, Embed_Dir, SOS));
-- Apply the resolution to both brackets
if Resolved_Dir /= BC_Default then
if O_Idx >= 1 and O_Idx <= Max_Paragraph_CPs then
Types (O_Idx) := Resolved_Dir;
end if;
if C_Idx >= 1 and C_Idx <= Max_Paragraph_CPs then
Types (C_Idx) := Resolved_Dir;
end if;
-- Also set any NSMs after each bracket to the
-- resolved direction (UAX #9 N0, final clause)
-- After opening bracket
for S in O + 1 .. Seq_Len loop
if Seq (S) >= 1
and then Seq (S) <= Max_Paragraph_CPs
then
if Orig_Types (Seq (S)) = BC_NSM then
Types (Seq (S)) := Resolved_Dir;
else
exit;
end if;
end if;
end loop;
-- After closing bracket
for S in C + 1 .. Seq_Len loop
if Seq (S) >= 1
and then Seq (S) <= Max_Paragraph_CPs
then
if Orig_Types (Seq (S)) = BC_NSM then
Types (Seq (S)) := Resolved_Dir;
else
exit;
end if;
end if;
end loop;
end if;
end if;
end;
pragma Loop_Invariant (Num_Pairs <= Max_Bracket_Stack);
end loop;
end Apply_N0;
-- ---------------------------------------------------------------
-- N1–N2: Neutral type resolution
-- ---------------------------------------------------------------
procedure Apply_N1_N2
with Global => (Input => (Seq, Seq_Len, Embed_Levels, SOS, EOS),
In_Out => Types),
Pre => Seq_Len >= 1
and then Seq_Len <= Max_Paragraph_CPs
and then Seq_Unique,
-- Platinum: each position gets Ghost_N_Result on original types
Post => (for all S in 1 .. Seq_Len =>
(if Seq (S) >= 1
and then Seq (S) <= Max_Paragraph_CPs
then Types (Seq (S)) =
Ghost_N_Result
(To_GBC (Types'Old),
To_Ghost_Seq (Seq),
S, Seq_Len, SOS, EOS,
Embed_Levels (Seq (S)))))
-- Frame: positions not in the sequence are unchanged
and then
(for all I in 1 .. Max_Paragraph_CPs =>
(if (for all S in 1 .. Seq_Len => Seq (S) /= I)
then Types (I) = Types'Old (I)))
is
Idx : Natural;
Run_Level : Embedding_Level;
Leading, Trailing : BC_Value;
-- Save pre-N1/N2 types for scanning (scan original types so
-- the leading/trailing match the ghost functions exactly).
Types_Pre_N : constant BC_Array := Types;
Types_G : constant Ghost_BC_Array := To_GBC (Types) with Ghost;
Seq_G : constant Ghost_Seq_Array := To_Ghost_Seq (Seq) with Ghost;
N_Done : array (1 .. Max_Paragraph_CPs) of Boolean :=
[others => False] with Ghost;
begin
for S in 1 .. Seq_Len loop
Idx := Seq (S);
if (Idx >= 1 and Idx <= Max_Paragraph_CPs) then
pragma Assert (not N_Done (Idx));
if Is_NI (Types_Pre_N (Idx)) then
-- Determine embedding level for N2
Run_Level := Embed_Levels (Idx);
-- Find leading strong type (scanning original types)
-- Track correspondence: after processing S-1 down to K
-- without finding strong, Ghost_N_Leading(K, SOS) =
-- Ghost_N_Leading(S, SOS). When found, Leading matches.
Leading := SOS;
declare
Found_Lead : Boolean := False with Ghost;
begin
for K in reverse 1 .. S - 1 loop
if Seq (K) >= 1 and Seq (K) <= Max_Paragraph_CPs then
declare
NT : constant BC_Value :=
Neutral_Type (Types_Pre_N (Seq (K)));
begin
if NT = BC_L or NT = BC_R then
Leading := NT;
Found_Lead := True;
exit;
end if;
end;
end if;
pragma Loop_Invariant (Leading = SOS);
pragma Loop_Invariant (not Found_Lead);
pragma Loop_Invariant
(Ghost_N_Leading (Types_G, Seq_G, K, SOS) =
Ghost_N_Leading (Types_G, Seq_G, S, SOS));
end loop;
-- After loop: either Found_Lead with Leading = strong type
-- at some K, or not Found_Lead with Leading = SOS.
-- In both cases: Leading = Ghost_N_Leading(S, SOS).
pragma Assert
(if not Found_Lead then
Ghost_N_Leading (Types_G, Seq_G, 1, SOS) =
Ghost_N_Leading (Types_G, Seq_G, S, SOS));
end;
pragma Assert
(Leading = Ghost_N_Leading (Types_G, Seq_G, S, SOS));
-- Find trailing strong type (scanning original types)
Trailing := EOS;
declare
Found_Trail : Boolean := False with Ghost;
begin
for K in S + 1 .. Seq_Len loop
if Seq (K) >= 1 and Seq (K) <= Max_Paragraph_CPs then
declare
NT : constant BC_Value :=
Neutral_Type (Types_Pre_N (Seq (K)));
begin
if NT = BC_L or NT = BC_R then
Trailing := NT;
Found_Trail := True;
exit;
end if;
end;
end if;
pragma Loop_Invariant (Trailing = EOS);
pragma Loop_Invariant (not Found_Trail);
pragma Loop_Invariant
(Ghost_N_Trailing
(Types_G, Seq_G, K, Seq_Len, EOS) =
Ghost_N_Trailing
(Types_G, Seq_G, S, Seq_Len, EOS));
end loop;
pragma Assert
(if not Found_Trail then
Ghost_N_Trailing
(Types_G, Seq_G, Seq_Len, Seq_Len, EOS) =
Ghost_N_Trailing
(Types_G, Seq_G, S, Seq_Len, EOS));
end;
pragma Assert
(Trailing = Ghost_N_Trailing
(Types_G, Seq_G, S, Seq_Len, EOS));
-- N1: Both sides match → that direction
if N1_Applies (Types_Pre_N (Idx), Leading, Trailing) then
Types (Idx) := N1_Resolved (Leading);
else
-- N2: Remaining NI → embedding direction
Types (Idx) := N2_Resolved (Types_Pre_N (Idx), Run_Level);
end if;
end if;
N_Done (Idx) := True;
end if;
-- Track which positions have been processed
pragma Loop_Invariant
(for all K in 1 .. S =>
(if Seq (K) >= 1 and then Seq (K) <= Max_Paragraph_CPs
then N_Done (Seq (K))));
pragma Loop_Invariant
(for all I in 1 .. Max_Paragraph_CPs =>
(if N_Done (I) then
(for some K in 1 .. S => Seq (K) = I)));
pragma Loop_Invariant
(for all K in S + 1 .. Seq_Len =>
(if Seq (K) >= 1 and then Seq (K) <= Max_Paragraph_CPs
then not N_Done (Seq (K))));
pragma Loop_Invariant
(for all I in 1 .. Max_Paragraph_CPs =>
(if not N_Done (I) then Types (I) = Types_Pre_N (I)));
pragma Loop_Invariant (Seq_Len <= Max_Paragraph_CPs);
-- Platinum: processed positions match ghost result
pragma Loop_Invariant
(for all K in 1 .. S =>
(if Seq (K) >= 1
and then Seq (K) <= Max_Paragraph_CPs
then Types (Seq (K)) =
Ghost_N_Result
(Types_G, Seq_G, K, Seq_Len, SOS, EOS,
Embed_Levels (Seq (K)))));
end loop;
end Apply_N1_N2;
-- ---------------------------------------------------------------
-- I1–I2: Implicit level resolution
-- ---------------------------------------------------------------
procedure Apply_I1_I2
with Global => (Input => (Seq, Seq_Len, Orig_Types, Types),
In_Out => Work_Levels,
Proof_In => Num),
Pre => (Seq_Len >= 1 and Seq_Len <= Max_Paragraph_CPs)
and then (Num >= 1 and Num <= Max_Paragraph_CPs)
and then Seq_Unique
and then (for all I in 1 .. Num =>
Work_Levels (I) <= Max_Depth + 1),
Post => (for all I in 1 .. Num =>
Work_Levels (I) <= Max_Depth + 1)
-- Platinum: each sequence member gets Implicit_Level
and then
(for all S in 1 .. Seq_Len =>
(if Seq (S) >= 1
and then Seq (S) <= Max_Paragraph_CPs
and then not Is_X9_Removed
(Orig_Types (Seq (S)))
and then Work_Levels'Old (Seq (S)) <= Max_Depth
then Work_Levels (Seq (S)) =
Implicit_Level
(Work_Levels'Old (Seq (S)),
Types (Seq (S)))))
-- Frame: non-sequence positions unchanged
and then
(for all I in 1 .. Max_Paragraph_CPs =>
(if not (for some S in 1 .. Seq_Len =>
Seq (S) = I)
then Work_Levels (I) = Work_Levels'Old (I)))
is
Idx : Natural;
Lev : Embedding_Level;
Levels_Orig : constant Level_Work_Array := Work_Levels with Ghost;
I12_Done : array (1 .. Max_Paragraph_CPs) of Boolean :=
[others => False] with Ghost;
begin
for S in 1 .. Seq_Len loop
Idx := Seq (S);
if (Idx >= 1 and Idx <= Max_Paragraph_CPs)
and then not Is_X9_Removed (Orig_Types (Idx))
then
-- This position is unvisited (Seq_Unique)
pragma Assert (not I12_Done (Idx));
pragma Assert (Work_Levels (Idx) = Levels_Orig (Idx));
Lev := Work_Levels (Idx);
if Lev <= Max_Depth then
Work_Levels (Idx) :=
Implicit_Level (Lev, Types (Idx));
end if;
I12_Done (Idx) := True;
end if;
pragma Loop_Invariant
(for all J in 1 .. Num =>
Work_Levels (J) <= Max_Depth + 1);
-- Track which positions have been processed
pragma Loop_Invariant
(for all K in 1 .. S =>
(if Seq (K) >= 1 and then Seq (K) <= Max_Paragraph_CPs
then I12_Done (Seq (K))
or else Is_X9_Removed (Orig_Types (Seq (K)))
or else Levels_Orig (Seq (K)) > Max_Depth));
pragma Loop_Invariant
(for all K in S + 1 .. Seq_Len =>
(if Seq (K) >= 1 and then Seq (K) <= Max_Paragraph_CPs
then not I12_Done (Seq (K))));
-- I12_Done(I) => I is a sequence member
pragma Loop_Invariant
(for all I in 1 .. Max_Paragraph_CPs =>
(if I12_Done (I) then
(for some K in 1 .. Seq_Len =>
Seq (K) = I)));
-- Unvisited positions retain original value
pragma Loop_Invariant
(for all I in 1 .. Max_Paragraph_CPs =>
(if not I12_Done (I)
then Work_Levels (I) = Levels_Orig (I)));
-- Platinum: processed positions match Implicit_Level
pragma Loop_Invariant
(for all K in 1 .. S =>
(if Seq (K) >= 1
and then Seq (K) <= Max_Paragraph_CPs
and then not Is_X9_Removed (Orig_Types (Seq (K)))
and then Levels_Orig (Seq (K)) <= Max_Depth
then Work_Levels (Seq (K)) =
Implicit_Level
(Levels_Orig (Seq (K)),
Types (Seq (K)))));
end loop;
end Apply_I1_I2;
-- Main body of Process_Run_Sequences
begin
-- For each position, determine if it starts an isolating run
-- sequence. An isolating run sequence starts at:
-- - The paragraph start (after X9 removal, first non-X9 char)
-- - After a PDI (the character after the PDI)
-- - Position that is not "continued" from a preceding isolate
-- initiator's matched PDI
--
-- Implementation: scan left to right. For each non-X9 character
-- that hasn't been visited, collect its isolating run sequence
-- (following isolate initiator → PDI links), then process it.
for I in 1 .. Num loop
if not Is_X9_Removed (Orig_Types (I))
and then not Visited (I)
then
-- Collect isolating run sequence starting at I
Seq_Len := 0;
declare
Run_Start : Natural := I;
Cont : Boolean := True;
begin
while Cont loop
pragma Loop_Invariant
(Run_Start >= 1
and then Run_Start <= Max_Paragraph_CPs + 1);
pragma Loop_Invariant
(Seq_Len <= Max_Paragraph_CPs);
pragma Loop_Invariant
(for all K in 1 .. Num =>
Work_Levels (K) <= Max_Depth + 1);
-- All Seq elements are Visited and in bounds:
pragma Loop_Invariant
(for all K in 1 .. Seq_Len =>
Seq (K) >= 1
and then Seq (K) <= Max_Paragraph_CPs
and then Visited (Seq (K)));
-- All Seq elements are pairwise distinct:
pragma Loop_Invariant
(for all A in 1 .. Seq_Len =>
(for all B in A + 1 .. Seq_Len =>
Seq (A) /= Seq (B)));
-- Add all non-X9 characters from this level run
for J in Run_Start .. Num loop
-- A level run ends when we hit a different level
-- (after X9 removal) or the end of the paragraph.
-- Use Embed_Levels (pre-I1/I2) for run boundaries.
if not Is_X9_Removed (Orig_Types (J)) then
-- Check if this is still the same level run
if J = Run_Start
or else Embed_Levels (J) = Embed_Levels (Run_Start)
then
if Seq_Len < Max_Paragraph_CPs
and then not Visited (J)
then
-- J is not yet visited, so J /= Seq(K)
-- for all K in 1..Seq_Len (since they
-- are all visited).
pragma Assert
(for all K in 1 .. Seq_Len =>
Visited (Seq (K)));
pragma Assert
(for all K in 1 .. Seq_Len =>
J /= Seq (K));
declare
Old_Len : constant Natural :=
Seq_Len with Ghost;
begin
Seq_Len := Seq_Len + 1;
Seq (Seq_Len) := J;
Visited (J) := True;
-- New element differs from all previous:
pragma Assert
(for all A in 1 .. Old_Len =>
Seq (A) /= Seq (Seq_Len));
-- Upper triangle maintained:
pragma Assert
(for all A in 1 .. Seq_Len =>
(for all B in A + 1 .. Seq_Len =>
Seq (A) /= Seq (B)));
end;
end if;
else
exit; -- different level = end of this level run
end if;
end if;
pragma Loop_Invariant (Seq_Len <= Max_Paragraph_CPs);
-- All Seq elements are Visited and in bounds:
pragma Loop_Invariant
(for all K in 1 .. Seq_Len =>
Seq (K) >= 1
and then Seq (K) <= Max_Paragraph_CPs
and then Visited (Seq (K)));
-- All Seq elements are pairwise distinct:
pragma Loop_Invariant
(for all A in 1 .. Seq_Len =>
(for all B in A + 1 .. Seq_Len =>
Seq (A) /= Seq (B)));
end loop;
-- Check if the last character in the run is an isolate
-- initiator with a matching PDI — if so, continue
-- the sequence from the character after the matching PDI
Cont := False;
if Seq_Len >= 1 then
declare
Last_Idx : constant Natural := Seq (Seq_Len);
begin
if Last_Idx >= 1
and then Last_Idx <= Max_Paragraph_CPs
and then Is_Isolate_Initiator (Orig_Types (Last_Idx))
and then Match_PDI (Last_Idx) > 0
and then Match_PDI (Last_Idx) <= Num
then
-- Add the matching PDI
declare
PDI_Pos : constant Natural :=
Match_PDI (Last_Idx);
begin
if Seq_Len < Max_Paragraph_CPs
and then not Visited (PDI_Pos)
then
pragma Assert
(for all K in 1 .. Seq_Len =>
Visited (Seq (K)));
pragma Assert
(for all K in 1 .. Seq_Len =>
PDI_Pos /= Seq (K));
declare
Old_Len : constant Natural :=
Seq_Len with Ghost;
begin
Seq_Len := Seq_Len + 1;
Seq (Seq_Len) := PDI_Pos;
Visited (PDI_Pos) := True;
pragma Assert
(for all A in 1 .. Old_Len =>
Seq (A) /= Seq (Seq_Len));
pragma Assert
(for all A in 1 .. Seq_Len =>
(for all B in A + 1 .. Seq_Len =>
Seq (A) /= Seq (B)));
end;
end if;
-- Continue from position after PDI
if PDI_Pos < Num then
Run_Start := PDI_Pos + 1;
-- Skip X9-removed chars to find next
-- non-removed at the same level
while Run_Start <= Num
and then Is_X9_Removed (Orig_Types (Run_Start))
loop
Run_Start := Run_Start + 1;
pragma Loop_Invariant
(Run_Start >= 1
and then Run_Start <= Num + 1);
pragma Loop_Invariant
(Seq_Len <= Max_Paragraph_CPs);
pragma Loop_Invariant
(for all K in 1 .. Seq_Len =>
Seq (K) >= 1
and then Seq (K) <= Max_Paragraph_CPs
and then Visited (Seq (K)));
pragma Loop_Invariant
(for all A in 1 .. Seq_Len =>
(for all B in A + 1 .. Seq_Len =>
Seq (A) /= Seq (B)));
end loop;
if Run_Start <= Num
and then Embed_Levels (Run_Start) =
Embed_Levels (PDI_Pos)
then
Cont := True;
end if;
end if;
end;
end if;
end;
end if;
end loop;
end;
if Seq_Len >= 1 then
-- Determine sos and eos (X10)
declare
First_Idx : constant Natural := Seq (1);
Last_Idx : constant Natural := Seq (Seq_Len);
First_Level, Last_Level : Embedding_Level;
Prev_Level, Next_Level : Embedding_Level;
Higher : Embedding_Level;
begin
-- Level of first and last characters in sequence
-- (use Embed_Levels = pre-I1/I2 embedding levels)
if First_Idx >= 1 and First_Idx <= Max_Paragraph_CPs then
First_Level := Embed_Levels (First_Idx);
else
First_Level := PL;
end if;
if Last_Idx >= 1 and Last_Idx <= Max_Paragraph_CPs then
Last_Level := Embed_Levels (Last_Idx);
else
Last_Level := PL;
end if;
-- sos: max(level of first char, level of preceding char)
-- The preceding char is the one before the start of
-- the first level run (or paragraph level if at start)
Prev_Level := PL;
if First_Idx >= 2
and then First_Idx <= Max_Paragraph_CPs
then
Prev_Level := Effective_Level (First_Idx - 1);
end if;
Higher := Embedding_Level'Max (First_Level, Prev_Level);
SOS := Direction_From_Level (Higher);
-- eos: max(level of last char, level of following char)
-- The following char is the one after the end of
-- the last level run (or paragraph level if at end).
-- Use Embed_Levels (pre-I1/I2) for eos computation.
Next_Level := PL;
if Last_Idx >= 1 and Last_Idx < Num then
-- Find next non-X9 character
for K in Last_Idx + 1 .. Num loop
if not Is_X9_Removed (Orig_Types (K)) then
Next_Level := Embed_Levels (K);
exit;
end if;
end loop;
end if;
Higher := Embedding_Level'Max (Last_Level, Next_Level);
EOS := Direction_From_Level (Higher);
end;
-- Apply W rules
Apply_W1;
Apply_W2;
Apply_W3;
Apply_W4;
Apply_W5;
Apply_W6;
Apply_W7;
-- Apply N0 (bracket pair resolution)
Apply_N0;
-- Apply N1–N2 (neutral resolution)
Apply_N1_N2;
-- After W+N rules, Types contains the final resolved
-- bidi types for this sequence. Work_Levels still holds
-- embedding levels (W/N rules don't touch Work_Levels:
-- their Global has In_Out => Types, not Work_Levels).
-- Apply I1–I2 (implicit level resolution)
Apply_I1_I2;
end if;
end if;
pragma Loop_Invariant
(for all J in 1 .. Num =>
Work_Levels (J) <= Max_Depth + 1);
end loop;
end Process_Run_Sequences;
-----------------------------------------------------------------------
-- Phase 5: L1 — Reset whitespace/isolate formatting levels
-----------------------------------------------------------------------
procedure Apply_L1
with Global => (Input => (PL, Num, Orig_Types),
In_Out => Work_Levels),
Pre => Num >= 1
and then Num <= Max_Paragraph_CPs
and then PL <= 1
and then (for all I in 1 .. Num =>
Work_Levels (I) <= Max_Depth + 1),
Post => (for all I in 1 .. Num =>
Work_Levels (I) <= Max_Depth + 1)
-- Platinum: positions identified by Ghost_L1_Should_Reset
-- are set to PL; all others are unchanged.
and then
(for all I in 1 .. Num =>
(if Ghost_L1_Should_Reset
(To_GBC_Outer (Orig_Types), I, Num)
then Work_Levels (I) = PL
else Work_Levels (I) = Work_Levels'Old (I)))
is
OT_G : constant Ghost_BC_Array := To_GBC_Outer (Orig_Types)
with Ghost;
Levels_Orig : constant Level_Work_Array := Work_Levels with Ghost;
begin
-- L1: On each line, reset the embedding level of the following
-- characters to the paragraph embedding level:
-- 1. Segment separators (S)
-- 2. Paragraph separators (B)
-- 3. Any sequence of whitespace characters and/or isolate formatting
-- characters preceding a segment separator, paragraph separator,
-- or the end of the line/paragraph.
-- Process from end backward: find trailing WS/isolate sequences
-- and reset them to paragraph level
declare
Reset : Boolean := True; -- Start at end of paragraph = True
begin
for I in reverse 1 .. Num loop
-- At entry: Reset = Ghost_L1_Trailing(OT_G, I, Num)
-- This holds initially: Reset=True, Ghost_L1_Trailing(Num, Num)=True.
-- Ghost_L1_Should_Reset unfolds to use Ghost_L1_Trailing for
-- L1-reset-type positions.
pragma Assert (OT_G (I) = Orig_Types (I));
if Is_X9_Removed (Orig_Types (I)) then
-- Ghost_L1_Should_Reset: X9 → False; level unchanged. ✓
null;
elsif Orig_Types (I) = BC_S or Orig_Types (I) = BC_B then
-- Ghost_L1_Should_Reset: S/B → True; set PL. ✓
Work_Levels (I) := PL;
Reset := True;
elsif Is_L1_Reset_Type (Orig_Types (I)) then
-- Ghost_L1_Should_Reset: L1-reset → Ghost_L1_Trailing(I, Num)
-- = Reset (at entry). If Reset then PL, else unchanged. ✓
if Reset then
Work_Levels (I) := PL;
end if;
else
-- Ghost_L1_Should_Reset: other → False; unchanged. ���
Reset := False;
end if;
-- After processing I, Reset captures the trailing state for
-- position I-1 (or is irrelevant if I = 1).
-- Ghost_L1_Trailing(I-1, Num) checks Types(I):
-- X9-removed(I): skip → Ghost_L1_Trailing(I, Num) = Reset(old)
-- S/B(I): True = Reset(new)
-- L1-reset(I): skip → Ghost_L1_Trailing(I, Num) = Reset(old)
-- other(I): False = Reset(new)
-- Safety: levels stay bounded
pragma Loop_Invariant
(for all J in 1 .. Num =>
Work_Levels (J) <= Max_Depth + 1);
-- Connect Reset to ghost trailing state for position I-1
pragma Loop_Invariant
(if I >= 2
then Reset = Ghost_L1_Trailing (OT_G, I - 1, Num)
else True);
-- Platinum: processed positions match ghost specification
pragma Loop_Invariant
(for all J in I .. Num =>
(if Ghost_L1_Should_Reset (OT_G, J, Num)
then Work_Levels (J) = PL
else Work_Levels (J) = Levels_Orig (J)));
-- Unprocessed positions retain original value
pragma Loop_Invariant
(for all J in 1 .. I - 1 =>
Work_Levels (J) = Levels_Orig (J));
end loop;
end;
end Apply_L1;
OK : Boolean;
-- Main body of Resolve_Levels
begin
Levels := [others => 0];
Num_CPs := 0;
Para_Level := 0;
Success := False;
-- Phase 1: Decode
Decode_Paragraph (OK);
if not OK then return; end if;
-- Phase 2: Determine paragraph level
Determine_Para_Level;
-- Initialize work levels
Work_Levels := [others => 0];
-- Phase 3: Resolve explicit levels (X1–X8)
Resolve_Explicit_Levels;
-- Save embedding levels before W/N/I rule modifications.
-- Embed_Levels preserves the X1-X8 output for sos/eos computation
-- and level run boundary detection in Process_Run_Sequences.
for I in 1 .. Num loop
Embed_Levels (I) := Work_Levels (I);
pragma Loop_Invariant
(for all J in 1 .. I => Embed_Levels (J) <= Max_Depth);
end loop;
-- Phase 4: Process isolating run sequences (W1–W7, N0–N2, I1–I2)
pragma Warnings
(GNATprove, Off,
"""Types"" is set by ""Process_Run_Sequences"" but not used*",
Reason => "Types is scratch storage; the resolved levels in "
& "Work_Levels are the phase output");
Process_Run_Sequences;
pragma Warnings
(GNATprove, On,
"""Types"" is set by ""Process_Run_Sequences"" but not used*");
-- Phase 5: L1 — Reset whitespace levels
Apply_L1;
-- X9 cleanup: set each X9-removed character's level to the level
-- of the nearest preceding non-removed character (or PL if at start).
-- This prevents X9-removed characters from creating artificial level
-- boundaries during L2 reordering.
declare
Prev_Level : Embedding_Level := PL;
begin
for I in 1 .. Num loop
if Is_X9_Removed (Orig_Types (I)) then
Work_Levels (I) := Prev_Level;
else
Prev_Level := Work_Levels (I);
end if;
pragma Loop_Invariant
(for all J in 1 .. Num =>
Work_Levels (J) <= Max_Depth + 1);
end loop;
end;
-- Copy results to output
Num_CPs := Num;
Para_Level := PL;
for I in 1 .. Num loop
Levels (I) := Work_Levels (I);
pragma Loop_Invariant
(for all J in 1 .. I =>
Levels (J) <= Max_Depth + 1);
end loop;
Success := True;
end Resolve_Levels;
---------------------------------------------------------------------------
-- Reorder (L2)
--
-- L2: From the highest level found in the text to the lowest odd
-- level on each line, including intermediate levels not actually
-- present in the text, reverse any contiguous sequence of characters
-- that are at that level or higher.
---------------------------------------------------------------------------
procedure Reorder
(Levels : Level_Array;
Num_CPs : Paragraph_Length;
Para_Level : Embedding_Level;
Order : out Index_Array;
Success : out Boolean)
is
Max_Level : Embedding_Level := 0;
Min_Odd : Embedding_Level := Max_Depth + 1;
-- Ghost inverse: Inv(V) = position I such that Order(I) = V.
-- Maintaining this makes the surjectivity proof tractable:
-- the witness for "for some I => Order(I) = V" is Inv(V).
Inv : Index_Array := [others => 0] with Ghost;
-- Ghost predicate: Order and Inv form a valid permutation pair
-- over 1..Num_CPs.
function Is_Perm return Boolean
is ((for all I in 1 .. Num_CPs =>
Order (I) >= 1 and Order (I) <= Num_CPs)
and then
(for all V in 1 .. Num_CPs =>
Inv (V) >= 1
and then Inv (V) <= Num_CPs
and then Order (Inv (V)) = V))
with Ghost;
begin
Order := [others => 0];
-- Initialize identity permutation and its inverse
for I in 1 .. Num_CPs loop
Order (I) := I;
Inv (I) := I;
pragma Loop_Invariant
(for all J in 1 .. I =>
Order (J) = J and Inv (J) = J);
end loop;
-- Is_Perm holds after identity init
pragma Assert (Is_Perm);
-- Find max level and min odd level
for I in 1 .. Num_CPs loop
if Levels (I) > Max_Level then
Max_Level := Levels (I);
end if;
if Levels (I) mod 2 = 1 and then Levels (I) < Min_Odd then
Min_Odd := Levels (I);
end if;
end loop;
-- If no RTL content, nothing to reorder
if Max_Level < 2 and then Min_Odd > Max_Level then
-- Check if paragraph level is RTL
if Para_Level = 1 then
Min_Odd := 1;
else
-- Provide surjectivity witnesses before returning
pragma Assert (Is_Perm);
pragma Assert
(for all V in 1 .. Num_CPs =>
Inv (V) >= 1
and then Inv (V) <= Num_CPs
and then Order (Inv (V)) = V);
pragma Assert
(for all V in 1 .. Num_CPs =>
(for some I in 1 .. Num_CPs => Order (I) = V));
Success := True;
return;
end if;
end if;
-- Ensure min_odd is at least 1
if Min_Odd > Max_Level then
Min_Odd := (if Max_Level mod 2 = 1 then Max_Level else 1);
end if;
-- L2: Reverse contiguous sequences at each level from max to min_odd
for Level in reverse Min_Odd .. Max_Level loop
declare
Start : Natural := 0;
begin
for I in 1 .. Num_CPs loop
if Levels (I) >= Level then
if Start = 0 then
Start := I;
end if;
else
if Start > 0 then
-- Reverse Order(Start..I-1)
declare
Left : Natural := Start;
Right : Natural := I - 1;
begin
while Left < Right loop
pragma Assert (Left >= 1 and Left <= Num_CPs);
pragma Assert (Right >= 1 and Right <= Num_CPs);
declare
OL : constant Natural := Order (Left);
OR_Val : constant Natural := Order (Right);
begin
pragma Assert (OL >= 1 and OL <= Num_CPs);
pragma Assert (OR_Val >= 1 and OR_Val <= Num_CPs);
-- Swap Order
Order (Left) := OR_Val;
Order (Right) := OL;
-- Swap Inv to maintain the inverse
Inv (OR_Val) := Left;
Inv (OL) := Right;
end;
Left := Left + 1;
Right := Right - 1;
pragma Loop_Invariant
(Left >= 1 and Left <= Max_Paragraph_CPs);
pragma Loop_Invariant
(Right >= 1 and Right <= Num_CPs);
pragma Loop_Invariant (Is_Perm);
end loop;
end;
Start := 0;
end if;
end if;
pragma Loop_Invariant (Start <= Num_CPs);
pragma Loop_Invariant (Is_Perm);
end loop;
-- Handle trailing sequence
if Start > 0 then
declare
Left : Natural := Start;
Right : Natural := Num_CPs;
begin
while Left < Right loop
pragma Assert (Left >= 1 and Left <= Num_CPs);
pragma Assert (Right >= 1 and Right <= Num_CPs);
declare
OL : constant Natural := Order (Left);
OR_Val : constant Natural := Order (Right);
begin
pragma Assert (OL >= 1 and OL <= Num_CPs);
pragma Assert (OR_Val >= 1 and OR_Val <= Num_CPs);
-- Swap Order
Order (Left) := OR_Val;
Order (Right) := OL;
-- Swap Inv to maintain the inverse
Inv (OR_Val) := Left;
Inv (OL) := Right;
end;
Left := Left + 1;
Right := Right - 1;
pragma Loop_Invariant
(Left >= 1 and Left <= Num_CPs);
pragma Loop_Invariant
(Right >= 1 and Right <= Num_CPs);
pragma Loop_Invariant (Is_Perm);
end loop;
end;
end if;
end;
pragma Loop_Invariant (Is_Perm);
end loop;
-- Provide surjectivity witnesses for the postcondition.
-- Is_Perm guarantees Order(Inv(V)) = V for all V.
-- We unfold this to provide existential witnesses.
pragma Assert (Is_Perm);
pragma Assert
(for all V in 1 .. Num_CPs =>
Inv (V) >= 1
and then Inv (V) <= Num_CPs
and then Order (Inv (V)) = V);
pragma Assert
(for all V in 1 .. Num_CPs =>
(for some I in 1 .. Num_CPs => Order (I) = V));
Success := True;
end Reorder;
---------------------------------------------------------------------------
-- Needs_Mirror — UAX #9 L4
---------------------------------------------------------------------------
function Needs_Mirror
(CP : Codepoint;
Level : Embedding_Level) return Boolean
is
((Level mod 2 = 1) and then Properties.Get_Bidi_Mirrored (CP));
end Lingenic_Text.Bidi;