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"