ISO 8601 datetime containment — the first time dimension for context NATs (docs/context-nat.md).
A DatetimeFn is a structural (unreifiableFunction) constructor taking a
reduced-precision ISO 8601 string that denotes an interval: "2000" is the year,
"2000-01" its January, "2000-01-15" a day, "2000-01-15T13" an hour, and so on
down through minute and second. Because the string stays readable inside the context
expression (an unreifiable NAT is never minted), the structural genlCx producer can read
two DatetimeFn terms and decide containment from their shape alone.
Containment is field nesting: a more-precise instant is inside a less-precise one
whose fields it shares — "2000-01" ⊆ "2000", "2000-01-15" ⊆ "2000-01", while
"2001" ⊄ "2000" (the year differs) and "2000" ⊄ "2000-01" (the year is the
coarser interval, so it contains the month, not the other way).
Everything here is a pure, bounded computation — parse two short strings and compare
vectors — so the producer may call it inside the settle/relabel loop, where a prover
search is forbidden (docs/naf.md). Fields are compared by numeric value, so "2000-1"
and "2000-01" denote the same month.
ISO 8601 datetime containment — the first time dimension for context NATs (docs/context-nat.md). A `DatetimeFn` is a **structural** (`unreifiableFunction`) constructor taking a reduced-precision ISO 8601 string that denotes an *interval*: `"2000"` is the year, `"2000-01"` its January, `"2000-01-15"` a day, `"2000-01-15T13"` an hour, and so on down through minute and second. Because the string stays readable inside the context expression (an unreifiable NAT is never minted), the structural genlCx producer can read two `DatetimeFn` terms and decide containment from their shape alone. Containment is **field nesting**: a more-precise instant is inside a less-precise one whose fields it shares — `"2000-01" ⊆ "2000"`, `"2000-01-15" ⊆ "2000-01"`, while `"2001" ⊄ "2000"` (the year differs) and `"2000" ⊄ "2000-01"` (the year is the *coarser* interval, so it contains the month, not the other way). Everything here is a **pure, bounded** computation — parse two short strings and compare vectors — so the producer may call it inside the settle/relabel loop, where a prover search is forbidden (docs/naf.md). Fields are compared by numeric value, so `"2000-1"` and `"2000-01"` denote the same month.
The structural constructor this namespace reads. A DatetimeFn application is the
time term inside a (CxTimeFn <dimension> (DatetimeFn <iso>)) context.
The structural constructor this namespace reads. A `DatetimeFn` application is the time term inside a `(CxTimeFn <dimension> (DatetimeFn <iso>))` context.
(datetime-term? form)True iff form is a (DatetimeFn "<iso>") term with a parseable ISO string.
True iff `form` is a `(DatetimeFn "<iso>")` term with a parseable ISO string.
(subinterval? a b)True iff datetime term a denotes an interval contained in b's — b's fields are a
prefix of a's and equal field-by-field (reflexive). The interval reading of ISO
reduced precision: fewer fields is a coarser, larger interval, and a finer interval
sharing every coarser field sits inside it. Returns false for anything that is not a
pair of datetime terms, so a caller can hand it any two argument terms.
True iff datetime term `a` denotes an interval contained in `b`'s — `b`'s fields are a prefix of `a`'s and equal field-by-field (reflexive). The interval reading of ISO reduced precision: fewer fields is a coarser, larger interval, and a finer interval sharing every coarser field sits inside it. Returns `false` for anything that is not a pair of datetime terms, so a caller can hand it any two argument terms.
cljdoc builds & hosts documentation for Clojure/Script libraries
| Ctrl+k | Jump to recent docs |
| ← | Move to previous article |
| → | Move to next article |
| Ctrl+/ | Jump to the search field |