bigmerge
c48db6c2a8
Both, at different layers, and the split is the same as everywhere else. The
NUMERAL is convention -- int_to_str was already form 1, because no position
determines that twelve is written 1 then 2 in base ten. The NUMBER is a
position: three things are three things regardless of notation.
But the sharper answer follows from `love = 0`. A bare `3` is a MAGNITUDE WITH
NO AXIS. It is not a position until something gives it a direction, which is
exactly why 3.days needs a calendar and why time_add(t, n, "min") had to carry
its axis as a string.
PREDICTIONS AND RESULTS
P1 numeral = convention, number = position TRUE
P2 a bare literal is dimensionless until context types it TRUE
P3 there is a measurable place where El guesses TRUE
P4 Instant + Int is not caught though Duration + Int is TRUE
P5 the rule catches it TRUE
P6 nothing legitimate in the tree relies on it TRUE
P3/P4 IS THE DEFECT, and it was found by reasoning from the philosophy and then
measured. Duration + Int was refused -- "an Int carries no unit" -- while
let t: Instant = now()
let u: Instant = t + 3
compiled to raw (t + 3) and reported CLEAN. Adding a dimensionless number to a
point is worse than adding it to a displacement: it silently moves the instant
by an unspecified amount. 3 of what? Whatever the representation happens to be,
which is the leak itself. The asymmetry had no justification; the rule was
simply never written.
P6 MATTERED. Two calendar tests looked like Instant + Int:
let later: Instant = i + 1.hour
let later: Instant = base + 15.hours
They are not. `1.hour` lexes to a Duration -- el_duration_from_nanos(1LL *
3600000000000LL) -- and both stay clean. That is the whole answer demonstrated
in one line: t + 3 is refused because 3 has no axis; t + 1.hour is accepted
because .hour supplies one.
104/104 native + 2 new, integration green, fixpoint ok.
20 lines
1.4 KiB
Plaintext
20 lines
1.4 KiB
Plaintext
# temporal.rel — the affine algebra of time, as data.
|
|
#
|
|
# An Instant is a POINT and a Duration is a DISPLACEMENT. Every rule below
|
|
# follows from that, and the set is closed because there are only two kinds of
|
|
# thing: you may add a displacement to a point, subtract two points to get a
|
|
# displacement, and combine displacements. Nothing else is meaningful.
|
|
#
|
|
# The emitter records which illegal combination it saw; this file says what that
|
|
# means and how to say it.
|
|
#
|
|
# <kind> means <message>
|
|
|
|
instant_plus_instant means Instant + Instant is not allowed — a point plus a point is not a point. Subtract them for a Duration, or add a Duration.
|
|
instant_plus_int means Instant + Int is not allowed — a bare literal is a magnitude with no axis. 3 of what? Adding it to a point moves the instant by an unspecified amount. Use a Duration.
|
|
duration_plus_int means Duration + Int is not allowed — an Int carries no unit. Use duration_seconds(n) or N.seconds.
|
|
duration_minus_int means Duration - Int is not allowed — an Int carries no unit.
|
|
instant_cmp_duration means Instant < Duration is not allowed — a point and a displacement are not on the same scale.
|
|
duration_cmp_instant means Duration < Instant is not allowed — a displacement and a point are not on the same scale.
|
|
caltime_plus_caltime means CalendarTime + CalendarTime is not allowed — a CalendarTime already projects an Instant under a Calendar. Use cal_to_instant first.
|