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

Check function depth for parsing object indices

Browse Source 
Closes PR 14509
This commit is contained in:
Asumu Takikawa 2014-07-07 16:03:57 -04:00
parent 65368108e1
commit e62f1cb8d9
3 changed files with 114 additions and 57 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

142
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/parse-type.rkt
View File

@ -64,6 +64,16 @@
;; interp. same as above
(define current-referenced-class-parents (make-parameter #f))
;; current-arities : Parameter<(Listof Natural)>
;; Represents the stack of function arities in the potentially
;; nested function type being parsed. The stack does not include the
;; innermost function (since syntax classes can check that locally)
(define current-arities (make-parameter null))
(define-syntax-rule (with-arity arity e ...)
(parameterize ([current-arities (cons arity (current-arities))])
e ...))
(define-literal-syntax-class #:for-label car)
(define-literal-syntax-class #:for-label cdr)
(define-literal-syntax-class #:for-label colon^ (:))
@ -263,10 +273,18 @@
arg (length doms))
#:attr obj (-arg-path arg 0))
(pattern (~seq depth-idx:nat idx:nat)
#:do [(define arg (syntax-e #'idx))]
#:fail-unless (< arg (length doms))
#:do [(define arg (syntax-e #'idx))
(define depth (syntax-e #'depth-idx))]
#:fail-unless (<= depth (length (current-arities)))
(format "Index ~a used in a filter, but the use is only within ~a enclosing functions"
depth (length (current-arities)))
#:do [(define actual-arg
(if (zero? depth)
(length doms)
(list-ref (current-arities) (sub1 depth))))]
#:fail-unless (< arg actual-arg)
(format "Filter proposition's object index ~a is larger than argument length ~a"
arg (length doms))
depth actual-arg)
#:attr obj (-arg-path arg (syntax-e #'depth-idx))))
@ -400,49 +418,55 @@
[((~and dom:non-keyword-ty (~not :->^)) ...
:->^
(~and (~seq rest-dom ...) (~seq (~or _ (~between :->^ 1 +inf.0)) ...)))
(let ([doms (for/list ([d (in-syntax #'(dom ...))])
(parse-type d))])
(make-Function
(list (make-arr
doms
(parse-type (syntax/loc stx (rest-dom ...)))))))]
(define doms (syntax->list #'(dom ...)))
(with-arity (length doms)
(let ([doms (for/list ([d (in-list doms)])
(parse-type d))])
(make-Function
(list (make-arr
doms
(parse-type (syntax/loc stx (rest-dom ...))))))))]
[(~or (:->^ dom rng :colon^ latent:simple-latent-filter)
(dom :->^ rng :colon^ latent:simple-latent-filter))
;; use parse-type instead of parse-values-type because we need to add the filters from the pred-ty
(make-pred-ty (list (parse-type #'dom)) (parse-type #'rng) (attribute latent.type)
(-acc-path (attribute latent.path) (-arg-path 0)))]
(with-arity 1
(make-pred-ty (list (parse-type #'dom)) (parse-type #'rng) (attribute latent.type)
(-acc-path (attribute latent.path) (-arg-path 0))))]
[(~or (:->^ dom:non-keyword-ty ... kws:keyword-tys ... rest:non-keyword-ty ddd:star rng)
(dom:non-keyword-ty ... kws:keyword-tys ... rest:non-keyword-ty ddd:star :->^ rng))
(make-Function
(list (make-arr
(parse-types #'(dom ...))
(parse-values-type #'rng)
#:rest (parse-type #'rest)
#:kws (map force (attribute kws.Keyword)))))]
(with-arity (length (syntax->list #'(dom ...)))
(make-Function
(list (make-arr
(parse-types #'(dom ...))
(parse-values-type #'rng)
#:rest (parse-type #'rest)
#:kws (map force (attribute kws.Keyword))))))]
[(~or (:->^ dom:non-keyword-ty ... rest:non-keyword-ty :ddd/bound rng)
(dom:non-keyword-ty ... rest:non-keyword-ty :ddd/bound :->^ rng))
(let* ([bnd (syntax-e #'bound)])
(unless (bound-index? bnd)
(parse-error
#:stx #'bound
"used a type variable not bound with ... as a bound on a ..."
"variable" bnd))
(make-Function
(list
(make-arr-dots (parse-types #'(dom ...))
(parse-values-type #'rng)
(extend-tvars (list bnd)
(parse-type #'rest))
bnd))))]
(with-arity (length (syntax->list #'(dom ...)))
(let* ([bnd (syntax-e #'bound)])
(unless (bound-index? bnd)
(parse-error
#:stx #'bound
"used a type variable not bound with ... as a bound on a ..."
"variable" bnd))
(make-Function
(list
(make-arr-dots (parse-types #'(dom ...))
(parse-values-type #'rng)
(extend-tvars (list bnd)
(parse-type #'rest))
bnd)))))]
[(~or (:->^ dom:non-keyword-ty ... rest:non-keyword-ty _:ddd rng)
(dom:non-keyword-ty ... rest:non-keyword-ty _:ddd :->^ rng))
(let ([var (infer-index stx)])
(make-Function
(list
(make-arr-dots (parse-types #'(dom ...))
(parse-values-type #'rng)
(extend-tvars (list var) (parse-type #'rest))
var))))]
(with-arity (length (syntax->list #'(dom ...)))
(let ([var (infer-index stx)])
(make-Function
(list
(make-arr-dots (parse-types #'(dom ...))
(parse-values-type #'rng)
(extend-tvars (list var) (parse-type #'rest))
var)))))]
#| ;; has to be below the previous one
[(dom:expr ... :->^ rng)
(->* (parse-types #'(dom ...))
@ -450,33 +474,37 @@
;; use expr to rule out keywords
[(~or (:->^ dom:non-keyword-ty ... kws:keyword-tys ... rng)
(dom:non-keyword-ty ... kws:keyword-tys ... :->^ rng))
(let ([doms (for/list ([d (in-syntax #'(dom ...))])
(parse-type d))])
(make-Function
(list (make-arr
doms
(parse-values-type #'rng)
#:kws (map force (attribute kws.Keyword))))))]
(define doms (syntax->list #'(dom ...)))
(with-arity (length doms)
(let ([doms (for/list ([d (in-list doms)])
(parse-type d))])
(make-Function
(list (make-arr
doms
(parse-values-type #'rng)
#:kws (map force (attribute kws.Keyword)))))))]
;; This case needs to be at the end because it uses cut points to give good error messages.
[(~or (:->^ ~! dom:non-keyword-ty ... rng:expr
:colon^ (~var latent (full-latent (syntax->list #'(dom ...)))))
(dom:non-keyword-ty ... :->^ rng:expr
~! :colon^ (~var latent (full-latent (syntax->list #'(dom ...))))))
;; use parse-type instead of parse-values-type because we need to add the filters from the pred-ty
(->* (parse-types #'(dom ...))
(parse-type #'rng)
: (-FS (attribute latent.positive) (attribute latent.negative))
: (attribute latent.object))]
(with-arity (length (syntax->list #'(dom ...)))
(->* (parse-types #'(dom ...))
(parse-type #'rng)
: (-FS (attribute latent.positive) (attribute latent.negative))
: (attribute latent.object)))]
[(:->*^ mand:->*-mand opt:->*-opt rest:->*-rest rng)
(define doms (for/list ([d (attribute mand.doms)])
(parse-type d)))
(define opt-doms (for/list ([d (attribute opt.doms)])
(parse-type d)))
(opt-fn doms opt-doms (parse-values-type #'rng)
#:rest (and (attribute rest.type)
(parse-type (attribute rest.type)))
#:kws (map force (append (attribute mand.kws)
(attribute opt.kws))))]
(with-arity (length (attribute mand.doms))
(define doms (for/list ([d (attribute mand.doms)])
(parse-type d)))
(define opt-doms (for/list ([d (attribute opt.doms)])
(parse-type d)))
(opt-fn doms opt-doms (parse-values-type #'rng)
#:rest (and (attribute rest.type)
(parse-type (attribute rest.type)))
#:kws (map force (append (attribute mand.kws)
(attribute opt.kws)))))]
[:->^
(parse-error #:delayed? #t "incorrect use of -> type constructor")
Err]

18
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/parse-type-tests.rkt
View File

@ -159,6 +159,15 @@
(t:->* (list Univ) -Boolean : (-FS (-not-filter -Number 0) (-filter -Number 0)))]
[(-> Any Boolean : #:+ (! Number @ 0) #:- (Number @ 0))
(t:->* (list Univ) -Boolean : (-FS (-not-filter -Number 0) (-filter -Number 0)))]
[(-> Any (-> Any Boolean : #:+ (Number @ 1 0) #:- (! Number @ 1 0)))
(t:-> Univ
(t:->* (list Univ) -Boolean : (-FS (-filter -Number '(1 0)) (-not-filter -Number '(1 0)))))]
[(-> Any Any (-> Any Boolean : #:+ (Number @ 1 1) #:- (! Number @ 1 1)))
(t:-> Univ Univ
(t:->* (list Univ) -Boolean : (-FS (-filter -Number '(1 1)) (-not-filter -Number '(1 1)))))]
[(-> Any #:foo Any (-> Any Boolean : #:+ (Number @ 1 0) #:- (! Number @ 1 0)))
(->key Univ #:foo Univ #t
(t:->* (list Univ) -Boolean : (-FS (-filter -Number '(1 0)) (-not-filter -Number '(1 0)))))]
[(All (a b) (-> (-> a Any : #:+ b) (Listof a) (Listof b)))
(-poly (a b) (t:-> (asym-pred a Univ (-FS (-filter b 0) -top)) (-lst a) (-lst b)))]
[(All (a b) (-> (-> a Any : #:+ (! b)) (Listof a) (Listof b)))
@ -178,6 +187,10 @@
[FAIL -> #:msg "incorrect use of -> type constructor"]
[FAIL (Any -> Any #:object 0) #:msg "expected the identifier `:'"]
[FAIL (-> Any Any #:+ (String @ x)) #:msg "expected the identifier `:'"]
[FAIL (-> Any Boolean : #:+ (Number @ 1 0) #:- (! Number @ 1 0))
#:msg "Index 1 used in"]
[FAIL (-> Any (-> Any Boolean : #:+ (Number @ 1 1) #:- (! Number @ 1 1)))
#:msg "larger than argument length"]
[(Any -> Boolean : #:+ (Symbol @ not-mutated-var))
@ -210,6 +223,11 @@
(->optkey -Integer [-String] #:bar -Integer #t -Void)]
[(->* (Integer #:bar Integer) (String #:foo Integer) Void)
(->optkey -Integer [-String] #:bar -Integer #t #:foo -Integer #f -Void)]
[(->* (Any (-> Any Boolean : #:+ (String @ 1 0))) Void)
(t:-> Univ (t:->* (list Univ) -Boolean : (-FS (-filter -String '(1 0)) -top))
-Void)]
[FAIL (->* (Any (-> Any Boolean : #:+ (String @ 2 0))) Void)
#:msg "Index 2 used in"]
[(Opaque foo?) (make-Opaque #'foo?)]
;; PR 14122

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

@ -3133,6 +3133,17 @@
(define (g x) (f x))
(error "foo"))
#:msg #rx"Polymorphic function `f' could not be applied"]
;; PR 14509
[tc-e
(let ()
(: f (-> Any (-> Any Boolean : #:+ (Number @ 1 0))))
(define f (λ (x) (λ (y) (number? x))))
(: g (-> Any (-> Boolean : #:+ (Number @ 1 0))))
(define g (λ (x) (λ () (number? x))))
(void))
-Void]
)
(test-suite