Idris2Doc : IotaTime.Calendar

IotaTime.Calendar

(source)
Reexports
import public IotaTime.Calendar.Component
Definitions
data DayOfWeek : Type
  A weekday in the standard seven-day civil week shared by all iotaTime
  calendars.

  Totality: total
  Visibility: public export
  Constructors:
  
Sunday : DayOfWeek
  
Monday : DayOfWeek
  
Tuesday : DayOfWeek
  
Wednesday : DayOfWeek
  
Thursday : DayOfWeek
  
Friday : DayOfWeek
  
Saturday : DayOfWeek

  Hints:
  
Eq DayOfWeek
  
Ord DayOfWeek
  
Show DayOfWeek
weekdayNumber : DayOfWeek -> Integer
  Zero-based weekday position from Sunday through Saturday.

  Totality: total
  Visibility: public export
daysPerWeek : Integer
  Number of days in the standard civil week modeled by iotaTime calendars.

  Totality: total
  Visibility: public export
weekdayFromNumber : Integer -> DayOfWeek
  Convert an integer weekday position to the corresponding weekday,
  wrapping values outside the standard zero-through-six range.

  Totality: total
  Visibility: public export
nextWeekdayOffset : Integer -> DayOfWeek -> DayOfWeek -> Integer
  Signed day offset to the requested following weekday occurrence.

  Totality: total
  Visibility: export
previousWeekdayOffset : Integer -> DayOfWeek -> DayOfWeek -> Integer
  Signed day offset to the requested preceding weekday occurrence.

  Totality: total
  Visibility: export
applyDatePeriodWith : (Integer -> date -> date) -> (Integer -> date -> date) -> (Integer -> date -> date) -> Period target -> date -> date
  Apply calendar period components from largest to smallest, preserving a
  separate shift for weeks before the final day shift.

  Totality: total
  Visibility: export
data DayNth : Type
  Selects an occurrence of a weekday within a month.

  Totality: total
  Visibility: public export
  Constructors:
  
FourthToLast : DayNth
  
ThirdToLast : DayNth
  
SecondToLast : DayNth
  
Last : DayNth
  
First : DayNth
  
Second : DayNth
  
Third : DayNth
  
Fourth : DayNth
  
Fifth : DayNth

  Hints:
  
Eq DayNth
  
Show DayNth
nthWeekdayDayNumber : DayNth -> Integer -> Integer -> Integer -> Integer
  Compute the raw day-of-month candidate for a weekday occurrence.
  Calendar implementations remain responsible for validating the candidate
  against their supported year and month ranges before constructing a date.

  Totality: total
  Visibility: export
data CalendarConversionError : Type
  A calendar conversion failed because the target calendar cannot represent
  the source date's bridge day.

  Totality: total
  Visibility: public export
  Constructor: 
TargetCalendarOutOfRange : String -> Integer -> CalendarConversionError
data DateDifferenceUnits : Type
  Calendar units used when decomposing the difference between two dates.

  Totality: total
  Visibility: public export
  Constructors:
  
DaysOnly : DateDifferenceUnits
  
YearsMonthsDays : DateDifferenceUnits
data MonthArithmeticPolicy : Type
  Month arithmetic used while decomposing a calendar difference.

  Totality: total
  Visibility: public export
  Constructor: 
ClampToMonth : MonthArithmeticPolicy
record DateDifferencePolicy : Type
  Controls how a difference between calendar dates is decomposed.

  Totality: total
  Visibility: public export
  Constructor: 
MkDateDifferencePolicy : DateDifferenceUnits -> MonthArithmeticPolicy -> DateDifferencePolicy

  Projections:
  
.monthArithmetic : DateDifferencePolicy -> MonthArithmeticPolicy
  
.units : DateDifferencePolicy -> DateDifferenceUnits
.units : DateDifferencePolicy -> DateDifferenceUnits
  Totality: total
  Visibility: public export
units : DateDifferencePolicy -> DateDifferenceUnits
  Totality: total
  Visibility: public export
.monthArithmetic : DateDifferencePolicy -> MonthArithmeticPolicy
  Totality: total
  Visibility: public export
monthArithmetic : DateDifferencePolicy -> MonthArithmeticPolicy
  Totality: total
  Visibility: public export
nodaTimePolicy : DateDifferencePolicy
  The standard largest-first, non-overshooting calendar decomposition.

  Totality: total
  Visibility: public export
interface Calendar : Type -> Type
  Capabilities and dependent representations required of a calendar.
  `MonthRep` may depend on the year, allowing calendars such as Hebrew to
  make leap-only months unrepresentable in common years.

  Parameters: calendar
Methods:
  
DateRep : Type
  
MonthRep : Year -> Type
  
isValidDays : Integer -> Bool
  
fromDays : (days : Integer) -> {auto 0 _ : So (isValidDays days)} -> DateRep
  
toDaysFor : DateRep -> Integer
  
0 toDaysValid : (date : DateRep) -> So (isValidDays (toDaysFor date))
  
0 toFromDays : (days : Integer) -> (0 valid : So (isValidDays days)) -> toDaysFor (fromDays days) = days
  
0 fromToDays : (date : DateRep) -> fromDays (toDaysFor date) = date
  
calendarName : String
  
year' : DateRep -> Year
  
toYmd : (date : DateRep) -> (MonthRep (year' date), DayOfMonth)
  
day' : DateRep -> DayOfMonth
  
month' : (date : DateRep) -> MonthRep (year' date)
  
applyCalendarPeriod' : Period target -> DateRep -> DateRep
  
shiftCalendarDays' : Integer -> DateRep -> DateRep
  
dayOfWeekFor : DateRep -> DayOfWeek
  
nextFor : Integer -> DayOfWeek -> DateRep -> DateRep
  
previousFor : Integer -> DayOfWeek -> DateRep -> DateRep
DateRep : Calendar calendar => Type
  Totality: total
  Visibility: public export
MonthRep : Calendar calendar => Year -> Type
  Totality: total
  Visibility: public export
isValidDays : Calendar calendar => Integer -> Bool
  Totality: total
  Visibility: public export
fromDays : {auto __con : Calendar calendar} -> (days : Integer) -> {auto 0 _ : So (isValidDays days)} -> DateRep
  Totality: total
  Visibility: public export
toDaysFor : {auto __con : Calendar calendar} -> DateRep -> Integer
  Totality: total
  Visibility: public export
0 toDaysValid : {auto __con : Calendar calendar} -> (date : DateRep) -> So (isValidDays (toDaysFor date))
  Totality: total
  Visibility: public export
0 toFromDays : {auto __con : Calendar calendar} -> (days : Integer) -> (0 valid : So (isValidDays days)) -> toDaysFor (fromDays days) = days
  Totality: total
  Visibility: public export
0 fromToDays : {auto __con : Calendar calendar} -> (date : DateRep) -> fromDays (toDaysFor date) = date
  Totality: total
  Visibility: public export
calendarName : Calendar calendar => String
  Totality: total
  Visibility: public export
year' : {auto __con : Calendar calendar} -> DateRep -> Year
  Totality: total
  Visibility: public export
toYmd : {auto __con : Calendar calendar} -> (date : DateRep) -> (MonthRep (year' date), DayOfMonth)
  Totality: total
  Visibility: public export
day' : {auto __con : Calendar calendar} -> DateRep -> DayOfMonth
  Totality: total
  Visibility: public export
month' : {auto __con : Calendar calendar} -> (date : DateRep) -> MonthRep (year' date)
  Totality: total
  Visibility: public export
applyCalendarPeriod' : {auto __con : Calendar calendar} -> Period target -> DateRep -> DateRep
  Totality: total
  Visibility: public export
shiftCalendarDays' : {auto __con : Calendar calendar} -> Integer -> DateRep -> DateRep
  Totality: total
  Visibility: public export
dayOfWeekFor : {auto __con : Calendar calendar} -> DateRep -> DayOfWeek
  Totality: total
  Visibility: public export
nextFor : {auto __con : Calendar calendar} -> Integer -> DayOfWeek -> DateRep -> DateRep
  Totality: total
  Visibility: public export
previousFor : {auto __con : Calendar calendar} -> Integer -> DayOfWeek -> DateRep -> DateRep
  Totality: total
  Visibility: public export
CalendarDate : (calendar : Type) -> Calendar calendar => Type
  The opaque date representation selected by a calendar implementation.

  Totality: total
  Visibility: public export
interface HasCalendarBridge : Type -> Type
  Internal normalization implemented by iotaTime's built-in calendars for
  cross-calendar and instant conversion. Calendar-local APIs use
  `Calendar.toDaysFor` instead.

  Parameters: date
Methods:
  
toBridgeDays : date -> Integer
  
acceptsBridgeDays : Integer -> Bool
  
fromBridgeDays : (days : Integer) -> {auto 0 _ : So (acceptsBridgeDays days)} -> date
  
bridgeCalendarName : String

Implementation: 
CalendarValue date -> HasCalendarBridge date
toBridgeDays : HasCalendarBridge date => date -> Integer
  Totality: total
  Visibility: export
acceptsBridgeDays : HasCalendarBridge date => Integer -> Bool
  Totality: total
  Visibility: export
fromBridgeDays : {auto __con : HasCalendarBridge date} -> (days : Integer) -> {auto 0 _ : So (acceptsBridgeDays days)} -> date
  Totality: total
  Visibility: export
bridgeCalendarName : HasCalendarBridge date => String
  Totality: total
  Visibility: export
interface CalendarValue : Type -> Type
  Calendar operations determined by a concrete date representation.
  This lets value-oriented APIs infer the calendar from their first date
  argument instead of requiring a repeated `{calendar = ...}` annotation.

  Parameters: date
Constraints: HasCalendarBridge date
Methods:
  
CalendarMonth : Year -> Type
  
calendarValueToDays : date -> Integer
  
calendarValueYear : date -> Year
  
calendarValueMonthDay : (value : date) -> (CalendarMonth (calendarValueYear value), DayOfMonth)
  
calendarValueDayOfWeek : date -> DayOfWeek
  
calendarValueBetweenWith : DateDifferencePolicy -> date -> date -> Period date

Implementation: 
CalendarNavigation date -> CalendarValue date
CalendarMonth : CalendarValue date => Year -> Type
  Totality: total
  Visibility: public export
calendarValueToDays : CalendarValue date => date -> Integer
  Totality: total
  Visibility: public export
calendarValueYear : CalendarValue date => date -> Year
  Totality: total
  Visibility: public export
calendarValueMonthDay : {auto __con : CalendarValue date} -> (value : date) -> (CalendarMonth (calendarValueYear value), DayOfMonth)
  Totality: total
  Visibility: public export
calendarValueDayOfWeek : CalendarValue date => date -> DayOfWeek
  Totality: total
  Visibility: public export
calendarValueBetweenWith : CalendarValue date => DateDifferencePolicy -> date -> date -> Period date
  Totality: total
  Visibility: public export
interface CalendarNavigation : Type -> Type
  Weekday navigation selected by the concrete date representation.

  Parameters: date
Constraints: CalendarValue date
Methods:
  
calendarValueNext : Integer -> DayOfWeek -> date -> date
  
calendarValuePrevious : Integer -> DayOfWeek -> date -> date
calendarValueNext : CalendarNavigation date => Integer -> DayOfWeek -> date -> date
  Totality: total
  Visibility: public export
calendarValuePrevious : CalendarNavigation date => Integer -> DayOfWeek -> date -> date
  Totality: total
  Visibility: public export
yearFor : {auto cal : Calendar calendar} -> CalendarDate calendar -> Year
  Extract the calendar year from a date.

  Totality: total
  Visibility: public export
monthFor : {auto cal : Calendar calendar} -> (date : CalendarDate calendar) -> MonthRep (yearFor date)
  Extract the year-indexed calendar month from a date.

  Totality: total
  Visibility: public export
dayFor : {auto cal : Calendar calendar} -> CalendarDate calendar -> DayOfMonth
  Extract the day of month from a date.

  Totality: total
  Visibility: public export
applyCalendarPeriod : {auto cal : Calendar calendar} -> Period target -> CalendarDate calendar -> CalendarDate calendar
  Totality: total
  Visibility: export
shiftCalendarDays : {auto cal : Calendar calendar} -> Integer -> CalendarDate calendar -> CalendarDate calendar
  Totality: total
  Visibility: export
betweenDaysFor : {auto cal : Calendar calendar} -> HasCalendar (CalendarDate calendar) => CalendarDate calendar -> CalendarDate calendar -> Period (CalendarDate calendar)
  Compute the exact signed day period from `start` to `end`.

  Totality: total
  Visibility: public export
betweenWithFor : {auto cal : Calendar calendar} -> HasCalendar (CalendarDate calendar) => DateDifferencePolicy -> CalendarDate calendar -> CalendarDate calendar -> Period (CalendarDate calendar)
  Decompose the signed difference from `start` to `end` according to `policy`.
  Calendar units are selected largest-first without passing the endpoint.

  Totality: total
  Visibility: public export
betweenFor : {auto cal : Calendar calendar} -> HasCalendar (CalendarDate calendar) => CalendarDate calendar -> CalendarDate calendar -> Period (CalendarDate calendar)
  Decompose the signed calendar difference using `nodaTimePolicy`.

  Totality: total
  Visibility: public export
yearMonthDayFor : {auto cal : Calendar calendar} -> CalendarDate calendar -> (valueYear : Year ** (MonthRep valueYear, DayOfMonth))
  Decompose a date while preserving the dependency between its year and month.

  Totality: total
  Visibility: public export
betweenDays : date -> CalendarValue date => date -> Period date
  Compute the exact signed day period from `start` to `end`.

  Totality: total
  Visibility: public export
betweenWith : DateDifferencePolicy -> date -> CalendarValue date => date -> Period date
  Decompose a difference according to `policy`, inferring the calendar from
  the first date argument.

  Totality: total
  Visibility: public export
between : date -> CalendarValue date => date -> Period date
  Decompose a signed date difference using `nodaTimePolicy`.

  Totality: total
  Visibility: public export
yearMonthDay : date -> {auto rep : CalendarValue date} -> (valueYear : Year ** (CalendarMonth valueYear, DayOfMonth))
  Decompose a date while preserving its year-indexed month type.

  Totality: total
  Visibility: public export
toDays : date -> CalendarValue date => Integer
  Return the calendar-relative day count for a concrete date value.

  Totality: total
  Visibility: public export
year : date -> CalendarValue date => Year
  Extract the calendar year from a concrete date value.

  Totality: total
  Visibility: public export
month : (value : date) -> {auto rep : CalendarValue date} -> CalendarMonth (year value)
  Extract the year-indexed calendar month from a concrete date value.

  Totality: total
  Visibility: public export
day : date -> CalendarValue date => DayOfMonth
  Extract the day of month from a concrete date value.

  Totality: total
  Visibility: public export
calendarComponentsCoherent : (value : date) -> {auto rep : CalendarValue date} -> yearMonthDay value = (year value ** (month value, day value))
  Combined and projected civil-date observations are definitionally coherent.

  Totality: total
  Visibility: public export
dayOfWeek : date -> CalendarValue date => DayOfWeek
  Extract the weekday from a concrete date value.

  Totality: total
  Visibility: public export
next : CalendarNavigation date => Integer -> DayOfWeek -> date -> date
  Find a matching weekday relative to a concrete date value.

  Totality: total
  Visibility: public export
previous : CalendarNavigation date => Integer -> DayOfWeek -> date -> date
  Find a preceding matching weekday relative to a concrete date value.

  Totality: total
  Visibility: public export
withCalendar : HasCalendarBridge sourceDate => HasCalendarBridge targetDate => sourceDate -> Either CalendarConversionError targetDate
  Convert a date to another calendar through their shared bridge day.
  Returns `TargetCalendarOutOfRange` when the target cannot represent it.

  Totality: total
  Visibility: public export