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

Accept polydots rest in TR lambda and define

Browse Source 
Also accept type variables before formals in all cases
This commit is contained in:
Asumu Takikawa 2014-02-13 15:02:42 -05:00
parent 3d177e454e
commit 35ef2f90eb
2 changed files with 31 additions and 19 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

30
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/prims.rkt
View File

@ -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)))]) (lambda (bs.ann-name ...) . #,(syntax/loc stx body)))])
#,(quasisyntax/loc stx nm)))]) #,(quasisyntax/loc stx nm)))])
bs.rhs ...))] bs.rhs ...))]
[(-let ([bn:optionally-annotated-name e] ...) [(-let vars:lambda-type-vars
vars:lambda-type-vars . rest) ([bn:optionally-annotated-name e] ...)
. rest)
(define/with-syntax (bn* ...) (define/with-syntax (bn* ...)
;; singleton names go to just the name ;; singleton names go to just the name
(for/list ([bn (in-syntax #'(bn ...))]) (for/list ([bn (in-syntax #'(bn ...))])
(if (empty? (stx-cdr bn)) (if (empty? (stx-cdr bn))
(stx-car bn) (stx-car bn)
bn))) bn)))
(template ((-lambda (bn* ...) (?@ . vars) . rest) e ...))] (template ((-lambda (?@ . vars) (bn* ...) . rest) e ...))]
[(-let . rest) [(-let . rest)
(syntax/loc stx (-let-internal . 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 #:opaque
(pattern rest:id #:attr form #'rest) (pattern rest:id #:attr form #'rest)
(pattern (rest:id : type:expr :star) (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 (define-syntax-class lambda-formals
#:attributes (opt-property kw-property erased) #: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) (define-syntax (-lambda stx)
(syntax-parse stx (syntax-parse stx
#:literals (:) #:literals (:)
[(_ formals:lambda-formals [(_ vars:maybe-lambda-type-vars
vars:maybe-lambda-type-vars formals:lambda-formals
return:return-ann return:return-ann
(~describe "body expression or definition" e) ... (~describe "body expression or definition" e) ...
(~describe "body expression" last-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:id ~! (~describe ":" :) (~describe "type" ty) body)
#'(-define nm : ty body)] #'(-define nm : ty body)]
[(define: tvars:type-variables nm:id : 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: 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) (define-syntax (-define stx)
(syntax-parse stx #:literals (:) (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) #'(: nm return.type)
#'(void))) #'(void)))
(syntax/loc stx (begin maybe-ann (define nm body)))] (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 (define/with-syntax type
(syntax/loc #'ty (All vars.type-vars ty))) (syntax/loc #'ty (All vars.type-vars ty)))
(syntax/loc stx (syntax/loc stx
(begin (begin
(: nm : type) (: nm : type)
(define nm body)))] (define nm body)))]
[(-define formals:curried-formals [(-define vars:maybe-lambda-type-vars
vars:maybe-lambda-type-vars formals:curried-formals
return:return-ann return:return-ann
body ... last-body) body ... last-body)
;; have to preprocess for the return type annotation ;; 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 (syntax-parse rhs
#:literals (-lambda) #:literals (-lambda)
[(-lambda formals . others) [(-lambda formals . others)
(template (-lambda formals (?@ . vars) . others))] (template (-lambda (?@ . vars) formals . others))]
[_ rhs])) [_ rhs]))
#`(define #,defined-id #,rhs*)])) #`(define #,defined-id #,rhs*)]))

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

@ -2137,15 +2137,18 @@
(->key Univ #:y -String #t #:z -String #f -String)] (->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)) [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)] (->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 ;; type of the function because the precise filters are hard to
;; get right in the expected result type. ;; get right in the expected result type and polymorphic types are
[tc-e ((inst (tr:lambda (x [y : A]) #:forall (A) y) String) 'a "foo") ;; 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))] #: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))] #: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 #| 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))] #:ret (ret (->opt Univ -String [-String] -String) (-FS -top -bot))]
|# |#
@ -2160,6 +2163,9 @@
;(tr:define ((g x) [y : String]) y) ;(tr:define ((g x) [y : String]) y)
(string-append ((f "foo") 'y) "bar")) (string-append ((f "foo") 'y) "bar"))
-String] -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 ;; test new :-less forms that allow fewer annotations
[tc-e (let ([x "foo"]) x) -String] [tc-e (let ([x "foo"]) x) -String]
@ -2171,9 +2177,9 @@
-String] -String]
[tc-e (let ([y 'y] [x : String "foo"]) (string-append x "bar")) [tc-e (let ([y 'y] [x : String "foo"]) (string-append x "bar"))
-String] -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))] #: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))] #:ret (ret -String (-FS -top -bot))]
[tc-e (let* ([x "foo"]) x) -String] [tc-e (let* ([x "foo"]) x) -String]
[tc-e (let* ([x : String "foo"]) (string-append x "bar")) [tc-e (let* ([x : String "foo"]) (string-append x "bar"))