This module defines the Formatter
types. It is based on the Java's DateTimeFormatter
format.
Equations
- Std.Time.instReprText = { reprPrec := Std.Time.reprText✝ }
Equations
- Std.Time.instInhabitedText = { default := Std.Time.Text.short }
Equations
- Std.Time.instReprNumber = { reprPrec := Std.Time.reprNumber✝ }
Equations
- Std.Time.instInhabitedNumber = { default := { padding := default } }
Fraction
represents the fraction of a second, which can either be full nanoseconds
or a truncated form with fewer digits.
Equations
- Std.Time.instReprFraction = { reprPrec := Std.Time.reprFraction✝ }
Equations
- Std.Time.instInhabitedFraction = { default := Std.Time.Fraction.nano }
Equations
- Std.Time.instReprYear = { reprPrec := Std.Time.reprYear✝ }
Equations
- Std.Time.instInhabitedYear = { default := Std.Time.Year.twoDigit }
Equations
- Std.Time.instReprZoneId = { reprPrec := Std.Time.reprZoneId✝ }
Equations
- Std.Time.instInhabitedZoneId = { default := Std.Time.ZoneId.short }
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
ZoneName
represents different zone name formats based on the number of pattern letters and
whether daylight saving time is considered.
Equations
- Std.Time.instReprZoneName = { reprPrec := Std.Time.reprZoneName✝ }
Equations
- Std.Time.instInhabitedZoneName = { default := Std.Time.ZoneName.short }
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.
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")
Equations
- Std.Time.instReprOffsetX = { reprPrec := Std.Time.reprOffsetX✝ }
Equations
- Std.Time.instInhabitedOffsetX = { default := Std.Time.OffsetX.hour }
OffsetO
represents localized offset text formats based on the number of pattern letters.
Equations
- Std.Time.instReprOffsetO = { reprPrec := Std.Time.reprOffsetO✝ }
Equations
- Std.Time.instInhabitedOffsetO = { default := Std.Time.OffsetO.short }
OffsetZ
represents different offset formats based on the number of pattern letters (capital 'Z').
Equations
- Std.Time.instReprOffsetZ = { reprPrec := Std.Time.reprOffsetZ✝ }
Equations
- Std.Time.instInhabitedOffsetZ = { default := Std.Time.OffsetZ.hourMinute }
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).
Equations
- Std.Time.instReprModifier = { reprPrec := Std.Time.reprModifier✝ }
Equations
- Std.Time.instInhabitedModifier = { default := Std.Time.Modifier.G default }
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.
Equations
- Std.Time.instReprFormatPart = { reprPrec := Std.Time.reprFormatPart✝ }
Equations
Equations
The format of date and time string.
Equations
Equations
Equations
- One or more equations did not get rendered due to their size.
A specification on how to format a data or parse some string.
- string : FormatString
The format that is not aware of the timezone.
Equations
- Std.Time.instInhabitedGenericFormat = { default := { string := default } }
Equations
- Std.Time.instReprGenericFormat = { reprPrec := Std.Time.reprGenericFormat✝ }
Parses a short value of a Month.Ordinal
Equations
- One or more equations did not get rendered due to their size.
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 }
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.
Formats a DateTime
value into a string using the given GenericFormat
.
Equations
- One or more equations did not get rendered due to their size.
Parser for a format with a builder.
Equations
- Std.Time.GenericFormat.builderParser format func = Std.Time.GenericFormat.builderParser.go format func
Equations
- Std.Time.GenericFormat.builderParser.go (Std.Time.FormatPart.modifier x :: xs) func_2 = do let res ← Std.Time.parseWith✝ x Std.Time.GenericFormat.builderParser.go xs (func_2 res)
- Std.Time.GenericFormat.builderParser.go (Std.Time.FormatPart.string s :: xs) func_2 = Std.Internal.Parsec.String.skipString s *> Std.Time.GenericFormat.builderParser.go xs func_2
- Std.Time.GenericFormat.builderParser.go [] (some res) = Std.Internal.Parsec.eof *> pure res
- Std.Time.GenericFormat.builderParser.go [] none = Std.Internal.Parsec.fail "invalid date."
Parses the input string into a ZoneDateTime
.
Equations
- format.parse input = (Std.Time.GenericFormat.parser✝ format.string aw <* Std.Internal.Parsec.eof).run input
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!" 1432 18 err
Parses an input string using a builder function to produce a value.
Equations
- format.parseBuilder builder input = (Std.Time.GenericFormat.builderParser format.string builder).run input
Parses an input string using a builder function, panicking on errors.
Equations
- One or more equations did not get rendered due to their size.
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
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
Constructs a FormatType
function to format a date into a string using a GenericFormat
.
Equations
- format.formatBuilder = Std.Time.GenericFormat.formatBuilder.go "" format.string
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
Typeclass for formatting and parsing values with the given format type.
- format (fmt : f) : typ String fmt
Converts a format
f
into a string. Parses a string into a format using the provided format type
f
.
Equations
- Std.Time.instFormatGenericFormatFormatTypeString = { format := Std.Time.GenericFormat.formatBuilder, parse := fun {α : Type} => Std.Time.GenericFormat.parseBuilder }