IotaTime.Period

Definitions

record Period : Type -> Type

  A calendar-relative amount applicable to `target`.
  The constructor is hidden so unit capabilities cannot be bypassed.

Totality: total
Visibility: export
Constructor: 

MkPeriod : Integer -> Integer -> Integer -> Integer -> Integer -> Integer -> Integer -> Integer -> Period target

Projections:

.storedDays : Period target -> Integer

.storedHours : Period target -> Integer

.storedMinutes : Period target -> Integer

.storedMonths : Period target -> Integer

.storedNanoseconds : Period target -> Integer

.storedSeconds : Period target -> Integer

.storedWeeks : Period target -> Integer

.storedYears : Period target -> Integer

Hints:

Eq (Period target)

Monoid (Period target)

Semigroup (Period target)

Show (Period target)

periodYears : Period target -> Integer

Totality: total
Visibility: export

periodMonths : Period target -> Integer

Totality: total
Visibility: export

periodWeeks : Period target -> Integer

Totality: total
Visibility: export

periodDays : Period target -> Integer

Totality: total
Visibility: export

periodHours : Period target -> Integer

Totality: total
Visibility: export

periodMinutes : Period target -> Integer

Totality: total
Visibility: export

periodSeconds : Period target -> Integer

Totality: total
Visibility: export

periodNanoseconds : Period target -> Integer

Totality: total
Visibility: export

interface HasCalendar : Type -> Type

  Types with calendar-relative date fields.

Parameters: target
Methods:

0 calendarCapability : ()

Implementation: 

HasCalendar (CalendarDateTime calendar)

0 calendarCapability : HasCalendar target => ()

Totality: total
Visibility: public export

interface HasTime : Type -> Type

  Types with local time-of-day fields.

Parameters: target
Methods:

0 timeCapability : ()

Implementations:

HasTime (CalendarDateTime calendar)

HasTime LocalTime

0 timeCapability : HasTime target => ()

Totality: total
Visibility: public export

interface ApplyPeriod : Type -> Type

  Library-owned types to which periods can be applied. The internal target
  capability seals this interface against client implementations.

Parameters: target
Constraints: PeriodTarget target
Methods:

applyPeriod : Period target -> target -> target

  Apply all components of a period using iotaTime's rules for the target.
  
  For calendar dates, components apply from largest to smallest: years,
  months, weeks, then days. Year and month shifts clamp an invalid day to
  the target month's final day; every shift also clamps at the concrete
  calendar's supported boundaries. Weeks are seven-day shifts. Components
  combined with `<+>` are aggregated before this sequence, so
  `months 1 <+> months 1` applies one two-month shift rather than two
  separately clamped one-month shifts.
  
  For `LocalTime`, clock components combine into one signed displacement
  and wrap within the 24-hour day. For `CalendarDateTime`, date components
  apply first as above, then clock components combine into one displacement
  whose signed day carry adjusts the resulting date.

Implementations:

ApplyPeriod (CalendarDateTime calendar)

ApplyPeriod LocalTime

applyPeriod : ApplyPeriod target => Period target -> target -> target

  Apply all components of a period using iotaTime's rules for the target.
  
  For calendar dates, components apply from largest to smallest: years,
  months, weeks, then days. Year and month shifts clamp an invalid day to
  the target month's final day; every shift also clamps at the concrete
  calendar's supported boundaries. Weeks are seven-day shifts. Components
  combined with `<+>` are aggregated before this sequence, so
  `months 1 <+> months 1` applies one two-month shift rather than two
  separately clamped one-month shifts.
  
  For `LocalTime`, clock components combine into one signed displacement
  and wrap within the 24-hour day. For `CalendarDateTime`, date components
  apply first as above, then clock components combine into one displacement
  whose signed day carry adjusts the resulting date.

Totality: total
Visibility: public export

years : HasCalendar target => Integer -> Period target

  Construct a period measured in calendar years.

Totality: total
Visibility: public export

months : HasCalendar target => Integer -> Period target

  Construct a period measured in calendar months.

Totality: total
Visibility: public export

weeks : HasCalendar target => Integer -> Period target

  Construct a period measured in seven-day calendar weeks.

Totality: total
Visibility: public export

days : HasCalendar target => Integer -> Period target

  Construct a period measured in calendar days.

Totality: total
Visibility: public export

hours : HasTime target => Integer -> Period target

  Construct a period measured in hours.

Totality: total
Visibility: public export

minutes : HasTime target => Integer -> Period target

  Construct a period measured in minutes.

Totality: total
Visibility: public export

seconds : HasTime target => Integer -> Period target

  Construct a period measured in seconds.

Totality: total
Visibility: public export

nanoseconds : HasTime target => Integer -> Period target

  Construct a period measured in nanoseconds.

Totality: total
Visibility: public export

negatePeriod : Period target -> Period target

  Negate every component of a period.

Totality: total
Visibility: public export

scalePeriod : Integer -> Period target -> Period target

  Multiply every component of a period by an integer.

Totality: total
Visibility: public export