lingenic_text-text_transform

--  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 — Generic text transformation body
--
--  UTF-8 decode loop.  Calls On_Codepoint for each decoded codepoint,
--  then On_Finish at end of input.  Output position tracking and error
--  propagation are handled here; the module callbacks do the real work.
-------------------------------------------------------------------------------

with Lingenic_Text.UTF8;

procedure Lingenic_Text.Text_Transform
  (Input  : Byte_Array;
   State  : in out State_Type;
   Output : in out Byte_Array;
   Last   : out Natural;
   OK     : out Boolean)
with SPARK_Mode
is
   Pos     : Positive := Input'First;
   CP      : Codepoint;
   Len     : Positive;
   Valid   : Boolean;
   Out_Pos : Natural := Output'First;
begin
   Last := Output'First - 1;
   OK := True;

   while Pos <= Input'Last loop
      pragma Loop_Invariant (Pos >= Input'First);
      pragma Loop_Invariant (Out_Pos >= Output'First);
      pragma Loop_Invariant (Out_Pos <= Output'Last + 1);
      pragma Loop_Invariant (OK);
      pragma Loop_Invariant (Partial_Valid (State, Output, Out_Pos));
      pragma Loop_Variant (Increases => Pos);

      UTF8.Decode (Input, Pos, CP, Len, Valid);
      if not Valid then
         OK := False;
         return;
      end if;

      On_Codepoint (State, CP, Output, Out_Pos, OK);
      if not OK then
         return;
      end if;

      --  Advance past decoded UTF-8 sequence
      if Pos > Input'Last - Len + 1 then
         Pos := Input'Last + 1;
      else
         Pos := Pos + Len;
      end if;
   end loop;

   On_Finish (State, Output, Out_Pos, OK);
   if not OK then
      return;
   end if;

   if Out_Pos = Output'First then
      --  No output produced.  Postcondition requires Last in range on
      --  success, so report failure.
      OK := False;
   else
      Last := Out_Pos - 1;
   end if;
end Lingenic_Text.Text_Transform;