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

support `map' over multiple ListDots with the same bound

Browse Source 
- also support ListDots + Listof (map errors when not same length)

original commit: 0c7c722e16cd9f6e3e88deaa45cb681337021078
This commit is contained in:
Sam Tobin-Hochstadt 2010-06-21 17:38:05 -04:00
parent 84247a1882
commit f50aa4917a
2 changed files with 30 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
collects/tests/typed-scheme/succeed/list-dots.rkt
View File

@ -1,5 +1,7 @@
#lang typed/racket
;; tests for the new iteration of ...
(: f (All (a ...) ((List a ...) -> (List a ... a))))
(define (f x) x)
@ -19,3 +21,15 @@
(: h4 (All (a ...) (a ... -> Number)))
(define (h4 . x) (length x))
(: i (All (a ...) (List a ...) (a ... -> Number) -> Number))
(define (i xs f) (apply f xs))
(: i2 (All (a ...) (List a ...) (Any * -> Number) -> Number))
(define (i2 xs f) (apply f xs))
(: i3 (All (a ...) (List a ...) (List a ...) ((Pairof a a) ... -> Number) -> Number))
(define (i3 xs ys f) (apply f (map cons xs ys)))
(: i4 (All (a ...) (List a ...) (Listof Number) ((Pairof a Number) ... -> Number) -> Number))
(define (i4 xs ys f) (apply f (map cons xs ys)))

25
collects/typed-scheme/typecheck/tc-app.rkt
View File

@ -625,21 +625,28 @@
(check-do-make-object #'cl #'args #'() #'())]
[(#%plain-app do-make-object cl (#%plain-app list . pos-args) (#%plain-app list (#%plain-app cons 'names named-args) ...))
(check-do-make-object #'cl #'pos-args #'(names ...) #'(named-args ...))]
[(#%plain-app (~literal map) f arg)
(match (single-value #'arg)
[(#%plain-app (~literal map) f arg0 arg ...)
(match* ((single-value #'arg0) (map single-value (syntax->list #'(arg ...))))
;; if the argument is a ListDots
[(tc-result1: (ListDots: t bound))
(match (extend-tvars (list bound)
[((tc-result1: (ListDots: t0 bound0))
(list (tc-result1: (or (and (ListDots: t bound) (app (λ _ #f) var))
;; a devious hack - just generate #f so the test below succeeds
;; have to explicitly bind `var' since otherwise `var' appears on only one side of the or
;; NOTE: safe to include these, `map' will error if any list is not the same length as all the others
(and (Listof: t var) (app (λ _ #f) bound))))
...))
(=> fail)
(unless (for/and ([b bound]) (or (not b) (eq? bound0 b))) (fail))
(match (extend-tvars (list bound0)
;; just check that the function applies successfully to the element type
(tc/funapp #'f #'(arg) (tc-expr #'f) (list (ret t)) expected))
[(tc-result1: t) (ret (make-ListDots t bound))]
(tc/funapp #'f #'(arg0 arg ...) (tc-expr #'f) (cons (ret t0) (map ret t)) expected))
[(tc-result1: t) (ret (make-ListDots t bound0))]
[(tc-results: ts)
(tc-error/expr #:return (ret (Un))
"Expected one value, but got ~a" (-values ts))])]
;; otherwise, if it's not a ListDots, defer to the regular function typechecking
[res
(tc/funapp #'map #'(f arg) (single-value #'map) (list (tc-expr #'f) res) expected)])]
[(res0 res)
(tc/funapp #'map #'(f arg0 arg ...) (single-value #'map) (list* (tc-expr #'f) res0 res) expected)])]
;; ormap/andmap of ... argument
[(#%plain-app (~and fun (~or (~literal andmap) (~literal ormap))) f arg)
;; check the arguments