`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:

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 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

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 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

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.

Navigation Menu

Uh oh!

`nelumbo.datetime`

Types

Literals

Arithmetic

Comparison

Native classes

Exports summary

See also

Uh oh!

FilesExpand file tree

datetime.md

Latest commit

History

datetime.md

File metadata and controls

nelumbo.datetime

Types

Literals

Arithmetic

Comparison

Native classes

Exports summary

See also

`nelumbo.datetime`