0 | module IotaTime.Offset
  1 |
  2 | import public Data.So
  3 |
  4 | %default total
  5 |
  6 | secondsPerMinute : Integer
  7 | secondsPerMinute = 60
  8 |
  9 | secondsPerHour : Integer
 10 | secondsPerHour = 3600
 11 |
 12 | maxOffsetHours : Integer
 13 | maxOffsetHours = 18
 14 |
 15 | maxOffsetSeconds : Integer
 16 | maxOffsetSeconds = maxOffsetHours * secondsPerHour
 17 |
 18 | ||| A signed whole-second displacement from UTC, bounded to plus or minus
 19 | ||| eighteen hours.
 20 | export
 21 | record OffsetRep where
 22 |   constructor MkOffset
 23 |   storedSeconds : Integer
 24 |
 25 | public export
 26 | Offset : Type
 27 | Offset = OffsetRep
 28 |
 29 | public export
 30 | isValidOffsetSeconds : Integer -> Bool
 31 | isValidOffsetSeconds value =
 32 |   value >= -64800 && value <= 64800
 33 |
 34 | public export
 35 | isValidOffsetMinutes : Integer -> Bool
 36 | isValidOffsetMinutes value =
 37 |   value >= -1080 && value <= 1080
 38 |
 39 | public export
 40 | isValidOffsetHours : Integer -> Bool
 41 | isValidOffsetHours value =
 42 |   value >= -18 && value <= 18
 43 |
 44 | public export
 45 | fromSeconds : (value : Integer) ->
 46 |               {auto 0 valid : So (isValidOffsetSeconds value)} -> Offset
 47 | fromSeconds value = MkOffset value
 48 |
 49 | public export
 50 | fromMinutes : (value : Integer) ->
 51 |               {auto 0 valid : So (isValidOffsetMinutes value)} -> Offset
 52 | fromMinutes value = MkOffset (value * secondsPerMinute)
 53 |
 54 | public export
 55 | fromHours : (value : Integer) ->
 56 |             {auto 0 valid : So (isValidOffsetHours value)} -> Offset
 57 | fromHours value = MkOffset (value * secondsPerHour)
 58 |
 59 | public export
 60 | data OffsetError = OffsetOutOfRange Integer
 61 |
 62 | public export
 63 | refineOffsetSeconds : (value : Integer) -> Either OffsetError Offset
 64 | refineOffsetSeconds value =
 65 |   case choose (isValidOffsetSeconds value) of
 66 |     Left valid => Right (fromSeconds value @{valid})
 67 |     Right _ => Left (OffsetOutOfRange value)
 68 |
 69 | ||| Internal exact-value observation used by sibling implementation modules.
 70 | ||| Public callers should normally use `hours`, `minutes`, and `seconds`.
 71 | export
 72 | totalOffsetSeconds : Offset -> Integer
 73 | totalOffsetSeconds (MkOffset value) = value
 74 |
 75 | componentSign : Integer -> Integer
 76 | componentSign value = if value < 0 then -1 else 1
 77 |
 78 | ||| The signed whole-hour component of an offset.
 79 | public export
 80 | hours : Offset -> Integer
 81 | hours value =
 82 |   componentSign seconds * (abs seconds `div` secondsPerHour)
 83 |   where
 84 |     seconds = totalOffsetSeconds value
 85 |
 86 | ||| The signed minute-within-hour component of an offset.
 87 | public export
 88 | minutes : Offset -> Integer
 89 | minutes value =
 90 |   componentSign seconds *
 91 |     ((abs seconds `mod` secondsPerHour) `div` secondsPerMinute)
 92 |   where
 93 |     seconds = totalOffsetSeconds value
 94 |
 95 | ||| The signed second-within-minute component of an offset.
 96 | public export
 97 | seconds : Offset -> Integer
 98 | seconds value =
 99 |   componentSign seconds * (abs seconds `mod` secondsPerMinute)
100 |   where
101 |     seconds = totalOffsetSeconds value
102 |
103 | public export
104 | empty : Offset
105 | empty = MkOffset 0
106 |
107 | clampOffsetSeconds : Integer -> Integer
108 | clampOffsetSeconds value = max (-64800) (min 64800 value)
109 |
110 | ||| Add two offsets, clamping the result to the supported bounds.
111 | public export
112 | addClamped : Offset -> Offset -> Offset
113 | addClamped left right = MkOffset (clampOffsetSeconds
114 |   (totalOffsetSeconds left + totalOffsetSeconds right))
115 |
116 | ||| Subtract the second offset, clamping the result to the supported bounds.
117 | public export
118 | minusClamped : Offset -> Offset -> Offset
119 | minusClamped left right = MkOffset (clampOffsetSeconds
120 |   (totalOffsetSeconds left - totalOffsetSeconds right))
121 |
122 | ||| Reverse an offset's direction.
123 | public export
124 | negateOffset : Offset -> Offset
125 | negateOffset value = MkOffset (negate (totalOffsetSeconds value))
126 |
127 | public export
128 | Eq OffsetRep where
129 |   left == right = totalOffsetSeconds left == totalOffsetSeconds right
130 |
131 | public export
132 | Ord OffsetRep where
133 |   compare left right = compare
134 |     (totalOffsetSeconds left) (totalOffsetSeconds right)
135 |
136 | public export
137 | Show OffsetRep where
138 |   show value = "fromSeconds " ++ show (totalOffsetSeconds value)