25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
|
-- This means a second granularity can be achieved with 7 characters. The --
-- most compact way of encoding such a timestamp would be counting seconds, --
-- like UNIX time. The time covered by this format is rought 2^37 seconds, --
-- which would mean 5 bytes or 7 base-64 digits (though 6 would be enough --
-- for a useful time range). --
------------------------------------------------------------------------------
with Ada.Calendar;
package Natools.Time_Keys is
function Is_Valid (Key : String) return Boolean;
-- Check whether Key is a valid encoded time.
-- WARNING: this function returns true for invalid dates,
-- like February 30th.
function To_Key
(Time : Ada.Calendar.Time;
Max_Sub_Second_Digits : in Natural := 120)
return String
with Post => Is_Valid (To_Key'Result);
-- Convert a time into a key
function To_Time (Key : String) return Ada.Calendar.Time
with Pre => Is_Valid (Key);
-- Convert a valid key into the original time
private
subtype Base_64_Digit is Character with Static_Predicate
|
|
>
>
>
>
>
>
>
>
>
>
>
>
>
>
|
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
|
-- This means a second granularity can be achieved with 7 characters. The --
-- most compact way of encoding such a timestamp would be counting seconds, --
-- like UNIX time. The time covered by this format is rought 2^37 seconds, --
-- which would mean 5 bytes or 7 base-64 digits (though 6 would be enough --
-- for a useful time range). --
------------------------------------------------------------------------------
with Ada.Calendar.Formatting;
package Natools.Time_Keys is
function Is_Valid (Key : String) return Boolean;
-- Check whether Key is a valid encoded time.
-- WARNING: this function returns true for invalid dates,
-- like February 30th.
function To_Key
(Time : Ada.Calendar.Time;
Max_Sub_Second_Digits : in Natural := 120)
return String
with Post => Is_Valid (To_Key'Result);
-- Convert a time into a key
function To_Key
(Year : Ada.Calendar.Year_Number;
Month : Ada.Calendar.Month_Number;
Day : Ada.Calendar.Day_Number;
Hour : Ada.Calendar.Formatting.Hour_Number := 0;
Minute : Ada.Calendar.Formatting.Minute_Number := 0;
Second : Ada.Calendar.Formatting.Second_Number := 0;
Sub_Second : Ada.Calendar.Formatting.Second_Duration := 0.0;
Leap_Second : Boolean := False;
Max_Sub_Second_Digits : Natural := 120)
return String
with Post => Is_Valid (To_Key'Result);
-- Convert a split time representation into a key
function To_Time (Key : String) return Ada.Calendar.Time
with Pre => Is_Valid (Key);
-- Convert a valid key into the original time
private
subtype Base_64_Digit is Character with Static_Predicate
|