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

Make parse type use literal-syntax-classes.

Browse Source 
Fixes arrows in check-syntax.
Adds actual bindings for Top and Bot filters.
Make tests give more info on failure, and change test to not use Number.
This commit is contained in:
Eric Dobson 2014-01-15 22:34:53 -08:00
parent 597ab590b4
commit 7fabf5f3fc
4 changed files with 102 additions and 119 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-types-extra.rkt
View File

@ -17,7 +17,7 @@
(define-other-types (define-other-types
-> case-> U Rec All Opaque Vector -> case-> U Rec All Opaque Vector
Parameterof List List* Class Values Instance Refinement Parameterof List List* Class Values Instance Refinement
pred Struct Struct-Type) pred Struct Struct-Type Top Bot)
(provide (rename-out [All ∀] (provide (rename-out [All ∀]
[U Un] [U Un]

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

@ -6,7 +6,7 @@
(except-in (rep type-rep object-rep filter-rep) make-arr) (except-in (rep type-rep object-rep filter-rep) make-arr)
(rename-in (types abbrev union utils filter-ops resolve) (rename-in (types abbrev union utils filter-ops resolve)
[make-arr* make-arr]) [make-arr* make-arr])
(utils tc-utils stxclass-util) (utils tc-utils stxclass-util literal-syntax-class)
syntax/stx (prefix-in c: (contract-req)) syntax/stx (prefix-in c: (contract-req))
syntax/parse unstable/sequence syntax/parse unstable/sequence
(env tvar-env type-name-env type-alias-env lexical-env index-env) (env tvar-env type-name-env type-alias-env lexical-env index-env)
@ -14,7 +14,7 @@
"parse-classes.rkt" "parse-classes.rkt"
(for-label (for-label
racket/base "../base-env/colon.rkt" racket/base "../base-env/colon.rkt"
(prefix-in t: "../base-env/base-types-extra.rkt"))) "../base-env/base-types-extra.rkt"))
(provide/cond-contract ;; Parse the given syntax as a type (provide/cond-contract ;; Parse the given syntax as a type
[parse-type (syntax? . c:-> . Type/c)] [parse-type (syntax? . c:-> . Type/c)]
@ -27,11 +27,31 @@
(provide star ddd/bound) (provide star ddd/bound)
(define-literal-set parse-type-literals (define-literal-syntax-class #:for-label car)
#:for-label (define-literal-syntax-class #:for-label cdr)
(: cons quote case-lambda values car cdr and or (define-literal-syntax-class #:for-label colon^ (:))
t:Class t:Refinement t:Instance t:List t:List* t:pred t:-> t:case-> (define-literal-syntax-class #:for-label quote)
t:Rec t:U t:All t:Opaque t:Parameter t:Vector t:Struct t:Struct-Type t:Values)) (define-literal-syntax-class #:for-label cons)
(define-literal-syntax-class #:for-label Class)
(define-literal-syntax-class #:for-label Refinement)
(define-literal-syntax-class #:for-label Instance)
(define-literal-syntax-class #:for-label List)
(define-literal-syntax-class #:for-label List*)
(define-literal-syntax-class #:for-label pred)
(define-literal-syntax-class #:for-label ->)
(define-literal-syntax-class #:for-label case->^ (case-> case-lambda))
(define-literal-syntax-class #:for-label Rec)
(define-literal-syntax-class #:for-label U)
(define-literal-syntax-class #:for-label All)
(define-literal-syntax-class #:for-label Opaque)
(define-literal-syntax-class #:for-label Parameter)
(define-literal-syntax-class #:for-label Vector)
(define-literal-syntax-class #:for-label Struct)
(define-literal-syntax-class #:for-label Struct-Type)
(define-literal-syntax-class #:for-label Values)
(define-literal-syntax-class #:for-label values)
(define-literal-syntax-class #:for-label Top)
(define-literal-syntax-class #:for-label Bot)
;; (Syntax -> Type) -> Syntax Any -> Syntax ;; (Syntax -> Type) -> Syntax Any -> Syntax
;; See `parse-type/id`. This is a curried generalization. ;; See `parse-type/id`. This is a curried generalization.
@ -43,13 +63,12 @@
;; The body of a Forall type ;; The body of a Forall type
(define-syntax-class all-body (define-syntax-class all-body
#:attributes (type) #:attributes (type)
#:literal-sets (parse-type-literals)
(pattern (type)) (pattern (type))
(pattern (~and type ((~or (~once t:->) x) ...)))) (pattern (~and type ((~or (~once :->^) x) ...))))
(define (parse-literal-alls stx) (define (parse-literal-alls stx)
(syntax-parse stx #:literal-sets (parse-type-literals) (syntax-parse stx
[(t:All (~or (vars:id ... v:id dd:ddd) (vars:id ...)) . t:all-body) [(:All^ (~or (vars:id ... v:id dd:ddd) (vars:id ...)) . t:all-body)
(define vars-list (syntax->list #'(vars ...))) (define vars-list (syntax->list #'(vars ...)))
(cons (if (attribute v) (cons (if (attribute v)
(list vars-list #'v) (list vars-list #'v)
@ -62,25 +81,23 @@
;; Parse a Forall type ;; Parse a Forall type
(define (parse-all-type stx) (define (parse-all-type stx)
;(printf "parse-all-type: ~a \n" (syntax->datum stx)) ;(printf "parse-all-type: ~a \n" (syntax->datum stx))
(syntax-parse stx #:literal-sets (parse-type-literals) (syntax-parse stx
[((~and kw t:All) (vars:id ... v:id dd:ddd) . t:all-body) [(:All^ (vars:id ... v:id dd:ddd) . t:all-body)
(when (check-duplicate-identifier (syntax->list #'(vars ... v))) (when (check-duplicate-identifier (syntax->list #'(vars ... v)))
(tc-error "All: duplicate type variable or index")) (tc-error "All: duplicate type variable or index"))
(let* ([vars (stx-map syntax-e #'(vars ...))] (let* ([vars (stx-map syntax-e #'(vars ...))]
[v (syntax-e #'v)]) [v (syntax-e #'v)])
(add-disappeared-use #'kw)
(extend-indexes v (extend-indexes v
(extend-tvars vars (extend-tvars vars
(make-PolyDots (append vars (list v)) (parse-type #'t.type)))))] (make-PolyDots (append vars (list v)) (parse-type #'t.type)))))]
[((~and kw t:All) (vars:id ...) . t:all-body) [(:All^ (vars:id ...) . t:all-body)
(when (check-duplicate-identifier (syntax->list #'(vars ...))) (when (check-duplicate-identifier (syntax->list #'(vars ...)))
(tc-error "All: duplicate type variable")) (tc-error "All: duplicate type variable"))
(let* ([vars (stx-map syntax-e #'(vars ...))]) (let* ([vars (stx-map syntax-e #'(vars ...))])
(add-disappeared-use #'kw)
(extend-tvars vars (extend-tvars vars
(make-Poly vars (parse-type #'t.type))))] (make-Poly vars (parse-type #'t.type))))]
[(t:All (_:id ...) _ _ _ ...) (tc-error "All: too many forms in body of All type")] [(:All^ (_:id ...) _ _ _ ...) (tc-error "All: too many forms in body of All type")]
[(t:All . rest) (tc-error "All: bad syntax")])) [(:All^ . rest) (tc-error "All: bad syntax")]))
(define-splicing-syntax-class keyword-tys (define-splicing-syntax-class keyword-tys
(pattern (~seq k:keyword t:expr) (pattern (~seq k:keyword t:expr)
@ -97,10 +114,9 @@
(define-syntax-class path-elem (define-syntax-class path-elem
#:description "path element" #:description "path element"
#:literal-sets (parse-type-literals) (pattern :car^
(pattern car
#:attr pe (make-CarPE)) #:attr pe (make-CarPE))
(pattern cdr (pattern :cdr^
#:attr pe (make-CdrPE))) #:attr pe (make-CdrPE)))
(define-splicing-syntax-class idx-obj (define-splicing-syntax-class idx-obj
@ -135,10 +151,9 @@
(define-syntax-class (prop doms) (define-syntax-class (prop doms)
#:description "filter proposition" #:description "filter proposition"
#:literal-sets (parse-type-literals)
#:attributes (prop) #:attributes (prop)
(pattern (~literal Top) #:attr prop -top) (pattern :Top^ #:attr prop -top)
(pattern (~literal Bot) #:attr prop -bot) (pattern :Bot^ #:attr prop -bot)
(pattern (t:expr :@ pe:path-elem ... i:idx-obj) (pattern (t:expr :@ pe:path-elem ... i:idx-obj)
#:fail-unless (< (attribute i.arg) (length doms)) #:fail-unless (< (attribute i.arg) (length doms))
(format "Filter proposition's object index ~a is larger than argument length ~a" (format "Filter proposition's object index ~a is larger than argument length ~a"
@ -188,15 +203,13 @@
(parameterize ([current-orig-stx stx]) (parameterize ([current-orig-stx stx])
(syntax-parse (syntax-parse
stx stx
#:literal-sets (parse-type-literals)
[t [t
#:declare t (3d Type/c?) #:declare t (3d Type/c?)
(attribute t.datum)] (attribute t.datum)]
[(fst . rst) [(fst . rst)
#:fail-unless (not (syntax->list #'rst)) #f #:fail-unless (not (syntax->list #'rst)) #f
(-pair (parse-type #'fst) (parse-type #'rst))] (-pair (parse-type #'fst) (parse-type #'rst))]
[((~and kw t:Class) (pos-args ...) ([fname fty . rest] ...) ([mname mty] ...)) [(:Class^ (pos-args ...) ([fname fty . rest] ...) ([mname mty] ...))
(add-disappeared-use #'kw)
(make-Class (make-Class
(parse-types #'(pos-args ...)) (parse-types #'(pos-args ...))
(map list (map list
@ -209,50 +222,40 @@
(map list (map list
(stx-map syntax-e #'(mname ...)) (stx-map syntax-e #'(mname ...))
(parse-types #'(mty ...))))] (parse-types #'(mty ...))))]
[((~and kw t:Refinement) p?:id) [(:Refinement^ p?:id)
(add-disappeared-use #'kw)
(match (lookup-type/lexical #'p?) (match (lookup-type/lexical #'p?)
[(and t (Function: (list (arr: (list dom) _ #f #f '())))) [(and t (Function: (list (arr: (list dom) _ #f #f '()))))
(make-Refinement dom #'p?)] (make-Refinement dom #'p?)]
[t (tc-error "cannot declare refinement for non-predicate ~a" t)])] [t (tc-error "cannot declare refinement for non-predicate ~a" t)])]
[((~and kw t:Struct) t) [(:Struct^ t)
(add-disappeared-use #'kw)
(let ([v (parse-type #'t)]) (let ([v (parse-type #'t)])
(match (resolve v) (match (resolve v)
[(and s (? Struct?)) (make-StructTop s)] [(and s (? Struct?)) (make-StructTop s)]
[_ (tc-error/delayed "Argument to Struct must be a structure type, got ~a" v) [_ (tc-error/delayed "Argument to Struct must be a structure type, got ~a" v)
(Un)]))] (Un)]))]
[((~and kw t:Struct-Type) t) [(:Struct-Type^ t)
(add-disappeared-use #'kw)
(define v (parse-type #'t)) (define v (parse-type #'t))
(match (resolve v) (match (resolve v)
[(? Struct? s) (make-StructType s)] [(? Struct? s) (make-StructType s)]
[_ (tc-error/delayed "Argument to Struct-Type must be a structure type, got ~a" v) [_ (tc-error/delayed "Argument to Struct-Type must be a structure type, got ~a" v)
(Un)])] (Un)])]
[((~and kw t:Instance) t) [(:Instance^ t)
(add-disappeared-use #'kw)
(let ([v (parse-type #'t)]) (let ([v (parse-type #'t)])
(if (not (or (Mu? v) (Class? v) (Union? v) (Error? v))) (if (not (or (Mu? v) (Class? v) (Union? v) (Error? v)))
(begin (tc-error/delayed "Argument to Instance must be a class type, got ~a" v) (begin (tc-error/delayed "Argument to Instance must be a class type, got ~a" v)
(make-Instance (Un))) (make-Instance (Un)))
(make-Instance v)))] (make-Instance v)))]
[((~and kw t:List) ts ...) [(:List^ ts ...)
(add-disappeared-use #'kw)
(parse-list-type stx)] (parse-list-type stx)]
[((~and kw t:List*) ts ... t) [(:List*^ ts ... t)
(add-disappeared-use #'kw)
(-Tuple* (parse-types #'(ts ...)) (parse-type #'t))] (-Tuple* (parse-types #'(ts ...)) (parse-type #'t))]
[((~and kw t:Vector) ts ...) [(:Vector^ ts ...)
(add-disappeared-use #'kw)
(make-HeterogeneousVector (parse-types #'(ts ...)))] (make-HeterogeneousVector (parse-types #'(ts ...)))]
[((~and kw cons) fst rst) [(:cons^ fst rst)
(add-disappeared-use #'kw)
(-pair (parse-type #'fst) (parse-type #'rst))] (-pair (parse-type #'fst) (parse-type #'rst))]
[((~and kw t:pred) t) [(:pred^ t)
(add-disappeared-use #'kw)
(make-pred-ty (parse-type #'t))] (make-pred-ty (parse-type #'t))]
[((~and kw (~or case-lambda t:case->)) tys ...) [(:case->^ tys ...)
(add-disappeared-use #'kw)
(make-Function (make-Function
(for/list ([ty (in-syntax #'(tys ...))]) (for/list ([ty (in-syntax #'(tys ...))])
(let ([t (parse-type ty)]) (let ([t (parse-type ty)])
@ -261,13 +264,11 @@
[_ (tc-error/stx [_ (tc-error/stx
ty ty
"Component of case-lambda type was not a function clause")]))))] "Component of case-lambda type was not a function clause")]))))]
#;[((~and kw t:Vectorof) t) #;[(:Vectorof^ t)
(add-disappeared-use #'kw)
(make-Vector (parse-type #'t))] (make-Vector (parse-type #'t))]
[((~and kw t:Rec) x:id t) [(:Rec^ x:id t)
(let* ([var (syntax-e #'x)] (let* ([var (syntax-e #'x)]
[tvar (make-F var)]) [tvar (make-F var)])
(add-disappeared-use #'kw)
(extend-tvars (list var) (extend-tvars (list var)
(let ([t* (parse-type #'t)]) (let ([t* (parse-type #'t)])
;; is t in a productive position? ;; is t in a productive position?
@ -289,57 +290,47 @@
(if (memq var (fv t*)) (if (memq var (fv t*))
(make-Mu var t*) (make-Mu var t*)
t*))))] t*))))]
[((~and kw t:U) ts ...) [(:U^ ts ...)
(add-disappeared-use #'kw)
(apply Un (parse-types #'(ts ...)))] (apply Un (parse-types #'(ts ...)))]
[((~and kw quote) t) [(:quote^ t)
(add-disappeared-use #'kw)
(parse-quoted-type #'t)] (parse-quoted-type #'t)]
[((~and kw t:All) . rest) [(:All^ . rest)
(parse-all-type stx)] (parse-all-type stx)]
[((~and kw t:Opaque) p?:id) [(:Opaque^ p?:id)
(add-disappeared-use #'kw)
(make-Opaque #'p?)] (make-Opaque #'p?)]
[((~and kw t:Parameter) t) [(:Parameter^ t)
(let ([ty (parse-type #'t)]) (let ([ty (parse-type #'t)])
(add-disappeared-use #'kw)
(-Param ty ty))] (-Param ty ty))]
[((~and kw t:Parameter) t1 t2) [(:Parameter^ t1 t2)
(add-disappeared-use #'kw)
(-Param (parse-type #'t1) (parse-type #'t2))] (-Param (parse-type #'t1) (parse-type #'t2))]
;; curried function notation ;; curried function notation
[((~and dom:non-keyword-ty (~not t:->)) ... [((~and dom:non-keyword-ty (~not :->^)) ...
(~and kw t:->) :->^
(~and (~seq rest-dom ...) (~seq (~or _ (~between t:-> 1 +inf.0)) ...))) (~and (~seq rest-dom ...) (~seq (~or _ (~between :->^ 1 +inf.0)) ...)))
(add-disappeared-use #'kw)
(let ([doms (for/list ([d (in-syntax #'(dom ...))]) (let ([doms (for/list ([d (in-syntax #'(dom ...))])
(parse-type d))]) (parse-type d))])
(make-Function (make-Function
(list (make-arr (list (make-arr
doms doms
(parse-type (syntax/loc stx (rest-dom ...)))))))] (parse-type (syntax/loc stx (rest-dom ...)))))))]
[(dom (~and kw t:->) rng : latent:simple-latent-filter) [(dom :->^ rng : latent:simple-latent-filter)
(add-disappeared-use #'kw)
;; use parse-type instead of parse-values-type because we need to add the filters from the pred-ty ;; 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) 0 (attribute latent.path))] (make-pred-ty (list (parse-type #'dom)) (parse-type #'rng) (attribute latent.type) 0 (attribute latent.path))]
[(dom ... (~and kw t:->) rng [(dom ... :->^ rng
: ~! (~var latent (full-latent (syntax->list #'(dom ...))))) : ~! (~var latent (full-latent (syntax->list #'(dom ...)))))
(add-disappeared-use #'kw)
;; use parse-type instead of parse-values-type because we need to add the filters from the pred-ty ;; use parse-type instead of parse-values-type because we need to add the filters from the pred-ty
(->* (parse-types #'(dom ...)) (->* (parse-types #'(dom ...))
(parse-type #'rng) (parse-type #'rng)
: (-FS (attribute latent.positive) (attribute latent.negative)) : (-FS (attribute latent.positive) (attribute latent.negative))
: (attribute latent.object))] : (attribute latent.object))]
[(dom:non-keyword-ty ... rest:non-keyword-ty ddd:star kws:keyword-tys ... (~and kw t:->) rng) [(dom:non-keyword-ty ... rest:non-keyword-ty ddd:star kws:keyword-tys ... :->^ rng)
(add-disappeared-use #'kw)
(make-Function (make-Function
(list (make-arr (list (make-arr
(parse-types #'(dom ...)) (parse-types #'(dom ...))
(parse-values-type #'rng) (parse-values-type #'rng)
#:rest (parse-type #'rest) #:rest (parse-type #'rest)
#:kws (attribute kws.Keyword))))] #:kws (attribute kws.Keyword))))]
[(dom:non-keyword-ty ... rest:non-keyword-ty :ddd/bound (~and kw t:->) rng) [(dom:non-keyword-ty ... rest:non-keyword-ty :ddd/bound :->^ rng)
(add-disappeared-use #'kw)
(let* ([bnd (syntax-e #'bound)]) (let* ([bnd (syntax-e #'bound)])
(unless (bound-index? bnd) (unless (bound-index? bnd)
(tc-error/stx #'bound (tc-error/stx #'bound
@ -352,8 +343,7 @@
(extend-tvars (list bnd) (extend-tvars (list bnd)
(parse-type #'rest)) (parse-type #'rest))
bnd))))] bnd))))]
[(dom:non-keyword-ty ... rest:non-keyword-ty _:ddd (~and kw t:->) rng) [(dom:non-keyword-ty ... rest:non-keyword-ty _:ddd :->^ rng)
(add-disappeared-use #'kw)
(let ([var (infer-index stx)]) (let ([var (infer-index stx)])
(make-Function (make-Function
(list (list
@ -362,13 +352,11 @@
(extend-tvars (list var) (parse-type #'rest)) (extend-tvars (list var) (parse-type #'rest))
var))))] var))))]
#| ;; has to be below the previous one #| ;; has to be below the previous one
[(dom:expr ... (~and kw t:->) rng) [(dom:expr ... :->^ rng)
(add-disappeared-use #'kw)
(->* (parse-types #'(dom ...)) (->* (parse-types #'(dom ...))
(parse-values-type #'rng))] |# (parse-values-type #'rng))] |#
;; use expr to rule out keywords ;; use expr to rule out keywords
[(dom:non-keyword-ty ... kws:keyword-tys ... (~and kw t:->) rng) [(dom:non-keyword-ty ... kws:keyword-tys ... :->^ rng)
(add-disappeared-use #'kw)
(let ([doms (for/list ([d (in-syntax #'(dom ...))]) (let ([doms (for/list ([d (in-syntax #'(dom ...))])
(parse-type d))]) (parse-type d))])
(make-Function (make-Function
@ -392,14 +380,14 @@
=> =>
(lambda (t) (lambda (t)
;(printf "found a type alias ~a\n" #'id) ;(printf "found a type alias ~a\n" #'id)
(add-disappeared-use #'id) (add-disappeared-use (syntax-local-introduce #'id))
t)] t)]
;; if it's a type name, we just use the name ;; if it's a type name, we just use the name
[(lookup-type-name #'id (lambda () #f)) [(lookup-type-name #'id (lambda () #f))
(add-disappeared-use #'id) (add-disappeared-use (syntax-local-introduce #'id))
;(printf "found a type name ~a\n" #'id) ;(printf "found a type name ~a\n" #'id)
(make-Name #'id)] (make-Name #'id)]
[(free-identifier=? #'id #'t:->) [(free-identifier=? #'id #'->)
(tc-error/delayed "Incorrect use of -> type constructor") (tc-error/delayed "Incorrect use of -> type constructor")
Err] Err]
[else [else
@ -407,17 +395,15 @@
"Unbound type name ~a" "Unbound type name ~a"
(syntax-e #'id)) (syntax-e #'id))
Err])] Err])]
[(t:Opaque . rest) [(:Opaque^ . rest)
(tc-error "Opaque: bad syntax")] (tc-error "Opaque: bad syntax")]
[(t:U . rest) [(:U^ . rest)
(tc-error "Union: bad syntax")] (tc-error "Union: bad syntax")]
#;[(t:Vectorof . rest) #;[(:Vectorof^ . rest)
(tc-error "Vectorof: bad syntax")] (tc-error "Vectorof: bad syntax")]
[((~and (~datum mu) t:Rec) . rest) [(:Rec^ . rest)
(tc-error "mu: bad syntax")]
[(t:Rec . rest)
(tc-error "Rec: bad syntax")] (tc-error "Rec: bad syntax")]
[(t ... t:-> . rest) [(t ... :->^ . rest)
(tc-error "->: bad syntax")] (tc-error "->: bad syntax")]
[(id arg args ...) [(id arg args ...)
(let loop (let loop
@ -454,9 +440,8 @@
;; Parse a (List ...) type ;; Parse a (List ...) type
(define (parse-list-type stx) (define (parse-list-type stx)
(parameterize ([current-orig-stx stx]) (parameterize ([current-orig-stx stx])
(syntax-parse stx #:literal-sets (parse-type-literals) (syntax-parse stx
[((~and kw t:List) tys ... dty :ddd/bound) [(:List^ tys ... dty :ddd/bound)
(add-disappeared-use #'kw)
(let ([var (syntax-e #'bound)]) (let ([var (syntax-e #'bound)])
(unless (bound-index? var) (unless (bound-index? var)
(if (bound-tvar? var) (if (bound-tvar? var)
@ -467,25 +452,22 @@
(extend-tvars (list var) (extend-tvars (list var)
(parse-type #'dty)) (parse-type #'dty))
var)))] var)))]
[((~and kw t:List) tys ... dty _:ddd) [(:List^ tys ... dty _:ddd)
(add-disappeared-use #'kw)
(let ([var (infer-index stx)]) (let ([var (infer-index stx)])
(-Tuple* (parse-types #'(tys ...)) (-Tuple* (parse-types #'(tys ...))
(make-ListDots (make-ListDots
(extend-tvars (list var) (extend-tvars (list var)
(parse-type #'dty)) (parse-type #'dty))
var)))] var)))]
[((~and kw t:List) tys ...) [(:List^ tys ...)
(add-disappeared-use #'kw)
(-Tuple (parse-types #'(tys ...)))]))) (-Tuple (parse-types #'(tys ...)))])))
;; Syntax -> Type ;; Syntax -> Type
;; Parse a (Values ...) type ;; Parse a (Values ...) type
(define (parse-values-type stx) (define (parse-values-type stx)
(parameterize ([current-orig-stx stx]) (parameterize ([current-orig-stx stx])
(syntax-parse stx #:literal-sets (parse-type-literals) (syntax-parse stx
[((~and kw (~or t:Values values)) tys ... dty :ddd/bound) [((~or :Values^ :values^) tys ... dty :ddd/bound)
(add-disappeared-use #'kw)
(let ([var (syntax-e #'bound)]) (let ([var (syntax-e #'bound)])
(unless (bound-index? var) (unless (bound-index? var)
(if (bound-tvar? var) (if (bound-tvar? var)
@ -495,23 +477,20 @@
(extend-tvars (list var) (extend-tvars (list var)
(parse-type #'dty)) (parse-type #'dty))
var))] var))]
[((~and kw (~or t:Values values)) tys ... dty _:ddd) [((~or :Values^ :values^) tys ... dty _:ddd)
(add-disappeared-use #'kw)
(let ([var (infer-index stx)]) (let ([var (infer-index stx)])
(-values-dots (parse-types #'(tys ...)) (-values-dots (parse-types #'(tys ...))
(extend-tvars (list var) (extend-tvars (list var)
(parse-type #'dty)) (parse-type #'dty))
var))] var))]
[((~and kw (~or t:Values values)) tys ...) [((~or :Values^ :values^) tys ...)
(add-disappeared-use #'kw)
(-values (parse-types #'(tys ...)))] (-values (parse-types #'(tys ...)))]
[t [t
(-values (list (parse-type #'t)))]))) (-values (list (parse-type #'t)))])))
(define (parse-tc-results stx) (define (parse-tc-results stx)
(syntax-parse stx #:literal-sets (parse-type-literals) (syntax-parse stx
[((~and kw values) t ...) [(:values^ t ...)
(add-disappeared-use #'kw)
(ret (parse-types #'(t ...)) (ret (parse-types #'(t ...))
(stx-map (lambda (x) (make-NoFilter)) #'(t ...)) (stx-map (lambda (x) (make-NoFilter)) #'(t ...))
(stx-map (lambda (x) (make-NoObject)) #'(t ...)))] (stx-map (lambda (x) (make-NoObject)) #'(t ...)))]

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

@ -44,12 +44,16 @@
(quasisyntax/loc (quasisyntax/loc
stx stx
(test-case #,(format "~a" (syntax->datum #'ty-stx)) (test-case #,(format "~a" (syntax->datum #'ty-stx))
(unless (define-values (expected actual same?)
(phase1-phase0-eval (phase1-phase0-eval
(parameterize ([current-tvars tvar-env] (parameterize ([current-tvars tvar-env]
[delay-errors? #f]) [delay-errors? #f])
#`#,(type-equal? (parse-type (quote-syntax ty-stx)) ty-val))) (define expected ty-val)
(fail-check "Unequal types"))))])) (define actual (parse-type (quote-syntax ty-stx)))
#`(values #,expected #,actual #,(type-equal? actual expected)))))
(unless same?
(with-check-info (['expected expected] ['actual actual])
(fail-check "Unequal types")))))]))
(define-syntax pt-tests (define-syntax pt-tests
(syntax-rules () (syntax-rules ()

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

@ -1779,14 +1779,14 @@
;; written by the user ;; written by the user
[tc-e [tc-e
(let () (let ()
(: f (Any -> (Any -> Boolean : #:+ (Number @ 1 0) (: f (Any -> (Any -> Boolean : #:+ (Symbol @ 1 0)
#:- (! Number @ 1 0)) #:- (! Symbol @ 1 0))
: #:+ Top #:- Bot)) : #:+ Top #:- Bot))
(define f (λ (x) (λ (y) (number? x)))) (define f (λ (x) (λ (y) (symbol? x))))
(: b (U Number String)) (: b (U Symbol String))
(define b 5) (define b 'sym)
(define g (f b)) (define g (f b))
(if (g "foo") (add1 b) 3) (if (g "foo") (symbol->string b) "str")
(void)) (void))
;; type doesn't really matter, just make sure it typechecks ;; type doesn't really matter, just make sure it typechecks
-Void] -Void]