66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
|
is record
Variable_Length_Verbatim : Boolean;
Max_Word_Length : Positive;
Offsets : Offset_Array
(Dictionary_Code'Succ (Dictionary_Code'First) .. Last_Code);
Values : String (1 .. Values_Last);
Hash : not null access function (Value : String) return Natural;
end record
with Dynamic_Predicate =>
(for all Code in Dictionary.Offsets'Range
=> Dictionary.Offsets (Code) in Dictionary.Values'Range)
and then (for all Code in Dictionary_Code'First .. Dictionary.Last_Code
=> Code_Last (Dictionary.Offsets, Code, Dictionary.Values'Last) + 1
- Code_First (Dictionary.Offsets, Code, Dictionary.Values'First)
in 1 .. Dictionary.Max_Word_Length);
function Code_First
(Offsets : in Offset_Array;
Code : in Dictionary_Code;
Fallback : in Positive)
return Positive
|
|
<
<
<
<
<
<
<
|
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
|
is record
Variable_Length_Verbatim : Boolean;
Max_Word_Length : Positive;
Offsets : Offset_Array
(Dictionary_Code'Succ (Dictionary_Code'First) .. Last_Code);
Values : String (1 .. Values_Last);
Hash : not null access function (Value : String) return Natural;
end record;
function Code_First
(Offsets : in Offset_Array;
Code : in Dictionary_Code;
Fallback : in Positive)
return Positive
|