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

Fix typechecking of andmap/ormap on dotted lists.

Browse Source 
original commit: c60b3d8b03cc095796f634c81ba04567bf192ec3
This commit is contained in:
Eric Dobson 2014-05-21 23:41:41 -07:00
parent f97ef41153
commit 231026ac8e
2 changed files with 21 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-list.rkt
View File

@ -22,6 +22,12 @@
#:for-label
(reverse k:reverse list list* cons map andmap ormap))
(define-syntax-class boolmap
#:literal-sets (list-literals)
#:attributes (default)
(pattern andmap #:attr default #t)
(pattern ormap #:attr default #f))
(define-tc/app-syntax-class (tc/app-list expected)
#:literal-sets (list-literals)
(pattern (~and form (map f arg0 arg ...))
@ -58,17 +64,18 @@
;; TODO fix double typechecking
[(res0 res) (tc/app-regular #'form expected)]))
;; ormap/andmap of ... argument
(pattern (~and form ((~or andmap ormap) f arg))
(match-let* ([arg-ty (single-value #'arg)]
(pattern (~and form (m:boolmap f arg))
(match-let* ([arg-ty (tc-expr/t #'arg)]
[ft (tc-expr #'f)])
(match (match arg-ty
;; if the argument is a ListDots
[(tc-result1: (ListDots: t bound))
[(ListDots: t bound)
;; just check that the function applies successfully to the element type
(tc/funapp #'f #'(arg) ft (list (ret (substitute Univ bound t))) expected)]
(extend-tvars (list bound)
(tc/funapp #'f #'(arg) ft (list (ret t)) expected))]
;; otherwise ...
[_ #f])
[(tc-result1: t) (ret (Un (-val #f) t))]
[(tc-result1: t) (ret (Un (-val (attribute m.default)) t))]
;; if it's not a ListDots, defer to the regular function typechecking
;; TODO fix double typechecking
[_ (tc/app-regular #'form expected)])))

9
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt
View File

@ -2978,6 +2978,15 @@
#:ret (ret (-polydots (a ...) (->... (list) (a a) (-values-dots (list (t:-> -Symbol -Symbol)) a 'a))))
#:expected (ret (-polydots (a ...) (->... (list) (a a) (-values-dots (list (t:-> -Symbol -Symbol)) a 'a))))]
[tc-err
(lambda xs (andmap (lambda: ([x : (Vectorof Any)]) x) xs))
#:ret (ret (-polydots (a ...) (->... (list) ((-vec a) a) (t:Un (-val #f) (-vec Univ)))))
#:expected (ret (-polydots (a ...) (->... (list) ((-vec a) a) (t:Un (-val #f) (-vec Univ)))))]
[tc-err
(lambda xs (andmap (lambda: ([x : #f]) x) xs))
#:ret (ret (-polydots (a ...) (->... (list) ((-val #f) a) (-val #f))))
#:expected (ret (-polydots (a ...) (->... (list) ((-val #f) a) (-val #f))))]
)
(test-suite
"tc-literal tests"