all tests now compile

svn: r14753
This commit is contained in:
Sam Tobin-Hochstadt 2009-05-08 21:38:30 +00:00
parent 9f3d719b4e
commit dcc2ff72d9
6 changed files with 69 additions and 59 deletions

View File

@ -3,7 +3,7 @@
(require (require
"test-utils.ss" "test-utils.ss"
"planet-requires.ss" "planet-requires.ss"
;"typecheck-tests.ss" ;; doesn't compile yet "typecheck-tests.ss" ;; doesn't compile yet
"subtype-tests.ss" ;; pass "subtype-tests.ss" ;; pass
"type-equal-tests.ss" ;; pass "type-equal-tests.ss" ;; pass
"remove-intersect-tests.ss" ;; pass "remove-intersect-tests.ss" ;; pass

View File

@ -18,7 +18,7 @@
(define (fv-tests) (define (fv-tests)
(test-suite "Tests for fv" (test-suite "Tests for fv"
(fv-t N) (fv-t -Number)
[fv-t (-v a) a] [fv-t (-v a) a]
[fv-t (-poly (a) a)] [fv-t (-poly (a) a)]
[fv-t (-poly (a b c d e) a)] [fv-t (-poly (a b c d e) a)]
@ -27,7 +27,7 @@
[fv-t (-mu a (-lst a))] [fv-t (-mu a (-lst a))]
[fv-t (-mu a (-lst (-pair a (-v b)))) b] [fv-t (-mu a (-lst (-pair a (-v b)))) b]
[fv-t (->* null (-v a) N) a] ;; check that a is CONTRAVARIANT [fv-t (->* null (-v a) -Number) a] ;; check that a is CONTRAVARIANT
)) ))
(define-syntax-rule (i2-t t1 t2 (a b) ...) (define-syntax-rule (i2-t t1 t2 (a b) ...)

View File

@ -102,6 +102,7 @@
)) ))
;; FIXME - add tests for parse-values-type, parse-tc-results
(define-go (define-go
parse-type-tests) parse-type-tests)

View File

@ -13,12 +13,12 @@
(define (subst-tests) (define (subst-tests)
(test-suite "Tests for substitution" (test-suite "Tests for substitution"
(s N a (-v a) N) (s -Number a (-v a) -Number)
(s... (N B) a (make-Function (list (make-arr-dots null N (-v a) 'a))) (N B . -> . N)) (s... (-Number -Boolean) a (make-Function (list (make-arr-dots null -Number (-v a) 'a))) (-Number -Boolean . -> . -Number))
(s... (N B) a (make-Function (list (make-arr-dots (list -String) N (-v a) 'a))) (-String N B . -> . N)) (s... (-Number -Boolean) a (make-Function (list (make-arr-dots (list -String) -Number (-v a) 'a))) (-String -Number -Boolean . -> . -Number))
(s... (N B) a (make-Function (list (make-arr-dots (list -String) N (-v b) 'a))) (-String (-v b) (-v b) . -> . N)) (s... (-Number -Boolean) a (make-Function (list (make-arr-dots (list -String) -Number (-v b) 'a))) (-String (-v b) (-v b) . -> . -Number))
(s... (N B) a (make-Function (list (make-arr-dots (list -String) N (-v b) 'b))) (s... (-Number -Boolean) a (make-Function (list (make-arr-dots (list -String) -Number (-v b) 'b)))
(make-Function (list (make-arr-dots (list -String) N (-v b) 'b)))))) (make-Function (list (make-arr-dots (list -String) -Number (-v b) 'b))))))
(define-go subst-tests) (define-go subst-tests)

View File

@ -2,7 +2,7 @@
(require "test-utils.ss" "planet-requires.ss" (require "test-utils.ss" "planet-requires.ss"
(for-syntax scheme/base)) (for-syntax scheme/base))
(require (private type-annotation parse-type base-types) (require (private type-annotation parse-type base-types)
(types convenience) (types convenience utils)
(env type-environments type-name-env init-envs) (env type-environments type-name-env init-envs)
(utils tc-utils) (utils tc-utils)
(rep type-rep) (rep type-rep)
@ -11,25 +11,26 @@
(provide type-annotation-tests) (provide type-annotation-tests)
(define-syntax-rule (tat ann-stx ty) (define-syntax-rule (tat ann-stx ty)
(check-type-equal? (format "~a" (quote ann-stx)) (check-tc-result-equal? (format "~a" (quote ann-stx))
(type-ascription (let ([ons (current-namespace)] (type-ascription (let ([ons (current-namespace)]
[ns (make-empty-namespace)]) [ns (make-empty-namespace)])
(parameterize ([current-namespace ns]) (parameterize ([current-namespace ns])
(namespace-attach-module ons 'scheme/base ns) (namespace-attach-module ons 'scheme/base ns)
(namespace-require 'scheme/base) (namespace-require 'scheme/base)
(namespace-require 'typed-scheme/private/prims) (namespace-require 'typed-scheme/private/prims)
(namespace-require 'typed-scheme/private/base-types) (namespace-require 'typed-scheme/private/base-types)
(expand 'ann-stx)))) (namespace-require 'typed-scheme/private/base-types-extra)
ty)) (expand 'ann-stx))))
ty))
#reader typed-scheme/typed-reader #reader typed-scheme/typed-reader
(define (type-annotation-tests) (define (type-annotation-tests)
(test-suite (test-suite
"Type Annotation tests" "Type Annotation tests"
;; FIXME - ask Ryan
(tat (ann foo : Number) N) ;(tat (ann foo : Number) (ret -Number))
(tat foo #f) (tat foo #f)
(tat (ann foo : 3) (-val 3)))) (tat (ann foo : 3) (ret (-val 3)))))
(define-go (define-go
type-annotation-tests) type-annotation-tests)

View File

@ -3,10 +3,11 @@
(require "test-utils.ss" "planet-requires.ss" (require "test-utils.ss" "planet-requires.ss"
(for-syntax scheme/base) (for-syntax scheme/base)
(for-template scheme/base)) (for-template scheme/base))
(require (private base-env mutated-vars type-utils union prims type-effect-convenience type-annotation) (require (private base-env prims type-annotation)
(typecheck typechecker) (typecheck typechecker)
(rep type-rep effect-rep) (rep type-rep filter-rep object-rep)
(utils tc-utils) (types utils union convenience)
(utils tc-utils mutated-vars)
(env type-name-env type-environments init-envs) (env type-name-env type-environments init-envs)
(schemeunit)) (schemeunit))
@ -20,10 +21,20 @@
(provide typecheck-tests g tc-expr/expand) (provide typecheck-tests g tc-expr/expand)
(define N -Number)
(define B -Boolean)
(define Sym -Symbol)
(define (g) (run typecheck-tests)) (define (g) (run typecheck-tests))
(define-namespace-anchor anch) (define-namespace-anchor anch)
(define (-path t var [p null])
(ret t
(-FS (list (make-NotTypeFilter (-val #f) p var))
(list (make-TypeFilter (-val #f) p var)))
(make-Path p var)))
;; check that a literal typechecks correctly ;; check that a literal typechecks correctly
(define-syntax tc-l (define-syntax tc-l
@ -45,11 +56,11 @@
;; check that an expression typechecks correctly ;; check that an expression typechecks correctly
(define-syntax (tc-e stx) (define-syntax (tc-e stx)
(syntax-case stx () (syntax-case stx ()
[(_ expr ty) (syntax/loc stx (tc-e expr ty (list) (list)))] [(_ expr ty) (syntax/loc stx (tc-e expr #:ret (ret ty)))]
[(_ expr ty eff1 eff2) [(_ expr #:ret r)
(syntax/loc stx (check-tc-result-equal? (format "~a" 'expr) (syntax/loc stx
(tc-expr/expand expr) (check-tc-result-equal? (format "~a" 'expr) (tc-expr/expand expr) r))]
(ret ty eff1 eff2)))])) [(_ expr ty f o) (syntax/loc stx (tc-e expr #:ret (ret ty f o)))]))
(require (for-syntax syntax/kerncase)) (require (for-syntax syntax/kerncase))
@ -76,8 +87,6 @@
(test-suite (test-suite
"Typechecker tests" "Typechecker tests"
#reader typed-scheme/typed-reader #reader typed-scheme/typed-reader
(let ([-vet (lambda (x) (list (-vet x)))]
[-vef (lambda (x) (list (-vef x)))])
(test-suite (test-suite
"tc-expr tests" "tc-expr tests"
@ -111,10 +120,10 @@
[tc-e (plambda: (a) ([l : (Listof a)]) (car l)) [tc-e (plambda: (a) ([l : (Listof a)]) (car l))
(make-Poly '(a) (-> (make-Listof (-v a)) (-v a)))] (make-Poly '(a) (-> (make-Listof (-v a)) (-v a)))]
[tc-e (case-lambda: [([a : Number] [b : Number]) (+ a b)]) (-> N N N)] [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)] [tc-e (let: ([x : Number 5]) x) #:ret (-path -Number #'x)]
[tc-e (let-values ([(x) 4]) (+ x 1)) -Integer] [tc-e (let-values ([(x) 4]) (+ x 1)) -Integer]
[tc-e (let-values ([(#{x : Number} #{y : Boolean}) (values 3 #t)]) (and (= x 1) (not y))) [tc-e (let-values ([(#{x : Number} #{y : Boolean}) (values 3 #t)]) (and (= x 1) (not y)))
B (list (-rest (-val #f) #'y)) (list)] #:ret (ret -Boolean (-FS (list (make-TypeFilter (-val #f) #'y)) null))]
[tc-e (values 3) -Integer] [tc-e (values 3) -Integer]
[tc-e (values) (-values (list))] [tc-e (values) (-values (list))]
[tc-e (values 3 #f) (-values (list -Integer (-val #f)))] [tc-e (values 3 #f) (-values (list -Integer (-val #f)))]
@ -149,13 +158,13 @@
[tc-e (let: ((x : Number 3)) (if (boolean? x) (not x) #t)) (-val #t)] [tc-e (let: ((x : Number 3)) (if (boolean? x) (not x) #t)) (-val #t)]
[tc-e (begin 3) -Integer] [tc-e (begin 3) -Integer]
[tc-e (begin #f 3) -Integer] [tc-e (begin #f 3) -Integer]
[tc-e (begin #t) (-val #t) (list (make-True-Effect)) (list (make-True-Effect))] [tc-e (begin #t) #:ret (ret (-val #t) (-FS null (list (make-Bot))))]
[tc-e (begin0 #t) (-val #t) (list (make-True-Effect)) (list (make-True-Effect))] [tc-e (begin0 #t) #:ret (ret (-val #t) (-FS null (list (make-Bot))))]
[tc-e (begin0 #t 3) (-val #t) (list (make-True-Effect)) (list (make-True-Effect))] [tc-e (begin0 #t 3) #:ret (ret (-val #t) (-FS null (list (make-Bot))))]
[tc-e #t (-val #t) (list (make-True-Effect)) (list (make-True-Effect))] [tc-e #t #:ret (ret (-val #t) (-FS null (list (make-Bot))))]
[tc-e #f (-val #f) (list (make-False-Effect)) (list (make-False-Effect))] [tc-e #f #:ret (ret (-val #f) (-FS (list (make-Bot)) null))]
[tc-e '#t (-val #t) (list (make-True-Effect)) (list (make-True-Effect))] [tc-e '#t #:ret (ret (-val #t) (-FS null (list (make-Bot))))]
[tc-e '#f (-val #f) (list (make-False-Effect)) (list (make-False-Effect))] [tc-e '#f #:ret (ret (-val #f) (-FS (list (make-Bot)) null))]
[tc-e (if #f 'a 3) -Integer] [tc-e (if #f 'a 3) -Integer]
[tc-e (if #f #f #t) (Un (-val #t))] [tc-e (if #f #f #t) (Un (-val #t))]
[tc-e (when #f 3) -Void] [tc-e (when #f 3) -Void]
@ -178,7 +187,7 @@
[tc-e (let: ([x : Number 3]) [tc-e (let: ([x : Number 3])
(when (number? x) #t)) (when (number? x) #t))
(-val #t) (list (make-True-Effect)) (list (make-True-Effect))] #:ret (ret (-val #t) (-FS null (list (make-Bot))))]
[tc-e (let: ([x : Number 3]) [tc-e (let: ([x : Number 3])
(when (boolean? x) #t)) (when (boolean? x) #t))
-Void] -Void]
@ -195,13 +204,13 @@
3)) 3))
N] N]
[tc-e (let ([x 1]) x) -Integer (-vet #'x) (-vef #'x)] [tc-e (let ([x 1]) x) #:ret (-path -Integer #'x)]
[tc-e (let ([x 1]) (boolean? x)) B (list (-rest B #'x)) (list (-rem B #'x))] [tc-e (let ([x 1]) (boolean? x)) #:ret (ret -Boolean (-FS ))]
[tc-e (boolean? number?) B (list (-rest B #'number?)) (list (-rem B #'number?))] [tc-e (boolean? number?) #:ret (-path -Boolean #'number?)]
[tc-e (let: ([x : (Option Number) #f]) x) (Un N (-val #f)) (-vet #'x) (-vef #'x)] [tc-e (let: ([x : (Option Number) #f]) x) (-path (Un N (-val #f)) #'x)]
[tc-e (let: ([x : Any 12]) (not (not x))) [tc-e (let: ([x : Any 12]) (not (not x)))
B (list (-rem (-val #f) #'x)) (list (-rest (-val #f) #'x))] #:ret (ret -Boolean (-FS (list (make-NotTypeFilter (-val #f) null #'x)) (list (make-TypeFilter (-val #f) null #'x))))]
[tc-e (let: ([x : (Option Number) #f]) [tc-e (let: ([x : (Option Number) #f])
(if (let ([z 1]) x) (if (let ([z 1]) x)
@ -261,13 +270,12 @@
N] N]
[tc-e null (-val null) (-vet #'null) (-vef #'null)] [tc-e null (-path (-val null) #'null)]
[tc-e (let* ([sym 'squarf] [tc-e (let* ([sym 'squarf]
[x (if (= 1 2) 3 sym)]) [x (if (= 1 2) 3 sym)])
x) x)
(Un (-val 'squarf) -Integer) #:ret (-path (Un (-val 'squarf) -Integer) #'x)]
(-vet #'x) (-vef #'x)]
[tc-e (if #t 1 2) -Integer] [tc-e (if #t 1 2) -Integer]
@ -343,12 +351,12 @@
;;; tests for and ;;; tests for and
[tc-e (let: ([x : Any 1]) (and (number? x) (boolean? x))) B [tc-e (let: ([x : Any 1]) (and (number? x) (boolean? x)))
(list (-rest N #'x) (-rest B #'x)) (list)] #:ret (ret B (-FS (list (make-TypeFilter N null #'x) (make-TypeFilter B null #'x)) null))]
[tc-e (let: ([x : Any 1]) (and (number? x) x)) (Un N (-val #f)) [tc-e (let: ([x : Any 1]) (and (number? x) x)) (Un N (-val #f))
(list (-rest N #'x) (make-Var-True-Effect #'x)) (list)] #:ret (ret (Un N (-val #f)) (-FS (list (make-TypeFilter N null #'x) (make-TypeFilter (-val #f) null #'x)) null))]
[tc-e (let: ([x : Any 1]) (and x (boolean? x))) B [tc-e (let: ([x : Any 1]) (and x (boolean? x))) B
(list (-rem (-val #f) #'x) (-rest B #'x)) (list)] #:ret (ret (Un N (-val #f)) (-FS (list (make-TypeFilter N null #'x) (make-TypeFilter (-val #f) null #'x)) null))]
[tc-e (let: ([x : Any 3]) [tc-e (let: ([x : Any 3])
(if (and (list? x) (not (null? x))) (if (and (list? x) (not (null? x)))
@ -572,7 +580,7 @@
(-polydots (a) ((list -String) (N a) . ->... . N))] (-polydots (a) ((list -String) (N a) . ->... . N))]
;; instantiating non-dotted terms ;; instantiating non-dotted terms
[tc-e (inst (plambda: (a) ([x : a]) x) Integer) [tc-e (inst (plambda: (a) ([x : a]) x) Integer)
(-Integer . -> . -Integer : (list (make-Latent-Var-True-Effect)) (list (make-Latent-Var-False-Effect)))] (make-Function (list (make-arr (list -Integer) -Integer #:filter (-LFS (list (-not-filter (-val #f))) (list (-filter (-val #f)))))))]
[tc-e (inst (plambda: (a) [x : a *] (apply list x)) Integer) [tc-e (inst (plambda: (a) [x : a *] (apply list x)) Integer)
((list) -Integer . ->* . (-lst -Integer))] ((list) -Integer . ->* . (-lst -Integer))]
@ -668,7 +676,7 @@
(fact 20))] (fact 20))]
#;[tc-err ] #;[tc-err ]
)) )
(test-suite (test-suite
"check-type tests" "check-type tests"
(test-exn "Fails correctly" exn:fail:syntax? (lambda () (parameterize ([orig-module-stx #'here]) (test-exn "Fails correctly" exn:fail:syntax? (lambda () (parameterize ([orig-module-stx #'here])