nelumbo.datetime
June 23, 2026 · View on GitHub
ISO 8601 dates, times, date-times, and durations, with chronological comparison and reversible arithmetic.
Source: src/main/resources/org/modelingvalue/nelumbo/datetime/datetime.nl — 95 lines.
Import:
import nelumbo.datetime
nelumbo.datetime imports nelumbo.integers (which transitively imports nelumbo.logic), so Integer, the Boolean type, connectives, and equality all come along automatically. Integer is needed for the Period * Integer scaling operator.
Types
DateTime :: Object
Date :: Object
Time :: Object
Period :: Object
Four independent value types. Each is backed by a java.time value:
| Type | Backed by | Example literal |
|---|---|---|
Date | LocalDate | 2024-01-15 |
Time | LocalTime | 20:04 |
DateTime | LocalDateTime | 2024-01-15T10:30 |
Period | IsoDuration — a calendar Period (Y/M/W/D) plus an exact Duration (H/M/S) | P1DT1H30M |
They are not in a subtype relationship with one another, and there is no implicit conversion between them: a Date plus a Time does not silently become a DateTime, and a Period never converts to an Integer.
Literals
All four literals are written inside a connected-token group (<[> … <]>), which forbids whitespace between the inner tokens — 2024-01-15 must be written tightly, not 2024 - 01 - 15. See built-in-tokens.md for the connected-token mechanism.
Date ::= <[> <NUMBER> - <NUMBER> - <NUMBER> <]> @nelumbo.datetime.NDate
Time ::= <[> <NUMBER> : <NUMBER> <(> : <NUMBER> <(> . <NUMBER> <)?> <)?> <]> @nelumbo.datetime.NTime
DateTime ::= <[> <Date> T <Time#50> <]> @nelumbo.datetime.NDateTime
Period ::= <[> P … <]> @nelumbo.datetime.NPeriod
Date—YYYY-MM-DD. Parsed into aLocalDate; out-of-range values (e.g. month 13) are rejected at parse time with afile:line:colerror, not as a query falsehood.Time—HH:MM, optionally:SSand a.fffsub-second fraction. Backed byLocalTime. A:00seconds field — and a zero fraction — is dropped on display (20:04:00.00prints as20:04,20:04:00.30as20:04:00.300).DateTime— aDate, a literalT, and aTime. Backed by a zone-lessLocalDateTime; there is no timezone or offset component.Period— an ISO 8601 duration:Pfollowed by date unitsY/M/W/Dand/or aT-introduced time section withH/M/S(Mis months before theT, minutes after it). The two halves are factored into the named patternsYMWD_PERIODandTIME_PERIOD, so the literal grammar reads<[> P <(> <YMWD_PERIOD> <(> <TIME_PERIOD> <)?> <|> <TIME_PERIOD> <)> <]>. Units must appear in canonical order without repeats —P1D1YandP1D1Dare parse errors. The value normalizes the time part on construction, soP1YT90MbecomesP1YT1H30M(the calendar part is left as written).
2024-01-15T10:30 = a ? [(a=2024-01-15T10:30)][..]
2024-01-15T10:30:00.30 = a ? [(a=2024-01-15T10:30:00.300)][..]
2024-01-15 = c ? [(c=2024-01-15)][..]
20:04:00 = e ? [(e=20:04)][..]
P1YT90M = x ? [(x=P1YT1H30M)][..]
Known limitation: bare time-only
T-prefixed literals are not parsed as of this writing — see theFLAGnotes indatetimeTest.nl.
Arithmetic
DateTime ::= <DateTime> + <Period> #40, <DateTime> - <Period> #40
Date ::= <Date> + <Period> #40, <Date> - <Period> #40
Time ::= <Time> + <Period> #40, <Time> - <Period> #40
Period ::= <DateTime> - <DateTime> #40, <Date> - <Date> #40, <Time> - <Time> #40,
<Period> + <Period> #40, <Period> - <Period> #40,
<Period> * <Integer> #50
| Pattern | #N | Meaning |
|---|---|---|
<instant> + <Period> | 40 | shift an instant forward by a duration |
<instant> - <Period> | 40 | shift an instant backward by a duration |
<instant> - <instant> | 40 | the duration between two instants |
<Period> + <Period> | 40 | duration addition |
<Period> - <Period> | 40 | duration subtraction |
<Period> * <Integer> | 50 | scale a duration by an integer |
(where <instant> is DateTime, Date, or Time). Underneath, five private natives do the work:
private Boolean ::= datetime_add(<DateTime>,<Period>,<DateTime>) @nelumbo.datetime.Add,
date_add(<Date>,<Period>,<Date>) @nelumbo.datetime.Add,
time_add(<Time>,<Period>,<Time>) @nelumbo.datetime.Add,
period_add(<Period>,<Period>,<Period>) @nelumbo.datetime.Add,
period_multiply(<Period>,<Integer>,<Period>) @nelumbo.datetime.Multiply
DateTime a, b Date c, d Time e, f Period x, y, z Integer n
a+x=b <=> datetime_add(a,x,b) // instant + duration = instant
a-x=b <=> datetime_add(b,x,a) // instant - duration : add viewed backward
a-b=x <=> datetime_add(b,x,a) // instant - instant = duration
x+y=z <=> period_add(x,y,z)
x-y=z <=> period_add(z,y,x)
x*n=y <=> period_multiply(x,n,y)
This is the same relational rewrite idiom as integers: subtraction is datetime_add read from a different angle, so all three of "instant + duration", "instant − duration", and "instant − instant" route through one native (Add). Because the relation has one unbound slot, any operand can be the unknown:
2024-01-15 + P1D = 2024-01-16 ? [()][] // verify
2024-01-15 + P1D = c ? [(c=2024-01-16)][..] // compute result
c + P1D = 2024-01-16 ? [(c=2024-01-15)][..] // solve left instant
2024-01-15 + x = 2024-01-16 ? [(x=P1D)][..] // solve duration
2024-01-16T00:00:00 - 2024-01-15T00:00:00 = x ? [(x=PT24H)][..] // duration between
P1D * 3 = P3D ? [()][]
PT1H + PT30M = PT1H30M ? [()][]
Type-matched durations. date_add only accepts a Period whose time part is zero, and time_add only one whose calendar part is zero — adding PT1H30M to a bare Date, or P1D to a bare Time, has no result. DateTime accepts both parts:
2024-01-15T10:00:00 + PT1H30M = a ? [(a=2024-01-15T11:30)][..]
20:04 + PT1H = 21:04 ? [()][]
Comparison
Boolean ::= <DateTime> ">" <DateTime> #30 @nelumbo.datetime.GreaterThan, … "<", "<=", ">="
Boolean ::= <Date> ">" <Date> #30 @nelumbo.datetime.GreaterThan, …
Boolean ::= <Time> ">" <Time> #30 @nelumbo.datetime.GreaterThan, …
Boolean ::= <Period> ">" <Period> #30 @nelumbo.datetime.GreaterThan, …
Each of the four types gets >, <, <=, >= at precedence 30. As in integers, only > is native; the other three are derived per type:
a<b <=> b>a a<=b <=> a<b | a=b a>=b <=> a>b | a=b
2024-01-16 > 2024-01-15 ? [()][]
20:04 > 20:05 ? [][()]
P2D > P1D ? [()][]
PT2H >= PT2H ? [()][]
2024-01-16T10:30:00 > 2024-01-15T10:30:00 ? [()][]
One comparison convention is worth knowing:
- Periods compare by a nominal magnitude — months count as 30 days, years as 365 — because
P1MversusP30Dhas no exact answer. This is an explicit ordering convention used only by>/</<=/>=. Period equality, by contrast, is field-based, soP1MandP30Dare not equal.
Known limitation: the comparison operators are only exercised on ground terms; reverse-solving a comparison (
2024-01-16 > c) is not covered.
Native classes
| Class | Backs | Role |
|---|---|---|
NDate | the Date literal | constant (LocalDate) |
NTime | the Time literal | constant (LocalTime) |
NDateTime | the DateTime literal | constant (LocalDateTime) |
NPeriod | the Period literal | constant (IsoDuration) |
Add | datetime_add / date_add / time_add (infer) plus period_add (@NelumboMethod) | three-arg relation (instant ± duration, instant − instant, duration ± duration) |
Multiply | period_multiply (@NelumboMethod) | three-arg relation (duration × integer) |
GreaterThan | > on all four types | comparison predicate |
IsoDuration | — | the immutable value record behind Period (not @-bound) |
IsoDuration is the value type, not a functor: it pairs a java.time.Period with a java.time.Duration and supplies the field-based equality, nominal-magnitude comparison, and toString normalization described above. See native-classes.md for the full catalogue.
Exports summary
Added to what nelumbo.integers already exports:
| Kind | Names |
|---|---|
| Types | DateTime, Date, Time, Period |
| Literals | ISO date YYYY-MM-DD, time HH:MM[:SS], date-time YYYY-MM-DDTHH:MM[:SS], period P… |
| Operators | +, - on instants and periods, - between instants, * (period × integer), <, <=, >, >= on each type |
datetime_add, date_add, time_add, period_add, and period_multiply are private and are not visible to importers.
See also
integers.md— the relationaladd/>idiom this module mirrors, lifted to dates and durationsbuilt-in-tokens.md— the<[> … <]>connected-token groups the literals are built fromnative-classes.md— catalogue of the@-bound classes, including the datetime nativesdatetimeTest.nl— executable specification covering every operator and the parse-time edge cases