RfcDateTime

RfcDateTime :: # (opaque)

RFC 5545 section 3.3.5 extracted DATE-TIME values, profile datetime-values-v1. Accept YYYYMMDDTHHMMSS with optional Z, years 0001–9999, whole seconds. ASCII t/z are accepted and canonical output uses uppercase. Numeric offsets, fractions, lists, whitespace and content lines are malformed. Leap seconds are explicitly unsupported on this POSIX profile, never normalized to 59.

Local means the value has no Z. A surrounding property may supply TZID; this value parser does not invent, retain or validate a property parameter. Without TZID the RFC property is floating. source/local_label expose the validated fields for the shared recurrence and zone APIs with explicit context. Equality includes the UTC/local form; no cross-form total order is defined. These are timestamp labels, not second-wide calendar selections.

Parsing and formatting have constant work and bounded output. A syntactically valid truncated prefix returns Incomplete; malformed prefixes return Malformed. No source spelling, full ICS or versioned persistence claim is made.

import time.RfcDateTime
import time.PosixBoundary
expect {
    value = RfcDateTime.parse("19691231T235959Z")?
    RfcDateTime.utc_boundary(value) == Ok(PosixBoundary.from_microseconds(-1000000))
}
parser_for : encoding -> (state -> Try({ value : RfcDateTime, rest : state }, [InvalidRfcDateTime(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 -> (RfcDateTime, state -> Try(state, err))
    where [
        encoding.encode_str : Str, state -> Try(state, err),
    ]
from_quote : Str -> Try(RfcDateTime, [BadQuotedBytes(Str)])

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

form : RfcDateTime -> Form
source : RfcDateTime -> { date : GregorianDate, clock : ClockTime }
local_label : RfcDateTime -> LocalDateTime

A field label only; callers must preserve form when interpreting it.

utc_boundary : RfcDateTime -> Try(PosixBoundary, [NeedsContext, OutOfRange, ..])

Only explicit Z permits context-free POSIX conversion. A local value requires the caller's interpretation context, even if the fields are zero.

fact_count : RfcDateTime -> U64

Declaration facts retain local versus UTC form. A local value records its need for explicit zone context without choosing one or resolving it.

fact_at : RfcDateTime, U64 -> [End, Item(SemanticFact)]
Form : [Local, Utc]
Error : [Malformed, Incomplete, OutOfRange, InvalidDate, InvalidTime, UnsupportedLeapSecond]