diff --git a/collects/tests/typed-scheme/fail/bad-type-app.ss b/collects/tests/typed-scheme/fail/bad-type-app.ss new file mode 100644 index 00000000..581e73e5 --- /dev/null +++ b/collects/tests/typed-scheme/fail/bad-type-app.ss @@ -0,0 +1,15 @@ +#; +(exn-pred exn:fail:syntax?) +#lang typed-scheme + +(define-typed-struct type ()) + +(define-typed-struct (type-base type) ([name : Symbol]) #:transparent) +(define-typed-struct (type-var type) ([uniq : (U Symbol Number)]) #:transparent) +(define-typed-struct (type-dots type) ([base : type]) #:transparent) + +(define-typed-struct (type-fun type) ([args : (Listof type)] [ret : type]) #:transparent) +(define-typed-struct (type-un type) ([cases : (Listof type)]) #:transparent) +(define-typed-struct (type-vals type) ([elems : (Listof type)]) #:transparent) + +(define-typed-struct (type-poly type) ([vars : (Listof (U (type-dots type-var) type-var))])) \ No newline at end of file diff --git a/collects/tests/typed-scheme/unit-tests/all-tests.ss b/collects/tests/typed-scheme/unit-tests/all-tests.ss index 5c3a5006..2e069f7f 100644 --- a/collects/tests/typed-scheme/unit-tests/all-tests.ss +++ b/collects/tests/typed-scheme/unit-tests/all-tests.ss @@ -2,19 +2,15 @@ (require "test-utils.ss" + "typecheck-tests.ss" "subtype-tests.ss" ;; done "type-equal-tests.ss" ;; done "remove-intersect-tests.ss" ;; done "parse-type-tests.ss" ;; done "type-annotation-test.ss" ;; done - "typecheck-tests.ss" "module-tests.ss" "infer-tests.ss") -(require (for-syntax scheme/base mzlib/etc)) - -(require (for-syntax (private utils))) - (require (private planet-requires)) (require (schemeunit)) @@ -25,52 +21,21 @@ (apply test-suite "Unit Tests" - (map (lambda (f) (f)) - (list - subtype-tests - type-equal-tests - restrict-tests - remove-tests - parse-type-tests - type-annotation-tests - typecheck-tests - module-tests - fv-tests)))) + (for/list ([f (list + typecheck-tests + subtype-tests + type-equal-tests + restrict-tests + remove-tests + parse-type-tests + type-annotation-tests + module-tests + fv-tests)]) + (f)))) -(define-go - subtype-tests - type-equal-tests - restrict-tests - remove-tests - parse-type-tests - type-annotation-tests - typecheck-tests - module-tests - fv-tests) - -(define (fast) - (run - subtype-tests - type-equal-tests - restrict-tests - remove-tests - parse-type-tests - type-annotation-tests - typecheck-tests - module-tests - fv-tests)) - -(define (faster) - (run - subtype-tests - type-equal-tests - restrict-tests - remove-tests - parse-type-tests - type-annotation-tests - fv-tests)) +(define-go (lambda () unit-tests)) ;(go/gui) diff --git a/collects/tests/typed-scheme/unit-tests/infer-tests.ss b/collects/tests/typed-scheme/unit-tests/infer-tests.ss index bcf33ad3..27726a74 100644 --- a/collects/tests/typed-scheme/unit-tests/infer-tests.ss +++ b/collects/tests/typed-scheme/unit-tests/infer-tests.ss @@ -1,10 +1,10 @@ #lang scheme/base (require "test-utils.ss" (for-syntax scheme/base)) -(require (private planet-requires type-effect-convenience type-rep unify union infer-ops) +(require (private planet-requires type-effect-convenience type-rep unify union infer-ops type-utils) (prefix-in table: (private tables))) (require (schemeunit)) -(define (fv . args) (list)) + (provide fv-tests) diff --git a/collects/tests/typed-scheme/unit-tests/parse-type-tests.ss b/collects/tests/typed-scheme/unit-tests/parse-type-tests.ss index e279d74b..748603c4 100644 --- a/collects/tests/typed-scheme/unit-tests/parse-type-tests.ss +++ b/collects/tests/typed-scheme/unit-tests/parse-type-tests.ss @@ -1,10 +1,12 @@ #lang scheme/base (require "test-utils.ss" (for-syntax scheme/base)) (require (private planet-requires type-comparison parse-type type-rep - type-effect-convenience tc-utils type-environments - type-name-env init-envs union)) + tc-utils type-environments type-alias-env + type-name-env init-envs union type-utils)) -(require (except-in (private base-env))) +(require (rename-in (private type-effect-convenience) [-> t:->]) + (except-in (private base-types) Un) + (for-template (private base-types))) (require (schemeunit)) @@ -12,22 +14,24 @@ (define-syntax (run-one stx) (syntax-case stx () - [(_ ty) #'(parameterize ([current-tvars initial-tvar-env] - [current-orig-stx #'here] - [orig-module-stx #'here] - [expanded-module-stx #'here]) - (parse-type (syntax ty)))])) + [(_ ty) (syntax/loc stx + (parameterize ([current-tvars initial-tvar-env] + [current-orig-stx #'ty] + [orig-module-stx #'ty] + [expanded-module-stx #'ty] + [delay-errors? #f]) + (parse-type (syntax ty))))])) (define-syntax (pt-test stx) (syntax-case stx () - [(_ ts tv) #'(pt-test ts tv () initial-tvar-env)] - [(_ ts tv tys) #'(pt-test ts tv tys initial-tvar-env)] - [(_ ty-stx ty-val ((nm ty) ...) tvar-env) - #`(test-case #,(format "~a" (syntax->datum #'ty-stx)) - (parameterize ([current-tvars tvar-env]) - #;(initialize-type-name-env initial-type-names) - (register-type-name #'nm ty) ... - (check type-equal? (parse-type (syntax ty-stx)) ty-val)))])) + [(_ ts tv) (syntax/loc stx (pt-test ts tv initial-tvar-env))] + [(_ ty-stx ty-val tvar-env) + (quasisyntax/loc + stx + (test-case #,(format "~a" (syntax->datum #'ty-stx)) + (parameterize ([current-tvars tvar-env] + [delay-errors? #f]) + (check type-equal? (parse-type (quote-syntax ty-stx)) ty-val))))])) (define-syntax pt-tests (syntax-rules () @@ -42,13 +46,13 @@ [Any Univ] [(All (Number) Number) (-poly (a) a)] [(Number . Number) (-pair N N)] - [(list-of Boolean) (make-Listof B)] + [(Listof Boolean) (make-Listof B)] [(Vectorof (Listof Symbol)) (make-Vector (make-Listof Sym))] [(pred Number) (make-pred-ty N)] [(values Number Boolean Number) (-values (list N B N))] - [(Number -> Number) (-> N N)] - [(Number -> Number) (-> N N)] - [(Number Number Number Boolean -> Number) (N N N B . -> . N)] + [(Number -> Number) (t:-> N N)] + [(Number -> Number) (t:-> N N)] + [(Number Number Number Boolean -> Number) (N N N B . t:-> . N)] [(Number Number Number .. -> Boolean) ((list N N) N . ->* . B)] ;[((. Number) -> Number) (->* (list) N N)] ;; not legal syntax [(Un Number Boolean) (Un N B)] @@ -62,17 +66,16 @@ [#f (-val #f)] ["foo" (-val "foo")] - [(poly-lst Number) (make-Listof N) ((poly-lst (-poly (a) (make-Listof a)))) - #;(extend-env (list 'poly-lst) (list (-poly (a) (make-Listof a))) initial-type-names)] + [(Listof Number) (make-Listof N)] - [a (-v a) () (extend-env (list 'a) (list (-v a)) + [a (-v a) (extend-env (list 'a) (list (-v a)) initial-tvar-env)] )) -(define (go) - (run parse-type-tests)) +(define-go + parse-type-tests) diff --git a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss index f2ab5a97..47a81f7e 100644 --- a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss +++ b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss @@ -17,7 +17,11 @@ -(provide typecheck-tests tc-expr/expand) +(provide typecheck-tests g tc-expr/expand) + +(define (g) (run typecheck-tests)) + +(define-namespace-anchor anch) ;; check that a literal typechecks correctly @@ -30,11 +34,11 @@ (define-syntax (tc-expr/expand stx) (syntax-case stx () [(_ e) - (with-syntax ([e* (local-expand #'e 'expression '())]) - #'(let ([ex #'e*]) + #`(parameterize ([delay-errors? #f] + [current-namespace (namespace-anchor->namespace anch)]) + (let ([ex (expand 'e)]) (find-mutated-vars ex) - (parameterize ([delay-errors? #f]) - (tc-expr ex))))])) + (tc-expr ex)))])) ;; check that an expression typechecks correctly (define-syntax (tc-e stx) @@ -102,7 +106,7 @@ [tc-e '(#t #f) (-lst* (-val #t) (-val #f))] [tc-e (plambda: (a) ([l : (Listof a)]) (car l)) (make-Poly '(a) (-> (make-Listof (-v a)) (-v a)))] - [tc-e #{(lambda: ([l : (Listof a)]) (car l)) PROP typechecker:plambda (a)} + [tc-e (plambda: (a) ([l : (Listof a)]) (car l)) (make-Poly '(a) (-> (make-Listof (-v a)) (-v a)))] [tc-e (case-lambda: [([a : Number] [b : Number]) (+ a b)]) (-> N N N)] [tc-e (let: ([x : Number 5]) x) N (-vet #'x) (-vef #'x)] @@ -417,7 +421,15 @@ [tc-err ((plambda: (a) ([x : (a -> a)] [y : a]) (x y)) 5)] [tc-err ((plambda: (a) ([x : a] [y : a]) x) 5)] [tc-err (ann 5 : String)] + + ;; these don't work because the type annotation gets lost in marshalling + #| [tc-e (letrec-syntaxes+values () ([(#{x : Number}) (values 1)]) (add1 x)) N] + [tc-e (letrec-values ([(#{x : Number}) (values 1)]) (add1 x)) N] + [tc-e (letrec ([#{x : Number} (values 1)]) (add1 x)) N] + |# + + [tc-e (letrec: ([x : Number (values 1)]) (add1 x)) N] [tc-err (let ([x (add1 5)]) (set! x "foo")