[minor] January 31st Update

forge/lang/ast.rkt

@@ -80,7 +80,19 @@
 (struct node/int node () #:transparent)
 
 ; Should never be directly instantiated
-(struct node/formula node () #:transparent)
+(struct node/formula node () #:transparent
+  ; Give a friendlier error if Racket thinks we are asking it to treat a formula as a function
+  #:property prop:procedure
+  (λ (f . x)
+    (cond [(node/fmla/pred-spacer? f)
+           (raise-forge-error
+            #:msg (format "Tried to give arguments to a predicate, but it takes none: ~a." (node/fmla/pred-spacer-name f))
+            #:context f)]
+          [else
+           (raise-forge-error
+            #:msg (format "Could not use formula as a function: ~a." (deparse f))
+            #:context f)])))
+
 
 ;; ARGUMENT CHECKS -------------------------------------------------------------
 
@@ -451,15 +463,21 @@
 ; Helper to construct a set comprehension (and give useful errors, in case
 ; these are shown to an end-user)
 (define (raise-set-comp-quantifier-error e)
-  (raise-user-error "Set-comprehension variable domain expected a singleton or relational expression" (deparse e)))
+  (raise-forge-error
+   #:msg (format "Set-comprehension variable domain expected a singleton or relational expression: ~a" (deparse e))
+   #:context e))
 (define (comprehension info decls formula)
   (for ([e (map cdr decls)])
     (unless (node/expr? e)
       (raise-set-comp-quantifier-error e))
     (unless (equal? (node/expr-arity e) 1)
-      (raise-user-error "Set-comprehension variable domain needs arity = 1" (deparse e)))
+      (raise-forge-error
+       #:msg (format "Set-comprehension variable domain needs arity = 1: ~a" (deparse e))
+       #:context e))
     (unless (node/formula? formula)
-      (raise-user-error "Set-comprehension condition expected a formula." (deparse formula))))
+      (raise-forge-error
+       #:msg (format "Set-comprehension condition expected a formula: ~a" (deparse formula))
+       #:context formula)))
   (node/expr/comprehension info (length decls) decls formula))
 (define (set/func decls formula #:info [node-info empty-nodeinfo])
   (comprehension node-info decls formula))
@@ -806,14 +824,16 @@
                              (datum->syntax #f (deparse expr) (build-source-location-syntax loc)))) 
   (node/formula/multiplicity info mult expr))
 
-(define (no-pairwise-intersect vars)
-  (apply &&/func (no-pairwise-intersect-recursive-helper vars)))
+(define (no-pairwise-intersect vars #:context [context #f])
+  (apply &&/func (no-pairwise-intersect-recursive-helper vars #:context context)))
 
-(define (no-pairwise-intersect-recursive-helper vars)
-  (cond [(empty? vars) (raise-user-error "Cannot take pairwise intersection of empty list")]
+(define (no-pairwise-intersect-recursive-helper vars #:context [context #f])
+  (cond [(empty? vars) (raise-forge-error
+                        #:msg "Cannot take pairwise intersection of empty list"
+                        #:context context)]
         [(empty? (rest vars)) (list true)]
         [else (append (map (lambda (elt) (no (& (first vars) elt))) (rest vars))
-                      (no-pairwise-intersect-recursive-helper (rest vars)))]))
+                      (no-pairwise-intersect-recursive-helper (rest vars) #:context context))]))
 
 ;;; ALL ;;;
 
@@ -830,7 +850,10 @@
     ; quantifier case with disjointness flag; embed and repeat
     ; TODO: currently discarding the multiplicity info, unchecked
     [(_ info #:disj ([v0 e0 m0:opt-mult-class] ...) pred)
-     #'(all/info info ([v0 e0 m0] ...) (=> (no-pairwise-intersect (list v0 ...)) pred))]
+     (quasisyntax/loc stx
+       (all/info info ([v0 e0 m0] ...)
+                 #,(quasisyntax/loc stx
+                     (=> (no-pairwise-intersect (list v0 ...) #:context #,(build-source-location stx)) pred))))]
     [(_ info ([v0 e0 m0:opt-mult-class] ...) pred)     
      (quasisyntax/loc stx
        (let* ([v0 (node/expr/quantifier-var info (node/expr-arity e0) (gensym (format "~a_all" 'v0)) 'v0)] ...)
@@ -863,7 +886,11 @@
          (quantified-formula info 'some (list (cons v0 e0) ...) pred)))]
     ; quantifier case with disjointness flag; embed and repeat
     [(_ info #:disj ([v0 e0 m0:opt-mult-class] ...) pred)
-     #'(some/info info ([v0 e0 m0] ...) (&& (no-pairwise-intersect (list v0 ...)) pred))]
+     (quasisyntax/loc stx
+       (some/info info ([v0 e0 m0] ...)
+                  #,(quasisyntax/loc stx
+                      (&& (no-pairwise-intersect (list v0 ...)
+                                                 #:context #,(build-source-location stx)) pred))))]
     ; multiplicity case
     [(_ info expr)
      (quasisyntax/loc stx
@@ -923,7 +950,10 @@
      (quasisyntax/loc stx
        ; Kodkod doesn't have a "one" quantifier natively.
        ; Instead, desugar as a multiplicity of a set comprehension
-       (multiplicity-formula info 'one (set ([x1 r1] ...) (&& (no-pairwise-intersect (list x1 ...)) pred))))]
+       (multiplicity-formula info 'one
+                             (set ([x1 r1] ...)
+                                  #,(quasisyntax/loc stx (&& (no-pairwise-intersect (list x1 ...)
+                                                                                    #:context #,(build-source-location stx)) pred)))))]
     [(_ info ([x1 r1 m0:opt-mult-class] ...) pred)
      (quasisyntax/loc stx
        ; Kodkod doesn't have a "one" quantifier natively.
@@ -955,7 +985,10 @@
      (quasisyntax/loc stx
        ; Kodkod doesn't have a lone quantifier natively.
        ; Instead, desugar as a multiplicity of a set comprehension
-       (multiplicity-formula info 'lone (set ([x1 r1] ...) (&& (no-pairwise-intersect (list x1 ...)) pred))))]
+       (multiplicity-formula info 'lone (set ([x1 r1] ...)
+                                             #,(quasisyntax/loc stx
+                                                 (&& (no-pairwise-intersect (list x1 ...)
+                                                                            #:context #,(build-source-location stx)) pred)))))]
     [(_ info ([x1 r1 m0:opt-mult-class] ...) pred)
      (quasisyntax/loc stx
        ; Kodkod doesn't have a lone quantifier natively.
@@ -1045,8 +1078,8 @@
                              (equal? (procedure-arity vala) 0)
                              (equal? (procedure-arity valb) 0))
                          (equal-proc (vala) (valb))]
-                       [(and (or (node/expr? vala) (not (procedure? vala)))
-                             (or (node/expr? valb) (not (procedure? valb))))
+                       [(and (or (node/expr? vala) (node/formula? vala) (not (procedure? vala)))
+                             (or (node/expr? valb) (node/formula? vala) (not (procedure? valb))))
                          (equal-proc vala valb)]
                        [else (raise (format "Mismatched procedure fields when checking equality for ~a. Got: ~a and ~a"
                                             structname vala valb))]))                                              
@@ -1061,15 +1094,32 @@
                  [multiplier (drop multipliers offset)])
         ; Some AST fields may be thunkified
         ; Also, any node/expr is a procedure? since that's how we impl. box join
+        ; Also, in order to add better error messages for mis-used node/formulas,
+        ;   any node/formula is also a procedure?
         ; ASSUME: node/expr will never be an exactly-arity-0 procedure.
         (define vala (access a))
-        (cond                         
+        (cond
+          ; zero-arity procedure (a "thunk"): invoke it and then hash the result
           [(and (procedure? vala)                
                 (equal? (procedure-arity vala) 0))
-            (@* multiplier (hash-proc (vala)))]
-          [(or (node/expr? vala) 
-               (not (procedure? vala)))
-            (@* multiplier (hash-proc vala))]
+           ;(printf "field was zero arity procedure: ~a~n" vala)
+           (@* multiplier (hash-proc (vala)))]
+
+          ; node/expr? (but not a zero-arity procedure): just hash it
+          [(node/expr? vala)
+           ;(printf "field was expr: ~a~n" vala)
+           (@* multiplier (hash-proc vala))]
+
+          ; node/formula? (but not a zero-arity procedure): just hash it
+          [(node/formula? vala)
+           ;(printf "field was formula: ~a~n" vala)
+           (@* multiplier (hash-proc vala))]
+
+          ; not a procedure at all: just hash it
+          [(not (procedure? vala))
+           ;(printf "field was other non-procedure: ~a~n" vala)
+           (@* multiplier (hash-proc vala))]
+
           [else (raise (format "Non-thunk procedure field when hashing for ~a. Got: ~a"
                               structname vala))])))
     ;(printf "in mrnhs for ~a/~a: ~a, multiplied: ~a~n" structname offset a multiplied)    
@@ -1106,4 +1156,24 @@
 (make-breaker bij 'bij)
 (make-breaker pbij 'pbij)
 
-(make-breaker default 'default)
+(make-breaker default 'default)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; *** raise-forge-error ***
+;
+; Use this error-throwing function whenever possible in Forge.
+; 
+; Racket "user errors" avoid the (possibly confusing) stack trace that a Racket 
+; "syntax error" produces, but only DrRacket will highlight source location from
+; a user error. For the VSCode extension (and use from the terminal), produce a
+; custom user error that contains the row and column information of the offending
+; AST node.
+(define (pretty-loc loc)
+  (format "~a:~a:~a" (srcloc-source loc) (srcloc-line loc) (srcloc-column loc)))
+(define (raise-forge-error #:msg [msg "error"] #:context [context #f])
+  (define loc (cond [(nodeinfo? context) (pretty-loc (nodeinfo-loc context))]
+                    [(node? context) (pretty-loc (nodeinfo-loc (node-info context)))]
+                    [(srcloc? context) (pretty-loc context)] 
+                    [else "unknown:?:?"]))
+  (raise-user-error (format "[~a] ~a" loc msg)))
+

forge/lang/expander.rkt

@@ -7,12 +7,14 @@
          (for-syntax racket/base syntax/parse racket/syntax syntax/parse/define racket/function
                      syntax/srcloc racket/match racket/list                     
                      (only-in racket/path file-name-from-path))
+         syntax/srcloc
          ; Needed because the abstract-tok definition below requires phase 2
          (for-syntax (for-syntax racket/base)))
 
 (require (only-in racket empty? first))
 (require forge/sigs)
 (require forge/choose-lang-specific)
+(require (only-in forge/lang/ast raise-forge-error))
 
 (provide isSeqOf seqFirst seqLast indsOf idxOf lastIdxOf elems inds isEmpty hasDups reachable)
 (provide #%module-begin)
@@ -1025,7 +1027,7 @@
              (syntax-parameterize ([current-forge-context 'inst])
                (list #,@(syntax/loc stx bounds.translate))))))]))
 
-(define (disambiguate-block xs)
+(define (disambiguate-block xs #:stx [stx #f])
   (cond [(empty? xs) 
          ; {} always means the formula true
          true]
@@ -1034,20 +1036,24 @@
          (first xs)]
          ; Body of a predicate: any number of formulas
         [(andmap node/formula? xs)
-         (&& xs)]
+         (define info (nodeinfo (build-source-location stx) 'checklangplaceholder))
+         (&&/info info xs)]
          ; body of a helper function that produces an int-expression: one int-expression
         [(and (equal? 1 (length xs)) (node/int? (first xs)))
          (first xs)]         
-        [else 
-         (raise-user-error (format "~a" xs)
-                           (format "Ill-formed block: expected either one expression or any number of formulas"))]))
+        [else
+         (raise-forge-error
+          #:msg (format "Ill-formed block: expected either one expression or any number of formulas")
+          #:context stx)]))
 
 ; Block : /LEFT-CURLY-TOK Expr* /RIGHT-CURLY-TOK
 (define-syntax (Block stx)
   (syntax-parse stx
     [((~datum Block) exprs:ExprClass ...)
      (with-syntax ([(exprs ...) (syntax->list #'(exprs ...))])
-       (syntax/loc stx (disambiguate-block (list exprs ...))))]))
+       (quasisyntax/loc stx
+         (disambiguate-block (list exprs ...)
+                             #:stx #,(build-source-location stx))))]))
 
 (define-syntax (Expr stx)
   ;(printf "Debug: Expr: ~a~n" stx)

forge/run-tests.sh

@@ -16,7 +16,7 @@ raco setup forge
 
 # Get test files
 testDir=$1
-doNotTestPattern="error/[^/]*\\.frg"
+doNotTestPattern="[error|srcloc]/[^/]*\\.frg"
 # ^ these tests get checked by tests/error/main.rkt
 testFiles="$( find $testDir -type f \( -name "*.rkt" -o -name "*.frg" \) | grep --invert-match ${doNotTestPattern} )"
 numTestFiles="$(echo "$testFiles" | wc -l)"

forge/shared.rkt

@@ -162,4 +162,3 @@
           (set!-gc-time gc)
           (format "~a at ~a\tlast step: ~a\tgc: ~a\ttotal: ~a"
                   new-msg t diff gc-diff (- t initial-time)))))))
-

forge/sigs-structs.rkt

@@ -620,7 +620,7 @@ Returns whether the given run resulted in sat or unsat, respectively.
   (if (node/formula? b)
       (&&/info info
                (=>/info info a b)
-               (=>/info info (! a) c))
+               (=>/info info (!/info info a) c))
       (ite/info info a b c)))
 (define-syntax (ifte stx)
   (syntax-parse stx 

forge/sigs.rkt

@@ -840,16 +840,16 @@
 
 (define-builtin (isSeqOf info r1 d)
   (&&/info info
-      (in/info info r1 (-> Int univ))
+      (in/info info r1 (->/info info Int univ))
       (in/info info (join/info info Int r1) d)
-      (all ([i1 (join/info info r1 univ)])
+      (all/info info ([i1 (join/info info r1 univ)])
            (&&/info info (int>= (sum/info info i1) (int 0))
-               (lone (join/info info i1 r1))))
-      (all ([e (join/info info Int r1)])
-           (some (join/info info r1 e)))
-      (all ([i1 (join/info info r1 univ)])
-           (implies (!= i1 (sing/info info (int 0)))
-                    (some (join/info info
+               (lone/info info (join/info info i1 r1))))
+      (all/info info ([e (join/info info Int r1)])
+           (some/info info (join/info info r1 e)))
+      (all/info info ([i1 (join/info info r1 univ)])
+           (=>/info info (!= i1 (sing/info info (int 0)))
+                    (some/info info (join/info info
                      (sing/info info
                       (subtract/info info
                        (sum/info info i1) (int 1))) r1))))))

forge/tests/error/expect-predicate-args.frg

@@ -0,0 +1,14 @@
+#lang forge/bsl
+option verbose 0 
+option run_sterling off
+abstract sig Player {}
+one sig X, O extends Player {}
+sig Board {board: pfunc Int -> Int -> Player}
+
+pred wellformed[b: Board] {
+  all row, col: Int | {
+    (row < 0 or row > 2 or col < 0 or col > 2) 
+      implies no b.board[row][col] }}
+
+test expect { should_error: { wellformed } is sat }
+

forge/tests/error/expect-predicate-no-args.frg

@@ -0,0 +1,14 @@
+#lang forge/bsl
+option verbose 0 
+option run_sterling off
+abstract sig Player {}
+one sig X, O extends Player {}
+sig Board {board: pfunc Int -> Int -> Player}
+
+pred wellformed {
+  all b: Board | all row, col: Int | {
+    (row < 0 or row > 2 or col < 0 or col > 2) 
+      implies no b.board[row][col] }}
+
+test expect { should_error: { all b: Board | wellformed[b] } is sat }
+

forge/tests/error/main.rkt

@@ -108,6 +108,8 @@
     (list "expr-in-comprehension-condition.frg" #rx"expected a formula")
     (list "non-expr-in-comprehension-domain.frg" #rx"expected a singleton or relational expression")
     (list "arity-in-comprehension-domain.frg" #rx"variable domain needs arity = 1")
+    (list "expect-predicate-args.frg" #rx"Ill-formed block")
+    (list "expect-predicate-no-args.frg" #rx"Tried to give arguments to a predicate, but it takes none") 
   ))
 
 

forge/tests/forge-core/formulas/disj-one-core.rkt

@@ -1,7 +1,6 @@
 #lang forge/core
 
 (set-option! 'verbose 0)
-;(set-option! 'verbose 10)
 
 (sig onede)
 (relation edges (onede onede))