Narrowing a date

Narrowing › date. The names in the examples are those of section 2.

A date alternative is the bare kind, every date from -999999999-01-01 to 999999999-12-31, or {:date, set}: a Feel.Type.NumberSet of the image of the dates, their number of days in the proleptic Gregorian calendar (Feel.Type.Image, D-109). A date is ordered as that number is, so a comparison is read exactly as a number's is, with the image of the other side (D-109). Days are whole numbers, so two sets of dates that follow one another are one ([2020-01-01..2020-01-05] and [2020-01-06..2020-01-09] are [2020-01-01..2020-01-09], Feel.Type.NumberSet.join_whole_neighbours/1): the join of the two branches of an if that split the calendar at a day is date, not the pieces. A date is not a date and time: they are of different kinds, so each is left only by its own.

Comparisons

The null rules are those of every kind (the rule). d < dt compares kinds that have no order between them, so it is never true; d = dt is only true when both are null.

Properties of a date

A fact about d.year, d.month, d.day or d.weekday (Table 67) is a fact about d too: the days of its set whose property is what the fact leaves (D-194). The year does not decrease with the day, so it leaves one interval; the month, the day and the weekday come back every year or week, so they leave a piece for each.

A set of days is kept in at most 16 pieces, and the properties are applied in the order that leaves the fewest: the year (and value), then the month, then the day of the month, then the weekday, each on what the one before left.

So a property narrows the date only as far as the date's set is bounded. A bare date has the whole calendar, and d.month > 6 would need a piece for each of two billion years, so it narrows nothing:

The last row: there is no such month, and the condition cannot be true.

When the date is bounded, by allowed values or by a condition before, the months and days have pieces to keep (dr is a date in [2020-01-01..2022-12-31]):

• dr.month = 2 and dr.day = 29 is the one day of the leap years in the set: February first (three pieces of the months in range), then the 29th of those. Taking the day first would make a piece for each month.
• dr.weekday = 7 has more than 16 Sundays in the set, so the pieces are replaced by the one interval from the first to the last: a superset, and the best a set of 16 can say.
• The else of an and narrows nothing unless both sides do (and and or), which is why the not-true column of a conjunction is mostly the whole set.

The property itself is a subject too (d.year > 2000 is about d.year, a number):

The sets of the properties are exact for year, month, day and weekday while the pieces fit (Feel.Analysis.DateProperties): each number in them is the property of some day of the set. value, the seconds since 1970 of midnight UTC, is a larger set than the days give.

A function of the date (D-170)

day of week(d) = "Monday" is not true of a null, so d is a date (or a date and time, the day of the clock of which it reads). The days of the week are not a set of days, so nothing more is said.

Date arithmetic in a comparison

A date plus or minus a duration, or the difference of two dates, in a comparison, narrows the operands as an arithmetic operation does (number): the date is not null, and is one of those that give such a result. The day of the month is clamped (2024-01-31 + P1M is 2024-02-29), so the sets come from Feel.Analysis.DateArithmetic and not from adding images. A duration that is not a constant gives no set.

The ends at the edge of the calendar (999999999-12-30, -999999999-01-02) are where adding or subtracting the duration would leave the calendar, and the result would be null. As for numbers, the else branch is the dates the comparison is false for and the dates for which the operation is null (number): the difference of two dates is a duration that can be written, and the sum of a date and a duration can leave the calendar, which Feel.Analysis.Failure gives:

• A duration of days and time moves a date by the whole days of its seconds, rounded down, so the dates in the set are those within the days of the duration from its end (d + @"P1D" for the last day, d - @"P1D" for the first).
• A duration of years and months moves the year by the months over twelve, rounded up, so the dates in the set are those of the years that the greatest number of months can leave past the calendar: the year of d + @"P1M" that is the last, all of it, where only December leaves (the set is wider than the dates the run gives null for).
• A duration that is not a constant has as many days or months as the type of it says, and a type that has no bound gives every date, so the else says nothing (d + dd).

Limits

• 16 pieces of days; past it a property leaves the set as it was (a longer interval has every month, every day of a month and every weekday).
• A property of an interval with no whole day in it ((2020-01-01..2020-01-02)) says nothing.

See also: time, date and time, years and months duration, days and time duration; type-system.md, 3.3.