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
|
datatype day_of_week = Sunday | Monday | Tuesday | Wednesday | Thursday |
Friday | Saturday
val show_day_of_week = mkShow (fn dow => case dow of
Sunday => "Sunday"
| Monday => "Monday"
| Tuesday => "Tuesday"
| Wednesday => "Wednesday"
| Thursday => "Thursday"
| Friday => "Friday"
| Saturday => "Saturday")
fun dayOfWeekToInt dow = case dow of
Sunday => 0
| Monday => 1
| Tuesday => 2
| Wednesday => 3
| Thursday => 4
| Friday => 5
| Saturday => 6
fun intToDayOfWeek i = case i of
0 => Sunday
| 1 => Monday
| 2 => Tuesday
| 3 => Wednesday
| 4 => Thursday
| 5 => Friday
| 6 => Saturday
| n => error <xml>Invalid day of week {[n]}</xml>
val eq_day_of_week = mkEq (fn a b => dayOfWeekToInt a = dayOfWeekToInt b)
datatype month = January | February | March | April | May | June | July |
August | September | October | November | December
val show_month = mkShow (fn m => case m of
January => "January"
| February => "February"
| March => "March"
| April => "April"
| May => "May"
| June => "June"
| July => "July"
| August => "August"
| September => "September"
| October => "October"
| November => "November"
| December => "December")
type t = {
Year : int,
Month : month,
Day : int,
Hour : int,
Minute : int,
Second : int
}
fun monthToInt m = case m of
January => 0
| February => 1
| March => 2
| April => 3
| May => 4
| June => 5
| July => 6
| August => 7
| September => 8
| October => 9
| November => 10
| December => 11
fun intToMonth i = case i of
0 => January
| 1 => February
| 2 => March
| 3 => April
| 4 => May
| 5 => June
| 6 => July
| 7 => August
| 8 => September
| 9 => October
| 10 => November
| 11 => December
| n => error <xml>Invalid month number {[n]}</xml>
val eq_month = mkEq (fn a b => monthToInt a = monthToInt b)
fun toTime dt : time = fromDatetime dt.Year (monthToInt dt.Month) dt.Day
dt.Hour dt.Minute dt.Second
fun fromTime t : t = {
Year = datetimeYear t,
Month = intToMonth (datetimeMonth t),
Day = datetimeDay t,
Hour = datetimeHour t,
Minute = datetimeMinute t,
Second = datetimeSecond t
}
val ord_datetime = mkOrd { Lt = fn a b => toTime a < toTime b,
Le = fn a b => toTime a <= toTime b }
fun format fmt dt : string = timef fmt (toTime dt)
fun dayOfWeek dt : day_of_week = intToDayOfWeek (datetimeDayOfWeek (toTime dt))
val now : transaction t =
n <- now;
return (fromTime n)
(* Normalize a datetime. This will convert, e.g., January 32nd into February
1st. *)
fun normalize dt = fromTime (toTime dt)
fun addToField [nm :: Name] [rest ::: {Type}] [[nm] ~ rest]
(delta : int) (r : $([nm = int] ++ rest))
: $([nm = int] ++ rest) =
(r -- nm) ++ {nm = r.nm + delta}
(* Functions for adding to a datetime. There is no addMonths or addYears since
it's not clear what should be done; what's 1 month after January 31, or 1
year after February 29th?
These can't all be defined in terms of addSeconds because of leap seconds. *)
fun addSeconds n dt = normalize (addToField [#Second] n dt)
fun addMinutes n dt = normalize (addToField [#Minute] n dt)
fun addHours n dt = normalize (addToField [#Hour] n dt)
fun addDays n dt = normalize (addToField [#Day] n dt)
|
