CASE MAPPING MODULE
===================
Standard: Unicode Standard, Section 3.13
Files: src/lingenic_text-case_mapping_spec.ads (ghost specification)
src/lingenic_text-case_mapping.ads (public API)
src/lingenic_text-case_mapping.adb (implementation)
PURPOSE
-------
The Case_Mapping module implements default (non-tailored) Unicode 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
GHOST SPECIFICATION (Case_Mapping_Spec)
---------------------------------------
Types:
type Case_Operation is
(Op_Uppercase, Op_Lowercase, Op_Titlecase, Op_Casefold);
Constants:
Max_Mapping_Len = 3
SpecialCasing.txt produces at most 3 codepoints per mapping.
Max_Pending = 32
Buffer for Final_Sigma context detection.
Greek_Capital_Sigma = 16#03A3#
Greek_Small_Sigma = 16#03C3# (medial sigma)
Greek_Final_Sigma = 16#03C2# (final sigma)
Final_Sigma Context (Unicode Standard, Section 3.13):
Capital Sigma maps to:
- Final sigma (U+03C2) if preceded by cased character AND not
followed by cased character
- Medial sigma (U+03C3) otherwise
Both conditions ignore intervening Case_Ignorable characters.
Is_Final_Sigma(Prev_Was_Cased, Followed_By_Cased):
True iff Prev_Was_Cased and not Followed_By_Cased.
INITIALIZATION
--------------
procedure Initialize
(UCD_Dir : String;
Success : out Boolean);
Pre: Properties.Initialized
Post: if Success then Initialized
Reads from UCD_Dir:
UnicodeData.txt Simple case mappings (fields 12/13/14)
SpecialCasing.txt Full multi-character mappings (unconditional)
CaseFolding.txt Case folding (status C and F for full)
DerivedCoreProperties.txt Uppercase, Lowercase boolean properties
Builds internal data tables:
Upper_Index/Data Per-codepoint uppercase mapping (1-3 codepoints)
Lower_Index/Data Per-codepoint lowercase mapping (1-3 codepoints)
Title_Index/Data Per-codepoint titlecase mapping (1-3 codepoints)
Fold_Index/Data Per-codepoint case fold mapping (1-3 codepoints)
Is_Cased_Table D135: has Uppercase/Lowercase property or GC=Lt
Is_Case_Ignorable_Table D136: WBP/GC classification
PUBLIC API
----------
Uppercase:
procedure Uppercase
(Input : Byte_Array;
Output : in out Byte_Array;
Last : out Natural;
Status : out Case_Status);
Pre: Initialized, Input'Length >= 1, Output'Length >= 1
Output'Length <= Max_Out_Acc
Post: if Success then
Last in Output'First..Output'Last
Last - Output'First + 1 = Ghost_Upper_Total(Input)
else
Last = Output'First - 1
Maps each character to its full uppercase mapping.
Output'Length >= Input'Length * 3 is sufficient for all inputs.
Lowercase:
procedure Lowercase
(Input : Byte_Array;
Output : in out Byte_Array;
Last : out Natural;
Status : out Case_Status);
Post: if Success then
Last - Output'First + 1 = Ghost_Lower_Total(Input)
Maps each character to its full lowercase mapping.
Handles Final_Sigma: Greek Capital Sigma (U+03A3) maps to final sigma
(U+03C2) or medial sigma (U+03C3) depending on context.
The implementation buffers sigma + trailing Case_Ignorable characters
during processing, resolving to final or medial sigma when the
following context (cased or not) becomes clear.
Titlecase:
procedure Titlecase
(Input : Byte_Array;
Output : in out Byte_Array;
Last : out Natural;
Status : out Case_Status);
Pre: additionally requires Properties.Initialized and Input'First = 1
Post: if Success then
Last - Output'First + 1 = Ghost_Title_Total(Input)
For each word (per UAX #29 word boundaries):
- Characters before the first cased character pass through unchanged
- The first cased character maps to its titlecase mapping
- All subsequent characters map to lowercase
Uses Next_Word_Break from the Words module to detect word boundaries.
Does NOT apply Final_Sigma for the lowercase portion.
Casefold:
procedure Casefold
(Input : Byte_Array;
Output : in out Byte_Array;
Last : out Natural;
Status : out Case_Status);
Post: if Success then
Last - Output'First + 1 = Ghost_Fold_Total(Input)
Maps each character to its full case fold (D144).
For caseless comparison: toCasefold(X) = toCasefold(Y).
Status values:
Success Mapping completed
Buffer_Overflow Output buffer too small
Invalid_Input Input contains invalid UTF-8
PROPERTY ACCESS
---------------
Is_Cased(CP) -> Boolean
D135: CP has Lowercase or Uppercase property, or GC = Lt.
Is_Case_Ignorable(CP) -> Boolean
D136: WBP in {MidLetter, MidNumLet, Single_Quote} or
GC in {Mn, Me, Cf, Lm, Sk}.
Get_Upper_Map_Len(CP) -> Natural
Get_Upper_Map_CP(CP, Idx) -> Codepoint
Length and Idx-th codepoint of the uppercase mapping.
Get_Lower_Map_Len(CP) / Get_Lower_Map_CP(CP, Idx)
Get_Title_Map_Len(CP) / Get_Title_Map_CP(CP, Idx)
Get_Fold_Map_Len(CP) / Get_Fold_Map_CP(CP, Idx)
Same pattern for each mapping direction.
GHOST OUTPUT BYTE COUNTS
-------------------------
The postconditions prove the exact output byte count:
Ghost_Upper_Out_Bytes(CP) Sum of Encoded_Length for uppercase mapping
Ghost_Lower_Out_Bytes(CP) Sum for lowercase (special case for sigma)
Ghost_Title_Out_Bytes(CP) Sum for titlecase mapping
Ghost_Fold_Out_Bytes(CP) Sum for casefold mapping
Ghost_Plain_Lower_Bytes(CP) Sum for plain lowercase (no Final_Sigma)
Ghost_Title_CP_Bytes(CP, Found_Cased)
Per-codepoint byte count within a word segment:
- Before first Cased: pass-through (Encoded_Length)
- First Cased: title mapping bytes
- After first Cased: lowercase mapping bytes
Recursive ghost functions accumulate the total:
Ghost_Upper_Out(Input, Cur, Acc) -> total uppercase output bytes
Ghost_Lower_Out(Input, Cur, Acc) -> total lowercase output bytes
Ghost_Fold_Out(Input, Cur, Acc) -> total casefold output bytes
Ghost_Title_Scan(Input, Cur, Found_Cased, WB_St, Acc) -> total titlecase
Top-level wrappers:
Ghost_Upper_Total(Input) = Ghost_Upper_Out(Input, Input'First, 0)
Ghost_Lower_Total(Input) = Ghost_Lower_Out(Input, Input'First, 0)
Ghost_Fold_Total(Input) = Ghost_Fold_Out(Input, Input'First, 0)
Ghost_Title_Total(Input) = first CP bytes + Ghost_Title_Scan(rest)
CONSTANTS
---------
Max_Out_Acc = Natural'Last / 2 Max output accumulator value