summaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorGravatar Patrick Hurst <phurst@mit.edu>2013-12-09 19:19:12 -0500
committerGravatar Patrick Hurst <phurst@mit.edu>2013-12-09 19:19:12 -0500
commit9dd4f9479ae62645b9150b37d3ae42512d1efff1 (patch)
tree0a574cf4e3535ecd0b595208fa4fd8ca35a5bf37 /lib
parente77a9942be6069301a0786f20646afa8a7dcd4f5 (diff)
Add datetime functions for adding time intervals.
Diffstat (limited to 'lib')
-rw-r--r--lib/ur/datetime.ur25
-rw-r--r--lib/ur/datetime.urs8
2 files changed, 32 insertions, 1 deletions
diff --git a/lib/ur/datetime.ur b/lib/ur/datetime.ur
index dbc68da1..676f141f 100644
--- a/lib/ur/datetime.ur
+++ b/lib/ur/datetime.ur
@@ -102,6 +102,9 @@ fun fromTime t : 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 =
@@ -115,7 +118,27 @@ fun dayOfWeek dt : day_of_week =
| 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)
diff --git a/lib/ur/datetime.urs b/lib/ur/datetime.urs
index 26ee795a..972f86bf 100644
--- a/lib/ur/datetime.urs
+++ b/lib/ur/datetime.urs
@@ -14,6 +14,8 @@ type t = {
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 fromTime : time -> t
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