lingenic_text-normalization_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
--
--  Normalization ghost specification (UAX #15).
--
--  CCC values, Quick Check values, Hangul syllable constants and
--  predicates, canonical ordering predicate.  All expression functions
--  for solver unfolding.
-------------------------------------------------------------------------------

package Lingenic_Text.Normalization_Spec
   with SPARK_Mode, Pure
is

   ---------------------------------------------------------------------------
   --  Canonical_Combining_Class (0 .. 254)
   --  0 = starter, non-zero = non-starter (reorderable)
   ---------------------------------------------------------------------------

   subtype CCC_Value is Natural range 0 .. 254;

   function Is_Starter (CCC : CCC_Value) return Boolean
   is (CCC = 0);

   ---------------------------------------------------------------------------
   --  Quick Check values
   ---------------------------------------------------------------------------

   type QC_Value is (QC_Yes, QC_No, QC_Maybe);

   ---------------------------------------------------------------------------
   --  Normalization forms
   ---------------------------------------------------------------------------

   type Normalization_Form is (NFD, NFC, NFKD, NFKC);

   function Is_Canonical (Form : Normalization_Form) return Boolean
   is (Form = NFD or Form = NFC);

   function Is_Compose (Form : Normalization_Form) return Boolean
   is (Form = NFC or Form = NFKC);

   ---------------------------------------------------------------------------
   --  Hangul syllable constants (Unicode Standard, Section 3.12)
   ---------------------------------------------------------------------------

   SBase  : constant := 16#AC00#;
   LBase  : constant := 16#1100#;
   VBase  : constant := 16#1161#;
   TBase  : constant := 16#11A7#;
   LCount : constant := 19;
   VCount : constant := 21;
   TCount : constant := 28;
   NCount : constant := VCount * TCount;   --  588
   SCount : constant := LCount * NCount;   --  11172

   function Is_Hangul_Syllable (CP : Codepoint) return Boolean
   is (CP >= SBase and then CP < SBase + SCount);

   function Is_Hangul_LV (CP : Codepoint) return Boolean
   is (Is_Hangul_Syllable (CP)
       and then (CP - SBase) mod TCount = 0);

   function Is_Hangul_L (CP : Codepoint) return Boolean
   is (CP >= LBase and then CP < LBase + LCount);

   function Is_Hangul_V (CP : Codepoint) return Boolean
   is (CP >= VBase and then CP < VBase + VCount);

   function Is_Hangul_T (CP : Codepoint) return Boolean
   is (CP > TBase and then CP <= TBase + TCount - 1);

   ---------------------------------------------------------------------------
   --  Canonical ordering
   --
   --  Within a segment of non-starters between two starters, CCC values
   --  must be in non-decreasing order.
   ---------------------------------------------------------------------------

   function CCC_Ordered (A, B : CCC_Value) return Boolean
   is (A <= B);

end Lingenic_Text.Normalization_Spec;