comparison lib/ur/datetime.ur @ 1977:50322ba22972

Add datetime functions for adding time intervals.
author Patrick Hurst <phurst@mit.edu>
date Mon, 09 Dec 2013 19:19:12 -0500
parents 98bb0e952a11
children abb6981a2c4c
comparison
equal deleted inserted replaced
1976:98bb0e952a11 1977:50322ba22972
100 Hour = datetimeHour t, 100 Hour = datetimeHour t,
101 Minute = datetimeMinute t, 101 Minute = datetimeMinute t,
102 Second = datetimeSecond t 102 Second = datetimeSecond t
103 } 103 }
104 104
105 val ord_datetime = mkOrd { Lt = fn a b => toTime a < toTime b,
106 Le = fn a b => toTime a <= toTime b }
107
105 fun format fmt dt : string = timef fmt (toTime dt) 108 fun format fmt dt : string = timef fmt (toTime dt)
106 109
107 fun dayOfWeek dt : day_of_week = 110 fun dayOfWeek dt : day_of_week =
108 case datetimeDayOfWeek (toTime dt) of 111 case datetimeDayOfWeek (toTime dt) of
109 0 => Sunday 112 0 => Sunday
113 | 4 => Thursday 116 | 4 => Thursday
114 | 5 => Friday 117 | 5 => Friday
115 | 6 => Saturday 118 | 6 => Saturday
116 | n => error <xml>Illegal day of week {[n]}</xml> 119 | n => error <xml>Illegal day of week {[n]}</xml>
117 120
118
119 val now : transaction t = 121 val now : transaction t =
120 n <- now; 122 n <- now;
121 return (fromTime n) 123 return (fromTime n)
124
125 (* Normalize a datetime. This will convert, e.g., January 32nd into February
126 1st. *)
127
128 fun normalize dt = fromTime (toTime dt)
129 fun addToField [nm :: Name] [rest ::: {Type}] [[nm] ~ rest]
130 (delta : int) (r : $([nm = int] ++ rest))
131 : $([nm = int] ++ rest) =
132 (r -- nm) ++ {nm = r.nm + delta}
133
134
135 (* Functions for adding to a datetime. There is no addMonths or addYears since
136 it's not clear what should be done; what's 1 month after January 31, or 1
137 year after February 29th?
138
139 These can't all be defined in terms of addSeconds because of leap seconds. *)
140
141 fun addSeconds n dt = normalize (addToField [#Second] n dt)
142 fun addMinutes n dt = normalize (addToField [#Minute] n dt)
143 fun addHours n dt = normalize (addToField [#Hour] n dt)
144 fun addDays n dt = normalize (addToField [#Day] n dt)