From 1945d848ebedba308d9be03d44dd94e8c9e4d99f Mon Sep 17 00:00:00 2001 From: Tim Nelson Date: Fri, 22 Mar 2024 10:49:48 -0400 Subject: [PATCH] feat: clean up core display so that VSCode can highlight matches --- forge/lang/ast.rkt | 29 +++++++++-------- forge/send-to-kodkod.rkt | 69 ++++++++++++++++++---------------------- 2 files changed, 47 insertions(+), 51 deletions(-) diff --git a/forge/lang/ast.rkt b/forge/lang/ast.rkt index 7d1d73ce..a06852ca 100644 --- a/forge/lang/ast.rkt +++ b/forge/lang/ast.rkt @@ -348,6 +348,7 @@ (define ast-checker-hash (get-ast-checker-hash)) ;(printf "ast-checker-hash ~a~n" (get-ast-checker-hash)) ;(printf "name: ~a args: ~a key:~a ~n" 'name raw-args key) + ;(printf "name: ~a args: ~a loc:~a ~n" 'name raw-args (nodeinfo-loc info)) ; Perform intexpr->expr and expr->intexpr coercion if needed: (define args (cond [(equal? node/expr? childtype) @@ -1240,20 +1241,22 @@ ; custom user error that contains the row and column information of the offending ; AST node. -(define (pretty-loc loc) - (format "~a:~a:~a (span ~a)" (srcloc-source loc) (srcloc-line loc) (srcloc-column loc) (srcloc-span loc))) +(define (pretty-loc context) + (define loc + (cond [(nodeinfo? context) (nodeinfo-loc context)] + ; Wheats/chaffs have their inner formula in the info field + [(and (node? context) (node? (node-info context))) + (nodeinfo-loc (node-info (node-info context)))] + [(node? context) (nodeinfo-loc (node-info context))] + [(srcloc? context) context] + [(syntax? context) (build-source-location context)] + [else #f])) + (if loc + (format "~a:~a:~a (span ~a)" (srcloc-source loc) (srcloc-line loc) (srcloc-column loc) (srcloc-span loc)) + "unknown:?:?")) (define (raise-forge-error #:msg [msg "error"] #:context [context #f] #:raise? [raise? #t]) - (define loc (cond - [(nodeinfo? context) (pretty-loc (nodeinfo-loc context))] - ; Wheats/chaffs have their inner formula in the info field - [(and (node? context) (node? (node-info context))) - (pretty-loc (nodeinfo-loc (node-info (node-info context))))] - [(node? context) (pretty-loc (nodeinfo-loc (node-info context)))] - [(srcloc? context) (pretty-loc context)] - [(syntax? context) (pretty-loc (build-source-location context))] - [else "unknown:?:?"])) (if raise? - (raise-user-error (format "[~a] ~a" loc msg)) - (fprintf (current-error-port) "[~a] ~a" loc msg))) + (raise-user-error (format "[~a] ~a" (pretty-loc context) msg)) + (fprintf (current-error-port) "[~a] ~a" (pretty-loc context) msg))) diff --git a/forge/send-to-kodkod.rkt b/forge/send-to-kodkod.rkt index efcb6a04..a2f61c40 100644 --- a/forge/send-to-kodkod.rkt +++ b/forge/send-to-kodkod.rkt @@ -360,39 +360,25 @@ all-rels all-atoms)) - ; Note on cores: if core granularity is high, Kodkod may return a formula we do not have an ID for - (define (do-core-highlight nd) - (define loc (nodeinfo-loc (node-info nd))) - (when (@>= (get-verbosity) VERBOSITY_LOW) - (printf " Core contained location: ~a~n" (srcloc->string loc))) - (when (@>= (get-verbosity) VERBOSITY_HIGH) - (pretty-print nd))) -; (if (is-drracket-linked?) -; (do-forge-highlight loc CORE-HIGHLIGHT-COLOR 'core) -; (begin -; ))) - + ; Note on cores: if core granularity is high, Kodkod may return a formula we do not have an ID for. + (define (pretty-core idx max known? fmla) + (fprintf (current-error-port) "Core(~a of ~a): [~a] ~a~n" (@+ idx 1) max (pretty-loc fmla) + (if known? (deparse fmla) fmla))) (when (and (Unsat? result) (Unsat-core result)) ; if we have a core (when (@>= (get-verbosity) VERBOSITY_DEBUG) (printf "core-map: ~a~n" core-map) (printf "core: ~a~n" (Unsat-core result))) - (cond ;[(is-drracket-linked?) - ; (do-forge-unhighlight 'core)] - [else - (when (@>= (get-verbosity) VERBOSITY_LOW) - (printf "No DrRacket linked, could not highlight core. Will print instead.~n"))]) - (for-each do-core-highlight - (filter-map (λ (id) - (let ([fmla-num (if (string-prefix? id "f:") (string->number (substring id 2)) #f)]) - (cond [(member fmla-num (hash-keys core-map)) - ; This is a formula ID and we know it - ;(printf "LOC: ~a~n" (nodeinfo-loc (node-info (hash-ref core-map fmla-num)))) - (hash-ref core-map fmla-num)] - [else - ; This is NOT a known formula id, but it's part of the core - (printf "WARNING: Core also contained: ~a~n" id) - #f]))) - (Unsat-core result)))) + (when (@>= (get-verbosity) VERBOSITY_LOW) + (printf "Unsat core available; printing it with source-location (where available):~n")) + (for ([id (Unsat-core result)] + [idx (range (length (Unsat-core result)))]) + (let ([fmla-num (if (string-prefix? id "f:") (string->number (substring id 2)) #f)]) + (cond [(member fmla-num (hash-keys core-map)) + ; This is a formula ID and we know it + (pretty-core idx (length (Unsat-core result)) fmla-num (hash-ref core-map fmla-num))] + [else + ; This is NOT a known formula id, but it's part of the core + (pretty-core idx (length (Unsat-core result)) #f id)])))) (when (@>= (get-verbosity) VERBOSITY_LOW) (displayln (format-statistics (if (Sat? result) (Sat-stats result) (Unsat-stats result))))) @@ -785,7 +771,10 @@ Please declare a sufficient scope for ~a." (define-values (bound-lower-size bound-upper-size) (values (length bound-lower) (length bound-upper))) (match-define (Range int-lower int-upper) (hash-ref (Scope-sig-scopes (Run-spec-scope run-spec)) (Sig-name sig) (Range #f #f))) - + + ; Sub-optimal, because it points to the sig definition + (define info (nodeinfo (nodeinfo-loc (node-info sig)) 'checklangNoCheck)) + (append (if (@and int-lower (@> int-lower bound-lower-size)) (let () @@ -794,7 +783,9 @@ Please declare a sufficient scope for ~a." "Sig: ~a, Lower-bound: ~a, Max-int: ~a") sig int-lower (sub1 max-int)) (get-blame-node run-spec sig))) - (list (int<= (int int-lower) (card sig)))) + (list (||/info info + (int (no (& sig1 sig2)) ; (unless both are #:one, in which case exact-bounds should enforce this constraint) (define (disjoin-pair sig1 sig2) - (let ([loc (nodeinfo-loc (node-info sig2))]) - (cond [(and (Sig-one sig1) (Sig-one sig2)) - true] - [else - (no (&/info (nodeinfo loc 'checklangNoCheck) sig1 sig2))]))) + (let* ([loc (nodeinfo-loc (node-info sig2))] + [info (nodeinfo loc 'checklangNoCheck)]) + (cond [(and (Sig-one sig1) (Sig-one sig2)) true] + [else (no/info info (&/info info sig1 sig2))]))) (define (disjoin-list a-sig a-list) (map (curry disjoin-pair a-sig) a-list)) (define (disjoin a-list) @@ -871,7 +863,8 @@ Please declare a sufficient scope for ~a." (define (get-relation-preds run-spec) (for/list ([relation (get-relations run-spec)]) (define sig-rels (get-sigs run-spec relation)) - (in relation (-> sig-rels)))) + (define info (nodeinfo (nodeinfo-loc (node-info relation)) 'checklangNoCheck)) + (in/info info relation (->/info info sig-rels)))) #|