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