Narrowing › time. The names in the examples are those of section 2.
A time alternative is the bare kind, every time of day, or {:time, set}: a set of the second of the day a value falls in (Feel.Type.Moment, D-109, D-118). A time is not ordered as a number is, because the order of two times depends on their zones (Feel.Runtime.Temporal.compare/3):
- when either has no zone, their local clocks are compared;
- when both have a zone, their instants are compared, at the second.
So a set has several lines of numbers, far apart on the number line, and a value is in it when its numbers are on the right lines:
| Line | Of | Written |
|---|---|---|
| the clock | the values with no zone | [08:00:00..18:00:00] |
| the zoned clock | the values with a zone: their local clock | zoned clock [08:00:00..18:00:00] |
| the instants | the values with a zone: the instant, as the seconds of the day less the offset (not wrapped, so it can be negative or past 24:00) | instants [-10:00:00Z..12:00:00Z) |
A set that has the clock and the instants of every zone is written any zone: time in [08:00:00..18:00:00] any zone is a time between eight and six, whatever its zone. A fourth line, the fraction of the second, is the same for every zone (D-118): comparisons look at the second, and only sums, differences and the second property look at the fraction.
Comparing with a time without a zone
The other side has a clock and no zone, so the comparison is on the clock whatever the subject's zone is: the subject's own clock for a value with a zone as well.
| Condition | tm when true | tm when not true |
|---|---|---|
tm < @"12:00:00" | time in [00:00:00..12:00:00) any zone | time in [12:00:00..23:59:59] any zone | Null |
tm = @"12:00:00" | time = 12:00:00 any zone | time in [00:00:00..12:00:00), (12:00:00..23:59:59] any zone | Null |
tm instance of time | time | Null |
| Condition | tmr when true | tmr when not true |
|---|---|---|
tmr < @"12:00:00" | time in [08:00:00..12:00:00) any zone | time in [12:00:00..18:00:00] any zone | Null |
tmr between @"09:00:00" and @"10:00:00" | time in [09:00:00..10:00:00] any zone | time in [08:00:00..09:00:00), (10:00:00..18:00:00] any zone | Null |
(tmr is a time in [08:00:00..18:00:00]; tm is any time.)
Comparing with a time that has a zone
Now the values with no zone are compared by their clock with the other side's, and the values with a zone by their instant. The sets for which a comparison can be true and for which it can be false are no longer each other's complement: two times ten hours apart can be either, since the other side may or may not have a zone. So the lines overlap, within the largest offset, which is 18 hours (a fixed offset is within 14, and the zones of the time zone database had a local mean time of up to 15 hours 56 minutes).
| Condition | tm when true | tm when not true |
|---|---|---|
tm < @"12:00:00Z" | time in [00:00:00..12:00:00), instants [-18:00:00Z..12:00:00Z) | time in [12:00:00..23:59:59], instants [12:00:00Z..41:59:59Z] | Null |
tm < @"12:00:00+01:00" | time in [00:00:00..12:00:00), instants [-18:00:00Z..11:00:00Z) | time in [12:00:00..23:59:59], instants [11:00:00Z..41:59:59Z] | Null |
| Condition | tmr when true | tmr when not true |
|---|---|---|
tmr >= @"12:00:00Z" | time in [12:00:00..18:00:00], zoned clock [08:00:00..18:00:00], instants [12:00:00Z..36:00:00Z] | time in [08:00:00..12:00:00), zoned clock [08:00:00..18:00:00], instants [-10:00:00Z..12:00:00Z) | Null |
Read the first row as: a time below noon UTC is either one without a zone whose clock is before twelve, or one with a zone whose instant is before 12:00:00Z. The instants can reach -18:00:00Z (a clock at midnight in an offset of +18 hours) and past 24:00 (41:59:59Z is 23:59:59 in an offset of −18 hours).
Properties of a time
A fact about tm.hour, tm.minute or tm.second is a fact about tm too: the seconds of the set that have it, on each line of clocks, and the instants cut to match (Feel.Analysis.MomentProperties). The seconds of the days are exact. Those of an hour, a minute or a second are the seconds of each hour, minute or day of the interval up to a number of pieces, and beyond that number the set is left as it was.
| Condition | tmr when true | tmr when not true |
|---|---|---|
tmr.hour >= 12 | time in [12:00:00..18:00:00] any zone | time in [08:00:00..11:59:59] any zone | Null |
tmr.hour = 9 and tmr.minute < 30 | time in [09:00:00..09:29:59] any zone | time in [08:00:00..18:00:00] any zone | Null |
| Condition | tm when true | tm when not true |
|---|---|---|
tm.hour >= 12 | time in [12:00:00..23:59:59] any zone | time in [00:00:00..11:59:59] any zone | Null |
A time has no year, month, day or weekday (tm.year is null, with an invalid_property warning).
time offset, timezone and value depend on the zone, so a time without one has none of them, and a true fact about one leaves only the line of the instants: the values that have a zone (Feel.Analysis.MomentZones works out their sets).
| Condition | tm when true | tm when not true |
|---|---|---|
tm.time offset = @"PT0S" | time in instants [00:00:00Z..23:59:59Z] | time | Null |
Limits
- The line of the instants and the line of the zoned clock are each within 18 hours of the other, and
normalize/2cuts both to that. - A set of seconds that is too fragmented (
tm.second = 0is a second in every minute of the day) is left as it was, with the lines of the clock and the instants whole. - The fraction line has every fraction when nothing is known.
See also: date and time, date; Feel.Type.Moment and Feel.Analysis.MomentTests have the algebra.