1(* Date -- 1995-07-03, 1998-04-07, 1999-08-04 *) 2 3datatype weekday = Mon | Tue | Wed | Thu | Fri | Sat | Sun 4 5datatype month 6 = Jan | Feb | Mar | Apr | May | Jun 7 | Jul | Aug | Sep | Oct | Nov | Dec 8 9datatype date = DATE of { 10 year : int, (* e.g. 1995 *) 11 month : month, 12 day : int, (* 1-31 *) 13 hour : int, (* 0-23 *) 14 minute : int, (* 0-59 *) 15 second : int, (* 0-61 (allowing for leap seconds) *) 16 wday : weekday, 17 yday : int, (* 0-365 *) 18 isDst : bool option, (* daylight savings time in force *) 19 offset : int option (* signed seconds t East of UTC: this 20 zone = UTC+t; ~43200 < t <= 43200 *) 21 } 22 23exception Date 24 25local 26 27 (* 86400 = 24*60*6 is the number of seconds per day *) 28 29 type tmoz = {tm_hour : int, 30 tm_isdst : int, (* 0 = no, 1 = yes, ~1 = don't know *) 31 tm_mday : int, 32 tm_min : int, 33 tm_mon : int, 34 tm_sec : int, 35 tm_wday : int, 36 tm_yday : int, 37 tm_year : int 38 } 39 40 prim_val getlocaltime_ : real -> tmoz = 1 "sml_localtime"; 41 prim_val getunivtime_ : real -> tmoz = 1 "sml_gmtime"; 42 prim_val mktime_ : tmoz -> real = 1 "sml_mktime"; 43 prim_val localoffset_ : unit -> real = 1 "sml_localoffset"; 44 45 (* The offset to add to local time to get UTC: positive West of UTC *) 46 47 val localoffset = localoffset_ () 48 49 prim_val asctime_ : tmoz -> string = 1 "sml_asctime"; 50 prim_val strftime_ : string -> tmoz -> string = 2 "sml_strftime"; 51 52 val toweekday = fn 0 => Sun | 1 => Mon | 2 => Tue | 3 => Wed 53 | 4 => Thu | 5 => Fri | 6 => Sat 54 | _ => raise Fail "Internal error: Date.toweekday"; 55 val fromwday = fn Sun => 0 | Mon => 1 | Tue => 2 | Wed => 3 56 | Thu => 4 | Fri => 5 | Sat => 6; 57 val tomonth = fn 0 => Jan | 1 => Feb | 2 => Mar | 3 => Apr 58 | 4 => May | 5 => Jun | 6 => Jul | 7 => Aug 59 | 8 => Sep | 9 => Oct | 10 => Nov | 11 => Dec 60 | _ => raise Fail "Internal error: Date.tomonth"; 61 val frommonth = fn Jan => 0 | Feb => 1 | Mar => 2 | Apr => 3 62 | May => 4 | Jun => 5 | Jul => 6 | Aug => 7 63 | Sep => 8 | Oct => 9 | Nov => 10 | Dec => 11; 64 65 fun tmozToDate {tm_hour, tm_isdst, tm_mday, tm_min, tm_mon, tm_sec, 66 tm_wday, tm_yday, tm_year} offset = 67 DATE {year = tm_year + 1900, month = tomonth tm_mon, 68 day = tm_mday, hour = tm_hour, minute = tm_min, 69 second = tm_sec, wday = toweekday tm_wday, 70 yday = tm_yday, 71 isDst = (case tm_isdst of 0 => SOME false 72 | 1 => SOME true 73 | _ => NONE), 74 offset = offset } 75 76 fun leapyear y = y mod 4 = 0 andalso y mod 100 <> 0 orelse y mod 400 = 0 77 78 val monthlengths = #[31, 28, 31, 30, 31, 30, 31, 31, 30, 31, 30, 31] 79 80 fun monthdays year month = 81 if month = Feb andalso leapyear year then 29 82 else Vector.sub(monthlengths, frommonth month) 83 84 fun yeardays year = if leapyear year then 366 else 365 85 86 (* Check whether date may be passed to ISO/ANSI C functions: *) 87 88 fun okDate (DATE {year, month, day, hour, minute, second, ...}) = 89 1900 <= year 90 andalso 1 <= day andalso day <= monthdays year month 91 andalso 0 <= hour andalso hour <= 23 92 andalso 0 <= minute andalso minute <= 59 93 andalso 0 <= second andalso second <= 61 (* leap seconds *) 94 95 fun dateToTmoz (dt as DATE {year, month, day, hour, minute, second, 96 wday, yday, isDst, offset}) = 97 if okDate dt then 98 {tm_hour = hour, tm_mday = day, tm_min = minute, 99 tm_mon = frommonth month, tm_sec = second, 100 tm_year = year - 1900, 101 tm_isdst = case isDst of SOME false=>0 | SOME true=>1 | NONE=> ~1, 102 tm_wday = fromwday wday, tm_yday = yday} 103 else 104 raise Date; 105 106 (* -------------------------------------------------- *) 107 (* Translated from Emacs's calendar.el: *) 108 109 (* Reingold: Number of the day within the year: *) 110 111 fun dayinyear year month day = 112 let val monthno = frommonth month 113 in 114 day - 1 + 31 * monthno 115 - (if monthno > 1 then 116 (27 + 4 * monthno) div 10 - (if leapyear year then 1 else 0) 117 else 0) 118 end 119 120 (* Reingold: Find the number of days elapsed from the (imagined) 121 Gregorian date Sunday, December 31, 1 BC to the given date. *) 122 123 fun todaynumber year month day = 124 let val prioryears = year - 1 125 in 126 dayinyear year month day 127 + 1 128 + 365 * prioryears 129 + prioryears div 4 130 - prioryears div 100 131 + prioryears div 400 132 end 133 134 (* Reingold et al: from absolute day number to year, month, date: *) 135 136 fun fromdaynumber n = 137 let val d0 = n - 1 138 val n400 = d0 div 146097 139 val d1 = d0 mod 146097 140 val n100 = d1 div 36524 141 val d2 = d1 mod 36524 142 val n4 = d2 div 1461 143 val d3 = d2 mod 1461 144 val n1 = d3 div 365 145 val day = 1 + d3 mod 365 146 val year = 400 * n400 + 100 * n100 + n4 * 4 + n1 + 1 147 fun loop month day = 148 let val mdays = monthdays year (tomonth month) 149 in 150 if mdays < day then loop (month+1) (day-mdays) 151 else (year, tomonth month, day) 152 end 153 in 154 if n100 = 4 orelse n1 = 4 then 155 (year-1, Dec, 31) 156 else 157 loop 0 day 158 end 159 160 (* -------------------------------------------------- *) 161 162 fun weekday daynumber = toweekday (daynumber mod 7) 163 164 (* Normalize a date, disregarding leap seconds: *) 165 166 fun normalizedate yr0 mo0 dy0 hr0 mn0 sec0 offset = 167 let val mn1 = mn0 + sec0 div 60 168 val second = sec0 mod 60 169 val hr1 = hr0 + mn1 div 60 170 val minute = mn1 mod 60 171 val dayno = todaynumber yr0 mo0 dy0 + hr1 div 24 172 val hour = hr1 mod 24 173 val (year, month, day) = fromdaynumber dayno 174 val date1 = DATE { 175 year = year, 176 month = month, 177 day = day, 178 hour = hour, 179 minute = minute, 180 second = second, 181 wday = weekday dayno, 182 yday = dayinyear year month day, 183 offset = offset, 184 isDst = case offset of 185 NONE => NONE 186 | SOME _ => SOME false } 187 in 188 (* One cannot reliably compute DST in non-local timezones, 189 not even given the offset from UTC. Countries in the 190 Northern hemisphere have DST during Mar-Oct, those around 191 Equator do not have DST, and those in the Southern 192 hemisphere have DST during Oct-Mar. *) 193 194 if year < 1970 orelse year > 2037 then date1 195 else 196 case offset of 197 NONE => 198 tmozToDate (getlocaltime_ (mktime_ (dateToTmoz date1))) 199 offset 200 | SOME t => date1 201 end 202 203in 204 205 fun fromTimeLocal t = 206 tmozToDate (getlocaltime_ (Time.toReal t)) NONE; 207 208 fun fromTimeUniv t = 209 tmozToDate (getunivtime_ (Time.toReal t)) (SOME 0); 210 211 (* The following implements conversion from a local date to 212 a Time.time. It IGNORES wday and yday. *) 213 214 fun toTime (date as DATE {offset, ...}) = 215 let val secoffset = 216 case offset of 217 NONE => 0.0 218 | SOME secs => localoffset + real secs 219 val clock = mktime_ (dateToTmoz date) - secoffset 220 in 221 if clock < 0.0 then raise Date 222 else Time.fromReal clock 223 end; 224 225 fun localOffset () = Time.fromSeconds (Real.round localoffset mod 86400) 226 227 fun toString date = 228 String.substring(asctime_ (dateToTmoz date), 0, 24) 229 handle Fail _ => raise Date 230 | Subscript => raise (Fail "Date.toString: internal error"); 231 232 fun fmt fmtstr date = 233 (strftime_ fmtstr (dateToTmoz date)) 234 handle Fail _ => raise Date 235 236 (* To scan dates in the format "Wed Mar 8 19:06:45 1995" *) 237 238 exception BadFormat; 239 fun getVal (SOME v) = v 240 | getVal NONE = raise BadFormat; 241 242 fun scan getc src = 243 let val getstring = StringCvt.splitl Char.isAlpha getc 244 fun getint src = getVal (Int.scan StringCvt.DEC getc src) 245 fun drop p = StringCvt.dropl p getc 246 fun isColon c = (c = #":") 247 248 val getMonth = fn "Jan" => Jan | "Feb" => Feb | "Mar" => Mar 249 | "Apr" => Apr | "May" => May | "Jun" => Jun 250 | "Jul" => Jul | "Aug" => Aug | "Sep" => Sep 251 | "Oct" => Oct | "Nov" => Nov | "Dec" => Dec 252 | _ => raise BadFormat 253 val getWday = fn "Sun" => Sun | "Mon" => Mon | "Tue" => Tue 254 | "Wed" => Wed | "Thu" => Thu | "Fri" => Fri 255 | "Sat" => Sat 256 | _ => raise BadFormat 257 258 val (wday, src1) = getstring src 259 val (month, src2) = getstring (drop Char.isSpace src1) 260 val (day, src3) = getint src2 261 val (hour, src4) = getint src3 262 val (min, src5) = getint (drop isColon src4) 263 val (sec, src6) = getint (drop isColon src5) 264 val (year, src7) = getint src6 265 val month = getMonth month 266 in SOME (DATE {year = year, month = month, 267 day = day, hour = hour, minute = min, 268 second = sec, wday = getWday wday, 269 yday = dayinyear year month day, 270 isDst = NONE, offset = NONE}, src7) 271 end 272 handle BadFormat => NONE 273 274 fun fromString s = StringCvt.scanString scan s 275 276 (* Ignore timezone and DST when comparing dates: *) 277 278 fun compare 279 (DATE {year=y1,month=mo1,day=d1,hour=h1,minute=mi1,second=s1, ...}, 280 DATE {year=y2,month=mo2,day=d2,hour=h2,minute=mi2,second=s2, ...}) = 281 let fun cmp(v1, v2, cmpnext) = 282 if v1 < v2 then LESS 283 else if v1 > v2 then GREATER 284 else (* EQUAL *) cmpnext () 285 in 286 cmp(y1, y2, 287 fn _ => cmp(frommonth mo1, frommonth mo2, 288 fn _ => cmp(d1, d2, 289 fn _ => cmp(h1, h2, 290 fn _ => cmp(mi1, mi2, 291 fn _ => cmp(s1, s2, 292 fn _ => EQUAL)))))) 293 end 294 295 fun date { year, month, day, hour, minute, second, offset } = 296 if year < 0 then raise Date 297 else 298 let val (dayoffset, offset') = 299 case offset of 300 NONE => (0, NONE) 301 | SOME time => 302 let val secs = Time.toSeconds time 303 val secoffset = 304 if secs <= 43200 then ~secs else 86400 - secs 305 in (Int.quot(secs, 86400), SOME secoffset) end 306 val day' = day + dayoffset 307 in 308 normalizedate year month day' hour minute second offset' 309 end 310 311 fun year (DATE { year, ... }) = year 312 313 fun month (DATE { month, ... }) = month 314 315 fun day (DATE { day, ... }) = day 316 317 fun hour (DATE { hour, ... }) = hour 318 319 fun minute (DATE { minute, ... }) = minute 320 321 fun second (DATE { second, ... }) = second 322 323 fun weekDay (DATE { wday, ... }) = wday 324 325 fun yearDay (DATE { yday, ... }) = yday 326 327 fun isDst (DATE { isDst, ... }) = isDst 328 329 fun offset (DATE { offset, ... }) = 330 Option.map (fn secs => Time.fromSeconds ((86400 - secs) mod 86400)) 331 offset 332end 333