TOML Date-Time

Defines data types for representing a TOML date-time. TOML date-times are based on IETF RFC 3339 with some components optionally left out, creating four distinct variants.

• Offset Date-Time: A full RFC 3339 date-time.
• Local Date-Time: An RFC 3339 date-time without the time zone.
• Local Date: The date portion of an RFC 3339 date-time (year-month-day).
• Local Time: The time portion of an RFC 3339 date-time (without time zone).

def Lake.Toml.lpad (s : String) (c : Char) (len : Nat) : String

Equations

• Lake.Toml.lpad s c len = "".pushn c (len - s.length) ++ s

def Lake.Toml.rpad (s : String) (c : Char) (len : Nat) : String

Equations

• Lake.Toml.rpad s c len = s.pushn c (len - s.length)

def Lake.Toml.zpad (n : Nat) (len : Nat) : String

Equations

• Lake.Toml.zpad n len = Lake.Toml.lpad (toString n) '0' len

structure Lake.Toml.Date : Type

A TOML date (year-month-day).

• year : Nat
• month : Nat
• day : Nat

Instances For

• Lake.Toml.Date.instToString
• Lake.Toml.instCoeDateDateTime
• Lake.Toml.instInhabitedDate
• Lake.Toml.instOrdDate

instance Lake.Toml.instInhabitedDate : Inhabited Lake.Toml.Date

Equations

• Lake.Toml.instInhabitedDate = { default := { year := default, month := default, day := default } }

instance Lake.Toml.instDecidableEqDate : DecidableEq Lake.Toml.Date

Equations

• Lake.Toml.instDecidableEqDate = Lake.Toml.decEqDate✝

instance Lake.Toml.instOrdDate : Ord Lake.Toml.Date

Equations

• Lake.Toml.instOrdDate = { compare := Lake.Toml.ordDate✝ }

@[reducible, inline]

abbrev Lake.Toml.Date.IsLeapYear (y : Nat) : Prop

Equations

• Lake.Toml.Date.IsLeapYear y = (y % 4 = 0 ∧ (y % 100 ≠ 0 ∨ y % 400 = 0))

@[reducible, inline]

abbrev Lake.Toml.Date.IsValidMonth (m : Nat) : Prop

Equations

• Lake.Toml.Date.IsValidMonth m = (m ≥ 1 ∧ m ≤ 12)

def Lake.Toml.Date.maxDay (y : Nat) (m : Nat) : Nat

Equations

• Lake.Toml.Date.maxDay y m = if m = 2 then if Lake.Toml.Date.IsLeapYear y then 29 else 28 else if m ≤ 7 then 30 + m % 2 else 31 - m % 2

@[reducible, inline]

abbrev Lake.Toml.Date.IsValidDay (y : Nat) (m : Nat) (d : Nat) : Prop

Equations

• Lake.Toml.Date.IsValidDay y m d = (d ≥ 1 ∧ d ≤ Lake.Toml.Date.maxDay y m)

def Lake.Toml.Date.ofValid? (year : Nat) (month : Nat) (day : Nat) : Option Lake.Toml.Date

Equations

• Lake.Toml.Date.ofValid? year month day = do guard (Lake.Toml.Date.IsValidMonth month ∧ Lake.Toml.Date.IsValidDay year month day) pure { year := year, month := month, day := day }

def Lake.Toml.Date.ofString? (t : String) : Option Lake.Toml.Date

Equations

• One or more equations did not get rendered due to their size.

def Lake.Toml.Date.toString (d : Lake.Toml.Date) : String

Equations

• One or more equations did not get rendered due to their size.

instance Lake.Toml.Date.instToString : ToString Lake.Toml.Date

Equations

• Lake.Toml.Date.instToString = { toString := Lake.Toml.Date.toString }

structure Lake.Toml.Time : Type

A TOML time (hour:minute:second.fraction).

We do not represent whole time as seconds to due to the possibility of leap seconds in RFC 3339 times.

• hour : Nat
• minute : Nat
• second : Nat
• fracExponent : Nat
• fracMantissa : Nat

Instances For

• Lake.Toml.Time.instOfNat
• Lake.Toml.Time.instToString
• Lake.Toml.instCoeTimeDateTime
• Lake.Toml.instInhabitedTime

instance Lake.Toml.instInhabitedTime : Inhabited Lake.Toml.Time

Equations

• Lake.Toml.instInhabitedTime = { default := { hour := default, minute := default, second := default, fracExponent := default, fracMantissa := default } }

instance Lake.Toml.instDecidableEqTime : DecidableEq Lake.Toml.Time

Equations

• Lake.Toml.instDecidableEqTime = Lake.Toml.decEqTime✝

@[reducible, inline]

abbrev Lake.Toml.Time.IsValidHour (h : Nat) : Prop

Equations

• Lake.Toml.Time.IsValidHour h = (h ≤ 23)

@[reducible, inline]

abbrev Lake.Toml.Time.IsValidMinute (m : Nat) : Prop

Equations

• Lake.Toml.Time.IsValidMinute m = (m ≤ 59)

@[reducible, inline]

abbrev Lake.Toml.Time.IsValidSecond (s : Nat) : Prop

Equations

• Lake.Toml.Time.IsValidSecond s = (s ≤ 60)

def Lake.Toml.Time.zero : Lake.Toml.Time

Equations

• Lake.Toml.Time.zero = { hour := 0, minute := 0, second := 0, fracExponent := 0, fracMantissa := 0 }

instance Lake.Toml.Time.instOfNat : OfNat Lake.Toml.Time 0

Equations

• Lake.Toml.Time.instOfNat = { ofNat := Lake.Toml.Time.zero }

def Lake.Toml.Time.ofValid? (hour : Nat) (minute : Nat) (second : Nat) : Option Lake.Toml.Time

Equations

• One or more equations did not get rendered due to their size.

def Lake.Toml.Time.ofString? (t : String) : Option Lake.Toml.Time

Equations

• One or more equations did not get rendered due to their size.

def Lake.Toml.Time.toString (t : Lake.Toml.Time) : String

Equations

• One or more equations did not get rendered due to their size.

instance Lake.Toml.Time.instToString : ToString Lake.Toml.Time

Equations

• Lake.Toml.Time.instToString = { toString := Lake.Toml.Time.toString }

inductive Lake.Toml.DateTime : Type

A TOML date-time.

• offsetDateTime: Lake.Toml.Date → Lake.Toml.Time → optParam (Option (Bool × Lake.Toml.Time)) none → Lake.Toml.DateTime
• localDateTime: Lake.Toml.Date → Lake.Toml.Time → Lake.Toml.DateTime
• localDate: Lake.Toml.Date → Lake.Toml.DateTime
• localTime: Lake.Toml.Time → Lake.Toml.DateTime

Instances For

• Lake.Toml.DateTime.instToString
• Lake.Toml.instCoeDateDateTime
• Lake.Toml.instCoeTimeDateTime
• Lake.Toml.instInhabitedDateTime

instance Lake.Toml.instInhabitedDateTime : Inhabited Lake.Toml.DateTime

Equations

• Lake.Toml.instInhabitedDateTime = { default := Lake.Toml.DateTime.offsetDateTime default default default }

instance Lake.Toml.instDecidableEqDateTime : DecidableEq Lake.Toml.DateTime

Equations

• Lake.Toml.instDecidableEqDateTime = Lake.Toml.decEqDateTime✝

instance Lake.Toml.instCoeDateDateTime : Coe Lake.Toml.Date Lake.Toml.DateTime

Equations

• Lake.Toml.instCoeDateDateTime = { coe := Lake.Toml.DateTime.localDate }

instance Lake.Toml.instCoeTimeDateTime : Coe Lake.Toml.Time Lake.Toml.DateTime

Equations

• Lake.Toml.instCoeTimeDateTime = { coe := Lake.Toml.DateTime.localTime }

def Lake.Toml.DateTime.ofString? (dt : String) : Option Lake.Toml.DateTime

Equations

• One or more equations did not get rendered due to their size.

def Lake.Toml.DateTime.toString (dt : Lake.Toml.DateTime) : String

Equations

• One or more equations did not get rendered due to their size.
• (Lake.Toml.DateTime.offsetDateTime d t o?).toString = toString "" ++ toString d ++ toString "T" ++ toString t ++ toString "Z"
• (Lake.Toml.DateTime.localDateTime d t).toString = toString "" ++ toString d ++ toString "T" ++ toString t ++ toString ""
• (Lake.Toml.DateTime.localDate d).toString = d.toString
• (Lake.Toml.DateTime.localTime t).toString = t.toString

instance Lake.Toml.DateTime.instToString : ToString Lake.Toml.DateTime

Equations

• Lake.Toml.DateTime.instToString = { toString := Lake.Toml.DateTime.toString }