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: Std.Time.Text

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

• full: Std.Time.Text

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

• narrow: Std.Time.Text

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

instance Std.Time.instReprText : Repr Std.Time.Text

Equations

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

instance Std.Time.instInhabitedText : Inhabited Std.Time.Text

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

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

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 Std.Time.Number

Equations

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

instance Std.Time.instInhabitedNumber : Inhabited Std.Time.Number

def Std.Time.classifyNumberText : Nat → Option (Std.Time.Number ⊕ Std.Time.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: Std.Time.Fraction

  Nanosecond precision (up to 9 digits)

• truncated: Nat → Std.Time.Fraction

  Fewer digits (truncated precision)

instance Std.Time.instReprFraction : Repr Std.Time.Fraction

instance Std.Time.instInhabitedFraction : Inhabited Std.Time.Fraction

Equations

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

def Std.Time.Fraction.classify (nat : Nat) : Option Std.Time.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.

• twoDigit: Std.Time.Year

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

• fourDigit: Std.Time.Year

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

• extended: Nat → Std.Time.Year

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

instance Std.Time.instReprYear : Repr Std.Time.Year

Equations

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

instance Std.Time.instInhabitedYear : Inhabited Std.Time.Year

Equations

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

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

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

inductive Std.Time.ZoneId : Type

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

• short: Std.Time.ZoneId

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

• full: Std.Time.ZoneId

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

instance Std.Time.instReprZoneId : Repr Std.Time.ZoneId

Equations

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

instance Std.Time.instInhabitedZoneId : Inhabited Std.Time.ZoneId

def Std.Time.ZoneId.classify (num : Nat) : Option Std.Time.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.

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: Std.Time.ZoneName

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

• full: Std.Time.ZoneName

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

instance Std.Time.instReprZoneName : Repr Std.Time.ZoneName

instance Std.Time.instInhabitedZoneName : Inhabited Std.Time.ZoneName

def Std.Time.ZoneName.classify (letter : Char) (num : Nat) : Option Std.Time.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.

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: Std.Time.OffsetX

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

• hourMinute: Std.Time.OffsetX

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

• hourMinuteColon: Std.Time.OffsetX

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

• hourMinuteSecond: Std.Time.OffsetX

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

• hourMinuteSecondColon: Std.Time.OffsetX

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

instance Std.Time.instReprOffsetX : Repr Std.Time.OffsetX

Equations

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

instance Std.Time.instInhabitedOffsetX : Inhabited Std.Time.OffsetX

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

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

inductive Std.Time.OffsetO : Type

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

• short: Std.Time.OffsetO

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

• full: Std.Time.OffsetO

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

instance Std.Time.instReprOffsetO : Repr Std.Time.OffsetO

instance Std.Time.instInhabitedOffsetO : Inhabited Std.Time.OffsetO

def Std.Time.OffsetO.classify (num : Nat) : Option Std.Time.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: Std.Time.OffsetZ

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

• full: Std.Time.OffsetZ

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

• hourMinuteSecondColon: Std.Time.OffsetZ

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

instance Std.Time.instReprOffsetZ : Repr Std.Time.OffsetZ

instance Std.Time.instInhabitedOffsetZ : Inhabited Std.Time.OffsetZ

def Std.Time.OffsetZ.classify (num : Nat) : Option Std.Time.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: Std.Time.Text → Std.Time.Modifier

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

• y: Std.Time.Year → Std.Time.Modifier

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

• u: Std.Time.Year → Std.Time.Modifier

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

• D: Std.Time.Number → Std.Time.Modifier

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

• MorL: Std.Time.Number ⊕ Std.Time.Text → Std.Time.Modifier

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

• d: Std.Time.Number → Std.Time.Modifier

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

• Qorq: Std.Time.Number ⊕ Std.Time.Text → Std.Time.Modifier

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

• w: Std.Time.Number → Std.Time.Modifier

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

• W: Std.Time.Number → Std.Time.Modifier

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

• E: Std.Time.Text → Std.Time.Modifier

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

• eorc: Std.Time.Number ⊕ Std.Time.Text → Std.Time.Modifier

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

• F: Std.Time.Number → Std.Time.Modifier

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

• a: Std.Time.Text → Std.Time.Modifier

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

• h: Std.Time.Number → Std.Time.Modifier

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

• K: Std.Time.Number → Std.Time.Modifier

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

• k: Std.Time.Number → Std.Time.Modifier

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

• H: Std.Time.Number → Std.Time.Modifier

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

• m: Std.Time.Number → Std.Time.Modifier

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

• s: Std.Time.Number → Std.Time.Modifier

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

• S: Std.Time.Fraction → Std.Time.Modifier

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

• A: Std.Time.Number → Std.Time.Modifier

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

• n: Std.Time.Number → Std.Time.Modifier

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

• N: Std.Time.Number → Std.Time.Modifier

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

• V: Std.Time.Modifier

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

• z: Std.Time.ZoneName → Std.Time.Modifier

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

• O: Std.Time.OffsetO → Std.Time.Modifier

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

• X: Std.Time.OffsetX → Std.Time.Modifier

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

• x: Std.Time.OffsetX → Std.Time.Modifier

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

• Z: Std.Time.OffsetZ → Std.Time.Modifier

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

instance Std.Time.instReprModifier : Repr Std.Time.Modifier

Equations

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

instance Std.Time.instInhabitedModifier : Inhabited Std.Time.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: String → Std.Time.FormatPart

  A string literal.

• modifier: Std.Time.Modifier → Std.Time.FormatPart

  A modifier that renders some data into text.

instance Std.Time.instReprFormatPart : Repr Std.Time.FormatPart

instance Std.Time.instCoeStringFormatPart : Coe String Std.Time.FormatPart

Equations

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

instance Std.Time.instCoeModifierFormatPart : Coe Std.Time.Modifier Std.Time.FormatPart

@[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: Std.Time.TimeZone → Std.Time.Awareness

  The format only parses a single timezone.

• any: Std.Time.Awareness

  The format parses any timezone.

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

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

Equations

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

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

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

• string : Std.Time.FormatString

  The format that is not aware of the timezone.

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

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

Equations

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

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

Parses a short value of a Month.Ordinal

def Std.Time.GenericFormat.spec {tz : Std.Time.Awareness} (input : String) : Except String (Std.Time.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 = do let string ← Std.Time.specParser✝.run input pure { string := string }

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

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

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

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

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

Parser for a format with a builder.

Equations

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

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

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

Parses the input string into a ZoneDateTime.

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

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

def Std.Time.GenericFormat.parseBuilder {aw : Std.Time.Awareness} {α : Type} (format : Std.Time.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.

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

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

def Std.Time.GenericFormat.formatGeneric {aw : Std.Time.Awareness} (format : Std.Time.GenericFormat aw) (getInfo : (typ : Std.Time.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.

def Std.Time.GenericFormat.formatGeneric.go (getInfo : (typ : Std.Time.Modifier) → Option (Std.Time.TypeFormat✝ typ)) (data : String) (format : Std.Time.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 : Std.Time.Awareness} (format : Std.Time.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 : Std.Time.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 : Std.Time.Awareness} : Std.Time.Format (Std.Time.GenericFormat aw) fun (x1 : Type) (x2 : Std.Time.GenericFormat aw) => Std.Time.FormatType✝ x1 x2.string

Equations

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