instans

Absolute point-in-time primitive with precision contract.

Syntax: instans | instans<ms> | instans<us> | instans<ns>

Category

conversion

Related

• ↦
• ⇥
• textus

Examples

examples/corpus/conversio/instans.fab (canonical · conversio)

Conversio arms for instans precision family and textus datetime provenance.

# conversio — instans precision family and valor provenance
#
# WHY: `textus ↦ instans<N>` restores datetime provenance from wire carriers;
# `instans ↔ instans` re-tags precision; `instans ↦ textus` emits RFC3339 UTC
# at the declared precision contract (no fabricated sub-precision digits).
#
# textus ↦ instans<N>    — RFC3339 wire per target precision
# instans ↦ instans<ms>  — coarse→fine widening (lossless at storage)
# instans<ns> ↦ instans    — fine→coarse narrowing (truncates sub-second bits)
# instans ↦ textus        — precision-honoring RFC3339 `Z` emit
# textus ↦ instans ⇥ …     — explicit recovery when wire is not a datetime

incipit {
    fixum textus utc ← "1979-05-27T07:32:00.123456Z"
    fixum textus offset ← "1979-05-27T16:32:00+0900"

    fixum instans seconds ← utc ↦ instans
    fixum instans<ms> millis ← seconds ↦ instans<ms>
    fixum instans<us> micros ← utc ↦ instans<us>
    fixum instans<ns> nanos ← utc ↦ instans<ns>
    fixum instans normalized ← offset ↦ instans

    adfirma millis ↦ textus ≡ "1979-05-27T07:32:00.000Z"
    adfirma micros ↦ textus ≡ "1979-05-27T07:32:00.123456Z"
    adfirma normalized ≡ seconds, "offset ingest lands on same UTC instant"

    fixum instans<ns> fine ← nanos
    fixum instans narrowed ← fine ↦ instans
    adfirma narrowed ↦ textus ≡ "1979-05-27T07:32:00Z"

    fixum textus bad ← "not-a-datetime"
    fixum instans recovered ← bad ↦ instans ⇥ seconds
    adfirma recovered ≡ seconds

    nota seconds ↦ textus
    nota millis ↦ textus
    nota micros ↦ textus
    nota nanos ↦ textus
    nota narrowed ↦ textus
}

Expected output:

1979-05-27T07:32:00Z
1979-05-27T07:32:00.000Z
1979-05-27T07:32:00.123456Z
1979-05-27T07:32:00.123456000Z
1979-05-27T07:32:00Z

examples/corpus/instans/instans.fab (canonical · existing-home)

Absolute point-in-time primitive with precision contract.

# instans — wall clock, precision contract, offset ingest, TOML provenance
#
# GRAMMAR:
#   instans | instans<ms> | instans<us> | instans<ns>
#   tempus.nunc() → instans<ns>; downconvert at use site
#   valor ↦ instans<N> | instans ↦ textus
#
# EXPECTED OUTPUT:
#   Smoke asserts exit 0 only.

importa ex "norma:tempus" privata tempus
importa ex "norma:toml" privata toml
importa ex "norma:valor" privata valor

functio epoch_wire(instans t) → textus {
    redde t ↦ textus
}

incipit {
    # --- precision declarations from canonical nanosecond wall clock ---
    fixum instans<ns> nanos ← tempus.nunc()
    fixum instans secunda ← nanos ↦ instans
    fixum instans<ms> millis ← nanos ↦ instans<ms>
    fixum instans<us> micros ← nanos ↦ instans<us>

    # --- valor ↦ instans: UTC wire and numeric offset normalize to same instant ---
    fixum valor utc ← "1979-05-27T07:32:00Z"
    fixum valor offset ← "1979-05-27T03:32:00-04:00"
    fixum instans parsed ← utc ↦ instans
    fixum instans normalized ← offset ↦ instans

    adfirma parsed ≡ normalized, "offset ingest normalizes to UTC instant"

    # --- TOML datetime provenance (Valor::Instans carrier, not textus) ---
    fixum valor doc ← toml.solve("creatus = 1979-05-27T07:32:00.123456Z")
    fixum valor carrier ← valor.cape(doc, "creatus")
    fixum instans<us> fromToml ← carrier ↦ instans<us>
    adfirma fromToml ↦ textus ≡ "1979-05-27T07:32:00.123456Z", "emit honors micros contract"

    # --- precision-tagged equality: distinct at ns, equal at ms ---
    fixum valor leftWire ← "1979-05-27T07:32:00.123456Z"
    fixum valor rightWire ← "1979-05-27T07:32:00.123999Z"
    fixum instans<ns> left ← leftWire ↦ instans<ns>
    fixum instans<ns> right ← rightWire ↦ instans<ns>
    adfirma left ≠ right, "sub-millisecond bits differ at nanosecond precision"
    fixum instans<ms> leftMs ← left ↦ instans<ms>
    fixum instans<ms> rightMs ← right ↦ instans<ms>
    adfirma leftMs ≡ rightMs, "same millisecond at declared ms precision"

    # --- cross-precision conversio: widen and narrow with observable truncation ---
    fixum instans<ns> fine ← parsed ↦ instans<ns>
    fixum instans<ms> coarse ← fine ↦ instans<ms>
    fixum instans seconds ← fine ↦ instans
    adfirma seconds ↦ textus ≡ "1979-05-27T07:32:00Z", "narrow to seconds strips sub-second wire"

    fixum instans<ms> wider ← secunda ↦ instans<ms>
    adfirma wider ≤ millis, "cross-precision comparison at coarser operand"

    # --- wire emit and parse-back via TOML (same instant) ---
    fixum textus wire ← epoch_wire(parsed)
    fixum valor replayDoc ← toml.solve("creatus = 1979-05-27T07:32:00Z")
    fixum valor replayCarrier ← valor.cape(replayDoc, "creatus")
    fixum instans roundtrip ← replayCarrier ↦ instans
    adfirma roundtrip ≡ parsed, "TOML ingest roundtrip matches UTC valor extract"
    adfirma wire ≡ "1979-05-27T07:32:00Z", "seconds-precision wire emit"

    nota wire, secunda, millis, micros, nanos, fromToml, coarse
}