PROPERTIES MODULE
=================
Standard: UAX #44 (Unicode Character Database)
Files: src/lingenic_text-properties_spec.ads (ghost: Joining_Type values)
src/lingenic_text-properties.ads (public API)
src/lingenic_text-properties.adb (implementation)
PURPOSE
-------
The Properties module provides O(1) lookup for Unicode character
properties across all 1,114,112 codepoints. Tables are populated at
runtime by reading UCD files from disk and parsing them with the proved
UCD parser.
All lookups are flat array accesses indexed by codepoint -- no trees,
no hash tables, fully deterministic.
INITIALIZATION
--------------
procedure Initialize
(UCD_Dir : String;
Success : out Boolean);
Post: if Success then Initialized
Reads the following UCD files from UCD_Dir:
Scripts.txt Script property (UAX #24)
ScriptExtensions.txt Script extensions (UAX #24)
GraphemeBreakProperty.txt Grapheme_Cluster_Break (UAX #29)
WordBreakProperty.txt Word_Break (UAX #29)
SentenceBreakProperty.txt Sentence_Break (UAX #29)
LineBreak.txt Line_Break (UAX #14)
EastAsianWidth.txt East_Asian_Width (UAX #11)
DerivedBidiClass.txt Bidi_Class (UAX #9)
DerivedGeneralCategory.txt General_Category (UAX #44)
DerivedJoiningType.txt Joining_Type (UAX #44)
DerivedCoreProperties.txt Multiple derived properties
After initialization, all property accessors are available.
PROPERTY ACCESSORS
------------------
All accessors require Properties.Initialized as a precondition.
Script (UAX #24):
Get_Script(CP) -> Property_Index
Returns the Script property index for CP.
Script_Name_Count -> Property_Index
Number of known script names.
Script_Name(Idx) -> String
Human-readable name for a script index.
Pre: Idx in 1..Script_Name_Count.
Script Extensions (UAX #24):
Is_In_Script_Extensions(CP, Script_Idx) -> Boolean
Full UAX #24 semantics:
- If ScriptExtensions.txt covers CP, tests membership in its set
- If not covered, tests (Script_Idx = Get_Script(CP))
Get_Script_Extension_Count(CP) -> Scx_Member_Count
Number of scripts in the extension set (1 if not in ScriptExtensions.txt).
Get_Script_Extension(CP, K) -> Property_Index
K-th script in the extension set (1-indexed).
Pre: K in 1..Get_Script_Extension_Count(CP).
Grapheme_Cluster_Break (UAX #29):
Get_GBP(CP) -> Property_Index
Raw GBP index for CP.
GBP_Name(Idx) -> String
Name of a GBP value.
GBP_To_Abstract(Idx) -> GBP_Value
Map runtime index to the abstract value used in ghost specifications.
Returns GBP_Other for unrecognized indices.
Extended_Pictographic (UTS #51):
Get_ExtPict(CP) -> Boolean
True if CP has the Extended_Pictographic property.
Indic_Conjunct_Break (UAX #44):
Get_InCB(CP) -> Property_Index
Raw InCB index for CP.
InCB_To_Abstract(Idx) -> InCB_Value
Map to abstract value. Returns InCB_None for unrecognized.
Word_Break (UAX #29):
Get_WBP(CP) -> Property_Index
WBP_Name(Idx) -> String
WBP_To_Abstract(Idx) -> WBP_Value
Same pattern as GBP. Returns WBP_Other for unrecognized.
Sentence_Break (UAX #29):
Get_SBP(CP) -> Property_Index
SBP_Name(Idx) -> String
SBP_To_Abstract(Idx) -> SBP_Value
Returns SBP_Other for unrecognized.
East_Asian_Width (UAX #11):
Get_EAW(CP) -> Property_Index
EAW_Name(Idx) -> String
EAW_To_Abstract(Idx) -> EAW_Value
Returns EAW_Neutral for unrecognized.
Line_Break (UAX #14):
Get_LBP(CP) -> LBP_Value
Returns the RESOLVED Line_Break class directly (after LB1 resolution,
QU/OP/CP splits by General_Category and East_Asian_Width).
The raw LB index is not exposed.
General_Category (UAX #44):
Get_GC(CP) -> Property_Index
GC_Name(Idx) -> String
Bidi_Class (UAX #9):
Get_BC(CP) -> BC_Value
Returns the RESOLVED Bidi_Class directly (with block-specific
@missing defaults applied for RTL scripts, Arabic, and Currency
Symbols).
Joining_Type (UAX #44):
Get_JT(CP) -> JT_Value
Returns the Joining_Type. Default is JT_U (Non_Joining).
Bidi_Mirrored (UAX #9):
Get_Bidi_Mirrored(CP) -> Boolean
True if the character's glyph should be mirrored in RTL context.
Identifier Properties (UAX #31):
Get_XID_Start(CP) -> Boolean
True if CP can start a Unicode identifier.
Get_XID_Continue(CP) -> Boolean
True if CP can continue a Unicode identifier.
ABSTRACT VALUE MAPPING
----------------------
The *_To_Abstract functions map runtime-discovered property indices
(which depend on the order values appear in UCD files) to fixed abstract
constants used in ghost specifications.
For example, GBP_To_Abstract maps the runtime index for "CR" (whatever
number it happens to be) to the constant GBP_CR (always 1). This
decoupling allows the ghost specification to use fixed constants while
the runtime system adapts to whatever UCD files provide.
This mapping is established during Initialize by comparing runtime-
discovered value names against known abstract value names.
USAGE BY ALGORITHM MODULES
---------------------------
Algorithm modules call Properties accessors and *_To_Abstract functions
at every codepoint during processing. Since the tables are flat arrays,
each lookup is O(1) with no branching beyond the array index.
The ghost helper functions in algorithm modules (Ghost_GBP, Ghost_WBP,
etc.) compose Properties calls with UTF-8 decoding, giving the solver
a single expression function to unfold when proving postconditions.