0 | module Data.Time.Time
  1 |
  2 | import public Data.Nat
  3 | import public Data.Refined
  4 | import public Data.Time.Date
  5 | import public Data.Refined.Integer
  6 | import Data.String
  7 | import Derive.Prelude
  8 | import Derive.Refined
  9 |
 10 | %default total
 11 | %language ElabReflection
 12 |
 13 | --------------------------------------------------------------------------------
 14 | --          Hour
 15 | --------------------------------------------------------------------------------
 16 |
 17 | public export
 18 | record Hour where
 19 |   constructor H
 20 |   hour : Integer
 21 |   {auto 0 valid : FromTo 0 23 hour}
 22 |
 23 | namespace Hour
 24 |   %runElab derive "Hour" [Show, Eq, Ord, RefinedInteger]
 25 |
 26 |   export
 27 |   Interpolation Hour where
 28 |     interpolate (H h) = padLeft 2 '0' $ show h
 29 |
 30 | --------------------------------------------------------------------------------
 31 | --          Minute
 32 | --------------------------------------------------------------------------------
 33 |
 34 | public export
 35 | record Minute where
 36 |   constructor M
 37 |   minute : Integer
 38 |   {auto 0 valid : FromTo 0 59 minute}
 39 |
 40 | namespace Minute
 41 |   %runElab derive "Minute" [Show, Eq, Ord, RefinedInteger]
 42 |
 43 |   export
 44 |   Interpolation Minute where
 45 |     interpolate (M m) = padLeft 2 '0' $ show m
 46 |
 47 | --------------------------------------------------------------------------------
 48 | --          Second
 49 | --------------------------------------------------------------------------------
 50 |
 51 | public export
 52 | record Second where
 53 |   constructor S
 54 |   second : Integer
 55 |   {auto 0 valid : FromTo 0 60 second}
 56 |
 57 | namespace Second
 58 |   %runElab derive "Second" [Show, Eq, Ord, RefinedInteger]
 59 |
 60 |   export
 61 |   Interpolation Second where
 62 |     interpolate (S s) = padLeft 2 '0' $ show s
 63 |
 64 | --------------------------------------------------------------------------------
 65 | --          MicroSecond
 66 | --------------------------------------------------------------------------------
 67 |
 68 | public export
 69 | record MicroSecond where
 70 |   constructor MS
 71 |   us : Integer
 72 |   {auto 0 valid : FromTo 0 999_999 us}
 73 |
 74 | namespace MicroSecond
 75 |   %runElab derive "MicroSecond" [Show, Eq, Ord, RefinedInteger]
 76 |
 77 |   export
 78 |   Interpolation MicroSecond where
 79 |     interpolate (MS n) = padLeft 6 '0' $ show n
 80 |
 81 | --------------------------------------------------------------------------------
 82 | --          LocalTime
 83 | --------------------------------------------------------------------------------
 84 |
 85 | public export
 86 | record LocalTime where
 87 |   constructor LT
 88 |   hour   : Hour
 89 |   minute : Minute
 90 |   second : Second
 91 |   prec   : Maybe MicroSecond
 92 |
 93 | %runElab derive "LocalTime" [Show, Eq, Ord]
 94 |
 95 | export
 96 | Interpolation LocalTime where
 97 |   interpolate (LT h m s ms) =
 98 |     let mss := maybe "" (\x => ".\{x}") ms
 99 |      in "\{h}:\{m}:\{s}\{mss}"
100 |
101 | --------------------------------------------------------------------------------
102 | --          Sign
103 | --------------------------------------------------------------------------------
104 |
105 | public export
106 | data Sign = Minus | Plus
107 |
108 | %runElab derive "Sign" [Show, Eq, Ord]
109 |
110 | export
111 | Interpolation Sign where
112 |   interpolate Minus = "-"
113 |   interpolate Plus  = "+"
114 |
115 | --------------------------------------------------------------------------------
116 | --          Offset
117 | --------------------------------------------------------------------------------
118 |
119 | public export
120 | data Offset : Type where
121 |   Z : Offset
122 |   O : (sign : Sign) -> (h : Hour) -> (m : Minute) -> Offset
123 |
124 | %runElab derive "Offset" [Show, Eq]
125 |
126 | export
127 | Interpolation Offset where
128 |   interpolate Z = "Z"
129 |   interpolate (O sign h m) = "\{sign}\{h}:\{m}"
130 |
131 | --------------------------------------------------------------------------------
132 | --          OffsetTime
133 | --------------------------------------------------------------------------------
134 |
135 | public export
136 | record OffsetTime where
137 |   constructor OT
138 |   time   : LocalTime
139 |   offset : Offset
140 |
141 | %runElab derive "OffsetTime" [Show, Eq]
142 |
143 | export
144 | Interpolation OffsetTime where
145 |   interpolate (OT t o) = "\{t}\{o}"
146 |
147 | --------------------------------------------------------------------------------
148 | --          DateTime
149 | --------------------------------------------------------------------------------
150 |
151 | public export
152 | record LocalDateTime where
153 |   constructor LDT
154 |   date : LocalDate
155 |   time : LocalTime
156 |
157 | %runElab derive "LocalDateTime" [Show, Eq]
158 |
159 | export
160 | Interpolation LocalDateTime where
161 |   interpolate (LDT d t) = "\{d}T\{t}"
162 |
163 | public export
164 | record OffsetDateTime where
165 |   constructor ODT
166 |   date : LocalDate
167 |   time : OffsetTime
168 |
169 | %runElab derive "OffsetDateTime" [Show, Eq]
170 |
171 | export
172 | Interpolation OffsetDateTime where
173 |   interpolate (ODT d t) = "\{d}T\{t}"
174 |
175 | --------------------------------------------------------------------------------
176 | --          AnyTime
177 | --------------------------------------------------------------------------------
178 |
179 | public export
180 | data AnyTime : Type where
181 |   ATLocalDate      : LocalDate -> AnyTime
182 |   ATLocalTime      : LocalTime -> AnyTime
183 |   ATLocalDateTime  : LocalDateTime -> AnyTime
184 |   ATOffsetDateTime : OffsetDateTime -> AnyTime
185 |
186 | %runElab derive "AnyTime" [Show, Eq]
187 |
188 | export
189 | getDate : AnyTime -> Maybe LocalDate
190 | getDate (ATLocalDate x)      = Just x
191 | getDate (ATLocalTime x)      = Nothing
192 | getDate (ATLocalDateTime x)  = Just x.date
193 | getDate (ATOffsetDateTime x) = Just x.date
194 |
195 | export
196 | extraCheckDate : AnyTime -> Either LocalDate AnyTime
197 | extraCheckDate at =
198 |   case getDate at of
199 |     Nothing                => Right at
200 |     Just (MkDate y FEB 29) =>
201 |       if isLeap y then Right at else Left (MkDate y FEB 29)
202 |     Just d                 => Right at
203 |
204 | export
205 | Interpolation AnyTime where
206 |   interpolate (ATLocalDate x)       = interpolate x
207 |   interpolate (ATLocalTime x)      = interpolate x
208 |   interpolate (ATLocalDateTime x)  = interpolate x
209 |   interpolate (ATOffsetDateTime x) = interpolate x
210 |