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
--  Formally Verified Unicode Text Processing Library
--
--  Generic text transformation.
--
--  One entry point for all modules that process UTF-8 input and produce
--  UTF-8 output: normalization, case mapping, or any future transform.
--
--  The generic handles:
--    - UTF-8 decoding of input bytes into codepoints
--    - Output buffer position tracking
--    - Per-codepoint dispatch to the module-specific callback
--    - End-of-input finalization
--
--  The module provides State_Type plus four formal subprograms:
--
--    Output_Valid    — final specification: what "correct output" means
--    Partial_Valid   — loop invariant: maintained across On_Codepoint calls
--    On_Codepoint    — per-codepoint processing (preserves Partial_Valid)
--    On_Finish       — finalization (bridges Partial_Valid → Output_Valid)
--
--  The generic carries Partial_Valid as its loop invariant.  On_Codepoint's
--  postcondition preserves it.  On_Finish's postcondition bridges from
--  Partial_Valid to Output_Valid.  The generic's postcondition asserts
--  Output_Valid holds on success.
--
--  Formal procedure contracts guarantee the output position never retreats
--  and never exceeds Output'Last + 1, so the generic loop invariants hold.
-------------------------------------------------------------------------------

generic
   type State_Type is private;

   with function Output_Valid
     (S      : State_Type;
      Output : Byte_Array;
      Last   : Natural) return Boolean;

   with function Partial_Valid
     (S      : State_Type;
      Output : Byte_Array;
      Pos    : Natural) return Boolean;

   with procedure On_Codepoint
     (State  : in out State_Type;
      CP     : Codepoint;
      Output : in out Byte_Array;
      Pos    : in out Natural;
      OK     : in out Boolean)
   with Pre  => Output'Last < Positive'Last
                and then Pos >= Output'First
                and then Pos <= Output'Last + 1
                and then OK
                and then Partial_Valid (State, Output, Pos),
        Post => Pos >= Pos'Old
                and then Pos <= Output'Last + 1
                and then (if OK then
                            Partial_Valid (State, Output, Pos));

   with procedure On_Finish
     (State  : in out State_Type;
      Output : in out Byte_Array;
      Pos    : in out Natural;
      OK     : in out Boolean)
   with Pre  => Output'Last < Positive'Last
                and then Pos >= Output'First
                and then Pos <= Output'Last + 1
                and then OK
                and then Partial_Valid (State, Output, Pos),
        Post => Pos >= Pos'Old
                and then Pos <= Output'Last + 1
                and then (if OK and then Pos > Output'First then
                            Output_Valid (State, Output, Pos - 1));

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,
     Pre  => Input'Length >= 1
             and then Output'Length >= 1
             and then Input'Last < Positive'Last
             and then Output'Last < Positive'Last
             and then Partial_Valid (State, Output, Output'First),
     Post => (if OK then Last in Output'First .. Output'Last
                         and then Output_Valid (State, Output, Last)
              else Last = Output'First - 1),
     Always_Terminates;