lingenic_text-case_mapping_spec

--  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
--
--  Case mapping ghost specification (Unicode Standard, Section 3.13).
--
--  Types and constants for case conversion operations.  Minimal ghost spec —
--  case mapping is table-driven.  The complexity is in initialization
--  (parsing UCD files) and the Final_Sigma state machine, not in ghost
--  predicates.
-------------------------------------------------------------------------------

package Lingenic_Text.Case_Mapping_Spec
   with SPARK_Mode, Pure
is

   ---------------------------------------------------------------------------
   --  Case operations
   ---------------------------------------------------------------------------

   type Case_Operation is (Op_Uppercase, Op_Lowercase, Op_Titlecase, Op_Casefold);

   ---------------------------------------------------------------------------
   --  Constants
   ---------------------------------------------------------------------------

   --  Max codepoints in a single full case mapping.
   --  SpecialCasing.txt mappings produce at most 3 codepoints.
   Max_Mapping_Len : constant := 3;

   --  Max pending codepoints for Final_Sigma buffering.
   --  During lowercase, when we see Greek capital sigma (U+03A3), we buffer
   --  it plus any trailing Case_Ignorable characters until we can determine
   --  whether Final_Sigma context applies.  32 is generous — in practice
   --  the run of Case_Ignorable characters between sigma and the next
   --  non-Case_Ignorable character is very short.
   Max_Pending : constant := 32;

   --  Greek sigma codepoints
   Greek_Capital_Sigma : constant Codepoint := 16#03A3#;
   Greek_Small_Sigma   : constant Codepoint := 16#03C3#;  --  medial
   Greek_Small_Final   : constant Codepoint := 16#03C2#;  --  final

   ---------------------------------------------------------------------------
   --  Is_Final_Sigma — ghost predicate for Final_Sigma context (Section 3.13)
   --
   --  A Greek capital sigma (U+03A3) maps to:
   --    ς (U+03C2, final)  when Preceded_By_Cased AND NOT Followed_By_Cased
   --    σ (U+03C3, medial) otherwise
   --
   --  Both conditions ignore intervening Case_Ignorable characters.
   --
   --  Parameters:
   --    Prev_Was_Cased  — True if the last non-Case_Ignorable before sigma
   --                      had the Cased property (Preceded_By_Cased).
   --    Followed_By_Cased — True if the next non-Case_Ignorable after sigma
   --                        has the Cased property.
   ---------------------------------------------------------------------------

   function Is_Final_Sigma
     (Prev_Was_Cased    : Boolean;
      Followed_By_Cased : Boolean) return Boolean
   is (Prev_Was_Cased and not Followed_By_Cased)
   with Ghost;

   function Final_Sigma_Result
     (Prev_Was_Cased    : Boolean;
      Followed_By_Cased : Boolean) return Codepoint
   is (if Is_Final_Sigma (Prev_Was_Cased, Followed_By_Cased)
       then Greek_Small_Final
       else Greek_Small_Sigma)
   with Ghost;

end Lingenic_Text.Case_Mapping_Spec;