Calendar containment — the first time dimension for context NATs (docs/context-nat.md), read off two spellings of the same interval.
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 such terms and decide containment from their shape alone.
YearFn / MonthFn / DayFn are the calendar constructors over the same three
coarsest fields, written as numbers instead of as a string: (YearFn 2000),
(MonthFn 2000 1), (DayFn 2000 1 15). They are unreifiable for the same reason
DatetimeFn is — the fields are what the ordering reads, and a minted constant would
hide them — and each carries one field per argument, so the arity is the
precision and there is no string to parse or mis-parse. A calendar term and the ISO
string naming the same interval read to the same fields, so the two spellings order
against each other as readily as against themselves.
Containment is field nesting: a more-precise interval is inside a less-precise one
whose fields it shares — (MonthFn 2000 1) ⊆ (YearFn 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).
Two sibling months nest neither way, which is what keeps January's facts out of
February.
InstantFn is the other half, and the one thing here that is about moments rather
than stretches: (InstantFn 2000 1 1 0 0 0) is one instant, six integer fields wide,
and bounds reads a calendar term to the two of them it lies between — half-open, so
the end of 1999 and the start of 2000 are the same term. vaelii.impl.calendar
answers startOf / endOf and the orderings out of that (docs/time.md).
Everything here is a pure, bounded computation — parse two short forms 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, and so does (MonthFn 2000 1).
Calendar containment — the first time dimension for context NATs (docs/context-nat.md), read off two spellings of the same interval. 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 such terms and decide containment from their shape alone. `YearFn` / `MonthFn` / `DayFn` are the **calendar constructors** over the same three coarsest fields, written as numbers instead of as a string: `(YearFn 2000)`, `(MonthFn 2000 1)`, `(DayFn 2000 1 15)`. They are unreifiable for the same reason `DatetimeFn` is — the fields are what the ordering reads, and a minted constant would hide them — and each carries **one field per argument**, so the arity *is* the precision and there is no string to parse or mis-parse. A calendar term and the ISO string naming the same interval read to the same fields, so the two spellings order against each other as readily as against themselves. Containment is **field nesting**: a more-precise interval is inside a less-precise one whose fields it shares — `(MonthFn 2000 1) ⊆ (YearFn 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). Two sibling months nest neither way, which is what keeps January's facts out of February. `InstantFn` is the other half, and the one thing here that is about **moments** rather than stretches: `(InstantFn 2000 1 1 0 0 0)` is one instant, six integer fields wide, and `bounds` reads a calendar term to the two of them it lies between — half-open, so the end of 1999 and the start of 2000 are the *same* term. `vaelii.impl.calendar` answers `startOf` / `endOf` and the orderings out of that (docs/time.md). Everything here is a **pure, bounded** computation — parse two short forms 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, and so does `(MonthFn 2000 1)`.
(bounds form)The half-open [start end] a calendar term lies between, each a six-field vector,
or nil for a term that is not a calendar one or names no moment.
Half-open — [start, end) — and that is the convention the whole ordering rests on.
The end of a term is the first moment of the next term at the same precision, so the
end of 1999 and the start of 2000 are one field vector and so one term: an interval's
two bounding instants can then be named without a smallest representable tick to sit
just inside the closing end, and consecutive calendar terms meet rather than being
separated by a gap whose width would depend on how finely the clock was read.
The **half-open** `[start end]` a calendar term lies between, each a six-field vector, or nil for a term that is not a calendar one or names no moment. Half-open — `[start, end)` — and that is the convention the whole ordering rests on. The end of a term is the *first* moment of the next term at the same precision, so the end of 1999 and the start of 2000 are one field vector and so one term: an interval's two bounding instants can then be named without a smallest representable tick to sit just inside the closing end, and consecutive calendar terms **meet** rather than being separated by a gap whose width would depend on how finely the clock was read.
The structural calendar constructors, functor → field count. Each takes one
integer per calendar field, coarsest first, so its arity is its precision:
(YearFn 2000), (MonthFn 2000 1), (DayFn 2000 1 15).
Three and not six. A year, a month and a day are the granularities a context is keyed
by — the ones somebody writes a holiday or a policy for — and each finer field is a
spelling ISO already gives ((DatetimeFn "2000-01-15T13")), read to the same fields
by the same comparator. A constructor per clock field would add nothing the ordering
can see.
The structural **calendar** constructors, `functor → field count`. Each takes one integer per calendar field, coarsest first, so its arity is its precision: `(YearFn 2000)`, `(MonthFn 2000 1)`, `(DayFn 2000 1 15)`. Three and not six. A year, a month and a day are the granularities a context is keyed by — the ones somebody writes a holiday or a policy for — and each finer field is a spelling ISO already gives (`(DatetimeFn "2000-01-15T13")`), read to the same fields by the same comparator. A constructor per clock field would add nothing the ordering can see.
(calendar-term? form)True iff form is a well-formed calendar term — (YearFn 2000), (MonthFn 2000 1) or
(DayFn 2000 1 15).
True iff `form` is a well-formed calendar term — `(YearFn 2000)`, `(MonthFn 2000 1)` or `(DayFn 2000 1 15)`.
The structural ISO constructor this namespace reads. A DatetimeFn application is one
time term inside a (CxTimeFn <dimension> (DatetimeFn <iso>)) context.
The structural ISO constructor this namespace reads. A `DatetimeFn` application is one 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.
(instant-fields form)The six fields of an (InstantFn Y M D h m s) term, or nil for anything that is not
one — a term of the wrong arity, a field out of range, or a date the calendar does not
have. Total, like every other reader here.
The six fields of an `(InstantFn Y M D h m s)` term, or nil for anything that is not one — a term of the wrong arity, a field out of range, or a date the calendar does not have. **Total**, like every other reader here.
The structural constructor for a moment: (InstantFn 2000 1 1 0 0 0) is midnight
at the start of 2000. Six integer fields, always — year, month, day, hour, minute,
second — so its arity is not its precision the way a calendar constructor's is, and
every moment has exactly one spelling. That is the whole reason it is not the
reduced-precision DatetimeFn string: a term is identified by its shape, and
"2000-01-01T00:00:00" and "2000-1-1T0:0:0" are two shapes for one moment where
six integers are one.
A DatetimeFn at full precision denotes the one-second interval, not the instant that
opens it — the whole family names stretches — so the two constructors are kept apart:
YearFn / MonthFn / DayFn / DatetimeFn are temporal_things, InstantFn is a
time_point.
The structural constructor for a **moment**: `(InstantFn 2000 1 1 0 0 0)` is midnight at the start of 2000. Six integer fields, always — year, month, day, hour, minute, second — so its arity is not its precision the way a calendar constructor's is, and every moment has exactly **one** spelling. That is the whole reason it is not the reduced-precision `DatetimeFn` string: a term is identified by its shape, and `"2000-01-01T00:00:00"` and `"2000-1-1T0:0:0"` are two shapes for one moment where six integers are one. A `DatetimeFn` at full precision denotes the one-*second* interval, not the instant that opens it — the whole family names stretches — so the two constructors are kept apart: `YearFn` / `MonthFn` / `DayFn` / `DatetimeFn` are `temporal_thing`s, `InstantFn` is a `time_point`.
(instant-term fields)The (InstantFn …) term six fields name — a PersistentList, the shape
sentex/canon normalizes a sentence's terms to, so a computed instant and one somebody
typed are the same term.
The `(InstantFn …)` term six fields name — a `PersistentList`, the shape `sentex/canon` normalizes a sentence's terms to, so a computed instant and one somebody typed are the same term.
(instant-term? form)True iff form is a well-formed (InstantFn …) term.
True iff `form` is a well-formed `(InstantFn …)` term.
(subinterval? a b)True iff time 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 a
reduced-precision calendar: 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 time terms, so a caller can hand it any two argument terms.
True iff time 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 a reduced-precision calendar: 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 time terms, so a caller can hand it any two argument terms.
(time-term? form)True iff form is any term this namespace reads — a calendar constructor, a
DatetimeFn string, or an InstantFn moment.
What provers/shadowing-channels asks: a goal naming one of these can be decided from
the term's own structure, which is a source no prover reading stored facts has, so
no prover may answer such a goal alone.
True iff `form` is any term this namespace reads — a calendar constructor, a `DatetimeFn` string, or an `InstantFn` moment. What `provers/shadowing-channels` asks: a goal naming one of these can be decided from the term's own **structure**, which is a source no prover reading stored facts has, so no prover may answer such a goal alone.
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 |