datatype day_of_week = Sunday | Monday | Tuesday | Wednesday | Thursday | Friday | Saturday val show_day_of_week = mkShow (fn dow => case dow of Sunday => "Sunday" | Monday => "Monday" | Tuesday => "Tuesday" | Wednesday => "Wednesday" | Thursday => "Thursday" | Friday => "Friday" | Saturday => "Saturday") fun dayOfWeekToInt dow = case dow of Sunday => 0 | Monday => 1 | Tuesday => 2 | Wednesday => 3 | Thursday => 4 | Friday => 5 | Saturday => 6 fun intToDayOfWeek i = case i of 0 => Sunday | 1 => Monday | 2 => Tuesday | 3 => Wednesday | 4 => Thursday | 5 => Friday | 6 => Saturday | n => error Invalid day of week {[n]} val eq_day_of_week = mkEq (fn a b => dayOfWeekToInt a = dayOfWeekToInt b) datatype month = January | February | March | April | May | June | July | August | September | October | November | December val show_month = mkShow (fn m => case m of January => "January" | February => "February" | March => "March" | April => "April" | May => "May" | June => "June" | July => "July" | August => "August" | September => "September" | October => "October" | November => "November" | December => "December") type t = { Year : int, Month : month, Day : int, Hour : int, Minute : int, Second : int } fun monthToInt m = case m of January => 0 | February => 1 | March => 2 | April => 3 | May => 4 | June => 5 | July => 6 | August => 7 | September => 8 | October => 9 | November => 10 | December => 11 fun intToMonth i = case i of 0 => January | 1 => February | 2 => March | 3 => April | 4 => May | 5 => June | 6 => July | 7 => August | 8 => September | 9 => October | 10 => November | 11 => December | n => error Invalid month number {[n]} val eq_month = mkEq (fn a b => monthToInt a = monthToInt b) fun toTime dt : time = fromDatetime dt.Year (monthToInt dt.Month) dt.Day dt.Hour dt.Minute dt.Second fun fromTime t : t = { Year = datetimeYear t, Month = intToMonth (datetimeMonth t), Day = datetimeDay t, Hour = datetimeHour t, Minute = datetimeMinute t, Second = datetimeSecond t } val ord_datetime = mkOrd { Lt = fn a b => toTime a < toTime b, Le = fn a b => toTime a <= toTime b } fun format fmt dt : string = timef fmt (toTime dt) fun dayOfWeek dt : day_of_week = intToDayOfWeek (datetimeDayOfWeek (toTime dt)) val now : transaction t = n <- now; return (fromTime n) (* Normalize a datetime. This will convert, e.g., January 32nd into February 1st. *) fun normalize dt = fromTime (toTime dt) fun addToField [nm :: Name] [rest ::: {Type}] [[nm] ~ rest] (delta : int) (r : $([nm = int] ++ rest)) : $([nm = int] ++ rest) = (r -- nm) ++ {nm = r.nm + delta} (* Functions for adding to a datetime. There is no addMonths or addYears since it's not clear what should be done; what's 1 month after January 31, or 1 year after February 29th? These can't all be defined in terms of addSeconds because of leap seconds. *) fun addSeconds n dt = normalize (addToField [#Second] n dt) fun addMinutes n dt = normalize (addToField [#Minute] n dt) fun addHours n dt = normalize (addToField [#Hour] n dt) fun addDays n dt = normalize (addToField [#Day] n dt)