phurst@1974
|
1 datatype day_of_week = Sunday | Monday | Tuesday | Wednesday | Thursday |
|
phurst@1974
|
2 Friday | Saturday
|
phurst@1974
|
3
|
phurst@1974
|
4 val show_day_of_week = mkShow (fn dow => case dow of
|
phurst@1974
|
5 Sunday => "Sunday"
|
phurst@1974
|
6 | Monday => "Monday"
|
phurst@1974
|
7 | Tuesday => "Tuesday"
|
phurst@1974
|
8 | Wednesday => "Wednesday"
|
phurst@1974
|
9 | Thursday => "Thursday"
|
phurst@1974
|
10 | Friday => "Friday"
|
phurst@1974
|
11 | Saturday => "Saturday")
|
phurst@1974
|
12
|
phurst@1974
|
13 fun dayOfWeekToInt dow = case dow of
|
phurst@1974
|
14 Sunday => 0
|
phurst@1974
|
15 | Monday => 1
|
phurst@1974
|
16 | Tuesday => 2
|
phurst@1974
|
17 | Wednesday => 3
|
phurst@1974
|
18 | Thursday => 4
|
phurst@1974
|
19 | Friday => 5
|
phurst@1974
|
20 | Saturday => 6
|
phurst@1974
|
21
|
phurst@1974
|
22 fun intToDayOfWeek i = case i of
|
phurst@1974
|
23 0 => Sunday
|
phurst@1974
|
24 | 1 => Monday
|
phurst@1974
|
25 | 2 => Tuesday
|
phurst@1974
|
26 | 3 => Wednesday
|
phurst@1974
|
27 | 4 => Thursday
|
phurst@1974
|
28 | 5 => Friday
|
phurst@1974
|
29 | 6 => Saturday
|
phurst@1974
|
30 | n => error <xml>Invalid day of week {[n]}</xml>
|
phurst@1974
|
31
|
phurst@1974
|
32 val eq_day_of_week = mkEq (fn a b => dayOfWeekToInt a = dayOfWeekToInt b)
|
phurst@1974
|
33
|
phurst@1974
|
34
|
phurst@1974
|
35 datatype month = January | February | March | April | May | June | July |
|
phurst@1974
|
36 August | September | October | November | December
|
phurst@1974
|
37
|
phurst@1974
|
38 val show_month = mkShow (fn m => case m of
|
phurst@1974
|
39 January => "January"
|
phurst@1974
|
40 | February => "February"
|
phurst@1974
|
41 | March => "March"
|
phurst@1974
|
42 | April => "April"
|
phurst@1974
|
43 | May => "May"
|
phurst@1974
|
44 | June => "June"
|
phurst@1974
|
45 | July => "July"
|
phurst@1974
|
46 | August => "August"
|
phurst@1974
|
47 | September => "September"
|
phurst@1974
|
48 | October => "October"
|
phurst@1974
|
49 | November => "November"
|
phurst@1974
|
50 | December => "December")
|
phurst@1974
|
51
|
phurst@1974
|
52 type t = {
|
phurst@1972
|
53 Year : int,
|
phurst@1974
|
54 Month : month,
|
phurst@1972
|
55 Day : int,
|
phurst@1972
|
56 Hour : int,
|
phurst@1972
|
57 Minute : int,
|
phurst@1972
|
58 Second : int
|
phurst@1972
|
59 }
|
phurst@1972
|
60
|
phurst@1974
|
61 fun monthToInt m = case m of
|
phurst@1974
|
62 January => 0
|
phurst@1974
|
63 | February => 1
|
phurst@1974
|
64 | March => 2
|
phurst@1974
|
65 | April => 3
|
phurst@1974
|
66 | May => 4
|
phurst@1974
|
67 | June => 5
|
phurst@1974
|
68 | July => 6
|
phurst@1974
|
69 | August => 7
|
phurst@1974
|
70 | September => 8
|
phurst@1974
|
71 | October => 9
|
phurst@1974
|
72 | November => 10
|
phurst@1974
|
73 | December => 11
|
phurst@1973
|
74
|
phurst@1974
|
75 fun intToMonth i = case i of
|
phurst@1974
|
76 0 => January
|
phurst@1974
|
77 | 1 => February
|
phurst@1974
|
78 | 2 => March
|
phurst@1974
|
79 | 3 => April
|
phurst@1974
|
80 | 4 => May
|
phurst@1974
|
81 | 5 => June
|
phurst@1974
|
82 | 6 => July
|
phurst@1974
|
83 | 7 => August
|
phurst@1974
|
84 | 8 => September
|
phurst@1974
|
85 | 9 => October
|
phurst@1974
|
86 | 10 => November
|
phurst@1974
|
87 | 11 => December
|
phurst@1974
|
88 | n => error <xml>Invalid month number {[n]}</xml>
|
phurst@1973
|
89
|
phurst@1974
|
90 val eq_month = mkEq (fn a b => monthToInt a = monthToInt b)
|
phurst@1974
|
91
|
phurst@1974
|
92
|
phurst@1974
|
93 fun toTime dt : time = fromDatetime dt.Year (monthToInt dt.Month) dt.Day
|
phurst@1972
|
94 dt.Hour dt.Minute dt.Second
|
phurst@1972
|
95
|
phurst@1976
|
96 fun fromTime t : t = {
|
phurst@1972
|
97 Year = datetimeYear t,
|
phurst@1974
|
98 Month = intToMonth (datetimeMonth t),
|
phurst@1972
|
99 Day = datetimeDay t,
|
phurst@1972
|
100 Hour = datetimeHour t,
|
phurst@1972
|
101 Minute = datetimeMinute t,
|
phurst@1972
|
102 Second = datetimeSecond t
|
phurst@1972
|
103 }
|
phurst@1972
|
104
|
phurst@1977
|
105 val ord_datetime = mkOrd { Lt = fn a b => toTime a < toTime b,
|
phurst@1977
|
106 Le = fn a b => toTime a <= toTime b }
|
phurst@1977
|
107
|
phurst@1974
|
108 fun format fmt dt : string = timef fmt (toTime dt)
|
phurst@1974
|
109
|
adam@1988
|
110 fun dayOfWeek dt : day_of_week = intToDayOfWeek (datetimeDayOfWeek (toTime dt))
|
phurst@1974
|
111
|
phurst@1976
|
112 val now : transaction t =
|
phurst@1972
|
113 n <- now;
|
phurst@1972
|
114 return (fromTime n)
|
phurst@1977
|
115
|
phurst@1977
|
116 (* Normalize a datetime. This will convert, e.g., January 32nd into February
|
phurst@1977
|
117 1st. *)
|
phurst@1977
|
118
|
phurst@1977
|
119 fun normalize dt = fromTime (toTime dt)
|
phurst@1977
|
120 fun addToField [nm :: Name] [rest ::: {Type}] [[nm] ~ rest]
|
phurst@1977
|
121 (delta : int) (r : $([nm = int] ++ rest))
|
phurst@1977
|
122 : $([nm = int] ++ rest) =
|
phurst@1977
|
123 (r -- nm) ++ {nm = r.nm + delta}
|
phurst@1977
|
124
|
phurst@1977
|
125
|
phurst@1977
|
126 (* Functions for adding to a datetime. There is no addMonths or addYears since
|
phurst@1977
|
127 it's not clear what should be done; what's 1 month after January 31, or 1
|
phurst@1977
|
128 year after February 29th?
|
phurst@1977
|
129
|
phurst@1977
|
130 These can't all be defined in terms of addSeconds because of leap seconds. *)
|
phurst@1977
|
131
|
phurst@1977
|
132 fun addSeconds n dt = normalize (addToField [#Second] n dt)
|
phurst@1977
|
133 fun addMinutes n dt = normalize (addToField [#Minute] n dt)
|
phurst@1977
|
134 fun addHours n dt = normalize (addToField [#Hour] n dt)
|
phurst@1977
|
135 fun addDays n dt = normalize (addToField [#Day] n dt)
|