Time.Format.Parse.Instances

source

def Parsec.count {α : Type} (n : Nat) (p : Std.Internal.Parsec.String.Parser α) :

Std.Internal.Parsec.String.Parser (List α)

Equations

Parsec.count n p = List.mapM id (List.replicate n p)

Instances For

source

def Parsec.choice {α : Type} :

List (Std.Internal.Parsec.String.Parser α) → Std.Internal.Parsec.String.Parser α

Equations

Parsec.choice [] = Std.Internal.Parsec.fail ""
Parsec.choice [p] = p
Parsec.choice (p :: ps) = (Std.Internal.Parsec.attempt p <|> Parsec.choice ps)

Instances For

source

def Parsec.toNat (chars : List Char) :

Nat

Equations

Parsec.toNat chars = List.foldl (fun (acc : Nat) (c : Char) => 10 * acc + (c.val.toNat - '0'.val.toNat)) 0 chars

Instances For

source

def Parsec.nat (n : Nat) :

Std.Internal.Parsec.String.Parser Nat

Equations

Parsec.nat n = do let __do_lift ← Parsec.count n Std.Internal.Parsec.String.digit pure (Parsec.toNat __do_lift)

Instances For

source

def Parsec.digits (n : Nat) :

Std.Internal.Parsec.String.Parser String

Equations

Parsec.digits n = do let __do_lift ← Parsec.count n Std.Internal.Parsec.String.digit pure __do_lift.asString

Instances For

source

def Parsec.allowChar (c : Char) :

Std.Internal.Parsec.String.Parser String

Equations

Parsec.allowChar c = ((fun (x : Char) => x.toString) <$> Std.Internal.Parsec.String.pchar c <|> pure "")

Instances For

source

instance Time.instMonadFailOption (α : Type) :

MonadFail Option α

Equations

Time.instMonadFailOption α = { fail := fun (x : String) => none }

source

instance Time.instMonadFailParser (α : Type) :

MonadFail Std.Internal.Parsec.String.Parser α

Equations

Time.instMonadFailParser α = { fail := fun (s : String) (it : String.Iterator) => Std.Internal.Parsec.ParseResult.error it s }

source

instance Time.instReadMaybeString :

ReadMaybe String

Equations

Time.instReadMaybeString = { readMaybe := fun (s : String) => some s }

source

instance Time.instReadMaybeInt :

ReadMaybe Int

Equations

Time.instReadMaybeInt = { readMaybe := fun (s : String) => s.toInt? }

source

inductive Time.PaddingSide :

Type

PrePadding : PaddingSide
PostPadding : PaddingSide

Instances For

source

inductive Time.WeekType :

Type

ISOWeek : WeekType
SundayWeek : WeekType
MondayWeek : WeekType

Instances For

source

instance Time.instReprWeekType :

Repr WeekType

Equations

Time.instReprWeekType = { reprPrec := Time.reprWeekType✝ }

source

instance Time.instBEqWeekType :

BEq WeekType

Equations

Time.instBEqWeekType = { beq := Time.beqWeekType✝ }

source

inductive Time.DayComponent :

Type

DCCentury (y : Int) : DayComponent
DCCenturyYear (y : Int) : DayComponent
DCYearMonth (m : Int) : DayComponent
DCMonthDay (d : Int) : DayComponent
DCYearDay (dy : Int) : DayComponent
DCWeekDay (d : Int) : DayComponent
DCYearWeek (wt : WeekType) (wk : Int) : DayComponent

Instances For

source

instance Time.instReprDayComponent :

Repr DayComponent

Equations

Time.instReprDayComponent = { reprPrec := Time.reprDayComponent✝ }

source

instance Time.instBEqDayComponent :

BEq DayComponent

Equations

Time.instBEqDayComponent = { beq := Time.beqDayComponent✝ }

source

def Time.DCCentury? :

DayComponent → Option Int

Equations

Time.DCCentury? (Time.DayComponent.DCCentury y) = some y
Time.DCCentury? x✝ = none

Instances For

source

def Time.DCCenturyYear? :

DayComponent → Option Int

Equations

Time.DCCenturyYear? (Time.DayComponent.DCCenturyYear y) = some y
Time.DCCenturyYear? x✝ = none

Instances For

source

def Time.DCYearMonth? :

DayComponent → Option Int

Equations

Time.DCYearMonth? (Time.DayComponent.DCYearMonth y) = some y
Time.DCYearMonth? x✝ = none

Instances For

source

def Time.DCMonthDay? :

DayComponent → Option Int

Equations

Time.DCMonthDay? (Time.DayComponent.DCMonthDay y) = some y
Time.DCMonthDay? x✝ = none

Instances For

source

def Time.DCYearDay? :

DayComponent → Option Int

Equations

Time.DCYearDay? (Time.DayComponent.DCYearDay y) = some y
Time.DCYearDay? x✝ = none

Instances For

source

def Time.DCWeekDay? :

DayComponent → Option Int

Equations

Time.DCWeekDay? (Time.DayComponent.DCWeekDay y) = some y
Time.DCWeekDay? x✝ = none

Instances For

source

def Time.DCYearWeek? :

WeekType → DayComponent → Option Int

Equations

Instances For

source

def Time.allowEmptyParser :

Bool → Std.Internal.Parsec.String.Parser String

Equations

Time.allowEmptyParser false = do let x ← Std.Internal.Parsec.many1 Std.Internal.Parsec.String.digit pure x.toList.asString
Time.allowEmptyParser true = do let x ← Std.Internal.Parsec.many Std.Internal.Parsec.String.digit pure x.toList.asString

Instances For

source

def Time.parsePaddedDigits :

PaddingSide → ParseNumericPadding → Bool → Nat → Std.Internal.Parsec.String.Parser String

Equations

Time.parsePaddedDigits x✝² Time.ParseNumericPadding.ZeroPadding x✝¹ x✝ = do let x ← Parsec.count x✝ Std.Internal.Parsec.String.digit pure x.asString
Time.parsePaddedDigits Time.PaddingSide.PrePadding Time.ParseNumericPadding.SpacePadding x✝¹ x✝ = Std.Internal.Parsec.String.ws *> Time.allowEmptyParser x✝¹
Time.parsePaddedDigits Time.PaddingSide.PostPadding Time.ParseNumericPadding.SpacePadding x✝¹ x✝ = Time.allowEmptyParser x✝¹ <* Std.Internal.Parsec.String.ws
Time.parsePaddedDigits x✝¹ Time.ParseNumericPadding.NoPadding false x✝ = do let x ← Std.Internal.Parsec.many1 Std.Internal.Parsec.String.digit pure x.toList.asString
Time.parsePaddedDigits x✝¹ Time.ParseNumericPadding.NoPadding true x✝ = do let x ← Std.Internal.Parsec.many Std.Internal.Parsec.String.digit pure x.toList.asString

Instances For

source

def Time.timeParseTimeSpecifier (l : TimeLocale) (mpad : Option ParseNumericPadding) (s : Specifier) :

Std.Internal.Parsec.String.Parser String

Equations

One or more equations did not get rendered due to their size.
Time.timeParseTimeSpecifier l mpad Time.Specifier.C = Time.timeParseTimeSpecifier.allowNegativeDigits mpad Time.ParseNumericPadding.SpacePadding 2
Time.timeParseTimeSpecifier l mpad Time.Specifier.f = Time.timeParseTimeSpecifier.allowNegativeDigits mpad Time.ParseNumericPadding.SpacePadding 2
Time.timeParseTimeSpecifier l mpad Time.Specifier.Y = Time.timeParseTimeSpecifier.allowNegativeDigits mpad Time.ParseNumericPadding.ZeroPadding 4
Time.timeParseTimeSpecifier l mpad Time.Specifier.G = Time.timeParseTimeSpecifier.allowNegativeDigits mpad Time.ParseNumericPadding.SpacePadding 4
Time.timeParseTimeSpecifier l mpad Time.Specifier.y = Time.timeParseTimeSpecifier.digits mpad Time.ParseNumericPadding.ZeroPadding 2
Time.timeParseTimeSpecifier l mpad Time.Specifier.g = Time.timeParseTimeSpecifier.digits mpad Time.ParseNumericPadding.ZeroPadding 2
Time.timeParseTimeSpecifier l mpad Time.Specifier.B = Time.timeParseTimeSpecifier.oneOf (List.map (fun (x : String × String) => x.fst) l.months)
Time.timeParseTimeSpecifier l mpad Time.Specifier.b = Time.timeParseTimeSpecifier.oneOf (List.map (fun (x : String × String) => x.snd) l.months)
Time.timeParseTimeSpecifier l mpad Time.Specifier.m = Time.timeParseTimeSpecifier.digits mpad Time.ParseNumericPadding.ZeroPadding 2
Time.timeParseTimeSpecifier l mpad Time.Specifier.d = Time.timeParseTimeSpecifier.digits mpad Time.ParseNumericPadding.ZeroPadding 2
Time.timeParseTimeSpecifier l mpad Time.Specifier.e = Time.timeParseTimeSpecifier.digits mpad Time.ParseNumericPadding.SpacePadding 2
Time.timeParseTimeSpecifier l mpad Time.Specifier.V = Time.timeParseTimeSpecifier.digits mpad Time.ParseNumericPadding.ZeroPadding 2
Time.timeParseTimeSpecifier l mpad Time.Specifier.U = Time.timeParseTimeSpecifier.digits mpad Time.ParseNumericPadding.ZeroPadding 2
Time.timeParseTimeSpecifier l mpad Time.Specifier.W = Time.timeParseTimeSpecifier.digits mpad Time.ParseNumericPadding.ZeroPadding 2
Time.timeParseTimeSpecifier l mpad Time.Specifier.u = Time.timeParseTimeSpecifier.oneOf (List.map toString [1, 2, 3, 4, 5, 6, 7])
Time.timeParseTimeSpecifier l mpad Time.Specifier.A = Time.timeParseTimeSpecifier.oneOf (List.map (fun (x : String × String) => x.fst) l.wDays)
Time.timeParseTimeSpecifier l mpad Time.Specifier.a = Time.timeParseTimeSpecifier.oneOf (List.map (fun (x : String × String) => x.snd) l.wDays)
Time.timeParseTimeSpecifier l mpad Time.Specifier.w = Time.timeParseTimeSpecifier.oneOf (List.map toString [0, 1, 2, 3, 4, 5, 6])
Time.timeParseTimeSpecifier l mpad Time.Specifier.j = Time.timeParseTimeSpecifier.digits mpad Time.ParseNumericPadding.ZeroPadding 3
Time.timeParseTimeSpecifier l mpad Time.Specifier.H = Time.timeParseTimeSpecifier.digits mpad Time.ParseNumericPadding.ZeroPadding 2
Time.timeParseTimeSpecifier l mpad Time.Specifier.M = Time.timeParseTimeSpecifier.digits mpad Time.ParseNumericPadding.ZeroPadding 2
Time.timeParseTimeSpecifier l mpad Time.Specifier.S = Time.timeParseTimeSpecifier.digits mpad Time.ParseNumericPadding.ZeroPadding 2
Time.timeParseTimeSpecifier l mpad Time.Specifier.q = Time.timeParseTimeSpecifier.digits' mpad Time.PaddingSide.PostPadding Time.ParseNumericPadding.ZeroPadding true Time.Nano
Time.timeParseTimeSpecifier l mpad Time.Specifier.z = Time.timeParseTimeSpecifier.numericTZ mpad
Time.timeParseTimeSpecifier l mpad Time.Specifier.Ez = Time.timeParseTimeSpecifier.numericTZ mpad
Time.timeParseTimeSpecifier l mpad Time.Specifier.Z = Time.timeParseTimeSpecifier.numericTZ mpad
Time.timeParseTimeSpecifier l mpad Time.Specifier.EZ = Time.timeParseTimeSpecifier.numericTZ mpad
Time.timeParseTimeSpecifier l mpad Time.Specifier.l = Std.Internal.Parsec.fail (toString "specifier 'lIkpP' only valid in format")
Time.timeParseTimeSpecifier l mpad Time.Specifier.I = Std.Internal.Parsec.fail (toString "specifier 'lIkpP' only valid in format")
Time.timeParseTimeSpecifier l mpad Time.Specifier.k = Std.Internal.Parsec.fail (toString "specifier 'lIkpP' only valid in format")
Time.timeParseTimeSpecifier l mpad Time.Specifier.p = Std.Internal.Parsec.fail (toString "specifier 'lIkpP' only valid in format")
Time.timeParseTimeSpecifier l mpad Time.Specifier.P = Std.Internal.Parsec.fail (toString "specifier 'lIkpP' only valid in format")

Instances For

source

def Time.timeParseTimeSpecifier.digits' (mpad : Option ParseNumericPadding) (ps : PaddingSide) (pad : ParseNumericPadding) (allowEmpty : Bool) (n : Nat) :

Std.Internal.Parsec.String.Parser String

Equations

Time.timeParseTimeSpecifier.digits' mpad ps pad allowEmpty n = Time.parsePaddedDigits ps (mpad.getD pad) allowEmpty n

Instances For

source

def Time.timeParseTimeSpecifier.digits (mpad : Option ParseNumericPadding) (pad : ParseNumericPadding) (n : Nat) :

Std.Internal.Parsec.String.Parser String

Equations

Time.timeParseTimeSpecifier.digits mpad pad n = Time.timeParseTimeSpecifier.digits' mpad Time.PaddingSide.PrePadding pad false n

Instances For

source

def Time.timeParseTimeSpecifier.allowNegativeDigits (mpad : Option ParseNumericPadding) (pad : ParseNumericPadding) (n : Nat) :

Std.Internal.Parsec.String.Parser String

Equations

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

Instances For

source

def Time.timeParseTimeSpecifier.oneOf (l : List String) :

Std.Internal.Parsec.String.Parser String

Equations

Time.timeParseTimeSpecifier.oneOf l = Parsec.choice (List.map (fun (x : String) => Std.Internal.Parsec.String.pstring x) l)

Instances For

source

def Time.timeParseTimeSpecifier.numericTZ (mpad : Option ParseNumericPadding) :

Std.Internal.Parsec.String.Parser String

Equations

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

Instances For

source

def Time.timeSubstituteTimeSpecifier :

TimeLocale → SubstituteSpecifier → String

Equations

Instances For

source

def Time.makeDayComponent (l : TimeLocale) (c : Specifier) (s : String) :

Option (List DayComponent)

Equations

One or more equations did not get rendered due to their size.
Time.makeDayComponent l Time.Specifier.Y s = do let a ← Time.readMaybe s pure [Time.DayComponent.DCCentury (a / 100), Time.DayComponent.DCCenturyYear (a % 100)]
Time.makeDayComponent l Time.Specifier.y s = do let a ← Time.readMaybe s pure [Time.DayComponent.DCCentury a]
Time.makeDayComponent l Time.Specifier.m s = do let raw ← Time.readMaybe s let a ← Time.Clip.clip? 1 12 raw Time.makeDayComponent._proof_8 pure [Time.DayComponent.DCYearMonth ↑a]
Time.makeDayComponent l Time.Specifier.d s = do let raw ← Time.readMaybe s let a ← Time.Clip.clip? 1 31 raw Time.makeDayComponent._proof_9 pure [Time.DayComponent.DCMonthDay ↑a]
Time.makeDayComponent l Time.Specifier.u s = do let raw ← Time.readMaybe s let a ← Time.Clip.clip? 1 7 raw Time.makeDayComponent._proof_12 pure [Time.DayComponent.DCWeekDay ↑a]
Time.makeDayComponent l Time.Specifier.w s = do let raw ← Time.readMaybe s let a ← Time.Clip.clip? 0 6 raw Time.makeDayComponent._proof_13 pure [Time.DayComponent.DCWeekDay ↑a]
Time.makeDayComponent l Time.Specifier.j s = do let raw ← Time.readMaybe s let a ← Time.Clip.clip? 1 366 raw Time.makeDayComponent._proof_14 pure [Time.DayComponent.DCYearDay ↑a]
Time.makeDayComponent l c s = pure []

Instances For

source

def Time.makeDayComponent.indexOf? {α : Type} (p : α → Bool) (l : List α) :

Option Int

Equations

Time.makeDayComponent.indexOf? p l = match List.find? (fun (x : α × Nat) => p x.fst) l.zipIdx with | some (fst, i) => some ↑i | x => none

Instances For

source

def Time.makeDayComponents (l : TimeLocale) (pairs : List (Specifier × String)) :

Option (List DayComponent)

Equations

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

Instances For

source

def Time.makeDayComponents.flatten {α : Type} (l : List (List α)) :

List α

Equations

Time.makeDayComponents.flatten l = List.foldr (fun (c acc : List α) => c ++ acc) [] l

Instances For

source

def Time.safeLast {α : Type} (a : α) (l : List α) :

Equations

Time.safeLast a l = (a :: l).getLast ⋯

Instances For

source

instance Time.instParseTimeDay :

ParseTime Day

Equations

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

source

def Time.instParseTimeDay.year (cs : List DayComponent) :

Int

Equations

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

Instances For

source

def Time.instParseTimeDay.rest :

List DayComponent → List DayComponent → Option Day

Equations

One or more equations did not get rendered due to their size.
Time.instParseTimeDay.rest x✝ (Time.DayComponent.DCYearMonth m :: tail) = Time.fromGregorianValid (Time.instParseTimeDay.year x✝) m (Time.safeLast 1 (List.filterMap Time.DCMonthDay? x✝))
Time.instParseTimeDay.rest x✝ (Time.DayComponent.DCYearDay yd :: tail) = Time.fromOrdinalDateValid (Time.instParseTimeDay.year x✝) yd
Time.instParseTimeDay.rest x✝ (head :: xs) = Time.instParseTimeDay.rest x✝ xs
Time.instParseTimeDay.rest x✝ [] = none

Instances For

source

instance Time.instParseTimeDate :

ParseTime Date

Equations

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

source

instance Time.instParseTimeTimeOfDay :

ParseTime TimeOfDay

Equations

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

source

def Time.instParseTimeTimeOfDay.f (tod : TimeOfDay) (pair : Specifier × String) :

Option TimeOfDay

Equations

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

Instances For

source

instance Time.instParseTimeLocalTime :

ParseTime LocalTime

Equations

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

source

def Time.readTzOffset (s : String) :

Option Int

Equations

Time.readTzOffset s = match s.toList with | [s, h1, h2, m1, m2] => Time.readTzOffset.calculate s h1 h2 m1 m2 | x => none

Instances For

source

def Time.readTzOffset.getSign :

Char → Option Int

Equations

Time.readTzOffset.getSign '+' = some 1
Time.readTzOffset.getSign '-' = some (-1)
Time.readTzOffset.getSign x✝ = none

Instances For

source

def Time.readTzOffset.calculate (s h1 h2 m1 m2 : Char) :

Option Int

Equations

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

Instances For

source

instance Time.instParseTimeTimeZone :

ParseTime TimeZone

Equations

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

source

def Time.instParseTimeTimeZone.f (tz : TimeZone) (pair : Specifier × String) :

Option TimeZone

Equations

Time.instParseTimeTimeZone.f tz (Time.Specifier.z , s) = do let offset ← Time.readTzOffset s pure { timeZoneMinutes := offset, timeZoneSummerOnly := false, timeZoneName := "" }
Time.instParseTimeTimeZone.f tz pair = some tz

Instances For

source

instance Time.instParseTimeZonedTime :

ParseTime ZonedTime

Equations

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