lingenic_text

--  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
--
--  Root package: core types used throughout the library.
-------------------------------------------------------------------------------

package Lingenic_Text
   with SPARK_Mode => On,
        Pure
is

   --  A Unicode codepoint: U+0000 .. U+10FFFF.
   --
   --  This subtype is the full Unicode codespace and DOES include the
   --  surrogate range U+D800 .. U+DFFF.  Surrogates are not Unicode scalar
   --  values, but they are codepoints in the abstract sense, so the type
   --  system does not exclude them here.  Scalar-value-only inputs are
   --  enforced structurally one layer up by the UTF-8 well-formedness
   --  predicates (`UTF8_Spec.WF3` rejects the `ED A0..BF tail` lead-tail
   --  combinations that would encode surrogates), so any codepoint that
   --  reaches the algorithm layer via `UTF8.Decode` is already a scalar
   --  value.  Use `Is_Scalar_Value` (below) when filtering codepoints
   --  obtained from non-UTF-8 sources.
   subtype Codepoint is Natural range 0 .. 16#10_FFFF#;

   --  A single byte value
   subtype Byte is Natural range 0 .. 255;

   --  A contiguous array of bytes (e.g. UTF-8 encoded text)
   type Byte_Array is array (Positive range <>) of Byte;

   --  Maximum codepoint value
   Max_Codepoint : constant Codepoint := 16#10_FFFF#;

   --  Total number of codepoint values
   Codepoint_Count : constant Positive := Max_Codepoint + 1;

   --  Surrogate range (not valid scalar values)
   Surrogate_First : constant := 16#D800#;
   Surrogate_Last  : constant := 16#DFFF#;

   --  A Unicode scalar value: a codepoint that is not a surrogate
   function Is_Scalar_Value (CP : Codepoint) return Boolean is
     (CP < Surrogate_First or CP > Surrogate_Last);

   --  Noncharacter codepoints: U+FDD0..U+FDEF and U+xFFFE, U+xFFFF per plane
   function Is_Noncharacter (CP : Codepoint) return Boolean is
     ((CP >= 16#FDD0# and CP <= 16#FDEF#)
      or (CP mod 16#10000# >= 16#FFFE#));

   ---------------------------------------------------------------------------
   --  ASCII byte constants used by UCD file format and parser
   ---------------------------------------------------------------------------

   LF_Byte        : constant Byte := 10;   --  Line feed
   CR_Byte        : constant Byte := 13;   --  Carriage return
   Space_Byte     : constant Byte := 32;   --  Space
   Tab_Byte       : constant Byte := 9;    --  Horizontal tab
   Hash_Byte      : constant Byte := 35;   --  '#'
   Dot_Byte       : constant Byte := 46;   --  '.'
   Semicolon_Byte : constant Byte := 59;   --  ';'
   Zero_Byte      : constant Byte := 48;   --  '0'
   Nine_Byte      : constant Byte := 57;   --  '9'
   Upper_A_Byte   : constant Byte := 65;   --  'A'
   Upper_F_Byte   : constant Byte := 70;   --  'F'

   ---------------------------------------------------------------------------
   --  Character classification for UCD file parsing
   ---------------------------------------------------------------------------

   function Is_Hex_Digit (B : Byte) return Boolean is
     (B in Zero_Byte .. Nine_Byte
      or else B in Upper_A_Byte .. Upper_F_Byte);

   function Hex_Value (B : Byte) return Natural is
     (if B in Zero_Byte .. Nine_Byte then B - Zero_Byte
      else B - Upper_A_Byte + 10)
   with Pre => Is_Hex_Digit (B),
        Post => Hex_Value'Result <= 15;

   function Is_Line_End (B : Byte) return Boolean is
     (B = LF_Byte or B = CR_Byte);

   function Is_Field_Space (B : Byte) return Boolean is
     (B = Space_Byte or B = Tab_Byte);

end Lingenic_Text;