suzanne.soy/typed-racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Make polydotted types generate contracts.

Browse Source 
original commit: 87414956ab23f0d4812b2cc5bd29025b0345666a
This commit is contained in:
Eric Dobson 2014-01-09 22:38:43 -08:00
parent 041577d7bb
commit c933380f40
2 changed files with 22 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

21
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/type-contract.rkt
View File

@ -253,6 +253,15 @@
(hash-set rv v-nm (same (parametric-var/sc temp)))))
(parametric->/sc temporaries
(t->sc b #:recursive-values rv)))))]
[(PolyDots: (list vs ... dotted-v) b)
(if (not (from-untyped? typed-side))
;; in positive position, no checking needed for the variables
(let ((recursive-values (for/fold ([rv recursive-values]) ([v vs])
(hash-set rv v (same any/sc)))))
(t->sc b #:recursive-values recursive-values))
;; in negative position, use parameteric contracts.
(fail #:reason "cannot generate contract for variable arity polymorphic type"))]
[(Mu: n b)
(match-define (and n*s (list untyped-n* typed-n* both-n*)) (generate-temporaries (list n n n)))
(define rv
@ -376,7 +385,7 @@
(define ((f case->) a)
(define (convert-arr arr)
(match arr
[(arr: dom (Values: (list (Result: rngs _ _) ...)) rst #f kws)
[(arr: dom (Values: (list (Result: rngs _ _) ...)) rst drst kws)
(let-values ([(mand-kws opt-kws) (partition-kws kws)])
;; Garr, I hate case->!
(when (and (not (empty? kws)) case->)
@ -389,14 +398,18 @@
null
(map conv mand-kws)
(map conv opt-kws)
(and rst (listof/sc (t->sc/neg rst)))
(or
(and rst (listof/sc (t->sc/neg rst)))
(and drst (listof/sc (t->sc/neg (car drst)
#:recursive-values
(hash-set recursive-values (cdr drst) (same any/sc))))))
(map t->sc rngs))))]))
(match a
;; functions with no filters or objects
[(arr: dom (Values: (list (Result: rngs (FilterSet: (Top:) (Top:)) (Empty:)) ...)) rst #f kws)
[(arr: dom (Values: (list (Result: rngs (FilterSet: (Top:) (Top:)) (Empty:)) ...)) rst drst kws)
(convert-arr a)]
;; functions with filters or objects
[(arr: dom (Values: (list (Result: rngs _ _) ...)) rst #f kws)
[(arr: dom (Values: (list (Result: rngs _ _) ...)) rst drst kws)
(if (from-untyped? typed-side)
(fail #:reason (~a "cannot generate contract for function type"
" with filters or objects."))

18
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/contract-tests.rkt
View File

@ -35,20 +35,8 @@
(with-check-info (('reason reason))
(fail-check "Reason didn't match expected.")))))))
(define known-bugs
(test-suite "Known Bugs"
;; Polydotted functions should work
(t/fail (-polydots (a) (->... (list) (a a) -Symbol))
"not supported for this type")))
(define tests
(test-suite "Contract Tests"
known-bugs
(t (-Number . -> . -Number))
(t (-Promise -Number))
(t (-set Univ))
@ -71,6 +59,9 @@
(t (-> (-poly (A B) (-> (Un A (-mu X (Un A (-lst X)))) (Un A (-mu X (Un A (-lst X))))))
(-> -Symbol (-mu X (Un -Symbol (-lst X))))))
(t (-polydots (a) -Symbol))
(t (-polydots (a) (->... (list) (a a) -Symbol)))
(t/fail ((-poly (a) (-vec a)) . -> . -Symbol)
"cannot generate contract for non-function polymorphic type")
(t/fail (-> (-poly (a b) (-> (Un a b) (Un a b))) Univ)
@ -79,7 +70,8 @@
(-> (-poly (A B) (-> (Un B (-mu X (Un A (-lst X)))) (Un B (-mu X (Un A (-lst X))))))
(-> -Symbol (-mu X (Un -Symbol (-lst X)))))
"multiple parametric contracts are not supported")
(t/fail (-> (-polydots (a) (->... (list) (a a) -Symbol)) Univ)
"cannot generate contract for variable arity polymorphic type")
(t/fail
(make-Function