diff --git a/forge/breaks.rkt b/forge/breaks.rkt
index 137efdca4..9a666ec86 100644
--- a/forge/breaks.rkt
+++ b/forge/breaks.rkt
@@ -652,11 +652,18 @@
(define (funcformula rllst quantvarlst)
(cond
- [(empty? (rest (rest rllst)))
- (let ([a (gensym)])
- (@all/info (@just-location-info loc) ([a (first rllst)]) (@one (funcformulajoin (cons a quantvarlst)))))]
- [else (let ([a (gensym)])
- (@all/info (@just-location-info loc) ([a (first rllst)]) (funcformula (rest rllst) (cons a quantvarlst))))]))
+ [(empty? (rest (rest rllst)))
+ (let* ([var-id (gensym 'pfunc)]
+ [a (@node/expr/quantifier-var (@just-location-info loc) 1 var-id var-id)])
+ (@quantified-formula (@just-location-info loc) 'all
+ (list (cons a (first rllst)))
+ (@one (funcformulajoin (cons a quantvarlst)))))]
+ [else
+ (let* ([var-id (gensym 'pfunc)]
+ [a (@node/expr/quantifier-var (@just-location-info loc) 1 var-id var-id)])
+ (@quantified-formula (@just-location-info loc) 'all
+ (list (cons a (first rllst)))
+ (funcformula (rest rllst) (cons a quantvarlst))))]))
(define formulas (set (funcformula rel-list (list))))
; OLD CODE
@@ -716,22 +723,31 @@
(λ () (break bound formulas)))
))
-(add-strategy 'pfunc (λ (pri rel bound atom-lists rel-list [loc #f])
-
- (define (pfuncformulajoin quantvarlst)
- (cond
- [(empty? (rest quantvarlst)) (@join (first quantvarlst) rel)]
- [else (@join (first quantvarlst) (pfuncformulajoin (rest quantvarlst)))]))
- (define (pfuncformula rllst quantvarlst)
- (cond
- [(empty? (rest (rest rllst)))
- (let ([a (gensym)])
- (@all/info (@just-location-info loc) ([a (first rllst)]) (@lone (pfuncformulajoin (cons a quantvarlst)))))]
- [else (let ([a (gensym)])
- (@all/info (@just-location-info loc) ([a (first rllst)]) (pfuncformula (rest rllst) (cons a quantvarlst))))]))
-
- (define formulas (set (pfuncformula rel-list (list))))
+(add-strategy 'pfunc
+ (λ (pri rel bound atom-lists rel-list [loc #f])
+ (define (pfuncformulajoin quantvarlst)
+ (cond
+ ; x_n.rel
+ [(empty? (rest quantvarlst)) (@join (first quantvarlst) rel)]
+ ; ... x_n-1.x_n.rel
+ [else (@join (first quantvarlst) (pfuncformulajoin (rest quantvarlst)))]))
+ (define (pfuncformula rllst quantvarlst)
+ (cond
+ [(empty? (rest (rest rllst)))
+ (let* ([var-id (gensym 'pfunc)]
+ [a (@node/expr/quantifier-var (@just-location-info loc) 1 var-id var-id)])
+ (@quantified-formula (@just-location-info loc) 'all
+ (list (cons a (first rllst)))
+ (@lone (pfuncformulajoin (cons a quantvarlst)))))]
+ [else (let* ([var-id (gensym 'pfunc)]
+ [a (@node/expr/quantifier-var (@just-location-info loc) 1 var-id var-id)])
+ (@quantified-formula (@just-location-info loc) 'all
+ (list (cons a (first rllst)))
+ (pfuncformula (rest rllst) (cons a quantvarlst))))]))
+ (define pf-fmla (pfuncformula rel-list (list)))
+ (define formulas (set pf-fmla))
+
; OLD CODE
; (if (equal? A B)
; (formula-breaker pri ; TODO: can improve, but need better symmetry-breaking predicates
diff --git a/forge/lang/alloy-syntax/lexer.rkt b/forge/lang/alloy-syntax/lexer.rkt
index bad95ce24..242538698 100644
--- a/forge/lang/alloy-syntax/lexer.rkt
+++ b/forge/lang/alloy-syntax/lexer.rkt
@@ -108,7 +108,8 @@
["some" (token+ `SOME-TOK "" lexeme "" lexeme-start lexeme-end)]
["sum" (token+ `SUM-TOK "" lexeme "" lexeme-start lexeme-end #f #t)]
["test" (token+ `TEST-TOK "" lexeme "" lexeme-start lexeme-end)]
- ["theorem" (token+ `THEOREM-TOK "" lexeme "" lexeme-start lexeme-end)]
+ ["theorem" (token+ `THEOREM-TOK "" lexeme "" lexeme-start lexeme-end)]
+ ["forge_error" (token+ `FORGE_ERROR-TOK "" lexeme "" lexeme-start lexeme-end)]
["two" (token+ `TWO-TOK "" lexeme "" lexeme-start lexeme-end)]
["univ" (token+ `UNIV-TOK "" lexeme "" lexeme-start lexeme-end)]
["unsat" (token+ `UNSAT-TOK "" lexeme "" lexeme-start lexeme-end)]
diff --git a/forge/lang/alloy-syntax/parser.rkt b/forge/lang/alloy-syntax/parser.rkt
index 4e90e6f4d..6485e5cbf 100644
--- a/forge/lang/alloy-syntax/parser.rkt
+++ b/forge/lang/alloy-syntax/parser.rkt
@@ -85,7 +85,8 @@ ParaDecls : /LEFT-PAREN-TOK @ParaDeclList? /RIGHT-PAREN-TOK
AssertDecl : /ASSERT-TOK Name? Block
CmdDecl : (Name /COLON-TOK)? (RUN-TOK | CHECK-TOK) (QualName | Block)? Scope? (/FOR-TOK Bounds)?
-TestDecl : (Name /COLON-TOK)? (QualName | Block)? Scope? (/FOR-TOK Bounds)? /IS-TOK (SAT-TOK | UNSAT-TOK | THEOREM-TOK)
+TestDecl : (Name /COLON-TOK)? (QualName | Block) Scope? (/FOR-TOK Bounds)? /IS-TOK
+ (SAT-TOK | UNSAT-TOK | THEOREM-TOK | FORGE_ERROR-TOK)
TestExpectDecl : TEST-TOK? EXPECT-TOK Name? TestBlock
TestBlock : /LEFT-CURLY-TOK TestDecl* /RIGHT-CURLY-TOK
Scope : /FOR-TOK Number (/BUT-TOK @TypescopeList)?
diff --git a/forge/lang/ast.rkt b/forge/lang/ast.rkt
index a1afa0f26..7d1d73ceb 100644
--- a/forge/lang/ast.rkt
+++ b/forge/lang/ast.rkt
@@ -5,7 +5,7 @@
racket/contract
racket/match
forge/shared ; for verbosity level
- (only-in racket false? empty? first second rest drop const thunk)
+ (only-in racket false? empty? first second rest drop const thunk range remove-duplicates)
(prefix-in @ (only-in racket + - * < > or <=)))
(provide deparse
@@ -91,7 +91,7 @@
#:context f)]
[else
(raise-forge-error
- #:msg (format "Could not use formula as a function: ~a." (deparse f))
+ #:msg (format "Could not use a boolean-valued formula as a predicate, function, or field name: ~a." (deparse f))
#:context f)])))
@@ -103,67 +103,102 @@
[(integer? a-node) (intexpr->expr/maybe (int a-node) #:op functionname #:info info)]
[(node/expr? a-node) a-node]
[else
- (define loc (nodeinfo-loc info))
- (define locstr (format "line ~a, col ~a, span: ~a" (source-location-line loc) (source-location-column loc) (source-location-span loc)))
- (raise-syntax-error functionname
- (format "~a operator expected to be given an expression, but instead got ~a at loc: ~a" functionname (node-type a-node) locstr)
- (datum->syntax #f (deparse a-node) (build-source-location-syntax loc)))]))
+ (raise-forge-error
+ #:msg (format "~a operator expected to be given an atom- or set-valued expression, but instead got ~a, which was ~a."
+ functionname (deparse a-node) (pretty-type-of a-node))
+ #:context a-node)]))
(define/contract (expr->intexpr/maybe a-node #:op functionname #:info info)
(@-> node? #:op symbol? #:info nodeinfo? node/int?)
- (cond [(node/expr? a-node) (node/int/op/sum (node-info a-node) (list a-node))]
+ (cond [(and (node/expr? a-node)
+ (equal? (node/expr-arity a-node) 1))
+ ; If arity 1, this node/expr can be converted automatically to a node/int
+ (node/int/op/sum (node-info a-node) (list a-node))]
+ [(node/expr? a-node)
+ ; Otherwise, this node/expr has the wrong arity for auto-conversion to a node/int
+ (raise-forge-error
+ #:msg (format "Could not treat ~a as an integer expression. Expected arity 1, got arity ~a"
+ (deparse a-node) (node/expr-arity a-node))
+ #:context a-node)]
[(node/int? a-node) a-node]
[(integer? a-node) (int a-node)]
[else
- (define loc (nodeinfo-loc info))
- (define locstr (format "line ~a, col ~a, span: ~a" (source-location-line loc) (source-location-column loc) (source-location-span loc)))
- (raise-syntax-error functionname
- (format "~a operator expected an expression, but instead got ~a at loc: ~a" functionname (node-type a-node) locstr)
- (datum->syntax #f (deparse a-node) (build-source-location-syntax loc)))]))
-
+ (raise-forge-error
+ #:msg (format "~a operator expected an expression, but instead got ~a, which was ~a"
+ functionname (deparse a-node) (pretty-type-of a-node))
+ #:context a-node)]))
+
+(define (pretty-name-predicate p)
+ (cond [(equal? p node/expr?) "atom- or set-valued expression"]
+ [(equal? p node/formula?) "boolean-valued formula"]
+ [(equal? p node/int?) "integer-valued expression"]
+ [else p]))
+(define (pretty-type-of x)
+ (cond [(node/formula? x) "boolean-valued formula"]
+ [(node/expr? x) "atom- or set-valued expression"]
+ [(node/int? x) "integer-valued expression"]
+ [(number? x) "number"]
+ [else "unknown expression type"]))
+
+; Check arguments to an operator declared with define-node-op
(define (check-args info op args type?
#:same-arity? [same-arity? #f] #:arity [arity #f]
#:min-length [min-length 2] #:max-length [max-length #f]
#:join? [join? #f] #:domain? [domain? #f] #:range? [range? #f])
(define loc (nodeinfo-loc info))
- (define locstr (format "line ~a, col ~a, span: ~a" (source-location-line loc) (source-location-column loc) (source-location-span loc)))
-
+
+ ; check: correct number of arguments
(when (< (length args) min-length)
- (raise-syntax-error op (format "building ~a; not enough arguments: required ~a got ~a at loc: ~a"
- op min-length args locstr)
- (datum->syntax #f (map deparse args) (build-source-location-syntax loc))))
+ (raise-forge-error
+ #:msg (format "building ~a; not enough arguments: required ~a got ~a."
+ op min-length args)
+ #:context loc))
(unless (false? max-length)
(when (> (length args) max-length)
- (raise-syntax-error op (format "too many arguments to ~a; maximum ~a, got ~a at loc: ~a" op max-length args locstr)
- (datum->syntax #f (map deparse args) (build-source-location-syntax loc)))))
- (for ([a (in-list args)])
+ (raise-forge-error
+ #:msg (format "too many arguments to ~a; maximum ~a, got ~a." op max-length args)
+ #:context loc)))
+
+ (for ([a (in-list args)]
+ [idx (map add1 (range (length args)))])
+ ; check: type of argument
(unless (type? a)
- (raise-syntax-error op (format "argument to ~a had unexpected type. expected ~a, got ~a. loc: ~a" op type? a locstr)
- (datum->syntax #f (map deparse args) (build-source-location-syntax loc))))
+ (raise-forge-error
+ #:msg (format "argument ~a of ~a to ~a had unexpected type. Expected ~a, got ~a, which was ~a."
+ idx (length args) op (pretty-name-predicate type?) (deparse a) (pretty-type-of a))
+ #:context loc))
+ ; check: arity of argument
(unless (false? arity)
(unless (equal? (node/expr-arity a) arity)
- (raise-syntax-error op (format "argument to ~a was not expression with arity ~v (got: ~a) at loc: ~a" op arity a locstr)
- (datum->syntax #f (map deparse args) (build-source-location-syntax loc))))))
+ (raise-forge-error
+ #:msg (format "argument ~a of ~a to ~a was not expression with arity ~v (got: ~a)"
+ idx (length args) op arity (deparse a))
+ #:context loc))))
+
(when same-arity?
(let ([arity (node/expr-arity (car args))])
(for ([a (in-list args)])
(unless (equal? (node/expr-arity a) arity)
- (raise-syntax-error op (format "arguments to ~a must have same arity. got ~a and ~a at loc: ~a"
- op arity (node/expr-arity a) locstr)
- (datum->syntax #f (map deparse args) (build-source-location-syntax loc)))))))
+ (raise-forge-error
+ #:msg (format "arguments to ~a must have same arity. got ~a and ~a"
+ op arity (node/expr-arity a))
+ #:context loc)))))
(when join?
(when (<= (apply join-arity (for/list ([a (in-list args)]) (node/expr-arity a))) 0)
- (raise-syntax-error op (format "join would create a relation of arity 0 at loc: ~a" locstr)
- (datum->syntax #f (map deparse args) (build-source-location-syntax loc)))))
+ (raise-forge-error
+ #:msg (format "join would create a relation of arity 0")
+ #:context loc)))
(when range?
(unless (equal? (node/expr-arity (cadr args)) 1)
- (raise-syntax-error op (format "second argument to ~a must have arity 1 at loc: ~a" op locstr)
- (datum->syntax #f (map deparse args) (build-source-location-syntax loc)))))
+ (raise-forge-error
+ #:msg (format "second argument to ~a must have arity 1" op)
+ #:context loc)))
(when domain?
(unless (equal? (node/expr-arity (car args)) 1)
- (raise-syntax-error op (format "first argument to ~a must have arity 1 at loc: ~a" op locstr)
- (datum->syntax #f (map deparse args) (build-source-location-syntax loc))))))
+ (raise-forge-error
+ #:msg (format "first argument to ~a must have arity 1" op)
+ #:context loc))))
;; EXPRESSIONS -----------------------------------------------------------------
@@ -244,17 +279,17 @@
(define c (intexpr->expr/maybe orig-c #:op 'if-then-else #:info info))
(unless (node/formula? a)
- (raise-syntax-error #f (format "If-then-else expression requires first argument to be a formula")
- (datum->syntax #f (deparse a) (build-source-location-syntax (nodeinfo-loc info)))))
+ (raise-forge-error #:msg (format "If-then-else expression requires first argument to be a formula")
+ #:context (nodeinfo-loc info)))
(unless (node/expr? b)
- (raise-syntax-error #f (format "If-then-else expression requires second argument to be an expression")
- (datum->syntax #f (deparse b) (build-source-location-syntax (nodeinfo-loc info)))))
+ (raise-forge-error #:msg (format "If-then-else expression requires second argument to be an expression")
+ #:context (nodeinfo-loc info)))
(unless (node/expr? c)
- (raise-syntax-error #f (format "If-then-else expression requires third argument to be an expression")
- (datum->syntax #f (deparse c) (build-source-location-syntax (nodeinfo-loc info)))))
+ (raise-forge-error #:msg (format "If-then-else expression requires third argument to be an expression")
+ #:context (nodeinfo-loc info)))
(unless (equal? (node/expr-arity b) (node/expr-arity c))
- (raise-syntax-error #f (format "If-then-else expression requires expression arguments to have same arity")
- (datum->syntax #f (deparse c) (build-source-location-syntax (nodeinfo-loc info)))))
+ (raise-forge-error #:msg (format "If-then-else expression requires expression arguments to have same arity")
+ #:context (nodeinfo-loc info)))
(node/expr/ite info (node/expr-arity b) a b c))
(define-syntax (ite/info stx)
@@ -465,9 +500,17 @@
; these are shown to an end-user)
(define (raise-set-comp-quantifier-error e)
(raise-forge-error
- #:msg (format "Set-comprehension variable domain expected a singleton or relational expression: ~a" (deparse e))
+ #:msg (format "Set-comprehension variable domain expected a singleton or relational expression of arity 1: ~a" (deparse e))
#:context e))
+
(define (comprehension info decls formula)
+ ; Check for re-use of a variable within the same quantifier/comprehension/sum form
+ (define vars (map car decls))
+ (unless (equal? (length (remove-duplicates vars)) (length vars))
+ (raise-forge-error
+ #:msg (format "Set-comprehension cannot use the same variable name more than once; used: ~a." vars)
+ #:context info))
+
(for ([e (map cdr decls)])
(unless (node/expr? e)
(raise-set-comp-quantifier-error e))
@@ -496,12 +539,18 @@
([r0 e0 m0:opt-mult-class] ...)
pred)
(quasisyntax/loc stx
- (begin
+ (let* ([r0 (node/expr/quantifier-var
+ (nodeinfo #,(build-source-location stx) check-lang.check-lang)
+ 1 (gensym (format "~a_set" 'r0)) 'r0)] ... )
+ ; We need to check these only inside the let*, to allow for later decls to use earlier ones.
(unless (node/expr? e0)
(raise-set-comp-quantifier-error e0))
...
- (let* ([r0 (node/expr/quantifier-var (nodeinfo #,(build-source-location stx) check-lang.check-lang) (node/expr-arity e0) (gensym (format "~a_set" 'r0)) 'r0)] ... )
- (set/func #:info (nodeinfo #,(build-source-location stx) check-lang.check-lang) (list (cons r0 e0) ...) pred))))]))
+ (unless (equal? 1 (node/expr-arity e0))
+ (raise-set-comp-quantifier-error e0))
+ ...
+ (set/func #:info (nodeinfo #,(build-source-location stx) check-lang.check-lang)
+ (list (cons r0 e0) ...) pred)))]))
;; -- relations ----------------------------------------------------------------
@@ -605,11 +654,8 @@
[val (identifier? (syntax val)) (quasisyntax/loc stx (node/expr/constant (nodeinfo #,(build-source-location stx) 'checklangplaceholder) 1 'univ))])))
(define-syntax iden (lambda (stx) (syntax-case stx ()
[val (identifier? (syntax val)) (quasisyntax/loc stx (node/expr/constant (nodeinfo #,(build-source-location stx) 'checklangplaceholder) 2 'iden))])))
-; relations, not constants
-; (define-syntax Int (lambda (stx) (syntax-case stx ()
-; [val (identifier? (syntax val)) (quasisyntax/loc stx (node/expr/relation (nodeinfo #,(build-source-location stx)) 1 "Int" '(Int) "univ" #f))])))
-; (define-syntax succ (lambda (stx) (syntax-case stx ()
-; [val (identifier? (syntax val)) (quasisyntax/loc stx (node/expr/relation (nodeinfo #,(build-source-location stx)) 2 "succ" '(Int Int) "Int" #f))])))
+
+; Int and succ are built-in relations, not constant expressions
;; INTS ------------------------------------------------------------------------
@@ -625,15 +671,16 @@
(define-node-op divide node/int/op #f #:min-length 2 #:type node/int?)
; id, parent, arity, checks
-; card and sum both accept a single node/expr as their argument
+; card and sum both accept a single node/expr as their argument.
(define-node-op card node/int/op #f #:min-length 1 #:max-length 1 #:type node/expr?)
-(define-node-op sum node/int/op #f #:min-length 1 #:max-length 1 #:type node/expr?)
+; sum must have an argument *of arity 1*; it is used to convert node/expr to node/int.
+(define-node-op sum node/int/op #f #:min-length 1 #:max-length 1 #:arity 1 #:type node/expr?)
(define-node-op remainder node/int/op #f #:min-length 2 #:max-length 2 #:type node/int?)
(define-node-op abs node/int/op #f #:min-length 1 #:max-length 1 #:type node/int?)
(define-node-op sign node/int/op #f #:min-length 1 #:max-length 1 #:type node/int?)
-; min and max are now *defined*, not declared, and in sigs-structs.rkt:
+; min and max are now *defined*, not declared, in sigs-structs.rkt.
;; -- constants ----------------------------------------------------------------
@@ -670,17 +717,26 @@
(define hash2-proc (make-robust-node-hash-syntax node/int/sum-quant 3))])
(define (sum-quant/func decls raw-int-expr #:info [node-info empty-nodeinfo])
+ (when (@> (length decls) 1)
+ (raise-forge-error
+ #:msg (format "sum aggregator only supports a single variable; if you wish to sum over multiple domains, please use nested sum aggregators.")
+ #:context node-info))
(for ([e (map cdr decls)])
(unless (node/expr? e)
- (raise-argument-error 'set "expr?" e))
+ (raise-forge-error
+ #:msg (format "sum aggregator expected an expression in its declaration, given ~a" e)
+ #:context e))
(unless (equal? (node/expr-arity e) 1)
- (raise-argument-error 'set "decl of arity 1" e)))
+ (raise-forge-error
+ #:msg (format "sum aggregator expected its declaration expression to have arity 1, given ~a" e)
+ #:context e)))
(define int-expr (cond [(node/expr? raw-int-expr)
(expr->intexpr/maybe raw-int-expr #:op 'sum #:info node-info)]
[else
raw-int-expr]))
(unless (node/int? int-expr)
- (raise-argument-error 'set "int-expr?" int-expr))
+ (raise-forge-error #:msg "sum aggregator body expected an integer expression, got ~a" int-expr
+ #:context int-expr))
(node/int/sum-quant node-info decls int-expr))
(define (sum-quant-expr info decls int-expr)
@@ -788,13 +844,23 @@
(define hash2-proc (make-robust-node-hash-syntax node/formula/quantified 3))])
(define (quantified-formula info quantifier decls formula)
+ ; Check for re-use of a variable within the same quantifier/comprehension/sum form
+ (define vars (map car decls))
+ (unless (equal? (length (remove-duplicates vars)) (length vars))
+ (raise-forge-error
+ #:msg (format "~a quantifier cannot use the same variable name more than once; used: ~a." quantifier vars)
+ #:context info))
+
(for ([e (in-list (map cdr decls))])
(unless (node/expr? e)
- (raise-argument-error quantifier "expr?" e))
- #'(unless (equal? (node/expr-arity e) 1)
- (raise-argument-error quantifier "decl of arity 1" e)))
+ (raise-forge-error #:msg (format "~a quantifier expected an expression for domain, got ~a" quantifier e)
+ #:context (if (node? e) e info)))
+ (unless (equal? (node/expr-arity e) 1)
+ (raise-forge-error #:msg (format "~a quantifier expected an arity-1 expression for domain, got ~a" quantifier e)
+ #:context (if (node? e) e info))))
(unless (or (node/formula? formula) (equal? #t formula))
- (raise-argument-error quantifier "formula?" formula))
+ (raise-forge-error #:msg (format "~a quantifier body expected a formula, got ~a" quantifier formula)
+ #:context (if (node? formula) formula info)))
(node/formula/quantified info quantifier decls formula))
;(struct node/formula/higher-quantified node/formula (quantifier decls formula))
@@ -811,18 +877,14 @@
(define hash-proc (make-robust-node-hash-syntax node/formula/multiplicity 0))
(define hash2-proc (make-robust-node-hash-syntax node/formula/multiplicity 3))])
-(define (node-type n)
- (cond [(node/expr? n) "expression"]
- [(node/int? n) "integer expression"]
- [(node/formula? n) "formula"]
- [else "unknown type"]))
-
(define (multiplicity-formula info mult expr)
(unless (node/expr? expr)
(define loc (nodeinfo-loc info))
(define locstr (format "line ~a, col ~a, span: ~a" (source-location-line loc) (source-location-column loc) (source-location-span loc)))
- (raise-syntax-error mult (format "~a operator expected to be given an expression, but instead got ~a at loc: ~a" mult (node-type expr) locstr)
- (datum->syntax #f (deparse expr) (build-source-location-syntax loc))))
+ (raise-forge-error
+ #:msg (format "~a operator expected to be given an atom- or set-valued expression, but instead got ~a"
+ mult (pretty-type-of expr))
+ #:context loc))
(node/formula/multiplicity info mult expr))
(define (no-pairwise-intersect vars #:context [context #f])
@@ -855,9 +917,11 @@
(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)
+ [(_ 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)] ...)
+ (let* ([v0 (node/expr/quantifier-var info
+ (if (node/expr? e0) (node/expr-arity e0) 1)
+ (gensym (format "~a_all" 'v0)) 'v0)] ...)
(quantified-formula info 'all (list (cons v0 e0) ...) pred)))]))
;;; SOME ;;;
@@ -883,7 +947,9 @@
; TODO: currently discarding the multiplicity info, unchecked (in this and the following cases)
[(_ 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_some" 'v0)) 'v0)] ...)
+ (let* ([v0 (node/expr/quantifier-var info
+ (if (node/expr? e0) (node/expr-arity e0) 1)
+ (gensym (format "~a_some" 'v0)) 'v0)] ...)
(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)
@@ -922,7 +988,9 @@
; quantifier without disj: rewrite as !some
[(_ 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_no" 'v0)) 'v0)] ...)
+ (let* ([v0 (node/expr/quantifier-var info
+ (if (node/expr? e0) (node/expr-arity e0) 1)
+ (gensym (format "~a_no" 'v0)) 'v0)] ...)
(! (quantified-formula info 'some (list (cons v0 e0) ...) pred))))]
[(_ info expr)
(quasisyntax/loc stx
@@ -1007,7 +1075,9 @@
(syntax-parse stx
[(_ (~optional (#:lang check-lang) #:defaults ([check-lang #''checklangNoCheck])) ([x1 r1 m0:opt-mult-class] ...) int-expr)
(quasisyntax/loc stx
- (let* ([x1 (node/expr/quantifier-var (nodeinfo #,(build-source-location stx) check-lang) (node/expr-arity r1) (gensym (format "~a_sum" 'x1)) 'x1)] ...)
+ (let* ([x1 (node/expr/quantifier-var (nodeinfo #,(build-source-location stx) check-lang)
+ (if (node/expr? r1) (node/expr-arity r1) 1)
+ (gensym (format "~a_sum" 'x1)) 'x1)] ...)
(sum-quant-expr (nodeinfo #,(build-source-location stx) check-lang) (list (cons x1 r1) ...) int-expr)))]))
@@ -1173,7 +1243,7 @@
(define (pretty-loc loc)
(format "~a:~a:~a (span ~a)" (srcloc-source loc) (srcloc-line loc) (srcloc-column loc) (srcloc-span loc)))
-(define (raise-forge-error #:msg [msg "error"] #:context [context #f] #:raise? [raise? #t])
+(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
diff --git a/forge/lang/expander.rkt b/forge/lang/expander.rkt
index 2ff4aa00d..b43d45018 100644
--- a/forge/lang/expander.rkt
+++ b/forge/lang/expander.rkt
@@ -54,7 +54,7 @@
(define-for-syntax (my-expand stx)
(define core-funcs-and-macros
- (map (curry datum->syntax stx)
+ (map (lambda (s) (datum->syntax stx s stx))
'(^ * ~ + - & join
-> => implies ! not and or && || ifte iff <=>
= in ni != !in !ni is
@@ -159,38 +159,39 @@
(pattern ((~datum SigExt)
"extends"
name:QualNameClass)
- #:attr symbol #'#:extends
- #:attr value #'name.name)
+ #:attr symbol (syntax/loc this-syntax #:extends)
+ #:attr value (syntax/loc this-syntax name.name))
(pattern ((~datum SigExt)
"in"
name:QualNameClass
(~seq (~seq "+" names:QualNameClass) ...))
- #:attr symbol #'#:in
- #:attr value #'(raise "Extending with in not yet implemented.")))
+ #:attr symbol (syntax/loc this-syntax #:in)
+ #:attr value (syntax/loc this-syntax (raise "Extending with in not yet implemented."))))
; Mult : LONE-TOK | SOME-TOK | ONE-TOK | TWO-TOK
(define-syntax-class MultClass
- (pattern ((~datum Mult) "lone") #:attr symbol #'#:lone)
- (pattern ((~datum Mult) "some") #:attr symbol #'#:some)
- (pattern ((~datum Mult) "one") #:attr symbol #'#:one)
- (pattern ((~datum Mult) "two") #:attr symbol #'#:two))
+ (pattern ((~datum Mult) "lone") #:attr symbol (syntax/loc this-syntax #:lone))
+ (pattern ((~datum Mult) "some") #:attr symbol (syntax/loc this-syntax #:some))
+ (pattern ((~datum Mult) "one") #:attr symbol (syntax/loc this-syntax #:one))
+ (pattern ((~datum Mult) "two") #:attr symbol (syntax/loc this-syntax #:two)))
; ArrowMult : used for field etc. declarations; the symbol attribute references a breaker
(define-syntax-class ArrowMultClass
- (pattern ((~datum ArrowMult) "lone") #:attr symbol #'pfunc)
- (pattern ((~datum ArrowMult) "set") #:attr symbol #'default)
- (pattern ((~datum ArrowMult) "one") #:attr symbol #'func)
- (pattern ((~datum ArrowMult) "func") #:attr symbol #'func)
- (pattern ((~datum ArrowMult) "pfunc") #:attr symbol #'pfunc)
- (pattern ((~datum ArrowMult) "two") #:attr symbol #'(raise "relation arity two not implemented")))
+ (pattern ((~datum ArrowMult) "lone") #:attr symbol (syntax/loc this-syntax pfunc))
+ (pattern ((~datum ArrowMult) "set") #:attr symbol (syntax/loc this-syntax default))
+ (pattern ((~datum ArrowMult) "one") #:attr symbol (syntax/loc this-syntax func))
+ (pattern ((~datum ArrowMult) "func") #:attr symbol (syntax/loc this-syntax func))
+ (pattern ((~datum ArrowMult) "pfunc") #:attr symbol (syntax/loc this-syntax pfunc))
+ (pattern ((~datum ArrowMult) "two") #:attr symbol (syntax/loc this-syntax
+ (raise "relation arity two not implemented"))))
; HelperMult : used for helper fun/pred definitions; the symbol attribute references a symbol
(define-syntax-class HelperMultClass
- (pattern ((~datum HelperMult) "lone") #:attr symbol #'(quote lone))
- (pattern ((~datum HelperMult) "set") #:attr symbol #'(quote set))
- (pattern ((~datum HelperMult) "one") #:attr symbol #'(quote one))
- (pattern ((~datum HelperMult) "func") #:attr symbol #'(quote func))
- (pattern ((~datum HelperMult) "pfunc") #:attr symbol #'(quote pfunc)))
+ (pattern ((~datum HelperMult) "lone") #:attr symbol (syntax/loc this-syntax (quote lone)))
+ (pattern ((~datum HelperMult) "set") #:attr symbol (syntax/loc this-syntax (quote set)))
+ (pattern ((~datum HelperMult) "one") #:attr symbol (syntax/loc this-syntax (quote one)))
+ (pattern ((~datum HelperMult) "func") #:attr symbol (syntax/loc this-syntax (quote func)))
+ (pattern ((~datum HelperMult) "pfunc") #:attr symbol (syntax/loc this-syntax (quote pfunc))))
; Declaration of variables with shared expr, shared optional multiplicity
@@ -208,8 +209,8 @@
#'(if (> (node/expr-arity expr) 1)
'set
'one))])
- #'((names-c.names expr mult) ...))
- #:attr names #'(names-c.names ...)))
+ (syntax/loc this-syntax ((names-c.names expr mult) ...)))
+ #:attr names (syntax/loc this-syntax (names-c.names ...))))
; Declaration of a comma-delimited list of variable declarations with expr and optional multiplicity
; DeclList : Decl
@@ -333,7 +334,7 @@
pred-block:BlockClass))
(~optional scope:ScopeClass)
(~optional bounds:BoundsClass)
- (~or "sat" "unsat" "theorem"))))
+ (~or "sat" "unsat" "theorem" "forge_error"))))
; TestBlock : /LEFT-CURLY-TOK TestDecl* /RIGHT-CURLY-TOK
(define-syntax-class TestBlockClass
@@ -530,7 +531,8 @@
(~optional "exactly")
name:QualNameClass)
#:attr translate (begin (datum->syntax #'name
- (list #'name.name)))))
+ (list #'name.name)
+ #'name))))
(define-syntax-class QualNameOrAtomOrAtomizedNumberClass
#:description "name, atom name, or number"
@@ -684,7 +686,9 @@
(~and op
(~or "in" "=" "<" ">" "<=" ">="
"is" "ni")))
- #:attr symbol (datum->syntax #'op (op-symbol-to-operator (string->symbol (syntax->datum #'op))))))
+ #:attr symbol (datum->syntax #'op
+ (op-symbol-to-operator (string->symbol (syntax->datum #'op)))
+ #'op)))
; We don't overload (e.g.) <, but we don't want users to need to write (e.g.) "int<".
(define (op-symbol-to-operator sym)
@@ -722,7 +726,8 @@
(pattern ((~datum Quant) (~and q (~or "all" "no" "lone"
"some" "one" "two")))
#:attr symbol (datum->syntax #'q
- (string->symbol (syntax->datum #'q))))
+ (string->symbol (syntax->datum #'q))
+ #'q))
(pattern ((~datum Quant) (~literal sum))
#:attr symbol (syntax/loc #'q sum-quant)))
@@ -831,7 +836,8 @@
(with-syntax ([relation-name relation-name-p1]
[relation-types (datum->syntax relation-types
(cons sig-name ;(syntax->datum sig-name)
- (syntax->list relation-types)))]
+ (syntax->list relation-types))
+ relation-types)]
[relation-mult relation-mult]
[is-var relation-is-var])
(syntax/loc relation-name-p1 (relation (#:lang (get-check-lang)) relation-name relation-types #:is relation-mult #:is-var is-var))))))))]))
@@ -869,8 +875,10 @@
name:NameClass
decls:ParaDeclsClass
block:BlockClass)
- (with-syntax ([decl (datum->syntax #'name (cons (syntax->datum #'name.name)
- (syntax->list #'decls.pairs)))]
+ (with-syntax ([decl (datum->syntax #'name
+ (cons (syntax->datum #'name.name)
+ (syntax->list #'decls.pairs))
+ #'name)]
[block #'block])
(quasisyntax/loc stx (begin
(~? (raise (format "Prefixes not allowed: ~a" 'prefix)))
@@ -898,7 +906,8 @@
output-expr:ExprClass
body:ExprClass)
(with-syntax ([decl (datum->syntax #'name (cons (syntax->datum #'name.name)
- (syntax->list #'decls.pairs)))]
+ (syntax->list #'decls.pairs))
+ #'name)]
; Parser "Expr" includes both expressions and formulas. Thus, disambiguate
; (e.g.) the "Expr" `one univ` into true expr and multiplicity in the expander;
; It's not the job of the `fun` macro to handle this. (Same for `pred`, etc.)
@@ -942,7 +951,8 @@
(~optional scope:ScopeClass)
(~optional bounds:BoundsClass))
(with-syntax ([cmd-type (datum->syntax #'cmd-type
- (string->symbol (syntax->datum #'cmd-type)))]
+ (string->symbol (syntax->datum #'cmd-type))
+ #'cmd-type)]
[name #`(~? name.name #,(make-temporary-name stx))]
[preds #'(~? pred.name preds)])
#`(begin
@@ -963,11 +973,12 @@
preds:BlockClass))
(~optional scope:ScopeClass)
(~optional bounds:BoundsClass)
- (~and expected (~or "sat" "unsat" "theorem")))
+ (~and expected (~or "sat" "unsat" "theorem" "forge_error")))
(with-syntax ([name #`(~? name.name #,(make-temporary-name stx))]
[preds #'(~? pred.name preds)]
[expected (datum->syntax #'expected
- (string->symbol (syntax->datum #'expected)))])
+ (string->symbol (syntax->datum #'expected))
+ #'expected)])
(syntax/loc stx
(test name (~? (~@ #:preds [preds]))
(~? (~@ #:scope scope.translate))
@@ -1008,8 +1019,8 @@
[qpd:QuantifiedPropertyDeclClass
;;;#:do [(printf "QuantifiedPropertyDeclClass.PropExprs: ~a~n" (syntax->datum #'qpd.prop-exprs))]
(with-syntax*
- ( [(exp-pred-exprs ...) (datum->syntax stx (cons (syntax->datum #'qpd.pred-name) (syntax->datum #'qpd.pred-exprs)))]
- [(exp-prop-exprs ...) (datum->syntax stx (cons (syntax->datum #'qpd.prop-name) (syntax->datum #'qpd.prop-exprs)))]
+ ( [(exp-pred-exprs ...) (datum->syntax stx (cons (syntax->datum #'qpd.pred-name) (syntax->datum #'qpd.pred-exprs)) stx)]
+ [(exp-prop-exprs ...) (datum->syntax stx (cons (syntax->datum #'qpd.prop-name) (syntax->datum #'qpd.prop-exprs)) stx)]
[prop-consolidated (if (equal? (syntax->datum #'qpd.prop-exprs) '())
(syntax/loc stx qpd.prop-name)
@@ -1125,7 +1136,7 @@
(first xs)]
[else
(raise-forge-error
- #:msg (format "Ill-formed block: expected either one expression or any number of formulas")
+ #:msg (format "Ill-formed block: expected either one expression or any number of formulas; got ~a" xs)
#:context stx)]))
; Block : /LEFT-CURLY-TOK Expr* /RIGHT-CURLY-TOK
@@ -1244,7 +1255,7 @@
op)
expr1:ExprClass)
(with-syntax ([expr1 (my-expand #'expr1)]
- [op (datum->syntax #'op (string->symbol (syntax->datum #'op)))])
+ [op (datum->syntax #'op (string->symbol (syntax->datum #'op)) #'op)])
(syntax/loc stx (op (#:lang (get-check-lang)) expr1)))]
[((~datum Expr) "#" expr1:ExprClass)
@@ -1438,11 +1449,13 @@
(with-syntax ([ellip '...])
(syntax/loc stx-outer
(define-syntax (macro-id stx)
+ ; Uncomment this if debugging loss of syntax location. Look through the spam for
+ ; syntax that doesn't carry a location or that has unexpected location.
+ ;(printf "in macro-id ~a: ~a~n" 'macro-id stx)
(syntax-parse stx
#:track-literals
[((~var macro-id id) . pattern) pattern-directive ... (syntax/loc stx template)]))))]))
-
(dsm-keep (Expr1 stx ...) (Expr stx ...))
(dsm-keep (Expr2 stx ...) (Expr stx ...))
(dsm-keep (Expr3 stx ...) (Expr stx ...))
diff --git a/forge/last-checker.rkt b/forge/last-checker.rkt
index 034043e8d..63c62c9fa 100644
--- a/forge/last-checker.rkt
+++ b/forge/last-checker.rkt
@@ -92,22 +92,35 @@
(check-and-output formula
node/formula/quantified
checker-hash
- (begin (for-each
- (lambda (decl)
- (let ([var (car decl)]
- [domain (cdr decl)])
- ; CHECK: shadowed variables
- (when (assoc var quantvars)
- (raise-syntax-error #f
- (format "Shadowing of variable ~a detected. Check for something like \"some x: A | some x : B | ...\"." var)
- (datum->syntax #f var (build-source-location-syntax (nodeinfo-loc info)))))
- ; CHECK: recur into domain(s)
- (checkExpression run-or-state domain quantvars checker-hash)))
- decls)
- ; Extend domain environment
- (let ([new-quantvars (append (map assocify decls) quantvars)])
- ; CHECK: recur into subformula
- (checkFormula run-or-state subform new-quantvars checker-hash))))]
+ (begin
+ ; The new set of quantified variables will be extended by the variables declared here.
+ ; When checking the domains of each, need to make the _prior_ decls available.
+
+ (let ([new-quantvars
+ (foldl
+ (lambda (decl sofar)
+ (let ([var (car decl)]
+ [domain (cdr decl)])
+ ; CHECK: shadowed variables
+ ; We look only at identity (taking the gensym suffix into account), rather than
+ ; looking at names. See tests/forge/ast-errors.frg.
+
+ (when (assoc var quantvars)
+ #;(ormap (lambda (qvd)
+ (equal?
+ (node/expr/quantifier-var-name var)
+ (node/expr/quantifier-var-name (first qvd)))) quantvars)
+ (raise-forge-error
+ #:msg (format "Nested re-use of variable ~a detected. Check for something like \"some x: A | some x : B | ...\"." var)
+ #:context var))
+ ; CHECK: recur into domain(s), carrying decls from prior quantifiers
+ ; (but not this one!)
+ (checkExpression run-or-state domain sofar checker-hash)
+ ; Add to _end_ of the list, to maintain ordering
+ (reverse (cons (assocify decl) (reverse sofar)))))
+ quantvars decls)])
+ ; CHECK: recur into subformula (with extended variable environment)
+ (checkFormula run-or-state subform new-quantvars checker-hash))))]
[(node/formula/sealed info)
(checkFormula run-or-state info quantvars)]
[else (error (format "no matching case in checkFormula for ~a" (deparse formula)))]))
@@ -434,34 +447,52 @@
checker-hash
; Look up in quantvars association list, type is type of domain
(cons (if (assoc expr quantvars) ; expr, not sym (decls are over var nodes)
- (checkExpression run-or-state (second (assoc expr quantvars)) quantvars checker-hash)
- (raise-syntax-error #f (format "Variable ~a used but was unbound in overall formula being checked. Bound variables: ~a" sym (map car quantvars) )
- (datum->syntax #f name (build-source-location-syntax (nodeinfo-loc info)))))
- #t))]
+ (checkExpression run-or-state (second (assoc expr quantvars)) quantvars checker-hash)
+ (raise-forge-error
+ #:msg (format "Variable ~a used, but it was unbound at this point.\
+ Often, this means that a sig, field, or helper name is being used as a quantifier variable.\
+ It might also mean that the variable domain references the variable itself.\
+ For help debugging, the bound variables at this point were: ~a" sym (map car quantvars) )
+ #:context info))
+ #t))]
; set comprehension e.g. {n : Node | some n.edges}
[(node/expr/comprehension info arity decls subform)
(check-and-output expr
node/expr/comprehension
checker-hash
- (cons (let ([child-values
- (map (lambda (decl)
- (let ([var (car decl)]
- [domain (cdr decl)])
- ; CHECK: shadowed variables
- (when (assoc var quantvars)
- (raise-syntax-error #f (format "Shadowing of variable ~a detected. Check for something like \"some x: A | some x : B | ...\"." var)
- (datum->syntax #f var (build-source-location-syntax (nodeinfo-loc info)))))
- ; CHECK: recur into domain(s)
- (checkExpression run-or-state domain quantvars checker-hash)))
- decls)]
- ; Extend domain environment
- [new-quantvars (append (map assocify decls) quantvars)])
- ; CHECK: recur into subformula
- (checkFormula run-or-state subform new-quantvars checker-hash)
- ; Return type constructed from decls above
- (map flatten (map append (apply cartesian-product child-values))))
- #f))]
+ ; For rationale here, see the quantified-formula case. This differs slightly
+ ; because a comprehension is an expression, and thus needs to report its type.
+
+ (begin
+ (let ([new-decls-and-child-values
+ (foldl (lambda (decl acc)
+ (let ([var (car decl)]
+ [domain (cdr decl)]
+ [expanded-quantvars (first acc)]
+ [child-types (second acc)])
+ ; CHECK: shadowed variables (by identity, not by name)
+ (when (assoc var quantvars)
+ (raise-forge-error
+ #:msg (format "Nested re-use of variable ~a detected. Check for something like \"some x: A | some x : B | ...\"." var)
+ #:context info))
+
+ ; CHECK: recur into domain(s), aware of prior variables
+ (let ([next-child-type
+ (checkExpression run-or-state domain expanded-quantvars checker-hash)])
+ ; Accumulator: add current decl, add type (to end)
+ (list (cons (assocify decl) expanded-quantvars)
+ (reverse (cons next-child-type (reverse child-types)))))))
+ ; Acc has the form: (quantvars-so-far child-values-in-order)
+ (list quantvars '())
+ decls)])
+ ; CHECK: recur into subformula
+ (define new-quantvars (first new-decls-and-child-values))
+ (define child-values (second new-decls-and-child-values))
+ (checkFormula run-or-state subform new-quantvars checker-hash)
+ ; Return type constructed from decls above
+ (cons (map flatten (map append (apply cartesian-product child-values)))
+ #f))))]
[else (error (format "no matching case in checkExpression for ~a" (deparse expr)))]))
@@ -508,12 +539,17 @@
; SETMINUS
[(? node/expr/op/-?)
- (check-and-output expr
- node/expr/op/-
- checker-hash
- ; A-B should have only 2 children. B may be empty.
- (cons (checkExpression run-or-state (first args) quantvars checker-hash)
- #t))]
+ (begin
+ ; A-B should have only 2 children. B may not exist; use A as the bound returned regardless.
+ ; However, if B is present, we must /check/ it anyway (and discard non-error results).
+ (when (@> (length args) 1)
+ (checkExpression run-or-state (second args) quantvars checker-hash))
+ (check-and-output expr
+ node/expr/op/-
+ checker-hash
+ ; A-B should have only 2 children. B may be empty.
+ (cons (checkExpression run-or-state (first args) quantvars checker-hash)
+ #t)))]
; INTERSECTION
[(? node/expr/op/&?)
@@ -548,14 +584,15 @@
(when (empty? join-result)
(if (eq? (nodeinfo-lang (node-info expr)) 'bsl)
((hash-ref checker-hash 'empty-join) expr)
- (raise-syntax-error #f
- (format "~n join always results in an empty relation: ~n Left argument of join \"~a\" is in ~a~n Right argument of join \"~a\" is in ~a~n There is no possible join result "
- (deparse (first (node/expr/op-children expr)))
- (map (lambda (lst) (string-join (map (lambda (c) (symbol->string c)) lst) " -> " #:before-first "(" #:after-last ")")) (car (first child-values)))
- (deparse (second (node/expr/op-children expr)))
- (map (lambda (lst) (string-join (map (lambda (c) (symbol->string c)) lst) " -> " #:before-first "(" #:after-last ")")) (car (second child-values)))
- )
- (datum->syntax #f (deparse expr) (build-source-location-syntax (nodeinfo-loc (node-info expr))))))))
+ (raise-forge-error
+ #:msg (format "Join always results in an empty relation:\
+ Left argument of join \"~a\" is in ~a.\
+ Right argument of join \"~a\" is in ~a"
+ (deparse (first (node/expr/op-children expr)))
+ (map (lambda (lst) (string-join (map (lambda (c) (symbol->string c)) lst) " -> " #:before-first "(" #:after-last ")")) (car (first child-values)))
+ (deparse (second (node/expr/op-children expr)))
+ (map (lambda (lst) (string-join (map (lambda (c) (symbol->string c)) lst) " -> " #:before-first "(" #:after-last ")")) (car (second child-values))))
+ #:context expr))))
(when (and (not (cdr (first child-values))) (eq? (nodeinfo-lang (node-info expr)) 'bsl))
((hash-ref checker-hash 'relation-join) expr args))
(cons join-result
@@ -684,10 +721,14 @@
(define decls (node/int/sum-quant-decls expr))
(let ([new-quantvars (append (map assocify decls) quantvars)])
(checkInt run-or-state (node/int/sum-quant-int-expr expr) new-quantvars checker-hash))
- (for ([decl decls])
+ (for/fold ([new-quantvars quantvars])
+ ([decl decls])
(define var (car decl))
(define domain (cdr decl))
- (checkExpression run-or-state domain quantvars checker-hash))]))
+ ; Check and throw away result
+ (checkExpression run-or-state domain new-quantvars checker-hash)
+ (cons (list var domain) quantvars))
+ (void)]))
; Is this integer literal safe under the current bitwidth?
(define/contract (check-int-literal run-or-state expr)
diff --git a/forge/run-tests.sh b/forge/run-tests.sh
index 748b7e326..57bb8e953 100755
--- a/forge/run-tests.sh
+++ b/forge/run-tests.sh
@@ -13,10 +13,12 @@ fi
echo "Re-running Forge setup for test efficiency."
raco setup forge
-
# Get test files
testDir=$1
-doNotTestPattern="[error|srcloc]/[^/]*\\.frg"
+# In "basic" regular expressions, use the backslashed versions of "(", ")", and "|"
+# Also, apply the pattern deeper than just one directory level (handle error/loc/*.frg)
+#doNotTestPattern="\(error\|srclocs\)/[^/]*\\.frg"
+doNotTestPattern="\(error\|srclocs\)/.*\\.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)"
diff --git a/forge/send-to-kodkod.rkt b/forge/send-to-kodkod.rkt
index 42316d9e4..efcb6a047 100644
--- a/forge/send-to-kodkod.rkt
+++ b/forge/send-to-kodkod.rkt
@@ -152,7 +152,7 @@
[(and (unbox server-state) ((Server-ports-is-running? (unbox server-state))))
(define sstate (unbox server-state))
(when (@> (get-verbosity) VERBOSITY_LOW)
- (printf "Pardinus solver process already running. Starting new run with id ~a.~n" run-name))
+ (printf "Pardinus solver process already running. Preparing to start new run with id ~a.~n" run-name))
(values (Server-ports-stdin sstate) (Server-ports-stdout sstate)
(Server-ports-stderr sstate) (Server-ports-shutdown sstate)
(Server-ports-is-running? sstate))]
@@ -190,7 +190,43 @@
; Print configure and declare univ size
; Note that target mode is passed separately, nearer to the (solve) invocation
- (define bitwidth (get-bitwidth run-spec))
+ (define bitwidth (get-bitwidth run-spec))
+
+
+ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+ ;; Generate top-level constraint for this run, execute last-checker
+ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+ (define (maybe-alwaysify fmla)
+ (if (equal? 'temporal (get-option run-spec 'problem_type))
+ (always/info (node-info fmla) fmla)
+ fmla))
+
+ ; If in temporal mode, need to always-ify the auto-generated constraints but not the
+ ; predicates that come from users
+ (define raw-implicit-constraints
+ (append (get-sig-size-preds run-spec sig-to-bound #:error raise-run-error)
+ (get-relation-preds run-spec)
+ (get-extender-preds run-spec)
+ relation-constraints
+ break-preds))
+ (define conjuncts-implicit-constraints
+ (apply append (map maybe-and->list raw-implicit-constraints)))
+ (define implicit-constraints
+ (map maybe-alwaysify conjuncts-implicit-constraints))
+ (define explicit-constraints
+ (apply append (map maybe-and->list (Run-spec-preds run-spec))))
+ (define run-constraints
+ (append explicit-constraints implicit-constraints))
+
+ ; Run last-minute checks for errors
+ (for-each (lambda (c)
+ (checkFormula run-spec c '() (get-checker-hash)))
+ run-constraints)
+
+ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+ ;; Beginning to send to Pardinus. All type-checking must be complete _before_ this point.
+ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(pardinus-print (pardinus:print-cmd (format "(with ~a" run-name)))
(pardinus-print
(pardinus:configure (format ":bitwidth ~a :solver ~a :max-solutions 1 :verbosity ~a :skolem-depth ~a :sb ~a :core-gran ~a :core-minimization ~a :log-trans ~a ~a ~a"
@@ -247,39 +283,6 @@
; Declare assertions
(define all-rels (get-all-rels run-spec))
-
- (define (maybe-alwaysify fmla)
- (if (equal? 'temporal (get-option run-spec 'problem_type))
- (always/info (node-info fmla) fmla)
- fmla))
-
- ; Get and print predicates
- ; If in temporal mode, need to always-ify the auto-generated constraints but not the
- ; predicates that come from users
- ; !!!
- (define raw-implicit-constraints
- (append (get-sig-size-preds run-spec sig-to-bound #:error raise-run-error)
- (get-relation-preds run-spec)
- (get-extender-preds run-spec)
- relation-constraints
- break-preds))
- (define conjuncts-implicit-constraints
- (apply append (map maybe-and->list raw-implicit-constraints)))
- (define implicit-constraints
- (map maybe-alwaysify conjuncts-implicit-constraints))
- (define explicit-constraints
- (apply append (map maybe-and->list (Run-spec-preds run-spec))))
-
- (define run-constraints
- (append explicit-constraints implicit-constraints))
-
- ; Run last-minute checks for errors
- (for-each (lambda (c)
- ;(printf "deparse-constraint: ~a~n" (deparse c))
- (checkFormula run-spec c '() (get-checker-hash)))
- run-constraints)
- ;(when (@>= (get-verbosity) VERBOSITY_LOW)
- ; (printf " Last-checker finished. Beginning to send problem.~n"))
; Keep track of which formula corresponds to which CLI assert
; for highlighting unsat cores. TODO: map back from CLI output
diff --git a/forge/server/forgeserver.rkt b/forge/server/forgeserver.rkt
index c72d267d4..c86a38572 100644
--- a/forge/server/forgeserver.rkt
+++ b/forge/server/forgeserver.rkt
@@ -50,11 +50,14 @@
(define id-to-instance-map (make-hash)) ; mutable hash
(define (get-current-instance)
- (tree:get-value current-tree))
+ (define returned-instance (tree:get-value current-tree))
+ (set-box! (Run-last-sterling-instance the-run) returned-instance)
+ returned-instance)
(define (get-next-instance [next-mode 'P])
(set! current-tree (tree:get-child current-tree next-mode))
(set! curr-datum-id (+ curr-datum-id 1))
- (hash-set! id-to-instance-map curr-datum-id (get-current-instance))
+ ; get-current-instance updates the Run's last sterling instance cursor when called
+ (hash-set! id-to-instance-map curr-datum-id (get-current-instance))
(values curr-datum-id (get-current-instance)))
(define command-string (format "~a" (syntax->datum command)))
diff --git a/forge/sigs-functional.rkt b/forge/sigs-functional.rkt
index 39e3b187f..7e4aab7aa 100644
--- a/forge/sigs-functional.rkt
+++ b/forge/sigs-functional.rkt
@@ -632,7 +632,7 @@
(define-values (result atoms server-ports kodkod-currents kodkod-bounds)
(send-to-kodkod spec command #:run-name name))
- (Run name command spec result server-ports atoms kodkod-currents kodkod-bounds))
+ (Run name command spec result server-ports atoms kodkod-currents kodkod-bounds (box #f)))
;; NOTE WELL: make sure not to re-use run names; this will cause an
diff --git a/forge/sigs-structs.rkt b/forge/sigs-structs.rkt
index a6d34bd79..cc2fc9483 100644
--- a/forge/sigs-structs.rkt
+++ b/forge/sigs-structs.rkt
@@ -210,11 +210,15 @@
[name symbol?]
[command syntax?]
[run-spec Run-spec?]
+ ; This is the *start* of the exploration tree
[result tree:node?]
[server-ports Server-ports?]
[atoms (listof (or/c symbol? number?))]
[kodkod-currents Kodkod-current?]
- [kodkod-bounds (listof any/c)] ; TODO: specify
+ [kodkod-bounds (listof any/c)]
+ ; This is Sterling's current cursor into the exploration tree.
+ ; It is mutated whenever Sterling asks for a new instance.
+ [last-sterling-instance (box/c (or/c Sat? Unsat? false/c))]
) #:transparent)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -652,11 +656,26 @@ Returns whether the given run resulted in sat or unsat, respectively.
; or expression form (which has its own AST node). Avoid exponential
; blowup from chained IFTEs by expanding to a chain of function calls.
(define (ifte-disambiguator info a b c)
- (if (node/formula? b)
- (&&/info info
- (=>/info info a b)
- (=>/info info (!/info info a) c))
- (ite/info info a b c)))
+ (unless (node/formula? a)
+ (raise-forge-error
+ #:msg ("If-then-else needed a boolean-valued formula for its first argument; got ~a." (pretty-type-of a))
+ #:context a))
+ (cond
+ ; It's a formula if-then-else
+ [(and (node/formula? b) (node/formula? c))
+ (&&/info info
+ (=>/info info a b)
+ (=>/info info (!/info info a) c))]
+ ; It's an expression if-then-else (note: mixing int-expr and rel-expr is OK)
+ [(and (or (node/expr? b) (node/int? b) (integer? b))
+ (or (node/expr? c) (node/int? c) (integer? c)))
+ (ite/info info a b c)]
+ ; It's an error
+ [else
+ (raise-forge-error #:msg (format "If-then-else needed consistent types (either both formulas or both expressions) for its true and false branches, but got (~a) and (~a)."
+ (pretty-type-of b) (pretty-type-of c))
+ #:context info)]))
+
(define-syntax (ifte stx)
(syntax-parse stx
[(_ (~optional (#:lang check-lang) #:defaults ([check-lang #''checklangNoCheck])) a b c) (quasisyntax/loc stx
@@ -722,19 +741,17 @@ Returns whether the given run resulted in sat or unsat, respectively.
(->/info info univ b)))
(define (domain-check<: a b loc)
- (let ([src-line (source-location-line loc)]
- [src-col (source-location-column loc)]
- [src-span (source-location-span loc)])
- (unless (equal? (node/expr-arity b)
- (@+ 1 (node/expr-arity a)))
- (raise-user-error (format "<: argument has incorrect arity (~a vs. ~a) in ~a <: ~a on line ~a, column ~a, span ~a"
- (node/expr-arity a) (node/expr-arity b) (deparse a) (deparse b) src-line src-col src-span)))))
+ (unless (equal? (node/expr-arity b)
+ (@+ 1 (node/expr-arity a)))
+ (raise-forge-error
+ #:msg (format "<: argument has incorrect arity (~a vs. ~a) in ~a <: ~a"
+ (node/expr-arity a) (node/expr-arity b) (deparse a) (deparse b))
+ #:context loc)))
(define (domain-check:> a b loc)
- (let ([src-line (source-location-line loc)]
- [src-col (source-location-column loc)]
- [src-span (source-location-span loc)])
- (unless (equal? (node/expr-arity a)
- (@+ 1 (node/expr-arity b)))
- (raise-user-error (format ":> argument has incorrect arity (~a vs. ~a) in ~a :> ~a on line ~a, column ~a, span ~a"
- (node/expr-arity a) (node/expr-arity b) (deparse a) (deparse b) src-line src-col src-span)))))
+ (unless (equal? (node/expr-arity a)
+ (@+ 1 (node/expr-arity b)))
+ (raise-forge-error
+ #:msg (format ":> argument has incorrect arity (~a vs. ~a) in ~a :> ~a"
+ (node/expr-arity a) (node/expr-arity b) (deparse a) (deparse b))
+ #:context loc)))
diff --git a/forge/sigs.rkt b/forge/sigs.rkt
index d1b375e42..3e0a86f70 100644
--- a/forge/sigs.rkt
+++ b/forge/sigs.rkt
@@ -638,7 +638,30 @@
(add-to-execs
(with-syntax ([loc (build-source-location stx)])
(quasisyntax/loc stx
- (cond
+ (cond
+
+ [(equal? 'expected 'forge_error)
+ ; Expecting an error. If we receive one, do nothing.
+ ; Otherwise, continue to report the error and then close the run.
+ ; (N.B., this assumes the run isn't actually created or sent to the solver.)
+ (define run-reference #f)
+ (with-handlers ([exn:fail:user? void])
+ #,(syntax/loc stx (run name args ...))
+ ; Cannot throw the new "failed test" Forge error here, or it will be caught and ignored
+ (set! run-reference name)
+ (close-run name))
+ ; Instead, wait and throw it here (note this will only happen if _NO_ user-error was
+ ; produced by the run, and thus a run-reference is present.
+ (when run-reference
+ (report-test-failure
+ #:name 'name
+ #:msg (format "Failed test ~a. No Forge error was produced." 'name)
+ #:context loc
+ #:run run-reference
+ #:sterling #f))
+ (when (member 'name (hash-keys (State-runmap curr-state)))
+ (printf "Warning: successful `is forge_error` test run left in state environment: ~a.~n" 'name))]
+
[(member 'expected '(sat unsat))
#,(syntax/loc stx (run name args ...))
(define first-instance (tree:get-value (Run-result name)))
@@ -1036,7 +1059,7 @@
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Struct to hold test-failure information for eventual reporting
-(struct test-failure (name msg context instance run))
+(struct test-failure (name msg context instance run sterling))
; Mutable value to store list of test-failure structs
(define delayed-test-failures null)
; Called to clear the mutable list
@@ -1044,7 +1067,8 @@
; Record (or report, depending on the value of the delay-test-failure-reporting?
; parameter) a test failure.
-(define (report-test-failure #:name name #:msg msg #:context context #:instance [instance #f] #:run run)
+(define (report-test-failure #:name name #:msg msg #:context context
+ #:instance [instance #f] #:run run #:sterling [sterling #t])
; Default is to not delay, but options may affect this.
(cond [(not (equal? (get-option run 'test_keep) 'first))
(unless (equal? (get-verbosity) 0)
@@ -1053,14 +1077,15 @@
(unless (empty? delayed-test-failures)
(close-run (test-failure-run (first delayed-test-failures))))
; then add this failure to the queue
- (set! delayed-test-failures (cons (test-failure name msg context instance run)
+ (set! delayed-test-failures (cons (test-failure name msg context instance run sterling)
delayed-test-failures))]
[else
; Raise a Forge error and stop execution; show Sterling if enabled.
(when (>= (get-verbosity) 1)
- (printf "Test ~a failed. Opening Sterling (if able) and stopping.~n" name))
- (true-display run)
+ (printf "Test ~a failed. Stopping execution.~n" name))
+ (when sterling
+ (true-display run))
(raise-forge-error #:msg msg #:context context)]))
; To be run at the very end of the Forge execution; reports test failures and opens
@@ -1074,14 +1099,14 @@
(define last-failure (if (empty? failures) #f (last failures)))
(for ([failure failures])
- (define-values (name msg context instance run)
+ (define-values (name msg context instance run sterling)
(values (test-failure-name failure) (test-failure-msg failure)
(test-failure-context failure) (test-failure-instance failure)
- (test-failure-run failure)))
+ (test-failure-run failure) (test-failure-sterling failure)))
; Print the error (don't raise an actual exception)
- (define sterling-or-instance (if (equal? (get-option run 'run_sterling) 'off)
- (format "Sterling disabled, so reporting raw instance data:~n~a" instance)
+ (define sterling-or-instance (if (or (not sterling) (equal? (get-option run 'run_sterling) 'off))
+ (format "Sterling disabled for this test. Reporting raw instance data:~n~a" instance)
(format "Running Sterling to show instance generated, if any.~n~a"
(if (equal? failure last-failure)
"Solver is active; evaluator and next are available."
@@ -1090,7 +1115,7 @@
#:context context
#:raise? #f)
; Display in Sterling (if run_sterling is enabled)
- (when (equal? failure last-failure)
+ (when (and sterling (equal? failure last-failure))
(true-display run)))
; Return to empty-failure-list state.
diff --git a/forge/sterling/README.md b/forge/sterling/README.md
index d3089f147..cafa2cc06 100644
--- a/forge/sterling/README.md
+++ b/forge/sterling/README.md
@@ -1 +1,3 @@
-This folder contains a build of the current version of Sterling.
+This folder contains a build of the current version of Sterling for Forge. To update, build Sterling and recursively copy the contents of the `dist` folder in that repo to the `build` sub-folder here. Remember to build with `yarn run build:forge`; the Forge version is slightly different from the Alloy version.
+
+
diff --git a/forge/sterling/build/6007.bundle.js b/forge/sterling/build/6007.bundle.js
deleted file mode 100644
index 885780ea5..000000000
--- a/forge/sterling/build/6007.bundle.js
+++ /dev/null
@@ -1,2 +0,0 @@
-/*! For license information please see 6007.bundle.js.LICENSE.txt */
-(self.webpackChunksterling_ts=self.webpackChunksterling_ts||[]).push([[6007],{68921:(e,t,n)=>{"use strict";n.d(t,{zx:()=>E,hE:()=>C,hU:()=>T});var i=n(97375),o=n(105),r=n(44592),s=n(38554),a=n.n(s),l=n(67294),c=n(26450),d=n(70917),u=n(1358);function h(){return h=Object.assign||function(e){for(var t=1;t
"+ue(e.message+"",!0)+"";throw e}},fe.Parser=oe,fe.parser=oe.parse,fe.Renderer=se,fe.TextRenderer=ae,fe.Lexer=ie,fe.lexer=ie.lex,fe.Tokenizer=re,fe.Slugger=le,fe.parse=fe,fe}))}(),i||exports,(i||exports).Parser,(i||exports).parser;var o=(i||exports).Renderer,r=((i||exports).TextRenderer,(i||exports).Lexer,(i||exports).lexer,(i||exports).Tokenizer,(i||exports).Slugger,(i||exports).parse)},23897:(e,t,n)=>{"use strict";n.d(t,{Q:()=>r});var i=n(53060),o=n(70666);function r(e){let t=JSON.parse(e);return t=s(t),t}function s(e,t=0){if(!e||t>200)return e;if("object"==typeof e){switch(e.$mid){case 1:return o.o.revive(e);case 2:return new RegExp(e.source,e.flags)}if(e instanceof i.KN||e instanceof Uint8Array)return e;if(Array.isArray(e))for(let n=0;n
${e}
`,t.codeBlockRenderer&&(g.code=(e,n)=>{const o=t.codeBlockRenderer(n,e),r=he.a.nextId();return(0,se.eP)(Promise.all([o,h]),a.token).then((e=>{var n;if(!s&&e){const o=l.querySelector(`div[data-code="${r}"]`);o&&i.mc(o,e[0]),null===(n=t.asyncRenderCallback)||void 0===n||n.call(t)}})).catch((()=>{})),`