# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1297359560 18000
# Node ID 4385bc6a0d2d05963991ff074ee7f6ccd1919eaf
# Parent  377c11586999e5d6fc7c653e3933efa019675e42
Some Datebox functions related to dates

diff -r 377c11586999 -r 4385bc6a0d2d datebox.ur
--- a/datebox.ur	Tue Feb 08 16:52:29 2011 -0500
+++ b/datebox.ur	Thu Feb 10 12:39:20 2011 -0500
@@ -10,6 +10,10 @@
 datatype month = Prev | This | Next
 
 type date = {Year : int, Month : int, Day : int}
+val date_ord = mkOrd {Lt = fn {Year = y1, Month = m1, Day = d1} {Year = y2, Month = m2, Day = d2} =>
+                              y1 < y2 || (y1 = y2 && m1 < m2) || (y1 = y2 && m1 = m2 && d1 < d2),
+                      Le = fn {Year = y1, Month = m1, Day = d1} {Year = y2, Month = m2, Day = d2} =>
+                              y1 < y2 || (y1 = y2 && m1 < m2) || (y1 = y2 && m1 = m2 && d1 <= d2)}
 
 type t = {Month : source {ThisMonth : int, Year : int,
                           ThisMonthLength : int, PrevMonthLength : int,
@@ -31,6 +35,8 @@
         pad' (len - String.length s) s
     end
 
+fun time {Year = y, Month = m, Day = d} = readError (show y ^ "-" ^ pad 2 m ^ "-" ^ pad 2 d ^ " 00:00:00")
+
 fun monthLen m =
     let
         fun f n tm =
diff -r 377c11586999 -r 4385bc6a0d2d datebox.urs
--- a/datebox.urs	Tue Feb 08 16:52:29 2011 -0500
+++ b/datebox.urs	Thu Feb 10 12:39:20 2011 -0500
@@ -1,6 +1,8 @@
 type t
 
 type date = {Year : int, Month : int, Day : int}
+val date_ord : ord date
+val time : date -> time
 
 val create : time -> transaction t
 val render : t -> xbody