Mercurial > urweb
changeset 1977:50322ba22972
Add datetime functions for adding time intervals.
author | Patrick Hurst <phurst@mit.edu> |
---|---|
date | Mon, 09 Dec 2013 19:19:12 -0500 (2013-12-10) |
parents | 98bb0e952a11 |
children | c5143edaf3c7 |
files | lib/ur/datetime.ur lib/ur/datetime.urs |
diffstat | 2 files changed, 32 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/lib/ur/datetime.ur Sun Dec 08 13:14:58 2013 -0500 +++ b/lib/ur/datetime.ur Mon Dec 09 19:19:12 2013 -0500 @@ -102,6 +102,9 @@ 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 = @@ -115,7 +118,27 @@ | 6 => Saturday | n => error <xml>Illegal day of week {[n]}</xml> - 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)
--- a/lib/ur/datetime.urs Sun Dec 08 13:14:58 2013 -0500 +++ b/lib/ur/datetime.urs Mon Dec 09 19:19:12 2013 -0500 @@ -14,6 +14,8 @@ Second : int } +val ord_datetime : ord t + val show_day_of_week : show day_of_week val show_month : show month val eq_day_of_week : eq day_of_week @@ -28,3 +30,9 @@ val format : string -> t -> string val dayOfWeek : t -> day_of_week val now : transaction t +val normalize : t -> t + +val addSeconds : int -> t -> t +val addMinutes : int -> t -> t +val addHours : int -> t -> t +val addDays : int -> t -> t