From 62d3dc146634aa5b6716e988a0e906bb0a90477f Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Mon, 11 Jan 2010 20:48:26 +0000 Subject: [PATCH] Propogate expected type through `reverse'. New loop special case for `for/list'. svn: r17609 original commit: 4fa4f6fd2d814de10e84300d1da76a311bf85160 --- .../typed-scheme/fail/reverse-special.ss | 13 +++++++ .../tests/typed-scheme/succeed/for-list.ss | 8 ++++ .../tests/typed-scheme/succeed/sequences.ss | 9 +++++ .../typed-scheme/private/base-special-env.ss | 23 ++++++++++- collects/typed-scheme/typecheck/tc-app.ss | 39 ++++++++++++++++--- collects/typed-scheme/types/abbrev.ss | 12 ++++++ collects/typed-scheme/types/printer.ss | 2 + 7 files changed, 100 insertions(+), 6 deletions(-) create mode 100644 collects/tests/typed-scheme/fail/reverse-special.ss create mode 100644 collects/tests/typed-scheme/succeed/for-list.ss create mode 100644 collects/tests/typed-scheme/succeed/sequences.ss diff --git a/collects/tests/typed-scheme/fail/reverse-special.ss b/collects/tests/typed-scheme/fail/reverse-special.ss new file mode 100644 index 00000000..6fd7b667 --- /dev/null +++ b/collects/tests/typed-scheme/fail/reverse-special.ss @@ -0,0 +1,13 @@ +#; +(exn-pred 3) +#lang typed/scheme + +(ann (list 1 2 'foo) (Listof Number)) + +(ann (reverse (list 1 2 'foo)) (Listof Number)) + + + + + +(ann (reverse (list 1 2 'foo)) (List String Number Number)) diff --git a/collects/tests/typed-scheme/succeed/for-list.ss b/collects/tests/typed-scheme/succeed/for-list.ss new file mode 100644 index 00000000..716b80fd --- /dev/null +++ b/collects/tests/typed-scheme/succeed/for-list.ss @@ -0,0 +1,8 @@ +#lang typed/scheme + +(ann (for/list ([z #"foobar"]) (add1 z)) (Listof Integer)) + +(: explode (String -> (Listof Char))) +(define (explode s) + (for/list ([i s]) i)) + diff --git a/collects/tests/typed-scheme/succeed/sequences.ss b/collects/tests/typed-scheme/succeed/sequences.ss new file mode 100644 index 00000000..c584ad85 --- /dev/null +++ b/collects/tests/typed-scheme/succeed/sequences.ss @@ -0,0 +1,9 @@ +#lang typed/scheme + +(ann (for ([z (list 1 2 3)]) (add1 z)) Void) +(ann (for ([z (vector 1 2 3)]) (add1 z)) Void) +(ann (for ([z "foobar"]) (string z)) Void) +(ann (for ([z #"foobar"]) (add1 z)) Void) +(ann (for ([z (open-input-string "foobar")]) (add1 z)) Void) + +(ann (for ([z (in-list (list 1 2 3))]) (add1 z)) Void) diff --git a/collects/typed-scheme/private/base-special-env.ss b/collects/typed-scheme/private/base-special-env.ss index 6f41f071..2d430d8b 100644 --- a/collects/typed-scheme/private/base-special-env.ss +++ b/collects/typed-scheme/private/base-special-env.ss @@ -76,7 +76,28 @@ (-poly (a b) (cl->* (-> (-lst a) (-val '()) (-lst a)) - (-> (-lst a) (-lst b) (-lst (*Un a b)))))) + (-> (-lst a) (-lst b) (-lst (*Un a b))))) + ;; make-sequence + [(syntax-parse (local-expand #'(for ([x '()]) x) 'expression #f) + #:context #'make-sequence + #:literals (let-values quote) + [(let-values ([_ (m-s '(_) '())]) . _) + #'m-s]) + (-poly (a) + (let ([seq-vals + (lambda ([a a]) + (-values (list + (-> Univ a) + (-> Univ Univ) + Univ + (-> Univ Univ) + (-> a Univ) + (-> Univ a Univ))))]) + (cl->* (-> Univ (-lst a) (seq-vals)) + (-> Univ (-vec a) (seq-vals)) + (-> Univ -String (seq-vals -Char)) + (-> Univ -Bytes (seq-vals -Nat)) + (-> Univ -Input-Port (seq-vals -Nat)))))]) diff --git a/collects/typed-scheme/typecheck/tc-app.ss b/collects/typed-scheme/typecheck/tc-app.ss index 834a05ac..4b002114 100644 --- a/collects/typed-scheme/typecheck/tc-app.ss +++ b/collects/typed-scheme/typecheck/tc-app.ss @@ -174,14 +174,14 @@ (define (let-loop-check form lp actuals args body expected) (syntax-parse #`(#,args #,body #,actuals) - #:literals (#%plain-app if null? pair?) + #:literals (#%plain-app if null? pair? null) [((val acc ...) ((~and inner-body (if (#%plain-app (~or pair? null?) val*) thn els))) (actual actuals ...)) - #:fail-unless + #:when (and (free-identifier=? #'val #'val*) (ormap (lambda (a) (find-annotation #'inner-body a)) - (syntax->list #'(acc ...)))) #f + (syntax->list #'(acc ...)))) (let* ([ts1 (generalize (tc-expr/t #'actual))] [ann-ts (for/list ([a (in-syntax #'(acc ...))] [ac (in-syntax #'(actuals ...))]) @@ -195,6 +195,24 @@ ;; then check that the function typechecks with the inferred types (tc/rec-lambda/check form args body lp ts expected) expected)] + ;; special case `for/list' + [((val acc ...) + ((~and inner-body (if e1 e2 e3:id))) + (null actuals ...)) + #:when (free-identifier=? #'val #'e3) + (let ([ts (for/list ([ac (syntax->list #'(actuals ...))] + [f (syntax->list #'(acc ...))]) + (or + (type-annotation f #:infer #t) + (generalize (tc-expr/t ac))))] + [acc-ty (or + (type-annotation #'val #:infer #t) + (match expected + [(tc-result1: (and t (Listof: _))) t] + [_ #f]) + (generalize (-val '())))]) + (tc/rec-lambda/check form args body lp (cons acc-ty ts) expected) + expected)] ;; special case when argument needs inference [_ (let ([ts (for/list ([ac (syntax->list actuals)] @@ -407,7 +425,7 @@ (syntax-parse form #:literals (#%plain-app #%plain-lambda letrec-values quote values apply k:apply not list list* call-with-values do-make-object make-object cons - andmap ormap) + andmap ormap reverse) ;; call-with-values [(#%plain-app call-with-values prod con) (match (tc/funapp #'prod #'() (single-value #'prod) null #f) @@ -517,7 +535,7 @@ ;; special case for `list' [(#%plain-app list . args) (begin - ;(printf "calling list: ~a ~a~n" (syntax->datum #'args) (Type? expected)) + ;(printf "calling list: ~a ~a~n" (syntax->datum #'args) expected) (match expected [(tc-result1: (Mu: var (Union: (or (list (Pair: elem-ty (F: var)) (Value: '())) @@ -543,6 +561,17 @@ (match-let* ([(list last tys-r ...) (reverse (map tc-expr/t (syntax->list #'args)))] [tys (reverse tys-r)]) (ret (foldr make-Pair last tys)))] + ;; special case for `reverse' to propogate expected type info + [(#%plain-app reverse arg) + #:when expected + (match expected + [(tc-result1: (Listof: _)) + (tc-expr/check #'arg expected)] + [(tc-result1: (List: ts)) + (tc-expr/check #'arg (ret (-Tuple (reverse ts)))) + expected] + [_ + (tc/funapp #'reverse #'(arg) (single-value #'reverse) (list (single-value #'arg)) expected)])] ;; inference for ((lambda [(#%plain-app (#%plain-lambda (x ...) . body) args ...) #:fail-unless (= (length (syntax->list #'(x ...))) diff --git a/collects/typed-scheme/types/abbrev.ss b/collects/typed-scheme/types/abbrev.ss index 9b1266df..ee4ffb99 100644 --- a/collects/typed-scheme/types/abbrev.ss +++ b/collects/typed-scheme/types/abbrev.ss @@ -50,6 +50,18 @@ [else #f])] [_ #f])) +(define-match-expander Listof: + (lambda (stx) + (syntax-parse stx + [(_ elem-pat) + #'(Mu: var (Union: (list (Value: '()) (Pair: elem-pat (F: var)))))]))) + +(define-match-expander List: + (lambda (stx) + (syntax-parse stx + [(_ elem-pats) + #'(app untuple elem-pats)]))) + (d/c (-result t [f -no-lfilter] [o -no-lobj]) (c:->* (Type/c) (LFilterSet? LatentObject?) Result?) diff --git a/collects/typed-scheme/types/printer.ss b/collects/typed-scheme/types/printer.ss index b39ccfdb..8763f202 100644 --- a/collects/typed-scheme/types/printer.ss +++ b/collects/typed-scheme/types/printer.ss @@ -138,6 +138,8 @@ [(Value: '()) null])) (match c [(Univ:) (fp "Any")] + ;; special case number until something better happens + [(Base: 'Number _) (fp "Number")] [(? has-name?) (fp "~a" (has-name? c))] ;; names are just the printed as the original syntax [(Name: stx) (fp "~a" (syntax-e stx))]