bigmerge
e8e25a07b4
The previous pass moved the type DATA and left the judgment inline, which I
stated rather than hid. This finishes it.
PREDICTIONS AND RESULTS
P1 codegen can emit operand-type relations TRUE
"main calls temporal:instant_plus_instant"
P2 the affine rules are a small closed set as data TRUE 6 rules
P3 violations still caught at build time TRUE exit=1
P4 the reporter leaves codegen TRUE 4538 -> 4507
P5 the TIME_TYPE_ERROR placeholder must STAY TRUE
P5 is the boundary of this whole approach. The emitter has to emit SOMETHING
for an illegal expression -- it cannot emit nothing and it cannot decide what
the program meant. So the placeholder is irreducible in the same way the AST
traversal was: what moved is the judgment and the wording, not the fact that
something must be written.
The rules are affine algebra and the set is closed because there are only two
kinds of thing. An Instant is a POINT, a Duration is a DISPLACEMENT: add a
displacement to a point, subtract two points for a displacement, combine
displacements. Nothing else is meaningful, which is why the enumeration in
temporal.rel cannot grow the way an allowlist does.
A defect in my own checker, found by running it: the .rel file uses aligned
columns and my awk assumed a single space, so the message came out with the
rule key still prefixed. Same class as the multi-line header parse in the arity
pass -- formatting assumptions that only fail when you look at the output.
98/98 native, 6/6 temporal_query.sh, fixpoint ok.
19 lines
1.2 KiB
Plaintext
19 lines
1.2 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.
|
|
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.
|