Hi all, Is there any reason that the #:forall, #:∀ clause (dual to #:exists, #:∃) doesn't exist for contract-out?
If it's just that nobody has written it, I've attached a patch that implements it. If there aren't any design issues anyone has in mind, I'll push it once I write tests and docs. Cheers, Asumu
>From 39c7f488736dc842e6989c5088930e7b049142b5 Mon Sep 17 00:00:00 2001 From: Asumu Takikawa <[email protected]> Date: Tue, 21 Aug 2012 14:46:13 -0400 Subject: [PATCH] =?UTF-8?q?Add=20#:forall,=20#:=E2=88=80=20to=20contract-out?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- collects/racket/contract/private/provide.rkt | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/collects/racket/contract/private/provide.rkt b/collects/racket/contract/private/provide.rkt index 5e92549..735a603 100644 --- a/collects/racket/contract/private/provide.rkt +++ b/collects/racket/contract/private/provide.rkt @@ -169,7 +169,8 @@ ;; compare raw identifiers for `struct' and `rename' just like provide does (syntax-case* clause (struct rename) (λ (x y) (eq? (syntax-e x) (syntax-e y))) [exists - (or (eq? '#:exists (syntax-e #'exists)) (eq? '#:∃ (syntax-e #'exists))) + (or (eq? '#:exists (syntax-e #'exists)) (eq? '#:∃ (syntax-e #'exists)) + (eq? '#:forall (syntax-e #'exists)) (eq? '#:∀ (syntax-e #'exists))) (cond [(null? (cdr clauses)) (raise-syntax-error who @@ -184,7 +185,7 @@ (if just-check-errors? (loop (cddr clauses) exists-binders) (with-syntax ([(x-gen) (generate-temporaries #'(x))]) - (cons (code-for-one-exists-id #'x #'x-gen) + (cons (code-for-one-poly-id #'x #'x-gen #'exists) (loop (cddr clauses) (add-a-binder #'x #'x-gen exists-binders)))))] [(x ...) @@ -192,7 +193,7 @@ (if just-check-errors? (loop (cddr clauses) exists-binders) (with-syntax ([(x-gen ...) (generate-temporaries #'(x ...))]) - (append (map code-for-one-exists-id + (append (map code-for-one-poly-id (syntax->list #'(x ...)) (syntax->list #'(x-gen ...))) (loop (cddr clauses) @@ -678,9 +679,11 @@ field-contract-id void?)))) - ;; code-for-one-exists-id : syntax -> syntax - (define (code-for-one-exists-id x x-gen) - #`(define #,x-gen (new-∃/c '#,x))) + ;; code-for-one-poly-id : syntax -> syntax + (define (code-for-one-poly-id x x-gen poly) + (if (or (eq? '#:exists (syntax-e poly)) (eq? '#:∃ (syntax-e poly))) + #`(define #,x-gen (new-∃/c '#,x)) + #`(define #,x-gen (new-∀/c '#,x)))) (define (add-exists-binders stx exists-binders) (if (null? exists-binders) -- 1.7.10.4
_________________________ Racket Developers list: http://lists.racket-lang.org/dev
