changeset 5:4385bc6a0d2d

Some Datebox functions related to dates
author Adam Chlipala <adam@chlipala.net>
date Thu, 10 Feb 2011 12:39:20 -0500
parents 377c11586999
children f17b869fbb71
files datebox.ur datebox.urs
diffstat 2 files changed, 8 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- 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 =
--- 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