Ixdtf

Ixdtf :: # (opaque)

Internet extended timestamps, rfc9557-microseconds-v1. The base timestamp uses OffsetTimestamp's four-digit Gregorian, six-fractional-digit profile. RFC 9557 sections 2–5 govern ordered annotations and offset assertions. https://www.rfc-editor.org/rfc/rfc9557.html (April 2024).

At most one leading named/numeric zone and 32 ordered key/value annotations. Limits: 4096 total UTF-8 bytes, 255 zone-name bytes, 64 key bytes, 256 value bytes. Parsing performs no provider lookup. Construction retains O(input) storage; bounded duplicate checking is O(tags squared). Serialization uses bounded repeated appends, at most O(tags * output) allocation traffic, with canonical base text and preserved annotation order/criticality. Unknown elective tags and calendar values survive serialization. Experimental keys are rejected. Elective duplicate keys select their first value; any conflicting duplicate involving a critical tag errors; identical tags are retained. Critical tags require understood processing; only u-ca=gregory is supported.

Interpretation uses a strict conflict policy even for elective zone hints. Named zones require supplied matching immutable rules; aliases require the rules' recorded requested-name provenance. No name guessing or data download. Z/-00:00 assert no local offset; numeric +00:00 does. Calendar annotations select presentation only, never reinterpret the base Gregorian fields. Interpretation uses ZoneRules.offset_at in O(transitions) and retains its actual rules. No lazy/budgeted interpretation claim is made. Snapshots expose stored results without resolving again. Non-Gregorian presentation errors. Numeric zone -00:00 denotes a fixed zero offset, serialized as +00:00. Persistence supports this strict snapshot through an explicit versioned profile with its complete immutable context. No complete ISO or broader-calendar claim.

parser_for : encoding -> (state -> Try({ value : Ixdtf, rest : state }, [InvalidIxdtf(Error), Encoding(err), ..]))
    where [
        encoding.parse_str : encoding, state -> Try({ value : Str, rest : state }, err),
    ]

Generic encodings carry canonical text, never the opaque backing record. Encoding failures remain distinct from this profile's validation errors. The encoding owns framing and its work limits; parse bounds the decoded text.

encoder_for : encoding -> (Ixdtf, state -> Try(state, err))
    where [
        encoding.encode_str : Str, state -> Try(state, err),
    ]

from_quote : Str -> Try(Ixdtf, [BadQuotedBytes(Str)])

Typed quoted literals use the same checked profile at compile time. Runtime interpolation remains Str followed by an explicit parse call.

profile : Str

new : Parts -> Try(Ixdtf, Error)

parts : Ixdtf -> Parts

parse : Str -> Try(Ixdtf, Error)

preferred_calendar : Ixdtf -> [None, Some(Str)]

to_text : Ixdtf -> Str

is_eq : Ixdtf, Ixdtf -> Bool

to_hash : Ixdtf, Hasher -> Hasher

fact_count : Ixdtf -> U64

Bounded declaration facts preserve ordered annotations and criticality. A named zone records its context requirement without looking up rules.

fact_at : Ixdtf, U64 -> [End, Item(SemanticFact)]

to_inspect : Ixdtf -> Str

resolve : Ixdtf, [None, Some(ZoneRules)] -> Try(Snapshot, ResolveError)

Strict interpretation: supplied context is required exactly for Named. Elective unknown tags are retained without acting on them. Unsupported elective calendars affect presentation, not the already supplied instant.

ZoneId : [Named(Str), Numeric(FixedOffset)]

Zone : { critical : Bool, identifier : ZoneId }

Tag : { critical : Bool, key : Str, value : Str }

Parts : { timestamp : OffsetTimestamp, zone : [None, Some(Zone)], tags : List(Tag) }

Error : [Base(Error), Malformed, Incomplete, TooLarge, TooManyAnnotations, InvalidZone, InvalidTag, ExperimentalKey, UnknownCritical, ConflictingCritical, UnsupportedCriticalCalendar]

ResolveError : [NeedsContext, UnexpectedContext, ZoneMismatch, OffsetConflict, OutsideValidity, OutOfRange]

Snapshot

Ixdtf.Snapshot :: # (opaque)

resolve : Ixdtf, [None, Some(ZoneRules)] -> Try(Snapshot, ResolveError)

source : Snapshot -> Ixdtf

context : Snapshot -> [None, Some(ZoneRules)]

boundary : Snapshot -> PosixBoundary

offset : Snapshot -> FixedOffset

presentation : Snapshot -> Try(LocalDateTime, [UnsupportedCalendar(Str)])

Read the stored Gregorian projection only when the requested preferred calendar is supported. An absent preference adds no calendar assertion.

reresolve : Snapshot, [None, Some(ZoneRules)] -> Try(Snapshot, ResolveError)

same_position : Snapshot, Snapshot -> Bool

is_eq : Snapshot, Snapshot -> Bool

Snapshot equality includes the source and complete immutable context, even when provider labels are reused. Use same_position for axis equality. Equality/hashing visit the retained definition; getters do not.

to_hash : Snapshot, Hasher -> Hasher

fact_count : Snapshot -> U64

Stored interpretation evidence only: no offset lookup, resolution or presentation conversion happens while reading these facts. The local position is the stored Gregorian projection even if a different requested presentation calendar is unsupported.

fact_at : Snapshot, U64 -> [End, Item(SemanticFact)]

to_inspect : Snapshot -> Str