0 | module IotaTime.Calendar.Component
  1 |
  2 | import public Data.So
  3 |
  4 | %default total
  5 |
  6 | ||| A calendar year with an unbounded signed integer value.
  7 | export
  8 | record Year where
  9 |   constructor MkYear
 10 |   integerValue : Integer
 11 |
 12 | public export
 13 | Eq Year where
 14 |   left == right = left.integerValue == right.integerValue
 15 |
 16 | public export
 17 | Ord Year where
 18 |   compare left right = compare left.integerValue right.integerValue
 19 |
 20 | public export
 21 | Show Year where
 22 |   show value = show value.integerValue
 23 |
 24 | public export
 25 | Num Year where
 26 |   MkYear left + MkYear right = MkYear (left + right)
 27 |   MkYear left * MkYear right = MkYear (left * right)
 28 |   fromInteger = MkYear
 29 |
 30 | public export
 31 | Neg Year where
 32 |   negate (MkYear value) = MkYear (negate value)
 33 |   MkYear left - MkYear right = MkYear (left - right)
 34 |
 35 | namespace Year
 36 |   ||| Construct a year from any integer.
 37 |   public export
 38 |   fromInteger : Integer -> Year
 39 |   fromInteger = MkYear
 40 |
 41 | ||| Return the signed integer represented by a year.
 42 | public export
 43 | yearValue : Year -> Integer
 44 | yearValue (MkYear value) = value
 45 |
 46 | export
 47 | yearFromInteger : Integer -> Year
 48 | yearFromInteger = MkYear
 49 |
 50 | ||| A day number constrained to the inclusive range 1 through 31.
 51 | export
 52 | record DayOfMonth where
 53 |   constructor MkDayOfMonth
 54 |   integerValue : Integer
 55 |
 56 | ||| Whether an integer is in the representable day-of-month range.
 57 | public export
 58 | isValidDayOfMonth : Integer -> Bool
 59 | isValidDayOfMonth value = value >= 1 && value <= 31
 60 |
 61 | public export
 62 | Eq DayOfMonth where
 63 |   left == right = left.integerValue == right.integerValue
 64 |
 65 | public export
 66 | Ord DayOfMonth where
 67 |   compare left right = compare left.integerValue right.integerValue
 68 |
 69 | public export
 70 | Show DayOfMonth where
 71 |   show value = show value.integerValue
 72 |
 73 | namespace DayOfMonth
 74 |   ||| Construct a day of month when its range proof is available statically.
 75 |   public export
 76 |   fromInteger : (value : Integer) ->
 77 |                 {auto 0 valid : So (isValidDayOfMonth value)} ->
 78 |                 DayOfMonth
 79 |   fromInteger value = MkDayOfMonth value
 80 |
 81 | ||| Return the integer day number.
 82 | public export
 83 | dayOfMonthValue : DayOfMonth -> Integer
 84 | dayOfMonthValue (MkDayOfMonth value) = value
 85 |
 86 | export
 87 | dayOfMonthFromInteger : Integer -> DayOfMonth
 88 | dayOfMonthFromInteger value = MkDayOfMonth (max 1 (min 31 value))
 89 |
 90 | ||| A runtime day-of-month value outside the inclusive range 1 through 31.
 91 | public export
 92 | data DayOfMonthError = DayOfMonthOutOfRange Integer
 93 |
 94 | ||| Refine an untrusted integer into a day of month or return a typed range error.
 95 | public export
 96 | refineDayOfMonth : (value : Integer) -> Either DayOfMonthError DayOfMonth
 97 | refineDayOfMonth value =
 98 |   case choose (isValidDayOfMonth value) of
 99 |     Left valid => Right (DayOfMonth.fromInteger value @{valid})
100 |     Right _ => Left (DayOfMonthOutOfRange value)
101 |
102 | ||| An unbounded signed week number used by calendar week calculations.
103 | export
104 | record WeekNumber where
105 |   constructor MkWeekNumber
106 |   integerValue : Integer
107 |
108 | public export
109 | Eq WeekNumber where
110 |   left == right = left.integerValue == right.integerValue
111 |
112 | public export
113 | Ord WeekNumber where
114 |   compare left right = compare left.integerValue right.integerValue
115 |
116 | public export
117 | Show WeekNumber where
118 |   show value = show value.integerValue
119 |
120 | public export
121 | Num WeekNumber where
122 |   MkWeekNumber left + MkWeekNumber right = MkWeekNumber (left + right)
123 |   MkWeekNumber left * MkWeekNumber right = MkWeekNumber (left * right)
124 |   fromInteger = MkWeekNumber
125 |
126 | public export
127 | Neg WeekNumber where
128 |   negate (MkWeekNumber value) = MkWeekNumber (negate value)
129 |   MkWeekNumber left - MkWeekNumber right = MkWeekNumber (left - right)
130 |
131 | namespace WeekNumber
132 |   ||| Construct a week number from any integer.
133 |   public export
134 |   fromInteger : Integer -> WeekNumber
135 |   fromInteger = MkWeekNumber
136 |
137 | ||| Return the signed integer represented by a week number.
138 | public export
139 | weekNumberValue : WeekNumber -> Integer
140 | weekNumberValue (MkWeekNumber value) = value
141 |