This module defines the Formatter types. It is based on the Java's DateTimeFormatter format.

inductive Std.Time.Text : Type

Text represents different text formatting styles.

• short : Text

  Short form (e.g., "Tue")

• full : Text

  Full form (e.g., "Tuesday")

• narrow : Text

  Narrow form (e.g., "T")

instance Std.Time.instReprText : Repr Text

Equations

• Std.Time.instReprText = { reprPrec := Std.Time.reprText✝ }

instance Std.Time.instInhabitedText : Inhabited Text

Equations

• Std.Time.instInhabitedText = { default := Std.Time.Text.short }

def Std.Time.Text.classify (num : Nat) : Option Text

classify classifies the number of pattern letters into a Text type.

Equations

• Std.Time.Text.classify num = if num < 4 then some Std.Time.Text.short else if num = 4 then some Std.Time.Text.full else if num = 5 then some Std.Time.Text.narrow else none

structure Std.Time.Number : Type

Number represents different number formatting styles.

• padding : Nat

  The number of digits to pad, based on the count of pattern letters.

instance Std.Time.instReprNumber : Repr Number

Equations

• Std.Time.instReprNumber = { reprPrec := Std.Time.reprNumber✝ }

instance Std.Time.instInhabitedNumber : Inhabited Number

Equations

• Std.Time.instInhabitedNumber = { default := { padding := default } }

def Std.Time.classifyNumberText : Nat → Option (Number ⊕ Text)

classifyNumberText classifies the number of pattern letters into either a Number or Text.

Equations

• Std.Time.classifyNumberText x✝ = if x✝ < 3 then some (Sum.inl { padding := x✝ }) else Sum.inr <$> Std.Time.Text.classify x✝

inductive Std.Time.Fraction : Type

Fraction represents the fraction of a second, which can either be full nanoseconds or a truncated form with fewer digits.

• nano : Fraction

  Nanosecond precision (up to 9 digits)

• truncated (digits : Nat) : Fraction

  Fewer digits (truncated precision)

instance Std.Time.instReprFraction : Repr Fraction

Equations

• Std.Time.instReprFraction = { reprPrec := Std.Time.reprFraction✝ }

instance Std.Time.instInhabitedFraction : Inhabited Fraction

Equations

• Std.Time.instInhabitedFraction = { default := Std.Time.Fraction.nano }

def Std.Time.Fraction.classify (nat : Nat) : Option Fraction

classify classifies the number of pattern letters into either a Fraction. It's used for nano.

Equations

• Std.Time.Fraction.classify nat = if nat < 9 then some (Std.Time.Fraction.truncated nat) else if nat = 9 then some Std.Time.Fraction.nano else none

inductive Std.Time.Year : Type

Year represents different year formatting styles based on the number of pattern letters.

• any : Year

  Any size (e.g., "19000000000000")

• twoDigit : Year

  Two-digit year format (e.g., "23" for 2023)

• fourDigit : Year

  Four-digit year format (e.g., "2023")

• extended (num : Nat) : Year

  Extended year format for more than 4 digits (e.g., "002023")

instance Std.Time.instReprYear : Repr Year

Equations

• Std.Time.instReprYear = { reprPrec := Std.Time.reprYear✝ }

instance Std.Time.instInhabitedYear : Inhabited Year

Equations

• Std.Time.instInhabitedYear = { default := Std.Time.Year.any }

def Std.Time.Year.classify (num : Nat) : Option Year

classify classifies the number of pattern letters into a Year format.

Equations

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

inductive Std.Time.ZoneId : Type

ZoneId represents different time zone ID formats based on the number of pattern letters.

• short : ZoneId

  Short form of time zone (e.g., "PST")

• full : ZoneId

  Full form of time zone (e.g., "Pacific Standard Time")

instance Std.Time.instReprZoneId : Repr ZoneId

Equations

• Std.Time.instReprZoneId = { reprPrec := Std.Time.reprZoneId✝ }

instance Std.Time.instInhabitedZoneId : Inhabited ZoneId

Equations

• Std.Time.instInhabitedZoneId = { default := Std.Time.ZoneId.short }

def Std.Time.ZoneId.classify (num : Nat) : Option ZoneId

classify classifies the number of pattern letters into a ZoneId format.

• If 2 letters, it returns the short form.
• If 4 letters, it returns the full form.
• Otherwise, it returns none.

Equations

• Std.Time.ZoneId.classify num = if num = 2 then some Std.Time.ZoneId.short else if num = 4 then some Std.Time.ZoneId.full else none

inductive Std.Time.ZoneName : Type

ZoneName represents different zone name formats based on the number of pattern letters and whether daylight saving time is considered.

• short : ZoneName

  Short form of zone name (e.g., "PST")

• full : ZoneName

  Full form of zone name (e.g., "Pacific Standard Time")

instance Std.Time.instReprZoneName : Repr ZoneName

Equations

• Std.Time.instReprZoneName = { reprPrec := Std.Time.reprZoneName✝ }

instance Std.Time.instInhabitedZoneName : Inhabited ZoneName

Equations

• Std.Time.instInhabitedZoneName = { default := Std.Time.ZoneName.short }

def Std.Time.ZoneName.classify (letter : Char) (num : Nat) : Option ZoneName

classify classifies the number of pattern letters and the letter type ('z' or 'v') into a ZoneName format.

• For 'z', if less than 4 letters, it returns the short form; if 4 letters, it returns the full form.
• For 'v', if 1 letter, it returns the short form; if 4 letters, it returns the full form.
• Otherwise, it returns none.

Equations

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

inductive Std.Time.OffsetX : Type

OffsetX represents different offset formats based on the number of pattern letters. The output will vary between the number of pattern letters, whether it's the hour, minute, second, and whether colons are used.

• hour : OffsetX

  Only the hour is output (e.g., "+01")

• hourMinute : OffsetX

  Hour and minute without colon (e.g., "+0130")

• hourMinuteColon : OffsetX

  Hour and minute with colon (e.g., "+01:30")

• hourMinuteSecond : OffsetX

  Hour, minute, and second without colon (e.g., "+013015")

• hourMinuteSecondColon : OffsetX

  Hour, minute, and second with colon (e.g., "+01:30:15")

instance Std.Time.instReprOffsetX : Repr OffsetX

Equations

• Std.Time.instReprOffsetX = { reprPrec := Std.Time.reprOffsetX✝ }

instance Std.Time.instInhabitedOffsetX : Inhabited OffsetX

Equations

• Std.Time.instInhabitedOffsetX = { default := Std.Time.OffsetX.hour }

def Std.Time.OffsetX.classify (num : Nat) : Option OffsetX

classify classifies the number of pattern letters into an OffsetX format.

Equations

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

inductive Std.Time.OffsetO : Type

OffsetO represents localized offset text formats based on the number of pattern letters.

• short : OffsetO

  Short form of the localized offset (e.g., "GMT+8")

• full : OffsetO

  Full form of the localized offset (e.g., "GMT+08:00")

instance Std.Time.instReprOffsetO : Repr OffsetO

Equations

• Std.Time.instReprOffsetO = { reprPrec := Std.Time.reprOffsetO✝ }

instance Std.Time.instInhabitedOffsetO : Inhabited OffsetO

Equations

• Std.Time.instInhabitedOffsetO = { default := Std.Time.OffsetO.short }

def Std.Time.OffsetO.classify (num : Nat) : Option OffsetO

classify classifies the number of pattern letters into an OffsetO format.

Equations

• Std.Time.OffsetO.classify 1 = some Std.Time.OffsetO.short
• Std.Time.OffsetO.classify 4 = some Std.Time.OffsetO.full
• Std.Time.OffsetO.classify num = none

inductive Std.Time.OffsetZ : Type

OffsetZ represents different offset formats based on the number of pattern letters (capital 'Z').

• hourMinute : OffsetZ

  Hour and minute without colon (e.g., "+0130")

• full : OffsetZ

  Localized offset text in full form (e.g., "GMT+08:00")

• hourMinuteSecondColon : OffsetZ

  Hour, minute, and second with colon (e.g., "+01:30:15")

instance Std.Time.instReprOffsetZ : Repr OffsetZ

Equations

• Std.Time.instReprOffsetZ = { reprPrec := Std.Time.reprOffsetZ✝ }

instance Std.Time.instInhabitedOffsetZ : Inhabited OffsetZ

Equations

• Std.Time.instInhabitedOffsetZ = { default := Std.Time.OffsetZ.hourMinute }

def Std.Time.OffsetZ.classify (num : Nat) : Option OffsetZ

classify classifies the number of pattern letters into an OffsetZ format.

Equations

• Std.Time.OffsetZ.classify 1 = some Std.Time.OffsetZ.hourMinute
• Std.Time.OffsetZ.classify 2 = some Std.Time.OffsetZ.hourMinute
• Std.Time.OffsetZ.classify 3 = some Std.Time.OffsetZ.hourMinute
• Std.Time.OffsetZ.classify 4 = some Std.Time.OffsetZ.full
• Std.Time.OffsetZ.classify 5 = some Std.Time.OffsetZ.hourMinuteSecondColon
• Std.Time.OffsetZ.classify num = none

inductive Std.Time.Modifier : Type

The Modifier inductive type represents various formatting options for date and time components, matching the format symbols used in date and time strings. These modifiers can be applied in formatting functions to generate custom date and time outputs.

• G (presentation : Text) : Modifier

  G: Era (e.g., AD, Anno Domini, A).

• y (presentation : Year) : Modifier

  y: Year of era (e.g., 2004, 04, 0002, 2).

• u (presentation : Year) : Modifier

  u: Year (e.g., 2004, 04, -0001, -1).

• D (presentation : Number) : Modifier

  D: Day of year (e.g., 189).

• MorL (presentation : Number ⊕ Text) : Modifier

  M: Month of year as number or text (e.g., 7, 07, Jul, July, J).

• d (presentation : Number) : Modifier

  d: Day of month (e.g., 10).

• Qorq (presentation : Number ⊕ Text) : Modifier

  Q: Quarter of year as number or text (e.g., 3, 03, Q3, 3rd quarter).

• w (presentation : Number) : Modifier

  w: Week of week-based year (e.g., 27).

• W (presentation : Number) : Modifier

  W: Week of month (e.g., 4).

• E (presentation : Text) : Modifier

  E: Day of week as text (e.g., Tue, Tuesday, T).

• eorc (presentation : Number ⊕ Text) : Modifier

  e: Localized day of week as number or text (e.g., 2, 02, Tue, Tuesday, T).

• F (presentation : Number) : Modifier

  F: Aligned week of month (e.g., 3).

• a (presentation : Text) : Modifier

  a: AM/PM of day (e.g., PM).

• h (presentation : Number) : Modifier

  h: Clock hour of AM/PM (1-12) (e.g., 12).

• K (presentation : Number) : Modifier

  K: Hour of AM/PM (0-11) (e.g., 0).

• k (presentation : Number) : Modifier

  k: Clock hour of day (1-24) (e.g., 24).

• H (presentation : Number) : Modifier

  H: Hour of day (0-23) (e.g., 0).

• m (presentation : Number) : Modifier

  m: Minute of hour (e.g., 30).

• s (presentation : Number) : Modifier

  s: Second of minute (e.g., 55).

• S (presentation : Fraction) : Modifier

  S: Fraction of second (e.g., 978).

• A (presentation : Number) : Modifier

  A: Millisecond of day (e.g., 1234).

• n (presentation : Number) : Modifier

  n: Nanosecond of second (e.g., 987654321).

• N (presentation : Number) : Modifier

  N: Nanosecond of day (e.g., 1234000000).

• V : Modifier

  V: Time zone ID (e.g., America/Los_Angeles, Z, -08:30).

• z (presentation : ZoneName) : Modifier

  z: Time zone name (e.g., Pacific Standard Time, PST).

• O (presentation : OffsetO) : Modifier

  O: Localized zone offset (e.g., GMT+8, GMT+08:00, UTC-08:00).

• X (presentation : OffsetX) : Modifier

  X: Zone offset with 'Z' for zero (e.g., Z, -08, -0830, -08:30).

• x (presentation : OffsetX) : Modifier

  x: Zone offset without 'Z' (e.g., +0000, -08, -0830, -08:30).

• Z (presentation : OffsetZ) : Modifier

  Z: Zone offset with 'Z' for UTC (e.g., +0000, -0800, -08:00).

instance Std.Time.instReprModifier : Repr Modifier

Equations

• Std.Time.instReprModifier = { reprPrec := Std.Time.reprModifier✝ }

instance Std.Time.instInhabitedModifier : Inhabited Modifier

Equations

• Std.Time.instInhabitedModifier = { default := Std.Time.Modifier.G default }

inductive Std.Time.FormatPart : Type

The part of a formatting string. A string is just a text and a modifier is in the format described in the Modifier type.

• string (val : String) : FormatPart

  A string literal.

• modifier (modifier : Modifier) : FormatPart

  A modifier that renders some data into text.

instance Std.Time.instReprFormatPart : Repr FormatPart

Equations

• Std.Time.instReprFormatPart = { reprPrec := Std.Time.reprFormatPart✝ }

instance Std.Time.instCoeStringFormatPart : Coe String FormatPart

Equations

• Std.Time.instCoeStringFormatPart = { coe := Std.Time.FormatPart.string }

instance Std.Time.instCoeModifierFormatPart : Coe Modifier FormatPart

Equations

• Std.Time.instCoeModifierFormatPart = { coe := Std.Time.FormatPart.modifier }

@[reducible, inline]

abbrev Std.Time.FormatString : Type

The format of date and time string.

Equations

• Std.Time.FormatString = List Std.Time.FormatPart

inductive Std.Time.Awareness : Type

If the format is aware of some timezone data it parses or if it parses any timezone.

• only : TimeZone → Awareness

  The format only parses a single timezone.

• any : Awareness

  The format parses any timezone.

instance Std.Time.Awareness.instCoeTimeZone : Coe TimeZone Awareness

Equations

• Std.Time.Awareness.instCoeTimeZone = { coe := Std.Time.Awareness.only }

instance Std.Time.Awareness.instInhabitedType {aw : Awareness} : Inhabited (Std.Time.Awareness.type✝ aw)

Equations

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

structure Std.Time.FormatConfig : Type

Configuration options for formatting and parsing date/time strings.

• allowLeapSeconds : Bool

  Whether to allow leap seconds, such as 2016-12-31T23:59:60Z. Default is false.

instance Std.Time.instInhabitedFormatConfig : Inhabited FormatConfig

Equations

• Std.Time.instInhabitedFormatConfig = { default := { allowLeapSeconds := default } }

instance Std.Time.instReprFormatConfig : Repr FormatConfig

Equations

• Std.Time.instReprFormatConfig = { reprPrec := Std.Time.reprFormatConfig✝ }

structure Std.Time.GenericFormat (awareness : Awareness) : Type

A specification on how to format a data or parse some string.

• config : FormatConfig

  Configuration options for formatting behavior.

• string : FormatString

  The format string used for parsing and formatting.

instance Std.Time.instInhabitedGenericFormat {a✝ : Awareness} : Inhabited (GenericFormat a✝)

Equations

• Std.Time.instInhabitedGenericFormat = { default := { config := default, string := default } }

instance Std.Time.instReprGenericFormat {awareness✝ : Awareness} : Repr (GenericFormat awareness✝)

Equations

• Std.Time.instReprGenericFormat = { reprPrec := Std.Time.reprGenericFormat✝ }

def Std.Time.parseMonthShort : Internal.Parsec.String.Parser Month.Ordinal

Parses a short value of a Month.Ordinal

Equations

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

def Std.Time.GenericFormat.spec {tz : Awareness} (input : String) (config : FormatConfig := { }) : Except String (GenericFormat tz)

Constructs a new GenericFormat specification for a date-time string. Modifiers can be combined to create custom formats, such as "YYYY, MMMM, D".

Equations

• Std.Time.GenericFormat.spec input config = do let string ← Std.Time.specParser✝.run input pure { config := config, string := string }

def Std.Time.GenericFormat.spec! {tz : Awareness} (input : String) (config : FormatConfig := { }) : GenericFormat tz

Builds a GenericFormat from the input string. If parsing fails, it will panic

Equations

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

def Std.Time.GenericFormat.format {aw : Awareness} {tz : TimeZone} (format : GenericFormat aw) (date : DateTime tz) : String

Formats a DateTime value into a string using the given GenericFormat.

Equations

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

def Std.Time.GenericFormat.builderParser {α : Type} (format : FormatString) (config : FormatConfig) (func : Std.Time.FormatType✝ (Option α) format) : Internal.Parsec.String.Parser α

Parser for a format with a builder.

Equations

• Std.Time.GenericFormat.builderParser format config func = Std.Time.GenericFormat.builderParser.go config format func

def Std.Time.GenericFormat.builderParser.go {α : Type} (config : FormatConfig) (format : FormatString) (func : Std.Time.FormatType✝ (Option α) format) : Internal.Parsec.String.Parser α

Equations

• One or more equations did not get rendered due to their size.
• Std.Time.GenericFormat.builderParser.go config (Std.Time.FormatPart.string s :: xs) func_2 = Std.Internal.Parsec.String.skipString s *> Std.Time.GenericFormat.builderParser.go config xs func_2
• Std.Time.GenericFormat.builderParser.go config [] (some res) = Std.Internal.Parsec.eof *> pure res
• Std.Time.GenericFormat.builderParser.go config [] none = Std.Internal.Parsec.fail "invalid date."

def Std.Time.GenericFormat.parse {aw : Awareness} (format : GenericFormat aw) (input : String) : Except String (Std.Time.Awareness.type✝ aw)

Parses the input string into a ZoneDateTime.

Equations

• format.parse input = (Std.Time.GenericFormat.parser✝ format.string format.config aw <* Std.Internal.Parsec.eof).run input

def Std.Time.GenericFormat.parse! {aw : Awareness} (format : GenericFormat aw) (input : String) : Std.Time.Awareness.type✝ aw

Parses the input string into a ZoneDateTime and panics if its wrong.

Equations

• format.parse! input = match format.parse input with | Except.ok res => res | Except.error err => panicWithPosWithDecl "Std.Time.Format.Basic" "Std.Time.GenericFormat.parse!" 1476 18 err

def Std.Time.GenericFormat.parseBuilder {aw : Awareness} {α : Type} (format : GenericFormat aw) (builder : Std.Time.FormatType✝ (Option α) format.string) (input : String) : Except String α

Parses an input string using a builder function to produce a value.

Equations

• format.parseBuilder builder input = (Std.Time.GenericFormat.builderParser format.string format.config builder).run input

def Std.Time.GenericFormat.parseBuilder! {α : Type} {aw : Awareness} [Inhabited α] (format : GenericFormat aw) (builder : Std.Time.FormatType✝ (Option α) format.string) (input : String) : α

Parses an input string using a builder function, panicking on errors.

Equations

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

def Std.Time.GenericFormat.formatGeneric {aw : Awareness} (format : GenericFormat aw) (getInfo : (typ : Modifier) → Option (Std.Time.TypeFormat✝ typ)) : Option String

Formats the date using the format into a String, using a getInfo function to get the information needed to build the String.

Equations

• format.formatGeneric getInfo = Std.Time.GenericFormat.formatGeneric.go getInfo "" format.string

def Std.Time.GenericFormat.formatGeneric.go (getInfo : (typ : Modifier) → Option (Std.Time.TypeFormat✝ typ)) (data : String) (format : FormatString) : Option String

Equations

• One or more equations did not get rendered due to their size.
• Std.Time.GenericFormat.formatGeneric.go getInfo data (Std.Time.FormatPart.string val :: xs) = Std.Time.GenericFormat.formatGeneric.go getInfo (data ++ val) xs
• Std.Time.GenericFormat.formatGeneric.go getInfo data [] = some data

def Std.Time.GenericFormat.formatBuilder {aw : Awareness} (format : GenericFormat aw) : Std.Time.FormatType✝ String format.string

Constructs a FormatType function to format a date into a string using a GenericFormat.

Equations

• format.formatBuilder = Std.Time.GenericFormat.formatBuilder.go "" format.string

def Std.Time.GenericFormat.formatBuilder.go (data : String) (format : FormatString) : Std.Time.FormatType✝ String format

Equations

• One or more equations did not get rendered due to their size.
• Std.Time.GenericFormat.formatBuilder.go data (Std.Time.FormatPart.string val :: xs) = Std.Time.GenericFormat.formatBuilder.go (data ++ val) xs
• Std.Time.GenericFormat.formatBuilder.go data [] = data

class Std.Time.Format (f : Type) (typ : Type → f → Type) : Type 1

Typeclass for formatting and parsing values with the given format type.

• format (fmt : f) : typ String fmt

  Converts a format f into a string.

• parse {α : Type} (fmt : f) : typ (Option α) fmt → String → Except String α

  Parses a string into a format using the provided format type f.

instance Std.Time.instFormatGenericFormatFormatTypeString {aw : Awareness} : Format (GenericFormat aw) fun (x1 : Type) (x2 : GenericFormat aw) => Std.Time.FormatType✝ x1 x2.string

Equations

• Std.Time.instFormatGenericFormatFormatTypeString = { format := Std.Time.GenericFormat.formatBuilder, parse := fun {α : Type} => Std.Time.GenericFormat.parseBuilder }