-- 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_Spec body
--
-- Bodies for the opaque boundary-safe wrapper functions.
-- Each wrapper dispatches to the corresponding recursive expression
-- function, with a boundary check for Pos > Source'Last.
-- The postcondition on each wrapper equates its result to the expression
-- function, so the solver uses only the postcondition at call sites
-- without inlining the recursive body.
-------------------------------------------------------------------------------
package body Lingenic_Text.Bidi_Brackets_Spec
with SPARK_Mode
is
function Expected_Open_From
(Source : Byte_Array;
Pos : Positive;
CP : Codepoint) return Natural
is
begin
if Pos > Source'Last then
return 0;
else
return Expected_Open_Mapping (Source, Pos, CP);
end if;
end Expected_Open_From;
function Expected_Close_From
(Source : Byte_Array;
Pos : Positive;
CP : Codepoint) return Natural
is
begin
if Pos > Source'Last then
return 0;
else
return Expected_Close_Mapping (Source, Pos, CP);
end if;
end Expected_Close_From;
function Expected_Is_Open_From
(Source : Byte_Array;
Pos : Positive;
CP : Codepoint) return Boolean
is
begin
if Pos > Source'Last then
return False;
else
return Expected_Is_Open (Source, Pos, CP);
end if;
end Expected_Is_Open_From;
function Expected_Is_Close_From
(Source : Byte_Array;
Pos : Positive;
CP : Codepoint) return Boolean
is
begin
if Pos > Source'Last then
return False;
else
return Expected_Is_Close (Source, Pos, CP);
end if;
end Expected_Is_Close_From;
end Lingenic_Text.Bidi_Brackets_Spec;