Waysys on the Web
(*
Class: WayDate
Package: com.waysysweb.util
Author: W. Shaffer
Date: 28-Nov-1997
Description:
This structure provides specifications for algorithms for manipulating
dates.
Maintenance:
Date Author Description
----------- ------ ----------------------------------------------------------------
28-Nov-1997 Shaffer File created
23-Feb-1998 Shaffer Day Positions added to support time zones
12-Mar-1998 Shaffer Day Position functions added to support daylight savings time
30-Jan-2000 Shaffer Adjustment to accommodate Version 1.44 of Moscow ML
31-May-2003 Shaffer Addition of age and currentAge functions
01-Aug-2005 Shaffer Addition of daysInPolicyYear for insurance applications
04-Apr-2006 Shaffer Added minDate function
05-Apr-2006 Shaffer Added anniversary methods
11-Nov-2006 Shaffer Moved holiday functions to separate structure
07-Jan-2007 Shaffer Moved insurance date manipulations to separate structure
*)
structure WAYDATE = struct
(*============ Exceptions ==============================================*)
exception DateError;
(*============ Types ==============================================*)
type Month = int;
type Day = int;
type Year = int;
type DayOfYear = int;
(* Days of the Week *)
datatype DayOfWeek = Sunday | Monday | Tuesday | Wednesday | Thursday |
Friday | Saturday;
(*============ Constants ==============================================*)
(* Maximum allowed year *)
val MaxYear : Year = 3999;
(* Minimum allowed year *)
val MinYear : Year = 1601;
(* Convert Day of Week to int *)
fun numDayOfWeek(Sunday) : int = 0
| numDayOfWeek(Monday) : int = 1
| numDayOfWeek(Tuesday) : int = 2
| numDayOfWeek(Wednesday) : int = 3
| numDayOfWeek(Thursday) : int = 4
| numDayOfWeek(Friday) : int = 5
| numDayOfWeek(Saturday) : int = 6;
(* Convert int to Day of Week *)
fun dayOfWeekEnum(0) = Sunday
| dayOfWeekEnum(1) = Monday
| dayOfWeekEnum(2) = Tuesday
| dayOfWeekEnum(3) = Wednesday
| dayOfWeekEnum(4) = Thursday
| dayOfWeekEnum(5) = Friday
| dayOfWeekEnum(6) = Saturday
| dayOfWeekEnum(_) = raise DateError;
(* Days of the month: non-leap year *)
fun daysNonLeapYear(1) = 31 (* January *)
| daysNonLeapYear(2) = 28 (* February *)
| daysNonLeapYear(3) = 31 (* March *)
| daysNonLeapYear(4) = 30 (* April *)
| daysNonLeapYear(5) = 31 (* May *)
| daysNonLeapYear(6) = 30 (* June *)
| daysNonLeapYear(7) = 31 (* July *)
| daysNonLeapYear(8) = 31 (* August *)
| daysNonLeapYear(9) = 30 (* September*)
| daysNonLeapYear(10)= 31 (* October *)
| daysNonLeapYear(11)= 30 (* November *)
| daysNonLeapYear(12)= 31 (* December *)
| daysNonLeapYear(_) = raise DateError;
(* Days of the month: leap year *)
fun daysLeapYear(1) = 31 (* January *)
| daysLeapYear(2) = 29 (* February *)
| daysLeapYear(3) = 31 (* March *)
| daysLeapYear(4) = 30 (* April *)
| daysLeapYear(5) = 31 (* May *)
| daysLeapYear(6) = 30 (* June *)
| daysLeapYear(7) = 31 (* July *)
| daysLeapYear(8) = 31 (* August *)
| daysLeapYear(9) = 30 (* September*)
| daysLeapYear(10)= 31 (* October *)
| daysLeapYear(11)= 30 (* November *)
| daysLeapYear(12)= 31 (* December *)
| daysLeapYear(_) = raise DateError;
(* The abbreviations of months *)
fun mnthAbbrev(1) = "Jan"
| mnthAbbrev(2) = "Feb"
| mnthAbbrev(3) = "Mar"
| mnthAbbrev(4) = "Apr"
| mnthAbbrev(5) = "May"
| mnthAbbrev(6) = "Jun"
| mnthAbbrev(7) = "Jul"
| mnthAbbrev(8) = "Aug"
| mnthAbbrev(9) = "Sep"
| mnthAbbrev(10) = "Oct"
| mnthAbbrev(11) = "Nov"
| mnthAbbrev(12) = "Dec"
| mnthAbbrev(_) = raise DateError;
(* Is leap year *)
fun isLeapYear(yr : Year) : bool =
if ( (yr mod 400) = 0) orelse (( (yr mod 4) = 0) andalso ((yr mod 100) <> 0))
then true
else false;
(* Days in year *)
fun daysInYear(yr : Year) : DayOfYear =
if isLeapYear(yr)
then 366
else 365;
val MaxDate = (12, 31, MaxYear);
val MinDate = (01, 01, MinYear);
(*============ Properties ==============================================*)
(* Valid month *)
fun isMonth(mnth : Month) : bool =
if (mnth > 0) andalso (mnth <= 12)
then true
else false;
(* Valid year *)
fun isYear(yr : Year) : bool =
if (yr >= MinYear) andalso (yr <= MaxYear)
then true
else false;
(* Days in month *)
fun daysInMonth(mnth : Month, yr : Year) : Day =
if isLeapYear(yr)
then daysLeapYear(mnth)
else daysNonLeapYear(mnth);
(* Is valid day *)
fun isValidDay(mnth : Month, dy : Day, yr : Year) : bool =
if (dy > 0) andalso (dy <= daysInMonth(mnth, yr))
then true
else false;
(* Valid date *)
fun isValidDate(mnth : Month, dy : Day, yr : Year) : bool =
if isMonth(mnth) andalso isYear(yr) andalso isValidDay(mnth, dy, yr)
then true
else false;
(* Is day of year *)
fun isDayOfYear(dayOfYear : DayOfYear, yr : Year) : bool =
if (dayOfYear > 0) andalso (dayOfYear <= daysInYear(yr))
then true
else false;
(*============ Attributes ==============================================*)
type WayDate = Month * Day * Year;
(*============ Invariant ==============================================*)
fun inv_WayDate(mn : Month, dy : Day, yr : Year) : bool =
isValidDate(mn, dy, yr);
(*============ Initialization ===========================================*)
(* Create a date *)
(* Precondition: (none) *)
fun create(mnth : Month, dy : Day, yr : Year) : WayDate =
if isValidDate(mnth, dy, yr)
then (mnth, dy, yr)
else raise DateError;
(* Return today's date *)
fun today() : WayDate =
let
val aDate =
Date.fromTimeLocal(TIME.now());
fun fromMonth(DATE.Jan) = 1
| fromMonth(DATE.Feb) = 2
| fromMonth(DATE.Mar) = 3
| fromMonth(DATE.Apr) = 4
| fromMonth(DATE.May) = 5
| fromMonth(DATE.Jun) = 6
| fromMonth(DATE.Jul) = 7
| fromMonth(DATE.Aug) = 8
| fromMonth(DATE.Sep) = 9
| fromMonth(DATE.Oct) = 10
| fromMonth(DATE.Nov) = 11
| fromMonth(DATE.Dec) = 12;
in
create(fromMonth(Date.month aDate), Date.day aDate, Date.year aDate)
end;
(*============ Operations ==============================================*)
(* Obtain attributes *)
fun getDay(_, dy, _) : Day = dy; (* day part of date *)
fun getMonth(mnth, _, _) : Month = mnth; (* month part of date*)
fun getYear(_, _, yr) : Year = yr; (* year part of date *)
(* Sum the days of the month *)
fun sumDaysOfMonth( 1, yr : Year) : int = daysInMonth(1, yr)
| sumDaysOfMonth(mnth : Month, yr : Year) : int =
daysInMonth(mnth, yr) + sumDaysOfMonth(mnth-1, yr);
(* Day of year *)
fun dayOfYear( 1, dy : Day, _ ) : DayOfYear =
dy
| dayOfYear(mnth : Month, dy : Day, yr : Year) : DayOfYear =
sumDaysOfMonth(mnth - 1, yr) + dy;
(* Days in prior years *)
fun daysInPriorYears(1601) : int = 0
| daysInPriorYears(yr : Year) : int =
daysInYear(yr - 1) + daysInPriorYears(yr - 1);
(* Add one day to the date *)
fun increment(12, 31, 3999) : WayDate =
raise DateError
| increment(12, 31, yr : Year) : WayDate =
(1, 1, yr + 1)
| increment(mnth : Month, dy : Day, yr : Year) : WayDate =
if dy = daysInMonth(mnth, yr)
then (mnth + 1, 1, yr)
else (mnth , dy + 1, yr);
(* Subtract one day from the date *)
fun decrement(1, 1, 1601) : WayDate =
raise DateError
| decrement(1, 1, yr : Month) : WayDate =
(12, 31, yr - 1)
| decrement(mnth : Month, 1, yr : Year) : WayDate =
(mnth - 1, daysInMonth(mnth - 1, yr), yr)
| decrement(mnth : Month, dy : Day, yr : Year) : WayDate =
(mnth, dy - 1, yr);
(* Add a number of days to a date *)
fun add(date1 : WayDate, value : int) : WayDate =
if value = 0
then date1
else
if value < 0
then add(decrement(date1), value + 1)
else add(increment(date1), value - 1);
(* Convert Julian to Gregorian Date *)
fun convertGregorian(dayInYear : DayOfYear, yr : Year) : WayDate =
if isDayOfYear(dayInYear, yr)
then add(create(1, 1, yr), dayInYear - 1)
else raise DateError;
(* Compare *)
fun compare(date1 : WayDate, date2 : WayDate) : order =
let
val yr1 = getYear(date1)
val yr2 = getYear(date2)
val mnth1 = getMonth(date1)
val mnth2 = getMonth(date2)
val dy1 = getDay(date1)
val dy2 = getDay(date2)
in
if yr1 < yr2 then LESS
else if yr1 = yr2 andalso mnth1 < mnth2 then LESS
else if yr1 = yr2 andalso mnth1 = mnth2 andalso dy1 < dy2 then LESS
else if yr1 = yr2 andalso mnth1 = mnth2 andalso dy1 = dy2 then EQUAL
else GREATER
end;
(* isEqual - are two dates equal *)
fun isEqual(date1 : WayDate, date2 : WayDate) : bool =
if (compare(date1, date2) = EQUAL) then true
else false;
(* Return the earliest of two dates *)
fun minDate(date1 : WayDate, date2 : WayDate) : WayDate =
case compare(date1, date2) of
LESS => date1
| EQUAL => date1
| GREATER => date2;
(* Return the later of two dates *)
fun maxDate(date1 : WayDate, date2 : WayDate) : WayDate =
case compare(date1, date2) of
LESS => date2
| EQUAL => date2
| GREATER => date1;
(* is in period *)
fun isInPeriod(begin_date : WayDate, end_date : WayDate, date1 : WayDate) : bool =
let
val bgn_cmp = compare(begin_date, date1);
val end_cmp = compare(end_date , date1);
in
if bgn_cmp = GREATER then false
else if end_cmp = LESS then false
else true
end;
(* Date Difference: date1 - date2 *)
fun difference(date1 : WayDate, date2 : WayDate) : int =
case compare(date1, date2) of
EQUAL => 0
| LESS => difference(increment(date1), date2) - 1
| GREATER => difference(decrement(date1), date2) + 1;
(* Day of week *)
(* This specification is based on 1-1-1601 being a Monday (1) *)
(* Precondition: isValidDate(getMonth(date1), getDay(date1), getYear(date1)) *)
fun dayOfWeek(date1 : WayDate) : DayOfWeek =
dayOfWeekEnum((difference(date1, (1, 1, MinYear)) + 1) mod 7);
(* Convert a date to a string *)
fun toString(mnth : Month, dy : Day, yr : Year) : string =
makestring(dy) ^ "-" ^ mnthAbbrev(mnth) ^ "-" ^ makestring(yr);
end (* WAYDATE *)
