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

Fix subtyping for keyword function types

Browse Source 
Closes PR 14252
Closes PR 14257

original commit: 0efd90f846913d87aba53d9d73483960a98e63a8
This commit is contained in:
Asumu Takikawa 2014-01-11 00:56:18 -05:00
parent 5e75b2c945
commit 905d355065
2 changed files with 52 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

26
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/subtype.rkt
View File

@ -66,23 +66,33 @@
(syntax/loc stx (let*/and (clauses ...)
A-last))))]))
;; kw-subtypes : (Listof (Pairof Num Num)) (Listof Keyword) (Listof Keyword)
;; -> (Option (Listof (Pairof Num Num)))
;;
;; Given function types F_s and F_t, this procedure is called to check that the
;; keyword types t-kws for F_t are subtypes of the keyword types s-kws for F_s
;; when checking that F_s <: F_t (but *not* F_t <: F_s).
;;
;; Note that in terms of width, s-kws may have more keywords (i.e., F_s accepts
;; all keywords that F_t does) but the types in s-kws must be supertypes of those
;; in t-kws (i.e., F_s domain types are at least as permissive as those of F_t).
(define (kw-subtypes* A0 t-kws s-kws)
(let loop ([A A0] [t t-kws] [s s-kws])
(and
A
(match* (t s)
[((list (Keyword: kt tt rt) rest-t) (list (Keyword: ks ts rs) rest-s))
[((cons (Keyword: kt tt rt) rest-t) (cons (Keyword: ks ts rs) rest-s))
(cond [(eq? kt ks)
(and ;; if s is optional, t must be as well
(or rs (not rt))
(and ;; if t is optional, s must be as well
(or rt (not rs))
(loop (subtype* A tt ts) rest-t rest-s))]
;; extra keywords in t are ok
;; optional extra keywords in s are ok
;; we just ignore them
[(keyword<? kt ks) (loop A rest-t s)]
;; extra keywords in s are a problem
[(and (not rs) (keyword<? ks kt)) (loop A t rest-s)]
;; extra keywords in t are a problem
[else #f])]
;; no more keywords to satisfy
[(_ '()) A]
;; no more keywords to satisfy, the rest in t must be optional
[('() _) (and (andmap (match-lambda [(Keyword: _ _ rs) (not rs)]) s) A)]
;; we failed to satisfy all the keyword
[(_ _) #f]))))

34
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/subtype-tests.rkt
View File

@ -253,4 +253,38 @@
[FAIL (make-ListDots (-box (make-F 'a)) 'a) (-lst (-box Univ))]
[(make-ListDots (-> -Symbol (make-F 'a)) 'a) (-lst (-> -Symbol Univ))]
;; keyword function types
[(->key #:x -Symbol #f Univ) (->key Univ)]
[FAIL (->key #:x -Symbol #t Univ) (->key Univ)]
[FAIL (->key Univ) (->key #:x -Symbol #t Univ)]
[(->key #:x -Symbol #f #:y -Symbol #f Univ) (->key Univ)]
[FAIL (->key #:x -Symbol #f #:y -Symbol #t Univ) (->key Univ)]
[(->key #:x -Symbol #f #:y -Symbol #f Univ) (->key #:x -Symbol #f Univ)]
[(->key #:x -Symbol #f #:y -Symbol #f Univ) (->key #:x -Symbol #t Univ)]
[FAIL (->key #:x -Symbol #f Univ) (->key #:x -Symbol #f #:y -Symbol #f Univ)]
[(->key #:x -Symbol #f #:y -Symbol #f Univ)
(->key #:x -Symbol #t #:y -Symbol #t Univ)]
[FAIL
(->key #:x -Symbol #t #:y -Symbol #f Univ)
(->key #:x -Symbol #f #:y -Symbol #t Univ)]
[(->key #:x (-opt -String) #f #:y -Symbol #f Univ)
(->key #:x -String #t Univ)]
[FAIL
(->key #:x -String #f #:y -Symbol #f Univ)
(->key #:x (-opt -String) #t Univ)]
[(->key -String #:x -Symbol #f #:y -Symbol #f Univ)
(->key -String #:x -Symbol #t Univ)]
[FAIL
(->key -String #:x -Symbol #f #:y -Symbol #f Univ)
(->key -Void #:x -Symbol #t Univ)]
[(->optkey -String [-String] #:x -Symbol #f #:y -Symbol #f Univ)
(->key -String #:x -Symbol #t Univ)]
[(->optkey -String [-String] #:x -Symbol #f #:y -Symbol #f Univ)
(->optkey -String [-String] #:x -Symbol #t Univ)]
[FAIL
(->optkey -String [-String] #:x -Symbol #f #:y -Symbol #f Univ)
(->optkey -String [-Void] #:x -Symbol #t Univ)]
[FAIL
(->key -String #:x -Symbol #f #:y -Symbol #f Univ)
(->optkey -String [-Void] #:x -Symbol #t Univ)]
))