0 | module Data.Time.Date
  1 |
  2 | import Data.String
  3 | import Data.Refined.Integer
  4 | import Derive.Prelude
  5 | import Derive.Refined
  6 |
  7 | %default total
  8 | %language ElabReflection
  9 |
 10 | --------------------------------------------------------------------------------
 11 | --          Year
 12 | --------------------------------------------------------------------------------
 13 |
 14 | public export
 15 | record Year where
 16 |   constructor Y
 17 |   year : Integer
 18 |   {auto 0 valid : FromTo 0 9999 year}
 19 |
 20 | %runElab derive "Year" [Show, Eq, Ord, RefinedInteger]
 21 |
 22 | export
 23 | Interpolation Year where
 24 |   interpolate (Y y) = padLeft 4 '0' $ show y
 25 |
 26 | public export
 27 | isLeap : Year -> Bool
 28 | isLeap (Y y) = mod y 4 == 0 && (mod y 100 /= 0 || mod y 400 == 0)
 29 |
 30 | --------------------------------------------------------------------------------
 31 | --          Month
 32 | --------------------------------------------------------------------------------
 33 |
 34 | public export
 35 | data Month : Type where
 36 |   JAN : Month
 37 |   FEB : Month
 38 |   MAR : Month
 39 |   APR : Month
 40 |   MAY : Month
 41 |   JUN : Month
 42 |   JUL : Month
 43 |   AUG : Month
 44 |   SEP : Month
 45 |   OCT : Month
 46 |   NOV : Month
 47 |   DEC : Month
 48 |
 49 | %runElab derive "Month" [Show, Eq, Ord]
 50 |
 51 | export
 52 | Interpolation Month where
 53 |   interpolate m = padLeft 2 '0' $ show (conIndexMonth m + 1)
 54 |
 55 | public export
 56 | DaysInMonth : Month -> Integer
 57 | DaysInMonth JAN = 31
 58 | DaysInMonth FEB = 29
 59 | DaysInMonth MAR = 31
 60 | DaysInMonth APR = 30
 61 | DaysInMonth MAY = 31
 62 | DaysInMonth JUN = 30
 63 | DaysInMonth JUL = 31
 64 | DaysInMonth AUG = 31
 65 | DaysInMonth SEP = 30
 66 | DaysInMonth OCT = 31
 67 | DaysInMonth NOV = 30
 68 | DaysInMonth DEC = 31
 69 |
 70 | public export
 71 | intToMonth : Integer -> Maybe Month
 72 | intToMonth 1  = Just JAN
 73 | intToMonth 2  = Just FEB
 74 | intToMonth 3  = Just MAR
 75 | intToMonth 4  = Just APR
 76 | intToMonth 5  = Just MAY
 77 | intToMonth 6  = Just JUN
 78 | intToMonth 7  = Just JUL
 79 | intToMonth 8  = Just AUG
 80 | intToMonth 9  = Just SEP
 81 | intToMonth 10 = Just OCT
 82 | intToMonth 11 = Just NOV
 83 | intToMonth 12 = Just DEC
 84 | intToMonth _  = Nothing
 85 |
 86 | --------------------------------------------------------------------------------
 87 | --          Day
 88 | --------------------------------------------------------------------------------
 89 |
 90 | public export
 91 | record Day (m : Month) where
 92 |   constructor D
 93 |   day : Integer
 94 |   {auto 0 valid : FromTo 1 (DaysInMonth m) day}
 95 |
 96 | %runElab deriveIndexed "Day" [Show, Eq, Ord]
 97 |
 98 | public export
 99 | refineDay : {m : _} -> Integer -> Maybe (Day m)
100 | refineDay n = case hdec0 {p = FromTo 1 (DaysInMonth m)} n of
101 |   Nothing0 => Nothing
102 |   Just0 v  => Just $ D n
103 |
104 | namespace Day
105 |   public export
106 |   fromInteger :
107 |        {m : _}
108 |     -> (n : Integer)
109 |     -> {auto 0 p : IsJust (refineDay {m} $ cast n)}
110 |     -> Day m
111 |   fromInteger n = fromJust $ refineDay (cast n)
112 |
113 | export
114 | Interpolation (Day m) where
115 |   interpolate (D d) = padLeft 2 '0' $ show d
116 |
117 | --------------------------------------------------------------------------------
118 | --          LocalDate
119 | --------------------------------------------------------------------------------
120 |
121 | public export
122 | record LocalDate where
123 |   constructor MkDate
124 |   year  : Year
125 |   month : Month
126 |   day   : Day month
127 |
128 | public export
129 | Eq LocalDate where
130 |   MkDate y1 m1 d1 == MkDate y2 m2 d2 =
131 |     y1 == y2 && m1 == m2  && d1.day == d2.day
132 |
133 | public export
134 | Ord LocalDate where
135 |   compare (MkDate y1 m1 d1) (MkDate y2 m2 d2) =
136 |     if y1 /= y2 then compare y1 y2
137 |     else if m1 /= m2 then compare m1 m2
138 |     else compare d1.day d2.day
139 |
140 | %runElab derive "LocalDate" [Show]
141 |
142 | export
143 | Interpolation LocalDate where
144 |   interpolate (MkDate y m d) = "\{y}-\{m}-\{d}"
145 |
146 | --------------------------------------------------------------------------------
147 | --          Tests
148 | --------------------------------------------------------------------------------
149 |
150 | testYear : Year
151 | testYear = 2022
152 |