make new-∀/c and new-∃/c figure our their own names and have a better printing

This commit is contained in:
Robby Findler 2014-05-11 16:42:57 -05:00
parent 4f7a119a08
commit 6df33ab08c
3 changed files with 40 additions and 10 deletions

View File

@ -1157,7 +1157,7 @@ if they do not, a contract violation is signaled.
]
}
@defproc[(new-∀/c [name symbol?]) contract?]{
@defproc[(new-∀/c [name (or/c symbol? #f) #f]) contract?]{
Constructs a new universal contract.
Universal contracts accept all values when in negative positions (e.g., function
@ -1166,22 +1166,22 @@ if they do not, a contract violation is signaled.
a universal contract accepts only values that were previously accepted
in negative positions (by checking for the wrappers).
The name is used to identify the contract in error messages.
The name is used to identify the contract in error messages and defaults
to a name based on the lexical context of @racket[new-∀/c].
For example, this contract:
@racketblock[(let ([a (new-∀/c 'a)])
(-> a a))]
describes the identity function (or a non-terminating function)
describes the identity function (or a non-terminating function).
That is, the first use of the @racket[a] appears in a
negative position and thus inputs to that function are wrapped with an opaque struct.
Then, when the function returns, it is checked to determine whether the result is wrapped, since
the second @racket[a] appears in a positive position.
The @racket[new-∀/c] construct constructor is dual to @racket[new-∃/c].
}
@defproc[(new-∃/c [name symbol?]) contract?]{
@defproc[(new-∃/c [name (or/c symbol? #f) #f]) contract?]{
Constructs a new existential contract.
Existential contracts accept all values when in positive positions (e.g., function
@ -1190,7 +1190,8 @@ if they do not, a contract violation is signaled.
they accepts only values that were previously accepted in positive positions (by checking
for the wrappers).
The name is used to identify the contract in error messages.
The name is used to identify the contract in error messages and defaults
to a name based on the lexical context of @racket[new-∀/c].
For example, this contract:
@racketblock[(let ([a (new-∃/c 'a)])

View File

@ -326,6 +326,12 @@
(test-name '(set/c (set/c char?) #:cmp 'eqv) (set/c (set/c char? #:cmp 'dont-care) #:cmp 'eqv))
(test-name '(set/c (-> char? char?) #:cmp 'equal) (set/c (-> char? char?) #:cmp 'equal))
(test-name 'α (let ([α (new-∀/c)]) α))
(test-name 'α (let ([α (new-∀/c #f)]) α))
(test-name 'β (let ([α (new-∀/c 'β)]) α))
(test-name '∀∃-unknown ((values new-∀/c)))
(test-name '∀∃-unknown ((values new-∀/c) #f))
(test-name '(class/c [m (->m integer? integer?)]) (class/c [m (->m integer? integer?)]))
(test-name '(class/c [m (->*m (integer?) (integer?) integer?)])
(class/c [m (->*m (integer?) (integer?) integer?)]))

View File

@ -1,10 +1,12 @@
#lang racket/base
(require "prop.rkt"
"blame.rkt")
"blame.rkt"
"guts.rkt"
(for-syntax racket/base syntax/name))
(provide new-∃/c
new-∀/c
(provide (rename-out [_new-∃/c new-∃/c]
[_new-∀/c new-∀/c])
∀∃?)
(define (∀∃-proj ctc)
@ -22,6 +24,7 @@
(define-struct ∀∃/c (in out pred? name neg?)
#:omit-define-syntaxes
#:property prop:custom-write custom-write-property-proc
#:property prop:contract
(build-contract-property
#:name (λ (ctc) (∀∃/c-name ctc))
@ -30,6 +33,27 @@
(define-struct ∀∃ ())
(define-for-syntax (∀∃/trans which stx)
(define name (or (syntax-local-name)
(let ([n (syntax-local-infer-name stx)])
(string->symbol
(format "∀∃-~a" (or n "unknown"))))))
(syntax-case stx ()
[x
(identifier? #'x)
#`(let ([which (case-lambda
[() (#,which '#,name)]
[(x) (#,which (or x '#,name))])])
which)]
[(f) #`(#,which '#,name)]
[(f x) #`(#,which (or x '#,name))]
[(f . x)
(with-syntax ([app (datum->syntax stx '#%app stx stx)])
#`(app #,which . x))]))
(define-syntax (_new-∀/c stx) (∀∃/trans #'new-∀/c stx))
(define-syntax (_new-∃/c stx) (∀∃/trans #'new-∃/c stx))
(define (new-∃/c raw-name) (mk raw-name #t))
(define (new-∀/c raw-name) (mk raw-name #f))
@ -38,4 +62,3 @@
(define-values (struct-type constructor predicate accessor mutator)
(make-struct-type name struct:∀∃ 1 0))
(make-∀∃/c constructor (λ (x) (accessor x 0)) predicate raw-name neg?))