Archived
land temporal adjudication as a query: the emitter records, the rules are data
This commit is contained in:
@@ -589,7 +589,7 @@ fn cg_expr(expr: Map<String, Any>) -> String {
|
|||||||
if left_is_ct {
|
if left_is_ct {
|
||||||
if op == "Plus" {
|
if op == "Plus" {
|
||||||
if right_is_ct {
|
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 */"
|
return "0 /* TIME_TYPE_ERROR: CalendarTime + CalendarTime */"
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
@@ -607,7 +607,7 @@ fn cg_expr(expr: Map<String, Any>) -> String {
|
|||||||
return "el_instant_add_dur(" + left_c + ", " + right_c + ")"
|
return "el_instant_add_dur(" + left_c + ", " + right_c + ")"
|
||||||
}
|
}
|
||||||
if right_is_inst {
|
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 */"
|
return "0 /* TIME_TYPE_ERROR: Instant + Instant */"
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
@@ -619,13 +619,13 @@ fn cg_expr(expr: Map<String, Any>) -> String {
|
|||||||
return "el_duration_add(" + left_c + ", " + right_c + ")"
|
return "el_duration_add(" + left_c + ", " + right_c + ")"
|
||||||
}
|
}
|
||||||
if is_int_expr(right) {
|
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 */"
|
return "0 /* TIME_TYPE_ERROR: Duration + Int */"
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
if right_is_dur {
|
if right_is_dur {
|
||||||
if is_int_expr(left) {
|
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 */"
|
return "0 /* TIME_TYPE_ERROR: Int + Duration */"
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
@@ -644,7 +644,7 @@ fn cg_expr(expr: Map<String, Any>) -> String {
|
|||||||
return "el_duration_sub(" + left_c + ", " + right_c + ")"
|
return "el_duration_sub(" + left_c + ", " + right_c + ")"
|
||||||
}
|
}
|
||||||
if is_int_expr(right) {
|
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 */"
|
return "0 /* TIME_TYPE_ERROR: Duration - Int */"
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
@@ -673,14 +673,14 @@ fn cg_expr(expr: Map<String, Any>) -> String {
|
|||||||
if left_is_inst {
|
if left_is_inst {
|
||||||
if right_is_inst { return "el_instant_lt(" + left_c + ", " + right_c + ")" }
|
if right_is_inst { return "el_instant_lt(" + left_c + ", " + right_c + ")" }
|
||||||
if right_is_dur {
|
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 */"
|
return "0 /* TIME_TYPE_ERROR: Instant < Duration */"
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
if left_is_dur {
|
if left_is_dur {
|
||||||
if right_is_dur { return "el_duration_lt(" + left_c + ", " + right_c + ")" }
|
if right_is_dur { return "el_duration_lt(" + left_c + ", " + right_c + ")" }
|
||||||
if right_is_inst {
|
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 */"
|
return "0 /* TIME_TYPE_ERROR: Duration < Instant */"
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
@@ -2353,15 +2353,6 @@ fn is_duration_expr(expr: Map<String, Any>) -> Bool {
|
|||||||
// Record a temporal-type violation. Surfaced as `#error` directives at the
|
// Record a temporal-type violation. Surfaced as `#error` directives at the
|
||||||
// top of the generated C, identical machinery to cap_record_violation.
|
// top of the generated C, identical machinery to cap_record_violation.
|
||||||
// kinds: "instant_plus_instant", "duration_plus_int", etc.
|
// 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?
|
// Recursive type-propagation: is `expr` known-Int at codegen time?
|
||||||
// This unifies the BinOp(+) dispatch so chained arithmetic over Int
|
// This unifies the BinOp(+) dispatch so chained arithmetic over Int
|
||||||
@@ -2542,24 +2533,6 @@ fn float_operand_c(expr: Map<String, Any>, expr_c: String) -> String {
|
|||||||
// as a CSV entry "kind:detail" via time_record_violation. Each entry maps
|
// 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-
|
// to a single #error so downstream cc fails the build with a clear El-
|
||||||
// source-level message before the bogus C even links.
|
// 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 -------------------------------------------------------
|
// -- Builtin arity table -------------------------------------------------------
|
||||||
//
|
//
|
||||||
@@ -3232,7 +3205,6 @@ fn codegen(stmts: [Map<String, Any>], source: String) -> String {
|
|||||||
// Clear capability-violation accumulator from any prior compile.
|
// Clear capability-violation accumulator from any prior compile.
|
||||||
// Clear arity-violation accumulator from any prior compile.
|
// Clear arity-violation accumulator from any prior compile.
|
||||||
// Clear temporal-type-violation accumulator from any prior compile.
|
// Clear temporal-type-violation accumulator from any prior compile.
|
||||||
state_set("__time_violations", "")
|
|
||||||
|
|
||||||
// Preamble
|
// Preamble
|
||||||
emit_line("#include <stdint.h>")
|
emit_line("#include <stdint.h>")
|
||||||
@@ -3498,7 +3470,6 @@ fn codegen(stmts: [Map<String, Any>], source: String) -> String {
|
|||||||
// so a misuse of a known builtin (wrong arg count) fails the build
|
// so a misuse of a known builtin (wrong arg count) fails the build
|
||||||
// with a clear message naming the builtin and its expected arity.
|
// with a clear message naming the builtin and its expected arity.
|
||||||
// Temporal-type violations (Instant + Instant, Duration + Int, -).
|
// Temporal-type violations (Instant + Instant, Duration + Int, -).
|
||||||
emit_time_violations()
|
|
||||||
|
|
||||||
// Return empty string - output was streamed via println
|
// Return empty string - output was streamed via println
|
||||||
""
|
""
|
||||||
@@ -4007,7 +3978,6 @@ fn emit_streaming_preamble(sigs: [Map<String, Any>], source: String) -> Void {
|
|||||||
if cgi_count >= 1 { let kind = "cgi" }
|
if cgi_count >= 1 { let kind = "cgi" }
|
||||||
if svc_count >= 1 { let kind = "service" }
|
if svc_count >= 1 { let kind = "service" }
|
||||||
state_set("__program_kind", kind)
|
state_set("__program_kind", kind)
|
||||||
state_set("__time_violations", "")
|
|
||||||
|
|
||||||
emit_line("#include <stdint.h>")
|
emit_line("#include <stdint.h>")
|
||||||
emit_line("#include <stdlib.h>")
|
emit_line("#include <stdlib.h>")
|
||||||
@@ -4530,7 +4500,6 @@ fn codegen_streaming(tokens: [Any], sigs: [Map<String, Any>], source: String) ->
|
|||||||
emit_line(" return 0;")
|
emit_line(" return 0;")
|
||||||
emit_line("}")
|
emit_line("}")
|
||||||
emit_blank()
|
emit_blank()
|
||||||
emit_time_violations()
|
|
||||||
el_arena_pop(main_arena_mark)
|
el_arena_pop(main_arena_mark)
|
||||||
|
|
||||||
""
|
""
|
||||||
|
|||||||
Executable
+30
@@ -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 <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
|
||||||
@@ -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.
|
||||||
|
#
|
||||||
|
# <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.
|
||||||
Executable
+22
@@ -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 <relations-file> [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"
|
||||||
Reference in New Issue
Block a user