summaryrefslogtreecommitdiff
path: root/lib/ur/datetime.ur
blob: 9aeab2915017f0e49e5a8b769b74275ec6e8e7b1 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
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 <xml>Invalid day of week {[n]}</xml>

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 <xml>Invalid month number {[n]}</xml>

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)