tc-app: add missing 'function' annotations
Update the type-table with annotations for some identifiers that are handled specially by `tc-app`. Add type table tests to `unit-tests/typecheck-tests.rkt`
This commit is contained in:
Ben Greenman
parent
fd5d5e9319
commit
504f11cc94
|
|
@ -5,7 +5,7 @@
|
|||
"utils.rkt"
|
||||
syntax/parse racket/match
|
||||
(typecheck signatures)
|
||||
(types abbrev utils)
|
||||
(types abbrev type-table utils)
|
||||
(rep type-rep)
|
||||
|
||||
(for-label
|
||||
|
|
@ -26,7 +26,9 @@
|
|||
(match (single-value #'e)
|
||||
[(tc-result1: (ListDots: dty dbound))
|
||||
(ret null null null dty dbound)]
|
||||
[(tc-result1: (List: ts)) (ret ts)]
|
||||
[(tc-result1: (List: ts))
|
||||
(add-typeof-expr #'f (ret (->* ts (-values ts))))
|
||||
(ret ts)]
|
||||
[_ (tc/apply #'f #'(e))]))
|
||||
(pattern ((~or apply k:apply) f . args)
|
||||
(tc/apply #'f #'args)))
|
||||
|
|
|
|||
|
|
@ -49,28 +49,37 @@
|
|||
|
||||
|
||||
;; FIXME - Do something with paths in the case that a structure/vector is not mutable
|
||||
(define (tc/hetero-ref i-e es-t vec-t name)
|
||||
(define (tc/hetero-ref i-e es-t vec-t name op)
|
||||
(define i-val (tc/index i-e))
|
||||
(define i-bound (length es-t))
|
||||
(cond
|
||||
[(valid-index? i-val i-bound)
|
||||
(ret (list-ref es-t i-val))]
|
||||
(define return-ty (list-ref es-t i-val))
|
||||
(add-typeof-expr op (ret (-> vec-t -Fixnum return-ty)))
|
||||
(ret return-ty)]
|
||||
[(not i-val)
|
||||
(ret (apply Un es-t))]
|
||||
(define return-ty (apply Un es-t))
|
||||
(add-typeof-expr op (ret (-> vec-t -Fixnum return-ty)))
|
||||
(ret return-ty)]
|
||||
[else
|
||||
(index-error i-val i-bound i-e vec-t name)]))
|
||||
|
||||
(define (tc/hetero-set! i-e es-t val-e vec-t name)
|
||||
(define (tc/hetero-set! i-e es-t val-e vec-t name op)
|
||||
(define i-val (tc/index i-e))
|
||||
(define i-bound (length es-t))
|
||||
(cond
|
||||
(cond
|
||||
[(valid-index? i-val i-bound)
|
||||
(tc-expr/check val-e (ret (list-ref es-t i-val)))
|
||||
(define val-t (list-ref es-t i-val))
|
||||
(tc-expr/check val-e (ret val-t))
|
||||
(add-typeof-expr op (ret (-> vec-t -Fixnum val-t -Void)))
|
||||
(ret -Void)]
|
||||
[(not i-val)
|
||||
(define val-t (single-value val-e))
|
||||
(define val-res (single-value val-e))
|
||||
(for ((es-type (in-list es-t)))
|
||||
(check-below val-t (ret es-type)))
|
||||
(check-below val-res (ret es-type)))
|
||||
(define val-t
|
||||
(match val-res [(tc-result1: t) t]))
|
||||
(add-typeof-expr op (ret (-> vec-t -Fixnum val-t -Void)))
|
||||
(ret -Void)]
|
||||
[else
|
||||
(single-value val-e)
|
||||
|
|
@ -78,47 +87,53 @@
|
|||
|
||||
(define-tc/app-syntax-class (tc/app-hetero expected)
|
||||
#:literal-sets (hetero-literals)
|
||||
(pattern (~and form ((~or unsafe-struct-ref unsafe-struct*-ref) struct:expr index:expr))
|
||||
(pattern (~and form ((~and op (~or unsafe-struct-ref unsafe-struct*-ref)) struct:expr index:expr))
|
||||
(match (single-value #'struct)
|
||||
[(tc-result1: (and struct-t (app resolve (Struct: _ _ (list (fld: flds _ _) ...) _ _ _))))
|
||||
(tc/hetero-ref #'index flds struct-t "struct")]
|
||||
(tc/hetero-ref #'index flds struct-t "struct" #'op)]
|
||||
[(tc-result1: (and struct-t (app resolve (Prefab: _ (list flds ...)))))
|
||||
(tc/hetero-ref #'index flds struct-t "prefab struct")]
|
||||
(tc/hetero-ref #'index flds struct-t "prefab struct" #'op)]
|
||||
[s-ty (tc/app-regular #'form expected)]))
|
||||
;; vector-ref on het vectors
|
||||
(pattern (~and form ((~or vector-ref unsafe-vector-ref unsafe-vector*-ref) vec:expr index:expr))
|
||||
(pattern (~and form ((~and op (~or vector-ref unsafe-vector-ref unsafe-vector*-ref)) vec:expr index:expr))
|
||||
(match (single-value #'vec)
|
||||
[(tc-result1: (and vec-t (app resolve (Is-a: (HeterogeneousVector: es)))))
|
||||
(tc/hetero-ref #'index es vec-t "vector")]
|
||||
(tc/hetero-ref #'index es vec-t "vector" #'op)]
|
||||
[v-ty (tc/app-regular #'form expected)]))
|
||||
;; unsafe struct-set!
|
||||
(pattern (~and form ((~or unsafe-struct-set! unsafe-struct*-set!) s:expr index:expr val:expr))
|
||||
;; unsafe struct-set!
|
||||
(pattern (~and form ((~and op (~or unsafe-struct-set! unsafe-struct*-set!)) s:expr index:expr val:expr))
|
||||
(match (single-value #'s)
|
||||
[(tc-result1: (and struct-t (app resolve (Struct: _ _ (list (fld: flds _ _) ...) _ _ _))))
|
||||
(tc/hetero-set! #'index flds #'val struct-t "struct")]
|
||||
(tc/hetero-set! #'index flds #'val struct-t "struct" #'op)]
|
||||
[s-ty (tc/app-regular #'form expected)]))
|
||||
;; vector-set! on het vectors
|
||||
(pattern (~and form ((~or vector-set! unsafe-vector-set! unsafe-vector*-set!) v:expr index:expr val:expr))
|
||||
(pattern (~and form ((~and op (~or vector-set! unsafe-vector-set! unsafe-vector*-set!)) v:expr index:expr val:expr))
|
||||
(match (single-value #'v)
|
||||
[(tc-result1: (and vec-t (app resolve (Is-a: (HeterogeneousVector: es)))))
|
||||
(tc/hetero-set! #'index es #'val vec-t "vector")]
|
||||
(tc/hetero-set! #'index es #'val vec-t "vector" #'op)]
|
||||
[v-ty (tc/app-regular #'form expected)]))
|
||||
(pattern (~and form ((~or vector-immutable vector) args:expr ...))
|
||||
(pattern (~and form ((~and op (~or vector-immutable vector)) args:expr ...))
|
||||
(match expected
|
||||
[(tc-result1: (app resolve (Is-a: (Vector: t))))
|
||||
(ret (make-HeterogeneousVector
|
||||
(for/list ([e (in-syntax #'(args ...))])
|
||||
(tc-expr/check e (ret t))
|
||||
t)))]
|
||||
(define arg-tys
|
||||
(for/list ([e (in-syntax #'(args ...))])
|
||||
(tc-expr/check e (ret t))
|
||||
t))
|
||||
(define return-ty
|
||||
(make-HeterogeneousVector arg-tys))
|
||||
(add-typeof-expr #'op (ret (->* arg-tys return-ty)))
|
||||
(ret return-ty)]
|
||||
[(tc-result1: (app resolve (Is-a: (HeterogeneousVector: ts))))
|
||||
(cond
|
||||
[(= (length ts) (syntax-length #'(args ...)))
|
||||
(ret
|
||||
(make-HeterogeneousVector
|
||||
(for/list ([e (in-syntax #'(args ...))]
|
||||
[t (in-list ts)])
|
||||
(tc-expr/check/t e (ret t))))
|
||||
-true-propset)]
|
||||
(define arg-tys
|
||||
(for/list ([e (in-syntax #'(args ...))]
|
||||
[t (in-list ts)])
|
||||
(tc-expr/check/t e (ret t))))
|
||||
(define return-ty
|
||||
(make-HeterogeneousVector arg-tys))
|
||||
(add-typeof-expr #'op (ret (->* arg-tys return-ty)))
|
||||
(ret return-ty -true-propset)]
|
||||
[else
|
||||
(tc-error/expr
|
||||
"expected vector with ~a elements, but got ~a"
|
||||
|
|
@ -136,7 +151,11 @@
|
|||
[_ (continue)])]
|
||||
;; since vectors are mutable, if there is no expected type, we want to generalize the element type
|
||||
[(or #f (tc-any-results: _) (tc-result1: _))
|
||||
(ret (make-HeterogeneousVector
|
||||
(for/list ((e (in-syntax #'(args ...))))
|
||||
(generalize (tc-expr/t e)))))]
|
||||
(define arg-tys
|
||||
(for/list ((e (in-syntax #'(args ...))))
|
||||
(generalize (tc-expr/t e))))
|
||||
(define return-ty
|
||||
(make-HeterogeneousVector arg-tys))
|
||||
(add-typeof-expr #'op (ret (->* arg-tys return-ty)))
|
||||
(ret return-ty)]
|
||||
[_ (ret Err)])))
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@
|
|||
"utils.rkt"
|
||||
syntax/parse syntax/stx racket/match racket/sequence
|
||||
(typecheck signatures tc-funapp error-message)
|
||||
(types abbrev utils substitute)
|
||||
(types abbrev type-table utils substitute)
|
||||
(rep type-rep)
|
||||
(env tvar-env)
|
||||
(prefix-in i: (infer infer))
|
||||
|
|
@ -79,58 +79,79 @@
|
|||
[_ (tc/app-regular #'form expected)])))
|
||||
;; special case for `list'
|
||||
(pattern
|
||||
(list . args)
|
||||
((~and op-name list) . args)
|
||||
(let ([args-list (syntax->list #'args)])
|
||||
(match expected
|
||||
[(tc-result1: t)
|
||||
(match t
|
||||
[(List: ts)
|
||||
(cond
|
||||
[(= (length ts) (length args-list))
|
||||
(for ([arg (in-list args-list)]
|
||||
[t (in-list ts)])
|
||||
(tc-expr/check arg (ret t)))
|
||||
(ret t)]
|
||||
[else
|
||||
(expected-but-got t (-Tuple (map tc-expr/t args-list)))
|
||||
(ret t)])]
|
||||
[_
|
||||
(define vs (map (λ (_) (gensym)) args-list))
|
||||
(define l-type (-Tuple (map make-F vs)))
|
||||
;; We want to infer the largest vs that are still under the element types
|
||||
(define substs (i:infer vs null (list l-type) (list t) (-values (list (-> l-type Univ)))
|
||||
#:multiple? #t))
|
||||
(cond
|
||||
[substs
|
||||
(define result
|
||||
(for*/first ([subst (in-list substs)]
|
||||
[argtys (in-value (for/list ([arg (in-list args-list)]
|
||||
[v (in-list vs)])
|
||||
(tc-expr/check/t? arg (ret (subst-all subst (make-F v))))))]
|
||||
#:when (andmap values argtys))
|
||||
(ret (-Tuple argtys))))
|
||||
(or result
|
||||
(begin (expected-but-got t (-Tuple (map tc-expr/t args-list)))
|
||||
(fix-results expected)))]
|
||||
[else (ret (-Tuple (map tc-expr/t args-list)))])])]
|
||||
[_ (ret (-Tuple (map tc-expr/t args-list)))])))
|
||||
(match expected
|
||||
[(tc-result1: t)
|
||||
(match t
|
||||
[(List: ts)
|
||||
(cond
|
||||
[(= (length ts) (length args-list))
|
||||
(for ([arg (in-list args-list)]
|
||||
[t (in-list ts)])
|
||||
(tc-expr/check arg (ret t)))
|
||||
(add-typeof-expr #'op-name (ret (->* ts t)))
|
||||
(ret t)]
|
||||
[else
|
||||
(expected-but-got t (-Tuple (map tc-expr/t args-list)))
|
||||
(ret t)])]
|
||||
[_
|
||||
(define vs (map (λ (_) (gensym)) args-list))
|
||||
(define l-type (-Tuple (map make-F vs)))
|
||||
;; We want to infer the largest vs that are still under the element types
|
||||
(define substs (i:infer vs null (list l-type) (list t) (-values (list (-> l-type Univ)))
|
||||
#:multiple? #t))
|
||||
(cond
|
||||
[substs
|
||||
(define result
|
||||
(for*/first ([subst (in-list substs)]
|
||||
[arg-tys (in-value (for/list ([arg (in-list args-list)]
|
||||
[v (in-list vs)])
|
||||
(tc-expr/check/t? arg (ret (subst-all subst (make-F v))))))]
|
||||
#:when (andmap values arg-tys))
|
||||
(define return-ty (-Tuple arg-tys))
|
||||
(add-typeof-expr #'op-name (ret (->* arg-tys return-ty)))
|
||||
(ret return-ty)))
|
||||
(or result
|
||||
(begin (expected-but-got t (-Tuple (map tc-expr/t args-list)))
|
||||
(fix-results expected)))]
|
||||
[else
|
||||
(define arg-tys (map tc-expr/t args-list))
|
||||
(define return-ty (-Tuple arg-tys))
|
||||
(add-typeof-expr #'op-name (ret (->* arg-tys return-ty)))
|
||||
(ret return-ty)])])]
|
||||
[_
|
||||
(define arg-tys (map tc-expr/t args-list))
|
||||
(define return-ty (-Tuple arg-tys))
|
||||
(add-typeof-expr #'op-name (ret (->* arg-tys return-ty)))
|
||||
(ret return-ty)])))
|
||||
;; special case for `list*'
|
||||
(pattern (list* (~between args:expr 1 +inf.0) ...)
|
||||
(match-let* ([(list tys ... last) (stx-map tc-expr/t #'(args ...))])
|
||||
(ret (foldr -pair last tys))))
|
||||
(pattern ((~and op-name list*) (~between args:expr 1 +inf.0) ...)
|
||||
(match-let* ([(and arg-tys (list tys ... last)) (stx-map tc-expr/t #'(args ...))])
|
||||
(define return-ty (foldr -pair last tys))
|
||||
(add-typeof-expr #'op-name (ret (->* arg-tys return-ty)))
|
||||
(ret return-ty)))
|
||||
;; special case for `reverse' to propagate expected type info
|
||||
(pattern ((~and fun (~or reverse k:reverse)) arg)
|
||||
(match expected
|
||||
[(tc-result1: (Listof: _))
|
||||
(tc-expr/check #'arg expected)]
|
||||
[(tc-result1: (and return-ty (Listof: _)))
|
||||
(begin0
|
||||
(tc-expr/check #'arg expected)
|
||||
(add-typeof-expr #'fun (ret (-> return-ty return-ty))))]
|
||||
[(tc-result1: (List: ts))
|
||||
(tc-expr/check #'arg (ret (-Tuple (reverse ts))))
|
||||
(ret (-Tuple ts))]
|
||||
(define arg-ty (-Tuple (reverse ts)))
|
||||
(define return-ty (-Tuple ts))
|
||||
(tc-expr/check #'arg (ret arg-ty))
|
||||
(add-typeof-expr #'fun (ret (-> arg-ty return-ty)))
|
||||
(ret return-ty)]
|
||||
[_
|
||||
(match (single-value #'arg)
|
||||
[(tc-result1: (List: ts))
|
||||
(ret (-Tuple (reverse ts)))]
|
||||
[(tc-result1: (and arg-ty (List: ts)))
|
||||
(define return-ty (-Tuple (reverse ts)))
|
||||
(add-typeof-expr #'fun (ret (-> arg-ty return-ty)))
|
||||
(ret return-ty)]
|
||||
[(tc-result1: (and r (Listof: t)))
|
||||
(add-typeof-expr #'fun (ret (-> r r)))
|
||||
(ret r)]
|
||||
[arg-ty
|
||||
(tc/funapp #'fun #'(arg) (tc-expr/t #'fun) (list arg-ty) expected)])])))
|
||||
|
|
|
|||
|
|
@ -51,10 +51,12 @@
|
|||
(list (ret Univ) (single-value #'arg))
|
||||
expected)]))
|
||||
;; special-case for not - flip the props
|
||||
(pattern ((~or false? not) arg)
|
||||
(pattern ((~and op-name (~or false? not)) arg)
|
||||
(match (single-value #'arg)
|
||||
[(tc-result1: t (PropSet: p+ p-) _)
|
||||
(ret -Boolean (make-PropSet p- p+))]))
|
||||
(define new-prop (make-PropSet p- p+))
|
||||
(add-typeof-expr #'op-name (ret (-> Univ -Boolean)))
|
||||
(ret -Boolean new-prop)]))
|
||||
;; 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
|
||||
|
|
|
|||
|
|
@ -4,8 +4,9 @@
|
|||
"signatures.rkt"
|
||||
"utils.rkt"
|
||||
syntax/parse racket/match racket/sequence
|
||||
(typecheck signatures tc-funapp)
|
||||
(types base-abbrev utils)
|
||||
(typecheck signatures tc-funapp tc-metafunctions)
|
||||
(types base-abbrev abbrev type-table utils)
|
||||
(rep values-rep)
|
||||
|
||||
(for-label racket/base))
|
||||
|
||||
|
|
@ -18,34 +19,51 @@
|
|||
(define-tc/app-syntax-class (tc/app-values expected)
|
||||
#:literal-sets (values-literals)
|
||||
;; call-with-values
|
||||
(pattern (call-with-values prod con)
|
||||
(match (tc/funapp #'prod #'() (tc-expr/t #'prod) null #f)
|
||||
(pattern ((~and op-name call-with-values) prod con)
|
||||
#:do [(define prod-ty (tc-expr/t #'prod))]
|
||||
(match (tc/funapp #'prod #'() prod-ty null #f)
|
||||
[(tc-results: tcrs #f)
|
||||
(tc/funapp #'con #'(prod) (tc-expr/t #'con)
|
||||
(for/list ([tcr (in-list tcrs)])
|
||||
(-tc-results (list tcr) #f))
|
||||
expected)]
|
||||
(define con-ty (tc-expr/t #'con))
|
||||
(define r
|
||||
(tc/funapp #'con #'(prod) con-ty
|
||||
(for/list ([tcr (in-list tcrs)])
|
||||
(-tc-results (list tcr) #f))
|
||||
expected))
|
||||
(define return-ty (tc-results->values r))
|
||||
(add-typeof-expr #'op-name (ret (-> prod-ty con-ty return-ty)))
|
||||
r]
|
||||
[(tc-results: _ (? RestDots?))
|
||||
(tc-error/expr "`call-with-values` with ... is not supported")]
|
||||
[(tc-any-results: _)
|
||||
(tc/app-regular this-syntax 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)
|
||||
(match expected
|
||||
[(or #f (tc-any-results: _)) (single-value #'arg)]
|
||||
[(tc-result1: tp)
|
||||
(single-value #'arg expected)]
|
||||
;; Type check the argument, to find other errors
|
||||
[_ (single-value #'arg)]))
|
||||
(pattern ((~and op-name values) arg)
|
||||
(let ([tc-result
|
||||
(match expected
|
||||
[(or #f (tc-any-results: _))
|
||||
(single-value #'arg)]
|
||||
[(tc-result1: tp)
|
||||
(single-value #'arg expected)]
|
||||
;; Type check the argument, to find other errors
|
||||
[_ (single-value #'arg)])])
|
||||
(define arg-ty
|
||||
;; match never fails; `single-value` always returns a tc-result1
|
||||
(match tc-result [(tc-result1: t) t]))
|
||||
(add-typeof-expr #'op-name (ret (-> arg-ty arg-ty)))
|
||||
tc-result))
|
||||
;; handle `values' specially
|
||||
(pattern (values . args)
|
||||
(pattern ((~and op-name values) . args)
|
||||
(match expected
|
||||
[(or (tc-results: tcrs #f)
|
||||
(bind tcrs '()))
|
||||
(-tc-results
|
||||
(for/list ([arg (in-syntax #'args)]
|
||||
[tcr (in-list/rest tcrs #f)])
|
||||
(match (single-value arg (and tcr (-tc-results (list tcr) #f)))
|
||||
[(tc-results: (list res) #f) res]))
|
||||
#f)])))
|
||||
(define res
|
||||
(-tc-results
|
||||
(for/list ([arg (in-syntax #'args)]
|
||||
[tcr (in-list/rest tcrs #f)])
|
||||
(match (single-value arg (and tcr (-tc-results (list tcr) #f)))
|
||||
[(tc-results: (list res) #f) res])) #f))
|
||||
(define return-ty (tc-results->values res))
|
||||
(define arg-tys (match return-ty [(Values: (list (Result: t* _ _) ...)) t*]))
|
||||
(add-typeof-expr #'op-name (ret (->* arg-tys return-ty)))
|
||||
res])))
|
||||
|
|
|
|||
|
|
@ -3,7 +3,7 @@
|
|||
(require (rename-in "../utils/utils.rkt" [infer r:infer])
|
||||
racket/match racket/list
|
||||
(typecheck signatures tc-app-helper)
|
||||
(types utils abbrev substitute)
|
||||
(types utils abbrev substitute type-table)
|
||||
(utils tc-utils)
|
||||
(rep type-rep core-rep values-rep)
|
||||
(r:infer infer))
|
||||
|
|
@ -67,8 +67,9 @@
|
|||
;; Takes a possible substitution and comuptes
|
||||
;; the substituted range type if it is not #f
|
||||
(define (finish substitution)
|
||||
(and substitution (do-ret (subst-all substitution rng))))
|
||||
|
||||
(begin0
|
||||
(and substitution (do-ret (subst-all substitution rng)))
|
||||
(add-typeof-expr f (ret (make-Fun (list arrow))))))
|
||||
(finish
|
||||
(infer vars dotted-vars
|
||||
(list (-Tuple* arg-tys full-tail-ty))
|
||||
|
|
|
|||
|
|
@ -42,14 +42,17 @@
|
|||
"test-utils.rkt"
|
||||
typed-racket/utils/utils
|
||||
racket/base racket/match
|
||||
syntax/id-table
|
||||
(rep core-rep)
|
||||
(rename-in (types prop-ops tc-result printer subtype) [ret raw-ret])
|
||||
(only-in (types type-table) type-of)
|
||||
syntax/parse
|
||||
(for-template (only-in typed-racket/typed-racket do-standard-inits))
|
||||
(typecheck typechecker check-below tc-metafunctions)
|
||||
(utils mutated-vars tc-utils)
|
||||
(env lexical-env mvar-env))
|
||||
(provide
|
||||
test-type-table
|
||||
test-literal test-literal/fail
|
||||
test test/proc test/fail)
|
||||
|
||||
|
|
@ -122,6 +125,38 @@
|
|||
(define golden (golden-fun expanded-expr))
|
||||
(check-tc-results result golden #:name "tc-expr"))
|
||||
|
||||
;; test-type-table : syntax? (listof (cons/c identifier? tc-results?)) -> void?
|
||||
;; Typecheck the given expression
|
||||
;; and assert that the type-table has an entry for every identifier
|
||||
;; in the given association list.
|
||||
;;
|
||||
;; Example: `(test-type-table expr (list (cons f t)))` will
|
||||
;; 1. type-check `expr`
|
||||
;; 2. search `expr` for occurrences of `f`
|
||||
;; 3. check that the type-table entry for `f` matches `t`
|
||||
(define (test-type-table expr assoc)
|
||||
(define expanded-expr
|
||||
(let ([expr+ (tr-expand expr)])
|
||||
(begin (tc expr+ #f) expr+)))
|
||||
(define expected-results
|
||||
(make-free-id-table assoc))
|
||||
(let loop ([x expanded-expr]) ;; loop : any/c -> void?
|
||||
(cond
|
||||
[(and (identifier? x)
|
||||
(free-id-table-ref expected-results x #f))
|
||||
=> (λ (expected)
|
||||
(define actual (type-of x))
|
||||
(define test-name (format "(type-of ~a)" (syntax-e x)))
|
||||
(check-tc-results actual expected #:name test-name))]
|
||||
[(syntax? x)
|
||||
(loop (syntax-e x))]
|
||||
[(list? x)
|
||||
(map loop x)]
|
||||
[(pair? x)
|
||||
(loop (car x))
|
||||
(loop (cdr x))]
|
||||
[else
|
||||
(void)])))
|
||||
|
||||
;; test/fail syntax? tc-results? (or/c string? regexp?) (option/c tc-results?)
|
||||
;; [(listof (list id type))] -> void?
|
||||
|
|
@ -278,6 +313,15 @@
|
|||
(test-phase1 #,(syntax/loc #'lit (LITERAL/FAIL lit))
|
||||
(test-literal/fail (quote-syntax lit) msg.v ex.v)))]))
|
||||
|
||||
(define-syntax (tc/type-table stx)
|
||||
(syntax-parse stx
|
||||
[(_ e:expr ([k v] ...))
|
||||
(quasisyntax/loc stx
|
||||
(test-phase1 e
|
||||
(test-type-table
|
||||
(quote-syntax e)
|
||||
(list (cons (quote-syntax k) (ret v)) ...))))]))
|
||||
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
|
|
@ -4490,4 +4534,99 @@
|
|||
(-prefab 'foo (-opt -String))
|
||||
#:expected (-prefab 'foo (-opt -String))]
|
||||
)
|
||||
|
||||
(test-suite
|
||||
"type-table tests"
|
||||
;; tc-app-apply
|
||||
(tc/type-table (apply values '(0))
|
||||
([values (t:-> (-val 0) (-val 0))]))
|
||||
(tc/type-table (apply + '(0))
|
||||
([values (t:-> (-val 0) (-val 0))]))
|
||||
|
||||
;; tc-app-hetero
|
||||
(tc/type-table (void ;; vector-ref on heterogeneous vectors
|
||||
(vector-ref (ann '#(A B) (Vector 'A 'B)) 0)
|
||||
(unsafe-vector-ref (ann (vector 'A 'B) (Vector 'A 'B)) 0)
|
||||
(unsafe-vector*-ref (ann (vector 'A 'B) (Vector 'A 'B)) 1))
|
||||
([vector-ref (t:-> (-vec* (-val 'A) (-val 'B)) -Fixnum (-val 'A))]
|
||||
[unsafe-vector-ref (t:-> (-vec* (-val 'A) (-val 'B)) -Fixnum (-val 'A))]
|
||||
[unsafe-vector*-ref (t:-> (-vec* (-val 'A) (-val 'B)) -Fixnum (-val 'B))]))
|
||||
(tc/type-table (void ;; vector-set! on heterogeneous vectors
|
||||
(vector-set! (ann (vector 'A 'B) (Vector Symbol 'B)) 0 'X)
|
||||
(unsafe-vector-set! (ann (vector 'C 'D) (Vector Symbol 'D)) 0 'X)
|
||||
(unsafe-vector*-set! (ann (vector 'E 'F) (Vector 'E Symbol)) 1 'X))
|
||||
([vector-set! (t:-> (-vec* -Symbol (-val 'B)) -Fixnum -Symbol -Void)]
|
||||
[unsafe-vector-set! (t:-> (-vec* -Symbol (-val 'D)) -Fixnum -Symbol -Void)]
|
||||
[unsafe-vector*-set! (t:-> (-vec* (-val 'E) -Symbol) -Fixnum -Symbol -Void)]))
|
||||
(tc/type-table (vector-set! (ann (vector 'a 'b) (Vector Symbol Symbol)) (+ -1 2) 'c)
|
||||
;; test when the index for vector-set! isn't know
|
||||
([vector-set! (t:-> (-vec* -Symbol -Symbol) -Fixnum (-val 'c) -Void)]))
|
||||
(tc/type-table (void ;; vector constructor, returning heterogeneous vector
|
||||
(ann (vector 'A 'B) (Vectorof Symbol))
|
||||
(ann (vector-immutable 'A 'B) (Vectorof Symbol)))
|
||||
([vector (t:-> -Symbol -Symbol (-vec* -Symbol -Symbol))]
|
||||
[vector-immutable (t:-> -Symbol -Symbol (-vec* -Symbol -Symbol))]))
|
||||
(tc/type-table (void ;; vector constructor, returning heterogeneous vector
|
||||
(ann (vector 'A 'B) (Vector 'A 'B))
|
||||
(ann (vector-immutable 'A 'B) (Vector 'A 'B)))
|
||||
([vector (t:-> (-val 'A) (-val 'B) (-vec* (-val 'A) (-val 'B)))]
|
||||
[vector-immutable (t:-> (-val 'A) (-val 'B) (-vec* (-val 'A) (-val 'B)))]))
|
||||
(tc/type-table (void ;; vector constructor, no expected type
|
||||
(vector 'A 'B)
|
||||
(vector-immutable 'A 'B))
|
||||
([vector (t:-> -Symbol -Symbol (-vec* -Symbol -Symbol))]
|
||||
[vector-immutable (t:-> -Symbol -Symbol (-vec* -Symbol -Symbol))]))
|
||||
|
||||
;; tc-app-list
|
||||
;;; list
|
||||
(tc/type-table (ann (list 'A 'B) (List Symbol Symbol))
|
||||
([list (t:-> -Symbol -Symbol (-lst* -Symbol -Symbol))]))
|
||||
(tc/type-table (ann (list 'A) Any)
|
||||
([list (t:-> Univ (-lst* Univ))]))
|
||||
(tc/type-table (list 'A 'B)
|
||||
([list (t:-> (-val 'A) (-val 'B) (-lst* (-val 'A) (-val 'B)))]))
|
||||
;;; list*
|
||||
(tc/type-table (list* #true #false)
|
||||
([list* (t:-> (-val #true) (-val #false) (-pair (-val #true) (-val #false)))]))
|
||||
(tc/type-table (list* "A" "B" (list "C"))
|
||||
([list* (t:-> -String -String (-lst* -String) (-lst* -String -String -String))]))
|
||||
;;; reverse
|
||||
(tc/type-table (ann (reverse '("A" "B")) (Listof String))
|
||||
([reverse (t:-> (-lst -String) (-lst -String))]))
|
||||
(tc/type-table (ann (reverse '(A B)) (List 'B 'A))
|
||||
([reverse (t:-> (-lst* (-val 'A) (-val 'B)) (-lst* (-val 'B) (-val 'A)))]))
|
||||
(tc/type-table (reverse (ann '(A B) (List 'A 'B)))
|
||||
([reverse (t:-> (-lst* (-val 'A) (-val 'B)) (-lst* (-val 'B) (-val 'A)))]))
|
||||
(tc/type-table (reverse (ann '("A" "B") (Listof String)))
|
||||
([reverse (t:-> (-lst -String) (-lst -String))]))
|
||||
|
||||
;; tc-app-special
|
||||
(tc/type-table (false? #true)
|
||||
([false? (t:-> Univ -Boolean)]))
|
||||
(tc/type-table (false? #false)
|
||||
([false? (t:-> Univ -Boolean)]))
|
||||
(tc/type-table (not #true)
|
||||
([not (t:-> Univ -Boolean)]))
|
||||
(tc/type-table (not #false)
|
||||
([not (t:-> Univ -Boolean)]))
|
||||
|
||||
;; tc-app-values
|
||||
(tc/type-table (values 0)
|
||||
([values (t:-> (-val 0) (-values (list (-val 0))))]))
|
||||
;; TODO tests fail because propsets are somehow different (2017-12-06)
|
||||
;(tc/type-table (values 0 0)
|
||||
; ([values (t:-> (-val 0) (-val 0) (-values (list (-val 0 ) (-val 0))))]))
|
||||
;(tc/type-table (call-with-values (λ () 'A) symbol->string)
|
||||
; ([call-with-values (->* (list (t:-> (-val 'A)) (t:-> -Symbol -String)) -String)]))
|
||||
;(tc/type-table (call-with-values (λ () "hello") (λ: ((x : String)) "world"))
|
||||
; ([call-with-values (t:-> (t:-> -String) (t:-> -String -String) -String)]))
|
||||
;(tc/type-table (call-with-values (λ () (values 0 0)) (λ: ((x : Zero) (y : Zero)) 0))
|
||||
; ([call-with-values (t:-> (t:-> (-values (list (-val 0) (-val 0))))
|
||||
; (t:-> (-val 0) (-val 0) (-val 0))
|
||||
; (-val 0))]))
|
||||
;(tc/type-table (call-with-values (λ () (values "a" "b")) (λ: ((x : String) (y : String)) (string-append x y)))
|
||||
; ([call-with-values (t:-> (t:-> (-values (list -String -String)))
|
||||
; (t:-> -String -String -String)
|
||||
; -String)]))
|
||||
)
|
||||
))
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user