Mercurial > urweb

annotate lib/ur/datetime.ur @ 2161:af3f5b58aed2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add a missed case in CoreUtil.Exp fold
author Adam Chlipala <adam@chlipala.net>
date Sun, 05 Jul 2015 16:11:24 -0400
parents abb6981a2c4c
children
rev   line source
phurst@1974 1 datatype day_of_week = Sunday | Monday | Tuesday | Wednesday | Thursday |
phurst@1974 2 Friday | Saturday
phurst@1974 3
phurst@1974 4 val show_day_of_week = mkShow (fn dow => case dow of
phurst@1974 5 Sunday => "Sunday"
phurst@1974 6 | Monday => "Monday"
phurst@1974 7 | Tuesday => "Tuesday"
phurst@1974 8 | Wednesday => "Wednesday"
phurst@1974 9 | Thursday => "Thursday"
phurst@1974 10 | Friday => "Friday"
phurst@1974 11 | Saturday => "Saturday")
phurst@1974 12
phurst@1974 13 fun dayOfWeekToInt dow = case dow of
phurst@1974 14 Sunday => 0
phurst@1974 15 | Monday => 1
phurst@1974 16 | Tuesday => 2
phurst@1974 17 | Wednesday => 3
phurst@1974 18 | Thursday => 4
phurst@1974 19 | Friday => 5
phurst@1974 20 | Saturday => 6
phurst@1974 21
phurst@1974 22 fun intToDayOfWeek i = case i of
phurst@1974 23 0 => Sunday
phurst@1974 24 | 1 => Monday
phurst@1974 25 | 2 => Tuesday
phurst@1974 26 | 3 => Wednesday
phurst@1974 27 | 4 => Thursday
phurst@1974 28 | 5 => Friday
phurst@1974 29 | 6 => Saturday
phurst@1974 30 | n => error <xml>Invalid day of week {[n]}</xml>
phurst@1974 31
phurst@1974 32 val eq_day_of_week = mkEq (fn a b => dayOfWeekToInt a = dayOfWeekToInt b)
phurst@1974 33
phurst@1974 34
phurst@1974 35 datatype month = January | February | March | April | May | June | July |
phurst@1974 36 August | September | October | November | December
phurst@1974 37
phurst@1974 38 val show_month = mkShow (fn m => case m of
phurst@1974 39 January => "January"
phurst@1974 40 | February => "February"
phurst@1974 41 | March => "March"
phurst@1974 42 | April => "April"
phurst@1974 43 | May => "May"
phurst@1974 44 | June => "June"
phurst@1974 45 | July => "July"
phurst@1974 46 | August => "August"
phurst@1974 47 | September => "September"
phurst@1974 48 | October => "October"
phurst@1974 49 | November => "November"
phurst@1974 50 | December => "December")
phurst@1974 51
phurst@1974 52 type t = {
phurst@1972 53 Year : int,
phurst@1974 54 Month : month,
phurst@1972 55 Day : int,
phurst@1972 56 Hour : int,
phurst@1972 57 Minute : int,
phurst@1972 58 Second : int
phurst@1972 59 }
phurst@1972 60
phurst@1974 61 fun monthToInt m = case m of
phurst@1974 62 January => 0
phurst@1974 63 | February => 1
phurst@1974 64 | March => 2
phurst@1974 65 | April => 3
phurst@1974 66 | May => 4
phurst@1974 67 | June => 5
phurst@1974 68 | July => 6
phurst@1974 69 | August => 7
phurst@1974 70 | September => 8
phurst@1974 71 | October => 9
phurst@1974 72 | November => 10
phurst@1974 73 | December => 11
phurst@1973 74
phurst@1974 75 fun intToMonth i = case i of
phurst@1974 76 0 => January
phurst@1974 77 | 1 => February
phurst@1974 78 | 2 => March
phurst@1974 79 | 3 => April
phurst@1974 80 | 4 => May
phurst@1974 81 | 5 => June
phurst@1974 82 | 6 => July
phurst@1974 83 | 7 => August
phurst@1974 84 | 8 => September
phurst@1974 85 | 9 => October
phurst@1974 86 | 10 => November
phurst@1974 87 | 11 => December
phurst@1974 88 | n => error <xml>Invalid month number {[n]}</xml>
phurst@1973 89
phurst@1974 90 val eq_month = mkEq (fn a b => monthToInt a = monthToInt b)
phurst@1974 91
phurst@1974 92
phurst@1974 93 fun toTime dt : time = fromDatetime dt.Year (monthToInt dt.Month) dt.Day
phurst@1972 94 dt.Hour dt.Minute dt.Second
phurst@1972 95
phurst@1976 96 fun fromTime t : t = {
phurst@1972 97 Year = datetimeYear t,
phurst@1974 98 Month = intToMonth (datetimeMonth t),
phurst@1972 99 Day = datetimeDay t,
phurst@1972 100 Hour = datetimeHour t,
phurst@1972 101 Minute = datetimeMinute t,
phurst@1972 102 Second = datetimeSecond t
phurst@1972 103 }
phurst@1972 104
phurst@1977 105 val ord_datetime = mkOrd { Lt = fn a b => toTime a < toTime b,
phurst@1977 106 Le = fn a b => toTime a <= toTime b }
phurst@1977 107
phurst@1974 108 fun format fmt dt : string = timef fmt (toTime dt)
phurst@1974 109
adam@1988 110 fun dayOfWeek dt : day_of_week = intToDayOfWeek (datetimeDayOfWeek (toTime dt))
phurst@1974 111
phurst@1976 112 val now : transaction t =
phurst@1972 113 n <- now;
phurst@1972 114 return (fromTime n)
phurst@1977 115
phurst@1977 116 (* Normalize a datetime. This will convert, e.g., January 32nd into February
phurst@1977 117 1st. *)
phurst@1977 118
phurst@1977 119 fun normalize dt = fromTime (toTime dt)
phurst@1977 120 fun addToField [nm :: Name] [rest ::: {Type}] [[nm] ~ rest]
phurst@1977 121 (delta : int) (r : $([nm = int] ++ rest))
phurst@1977 122 : $([nm = int] ++ rest) =
phurst@1977 123 (r -- nm) ++ {nm = r.nm + delta}
phurst@1977 124
phurst@1977 125
phurst@1977 126 (* Functions for adding to a datetime. There is no addMonths or addYears since
phurst@1977 127 it's not clear what should be done; what's 1 month after January 31, or 1
phurst@1977 128 year after February 29th?
phurst@1977 129
phurst@1977 130 These can't all be defined in terms of addSeconds because of leap seconds. *)
phurst@1977 131
phurst@1977 132 fun addSeconds n dt = normalize (addToField [#Second] n dt)
phurst@1977 133 fun addMinutes n dt = normalize (addToField [#Minute] n dt)
phurst@1977 134 fun addHours n dt = normalize (addToField [#Hour] n dt)
phurst@1977 135 fun addDays n dt = normalize (addToField [#Day] n dt)