0 | module IotaTime.LocalTime
  1 |
  2 | import public IotaTime.Time.Component
  3 | import IotaTime.Internal.ApplyPeriod
  4 | import IotaTime.Period
  5 |
  6 | %default total
  7 |
  8 | nanosPerSecond : Integer
  9 | nanosPerSecond = 1000000000
 10 |
 11 | nanosPerDay : Integer
 12 | nanosPerDay = 86400 * nanosPerSecond
 13 |
 14 | ||| An opaque time of day with nanosecond precision.
 15 | export
 16 | record LocalTime where
 17 |   constructor MkLocalTime
 18 |   nanosSinceMidnight : Integer
 19 |
 20 | public export
 21 | Eq LocalTime where
 22 |   left == right = left.nanosSinceMidnight == right.nanosSinceMidnight
 23 |
 24 | public export
 25 | Ord LocalTime where
 26 |   compare left right = compare left.nanosSinceMidnight right.nanosSinceMidnight
 27 |
 28 | export
 29 | toNanosecondsSinceMidnight : LocalTime -> Integer
 30 | toNanosecondsSinceMidnight = nanosSinceMidnight
 31 |
 32 | ||| Construct a local time from already refined components.
 33 | public export
 34 | localTime : Hour -> Minute -> Second -> Nanosecond -> LocalTime
 35 | localTime valueHour valueMinute valueSecond valueNanosecond = MkLocalTime
 36 |   (((hourValue valueHour * 60 + minuteValue valueMinute) * 60 + secondValue valueSecond) *
 37 |     nanosPerSecond + nanosecondValue valueNanosecond)
 38 |
 39 | ||| Extract the hour in the range 0-23.
 40 | public export
 41 | hour : LocalTime -> Hour
 42 | -- The refined value is always in range for a valid time; the fallback is unreachable.
 43 | hour value = either (const 0) id
 44 |   (refineHour (value.nanosSinceMidnight `div` (3600 * nanosPerSecond)))
 45 |
 46 | ||| Extract the minute in the range 0-59.
 47 | public export
 48 | minute : LocalTime -> Minute
 49 | minute value = either (const 0) id
 50 |   (refineMinute (value.nanosSinceMidnight `div` (60 * nanosPerSecond) `mod` 60))
 51 |
 52 | ||| Extract the second in the range 0-59.
 53 | public export
 54 | second : LocalTime -> Second
 55 | second value = either (const 0) id
 56 |   (refineSecond (value.nanosSinceMidnight `div` nanosPerSecond `mod` 60))
 57 |
 58 | ||| Extract the nanosecond within the current second.
 59 | public export
 60 | nanosecond : LocalTime -> Nanosecond
 61 | nanosecond value = either (const 0) id
 62 |   (refineNanosecond (value.nanosSinceMidnight `mod` nanosPerSecond))
 63 |
 64 | public export
 65 | Show LocalTime where
 66 |   show value = "localTime " ++
 67 |     show (hour value) ++ " " ++
 68 |     show (minute value) ++ " " ++
 69 |     show (second value) ++ " " ++
 70 |     show (nanosecond value)
 71 |
 72 | ||| Identifies which raw local-time component failed refinement.
 73 | public export
 74 | data LocalTimeError
 75 |   = InvalidHour HourError
 76 |   | InvalidMinute MinuteError
 77 |   | InvalidSecond SecondError
 78 |   | InvalidNanosecond NanosecondError
 79 |
 80 | ||| Validate raw hour, minute, second, and nanosecond values as a local time.
 81 | public export
 82 | refineLocalTime : Integer -> Integer -> Integer -> Integer -> Either LocalTimeError LocalTime
 83 | refineLocalTime rawHour rawMinute rawSecond rawNanosecond = do
 84 |   valueHour <- mapFst InvalidHour (refineHour rawHour)
 85 |   valueMinute <- mapFst InvalidMinute (refineMinute rawMinute)
 86 |   valueSecond <- mapFst InvalidSecond (refineSecond rawSecond)
 87 |   valueNanosecond <- mapFst InvalidNanosecond (refineNanosecond rawNanosecond)
 88 |   pure (localTime valueHour valueMinute valueSecond valueNanosecond)
 89 |
 90 | export
 91 | applyTimePeriodWithCarry : Period target -> LocalTime -> (Integer, LocalTime)
 92 | applyTimePeriodWithCarry period value =
 93 |   let combined = value.nanosSinceMidnight + delta
 94 |       carry = combined `div` nanosPerDay
 95 |       withinDay = combined `mod` nanosPerDay
 96 |    in (carry, MkLocalTime withinDay)
 97 |   where
 98 |     delta = (((periodHours period * 60 + periodMinutes period) * 60 +
 99 |       periodSeconds period) * nanosPerSecond) + periodNanoseconds period
100 |
101 | public export
102 | HasTime LocalTime where
103 |   timeCapability = ()
104 |
105 | public export
106 | PeriodTarget LocalTime where
107 |   periodTarget = ()
108 |
109 | public export
110 | ApplyPeriod LocalTime where
111 |   applyPeriod period = snd . applyTimePeriodWithCarry period
112 |
113 | ||| Compute the signed same-day period from `start` to `end`.
114 | ||| No implicit midnight crossing is chosen: an earlier `end` produces a
115 | ||| negative period.
116 | public export
117 | between : (start : LocalTime) -> (end : LocalTime) -> Period LocalTime
118 | between start end = nanoseconds
119 |   (toNanosecondsSinceMidnight end - toNanosecondsSinceMidnight start)