1(* 2 Title: Standard Basis Library: Date structure. 3 Copyright David Matthews 2000, 2016-17 4 5 This library is free software; you can redistribute it and/or 6 modify it under the terms of the GNU Lesser General Public 7 License version 2.1 as published by the Free Software Foundation. 8 9 This library is distributed in the hope that it will be useful, 10 but WITHOUT ANY WARRANTY; without even the implied warranty of 11 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU 12 Lesser General Public License for more details. 13 14 You should have received a copy of the GNU Lesser General Public 15 License along with this library; if not, write to the Free Software 16 Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA 17*) 18 19structure Date :> DATE = 20struct 21 (* There seems to be an assumption, particularly in the "compare" 22 function, that Date.date values are records of year, month, day 23 etc. *) 24 type date = { 25 year: int, (* Signed year. *) 26 month: int, (* Month as 0..11 *) 27 day: int, (* Day as 1..(28, 29, 30, 31) *) 28 hour: int, (* Hour as 0..23 *) 29 minute: int, (* Minute as 0..59 *) 30 second: int, (* Second as 0..59 (maybe 60 or 61 if leap) *) 31 offset: Time.time option (* Offset as Time.time -24hrs<t<24hrs *) 32 } 33 34 datatype weekday = Mon | Tue | Wed | Thu | Fri | Sat | Sun 35 datatype month = Jan | Feb | Mar | Apr | May | Jun | 36 Jul | Aug | Sep | Oct | Nov | Dec 37 38 exception Date 39 40 val secsPerHour: LargeInt.int = 60*60 41 val secsPerDay: LargeInt.int = 24*secsPerHour 42 val monthVec = 43 Vector.fromList [Jan, Feb, Mar, Apr, May, Jun, Jul, Aug, Sep, Oct, Nov, Dec]; 44 val dayOfWkVec = 45 Vector.fromList [Sun, Mon, Tue, Wed, Thu, Fri, Sat] 46 47 (* Vector of days from the beginning of the year. *) 48 val dayVec: int Vector.vector = 49 Vector.fromList [~1, 30, 58, 89, 119, 150, 180, 211, 242, 272, 303, 333, 365]; 50 val dayInLeapYearVec: int Vector.vector = 51 Vector.fromList [~1, 30, 59, 90, 120, 151, 181, 212, 243, 273, 304, 334, 366]; 52 53 (* Days of the week and months in abbreviated English form. *) 54 val dayNames = 55 Vector.fromList ["Sun", "Mon", "Tue", "Wed", "Thu", "Fri", "Sat"] 56 val monthNames = 57 Vector.fromList ["Jan", "Feb", "Mar", "Apr", "May", "Jun", 58 "Jul", "Aug", "Sep", "Oct", "Nov", "Dec"]; 59 60 (* Convert a month number to the enumerated type. *) 61 fun monthNoToMonth n = 62 Vector.sub(monthVec, n) handle Subscript => raise Date (* Should never happen *) 63 64 fun isLeapYear(l: int): bool = 65 if l mod 100 = 0 then (l div 100) mod 4 = 0 else l mod 4 = 0 66 67 (* Convert the enumerated type to a month number. *) 68 fun monthToMonthNo Jan = 0 69 | monthToMonthNo Feb = 1 70 | monthToMonthNo Mar = 2 71 | monthToMonthNo Apr = 3 72 | monthToMonthNo May = 4 73 | monthToMonthNo Jun = 5 74 | monthToMonthNo Jul = 6 75 | monthToMonthNo Aug = 7 76 | monthToMonthNo Sep = 8 77 | monthToMonthNo Oct = 9 78 | monthToMonthNo Nov = 10 79 | monthToMonthNo Dec = 11 80 81 local 82 val timingGeneralCall = RunCall.rtsCallFull2 "PolyTimingGeneral" 83 fun timingGeneral(code: int, arg:'a):'b = RunCall.unsafeCast(timingGeneralCall(RunCall.unsafeCast(code, arg))) 84 in 85 fun callTiming (code: int) args = timingGeneral (code,args) 86 end 87 88 (* Get the local time offset which applied at the specific time. 89 The time is in seconds since the epoch. The result may be the 90 current time offset if it is outside the range for which we have 91 information. We use seconds as the argument and result here because 92 it avoids having to multiply and divide arbitrary precision values 93 in the RTS. May raise Size if the value is too large (or small). In 94 that case we use the current time offset. *) 95 fun localOffsetApplying (t: LargeInt.int) : LargeInt.int = 96 callTiming 4 t 97 handle General.Size => callTiming 4 (Time.toSeconds(Time.now())) 98 99 (* Get the current local time offset. *) 100 fun localOffset (): Time.time = 101 Time.fromSeconds(localOffsetApplying(Time.toSeconds(Time.now()))) 102 103 local 104 (* Time values are since 1st January of this year. *) 105 val baseYear: int = callTiming 2 0 (* 1601 or 1970 *) 106 val yearOffset: int = callTiming 3 0 (* The offset of zeroTime within that year. 0 on both Unix and Windows *) 107 108 (* Get the day in the year. Either of day or year may be unnormalised 109 but that shouldn't affect the result (except if year is negative???) *) 110 fun dayInYear (day, month, year) = 111 if isLeapYear year then Vector.sub(dayInLeapYearVec, month) + day 112 else Vector.sub(dayVec, month) + day 113 114 (* Compute the number of days since the start. *) 115 fun yearToDays y = 116 let 117 fun ytod dys yr = 118 if yr = baseYear then dys 119 (* If the year is before the base year we subtract the number of 120 days in this year and recurse. *) 121 else if yr < baseYear 122 then if isLeapYear yr then ytod (dys-366) (yr+1) 123 else ytod (dys-365) (yr+1) 124 (* The year we want is after the base year. *) 125 else if yr - baseYear >= 100 126 (* If it is more than a century apart then we can add in the 127 number of days in a century. There are 24 leap years in most 128 centuries except those which are divisible by 400. 129 Note: We're assuming the Gregorian calendar. *) 130 then if ((yr-1) div 100) mod 4 = 0 then ytod (dys+36525) (yr-100) 131 else ytod (dys+36524) (yr-100) 132 else if isLeapYear(yr-1) then ytod (dys+366) (yr-1) 133 else ytod (dys+365) (yr-1) 134 in 135 ytod 0 y 136 end 137 138 (* Convert days to number of years plus the day within the year. *) 139 fun daysToYears d = 140 let 141 fun dtoy dys yr = 142 if dys < 0 143 then (* Before the base year: have to add in days. *) 144 if isLeapYear (yr-1) then dtoy (dys+366) (yr-1) 145 else dtoy (dys+365) (yr-1) 146 (* If we are at least a century away we can subtract the century. *) 147 else if dys >= 36525 148 then if ((yr+99) div 100) mod 4 = 0 then dtoy (dys-36525) (yr+100) 149 else dtoy (dys-36524) (yr+100) 150 else if isLeapYear yr 151 then if dys >= 366 then dtoy (dys-366) (yr+1) else (yr, dys) 152 else if dys >= 365 then dtoy (dys-365) (yr+1) else (yr, dys) 153 in 154 dtoy d baseYear 155 end 156 157 (* Convert a number of seconds to a date. *) 158 fun fromSeconds t (tzOffset: Time.time option) : date = 159 let 160 val tsecs = t - LargeInt.fromInt yearOffset 161 val secs = LargeInt.toInt(tsecs mod 60) 162 val mins = LargeInt.toInt((tsecs div 60) mod 60) 163 val hrs = LargeInt.toInt((tsecs div secsPerHour) mod 24) 164 (* Get the day and year. The day is a value between 0 and 364/365. *) 165 val (year, days) = daysToYears(LargeInt.toInt(tsecs div secsPerDay)) 166 (* Convert the day into a month+day *) 167 val isLeap = isLeapYear year 168 fun dayToMonth dy mth = 169 if dy <= Vector.sub(if isLeap then dayInLeapYearVec else dayVec, mth+1) 170 then mth 171 else dayToMonth dy (mth+1) 172 173 val month = dayToMonth days 0 174 val dayInMonth = 175 days - Vector.sub(if isLeap then dayInLeapYearVec else dayVec, month) 176 in 177 {year=year, month=month, day=dayInMonth, hour=hrs, minute=mins, 178 second=secs, offset = tzOffset } 179 end 180 in 181 (* Get the day in the year. *) 182 fun yearDay({day, month, year, ...}:date) = dayInYear(day, month, year) 183 184 (* Convert the date into a UTC time value. *) 185 fun toTime (date as {year, hour, minute, second, offset, ...}) = 186 let 187 (* Compute the seconds. *) 188 val secs = 189 LargeInt.fromInt second + LargeInt.fromInt minute * 60 + LargeInt.fromInt hour * secsPerHour + 190 LargeInt.fromInt(yearDay date + yearToDays year) * secsPerDay + 191 LargeInt.fromInt yearOffset 192 in 193 case offset of 194 SOME t => Time.+(t, Time.fromSeconds secs) 195 | NONE => 196 Time.fromSeconds(secs + localOffsetApplying secs) 197 end 198 199 (* Convert a UTC time to a UTC date. *) 200 fun fromTimeUniv t = fromSeconds (Time.toSeconds t) (SOME Time.zeroTime) 201 202 (* Convert a UTC time to a date in the local time zone. *) 203 fun fromTimeLocal t = 204 let 205 val secs = Time.toSeconds t 206 val localOffset = localOffsetApplying secs 207 in 208 fromSeconds (secs-localOffset) NONE 209 end 210 211 (* Generate a normalised date. *) 212 fun date {year, month, day, hour, minute, second, offset} = 213 let 214 (* Get the time zone information if it is provided. If it is 215 outside +/- 24 hours we get the number of full days. *) 216 val (tzDays, normTz) = 217 case offset of 218 SOME tz => 219 let 220 open Time 221 val excess = LargeInt.quot(Time.toSeconds tz, secsPerDay)*secsPerDay; 222 in 223 (excess, SOME(tz-Time.fromSeconds excess)) 224 end 225 | NONE => (0, NONE) 226 (* Convert it to the number of seconds since the epoch which will 227 normalise it. *) 228 val secs = 229 LargeInt.fromInt second + LargeInt.fromInt minute * 60 + LargeInt.fromInt hour * secsPerHour + 230 LargeInt.fromInt (dayInYear(day, monthToMonthNo month, year) + yearToDays year) * secsPerDay + 231 LargeInt.fromInt yearOffset + tzDays 232 in 233 (* Convert it into a date. *) 234 fromSeconds secs normTz 235 end 236 237 end 238 239 val year: date->int = #year 240 and day: date->int = #day 241 and hour: date->int = #hour 242 and minute: date->int = #minute 243 and second: date->int = #second 244 and offset: date->Time.time option = #offset 245 246 (* Return the month from the enumerated type. *) 247 fun month({month, ...}:date) = monthNoToMonth month 248 249 (* Get the day of the week as a number - not exported. *) 250 fun dayOfWeek({year, month, day, ...}: date) = 251 let 252 (* From looking at the code of mktime, which is marked as being in 253 the public domain, this formula (Zeller's Congruence?) is used to 254 find the day of the week for the first of any month. 255 I don't know what range this works for but it seems accurate as 256 far as I can test it. *) 257 val m0 = month+1 (* Count months from 1 *) 258 val m1 = (m0 + 9) mod 12 + 1 259 val yy0 = if m0 <= 2 then year-1 else year 260 val yy1 = yy0 div 100 261 val yy2 = yy0 mod 100 262 val dow = ((26*m1 - 2) div 10 + 1 + yy2 + yy2 div 4 + yy1 div 4 - 2*yy1) mod 7 263 in 264 (* Add on the day within the month. *) 265 (dow + day - 1) mod 7 266 end 267 268 (* Get day of week as an enumerated type - exported. *) 269 fun weekDay date = Vector.sub(dayOfWkVec, dayOfWeek date) 270 271 (* QUESTION: The definition of isDst is very vague. I am assuming that it 272 means that, for a local time, did/will Summer Time apply at that time? *) 273 fun isDst (d as {offset=NONE, ...} : date): bool option = 274 let 275 val isSummer = 276 callTiming 5 (Time.toSeconds(toTime d)) handle Size => ~1 277 in 278 if isSummer < 0 then NONE 279 else SOME (isSummer > 0) 280 end 281 | isDst {offset=SOME _, ...} = SOME false (* ?? *) 282 283 (* Compare the dates ignoring time zone information. *) 284 fun compare({year=y1, month=m1, day=d1, hour=h1, minute=n1, second=s1, ...}:date, 285 {year=y2, month=m2, day=d2, hour=h2, minute=n2, second=s2, ...}:date) = 286 if y1 < y2 then General.LESS 287 else if y1 > y2 then General.GREATER 288 else if m1 < m2 then General.LESS 289 else if m1 > m2 then General.GREATER 290 else if d1 < d2 then General.LESS 291 else if d1 > d2 then General.GREATER 292 else if h1 < h2 then General.LESS 293 else if h1 > h2 then General.GREATER 294 else if n1 < n2 then General.LESS 295 else if n1 > n2 then General.GREATER 296 else Int.compare(s1, s2) 297 298 (* Parse a date/time. *) 299 fun scan getc str = 300 let 301 (* Try to extract an n-character string. *) 302 fun getChars n str = 303 let 304 fun getN 0 s str = SOME (String.implode(List.rev s), str) 305 | getN n s str = 306 case getc str of 307 NONE => NONE 308 | SOME(ch, str') => getN (n-1) (ch :: s) str' 309 in 310 getN n [] str 311 end 312 313 (* Get the day of the week. We don't actually use it but we 314 need to verify it. *) 315 (* QUESTION: What time offset should be used? I presume NONE. *) 316 fun parseDayOfWeek str = 317 case getChars 3 str of 318 NONE => NONE 319 | SOME(s, str') => 320 if Vector.foldr (fn(s', t) => t orelse s=s') false dayNames 321 then SOME(s, str') else NONE 322 323 fun parseMonth str = 324 case getChars 3 str of 325 NONE => NONE 326 | SOME(s, str') => 327 (* Return the month corresponding to the month name 328 otherwise NONE. *) 329 Vector.foldri (fn(n:int, s':string, t) => 330 if s = s' then SOME(Vector.sub(monthVec, n), str') else t) NONE 331 monthNames 332 333 (* Get a two digit number. *) 334 fun parse2Digits str = 335 case getc str of 336 NONE => NONE 337 | SOME(ch0, str1) => 338 if ch0 < #"0" orelse ch0 > #"9" then NONE 339 else case getc str1 of 340 NONE => NONE 341 | SOME(ch1, str2) => 342 if ch1 < #"0" orelse ch1 > #"9" then NONE 343 else SOME((Char.ord ch0 - Char.ord #"0")*10 + 344 (Char.ord ch1 - Char.ord #"0"), str2) 345 346 (* Get two digits as a day of the month. Don't check the range. *) 347 val parseDayOfMonth = parse2Digits 348 349 (* A time is written as hh:mm:ss *) 350 fun parseTime str = 351 case parse2Digits str of 352 NONE => NONE 353 | SOME(hh, str1) => 354 case getc str1 of 355 NONE => NONE 356 | SOME(ch, str2) => 357 if ch <> #":" then NONE 358 else case parse2Digits str2 of 359 NONE => NONE 360 | SOME(mm, str3) => 361 case getc str3 of 362 NONE => NONE 363 | SOME(ch, str4) => 364 if ch <> #":" then NONE 365 else case parse2Digits str4 of 366 NONE => NONE 367 | SOME(ss, str5) => 368 SOME((hh, mm, ss), str5) 369 370 (* A year is represented as four digits. *) 371 fun parseYear str = 372 case parse2Digits str of 373 NONE => NONE 374 | SOME(yy0, str1) => 375 case parse2Digits str1 of 376 NONE => NONE 377 | SOME(yy1, str2) => SOME(yy0*100+yy1, str2) 378 379 380 fun parseDate str = 381 case parseDayOfWeek str of 382 NONE => NONE 383 | SOME(_, str1) => 384 case getc str1 of (* Get exactly one space. *) 385 NONE => NONE 386 | SOME(ch, str2) => 387 if ch <> #" " then NONE 388 else case parseMonth str2 of (* Name of month. *) 389 NONE => NONE 390 | SOME(mth, str3) => 391 case getc str3 of (* Get exactly one space. *) 392 NONE => NONE 393 | SOME(ch, str4) => 394 if ch <> #" " then NONE 395 else case parseDayOfMonth str4 of 396 NONE => NONE 397 | SOME(day, str5) => 398 case getc str5 of (* Get exactly one space. *) 399 NONE => NONE 400 | SOME(ch, str6) => 401 if ch <> #" " then NONE 402 else case parseTime str6 of 403 NONE => NONE 404 | SOME((hr,min,sec), str7) => 405 case getc str7 of (* Get exactly one space. *) 406 NONE => NONE 407 | SOME(ch, str8) => 408 if ch <> #" " then NONE 409 else case parseYear str8 of 410 NONE => NONE 411 | SOME(year, str9) => 412 SOME(date{year=year, month=mth, day=day, 413 hour=hr, minute=min, second=sec, 414 offset=NONE}, str9) 415 in 416 case getc str of 417 NONE => NONE 418 | SOME (ch, str') => 419 (* Remove initial white space. *) 420 if Char.isSpace ch then scan getc str' 421 else parseDate str 422 end 423 424 val fromString = StringCvt.scanString scan 425 426 (* toString generates an English language, American style date. *) 427 fun toString (date as {year, month, day, hour, minute, second, ...}: date) = 428 let 429 (* Pad a number with zeros up to the required width. Doesn't 430 work for negatives which ought to be padded after the 431 minus sign, but that's only a problem for years. *) 432 fun int2str n i = 433 let 434 val str = Int.toString i 435 fun padZeros n = if n <= 0 then "" else "0" ^ padZeros (n-1) 436 in 437 padZeros (n-String.size str) ^ str 438 end 439 in 440 String.concat[ 441 Vector.sub(dayNames, dayOfWeek date), " ", 442 Vector.sub(monthNames, month), " ", 443 int2str 2 day, " ", 444 int2str 2 hour, ":", int2str 2 minute, ":", int2str 2 second, " ", 445 int2str 4 year] 446 end 447 448 fun fmt s (date as {year, month, day, hour, minute, second, offset}) = 449 let 450 (* Edit the string to remove any undefined escape combinations. 451 They shouldn't normally occur. *) 452 fun editString s i l = 453 if i = l then s (* Done *) 454 else if String.sub(s, i) <> #"%" 455 then editString s (i+1) l 456 else (* Found a % sign. *) 457 if i = l-1 458 then (* This was the last character. QUESTION: This isn't defined 459 assume we should remove it. *) 460 String.substring(s, 0, i) 461 else 462 let 463 val c = String.sub(s, i+1) 464 in 465 if Char.contains "aAbBcdHIjmMpSUwWxXyYZ%" c 466 then (* OK *) editString s (i+2) l 467 else (* Replace %c by c, i.e. remove the %. *) 468 editString (String.substring(s, 0, i) ^ 469 String.substring(s, i+1, l-i-1)) 470 i (l-1) 471 end 472 val newFormat = editString s 0 (String.size s) 473 val summer = 474 case offset of 475 SOME _ => ~1 476 | NONE => callTiming 5 (Time.toSeconds(toTime date)) 477 handle Size => ~1 478 in 479 callTiming 6 (newFormat, year, month, day, hour, minute, second, 480 dayOfWeek date, yearDay date, summer) 481 handle RunCall.Size => raise Date 482 end 483end; 484 485local 486 (* Install the pretty printer for Date.date. This has to be 487 done outside the structure because of the opaque matching. *) 488 fun pretty _ _ x = PolyML.PrettyString(Date.toString x) 489in 490 val () = PolyML.addPrettyPrinter pretty 491end 492