From e8e25a07b4decfe4a5a0799a212262dffd73edc9 Mon Sep 17 00:00:00 2001 From: bigmerge Date: Mon, 17 Aug 2026 09:27:42 -0500 Subject: [PATCH] EXPERIMENT: temporal adjudication moves out; the placeholder stays 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. --- lang/el-compiler/src/codegen.el | 45 ++++-------------------- lang/tests/integration/temporal_query.sh | 30 ++++++++++++++++ lang/tools/check/temporal.rel | 18 ++++++++++ lang/tools/check/temporal.sh | 22 ++++++++++++ 4 files changed, 77 insertions(+), 38 deletions(-) create mode 100755 lang/tests/integration/temporal_query.sh create mode 100644 lang/tools/check/temporal.rel create mode 100755 lang/tools/check/temporal.sh diff --git a/lang/el-compiler/src/codegen.el b/lang/el-compiler/src/codegen.el index 65ba9df..f1de5d1 100644 --- a/lang/el-compiler/src/codegen.el +++ b/lang/el-compiler/src/codegen.el @@ -589,7 +589,7 @@ fn cg_expr(expr: Map) -> String { if left_is_ct { if op == "Plus" { if right_is_ct { - time_record_violation("caltime_plus_caltime", "CalendarTime + CalendarTime is not allowed (use cal_to_instant + Duration)") + record_call(state_get("__cg_current_fn"), "temporal:caltime_plus_caltime") return "0 /* TIME_TYPE_ERROR: CalendarTime + CalendarTime */" } } @@ -607,7 +607,7 @@ fn cg_expr(expr: Map) -> String { return "el_instant_add_dur(" + left_c + ", " + right_c + ")" } if right_is_inst { - time_record_violation("instant_plus_instant", "Instant + Instant is not allowed") + record_call(state_get("__cg_current_fn"), "temporal:instant_plus_instant") return "0 /* TIME_TYPE_ERROR: Instant + Instant */" } } @@ -619,13 +619,13 @@ fn cg_expr(expr: Map) -> String { return "el_duration_add(" + left_c + ", " + right_c + ")" } if is_int_expr(right) { - time_record_violation("duration_plus_int", "Duration + Int is not allowed (use duration_seconds(n) or N.seconds)") + record_call(state_get("__cg_current_fn"), "temporal:duration_plus_int") return "0 /* TIME_TYPE_ERROR: Duration + Int */" } } if right_is_dur { if is_int_expr(left) { - time_record_violation("duration_plus_int", "Int + Duration is not allowed") + record_call(state_get("__cg_current_fn"), "temporal:duration_plus_int") return "0 /* TIME_TYPE_ERROR: Int + Duration */" } } @@ -644,7 +644,7 @@ fn cg_expr(expr: Map) -> String { return "el_duration_sub(" + left_c + ", " + right_c + ")" } if is_int_expr(right) { - time_record_violation("duration_minus_int", "Duration - Int is not allowed") + record_call(state_get("__cg_current_fn"), "temporal:duration_minus_int") return "0 /* TIME_TYPE_ERROR: Duration - Int */" } } @@ -673,14 +673,14 @@ fn cg_expr(expr: Map) -> String { if left_is_inst { if right_is_inst { return "el_instant_lt(" + left_c + ", " + right_c + ")" } if right_is_dur { - time_record_violation("instant_cmp_duration", "Instant < Duration is not allowed") + record_call(state_get("__cg_current_fn"), "temporal:instant_cmp_duration") return "0 /* TIME_TYPE_ERROR: Instant < Duration */" } } if left_is_dur { if right_is_dur { return "el_duration_lt(" + left_c + ", " + right_c + ")" } if right_is_inst { - time_record_violation("duration_cmp_instant", "Duration < Instant is not allowed") + record_call(state_get("__cg_current_fn"), "temporal:duration_cmp_instant") return "0 /* TIME_TYPE_ERROR: Duration < Instant */" } } @@ -2353,15 +2353,6 @@ fn is_duration_expr(expr: Map) -> Bool { // Record a temporal-type violation. Surfaced as `#error` directives at the // top of the generated C, identical machinery to cap_record_violation. // kinds: "instant_plus_instant", "duration_plus_int", etc. -fn time_record_violation(kind: String, detail: String) -> Bool { - let csv: String = state_get("__time_violations") - if str_eq(csv, "") { let csv = "," } - let entry: String = kind + ":" + detail - let key: String = "," + entry + "," - if str_contains(csv, key) { return true } - state_set("__time_violations", csv + entry + ",") - return true -} // Recursive type-propagation: is `expr` known-Int at codegen time? // This unifies the BinOp(+) dispatch so chained arithmetic over Int @@ -2542,24 +2533,6 @@ fn float_operand_c(expr: Map, expr_c: String) -> String { // as a CSV entry "kind:detail" via time_record_violation. Each entry maps // to a single #error so downstream cc fails the build with a clear El- // source-level message before the bogus C even links. -fn emit_time_violations() -> Void { - let csv: String = state_get("__time_violations") - if str_eq(csv, "") { return } - if str_eq(csv, ",") { return } - let n: Int = str_len(csv) - let i: Int = 1 - while i < n { - let next_comma: Int = str_index_of(str_slice(csv, i, n), ",") - if next_comma < 0 { return } - let entry: String = str_slice(csv, i, i + next_comma) - let colon: Int = str_index_of(entry, ":") - if colon > 0 { - let detail: String = str_slice(entry, colon + 1, str_len(entry)) - emit_line("#error \"temporal type error: " + detail + "\"") - } - let i = i + next_comma + 1 - } -} // -- Builtin arity table ------------------------------------------------------- // @@ -3232,7 +3205,6 @@ fn codegen(stmts: [Map], source: String) -> String { // Clear capability-violation accumulator from any prior compile. // Clear arity-violation accumulator from any prior compile. // Clear temporal-type-violation accumulator from any prior compile. - state_set("__time_violations", "") // Preamble emit_line("#include ") @@ -3498,7 +3470,6 @@ fn codegen(stmts: [Map], source: String) -> String { // so a misuse of a known builtin (wrong arg count) fails the build // with a clear message naming the builtin and its expected arity. // Temporal-type violations (Instant + Instant, Duration + Int, -). - emit_time_violations() // Return empty string - output was streamed via println "" @@ -4007,7 +3978,6 @@ fn emit_streaming_preamble(sigs: [Map], source: String) -> Void { if cgi_count >= 1 { let kind = "cgi" } if svc_count >= 1 { let kind = "service" } state_set("__program_kind", kind) - state_set("__time_violations", "") emit_line("#include ") emit_line("#include ") @@ -4530,7 +4500,6 @@ fn codegen_streaming(tokens: [Any], sigs: [Map], source: String) -> emit_line(" return 0;") emit_line("}") emit_blank() - emit_time_violations() el_arena_pop(main_arena_mark) "" diff --git a/lang/tests/integration/temporal_query.sh b/lang/tests/integration/temporal_query.sh new file mode 100755 index 0000000..0b88bf1 --- /dev/null +++ b/lang/tests/integration/temporal_query.sh @@ -0,0 +1,30 @@ +#!/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 }" +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 diff --git a/lang/tools/check/temporal.rel b/lang/tools/check/temporal.rel new file mode 100644 index 0000000..ae8fb16 --- /dev/null +++ b/lang/tools/check/temporal.rel @@ -0,0 +1,18 @@ +# 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. +# +# means + +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. diff --git a/lang/tools/check/temporal.sh b/lang/tools/check/temporal.sh new file mode 100755 index 0000000..8452c8d --- /dev/null +++ b/lang/tools/check/temporal.sh @@ -0,0 +1,22 @@ +#!/usr/bin/env bash +# temporal.sh — report temporal type violations from emitted relations. +# +# The emitter still has to emit SOMETHING for an illegal expression, so the +# TIME_TYPE_ERROR placeholder stays in the generated C. What moved out is the +# judgment and the wording: codegen records "temporal:instant_plus_instant" and +# this decides what that means. +set -uo pipefail +REL="${1:?usage: temporal.sh [rules]}" +RULES="${2:-$(dirname "${BASH_SOURCE[0]}")/temporal.rel}" +[ -f "$REL" ] || exit 0 +V=0 +while read -r caller _ rest; do + [ "${rest#temporal:}" = "$rest" ] && continue + kind="${rest#temporal:}" + msg=$(awk -v k="$kind" '$1==k && $2=="means" {sub(/^[^ ]+[ ]+means[ ]+/,""); print; exit}' "$RULES") + [ -n "$msg" ] || msg="$kind" + printf 'temporal type error in %s: %s\n' "$caller" "$msg" + V=$((V+1)) +done < <(sort -u "$REL") +[ "$V" -eq 0 ] && echo "temporal: clean" +exit "$V"