「‍」 Lingenic

lingenic_text-eaw_spec

(⤓.ads ◇.ads); γ ≜ [2026-07-12T135427.522, 2026-07-12T135427.522] ∧ |γ| = 1

--  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
--
--  Ghost specification for East Asian Width (UAX #11).
--
--  Defines abstract East_Asian_Width property values and a Cell_Width
--  function that maps each value to a display width (1 or 2 cells).
--
--  Wide and Fullwidth characters occupy 2 cells in a fixed-pitch font.
--  All others occupy 1 cell.
-------------------------------------------------------------------------------

package Lingenic_Text.EAW_Spec
   with SPARK_Mode, Pure
is

   ---------------------------------------------------------------------------
   --  Abstract East_Asian_Width property values
   ---------------------------------------------------------------------------

   EAW_Neutral   : constant := 0;  --  N (default)
   EAW_Ambiguous : constant := 1;  --  A
   EAW_Halfwidth : constant := 2;  --  H
   EAW_Wide      : constant := 3;  --  W
   EAW_Fullwidth : constant := 4;  --  F
   EAW_Narrow    : constant := 5;  --  Na

   subtype EAW_Value is Natural range 0 .. 5;

   ---------------------------------------------------------------------------
   --  Cell_Width — display width in fixed-pitch cells
   --
   --  Wide and Fullwidth characters take 2 cells.
   --  All other categories (Neutral, Ambiguous, Halfwidth, Narrow) take 1.
   --
   --  Note: Ambiguous characters may be 2 cells in East Asian context.
   --  This function returns 1 for Ambiguous, which is correct for
   --  non-East-Asian contexts.  Callers can override for Ambiguous.
   ---------------------------------------------------------------------------

   function Cell_Width (V : EAW_Value) return Natural
   is (if V = EAW_Wide or V = EAW_Fullwidth then 2 else 1);

end Lingenic_Text.EAW_Spec;