Cleaned up special cases by adding macros to reduce duplication.
original commit: 5c7ed4a21d1c77866891b2c69fb8c152e5872fca
This commit is contained in:
Eric Dobson
Sam Tobin-Hochstadt
parent
5754267aa0
commit
696b463b46
|
|
@ -18,38 +18,39 @@
|
|||
;; the main dispatching function
|
||||
;; syntax tc-results? -> tc-results?
|
||||
(define (tc/app/internal form expected)
|
||||
(or
|
||||
(tc/app-annotated form expected)
|
||||
(syntax-parse form
|
||||
[(#%plain-app .
|
||||
(~or (~reflect v (tc/app-list expected) #:attributes (check))
|
||||
(~reflect v (tc/app-apply expected) #:attributes (check))
|
||||
(~reflect v (tc/app-eq expected) #:attributes (check))
|
||||
(~reflect v (tc/app-hetero expected) #:attributes (check))
|
||||
(~reflect v (tc/app-values expected) #:attributes (check))
|
||||
(~reflect v (tc/app-keywords expected) #:attributes (check))
|
||||
(~reflect v (tc/app-objects expected) #:attributes (check))
|
||||
(~reflect v (tc/app-lambda expected) #:attributes (check))
|
||||
(~reflect v (tc/app-special expected) #:attributes (check))))
|
||||
((attribute v.check))]
|
||||
[_ #f])
|
||||
(tc/app-regular form expected)))
|
||||
(syntax-parse form
|
||||
[(#%plain-app .
|
||||
(~or (~var v (tc/app-annotated expected))
|
||||
(~reflect v (tc/app-list expected) #:attributes (check))
|
||||
(~reflect v (tc/app-apply expected) #:attributes (check))
|
||||
(~reflect v (tc/app-eq expected) #:attributes (check))
|
||||
(~reflect v (tc/app-hetero expected) #:attributes (check))
|
||||
(~reflect v (tc/app-values expected) #:attributes (check))
|
||||
(~reflect v (tc/app-keywords expected) #:attributes (check))
|
||||
(~reflect v (tc/app-objects expected) #:attributes (check))
|
||||
(~reflect v (tc/app-lambda expected) #:attributes (check))
|
||||
(~reflect v (tc/app-special expected) #:attributes (check))
|
||||
(~var v (tc/app-regular* expected))))
|
||||
((attribute v.check))]))
|
||||
|
||||
(define-syntax-class annotated-op
|
||||
(pattern i:identifier
|
||||
#:when (or (syntax-property #'i 'type-inst)
|
||||
(syntax-property #'i 'type-ascription))))
|
||||
|
||||
(define (tc/app-annotated form expected)
|
||||
(syntax-parse form
|
||||
#:literals (#%plain-app)
|
||||
;; Just do regular typechecking if we have one of these.
|
||||
[(#%plain-app rator:annotated-op . rands) (tc/app-regular form expected)]
|
||||
[_ #f]))
|
||||
|
||||
(define-syntax-class (tc/app-annotated expected)
|
||||
;; Just do regular typechecking if we have one of these.
|
||||
(pattern (~and form (rator:annotated-op . rands))
|
||||
#:attr check (lambda () (tc/app-regular #'form expected))))
|
||||
|
||||
(define-syntax-class (tc/app-regular* expected)
|
||||
(pattern form
|
||||
#:attr check (lambda () (tc/app-regular #'form expected))))
|
||||
|
||||
(define (tc/app-regular form expected)
|
||||
(syntax-parse form #:literals (#%plain-app)
|
||||
[(#%plain-app f . args)
|
||||
(syntax-parse form
|
||||
[(f . args)
|
||||
(let* ([f-ty (single-value #'f)])
|
||||
(match f-ty
|
||||
[(tc-result1:
|
||||
|
|
|
|||
|
|
@ -2,6 +2,7 @@
|
|||
|
||||
(require "../../utils/utils.rkt"
|
||||
"signatures.rkt"
|
||||
"utils.rkt"
|
||||
syntax/parse racket/match
|
||||
syntax/parse/experimental/reflect
|
||||
(typecheck signatures tc-funapp check-below tc-subst)
|
||||
|
|
@ -19,21 +20,12 @@
|
|||
(import tc-expr^ tc-apply^)
|
||||
(export tc-app-apply^)
|
||||
|
||||
(define-syntax-class (tc/app-apply* expected)
|
||||
#:attributes (check)
|
||||
#:literals (k:apply apply values)
|
||||
(define-tc/app-syntax-class (tc/app-apply expected)
|
||||
#:literals (k:apply apply values)
|
||||
(pattern ((~or apply k:apply) values e)
|
||||
#:attr check
|
||||
(lambda ()
|
||||
(match (single-value #'e)
|
||||
[(tc-result1: (ListDots: dty dbound)) (values->tc-results (make-ValuesDots null dty dbound) #f)]
|
||||
[(tc-result1: (List: ts)) (ret ts)]
|
||||
[_ (tc/apply #'values #'(e))])))
|
||||
(match (single-value #'e)
|
||||
[(tc-result1: (ListDots: dty dbound)) (values->tc-results (make-ValuesDots null dty dbound) #f)]
|
||||
[(tc-result1: (List: ts)) (ret ts)]
|
||||
[_ (tc/apply #'values #'(e))]))
|
||||
(pattern ((~or apply k:apply) f . args)
|
||||
#:attr check
|
||||
(lambda () (tc/apply #'f #'args))))
|
||||
|
||||
|
||||
(define tc/app-apply (reify-syntax-class tc/app-apply*))
|
||||
|
||||
|
||||
(tc/apply #'f #'args)))
|
||||
|
|
|
|||
|
|
@ -2,6 +2,7 @@
|
|||
|
||||
(require "../../utils/utils.rkt"
|
||||
"signatures.rkt"
|
||||
"utils.rkt"
|
||||
syntax/parse racket/match
|
||||
syntax/parse/experimental/reflect
|
||||
(typecheck signatures tc-funapp check-below)
|
||||
|
|
@ -24,20 +25,15 @@
|
|||
(pattern member) (pattern memq) (pattern memv))
|
||||
|
||||
|
||||
(define-syntax-class (tc/app-eq* expected)
|
||||
#:attributes (check)
|
||||
(define-tc/app-syntax-class (tc/app-eq expected)
|
||||
(pattern (eq?:comparator v1 v2)
|
||||
#:attr check
|
||||
(lambda ()
|
||||
;; make sure the whole expression is type correct
|
||||
(match* ((tc/funapp #'eq? #'(v1 v2) (single-value #'eq?)
|
||||
(map single-value (syntax->list #'(v1 v2))) expected)
|
||||
;; check thn and els with the eq? info
|
||||
(tc/eq #'eq? #'v1 #'v2))
|
||||
[((tc-result1: t) (tc-result1: t* f o))
|
||||
(ret t f o)]))))
|
||||
|
||||
(define tc/app-eq (reify-syntax-class tc/app-eq*))
|
||||
;; make sure the whole expression is type correct
|
||||
(match* ((tc/funapp #'eq? #'(v1 v2) (single-value #'eq?)
|
||||
(map single-value (syntax->list #'(v1 v2))) expected)
|
||||
;; check thn and els with the eq? info
|
||||
(tc/eq #'eq? #'v1 #'v2))
|
||||
[((tc-result1: t) (tc-result1: t* f o))
|
||||
(ret t f o)])))
|
||||
|
||||
|
||||
;; typecheck eq? applications
|
||||
|
|
|
|||
|
|
@ -5,6 +5,7 @@
|
|||
syntax/parse racket/match
|
||||
syntax/parse/experimental/reflect
|
||||
"signatures.rkt"
|
||||
"utils.rkt"
|
||||
;; fixme - don't need to be bound in this phase - only to make tests work
|
||||
racket/unsafe/ops
|
||||
;; end fixme
|
||||
|
|
@ -76,73 +77,60 @@
|
|||
(single-value val-e)
|
||||
(index-error i-val i-bound i-e vec-t expected name)]))
|
||||
|
||||
(define-syntax-class (tc/app-hetero* expected)
|
||||
#:attributes (check)
|
||||
#:literals (vector-ref unsafe-vector-ref unsafe-vector*-ref
|
||||
vector-set! unsafe-vector-set! unsafe-vector*-set!
|
||||
unsafe-struct-ref unsafe-struct*-ref
|
||||
unsafe-struct-set! unsafe-struct*-set!
|
||||
vector-immutable vector)
|
||||
(define-tc/app-syntax-class (tc/app-hetero expected)
|
||||
#:literals (vector-ref unsafe-vector-ref unsafe-vector*-ref
|
||||
vector-set! unsafe-vector-set! unsafe-vector*-set!
|
||||
unsafe-struct-ref unsafe-struct*-ref
|
||||
unsafe-struct-set! unsafe-struct*-set!
|
||||
vector-immutable vector)
|
||||
(pattern ((~or unsafe-struct-ref unsafe-struct*-ref) struct:expr index:expr)
|
||||
#:attr check
|
||||
(lambda ()
|
||||
(match (single-value #'struct)
|
||||
[(tc-result1: (and struct-t (app resolve (Struct: _ _ (list (fld: flds _ _) ...) _ _ _ _ _))))
|
||||
(tc/hetero-ref #'index flds struct-t expected "struct")]
|
||||
[s-ty #f])))
|
||||
(match (single-value #'struct)
|
||||
[(tc-result1: (and struct-t (app resolve (Struct: _ _ (list (fld: flds _ _) ...) _ _ _ _ _))))
|
||||
(tc/hetero-ref #'index flds struct-t expected "struct")]
|
||||
[s-ty #f]))
|
||||
;; vector-ref on het vectors
|
||||
(pattern ((~or vector-ref unsafe-vector-ref unsafe-vector*-ref) vec:expr index:expr)
|
||||
#:attr check
|
||||
(lambda ()
|
||||
(match (single-value #'vec)
|
||||
[(tc-result1: (and vec-t (app resolve (HeterogenousVector: es))))
|
||||
(tc/hetero-ref #'index es vec-t expected "vector")]
|
||||
[v-ty #f])))
|
||||
(match (single-value #'vec)
|
||||
[(tc-result1: (and vec-t (app resolve (HeterogenousVector: es))))
|
||||
(tc/hetero-ref #'index es vec-t expected "vector")]
|
||||
[v-ty #f]))
|
||||
;; unsafe struct-set!
|
||||
(pattern ((~or unsafe-struct-set! unsafe-struct*-set!) s:expr index:expr val:expr)
|
||||
#:attr check
|
||||
(lambda ()
|
||||
(match (single-value #'s)
|
||||
[(tc-result1: (and struct-t (app resolve (Struct: _ _ (list (fld: flds _ _) ...) _ _ _ _ _))))
|
||||
(tc/hetero-set! #'index flds #'val struct-t expected "struct")]
|
||||
[s-ty #f])))
|
||||
(match (single-value #'s)
|
||||
[(tc-result1: (and struct-t (app resolve (Struct: _ _ (list (fld: flds _ _) ...) _ _ _ _ _))))
|
||||
(tc/hetero-set! #'index flds #'val struct-t expected "struct")]
|
||||
[s-ty #f]))
|
||||
;; vector-set! on het vectors
|
||||
(pattern ((~or vector-set! unsafe-vector-set! unsafe-vector*-set!) v:expr index:expr val:expr)
|
||||
#:attr check
|
||||
(lambda ()
|
||||
(match (single-value #'v)
|
||||
[(tc-result1: (and vec-t (app resolve (HeterogenousVector: es))))
|
||||
(tc/hetero-set! #'index es #'val vec-t expected "vector")]
|
||||
[v-ty #f])))
|
||||
(match (single-value #'v)
|
||||
[(tc-result1: (and vec-t (app resolve (HeterogenousVector: es))))
|
||||
(tc/hetero-set! #'index es #'val vec-t expected "vector")]
|
||||
[v-ty #f]))
|
||||
(pattern (~and form ((~or vector-immutable vector) args:expr ...))
|
||||
#:attr check
|
||||
(lambda ()
|
||||
(match expected
|
||||
[(tc-result1: (app resolve (Vector: t))) #f]
|
||||
[(tc-result1: (app resolve (HeterogenousVector: ts)))
|
||||
(unless (= (length ts) (length (syntax->list #'(args ...))))
|
||||
(tc-error/expr "expected vector with ~a elements, but got ~a"
|
||||
(length ts)
|
||||
(make-HeterogenousVector (map tc-expr/t (syntax->list #'(args ...))))))
|
||||
(for ([e (in-list (syntax->list #'(args ...)))]
|
||||
[t (in-list ts)])
|
||||
(tc-expr/check e (ret t)))
|
||||
expected]
|
||||
;; If the expected type is a union, then we examine just the parts
|
||||
;; of the union that are vectors. If there's only one of those,
|
||||
;; we re-run this whole algorithm with that. Otherwise, we treat
|
||||
;; it like any other expected type.
|
||||
[(tc-result1: (app resolve (Union: ts))) (=> continue)
|
||||
(define u-ts (for/list ([t (in-list ts)]
|
||||
#:when (eq? 'vector (Type-key t)))
|
||||
t))
|
||||
(match u-ts
|
||||
[(list t0) (tc/app/check #'(#%plain-app . form) (ret t0))]
|
||||
[_ (continue)])]
|
||||
;; since vectors are mutable, if there is no expected type, we want to generalize the element type
|
||||
[(or #f (tc-result1: _))
|
||||
(ret (make-HeterogenousVector (map (lambda (x) (generalize (tc-expr/t x)))
|
||||
(syntax->list #'(args ...)))))]
|
||||
[_ (int-err "bad expected: ~a" expected)]))))
|
||||
|
||||
(define tc/app-hetero (reify-syntax-class tc/app-hetero*))
|
||||
(match expected
|
||||
[(tc-result1: (app resolve (Vector: t))) #f]
|
||||
[(tc-result1: (app resolve (HeterogenousVector: ts)))
|
||||
(unless (= (length ts) (length (syntax->list #'(args ...))))
|
||||
(tc-error/expr "expected vector with ~a elements, but got ~a"
|
||||
(length ts)
|
||||
(make-HeterogenousVector (map tc-expr/t (syntax->list #'(args ...))))))
|
||||
(for ([e (in-list (syntax->list #'(args ...)))]
|
||||
[t (in-list ts)])
|
||||
(tc-expr/check e (ret t)))
|
||||
expected]
|
||||
;; If the expected type is a union, then we examine just the parts
|
||||
;; of the union that are vectors. If there's only one of those,
|
||||
;; we re-run this whole algorithm with that. Otherwise, we treat
|
||||
;; it like any other expected type.
|
||||
[(tc-result1: (app resolve (Union: ts))) (=> continue)
|
||||
(define u-ts (for/list ([t (in-list ts)]
|
||||
#:when (eq? 'vector (Type-key t)))
|
||||
t))
|
||||
(match u-ts
|
||||
[(list t0) (tc/app/check #'(#%plain-app . form) (ret t0))]
|
||||
[_ (continue)])]
|
||||
;; since vectors are mutable, if there is no expected type, we want to generalize the element type
|
||||
[(or #f (tc-result1: _))
|
||||
(ret (make-HeterogenousVector (map (lambda (x) (generalize (tc-expr/t x)))
|
||||
(syntax->list #'(args ...)))))]
|
||||
[_ (int-err "bad expected: ~a" expected)])))
|
||||
|
|
|
|||
|
|
@ -3,6 +3,7 @@
|
|||
|
||||
(require (rename-in "../../utils/utils.rkt" [infer r:infer])
|
||||
"signatures.rkt"
|
||||
"utils.rkt"
|
||||
syntax/parse racket/match
|
||||
syntax/parse/experimental/reflect
|
||||
(typecheck signatures tc-app-helper tc-funapp tc-metafunctions)
|
||||
|
|
@ -17,45 +18,39 @@
|
|||
(import tc-expr^)
|
||||
(export tc-app-keywords^)
|
||||
|
||||
(define-syntax-class (tc/app-keywords* expected)
|
||||
#:attributes (check)
|
||||
#:literals (#%plain-app list)
|
||||
(pattern (~and form
|
||||
((#%plain-app cpce s-kp fn kpe kws num)
|
||||
kw-list
|
||||
(#%plain-app list . kw-arg-list)
|
||||
. pos-args))
|
||||
#:declare cpce (id-from 'checked-procedure-check-and-extract 'racket/private/kw)
|
||||
#:declare s-kp (id-from 'struct:keyword-procedure 'racket/private/kw)
|
||||
#:declare kpe (id-from 'keyword-procedure-extract 'racket/private/kw)
|
||||
#:attr check
|
||||
(lambda ()
|
||||
|
||||
(match (tc-expr #'fn)
|
||||
[(tc-result1:
|
||||
(Poly: vars
|
||||
(Function: (list (and ar (arr: dom rng (and rest #f) (and drest #f) kw-formals))))))
|
||||
(=> fail)
|
||||
(unless (null? (fv/list kw-formals))
|
||||
(fail))
|
||||
(match (map single-value (syntax->list #'pos-args))
|
||||
[(list (tc-result1: argtys-t) ...)
|
||||
(let* ([subst (infer vars null argtys-t dom rng
|
||||
(and expected (tc-results->values expected)))])
|
||||
(unless subst (fail))
|
||||
(tc-keywords #'form (list (subst-all subst ar))
|
||||
(type->list (tc-expr/t #'kws)) #'kw-arg-list #'pos-args expected))])]
|
||||
[(tc-result1: (Function: arities))
|
||||
(tc-keywords #'(#%plain-app . form) arities (type->list (tc-expr/t #'kws))
|
||||
#'kw-arg-list #'pos-args expected)]
|
||||
[(tc-result1: (Poly: _ (Function: _)))
|
||||
(tc-error/expr #:return (ret (Un))
|
||||
"Inference for polymorphic keyword functions not supported")]
|
||||
[(tc-result1: t)
|
||||
(tc-error/expr #:return (ret (Un))
|
||||
"Cannot apply expression of type ~a, since it is not a function type" t)]))))
|
||||
|
||||
(define tc/app-keywords (reify-syntax-class tc/app-keywords*))
|
||||
(define-tc/app-syntax-class (tc/app-keywords expected)
|
||||
#:literals (#%plain-app list)
|
||||
(pattern (~and form
|
||||
((#%plain-app cpce s-kp fn kpe kws num)
|
||||
kw-list
|
||||
(#%plain-app list . kw-arg-list)
|
||||
. pos-args))
|
||||
#:declare cpce (id-from 'checked-procedure-check-and-extract 'racket/private/kw)
|
||||
#:declare s-kp (id-from 'struct:keyword-procedure 'racket/private/kw)
|
||||
#:declare kpe (id-from 'keyword-procedure-extract 'racket/private/kw)
|
||||
(match (tc-expr #'fn)
|
||||
[(tc-result1:
|
||||
(Poly: vars
|
||||
(Function: (list (and ar (arr: dom rng (and rest #f) (and drest #f) kw-formals))))))
|
||||
(=> fail)
|
||||
(unless (null? (fv/list kw-formals))
|
||||
(fail))
|
||||
(match (map single-value (syntax->list #'pos-args))
|
||||
[(list (tc-result1: argtys-t) ...)
|
||||
(let* ([subst (infer vars null argtys-t dom rng
|
||||
(and expected (tc-results->values expected)))])
|
||||
(unless subst (fail))
|
||||
(tc-keywords #'form (list (subst-all subst ar))
|
||||
(type->list (tc-expr/t #'kws)) #'kw-arg-list #'pos-args expected))])]
|
||||
[(tc-result1: (Function: arities))
|
||||
(tc-keywords #'(#%plain-app . form) arities (type->list (tc-expr/t #'kws))
|
||||
#'kw-arg-list #'pos-args expected)]
|
||||
[(tc-result1: (Poly: _ (Function: _)))
|
||||
(tc-error/expr #:return (ret (Un))
|
||||
"Inference for polymorphic keyword functions not supported")]
|
||||
[(tc-result1: t)
|
||||
(tc-error/expr #:return (ret (Un))
|
||||
"Cannot apply expression of type ~a, since it is not a function type" t)])))
|
||||
|
||||
(define (tc-keywords/internal arity kws kw-args error?)
|
||||
(match arity
|
||||
|
|
|
|||
|
|
@ -2,6 +2,7 @@
|
|||
|
||||
(require "../../utils/utils.rkt"
|
||||
"signatures.rkt"
|
||||
"utils.rkt"
|
||||
syntax/parse racket/match racket/list
|
||||
syntax/parse/experimental/reflect
|
||||
unstable/sequence
|
||||
|
|
@ -16,46 +17,37 @@
|
|||
(import tc-expr^ tc-let^ tc-lambda^)
|
||||
(export tc-app-lambda^)
|
||||
|
||||
(define-syntax-class (tc/app-lambda* expected)
|
||||
#:attributes (check)
|
||||
#:literals (#%plain-app #%plain-lambda letrec-values)
|
||||
;; let loop
|
||||
(pattern (~and form ((letrec-values ([(lp) (~and lam (#%plain-lambda args . body))]) lp*) . actuals))
|
||||
#:fail-unless expected #f
|
||||
#:fail-unless (not (andmap type-annotation (syntax->list #'(lp . args)))) #f
|
||||
#:fail-unless (free-identifier=? #'lp #'lp*) #f
|
||||
#:attr check
|
||||
(lambda ()
|
||||
(let-loop-check #'(#%plain-app . form) #'lam #'lp #'actuals #'args #'body expected)))
|
||||
;; inference for ((lambda
|
||||
(pattern ((#%plain-lambda (x ...) . body) args ...)
|
||||
#:fail-unless (= (length (syntax->list #'(x ...)))
|
||||
(length (syntax->list #'(args ...)))) #f
|
||||
#:fail-when (andmap type-annotation (syntax->list #'(x ...))) #f
|
||||
#:attr check
|
||||
(lambda ()
|
||||
(tc/let-values #'((x) ...) #'(args ...) #'body
|
||||
#'(let-values ([(x) args] ...) . body)
|
||||
expected)))
|
||||
;; inference for ((lambda with dotted rest
|
||||
(pattern ((#%plain-lambda (x ... . rst:id) . body) args ...)
|
||||
#:fail-unless (<= (length (syntax->list #'(x ...)))
|
||||
(length (syntax->list #'(args ...)))) #f
|
||||
;; FIXME - remove this restriction - doesn't work because the annotation
|
||||
;; on rst is not a normal annotation, may have * or ...
|
||||
#:fail-when (type-annotation #'rst) #f
|
||||
#:fail-when (andmap type-annotation (syntax->list #'(x ...))) #f
|
||||
#:attr check
|
||||
(lambda ()
|
||||
(let-values ([(fixed-args varargs)
|
||||
(split-at (syntax->list #'(args ...)) (length (syntax->list #'(x ...))))])
|
||||
(with-syntax ([(fixed-args ...) fixed-args]
|
||||
[varg #`(#%plain-app list #,@varargs)])
|
||||
(tc/let-values #'((x) ... (rst)) #`(fixed-args ... varg) #'body
|
||||
#'(let-values ([(x) fixed-args] ... [(rst) varg]) . body)
|
||||
expected))))))
|
||||
|
||||
(define tc/app-lambda (reify-syntax-class tc/app-lambda*))
|
||||
(define-tc/app-syntax-class (tc/app-lambda expected)
|
||||
#:literals (#%plain-app #%plain-lambda letrec-values)
|
||||
;; let loop
|
||||
(pattern (~and form ((letrec-values ([(lp) (~and lam (#%plain-lambda args . body))]) lp*) . actuals))
|
||||
#:fail-unless expected #f
|
||||
#:fail-unless (not (andmap type-annotation (syntax->list #'(lp . args)))) #f
|
||||
#:fail-unless (free-identifier=? #'lp #'lp*) #f
|
||||
(let-loop-check #'(#%plain-app . form) #'lam #'lp #'actuals #'args #'body expected))
|
||||
;; inference for ((lambda
|
||||
(pattern ((#%plain-lambda (x ...) . body) args ...)
|
||||
#:fail-unless (= (length (syntax->list #'(x ...)))
|
||||
(length (syntax->list #'(args ...)))) #f
|
||||
#:fail-when (andmap type-annotation (syntax->list #'(x ...))) #f
|
||||
(tc/let-values #'((x) ...) #'(args ...) #'body
|
||||
#'(let-values ([(x) args] ...) . body)
|
||||
expected))
|
||||
;; inference for ((lambda with dotted rest
|
||||
(pattern ((#%plain-lambda (x ... . rst:id) . body) args ...)
|
||||
#:fail-unless (<= (length (syntax->list #'(x ...)))
|
||||
(length (syntax->list #'(args ...)))) #f
|
||||
;; FIXME - remove this restriction - doesn't work because the annotation
|
||||
;; on rst is not a normal annotation, may have * or ...
|
||||
#:fail-when (type-annotation #'rst) #f
|
||||
#:fail-when (andmap type-annotation (syntax->list #'(x ...))) #f
|
||||
(let-values ([(fixed-args varargs)
|
||||
(split-at (syntax->list #'(args ...)) (length (syntax->list #'(x ...))))])
|
||||
(with-syntax ([(fixed-args ...) fixed-args]
|
||||
[varg #`(#%plain-app list #,@varargs)])
|
||||
(tc/let-values #'((x) ... (rst)) #`(fixed-args ... varg) #'body
|
||||
#'(let-values ([(x) fixed-args] ... [(rst) varg]) . body)
|
||||
expected)))))
|
||||
|
||||
|
||||
(define (let-loop-check form lam lp actuals args body expected)
|
||||
|
|
|
|||
|
|
@ -3,6 +3,7 @@
|
|||
|
||||
(require "../../utils/utils.rkt"
|
||||
"signatures.rkt"
|
||||
"utils.rkt"
|
||||
syntax/parse racket/match
|
||||
syntax/parse/experimental/reflect
|
||||
(only-in '#%kernel [reverse k:reverse])
|
||||
|
|
@ -24,95 +25,80 @@
|
|||
(export tc-app-list^)
|
||||
|
||||
|
||||
(define-syntax-class (tc/app-list* expected)
|
||||
#:attributes (check)
|
||||
#:literals (reverse k:reverse list list*
|
||||
cons map andmap ormap)
|
||||
(define-tc/app-syntax-class (tc/app-list expected)
|
||||
#:literals (reverse k:reverse list list*
|
||||
cons map andmap ormap)
|
||||
(pattern (~and form (map f arg0 arg ...))
|
||||
#:attr check
|
||||
(lambda ()
|
||||
(match* ((single-value #'arg0) (map single-value (syntax->list #'(arg ...))))
|
||||
;; if the argument is a ListDots
|
||||
[((tc-result1: (ListDots: t0 bound0))
|
||||
(list (tc-result1: (or (and (ListDots: t bound) (app (λ _ #f) var))
|
||||
;; a devious hack - just generate #f so the test below succeeds
|
||||
;; have to explicitly bind `var' since otherwise `var' appears
|
||||
;; on only one side of the or
|
||||
;; NOTE: safe to include these, `map' will error if any list is
|
||||
;; not the same length as all the others
|
||||
(and (Listof: t var) (app (λ _ #f) bound))))
|
||||
...))
|
||||
(=> fail)
|
||||
(unless (for/and ([b bound]) (or (not b) (eq? bound0 b))) (fail))
|
||||
(match (extend-tvars (list bound0)
|
||||
;; just check that the function applies successfully to the element type
|
||||
(tc/funapp #'f #'(arg0 arg ...) (tc-expr #'f) (cons (ret t0) (map ret t)) expected))
|
||||
[(tc-result1: t) (ret (make-ListDots t bound0))]
|
||||
[(tc-results: ts)
|
||||
(tc-error/expr #:return (ret (Un))
|
||||
"Expected one value, but got ~a" (-values ts))])]
|
||||
;; otherwise, if it's not a ListDots, defer to the regular function typechecking
|
||||
;; TODO fix double typechecking
|
||||
[(res0 res) (tc/app-regular #'(#%plain-app . form) expected)])))
|
||||
(match* ((single-value #'arg0) (map single-value (syntax->list #'(arg ...))))
|
||||
;; if the argument is a ListDots
|
||||
[((tc-result1: (ListDots: t0 bound0))
|
||||
(list (tc-result1: (or (and (ListDots: t bound) (app (λ _ #f) var))
|
||||
;; a devious hack - just generate #f so the test below succeeds
|
||||
;; have to explicitly bind `var' since otherwise `var' appears
|
||||
;; on only one side of the or
|
||||
;; NOTE: safe to include these, `map' will error if any list is
|
||||
;; not the same length as all the others
|
||||
(and (Listof: t var) (app (λ _ #f) bound))))
|
||||
...))
|
||||
(=> fail)
|
||||
(unless (for/and ([b bound]) (or (not b) (eq? bound0 b))) (fail))
|
||||
(match (extend-tvars (list bound0)
|
||||
;; just check that the function applies successfully to the element type
|
||||
(tc/funapp #'f #'(arg0 arg ...) (tc-expr #'f) (cons (ret t0) (map ret t)) expected))
|
||||
[(tc-result1: t) (ret (make-ListDots t bound0))]
|
||||
[(tc-results: ts)
|
||||
(tc-error/expr #:return (ret (Un))
|
||||
"Expected one value, but got ~a" (-values ts))])]
|
||||
;; otherwise, if it's not a ListDots, defer to the regular function typechecking
|
||||
;; TODO fix double typechecking
|
||||
[(res0 res) (tc/app-regular #'form expected)]))
|
||||
;; ormap/andmap of ... argument
|
||||
(pattern (~and form ((~or andmap ormap) f arg))
|
||||
#:attr check
|
||||
(lambda ()
|
||||
(match-let* ([arg-ty (single-value #'arg)]
|
||||
[ft (tc-expr #'f)])
|
||||
(match (match arg-ty
|
||||
;; if the argument is a ListDots
|
||||
[(tc-result1: (ListDots: t bound))
|
||||
;; just check that the function applies successfully to the element type
|
||||
(tc/funapp #'f #'(arg) ft (list (ret (substitute Univ bound t))) expected)]
|
||||
;; otherwise ...
|
||||
[_ #f])
|
||||
[(tc-result1: t) (ret (Un (-val #f) t))]
|
||||
;; if it's not a ListDots, defer to the regular function typechecking
|
||||
;; TODO fix double typechecking
|
||||
[_ (tc/app-regular #'(#%plain-app . form) expected)]))))
|
||||
(match-let* ([arg-ty (single-value #'arg)]
|
||||
[ft (tc-expr #'f)])
|
||||
(match (match arg-ty
|
||||
;; if the argument is a ListDots
|
||||
[(tc-result1: (ListDots: t bound))
|
||||
;; just check that the function applies successfully to the element type
|
||||
(tc/funapp #'f #'(arg) ft (list (ret (substitute Univ bound t))) expected)]
|
||||
;; otherwise ...
|
||||
[_ #f])
|
||||
[(tc-result1: t) (ret (Un (-val #f) t))]
|
||||
;; if it's not a ListDots, defer to the regular function typechecking
|
||||
;; TODO fix double typechecking
|
||||
[_ (tc/app-regular #'form expected)])))
|
||||
;; special case for `list'
|
||||
(pattern (list . args)
|
||||
#:attr check
|
||||
(lambda ()
|
||||
(match expected
|
||||
[(tc-result1: (Listof: elem-ty))
|
||||
(for ([i (in-list (syntax->list #'args))])
|
||||
(tc-expr/check i (ret elem-ty)))
|
||||
expected]
|
||||
[(tc-result1: (List: (? (lambda (ts) (= (length (syntax->list #'args))
|
||||
(length ts)))
|
||||
ts)))
|
||||
(for ([ac (in-list (syntax->list #'args))]
|
||||
[exp (in-list ts)])
|
||||
(tc-expr/check ac (ret exp)))
|
||||
expected]
|
||||
[_
|
||||
(let ([tys (map tc-expr/t (syntax->list #'args))])
|
||||
(ret (apply -lst* tys)))])))
|
||||
(match expected
|
||||
[(tc-result1: (Listof: elem-ty))
|
||||
(for ([i (in-list (syntax->list #'args))])
|
||||
(tc-expr/check i (ret elem-ty)))
|
||||
expected]
|
||||
[(tc-result1: (List: (? (lambda (ts) (= (length (syntax->list #'args))
|
||||
(length ts)))
|
||||
ts)))
|
||||
(for ([ac (in-list (syntax->list #'args))]
|
||||
[exp (in-list ts)])
|
||||
(tc-expr/check ac (ret exp)))
|
||||
expected]
|
||||
[_
|
||||
(let ([tys (map tc-expr/t (syntax->list #'args))])
|
||||
(ret (apply -lst* tys)))]))
|
||||
;; special case for `list*'
|
||||
(pattern (list* . args)
|
||||
#:attr check
|
||||
(lambda ()
|
||||
(match-let* ([(list tys ... last) (map tc-expr/t (syntax->list #'args))])
|
||||
(ret (foldr -pair last tys)))))
|
||||
(match-let* ([(list tys ... last) (map tc-expr/t (syntax->list #'args))])
|
||||
(ret (foldr -pair last tys))))
|
||||
;; special case for `reverse' to propagate expected type info
|
||||
(pattern ((~or reverse k:reverse) arg)
|
||||
#:attr check
|
||||
(lambda ()
|
||||
(match expected
|
||||
[(tc-result1: (Listof: _))
|
||||
(tc-expr/check #'arg expected)]
|
||||
(match expected
|
||||
[(tc-result1: (Listof: _))
|
||||
(tc-expr/check #'arg expected)]
|
||||
[(tc-result1: (List: ts))
|
||||
(tc-expr/check #'arg (ret (-Tuple (reverse ts))))
|
||||
expected]
|
||||
[_
|
||||
(match (single-value #'arg)
|
||||
[(tc-result1: (List: ts))
|
||||
(tc-expr/check #'arg (ret (-Tuple (reverse ts))))
|
||||
expected]
|
||||
[_
|
||||
(match (single-value #'arg)
|
||||
[(tc-result1: (List: ts))
|
||||
(cond-check-below (ret (-Tuple (reverse ts))) expected)]
|
||||
[arg-ty
|
||||
(tc/funapp #'reverse #'(arg) (single-value #'reverse) (list arg-ty) expected)])]))))
|
||||
|
||||
|
||||
(define tc/app-list (reify-syntax-class tc/app-list*))
|
||||
|
||||
(cond-check-below (ret (-Tuple (reverse ts))) expected)]
|
||||
[arg-ty
|
||||
(tc/funapp #'reverse #'(arg) (single-value #'reverse) (list arg-ty) expected)])])))
|
||||
|
|
|
|||
|
|
@ -2,6 +2,7 @@
|
|||
|
||||
(require "../../utils/utils.rkt"
|
||||
"signatures.rkt"
|
||||
"utils.rkt"
|
||||
syntax/parse racket/match unstable/sequence
|
||||
syntax/parse/experimental/reflect
|
||||
(typecheck signatures tc-funapp check-below)
|
||||
|
|
@ -16,24 +17,16 @@
|
|||
(export tc-app-objects^)
|
||||
|
||||
|
||||
(define-syntax-class (tc/app-objects* expected)
|
||||
#:attributes (check)
|
||||
#:literals (#%plain-app list cons quote)
|
||||
|
||||
(define-tc/app-syntax-class (tc/app-objects expected)
|
||||
#:literals (#%plain-app list cons quote)
|
||||
(pattern (dmo b cl
|
||||
(#%plain-app list . pos-args)
|
||||
(#%plain-app list (#%plain-app cons (quote names) named-args) ...))
|
||||
#:declare dmo (id-from 'do-make-object 'racket/private/class-internal)
|
||||
#:attr check
|
||||
(lambda ()
|
||||
(check-do-make-object #'b #'cl #'pos-args #'(names ...) #'(named-args ...))))
|
||||
(check-do-make-object #'b #'cl #'pos-args #'(names ...) #'(named-args ...)))
|
||||
(pattern (dmo . args)
|
||||
#:declare dmo (id-from 'do-make-object 'racket/private/class-internal)
|
||||
#:attr check
|
||||
(lambda ()
|
||||
(int-err "unexpected arguments to do-make-object"))))
|
||||
|
||||
(define tc/app-objects (reify-syntax-class tc/app-objects*))
|
||||
(int-err "unexpected arguments to do-make-object")))
|
||||
|
||||
;; do-make-object now takes blame as its first argument, which isn't checked
|
||||
;; (it's just an s-expression)
|
||||
|
|
|
|||
|
|
@ -2,6 +2,7 @@
|
|||
|
||||
(require "../../utils/utils.rkt"
|
||||
"signatures.rkt"
|
||||
"utils.rkt"
|
||||
syntax/parse racket/match
|
||||
syntax/parse/experimental/reflect
|
||||
unstable/list
|
||||
|
|
@ -22,66 +23,53 @@
|
|||
(import tc-expr^)
|
||||
(export tc-app-special^)
|
||||
|
||||
(define-syntax-class (tc/app-special* expected)
|
||||
#:attributes (check)
|
||||
#:literals (#%plain-app #%plain-lambda extend-parameterization quote
|
||||
false? not call-with-values list)
|
||||
;; parameterize
|
||||
(pattern (extend-parameterization pmz args ...)
|
||||
#:attr check
|
||||
(lambda ()
|
||||
(let loop ([args (syntax->list #'(args ...))])
|
||||
(if (null? args) (ret Univ)
|
||||
(let* ([p (car args)]
|
||||
[pt (single-value p)]
|
||||
[v (cadr args)]
|
||||
[vt (single-value v)])
|
||||
(match pt
|
||||
[(tc-result1: (Param: a b))
|
||||
(check-below vt a)
|
||||
(loop (cddr args))]
|
||||
[(tc-result1: t)
|
||||
(tc-error/expr #:return (or expected (ret Univ)) "expected Parameter, but got ~a" t)
|
||||
(loop (cddr args))]))))))
|
||||
;; use the additional but normally ignored first argument to make-sequence
|
||||
;; to provide a better instantiation
|
||||
(pattern ((~var op (id-from 'make-sequence 'racket/private/for))
|
||||
(~and quo (quote (i:id ...))) arg:expr)
|
||||
#:when (andmap type-annotation (syntax->list #'(i ...)))
|
||||
#:attr check
|
||||
(lambda ()
|
||||
(match (single-value #'op)
|
||||
[(tc-result1: (and t Poly?))
|
||||
(tc-expr/check #'quo (ret Univ))
|
||||
(tc/funapp #'op #'(quo arg)
|
||||
(ret (instantiate-poly t (extend (list Univ Univ)
|
||||
(map type-annotation (syntax->list #'(i ...)))
|
||||
Univ)))
|
||||
(list (ret Univ) (single-value #'arg))
|
||||
expected)])))
|
||||
;; special-case for not - flip the filters
|
||||
(pattern ((~or false? not) arg)
|
||||
#:attr check
|
||||
(lambda ()
|
||||
(match (single-value #'arg)
|
||||
[(tc-result1: t (FilterSet: f+ f-) _)
|
||||
(ret -Boolean (make-FilterSet f- f+))])))
|
||||
;; special case for (current-contract-region)'s default expansion
|
||||
;; just let it through without any typechecking, since module-name-fixup
|
||||
;; is a private function from syntax/location, so this must have been
|
||||
;; (quote-module-name) originally.
|
||||
(pattern (op src path)
|
||||
#:declare op (id-from 'module-name-fixup 'syntax/location)
|
||||
#:attr check
|
||||
(lambda ()
|
||||
(ret Univ)))
|
||||
;; special case for `delay'
|
||||
(pattern (mp1 (#%plain-lambda ()
|
||||
(#%plain-app mp2 (#%plain-app call-with-values (#%plain-lambda () e) list))))
|
||||
#:declare mp1 (id-from 'make-promise 'racket/promise)
|
||||
#:declare mp2 (id-from 'make-promise 'racket/promise)
|
||||
#:attr check
|
||||
(lambda ()
|
||||
(ret (-Promise (tc-expr/t #'e))))))
|
||||
|
||||
(define tc/app-special (reify-syntax-class tc/app-special*))
|
||||
(define-tc/app-syntax-class (tc/app-special expected)
|
||||
#:literals (#%plain-app #%plain-lambda extend-parameterization quote
|
||||
false? not call-with-values list)
|
||||
;; parameterize
|
||||
(pattern (extend-parameterization pmz args ...)
|
||||
(let loop ([args (syntax->list #'(args ...))])
|
||||
(if (null? args) (ret Univ)
|
||||
(let* ([p (car args)]
|
||||
[pt (single-value p)]
|
||||
[v (cadr args)]
|
||||
[vt (single-value v)])
|
||||
(match pt
|
||||
[(tc-result1: (Param: a b))
|
||||
(check-below vt a)
|
||||
(loop (cddr args))]
|
||||
[(tc-result1: t)
|
||||
(tc-error/expr #:return (or expected (ret Univ)) "expected Parameter, but got ~a" t)
|
||||
(loop (cddr args))])))))
|
||||
;; use the additional but normally ignored first argument to make-sequence
|
||||
;; to provide a better instantiation
|
||||
(pattern ((~var op (id-from 'make-sequence 'racket/private/for))
|
||||
(~and quo (quote (i:id ...))) arg:expr)
|
||||
#:when (andmap type-annotation (syntax->list #'(i ...)))
|
||||
(match (single-value #'op)
|
||||
[(tc-result1: (and t Poly?))
|
||||
(tc-expr/check #'quo (ret Univ))
|
||||
(tc/funapp #'op #'(quo arg)
|
||||
(ret (instantiate-poly t (extend (list Univ Univ)
|
||||
(map type-annotation (syntax->list #'(i ...)))
|
||||
Univ)))
|
||||
(list (ret Univ) (single-value #'arg))
|
||||
expected)]))
|
||||
;; special-case for not - flip the filters
|
||||
(pattern ((~or false? not) arg)
|
||||
(match (single-value #'arg)
|
||||
[(tc-result1: t (FilterSet: f+ f-) _)
|
||||
(ret -Boolean (make-FilterSet f- f+))]))
|
||||
;; special case for (current-contract-region)'s default expansion
|
||||
;; just let it through without any typechecking, since module-name-fixup
|
||||
;; is a private function from syntax/location, so this must have been
|
||||
;; (quote-module-name) originally.
|
||||
(pattern (op src path)
|
||||
#:declare op (id-from 'module-name-fixup 'syntax/location)
|
||||
(ret Univ))
|
||||
;; special case for `delay'
|
||||
(pattern (mp1 (#%plain-lambda ()
|
||||
(#%plain-app mp2 (#%plain-app call-with-values (#%plain-lambda () e) list))))
|
||||
#:declare mp1 (id-from 'make-promise 'racket/promise)
|
||||
#:declare mp2 (id-from 'make-promise 'racket/promise)
|
||||
(ret (-Promise (tc-expr/t #'e)))))
|
||||
|
|
|
|||
|
|
@ -2,6 +2,7 @@
|
|||
|
||||
(require "../../utils/utils.rkt"
|
||||
"signatures.rkt"
|
||||
"utils.rkt"
|
||||
syntax/parse racket/match
|
||||
syntax/parse/experimental/reflect
|
||||
(typecheck signatures tc-funapp check-below)
|
||||
|
|
@ -14,48 +15,39 @@
|
|||
(import tc-expr^)
|
||||
(export tc-app-values^)
|
||||
|
||||
(define-syntax-class (tc/app-values* expected)
|
||||
#:attributes (check)
|
||||
#:literals (values call-with-values)
|
||||
(define-tc/app-syntax-class (tc/app-values expected)
|
||||
#:literals (values call-with-values)
|
||||
;; call-with-values
|
||||
(pattern (call-with-values prod con)
|
||||
#:attr check
|
||||
(lambda ()
|
||||
(match (tc/funapp #'prod #'() (single-value #'prod) null #f)
|
||||
[(tc-results: ts fs os)
|
||||
(tc/funapp #'con #'(prod) (single-value #'con) (map ret ts fs os) expected)])))
|
||||
(match (tc/funapp #'prod #'() (single-value #'prod) null #f)
|
||||
[(tc-results: ts fs os)
|
||||
(tc/funapp #'con #'(prod) (single-value #'con) (map ret ts fs os) expected)]))
|
||||
|
||||
;; special case for `values' with single argument
|
||||
;; we just ignore the values, except that it forces arg to return one value
|
||||
(pattern (values arg)
|
||||
#:attr check
|
||||
(lambda ()
|
||||
(match expected
|
||||
[#f (single-value #'arg)]
|
||||
[(tc-result1: tp)
|
||||
(single-value #'arg expected)]
|
||||
[(tc-results: ts)
|
||||
(single-value #'arg) ;Type check the argument, to find other errors
|
||||
(tc-error/expr #:return expected
|
||||
"wrong number of values: expected ~a but got one"
|
||||
(length ts))])))
|
||||
(match expected
|
||||
[#f (single-value #'arg)]
|
||||
[(tc-result1: tp)
|
||||
(single-value #'arg expected)]
|
||||
[(tc-results: ts)
|
||||
(single-value #'arg) ;Type check the argument, to find other errors
|
||||
(tc-error/expr #:return expected
|
||||
"wrong number of values: expected ~a but got one"
|
||||
(length ts))]))
|
||||
;; handle `values' specially
|
||||
(pattern (values . args)
|
||||
#:attr check
|
||||
(lambda ()
|
||||
(match expected
|
||||
[(tc-results: ets efs eos)
|
||||
(match-let ([(list (tc-result1: ts fs os) ...)
|
||||
(for/list ([arg (syntax->list #'args)]
|
||||
[et ets] [ef efs] [eo eos])
|
||||
(single-value arg (ret et ef eo)))])
|
||||
(if (= (length ts) (length ets) (length (syntax->list #'args)))
|
||||
(ret ts fs os)
|
||||
(tc-error/expr #:return expected "wrong number of values: expected ~a but got ~a"
|
||||
(length ets) (length (syntax->list #'args)))))]
|
||||
[_ (match-let ([(list (tc-result1: ts fs os) ...)
|
||||
(for/list ([arg (syntax->list #'args)])
|
||||
(single-value arg))])
|
||||
(ret ts fs os))]))))
|
||||
|
||||
(define tc/app-values (reify-syntax-class tc/app-values*))
|
||||
(match expected
|
||||
[(tc-results: ets efs eos)
|
||||
(match-let ([(list (tc-result1: ts fs os) ...)
|
||||
(for/list ([arg (syntax->list #'args)]
|
||||
[et ets] [ef efs] [eo eos])
|
||||
(single-value arg (ret et ef eo)))])
|
||||
(if (= (length ts) (length ets) (length (syntax->list #'args)))
|
||||
(ret ts fs os)
|
||||
(tc-error/expr #:return expected "wrong number of values: expected ~a but got ~a"
|
||||
(length ets) (length (syntax->list #'args)))))]
|
||||
[_ (match-let ([(list (tc-result1: ts fs os) ...)
|
||||
(for/list ([arg (syntax->list #'args)])
|
||||
(single-value arg))])
|
||||
(ret ts fs os))])))
|
||||
|
|
|
|||
23
collects/typed-racket/typecheck/tc-app/utils.rkt
Normal file
23
collects/typed-racket/typecheck/tc-app/utils.rkt
Normal file
|
|
@ -0,0 +1,23 @@
|
|||
#lang racket/base
|
||||
|
||||
(require syntax/parse
|
||||
syntax/parse/experimental/reflect
|
||||
(for-syntax racket/base syntax/parse))
|
||||
|
||||
(provide define-reified-syntax-class define-tc/app-syntax-class)
|
||||
|
||||
(define-syntax-rule (define-reified-syntax-class (id . args) . body)
|
||||
(define id
|
||||
(let ()
|
||||
(define-syntax-class (id . args) . body)
|
||||
(reify-syntax-class id))))
|
||||
|
||||
(define-syntax define-tc/app-syntax-class
|
||||
(syntax-parser
|
||||
#:literals (pattern)
|
||||
((_ (id expected) (~and parse-option (~not (pattern . args))) ...
|
||||
(pattern syntax-pattern pattern-directive ... body) ...+)
|
||||
#'(define-reified-syntax-class (id expected)
|
||||
#:attributes (check) parse-option ...
|
||||
(pattern syntax-pattern pattern-directive ...
|
||||
#:attr check (lambda () body)) ...))))
|
||||
Loading…
Reference in New Issue
Block a user