Commit | Line | Data |
---|---|---|
7f918cf1 CE |
1 | (* Modified from the ML Kit 4.1.4; basislib/Date.sml |
2 | * by mfluet@acm.org on 2017-04-07 | |
3 | * by mfluet@acm.org on 2006-4-25 | |
4 | * by mfluet@acm.org on 2005-8-10 based on | |
5 | * modifications from the ML Kit Version 3; basislib/Date.sml | |
6 | * by sweeks@research.nj.nec.com on 1999-1-3 and | |
7 | * by sweeks@acm.org on 2000-1-18. | |
8 | *) | |
9 | ||
10 | (* Date -- 1995-07-03, 1998-04-07 *) | |
11 | ||
12 | structure Date :> DATE = | |
13 | struct | |
14 | structure Prim = PrimitiveFFI.Date | |
15 | structure Tm = Prim.Tm | |
16 | ||
17 | (* Patch to make Time look like it deals with Int.int | |
18 | * instead of LargeInt.int. | |
19 | *) | |
20 | structure Time = | |
21 | struct | |
22 | open Time | |
23 | val toSeconds = LargeInt.toInt o toSeconds | |
24 | val fromSeconds = fromSeconds o LargeInt.fromInt | |
25 | end | |
26 | ||
27 | datatype weekday = Mon | Tue | Wed | Thu | Fri | Sat | Sun | |
28 | ||
29 | datatype month = Jan | Feb | Mar | Apr | May | Jun | |
30 | | Jul | Aug | Sep | Oct | Nov | Dec | |
31 | ||
32 | datatype t = | |
33 | T of {day: int, (* 1-31 *) | |
34 | hour: int, (* 0-23 *) | |
35 | isDst: bool option, (* daylight savings time in force *) | |
36 | minute: int, (* 0-59 *) | |
37 | month: month, | |
38 | offset: int option, (* signed seconds East of UTC: | |
39 | * this zone = UTC+t; ~82800 < t <= 82800 *) | |
40 | second: int, (* 0-61 (allowing for leap seconds) *) | |
41 | weekDay: weekday, | |
42 | year: int, (* e.g. 1995 *) | |
43 | yearDay: int} (* 0-365 *) | |
44 | type date = t | |
45 | ||
46 | local | |
47 | fun make f (T r) = f r | |
48 | in | |
49 | val day = make #day | |
50 | val hour = make #hour | |
51 | val isDst = make #isDst | |
52 | val minute = make #minute | |
53 | val month = make #month | |
54 | val second = make #second | |
55 | val weekDay = make #weekDay | |
56 | val year = make #year | |
57 | val yearDay = make #yearDay | |
58 | end | |
59 | ||
60 | exception Date | |
61 | ||
62 | (* 86400 = 24*60*6 is the number of seconds per day *) | |
63 | ||
64 | type tmoz = {tm_hour : C_Int.t, | |
65 | tm_isdst : C_Int.t, (* 0 = no, 1 = yes, ~1 = don't know *) | |
66 | tm_mday : C_Int.t, | |
67 | tm_min : C_Int.t, | |
68 | tm_mon : C_Int.t, | |
69 | tm_sec : C_Int.t, | |
70 | tm_wday : C_Int.t, | |
71 | tm_yday : C_Int.t, | |
72 | tm_year : C_Int.t} | |
73 | local | |
74 | fun make (f: C_Time.t ref -> C_Int.t C_Errno.t) (n: C_Time.t) : tmoz = | |
75 | (ignore (f (ref n)) | |
76 | ; {tm_hour = Tm.getHour (), | |
77 | tm_isdst = Tm.getIsDst (), | |
78 | tm_mday = Tm.getMDay (), | |
79 | tm_min = Tm.getMin (), | |
80 | tm_mon = Tm.getMon (), | |
81 | tm_sec = Tm.getSec (), | |
82 | tm_wday = Tm.getWDay (), | |
83 | tm_yday = Tm.getYDay (), | |
84 | tm_year = Tm.getYear ()}) | |
85 | in | |
86 | val getlocaltime_ = make Prim.localTime | |
87 | val getgmtime_ = make Prim.gmTime | |
88 | end | |
89 | ||
90 | fun setTmBuf ({tm_hour, tm_isdst, tm_mday, tm_min, tm_mon, | |
91 | tm_sec, tm_wday, tm_yday, tm_year}: tmoz) : unit = | |
92 | (Tm.setHour tm_hour | |
93 | ; Tm.setIsDst tm_isdst | |
94 | ; Tm.setMDay tm_mday | |
95 | ; Tm.setMin tm_min | |
96 | ; Tm.setMon tm_mon | |
97 | ; Tm.setSec tm_sec | |
98 | ; Tm.setWDay tm_wday | |
99 | ; Tm.setYDay tm_yday | |
100 | ; Tm.setYear tm_year) | |
101 | ||
102 | fun mktime_ (t: tmoz): C_Time.t = C_Errno.check (setTmBuf t; Prim.mkTime ()) | |
103 | ||
104 | (* The offset to add to local time to get UTC: positive West of UTC *) | |
105 | val localoffset: int = C_Double.round (Prim.localOffset ()) | |
106 | ||
107 | val toweekday: int -> weekday = | |
108 | fn 0 => Sun | 1 => Mon | 2 => Tue | 3 => Wed | |
109 | | 4 => Thu | 5 => Fri | 6 => Sat | |
110 | | _ => raise Fail "Internal error: Date.toweekday" | |
111 | ||
112 | val fromwday: weekday -> int = | |
113 | fn Sun => 0 | Mon => 1 | Tue => 2 | Wed => 3 | |
114 | | Thu => 4 | Fri => 5 | Sat => 6 | |
115 | ||
116 | val tomonth: int -> month = | |
117 | fn 0 => Jan | 1 => Feb | 2 => Mar | 3 => Apr | |
118 | | 4 => May | 5 => Jun | 6 => Jul | 7 => Aug | |
119 | | 8 => Sep | 9 => Oct | 10 => Nov | 11 => Dec | |
120 | | _ => raise Fail "Internal error: Date.tomonth" | |
121 | ||
122 | val frommonth: month -> int = | |
123 | fn Jan => 0 | Feb => 1 | Mar => 2 | Apr => 3 | |
124 | | May => 4 | Jun => 5 | Jul => 6 | Aug => 7 | |
125 | | Sep => 8 | Oct => 9 | Nov => 10 | Dec => 11 | |
126 | ||
127 | fun tmozToDate ({tm_hour, tm_isdst, tm_mday, tm_min, tm_mon, | |
128 | tm_sec, tm_wday, tm_yday, tm_year}: tmoz) offset = | |
129 | T {day = C_Int.toInt tm_mday, | |
130 | hour = C_Int.toInt tm_hour, | |
131 | isDst = (case tm_isdst of | |
132 | 0 => SOME false | |
133 | | 1 => SOME true | |
134 | | _ => NONE), | |
135 | minute = C_Int.toInt tm_min, | |
136 | month = tomonth (C_Int.toInt tm_mon), | |
137 | offset = offset, | |
138 | second = C_Int.toInt tm_sec, | |
139 | weekDay = toweekday (C_Int.toInt tm_wday), | |
140 | yearDay = C_Int.toInt tm_yday, | |
141 | year = (C_Int.toInt tm_year) + 1900} | |
142 | ||
143 | fun leapyear (y: int) = | |
144 | y mod 4 = 0 andalso y mod 100 <> 0 orelse y mod 400 = 0 | |
145 | ||
146 | fun monthdays year month : int = | |
147 | case month of | |
148 | Jan => 31 | |
149 | | Feb => if leapyear year then 29 else 28 | |
150 | | Mar => 31 | |
151 | | Apr => 30 | |
152 | | May => 31 | |
153 | | Jun => 30 | |
154 | | Jul => 31 | |
155 | | Aug => 31 | |
156 | | Sep => 30 | |
157 | | Oct => 31 | |
158 | | Nov => 30 | |
159 | | Dec => 31 | |
160 | ||
161 | (* Check whether date may be passed to ISO/ANSI C functions: *) | |
162 | ||
163 | fun okDate (T {year, month, day, hour, minute, second, ...}) = | |
164 | 1 <= day andalso day <= monthdays year month | |
165 | andalso 0 <= hour andalso hour <= 23 | |
166 | andalso 0 <= minute andalso minute <= 59 | |
167 | andalso 0 <= second andalso second <= 61 (* leap seconds *) | |
168 | ||
169 | fun dateToTmoz (dt as T {year, month, day, hour, minute, second, | |
170 | weekDay, yearDay, isDst, ...}): tmoz = | |
171 | if not (okDate dt) | |
172 | then raise Date | |
173 | else {tm_hour = C_Int.fromInt hour, | |
174 | tm_isdst = (case isDst of | |
175 | SOME false => 0 | |
176 | | SOME true => 1 | |
177 | | NONE=> ~1), | |
178 | tm_mday = C_Int.fromInt day, | |
179 | tm_min = C_Int.fromInt minute, | |
180 | tm_mon = C_Int.fromInt (frommonth month), | |
181 | tm_sec = C_Int.fromInt second, | |
182 | tm_wday = C_Int.fromInt (fromwday weekDay), | |
183 | tm_yday = C_Int.fromInt yearDay, | |
184 | tm_year = C_Int.fromInt (year - 1900)} | |
185 | ||
186 | (* -------------------------------------------------- *) | |
187 | (* Translated from Emacs's calendar.el: *) | |
188 | ||
189 | (* Reingold: Number of the day within the year: *) | |
190 | ||
191 | fun dayinyear (year: int, month: month, day: int): int = | |
192 | let val monthno = frommonth month | |
193 | in | |
194 | day - 1 + 31 * monthno | |
195 | - (if monthno > 1 then | |
196 | (27 + 4 * monthno) div 10 - (if leapyear year then 1 else 0) | |
197 | else 0) | |
198 | end | |
199 | ||
200 | (* Reingold: Find the number of days elapsed from the (imagined) | |
201 | Gregorian date Sunday, December 31, 1 BC to the given date. *) | |
202 | ||
203 | fun todaynumber year month day = | |
204 | let val prioryears = year - 1 | |
205 | in | |
206 | dayinyear (year, month, day) | |
207 | + 1 | |
208 | + 365 * prioryears | |
209 | + prioryears div 4 | |
210 | - prioryears div 100 | |
211 | + prioryears div 400 | |
212 | end | |
213 | ||
214 | (* Reingold et al: from absolute day number to year, month, date: *) | |
215 | ||
216 | fun fromdaynumber n = | |
217 | let val d0 = n - 1 | |
218 | val n400 = d0 div 146097 | |
219 | val d1 = d0 mod 146097 | |
220 | val n100 = d1 div 36524 | |
221 | val d2 = d1 mod 36524 | |
222 | val n4 = d2 div 1461 | |
223 | val d3 = d2 mod 1461 | |
224 | val n1 = d3 div 365 | |
225 | val day = 1 + d3 mod 365 | |
226 | val year = 400 * n400 + 100 * n100 + n4 * 4 + n1 + 1 | |
227 | fun loop month day = | |
228 | let val mdays = monthdays year (tomonth month) | |
229 | in | |
230 | if mdays < day then loop (month+1) (day-mdays) | |
231 | else (year, tomonth month, day) | |
232 | end | |
233 | in | |
234 | if n100 = 4 orelse n1 = 4 then | |
235 | (year-1, Dec, 31) | |
236 | else | |
237 | loop 0 day | |
238 | end | |
239 | ||
240 | (* -------------------------------------------------- *) | |
241 | ||
242 | fun weekday daynumber = toweekday (daynumber mod 7) | |
243 | ||
244 | (* Normalize a date, disregarding leap seconds: *) | |
245 | ||
246 | fun normalizedate yr0 mo0 dy0 hr0 mn0 sec0 offset = | |
247 | let val mn1 = mn0 + sec0 div 60 | |
248 | val second = sec0 mod 60 | |
249 | val hr1 = hr0 + mn1 div 60 | |
250 | val minute = mn1 mod 60 | |
251 | val dayno = todaynumber yr0 mo0 dy0 + hr1 div 24 | |
252 | val hour = hr1 mod 24 | |
253 | val (year, month, day) = fromdaynumber dayno | |
254 | val date1 = T {day = day, | |
255 | hour = hour, | |
256 | isDst = (case offset of | |
257 | NONE => NONE | |
258 | | SOME _ => SOME false), | |
259 | minute = minute, | |
260 | month = month, | |
261 | offset = offset, | |
262 | second = second, | |
263 | weekDay = weekday dayno, | |
264 | year = year, | |
265 | yearDay = dayinyear (year, month, day)} | |
266 | in | |
267 | (* One cannot reliably compute DST in non-local timezones, | |
268 | not even given the offset from UTC. Countries in the | |
269 | Northern hemisphere have DST during Mar-Oct, those around | |
270 | Equator do not have DST, and those in the Southern | |
271 | hemisphere have DST during Oct-Mar. *) | |
272 | if year < 1970 orelse year > 2037 then date1 | |
273 | else | |
274 | case offset of | |
275 | NONE => | |
276 | tmozToDate (getlocaltime_ (mktime_ (dateToTmoz date1))) | |
277 | offset | |
278 | | SOME _ => date1 | |
279 | end | |
280 | ||
281 | fun fromTimeLocal t = | |
282 | tmozToDate (getlocaltime_ (C_Time.fromInt (Time.toSeconds t))) NONE | |
283 | ||
284 | fun fromTimeUniv t = | |
285 | tmozToDate (getgmtime_ (C_Time.fromInt (Time.toSeconds t))) (SOME 0) | |
286 | ||
287 | (* The following implements conversion from a local date to | |
288 | * a Time.time. It IGNORES wday and yday. | |
289 | *) | |
290 | ||
291 | fun toTime (date as T {offset, ...}) = | |
292 | let | |
293 | val secoffset = | |
294 | case offset of | |
295 | NONE => 0 | |
296 | | SOME secs => localoffset + secs | |
297 | val clock = C_Time.toInt (mktime_ (dateToTmoz date)) - secoffset | |
298 | in | |
299 | if clock < 0 then raise Date | |
300 | else Time.fromSeconds clock | |
301 | end | |
302 | ||
303 | fun localOffset () = Time.fromSeconds (localoffset mod 86400) | |
304 | ||
305 | local | |
306 | val isFormatChar = | |
307 | let | |
308 | val a = Array.tabulate (Char.maxOrd + 1, fn _ => false) | |
309 | val validChars = "aAbBcdHIjmMpSUwWxXyYZ%" | |
310 | in Natural.foreach | |
311 | (size validChars, fn i => | |
312 | Array.update (a, Char.ord (String.sub (validChars, i)), true)); | |
313 | fn c => Array.sub (a, Char.ord c) | |
314 | end | |
315 | in | |
316 | fun fmt fmtStr d = | |
317 | let | |
318 | val _ = setTmBuf (dateToTmoz d) | |
319 | val bufLen = 50 (* more than enough for a single format char *) | |
320 | val buf = Array.alloc bufLen | |
321 | fun strftime fmtChar = | |
322 | let | |
323 | val len = | |
324 | Prim.strfTime | |
325 | (buf, C_Size.fromInt bufLen, | |
326 | NullString.fromString (concat ["%", str fmtChar, "\000"])) | |
327 | val len = C_Size.toInt len | |
328 | in if len = 0 | |
329 | then raise Fail "Date.fmt" | |
330 | else ArraySlice.vector (ArraySlice.slice (buf, 0, SOME len)) | |
331 | end | |
332 | val max = size fmtStr | |
333 | fun loop (i, start, accum) = | |
334 | let | |
335 | fun newAccum () = | |
336 | let val len = i - start | |
337 | in | |
338 | if len = 0 | |
339 | then accum | |
340 | else String.extract (fmtStr, start, SOME len) :: accum | |
341 | end | |
342 | in | |
343 | if i >= max | |
344 | then newAccum () | |
345 | else | |
346 | if #"%" = String.sub (fmtStr, i) | |
347 | then | |
348 | let | |
349 | val i = i + 1 | |
350 | in | |
351 | if i >= max | |
352 | then newAccum () | |
353 | else let | |
354 | val c = String.sub (fmtStr, i) | |
355 | in | |
356 | if isFormatChar c | |
357 | then loop (i + 1, i + 1, | |
358 | strftime c :: newAccum ()) | |
359 | else loop (i, i, newAccum ()) | |
360 | end | |
361 | end | |
362 | else loop (i + 1, start, accum) | |
363 | end | |
364 | in concat (rev (loop (0, 0, []))) | |
365 | end | |
366 | end | |
367 | ||
368 | val toString = fmt "%a %b %d %H:%M:%S %Y" | |
369 | ||
370 | type ('a, 'b) reader = ('a, 'b) Reader.reader | |
371 | ||
372 | fun scan (reader: (char, 'a) reader): (t, 'a) reader = | |
373 | let | |
374 | type 'b t = ('b, 'a) reader | |
375 | val none: 'b t = fn _ => NONE | |
376 | fun done (b: 'b): 'b t = fn a => SOME (b, a) | |
377 | fun peek1 (f: char -> 'b t): 'b t = | |
378 | fn a => | |
379 | case reader a of | |
380 | NONE => NONE | |
381 | | SOME (c, _) => f c a | |
382 | fun read1 (f: char -> 'b t): 'b t = | |
383 | fn a => | |
384 | case reader a of | |
385 | NONE => NONE | |
386 | | SOME (c, a) => f c a | |
387 | fun skipSpace (r: 'b t): 'b t = | |
388 | let | |
389 | fun loop (): 'b t = | |
390 | peek1 (fn c => | |
391 | if Char.isSpace c | |
392 | then read1 (fn _ => loop ()) | |
393 | else r) | |
394 | in | |
395 | loop () | |
396 | end | |
397 | fun readN (n: int, f: string -> 'b t): 'b t = | |
398 | let | |
399 | fun loop (n: int, ac: char list): 'b t = | |
400 | if 0 = n | |
401 | then f (implode (rev ac)) | |
402 | else read1 (fn c => loop (n - 1, c :: ac)) | |
403 | in | |
404 | loop (n, []) | |
405 | end | |
406 | fun readChar (c: char, r: 'b t): 'b t = | |
407 | read1 (fn c' => if c = c' then r else none) | |
408 | fun readWeekDay (f: weekday -> 'b t): 'b t = | |
409 | readN (3, fn s => | |
410 | case s of | |
411 | "Mon" => f Mon | |
412 | | "Tue" => f Tue | |
413 | | "Wed" => f Wed | |
414 | | "Thu" => f Thu | |
415 | | "Fri" => f Fri | |
416 | | "Sat" => f Sat | |
417 | | "Sun" => f Sun | |
418 | | _ => none) | |
419 | fun readMonth (f: month -> 'b t): 'b t = | |
420 | readN (3, fn s => | |
421 | case s of | |
422 | "Jan" => f Jan | |
423 | | "Feb" => f Feb | |
424 | | "Mar" => f Mar | |
425 | | "Apr" => f Apr | |
426 | | "May" => f May | |
427 | | "Jun" => f Jun | |
428 | | "Jul" => f Jul | |
429 | | "Aug" => f Aug | |
430 | | "Sep" => f Sep | |
431 | | "Oct" => f Oct | |
432 | | "Nov" => f Nov | |
433 | | "Dec" => f Dec | |
434 | | _ => none) | |
435 | fun readDigs (n: int, lower: int, upper: int, f: int -> 'b t): 'b t = | |
436 | readN (n, fn s => | |
437 | if not (CharVector.all Char.isDigit s) | |
438 | then none | |
439 | else | |
440 | let | |
441 | val v = | |
442 | CharVector.foldl | |
443 | (fn (c, ac) => | |
444 | ac * 10 + (Char.ord c - Char.ord #"0")) | |
445 | 0 s | |
446 | in | |
447 | if lower <= v andalso v <= upper | |
448 | then f v | |
449 | else none | |
450 | end) | |
451 | fun readDay f = | |
452 | peek1 (fn c => | |
453 | if c = #" " | |
454 | then read1 (fn _ => readDigs (1, 1, 9, f)) | |
455 | else readDigs (2, 1, 31, f)) | |
456 | fun readHour f = readDigs (2, 0, 23, f) | |
457 | fun readMinute f = readDigs (2, 0, 59, f) | |
458 | fun readSeconds f = readDigs (2, 0, 61, f) | |
459 | fun readYear f = readDigs (4, 0, 9999, f) | |
460 | in | |
461 | skipSpace | |
462 | (readWeekDay | |
463 | (fn weekDay => | |
464 | readChar | |
465 | (#" ", | |
466 | readMonth | |
467 | (fn month => | |
468 | readChar | |
469 | (#" ", | |
470 | readDay | |
471 | (fn day => | |
472 | readChar | |
473 | (#" ", | |
474 | readHour | |
475 | (fn hour => | |
476 | readChar | |
477 | (#":", | |
478 | readMinute | |
479 | (fn minute => | |
480 | (readChar | |
481 | (#":", | |
482 | readSeconds | |
483 | (fn second => | |
484 | readChar | |
485 | (#" ", | |
486 | readYear | |
487 | (fn year => | |
488 | done (T {day = day, | |
489 | hour = hour, | |
490 | isDst = NONE, | |
491 | minute = minute, | |
492 | month = month, | |
493 | offset = NONE, | |
494 | second = second, | |
495 | weekDay = weekDay, | |
496 | year = year, | |
497 | yearDay = dayinyear (year, month, day)} | |
498 | )))))))))))))))) | |
499 | end | |
500 | ||
501 | fun fromString s = StringCvt.scanString scan s | |
502 | ||
503 | (* Ignore timezone and DST when comparing dates: *) | |
504 | fun compare | |
505 | (T {year=y1,month=mo1,day=d1,hour=h1,minute=mi1,second=s1, ...}, | |
506 | T {year=y2,month=mo2,day=d2,hour=h2,minute=mi2,second=s2, ...}) = | |
507 | let | |
508 | fun cmp (v1, v2, cmpnext) = | |
509 | case Int.compare (v1, v2) of | |
510 | EQUAL => cmpnext () | |
511 | | r => r | |
512 | in | |
513 | cmp (y1, y2, | |
514 | fn _ => cmp (frommonth mo1, frommonth mo2, | |
515 | fn _ => cmp (d1, d2, | |
516 | fn _ => cmp (h1, h2, | |
517 | fn _ => cmp (mi1, mi2, | |
518 | fn _ => cmp (s1, s2, | |
519 | fn _ => EQUAL)))))) | |
520 | end | |
521 | ||
522 | fun date { year, month, day, hour, minute, second, offset } = | |
523 | if year < 0 then raise Date | |
524 | else | |
525 | let | |
526 | val (dayoffset, offset') = | |
527 | case offset of | |
528 | NONE => (0, NONE) | |
529 | | SOME time => | |
530 | let | |
531 | val secs = Time.toSeconds time | |
532 | val secoffset = | |
533 | if secs <= 82800 then ~secs else 86400 - secs | |
534 | in | |
535 | (Int.quot (secs, 86400), SOME secoffset) | |
536 | end | |
537 | val day' = day + dayoffset | |
538 | in | |
539 | normalizedate year month day' hour minute second offset' | |
540 | end | |
541 | ||
542 | fun offset (T {offset, ...}) = | |
543 | Option.map | |
544 | (fn secs => Time.fromSeconds ((86400 + secs) mod 86400)) | |
545 | offset | |
546 | end |