nelumbo.datetime

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:

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 a LocalDate; out-of-range values (e.g. month 13) are rejected at parse time with a file:line:col error, not as a query falsehood.
• Time — HH:MM, optionally :SS and a .fff sub-second fraction. Backed by LocalTime. A :00 seconds field — and a zero fraction — is dropped on display (20:04:00.00 prints as 20:04, 20:04:00.30 as 20:04:00.300).
• DateTime — a Date, a literal T, and a Time. Backed by a zone-less LocalDateTime; there is no timezone or offset component.
• Period — an ISO 8601 duration: P followed by date units Y/M/W/D and/or a T-introduced time section with H/M/S (M is months before the T, minutes after it). The two halves are factored into the named patterns YMWD_PERIOD and TIME_PERIOD, so the literal grammar reads <[> P <(> <YMWD_PERIOD> <(> <TIME_PERIOD> <)?> <|> <TIME_PERIOD> <)> <]>. Units must appear in canonical order without repeats — P1D1Y and P1D1D are parse errors. The value normalizes the time part on construction, so P1YT90M becomes P1YT1H30M (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 the FLAG notes in datetimeTest.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

(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 P1M versus P30D has no exact answer. This is an explicit ordering convention used only by >/</<=/>=. Period equality, by contrast, is field-based, so P1M and P30D are 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

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:

datetime_add, date_add, time_add, period_add, and period_multiply are private and are not visible to importers.

See also

• integers.md — the relational add/> idiom this module mirrors, lifted to dates and durations
• built-in-tokens.md — the <[> … <]> connected-token groups the literals are built from
• native-classes.md — catalogue of the @-bound classes, including the datetime natives
• datetimeTest.nl — executable specification covering every operator and the parse-time edge cases