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.
31 lines
1.7 KiB
Bash
Executable File
31 lines
1.7 KiB
Bash
Executable File
#!/usr/bin/env bash
|
|
# Control for temporal adjudication as a query.
|
|
#
|
|
# The emitter records which illegal combination it saw and still emits a
|
|
# TIME_TYPE_ERROR placeholder -- it has to emit SOMETHING for an illegal
|
|
# expression. What moved out is the judgment and the wording.
|
|
set -uo pipefail
|
|
ELC="${1:?usage: temporal_query.sh <elc>}"
|
|
LANG_DIR="${2:-$(cd "$(dirname "${BASH_SOURCE[0]}")/../.." && pwd)}"
|
|
W=$(mktemp -d); trap 'rm -rf "$W"' EXIT; F=0
|
|
chk(){ [ "$2" = "$3" ] && printf ' ok %s\n' "$1" || { printf ' FAIL %s\n expected %s got %s\n' "$1" "$2" "$3"; F=$((F+1)); }; }
|
|
cd "$LANG_DIR"
|
|
|
|
printf 'fn main() {\n let a: Instant = now()\n let b: Instant = now()\n let c: Instant = a + b\n println("x")\n}\n' > "$W/b.el"
|
|
EL_RELATIONS_OUT="$W/r.txt" "$ELC" "$W/b.el" >/dev/null 2>&1
|
|
chk "the illegal combination is recorded, not judged, by the emitter" \
|
|
"1" "$(grep -c 'temporal:instant_plus_instant' "$W/r.txt")"
|
|
chk "the emitter no longer authors the message" \
|
|
"0" "$("$ELC" "$W/b.el" 2>/dev/null | grep -c 'is not allowed')"
|
|
chk "a placeholder is still emitted for the illegal expression" \
|
|
"1" "$("$ELC" "$W/b.el" 2>/dev/null | grep -c TIME_TYPE_ERROR)"
|
|
out=$("./tools/check/temporal.sh" "$W/r.txt" 2>&1); rc=$?
|
|
chk "the query judges it" "1" "$rc"
|
|
chk "and explains why, from data" "1" "$(echo "$out" | grep -c 'a point plus a point is not a point')"
|
|
|
|
printf 'fn main() {\n let a: Instant = now()\n let d: Duration = el_duration_from_nanos(1)\n let c: Instant = a + d\n println("x")\n}\n' > "$W/g.el"
|
|
EL_RELATIONS_OUT="$W/r2.txt" "$ELC" "$W/g.el" >/dev/null 2>&1
|
|
"./tools/check/temporal.sh" "$W/r2.txt" >/dev/null 2>&1
|
|
chk "a legal program exits 0" "0" "$?"
|
|
echo; echo " 6 assertions, $((6-F)) passed, $F failed"; exit $F
|