Guide vector-ref list runtime repairs
ober
96f843fa426ea730b0816d6b30f6d880d635701e
--- a/src/jcode/core/verified-run.ss +++ b/src/jcode/core/verified-run.ss @@ -1746,6 +1746,27 @@ (else (loop (cdr rest) (+ line-no 1) out left))))) +(def (runtime-primitive-specific-guidance detail primitive) + (let ((lower (string-downcase (or detail "")))) + (cond + ((and (string=? primitive "vector-ref") + (string-contains lower "is not a vector")) + (string-append + "\nThe runtime value printed before `is not a vector` is the actual " + "argument passed to `vector-ref`. If it starts with `(`, that argument " + "is a list, not a vector. Prefer the smallest local edit: change the " + "specific `vector-ref` call whose first argument is that list to " + "`list-ref`, or convert exactly that data initializer to a valid vector " + "of vectors. Do not rewrite the whole constant block unless the one-line " + "accessor repair cannot fit the current data shape.")) + ((and (string=? primitive "vector-set!") + (string-contains lower "is not a vector")) + (string-append + "\nThe runtime value passed to `vector-set!` is not mutable vector data. " + "Repair the specific container shape first: use vectors for mutable " + "grids/rows, or rebuild lists functionally instead of mutating them.")) + (else "")))) + (def (runtime-source-guidance detail cwd) (let* ((primitive (failure-source-primitive detail)) (path (and primitive (failure-source-target-path detail cwd)))) @@ -1758,7 +1779,9 @@ (string-append "Source targets for `" primitive "`:\n" (string-join targets "\n") - "\nRepair the call site or its argument/index guard with the smallest local edit, then call verify.")))))))) + "\nRepair the call site or its argument/index guard with the smallest local edit, then call verify." + (runtime-primitive-specific-guidance + detail primitive))))))))) (def (append-guidance-section base title text) (if (and (string? text) --- a/test/run.ss +++ b/test/run.ss @@ -6482,6 +6482,30 @@ (str-contains? s "smallest local edit"))))) (safe-delete-test-file! target-path)) +(let* ([vr-dir "/tmp"] + [target "jcode-verified-runtime-list-vector-source-target.ss"] + [target-path (string-append vr-dir "/" target)] + [source "(def PIECES (vector (list '#(0 0) '#(0 1))))\n(def (piece-rotations type) (vector-ref PIECES type))\n(def (piece-cells type rotation)\n (let* ([rots (piece-rotations type)])\n (vector-ref rots rotation)))\n"]) + (safe-delete-test-file! target-path) + (write-test-output-file target-path + (lambda (o) (display source o)) + 'replace) + (let* ([scope (parse-write-scope target)] + [result (parameterize ((current-write-scope scope)) + (run-verify-command + "sh -c 'echo \"Exception in vector-ref: (#(0 0) #(0 1)) is not a vector\"; exit 1'" + vr-dir))]) + (check! "verified-run: list/vector source guidance keeps verify failing" + (car result) #f) + (check-pred! "verified-run: list/vector source guidance suggests accessor repair" + (cdr result) + (lambda (s) + (and (str-contains? s "If it starts with `(`") + (str-contains? s "change the specific `vector-ref` call") + (str-contains? s "`list-ref`") + (str-contains? s "Do not rewrite the whole constant block"))))) + (safe-delete-test-file! target-path)) + (let* ([wf (coding-workflow "true" "/tmp" (list (cons 'task-guidance "recipe-context-marker")))]) (check-pred! "verified-run: caller guidance appears in prompt"