0 | module IotaTime.Period
  1 |
  2 | import IotaTime.Internal.ApplyPeriod
  3 |
  4 | %default total
  5 |
  6 | ||| A calendar-relative amount applicable to `target`.
  7 | ||| The constructor is hidden so unit capabilities cannot be bypassed.
  8 | export
  9 | record Period (target : Type) where
 10 |   constructor MkPeriod
 11 |   storedYears : Integer
 12 |   storedMonths : Integer
 13 |   storedWeeks : Integer
 14 |   storedDays : Integer
 15 |   storedHours : Integer
 16 |   storedMinutes : Integer
 17 |   storedSeconds : Integer
 18 |   storedNanoseconds : Integer
 19 |
 20 | export
 21 | periodYears : Period target -> Integer
 22 | periodYears (MkPeriod value _ _ _ _ _ _ _) = value
 23 |
 24 | export
 25 | periodMonths : Period target -> Integer
 26 | periodMonths (MkPeriod _ value _ _ _ _ _ _) = value
 27 |
 28 | export
 29 | periodWeeks : Period target -> Integer
 30 | periodWeeks (MkPeriod _ _ value _ _ _ _ _) = value
 31 |
 32 | export
 33 | periodDays : Period target -> Integer
 34 | periodDays (MkPeriod _ _ _ value _ _ _ _) = value
 35 |
 36 | export
 37 | periodHours : Period target -> Integer
 38 | periodHours (MkPeriod _ _ _ _ value _ _ _) = value
 39 |
 40 | export
 41 | periodMinutes : Period target -> Integer
 42 | periodMinutes (MkPeriod _ _ _ _ _ value _ _) = value
 43 |
 44 | export
 45 | periodSeconds : Period target -> Integer
 46 | periodSeconds (MkPeriod _ _ _ _ _ _ value _) = value
 47 |
 48 | export
 49 | periodNanoseconds : Period target -> Integer
 50 | periodNanoseconds (MkPeriod _ _ _ _ _ _ _ value) = value
 51 |
 52 | public export
 53 | Eq (Period target) where
 54 |   MkPeriod leftYears leftMonths leftWeeks leftDays
 55 |     leftHours leftMinutes leftSeconds leftNanoseconds ==
 56 |     MkPeriod rightYears rightMonths rightWeeks rightDays
 57 |       rightHours rightMinutes rightSeconds rightNanoseconds =
 58 |         leftYears == rightYears &&
 59 |         leftMonths == rightMonths &&
 60 |         leftWeeks == rightWeeks &&
 61 |         leftDays == rightDays &&
 62 |         leftHours == rightHours &&
 63 |         leftMinutes == rightMinutes &&
 64 |         leftSeconds == rightSeconds &&
 65 |         leftNanoseconds == rightNanoseconds
 66 |
 67 | public export
 68 | Show (Period target) where
 69 |   show value = "period " ++
 70 |     show (periodYears value) ++ " " ++
 71 |     show (periodMonths value) ++ " " ++
 72 |     show (periodWeeks value) ++ " " ++
 73 |     show (periodDays value) ++ " " ++
 74 |     show (periodHours value) ++ " " ++
 75 |     show (periodMinutes value) ++ " " ++
 76 |     show (periodSeconds value) ++ " " ++
 77 |     show (periodNanoseconds value)
 78 |
 79 | emptyPeriod : Period target
 80 | emptyPeriod = MkPeriod 0 0 0 0 0 0 0 0
 81 |
 82 | public export
 83 | Semigroup (Period target) where
 84 |   left <+> right = MkPeriod
 85 |     (periodYears left + periodYears right)
 86 |     (periodMonths left + periodMonths right)
 87 |     (periodWeeks left + periodWeeks right)
 88 |     (periodDays left + periodDays right)
 89 |     (periodHours left + periodHours right)
 90 |     (periodMinutes left + periodMinutes right)
 91 |     (periodSeconds left + periodSeconds right)
 92 |     (periodNanoseconds left + periodNanoseconds right)
 93 |
 94 | public export
 95 | Monoid (Period target) where
 96 |   neutral = emptyPeriod
 97 |
 98 | ||| Types with calendar-relative date fields.
 99 | public export
100 | interface HasCalendar target where
101 |   0 calendarCapability : ()
102 |
103 | ||| Types with local time-of-day fields.
104 | public export
105 | interface HasTime target where
106 |   0 timeCapability : ()
107 |
108 | ||| Library-owned types to which periods can be applied. The internal target
109 | ||| capability seals this interface against client implementations.
110 | public export
111 | interface PeriodTarget target => ApplyPeriod target where
112 |   ||| Apply all components of a period using iotaTime's rules for the target.
113 |   |||
114 |   ||| For calendar dates, components apply from largest to smallest: years,
115 |   ||| months, weeks, then days. Year and month shifts clamp an invalid day to
116 |   ||| the target month's final day; every shift also clamps at the concrete
117 |   ||| calendar's supported boundaries. Weeks are seven-day shifts. Components
118 |   ||| combined with `<+>` are aggregated before this sequence, so
119 |   ||| `months 1 <+> months 1` applies one two-month shift rather than two
120 |   ||| separately clamped one-month shifts.
121 |   |||
122 |   ||| For `LocalTime`, clock components combine into one signed displacement
123 |   ||| and wrap within the 24-hour day. For `CalendarDateTime`, date components
124 |   ||| apply first as above, then clock components combine into one displacement
125 |   ||| whose signed day carry adjusts the resulting date.
126 |   applyPeriod : Period target -> target -> target
127 |
128 | ||| Construct a period measured in calendar years.
129 | public export
130 | years : HasCalendar target => Integer -> Period target
131 | years value = MkPeriod value 0 0 0 0 0 0 0
132 |
133 | ||| Construct a period measured in calendar months.
134 | public export
135 | months : HasCalendar target => Integer -> Period target
136 | months value = MkPeriod 0 value 0 0 0 0 0 0
137 |
138 | ||| Construct a period measured in seven-day calendar weeks.
139 | public export
140 | weeks : HasCalendar target => Integer -> Period target
141 | weeks value = MkPeriod 0 0 value 0 0 0 0 0
142 |
143 | ||| Construct a period measured in calendar days.
144 | public export
145 | days : HasCalendar target => Integer -> Period target
146 | days value = MkPeriod 0 0 0 value 0 0 0 0
147 |
148 | ||| Construct a period measured in hours.
149 | public export
150 | hours : HasTime target => Integer -> Period target
151 | hours value = MkPeriod 0 0 0 0 value 0 0 0
152 |
153 | ||| Construct a period measured in minutes.
154 | public export
155 | minutes : HasTime target => Integer -> Period target
156 | minutes value = MkPeriod 0 0 0 0 0 value 0 0
157 |
158 | ||| Construct a period measured in seconds.
159 | public export
160 | seconds : HasTime target => Integer -> Period target
161 | seconds value = MkPeriod 0 0 0 0 0 0 value 0
162 |
163 | ||| Construct a period measured in nanoseconds.
164 | public export
165 | nanoseconds : HasTime target => Integer -> Period target
166 | nanoseconds = MkPeriod 0 0 0 0 0 0 0
167 |
168 | ||| Negate every component of a period.
169 | public export
170 | negatePeriod : Period target -> Period target
171 | negatePeriod period = MkPeriod
172 |   (negate (periodYears period))
173 |   (negate (periodMonths period))
174 |   (negate (periodWeeks period))
175 |   (negate (periodDays period))
176 |   (negate (periodHours period))
177 |   (negate (periodMinutes period))
178 |   (negate (periodSeconds period))
179 |   (negate (periodNanoseconds period))
180 |
181 | ||| Multiply every component of a period by an integer.
182 | public export
183 | scalePeriod : Integer -> Period target -> Period target
184 | scalePeriod factor period = MkPeriod
185 |   (factor * periodYears period)
186 |   (factor * periodMonths period)
187 |   (factor * periodWeeks period)
188 |   (factor * periodDays period)
189 |   (factor * periodHours period)
190 |   (factor * periodMinutes period)
191 |   (factor * periodSeconds period)
192 |   (factor * periodNanoseconds period)