Idris2Doc : IotaTime.Calendar.Persian

IotaTime.Calendar.Persian

(source)
Definitions
data Persian : Type
  The astronomical Persian calendar over its vouched year range 1-1500.

  Totality: total
  Visibility: public export
  Constructor: 
PersianCalendar : Persian

  Hint: 
Calendar Persian
data PersianMonth : Type
  Totality: total
  Visibility: public export
  Constructors:
  
Farvardin : PersianMonth
  
Ordibehesht : PersianMonth
  
Khordad : PersianMonth
  
Tir : PersianMonth
  
Mordad : PersianMonth
  
Shahrivar : PersianMonth
  
Mehr : PersianMonth
  
Aban : PersianMonth
  
Azar : PersianMonth
  
Dey : PersianMonth
  
Bahman : PersianMonth
  
Esfand : PersianMonth

  Hints:
  
Eq PersianMonth
  
Ord PersianMonth
  
Show PersianMonth
monthNumber : PersianMonth -> Integer
  Totality: total
  Visibility: public export
weekdayFromDays : Integer -> DayOfWeek
  Totality: total
  Visibility: public export
minimumYear : Integer
  Totality: total
  Visibility: public export
maximumYear : Integer
  Totality: total
  Visibility: public export
epoch : Integer
  Totality: total
  Visibility: public export
leapYears : List Integer
  Totality: total
  Visibility: public export
isLeapYear : Year -> Bool
  Whether a supported Persian year contains Esfand 30.

  Totality: total
  Visibility: public export
countLeapsBefore : Integer -> List Integer -> Integer
  Totality: total
  Visibility: public export
newYearDay : Year -> Integer
  Totality: total
  Visibility: public export
lastDay : Integer
  Totality: total
  Visibility: public export
record PersianDate : Type
  Totality: total
  Visibility: export
  Constructor: 
MkPersianDate : (daysSinceEpoch : Integer) -> (0 _ : So ((daysSinceEpoch >= epoch) && Delay (daysSinceEpoch <= lastDay))) -> PersianDate

  Projections:
  
.daysSinceEpoch : PersianDate -> Integer
  
0 .validDays : ({rec:0} : PersianDate) -> So ((daysSinceEpoch {rec:0} >= epoch) && Delay (daysSinceEpoch {rec:0} <= lastDay))

  Hints:
  
ApplyPeriod PersianDate
  
CalendarNavigation PersianDate
  
CalendarValue PersianDate
  
Eq PersianDate
  
HasCalendar PersianDate
  
HasCalendarBridge PersianDate
  
Ord PersianDate
  
PeriodTarget PersianDate
  
Show PersianDate
maxDaysInMonth : PersianMonth -> Year -> DayOfMonth
  Totality: total
  Visibility: public export
isValidDate : DayOfMonth -> PersianMonth -> Year -> Bool
  Totality: total
  Visibility: public export
monthOffset : PersianMonth -> Integer
  Totality: total
  Visibility: public export
daysFromCivil : Year -> PersianMonth -> DayOfMonth -> Integer
  Totality: total
  Visibility: public export
calendarDate : (valueDay : DayOfMonth) -> (valueMonth : PersianMonth) -> (valueYear : Year) -> {auto 0 _ : So (isValidDate valueDay valueMonth valueYear)} -> CalendarDate Persian
  Construct a statically validated Persian date in years 1-1500.

  Totality: total
  Visibility: public export
data PersianDateError : Type
  Failures produced while refining untrusted Persian date data.

  Totality: total
  Visibility: public export
  Constructors:
  
InvalidPersianDate : DayOfMonth -> PersianMonth -> Year -> PersianDateError
  
InvalidPersianDayCount : Integer -> PersianDateError
  
InvalidPersianNthDay : DayNth -> DayOfWeek -> PersianMonth -> Year -> PersianDateError
  
InvalidPersianWeekDate : WeekNumber -> DayOfWeek -> Year -> PersianDateError
refineDate : DayOfMonth -> PersianMonth -> Year -> Either PersianDateError (CalendarDate Persian)
  Validate runtime day, month, and year components as a Persian date.

  Totality: total
  Visibility: public export
fromDays : (days : Integer) -> {auto 0 _ : So (isValidDays days)} -> CalendarDate Persian
  Construct a Persian date from a statically valid calendar-relative day count.

  Totality: total
  Visibility: public export
refineDays : Integer -> Either PersianDateError (CalendarDate Persian)
  Validate a runtime Persian day count within the supported year range.

  Totality: total
  Visibility: public export
nthDayOfMonth : DayNth -> DayOfWeek -> PersianMonth -> Year -> DayOfMonth
  Totality: total
  Visibility: public export
isValidNthDay : DayNth -> DayOfWeek -> PersianMonth -> Year -> Bool
  Totality: total
  Visibility: public export
fromNthDay : (nth : DayNth) -> (target : DayOfWeek) -> (valueMonth : PersianMonth) -> (valueYear : Year) -> {auto 0 _ : So (isValidNthDay nth target valueMonth valueYear)} -> CalendarDate Persian
  Construct the nth requested weekday in a Persian month.

  Totality: total
  Visibility: public export
refineNthDay : DayNth -> DayOfWeek -> PersianMonth -> Year -> Either PersianDateError (CalendarDate Persian)
  Validate an nth-weekday request for a Persian month.

  Totality: total
  Visibility: public export
weekDateDays : WeekNumber -> DayOfWeek -> Year -> Integer
  Totality: total
  Visibility: public export
isValidWeekDate : WeekNumber -> DayOfWeek -> Year -> Bool
  Totality: total
  Visibility: public export
fromWeekDate : (week : WeekNumber) -> (target : DayOfWeek) -> (valueYear : Year) -> {auto 0 _ : So (isValidWeekDate week target valueYear)} -> CalendarDate Persian
  Construct a Persian Saturday-based week date under static validity evidence.

  Totality: total
  Visibility: public export
refineWeekDate : WeekNumber -> DayOfWeek -> Year -> Either PersianDateError (CalendarDate Persian)
  Validate a runtime Persian Saturday-based week date.

  Totality: total
  Visibility: public export
data PersianArithmeticRule : Type
  Exact arithmetic rules available for the Solar Hijri calendar.

  Totality: total
  Visibility: public export
  Constructors:
  
Simple : PersianArithmeticRule
  
Birashk : PersianArithmeticRule

  Hints:
  
ApplyPeriod (ArithmeticPersianDate rule)
  
Calendar (ArithmeticPersian rule)
  
CalendarNavigation (ArithmeticPersianDate rule)
  
CalendarValue (ArithmeticPersianDate rule)
  
Eq (ArithmeticPersianDate rule)
  
HasCalendar (ArithmeticPersianDate rule)
  
HasCalendarBridge (ArithmeticPersianDate rule)
  
Ord (ArithmeticPersianDate rule)
  
PeriodTarget (ArithmeticPersianDate rule)
  
Show (ArithmeticPersianDate rule)
data ArithmeticPersian : PersianArithmeticRule -> Type
  A Persian calendar whose leap years are fixed by an arithmetic rule.

  Totality: total
  Visibility: public export
  Constructor: 
MkArithmeticPersian : ArithmeticPersian rule

  Hint: 
Calendar (ArithmeticPersian rule)
PersianSimple : Type
  The legacy 33-year Persian cycle used by the BCL before .NET 4.6.

  Totality: total
  Visibility: public export
PersianArithmetic : Type
  Ahmad Birashk's nested 2820-year arithmetic Persian cycle.

  Totality: total
  Visibility: public export
arithmeticRuleName : PersianArithmeticRule -> String
  Totality: total
  Visibility: export
record ArithmeticPersianDate : PersianArithmeticRule -> Type
  Totality: total
  Visibility: export
  Constructor: 
MkArithmeticPersianDate : (arithmeticDaysSinceEpoch : Integer) -> (0 _ : So ((arithmeticDaysSinceEpoch >= arithmeticRuleEpoch rule) && Delay (arithmeticDaysSinceEpoch <= arithmeticRuleLastDay rule))) -> ArithmeticPersianDate rule

  Projections:
  
.arithmeticDaysSinceEpoch : ArithmeticPersianDate rule -> Integer
  
0 .validDays : ({rec:0} : ArithmeticPersianDate rule) -> So ((arithmeticDaysSinceEpoch {rec:0} >= arithmeticRuleEpoch rule) && Delay (arithmeticDaysSinceEpoch {rec:0} <= arithmeticRuleLastDay rule))

  Hints:
  
ApplyPeriod (ArithmeticPersianDate rule)
  
CalendarNavigation (ArithmeticPersianDate rule)
  
CalendarValue (ArithmeticPersianDate rule)
  
Eq (ArithmeticPersianDate rule)
  
HasCalendar (ArithmeticPersianDate rule)
  
HasCalendarBridge (ArithmeticPersianDate rule)
  
Ord (ArithmeticPersianDate rule)
  
PeriodTarget (ArithmeticPersianDate rule)
  
Show (ArithmeticPersianDate rule)
minimumArithmeticYear : Integer
  Totality: total
  Visibility: public export
maximumArithmeticYear : Integer
  Totality: total
  Visibility: public export
isArithmeticLeapYear : Year -> Bool
  Totality: total
  Visibility: public export
arithmeticNewYearDay : Year -> Integer
  Totality: total
  Visibility: public export
arithmeticLastDay : Integer
  The final supported day under the selected arithmetic Persian rule.

  Totality: total
  Visibility: public export
maxArithmeticDaysInMonth : PersianMonth -> Year -> DayOfMonth
  Totality: total
  Visibility: public export
isValidArithmeticDate : DayOfMonth -> PersianMonth -> Year -> Bool
  Totality: total
  Visibility: public export
arithmeticDaysFromCivil : Year -> PersianMonth -> DayOfMonth -> Integer
  Totality: total
  Visibility: public export
arithmeticRuleCalendarDate : (valueDay : DayOfMonth) -> (valueMonth : PersianMonth) -> (valueYear : Year) -> {auto 0 _ : So (isValidArithmeticDate valueDay valueMonth valueYear)} -> CalendarDate (ArithmeticPersian rule)
  Construct a statically validated Persian date under an arithmetic rule.

  Totality: total
  Visibility: public export
simpleCalendarDate : (valueDay : DayOfMonth) -> (valueMonth : PersianMonth) -> (valueYear : Year) -> {auto 0 _ : So (isValidArithmeticDate valueDay valueMonth valueYear)} -> CalendarDate PersianSimple
  Construct a date in the legacy 33-year Persian cycle.

  Totality: total
  Visibility: public export
arithmeticCalendarDate : (valueDay : DayOfMonth) -> (valueMonth : PersianMonth) -> (valueYear : Year) -> {auto 0 _ : So (isValidArithmeticDate valueDay valueMonth valueYear)} -> CalendarDate PersianArithmetic
  Construct a date in Birashk's 2820-year arithmetic Persian cycle.

  Totality: total
  Visibility: public export
refineArithmeticRuleDate : DayOfMonth -> PersianMonth -> Year -> Either PersianDateError (CalendarDate (ArithmeticPersian rule))
  Validate runtime components under a selected arithmetic Persian rule.

  Totality: total
  Visibility: public export
refineSimpleDate : DayOfMonth -> PersianMonth -> Year -> Either PersianDateError (CalendarDate PersianSimple)
  Totality: total
  Visibility: public export
refineArithmeticDate : DayOfMonth -> PersianMonth -> Year -> Either PersianDateError (CalendarDate PersianArithmetic)
  Totality: total
  Visibility: public export
refineArithmeticDays : Integer -> Either PersianDateError (CalendarDate (ArithmeticPersian rule))
  Validate a day count under a selected arithmetic Persian rule.

  Totality: total
  Visibility: public export
isValidArithmeticNthDay : DayNth -> DayOfWeek -> PersianMonth -> Year -> Bool
  Totality: total
  Visibility: public export
arithmeticFromNthDay : (nth : DayNth) -> (target : DayOfWeek) -> (valueMonth : PersianMonth) -> (valueYear : Year) -> {auto 0 _ : So (isValidArithmeticNthDay nth target valueMonth valueYear)} -> CalendarDate (ArithmeticPersian rule)
  Construct an nth weekday under a selected arithmetic Persian rule.

  Totality: total
  Visibility: public export
refineArithmeticNthDay : DayNth -> DayOfWeek -> PersianMonth -> Year -> Either PersianDateError (CalendarDate (ArithmeticPersian rule))
  Validate an nth-weekday request under an arithmetic Persian rule.

  Totality: total
  Visibility: public export
isValidArithmeticWeekDate : WeekNumber -> DayOfWeek -> Year -> Bool
  Totality: total
  Visibility: public export
arithmeticFromWeekDate : (week : WeekNumber) -> (target : DayOfWeek) -> (valueYear : Year) -> {auto 0 _ : So (isValidArithmeticWeekDate week target valueYear)} -> CalendarDate (ArithmeticPersian rule)
  Construct a Saturday-based week date under an arithmetic Persian rule.

  Totality: total
  Visibility: public export
refineArithmeticWeekDate : WeekNumber -> DayOfWeek -> Year -> Either PersianDateError (CalendarDate (ArithmeticPersian rule))
  Validate a Saturday-based week date under an arithmetic Persian rule.

  Totality: total
  Visibility: public export