From 9dd4f9479ae62645b9150b37d3ae42512d1efff1 Mon Sep 17 00:00:00 2001
From: Patrick Hurst <phurst@mit.edu>
Date: Mon, 9 Dec 2013 19:19:12 -0500
Subject: Add datetime functions for adding time intervals.

---
 lib/ur/datetime.ur  | 25 ++++++++++++++++++++++++-
 lib/ur/datetime.urs |  8 ++++++++
 2 files changed, 32 insertions(+), 1 deletion(-)

(limited to 'lib')

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
-- 
cgit v1.2.3