Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add support for negated predicates in assert and with-asserts. #1324

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
Expand Up @@ -13,10 +13,12 @@

Typed Racket provides some additional utility functions to facilitate typed programming.

@defproc*[
([(assert [v (U #f A)]) A]
[(assert [v A] [p? (A -> Any : B)]) B])]{
Verifies that the argument satisfies the constraint. If no predicate
@defform*/subs[[(assert val maybe-pred)]
([pred (code:line predicate)
(code:line (not/p pred))]
[maybe-pred code:blank
(code:line pred)])]{
Verifies that the argument satisfies the constraint. If no predicate
is provided, simply checks that the value is not
@racket[#f].

Expand All @@ -30,11 +32,16 @@ x
(define: y : (U String Symbol) "hello")
y
(assert y string?)
(eval:error (assert y boolean?))]
(eval:error (assert y boolean?))
(eval:error (assert y (not/p string?)))
(assert y (not/p (not/p string?)))
(assert y (not/p boolean?))]

@defform*/subs[[(with-asserts ([id maybe-pred] ...) body ...+)]
([maybe-pred code:blank
(code:line predicate)])]{
([pred (code:line predicate)
(code:line (not/p pred))]
[maybe-pred code:blank
(code:line pred)])]{
Guard the body with assertions. If any of the assertions fail, the
program errors. These assertions behave like @racket[assert].
}
Expand Down
23 changes: 16 additions & 7 deletions typed-racket-lib/typed-racket/base-env/extra-procs.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -3,21 +3,30 @@
(provide assert defined?)

(define-syntax (assert stx)
(syntax-case stx ()
[(assert v)
#`(let ([val v])
(syntax-case stx (not/p)
[(assert v) #'(assert v (not/p not))]
[(assert v (not/p (not/p p))) #'(assert v p)]
[(assert v (not/p p))
#`(let ([val v] [pred p])
#,(syntax-property
(syntax/loc stx
(or val (error (format "Assertion failed on ~e" val))))
(if (pred val)
(raise-arguments-error 'assert
(format "Assertion ~s failed" '(assert v (not/p p)))
"expected" `(not/p ,(or (object-name pred) pred))
"given" val)
val))
'feature-profile:TR-dynamic-check #t))]
[(assert v p)
#`(let ([val v]
[pred p])
#`(let ([val v] [pred p])
#,(syntax-property
(quasisyntax/loc stx
(if (pred val)
val
(error (format "Assertion ~e failed on ~e" pred val))))
(raise-arguments-error 'assert
(format "Assertion ~s failed" '(assert v p))
"expected" (or (object-name pred) pred)
"given" val)))
'feature-profile:TR-dynamic-check #t))]))

(define (defined? v) #t)
62 changes: 40 additions & 22 deletions typed-racket-lib/typed-racket/base-env/prims.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -729,28 +729,46 @@ the typed racket language.
[_ rhs]))
(quasisyntax/loc stx (define #,defined-id #,rhs*))]))

(define-syntax (with-asserts stx)
(define-syntax-class with-asserts-clause
[pattern [x:id]
#:with cond-clause
(syntax/loc #'x
[(not x)
(error "Assertion failed")])]
[pattern [x:id pred]
#:with cond-clause
(syntax/loc #'x
[(not (pred x))
(error "Assertion failed")])])
(syntax-parse stx
[(_ (c:with-asserts-clause ...) body:expr ...+)
(syntax-property
(quasisyntax/loc stx
(cond c.cond-clause
...
[else #,(syntax-property
#'(begin body ...)
'feature-profile:TR-dynamic-check 'antimark)]))
'feature-profile:TR-dynamic-check #t)]))
(define-syntax with-asserts
(let ()
(define pred-parser
(λ (stx)
(syntax-parse stx
#:datum-literals (not/p)
[(not/p (not/p p)) (pred-parser #'p)]
[_ stx])))

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

define-lambda-to-define: The define form supports a shorthand for defining functions (including function-returning functions).

Suggested change
(define pred-parser
(λ (stx)
(syntax-parse stx
#:datum-literals (not/p)
[(not/p (not/p p)) (pred-parser #'p)]
[_ stx])))
(define (pred-parser stx)
(syntax-parse stx
#:datum-literals (not/p)
[(not/p (not/p p)) (pred-parser #'p)]
[_ stx]))
Debugging details
Textual replacement
(line-replacement
  #:new-lines
    '#("    (define (pred-parser stx)"
       "      (syntax-parse stx"
       "        #:datum-literals (not/p)"
       "        [(not/p (not/p p)) (pred-parser #'p)]"
       "        [_ stx]))")
  #:original-lines
    '#("    (define pred-parser"
       "      (λ (stx)"
       "        (syntax-parse stx"
       "          #:datum-literals (not/p)"
       "          [(not/p (not/p p)) (pred-parser #'p)]"
       "          [_ stx])))")
  #:start-line 734)
Syntactic replacement
(syntax-replacement
  #:introduction-scope #<procedure:do-make-syntax-introducer>
  #:new-syntax
    #<syntax:/home/runner/.local/share/racket/snapshot/pkgs/resyntax/default-recommendations/function-definition-shortcuts.rkt:87:3 (define (pred-parser (ORIGINAL-SPLICE stx)) (ORIGINAL-GAP (stx) (syntax-parse stx #:datum-literals (not/p) ((not/p (not/p p)) (pred-parser (syntax p))) (_ stx))) (ORIGINAL-SPLICE (syntax-parse stx #:datum-literals (not/p) ((not/p (not/p p)) (pred-parser...>
  #:original-syntax
    #<syntax:typed-racket-lib/typed-racket/base-env/prims.rkt:734:4 (define pred-parser (λ (stx) (syntax-parse stx #:datum-literals (not/p) ((not/p (not/p p)) (pred-parser (syntax p))) (_ stx))))>)

(define assert-parser
(λ (stx)
(syntax-parse stx
#:datum-literals (not/p)
[[x (not/p p)] #'(p x)]
[[x p] #'(not (p x))])))

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

define-lambda-to-define: The define form supports a shorthand for defining functions (including function-returning functions).

Suggested change
(define assert-parser
(λ (stx)
(syntax-parse stx
#:datum-literals (not/p)
[[x (not/p p)] #'(p x)]
[[x p] #'(not (p x))])))
(define (assert-parser stx)
(syntax-parse stx
#:datum-literals (not/p)
[[x (not/p p)] #'(p x)]
[[x p] #'(not (p x))]))
Debugging details
Textual replacement
(line-replacement
  #:new-lines
    '#("    (define (assert-parser stx)"
       "      (syntax-parse stx"
       "        #:datum-literals (not/p)"
       "        [[x (not/p p)] #'(p x)]"
       "        [[x p] #'(not (p x))]))")
  #:original-lines
    '#("    (define assert-parser"
       "      (λ (stx)"
       "        (syntax-parse stx"
       "          #:datum-literals (not/p)"
       "          [[x (not/p p)] #'(p x)]"
       "          [[x p] #'(not (p x))])))")
  #:start-line 740)
Syntactic replacement
(syntax-replacement
  #:introduction-scope #<procedure:do-make-syntax-introducer>
  #:new-syntax
    #<syntax:/home/runner/.local/share/racket/snapshot/pkgs/resyntax/default-recommendations/function-definition-shortcuts.rkt:87:3 (define (assert-parser (ORIGINAL-SPLICE stx)) (ORIGINAL-GAP (stx) (syntax-parse stx #:datum-literals (not/p) ((x (not/p p)) (syntax (p x))) ((x p) (syntax (not (p x)))))) (ORIGINAL-SPLICE (syntax-parse stx #:datum-literals (not/p) ((x (not/p p)) (syntax...>
  #:original-syntax
    #<syntax:typed-racket-lib/typed-racket/base-env/prims.rkt:740:4 (define assert-parser (λ (stx) (syntax-parse stx #:datum-literals (not/p) ((x (not/p p)) (syntax (p x))) ((x p) (syntax (not (p x)))))))>)

(define-syntax-class with-asserts-clause
[pattern [x:id]
#:with cond-clause
(syntax/loc #'x
[(not x)
(raise-arguments-error 'with-asserts
(format "Assertion ~s failed" '(assert x (not/p not))))])]
[pattern [x:id p]
#:with cond-clause
(with-syntax ([p (pred-parser #'p)])
(quasisyntax/loc #'x
[#,(assert-parser #'[x p])
(raise-arguments-error 'with-asserts
(format "Assertion ~s failed" '(assert x p)))]))])
(λ (stx)
(syntax-parse stx
[(_ (c:with-asserts-clause ...) body:expr ...+)
(syntax-property
(quasisyntax/loc stx
(cond c.cond-clause
...
[else
#,(syntax-property
#'(begin body ...)
'feature-profile:TR-dynamic-check 'antimark)]))
'feature-profile:TR-dynamic-check #t)]))))

(define-syntax (typecheck-fail stx)
(syntax-parse stx
Expand Down
2 changes: 1 addition & 1 deletion typed-racket-test/fail/with-asserts.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -4,4 +4,4 @@

(let ([x 1] [y "2"])
(with-asserts ([x string?] [y integer?])
x))
x))
2 changes: 1 addition & 1 deletion typed-racket-test/fail/with-asserts2.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -4,4 +4,4 @@

(let ([x 1] [y "2"])
(with-asserts ([x string?])
x))
x))
2 changes: 1 addition & 1 deletion typed-racket-test/fail/with-asserts3.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -4,4 +4,4 @@

(let ([x #f])
(with-asserts ([x])
x))
x))
7 changes: 7 additions & 0 deletions typed-racket-test/fail/with-asserts4.rkt
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
#;
(exn-pred exn:fail?)
#lang typed/racket

(let ([x 1] [y "2"])
(with-asserts ([x (not/p integer?)] [y integer?])
x))
7 changes: 7 additions & 0 deletions typed-racket-test/fail/with-asserts5.rkt
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
#;
(exn-pred exn:fail?)
#lang typed/racket

(let ([x 1] [y "2"])
(with-asserts ([y (not/p (not/p integer?))])
x))
14 changes: 9 additions & 5 deletions typed-racket-test/succeed/with-asserts.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -2,19 +2,23 @@

(let ([x 1] [y "2"])
(with-asserts ([x integer?] [y string?])
x))
x)
(with-asserts ([x (not/p string?)] [y (not/p (not/p string?))])
x))
(let ([x 1] [y "2"])
(with-asserts ([x integer?])
x))
x)
(with-asserts ([x (not/p (not/p (not/p string?)))])
x))
(let ([x 1] [y "2"])
(with-asserts ()
x))
x))
(let ([x 1] [y "2"])
(with-asserts ([x])
x))
x))

(: f : (U Integer String) -> Integer)
(define (f x)
(with-asserts ([x integer?])
x))
x))
(f 1)