depdate.hs

module Date

-- leap year ?
leap : Integer -> Bool
leap year = (mod year 4 == 0) && ((mod year 400 == 0) || not (mod year 100 == 0))

-- number of days in month/year
days : Integer -> Integer -> Integer
days 2     year = if leap year then 29 else 28 
days month _    = if month `List.elem` [4,6,9,11] then 30 else 31

-- is day within bounds for month/year ?                                                       
inBounds : Integer -> Integer -> Integer -> Bool
inBounds day month year = day >= 1 && day <= days month year 

-- Date datatype 
-- a value of type: so (inBounds d m y),
-- can only be constructed if: (inBounds d m y) == True
data Date : Integer -> Integer -> Integer -> Type where
   mkDate : (d:Integer) -> (m:Integer) -> (y:Integer) -> so (inBounds d m y)
            -> Date d m y

-- making a new date succeeds if (d,m,y) is valid or is an error
newDate : (d:Integer) -> (m:Integer) -> (y:Integer) -> Either (Date d m y) String
newDate d m y = case choose (inBounds d m y) of
                     Left prf => Left (mkDate d m y prf)
                     Right _  => Right ("Day: " ++ show d ++ " is out of bounds!")

date1 : Either (Date 29 2 1980) String
date1 = newDate 29 2 1980 -- Left (mkDate 29 2 1980 oh) 

date2 : Either (Date 29 2 1981) String
date2 = newDate 29 2 1981 -- Right "Day: 29 is out of bounds!"