time.anubis
3.53 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
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
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
read bool.anubis
read string.anubis
*** (11) Time
*** (11.1) Time conversions.
public define Int year(Int t) = year(convert_time(t)).
public define Int month(Int t) = month(convert_time(t)).
public define Int day(Int t) = day(convert_time(t)).
public define Int hour(Int t) = hour(convert_time(t)).
public define Int minute(Int t) = minute(convert_time(t)).
public define Int second(Int t) = second(convert_time(t)).
public define Int week_day(Int t) = week_day(convert_time(t)).
public define Int year_day(Int t) = year_day(convert_time(t)).
public define Bool daylight_saving_time(Int t) = daylight_saving_time(convert_time(t)).
public define Int
date_and_time
(
Int y,
Int mo,
Int d,
Int h,
Int mi,
Int s,
Bool dst
) =
convert_time(date_and_time(y,mo,d,h,mi,s,0,0,dst)).
*** (11.2) Calculations with UTime.
A datum of type 'UTime' is a pair 'utime(s,m)' of two 'Int's. Such a pair is in
'normal form' if either:
- s >= 0 and 0 =< m < 10^6
- s =< 0 and -10^6 < m =< 0
Notice that 'utime(s,m)' represents always '(10^6)s + m' microseconds even if it is not
in normal form, and regardless of the signs of 's' and 'm'.
All our fonctions below assume that their arguments are in normal form, and (under this
assumption) return results in normal form.
define UTime
normalize
(
Int s,
Int m
) =
if m >= 1000000 then normalize(s+1,m-1000000)
else if m > 0 & s < 0 then normalize(s+1,m-1000000)
else if m < 0 & s > 0 then normalize(s-1,m+1000000)
else if m =< -1000000 then normalize(s-1,m+1000000)
else utime(s,m).
public define UTime
normalize
(
UTime u
) =
if u is utime(s,m) then normalize(s,m).
public define Bool
UTime u1 < UTime u2
=
if normalize(u1) is utime(s1,m1) then
if normalize(u2) is utime(s2,m2) then
if s1 < s2 then true else
if s1 = s2 then m1 < m2 else
false.
public define Bool
UTime u1 =< UTime u2
=
if normalize(u1) is utime(s1,m1) then
if normalize(u2) is utime(s2,m2) then
if s1 =< s2 then true else
if s1 = s2 then m1 =< m2 else
false.
public define UTime
UTime u1 - UTime u2
=
if u1 is utime(s1,m1) then
if u2 is utime(s2,m2) then
normalize(s1-s2,m1-m2).
public define UTime
UTime u1 + UTime u2
=
if u1 is utime(s1,m1) then
if u2 is utime(s2,m2) then
normalize(s1+s2,m1+m2).
public define String
show_duration_string
(
String comment,
UTime start
)=
with duration = unow - start, //compute the duration of the function
//print the duration and comment
comment + " duration = "+seconds(duration)+"."+microseconds(duration)+" seconds".
public define One
show_duration
(
String comment,
UTime start
)=
//print the duration and comment
println(show_duration_string(comment, start)).
*** (8) Putting a virtual machine at bed.
The next function forces the virtual machine to sleep during a number of
milliseconds. This works because the virtual machine waits 'ms' milliseconds before
computing 'true' for the first time. Since 'true' is always 'satisfied', the function
returns 'unique' immediatly after this first computation of 'true'.
public define One
sleep
(
Int ms // number of milliseconds to sleep
) =
checking every truncate_to_Word32(ms) milliseconds, wait for true then unique.