-- 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
--
-- Unicode case mapping (Unicode Standard, Section 3.13).
--
-- Implements default (non-tailored) case conversion:
-- Uppercase — toUppercase: per-codepoint full case mapping
-- Lowercase — toLowercase: per-codepoint full case mapping + Final_Sigma
-- Titlecase — toTitlecase: word-boundary-aware, first cased → title
-- Casefold — toCasefold: per-codepoint full case folding
--
-- Self-contained module with its own Initialize. Reads:
-- UnicodeData.txt — simple case mappings (fields 12/13/14)
-- SpecialCasing.txt — full (multi-char) mappings, unconditional
-- CaseFolding.txt — case folding (status C+F for full)
-- DerivedCoreProperties.txt — Uppercase/Lowercase boolean properties
--
-- Data tables:
-- Upper_Index/Data — per-codepoint uppercase mapping
-- Lower_Index/Data — per-codepoint lowercase mapping
-- Title_Index/Data — per-codepoint titlecase mapping
-- Fold_Index/Data — per-codepoint case fold mapping
-- Is_Cased_Table — D135: has Uppercase/Lowercase property or GC=Lt
-- Is_Case_Ignorable_Table — D136: WBP/GC classification
--
-- Final_Sigma (the only context-dependent mapping in default mode) is
-- handled by buffering sigma + trailing Case_Ignorable characters during
-- lowercase, resolving to final sigma (ς) or medial sigma (σ) when the
-- following context becomes clear.
-------------------------------------------------------------------------------
with Lingenic_Text.Case_Mapping_Spec;
with Lingenic_Text.Properties;
with Lingenic_Text.UTF8_Spec;
with Lingenic_Text.Words;
package Lingenic_Text.Case_Mapping
with SPARK_Mode,
Abstract_State => Case_State,
Initializes => Case_State
is
---------------------------------------------------------------------------
-- Initialization
---------------------------------------------------------------------------
function Initialized return Boolean
with Global => Case_State;
procedure Initialize
(UCD_Dir : String;
Success : out Boolean)
with Global => (Output => Case_State,
Input => Properties.Property_State),
Pre => Properties.Initialized,
Post => (if Success then Initialized);
---------------------------------------------------------------------------
-- Status
---------------------------------------------------------------------------
type Case_Status is (Success, Buffer_Overflow, Invalid_Input);
---------------------------------------------------------------------------
-- Uppercase
--
-- Map each character in Input to its full uppercase mapping.
-- Output'Length >= Input'Length * 3 is sufficient for all inputs.
---------------------------------------------------------------------------
procedure Uppercase
(Input : Byte_Array;
Output : in out Byte_Array;
Last : out Natural;
Status : out Case_Status)
with Pre => Initialized
and then Input'Length >= 1
and then Output'Length >= 1
and then Input'Last < Positive'Last
and then Output'Last < Positive'Last
and then Output'Length <= Max_Out_Acc,
Post => (if Status = Success then
Last in Output'First .. Output'Last
and then Last - Output'First + 1 =
Ghost_Upper_Total (Input)
else
Last = Output'First - 1),
Always_Terminates;
---------------------------------------------------------------------------
-- Lowercase
--
-- Map each character in Input to its full lowercase mapping.
-- Handles Final_Sigma context for Greek sigma (U+03A3).
-- Output'Length >= Input'Length * 3 is sufficient for all inputs.
---------------------------------------------------------------------------
procedure Lowercase
(Input : Byte_Array;
Output : in out Byte_Array;
Last : out Natural;
Status : out Case_Status)
with Pre => Initialized
and then Input'Length >= 1
and then Output'Length >= 1
and then Input'Last < Positive'Last
and then Output'Last < Positive'Last
and then Output'Length <= Max_Out_Acc,
Post => (if Status = Success then
Last in Output'First .. Output'Last
and then Last - Output'First + 1 =
Ghost_Lower_Total (Input)
else
Last = Output'First - 1),
Always_Terminates;
---------------------------------------------------------------------------
-- Titlecase
--
-- For each word (per UAX #29 word boundaries): map the first cased
-- character to its titlecase mapping, map all subsequent characters
-- to lowercase. Uncased characters before the first cased character
-- in each word are passed through unchanged.
-- Output'Length >= Input'Length * 3 is sufficient for all inputs.
---------------------------------------------------------------------------
procedure Titlecase
(Input : Byte_Array;
Output : in out Byte_Array;
Last : out Natural;
Status : out Case_Status)
with Pre => Initialized
and then Input'Length >= 1
and then Output'Length >= 1
and then Input'First = 1
and then Input'Last < Positive'Last
and then Output'Last < Positive'Last
and then Output'Length <= Max_Out_Acc
and then Properties.Initialized,
Post => (if Status = Success then
Last in Output'First .. Output'Last
and then Last - Output'First + 1 =
Ghost_Title_Total (Input)
else
Last = Output'First - 1),
Always_Terminates;
---------------------------------------------------------------------------
-- Casefold
--
-- Map each character in Input to its full case fold.
-- For caseless matching (D144): toCasefold(X) = toCasefold(Y).
-- Output'Length >= Input'Length * 3 is sufficient for all inputs.
---------------------------------------------------------------------------
procedure Casefold
(Input : Byte_Array;
Output : in out Byte_Array;
Last : out Natural;
Status : out Case_Status)
with Pre => Initialized
and then Input'Length >= 1
and then Output'Length >= 1
and then Input'Last < Positive'Last
and then Output'Last < Positive'Last
and then Output'Length <= Max_Out_Acc,
Post => (if Status = Success then
Last in Output'First .. Output'Last
and then Last - Output'First + 1 =
Ghost_Fold_Total (Input)
else
Last = Output'First - 1),
Always_Terminates;
---------------------------------------------------------------------------
-- Direct property access
---------------------------------------------------------------------------
-- D135: Cased — has Lowercase or Uppercase property, or GC = Lt
function Is_Cased (CP : Codepoint) return Boolean
with Pre => Initialized,
Global => Case_State;
-- D136: Case_Ignorable — WBP in {MidLetter, MidNumLet, Single_Quote}
-- or GC in {Mn, Me, Cf, Lm, Sk}
function Is_Case_Ignorable (CP : Codepoint) return Boolean
with Pre => Initialized,
Global => Case_State;
---------------------------------------------------------------------------
-- Mapping accessor functions
--
-- Abstractly expose the per-codepoint mapping table structure.
-- These are expression functions in the body (where tables are visible).
-- Ghost expression functions reference these to compute expected output.
---------------------------------------------------------------------------
-- Number of mapped codepoints for Uppercase mapping.
-- Returns 1 for self-mapping, or the table entry length (1..3).
function Get_Upper_Map_Len (CP : Codepoint) return Natural
with Pre => Initialized,
Global => Case_State;
-- The Idx-th mapped codepoint for Uppercase (1-based).
-- For self-mapping, always returns CP.
function Get_Upper_Map_CP (CP : Codepoint; Idx : Positive) return Codepoint
with Pre => Initialized
and then Idx <= Get_Upper_Map_Len (CP)
and then Get_Upper_Map_Len (CP) >= 1,
Global => Case_State;
-- Number of mapped codepoints for Casefold mapping.
function Get_Fold_Map_Len (CP : Codepoint) return Natural
with Pre => Initialized,
Global => Case_State;
-- The Idx-th mapped codepoint for Casefold (1-based).
function Get_Fold_Map_CP (CP : Codepoint; Idx : Positive) return Codepoint
with Pre => Initialized
and then Idx <= Get_Fold_Map_Len (CP)
and then Get_Fold_Map_Len (CP) >= 1,
Global => Case_State;
-- Number of mapped codepoints for Lowercase mapping.
function Get_Lower_Map_Len (CP : Codepoint) return Natural
with Pre => Initialized,
Global => Case_State;
-- The Idx-th mapped codepoint for Lowercase (1-based).
function Get_Lower_Map_CP (CP : Codepoint; Idx : Positive) return Codepoint
with Pre => Initialized
and then Idx <= Get_Lower_Map_Len (CP)
and then Get_Lower_Map_Len (CP) >= 1,
Global => Case_State;
-- Number of mapped codepoints for Titlecase mapping.
function Get_Title_Map_Len (CP : Codepoint) return Natural
with Pre => Initialized,
Global => Case_State;
-- The Idx-th mapped codepoint for Titlecase (1-based).
function Get_Title_Map_CP (CP : Codepoint; Idx : Positive) return Codepoint
with Pre => Initialized
and then Idx <= Get_Title_Map_Len (CP)
and then Get_Title_Map_Len (CP) >= 1,
Global => Case_State;
---------------------------------------------------------------------------
-- Ghost helper functions
--
-- Mirror the runtime decode + mapping logic as expression functions
-- so the solver can unfold them.
---------------------------------------------------------------------------
-- Step length at position Cur (same pattern as segmentation modules).
function Ghost_Step_Length
(Input : Byte_Array;
Cur : Positive) return Positive
is (if UTF8_Spec.Well_Formed_At (Input, Cur)
then UTF8_Spec.Lead_Length (Input (Cur))
else 1)
with Ghost,
Pre => Input'Last < Positive'Last
and then Cur in Input'Range;
-- Well-formedness at Cur.
function Ghost_Valid
(Input : Byte_Array;
Cur : Positive) return Boolean
is (UTF8_Spec.Well_Formed_At (Input, Cur))
with Ghost,
Pre => Input'Last < Positive'Last
and then Cur in Input'Range;
-- Decoded codepoint at Cur.
function Ghost_CP
(Input : Byte_Array;
Cur : Positive) return Codepoint
is (if UTF8_Spec.Well_Formed_At (Input, Cur)
then UTF8_Spec.Decoded_At (Input, Cur)
else 0)
with Ghost,
Pre => Input'Last < Positive'Last
and then Cur in Input'Range;
---------------------------------------------------------------------------
-- Ghost output byte count for one codepoint's mapping
--
-- Sum of Encoded_Length for each mapped codepoint.
-- Max_Mapping_Len = 3, so we handle 1, 2, 3 cases explicitly.
---------------------------------------------------------------------------
function Ghost_Upper_Out_Bytes (CP : Codepoint) return Positive
is (case Get_Upper_Map_Len (CP) is
when 1 =>
UTF8_Spec.Encoded_Length (Get_Upper_Map_CP (CP, 1)),
when 2 =>
UTF8_Spec.Encoded_Length (Get_Upper_Map_CP (CP, 1))
+ UTF8_Spec.Encoded_Length (Get_Upper_Map_CP (CP, 2)),
when 3 =>
UTF8_Spec.Encoded_Length (Get_Upper_Map_CP (CP, 1))
+ UTF8_Spec.Encoded_Length (Get_Upper_Map_CP (CP, 2))
+ UTF8_Spec.Encoded_Length (Get_Upper_Map_CP (CP, 3)),
when others =>
UTF8_Spec.Encoded_Length (CP))
with Ghost,
Global => Case_State,
Pre => Initialized;
function Ghost_Fold_Out_Bytes (CP : Codepoint) return Positive
is (case Get_Fold_Map_Len (CP) is
when 1 =>
UTF8_Spec.Encoded_Length (Get_Fold_Map_CP (CP, 1)),
when 2 =>
UTF8_Spec.Encoded_Length (Get_Fold_Map_CP (CP, 1))
+ UTF8_Spec.Encoded_Length (Get_Fold_Map_CP (CP, 2)),
when 3 =>
UTF8_Spec.Encoded_Length (Get_Fold_Map_CP (CP, 1))
+ UTF8_Spec.Encoded_Length (Get_Fold_Map_CP (CP, 2))
+ UTF8_Spec.Encoded_Length (Get_Fold_Map_CP (CP, 3)),
when others =>
UTF8_Spec.Encoded_Length (CP))
with Ghost,
Global => Case_State,
Pre => Initialized;
---------------------------------------------------------------------------
-- Ghost output byte count for one codepoint's lowercase mapping
--
-- Greek Capital Sigma (U+03A3) is special: Final_Sigma context determines
-- whether it maps to final sigma (U+03C2) or medial sigma (U+03C3).
-- Both are 2-byte UTF-8 sequences, so the byte count is the same.
-- We use medial sigma (U+03C3) as the reference.
---------------------------------------------------------------------------
function Ghost_Lower_Out_Bytes (CP : Codepoint) return Positive
is (if CP = Case_Mapping_Spec.Greek_Capital_Sigma then
-- Both sigma variants produce 2 bytes
UTF8_Spec.Encoded_Length (Case_Mapping_Spec.Greek_Small_Sigma)
else
(case Get_Lower_Map_Len (CP) is
when 1 =>
UTF8_Spec.Encoded_Length (Get_Lower_Map_CP (CP, 1)),
when 2 =>
UTF8_Spec.Encoded_Length (Get_Lower_Map_CP (CP, 1))
+ UTF8_Spec.Encoded_Length (Get_Lower_Map_CP (CP, 2)),
when 3 =>
UTF8_Spec.Encoded_Length (Get_Lower_Map_CP (CP, 1))
+ UTF8_Spec.Encoded_Length (Get_Lower_Map_CP (CP, 2))
+ UTF8_Spec.Encoded_Length (Get_Lower_Map_CP (CP, 3)),
when others =>
UTF8_Spec.Encoded_Length (CP)))
with Ghost,
Global => Case_State,
Pre => Initialized;
---------------------------------------------------------------------------
-- Ghost output byte count for one codepoint's plain lowercase mapping
--
-- Unlike Ghost_Lower_Out_Bytes (which has a special case for sigma),
-- this uses the lower table directly for ALL codepoints. Used by
-- Titlecase, which does not apply Final_Sigma context.
---------------------------------------------------------------------------
function Ghost_Plain_Lower_Bytes (CP : Codepoint) return Positive
is (case Get_Lower_Map_Len (CP) is
when 1 =>
UTF8_Spec.Encoded_Length (Get_Lower_Map_CP (CP, 1)),
when 2 =>
UTF8_Spec.Encoded_Length (Get_Lower_Map_CP (CP, 1))
+ UTF8_Spec.Encoded_Length (Get_Lower_Map_CP (CP, 2)),
when 3 =>
UTF8_Spec.Encoded_Length (Get_Lower_Map_CP (CP, 1))
+ UTF8_Spec.Encoded_Length (Get_Lower_Map_CP (CP, 2))
+ UTF8_Spec.Encoded_Length (Get_Lower_Map_CP (CP, 3)),
when others =>
UTF8_Spec.Encoded_Length (CP))
with Ghost,
Global => Case_State,
Pre => Initialized;
---------------------------------------------------------------------------
-- Ghost output byte count for one codepoint's titlecase mapping
---------------------------------------------------------------------------
function Ghost_Title_Out_Bytes (CP : Codepoint) return Positive
is (case Get_Title_Map_Len (CP) is
when 1 =>
UTF8_Spec.Encoded_Length (Get_Title_Map_CP (CP, 1)),
when 2 =>
UTF8_Spec.Encoded_Length (Get_Title_Map_CP (CP, 1))
+ UTF8_Spec.Encoded_Length (Get_Title_Map_CP (CP, 2)),
when 3 =>
UTF8_Spec.Encoded_Length (Get_Title_Map_CP (CP, 1))
+ UTF8_Spec.Encoded_Length (Get_Title_Map_CP (CP, 2))
+ UTF8_Spec.Encoded_Length (Get_Title_Map_CP (CP, 3)),
when others =>
UTF8_Spec.Encoded_Length (CP))
with Ghost,
Global => Case_State,
Pre => Initialized;
---------------------------------------------------------------------------
-- Ghost per-CP byte count within a word segment for titlecase.
--
-- Before the first Cased character: pass-through (Encoded_Length).
-- First Cased character: title mapping (Ghost_Title_Out_Bytes).
-- After first Cased: lowercase mapping (Ghost_Lower_Out_Bytes).
--
-- Note: the Titlecase body does NOT apply Final_Sigma for subsequent
-- lowercase characters — it uses the plain lower table. For sigma,
-- Ghost_Lower_Out_Bytes returns Encoded_Length(U+03C3) = 2, which
-- matches Map_Written_Bytes with the lower table (also 2).
---------------------------------------------------------------------------
function Ghost_Title_CP_Bytes
(CP : Codepoint; Found_Cased : Boolean) return Positive
is (if not Found_Cased and then Is_Cased (CP) then
Ghost_Title_Out_Bytes (CP)
elsif Found_Cased then
Ghost_Plain_Lower_Bytes (CP)
else
UTF8_Spec.Encoded_Length (CP))
with Ghost,
Global => Case_State,
Pre => Initialized;
---------------------------------------------------------------------------
-- Recursive ghost functions: simulate the forward transform loop.
--
-- Ghost_Upper_Out(Input, Cur, Acc) returns the total output byte count
-- after processing all codepoints from Cur onward, starting with
-- accumulator Acc.
--
-- Invalid UTF-8 at any position → 0 (failure).
-- At end of input → Acc.
-- Otherwise → decode, add mapping byte count to Acc, advance, recurse.
---------------------------------------------------------------------------
Max_Out_Acc : constant := Natural'Last / 2;
function Ghost_Upper_Out
(Input : Byte_Array;
Cur : Positive;
Acc : Natural) return Natural
is (if Cur not in Input'Range then
-- Past end of input: return accumulated output count
Acc
elsif not Ghost_Valid (Input, Cur) then
-- Invalid UTF-8: return 0 (failure sentinel)
0
elsif Acc > Max_Out_Acc then
-- Overflow guard: return 0
0
elsif Cur > Input'Last - Ghost_Step_Length (Input, Cur) + 1 then
-- Last codepoint: add its output bytes and return
Acc + Ghost_Upper_Out_Bytes (Ghost_CP (Input, Cur))
else
-- More codepoints: add output bytes, advance, recurse
Ghost_Upper_Out
(Input,
Cur + Ghost_Step_Length (Input, Cur),
Acc + Ghost_Upper_Out_Bytes (Ghost_CP (Input, Cur))))
with Ghost,
Global => Case_State,
Pre => Input'Last < Positive'Last
and then Input'Length >= 1
and then Cur > 0
and then Initialized,
Subprogram_Variant => (Decreases => Input'Last - Cur + 1);
function Ghost_Fold_Out
(Input : Byte_Array;
Cur : Positive;
Acc : Natural) return Natural
is (if Cur not in Input'Range then
Acc
elsif not Ghost_Valid (Input, Cur) then
0
elsif Acc > Max_Out_Acc then
0
elsif Cur > Input'Last - Ghost_Step_Length (Input, Cur) + 1 then
Acc + Ghost_Fold_Out_Bytes (Ghost_CP (Input, Cur))
else
Ghost_Fold_Out
(Input,
Cur + Ghost_Step_Length (Input, Cur),
Acc + Ghost_Fold_Out_Bytes (Ghost_CP (Input, Cur))))
with Ghost,
Global => Case_State,
Pre => Input'Last < Positive'Last
and then Input'Length >= 1
and then Cur > 0
and then Initialized,
Subprogram_Variant => (Decreases => Input'Last - Cur + 1);
function Ghost_Lower_Out
(Input : Byte_Array;
Cur : Positive;
Acc : Natural) return Natural
is (if Cur not in Input'Range then
Acc
elsif not Ghost_Valid (Input, Cur) then
0
elsif Acc > Max_Out_Acc then
0
elsif Cur > Input'Last - Ghost_Step_Length (Input, Cur) + 1 then
Acc + Ghost_Lower_Out_Bytes (Ghost_CP (Input, Cur))
else
Ghost_Lower_Out
(Input,
Cur + Ghost_Step_Length (Input, Cur),
Acc + Ghost_Lower_Out_Bytes (Ghost_CP (Input, Cur))))
with Ghost,
Global => Case_State,
Pre => Input'Last < Positive'Last
and then Input'Length >= 1
and then Cur > 0
and then Initialized,
Subprogram_Variant => (Decreases => Input'Last - Cur + 1);
---------------------------------------------------------------------------
-- Recursive ghost function for Titlecase.
--
-- Ghost_Title_Scan processes codepoints one at a time. At word
-- boundaries (detected by Words.Ghost_Break), Found_Cased resets.
-- This is a single-loop recursion that mirrors the body's two-loop
-- structure but avoids the need for Next_WB_From in the definition.
---------------------------------------------------------------------------
---------------------------------------------------------------------------
-- Ghost_Title_Scan: single-codepoint recursion for titlecase.
--
-- Processes codepoints one at a time. At word boundaries (detected by
-- Ghost_Break from the Words module), Found_Cased resets to False.
-- This avoids the need for Next_WB_From in the ghost definition,
-- which the solver cannot easily prove terminates from (variant issue).
--
-- The body Titlecase procedure uses Next_Word_Break for word boundaries,
-- but the ghost function uses Ghost_Break (which is what Next_WB_From
-- is built from). The bridge assertions connect them.
--
-- Parameters:
-- Found_Cased — whether the first Cased char in the current word was seen
-- WB_St — word break state machine state
-- Acc — accumulated output byte count
---------------------------------------------------------------------------
function Ghost_Title_Scan
(Input : Byte_Array;
Cur : Positive;
Found_Cased : Boolean;
WB_St : Words.WB_State;
Acc : Natural) return Natural
is (if Cur not in Input'Range then
Acc
elsif not Ghost_Valid (Input, Cur) then
0
elsif Acc > Max_Out_Acc then
0
elsif Cur > Input'Last - Ghost_Step_Length (Input, Cur) + 1 then
-- Last codepoint: add its output bytes
Acc + Ghost_Title_CP_Bytes
(Ghost_CP (Input, Cur),
(if Words.Ghost_Break (WB_St, Input, Cur)
then False else Found_Cased))
else
-- More codepoints: compute effective Found_Cased, add bytes, recurse
Ghost_Title_Scan
(Input,
Cur + Ghost_Step_Length (Input, Cur),
(if Words.Ghost_Break (WB_St, Input, Cur)
then False else Found_Cased)
or else Is_Cased (Ghost_CP (Input, Cur)),
Words.Updated_State (WB_St, Input, Cur),
Acc + Ghost_Title_CP_Bytes
(Ghost_CP (Input, Cur),
(if Words.Ghost_Break (WB_St, Input, Cur)
then False else Found_Cased))))
with Ghost,
Global => (Case_State, Properties.Property_State),
Pre => Input'First = 1
and then Input'Last >= 1
and then Input'Last < Positive'Last
and then Cur > 0
and then Initialized
and then Properties.Initialized,
Subprogram_Variant => (Decreases => Input'Last - Cur + 1);
---------------------------------------------------------------------------
-- Top-level wrappers
---------------------------------------------------------------------------
function Ghost_Upper_Total (Input : Byte_Array) return Natural
is (Ghost_Upper_Out (Input, Input'First, 0))
with Ghost,
Global => Case_State,
Pre => Input'Last < Positive'Last
and then Input'Length >= 1
and then Initialized;
function Ghost_Fold_Total (Input : Byte_Array) return Natural
is (Ghost_Fold_Out (Input, Input'First, 0))
with Ghost,
Global => Case_State,
Pre => Input'Last < Positive'Last
and then Input'Length >= 1
and then Initialized;
function Ghost_Lower_Total (Input : Byte_Array) return Natural
is (Ghost_Lower_Out (Input, Input'First, 0))
with Ghost,
Global => Case_State,
Pre => Input'Last < Positive'Last
and then Input'Length >= 1
and then Initialized;
-- Ghost_Title_Total: for the first codepoint, there's always a word
-- break (WB1), so Found_Cased starts as False. The WB_State is
-- initialized from the first codepoint but the break decision at
-- position 2+ uses it. At position 1, the first CP is always
-- processed with Found_Cased = False (start of first word).
--
-- The initial WB_State is set to Initial_State(Input, 1) after
-- processing the first CP. The first CP is handled by the ghost
-- function's non-break path (since Ghost_Break is not called for
-- the first position — it's implicitly a word start).
--
-- Actually, in the body, the outer loop calls Next_Word_Break(Input, 1)
-- which returns the end of the first word. The inner loop processes
-- CPs 1..Word_End-1 with Found_Cased starting at False. Ghost_Title_Scan
-- mirrors this by treating the first CP as part of the first word.
-- The Ghost_Break check at position 2+ will detect the boundary.
--
-- For the scan, we need a "dummy" initial WB_State that won't trigger
-- a break at position 1. We use Initial_State(Input, 1) — which is
-- constructed from the first CP and won't trigger Ghost_Break at
-- position 1 because Ghost_Break compares "previous" vs "current".
-- At position 1 there IS an implicit break (WB1), but the ghost scan
-- starts with Found_Cased = False, which is correct for position 1.
--
-- Approach: skip the first CP in the scan setup. Process CP at
-- Input'First directly, then scan from position 2 onward.
function Ghost_Title_First_Bytes (Input : Byte_Array) return Positive
is (Ghost_Title_CP_Bytes (Ghost_CP (Input, Input'First), False))
with Ghost,
Global => Case_State,
Pre => Input'First = 1
and then Input'Last >= 1
and then Input'Last < Positive'Last
and then Initialized;
function Ghost_Title_Total (Input : Byte_Array) return Natural
is (if not Ghost_Valid (Input, Input'First) then
0
elsif Input'First > Input'Last -
Ghost_Step_Length (Input, Input'First) + 1
then
-- Single codepoint: just the first CP's title bytes
Ghost_Title_First_Bytes (Input)
else
Ghost_Title_Scan
(Input,
Input'First + Ghost_Step_Length (Input, Input'First),
Is_Cased (Ghost_CP (Input, Input'First)),
Words.Initial_State (Input, Input'First),
Ghost_Title_First_Bytes (Input)))
with Ghost,
Global => (Case_State, Properties.Property_State),
Pre => Input'First = 1
and then Input'Last >= 1
and then Input'Last < Positive'Last
and then Initialized
and then Properties.Initialized;
end Lingenic_Text.Case_Mapping;