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