From 35ef2f90ebef94c8f7c4e46fc43c03b6ce329a41 Mon Sep 17 00:00:00 2001 From: Asumu Takikawa Date: Thu, 13 Feb 2014 15:02:42 -0500 Subject: [PATCH] Accept polydots rest in TR lambda and define Also accept type variables before formals in all cases --- .../typed-racket/base-env/prims.rkt | 30 +++++++++++-------- .../unit-tests/typecheck-tests.rkt | 20 ++++++++----- 2 files changed, 31 insertions(+), 19 deletions(-) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/prims.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/prims.rkt index 83fa978a1c..2b61935e28 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/prims.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/prims.rkt @@ -472,15 +472,16 @@ This file defines two sorts of primitives. All of them are provided into any mod (lambda (bs.ann-name ...) . #,(syntax/loc stx body)))]) #,(quasisyntax/loc stx nm)))]) bs.rhs ...))] - [(-let ([bn:optionally-annotated-name e] ...) - vars:lambda-type-vars . rest) + [(-let vars:lambda-type-vars + ([bn:optionally-annotated-name e] ...) + . rest) (define/with-syntax (bn* ...) ;; singleton names go to just the name (for/list ([bn (in-syntax #'(bn ...))]) (if (empty? (stx-cdr bn)) (stx-car bn) bn))) - (template ((-lambda (bn* ...) (?@ . vars) . rest) e ...))] + (template ((-lambda (?@ . vars) (bn* ...) . rest) e ...))] [(-let . rest) (syntax/loc stx (-let-internal . rest))])) @@ -1188,7 +1189,12 @@ This file defines two sorts of primitives. All of them are provided into any mod #:opaque (pattern rest:id #:attr form #'rest) (pattern (rest:id : type:expr :star) - #:attr form (type-label-property #'rest #'type))) + #:attr form (type-label-property #'rest #'type)) + (pattern (rest:id : type:expr bnd:ddd/bound) + #:attr bound (attribute bnd.bound) + #:attr form (type-dotted-property + (type-label-property #'rest #'type) + (attribute bound)))) (define-syntax-class lambda-formals #:attributes (opt-property kw-property erased) @@ -1221,8 +1227,8 @@ This file defines two sorts of primitives. All of them are provided into any mod (define-syntax (-lambda stx) (syntax-parse stx #:literals (:) - [(_ formals:lambda-formals - vars:maybe-lambda-type-vars + [(_ vars:maybe-lambda-type-vars + formals:lambda-formals return:return-ann (~describe "body expression or definition" e) ... (~describe "body expression" last-e)) @@ -1258,9 +1264,9 @@ This file defines two sorts of primitives. All of them are provided into any mod [(define: nm:id ~! (~describe ":" :) (~describe "type" ty) body) #'(-define nm : ty body)] [(define: tvars:type-variables nm:id : ty body) - #'(-define nm #:forall tvars : ty body)] + #'(-define #:forall tvars nm : ty body)] [(define: tvars:type-variables (nm:id . formals:annotated-formals) : ret-ty body ...) - #'(-define (nm . formals) #:forall tvars : ret-ty body ...)])) + #'(-define #:forall tvars (nm . formals) : ret-ty body ...)])) (define-syntax (-define stx) (syntax-parse stx #:literals (:) @@ -1273,15 +1279,15 @@ This file defines two sorts of primitives. All of them are provided into any mod #'(: nm return.type) #'(void))) (syntax/loc stx (begin maybe-ann (define nm body)))] - [(-define nm:id vars:lambda-type-vars : ty body) + [(-define vars:lambda-type-vars nm:id : ty body) (define/with-syntax type (syntax/loc #'ty (All vars.type-vars ty))) (syntax/loc stx (begin (: nm : type) (define nm body)))] - [(-define formals:curried-formals - vars:maybe-lambda-type-vars + [(-define vars:maybe-lambda-type-vars + formals:curried-formals return:return-ann body ... last-body) ;; have to preprocess for the return type annotation @@ -1299,7 +1305,7 @@ This file defines two sorts of primitives. All of them are provided into any mod (syntax-parse rhs #:literals (-lambda) [(-lambda formals . others) - (template (-lambda formals (?@ . vars) . others))] + (template (-lambda (?@ . vars) formals . others))] [_ rhs])) #`(define #,defined-id #,rhs*)])) diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt index 299c051519..45bffee882 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt @@ -2137,15 +2137,18 @@ (->key Univ #:y -String #t #:z -String #f -String)] [tc-e (tr:lambda (x #:y [y : String "y"] #:z [z : String "z"]) (string-append y z)) (->key Univ #:y -String #f #:z -String #f -String)] - ;; for these next two tests, test the application instead of the + ;; for these next three tests, test the application instead of the ;; type of the function because the precise filters are hard to - ;; get right in the expected result type. - [tc-e ((inst (tr:lambda (x [y : A]) #:forall (A) y) String) 'a "foo") + ;; get right in the expected result type and polymorphic types are + ;; harder to test for equality. + [tc-e ((inst (tr:lambda #:forall (A) (x [y : A]) y) String) 'a "foo") #:ret (ret -String (-FS -top -bot))] - [tc-e ((inst (tr:lambda (x [y : A]) #:∀ (A) y) String) 'a "foo") + [tc-e ((inst (tr:lambda #:∀ (A) (x [y : A]) y) String) 'a "foo") #:ret (ret -String (-FS -top -bot))] + [tc-e ((inst (tr:lambda #:forall (A ...) (x . [rst : A ... A]) rst) String) 'a "foo") + #:ret (ret (-lst* -String) (-FS -top -bot))] #| FIXME: does not work yet, TR thinks the type variable is unbound - [tc-e (inst (tr:lambda (x [y : A] [z : String "z"]) #:forall (A) y) String) + [tc-e (inst (tr:lambda #:forall (A) (x [y : A] [z : String "z"]) y) String) #:ret (ret (->opt Univ -String [-String] -String) (-FS -top -bot))] |# @@ -2160,6 +2163,9 @@ ;(tr:define ((g x) [y : String]) y) (string-append ((f "foo") 'y) "bar")) -String] + [tc-e (let () (tr:define #:forall (A ...) (f x . [rst : A ... A]) rst) + (f 'a "b" "c")) + #:ret (ret (-lst* -String -String) (-FS -top -bot))] ;; test new :-less forms that allow fewer annotations [tc-e (let ([x "foo"]) x) -String] @@ -2171,9 +2177,9 @@ -String] [tc-e (let ([y 'y] [x : String "foo"]) (string-append x "bar")) -String] - [tc-e (let ([x : A "foo"]) #:forall (A) x) + [tc-e (let #:forall (A) ([x : A "foo"]) x) #:ret (ret -String (-FS -top -bot))] - [tc-e (let ([y 'y] [x : A "foo"]) #:forall (A) x) + [tc-e (let #:forall (A) ([y 'y] [x : A "foo"]) x) #:ret (ret -String (-FS -top -bot))] [tc-e (let* ([x "foo"]) x) -String] [tc-e (let* ([x : String "foo"]) (string-append x "bar"))