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 35b55618..c451af0b 100644 --- a/collects/tests/typed-scheme/unit-tests/parse-type-tests.ss +++ b/collects/tests/typed-scheme/unit-tests/parse-type-tests.ss @@ -55,6 +55,10 @@ (test-suite nm (pt-test elems ...) ...)])) +(define N -Number) +(define B -Boolean) +(define Sym -Symbol) + (define (parse-type-tests) (pt-tests "parse-type tests" @@ -65,7 +69,7 @@ [(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))] + [(-> (values Number Boolean Number)) (t:-> (-values (list N B N)))] [(Number -> Number) (t:-> N N)] [(Number -> Number) (t:-> N N)] [(Number Number Number Boolean -> Number) (N N N B . t:-> . N)] @@ -80,8 +84,8 @@ [(∀ (a ...) (a ... a -> Integer)) (-polydots (a) ( (list) (a a) . ->... . -Integer))] [(All (a ...) (a ... -> Number)) (-polydots (a) ((list) [a a] . ->... . N))] - [(All (a ...) (values a ...)) - (-polydots (a) (make-ValuesDots (list) a 'a))] + [(All (a ...) (-> (values a ...))) + (-polydots (a) (t:-> (make-ValuesDots (list) a 'a)))] [(case-lambda (Number -> Boolean) (Number Number -> Number)) (cl-> [(N) B] [(N N) N])] [1 (-val 1)] diff --git a/collects/tests/typed-scheme/unit-tests/remove-intersect-tests.ss b/collects/tests/typed-scheme/unit-tests/remove-intersect-tests.ss index 53b99e22..95fc97fc 100644 --- a/collects/tests/typed-scheme/unit-tests/remove-intersect-tests.ss +++ b/collects/tests/typed-scheme/unit-tests/remove-intersect-tests.ss @@ -15,15 +15,15 @@ (define (restrict-tests) (restr-tests - [N (Un N Sym) N] - [N N N] - [(Un (-val 'foo) (-val 6)) (Un N Sym) (Un (-val 'foo) (-val 6))] - [N (-mu a (Un N Sym (make-Listof a))) N] - [(Un N B) (-mu a (Un N Sym (make-Listof a))) N] - [(-mu x (Un N (make-Listof x))) (Un Sym N B) N] - [(Un N -String Sym B) N N] + [-Number (Un -Number -Symbol) -Number] + [-Number -Number -Number] + [(Un (-val 'foo) (-val 6)) (Un -Number -Symbol) (Un (-val 'foo) (-val 6))] + [-Number (-mu a (Un -Number -Symbol (make-Listof a))) -Number] + [(Un -Number -Boolean) (-mu a (Un -Number -Symbol (make-Listof a))) -Number] + [(-mu x (Un -Number (make-Listof x))) (Un -Symbol -Number -Boolean) -Number] + [(Un -Number -String -Symbol -Boolean) -Number -Number] - [(-lst N) (-pair Univ Univ) (-pair N (-lst N))] + [(-lst -Number) (-pair Univ Univ) (-pair -Number (-lst -Number))] ;; FIXME #; [-Listof -Sexp (-lst (Un B N -String Sym))] @@ -40,18 +40,18 @@ (define (remove-tests) (remo-tests - [(Un N Sym) N Sym] - [N N (Un)] - [(-mu x (Un N Sym (make-Listof x))) N (Un Sym (make-Listof (-mu x (Un N Sym (make-Listof x)))))] - [(-mu x (Un N Sym B (make-Listof x))) N (Un Sym B (make-Listof (-mu x (Un N Sym B (make-Listof x)))))] - [(Un (-val #f) (-mu x (Un N Sym (make-Listof (-v x))))) - (Un B N) - (Un Sym (make-Listof (-mu x (Un N Sym (make-Listof x)))))] - [(Un (-val 'foo) (-val 6)) (Un N Sym) (Un)] - [(-> (Un Sym N) N) (-> N N) (Un)] - [(Un (-poly (a) (make-Listof a)) (-> N N)) (-> N N) (-poly (a) (make-Listof a))] - [(Un Sym N) (-poly (a) N) Sym] - [(-pair N (-v a)) (-pair Univ Univ) (Un)] + [(Un -Number -Symbol) -Number -Symbol] + [-Number -Number (Un)] + [(-mu x (Un -Number -Symbol (make-Listof x))) -Number (Un -Symbol (make-Listof (-mu x (Un -Number -Symbol (make-Listof x)))))] + [(-mu x (Un -Number -Symbol -Boolean (make-Listof x))) -Number (Un -Symbol -Boolean (make-Listof (-mu x (Un -Number -Symbol -Boolean (make-Listof x)))))] + [(Un (-val #f) (-mu x (Un -Number -Symbol (make-Listof (-v x))))) + (Un -Boolean -Number) + (Un -Symbol (make-Listof (-mu x (Un -Number -Symbol (make-Listof x)))))] + [(Un (-val 'foo) (-val 6)) (Un -Number -Symbol) (Un)] + [(-> (Un -Symbol -Number) -Number) (-> -Number -Number) (Un)] + [(Un (-poly (a) (make-Listof a)) (-> -Number -Number)) (-> -Number -Number) (-poly (a) (make-Listof a))] + [(Un -Symbol -Number) (-poly (a) -Number) -Symbol] + [(-pair -Number (-v a)) (-pair Univ Univ) (Un)] )) (define-go @@ -62,11 +62,11 @@ (-mu list-rec (Un (-val '()) - (-pair (-mu x (Un B N -String Sym (-val '()) (-pair x x))) + (-pair (-mu x (Un -Boolean -Number -String -Symbol (-val '()) (-pair x x))) list-rec)))) (define x2 (Un (-val '()) - (-pair (-mu x (Un B N -String Sym (-val '()) (-pair x x))) - (-mu x (Un B N -String Sym (-val '()) (-pair x x)))))) + (-pair (-mu x (Un -Boolean -Number -String -Symbol (-val '()) (-pair x x))) + (-mu x (Un -Boolean -Number -String -Symbol (-val '()) (-pair x x)))))) (provide remove-tests restrict-tests) diff --git a/collects/tests/typed-scheme/unit-tests/type-equal-tests.ss b/collects/tests/typed-scheme/unit-tests/type-equal-tests.ss index 2a2625d9..57aaa478 100644 --- a/collects/tests/typed-scheme/unit-tests/type-equal-tests.ss +++ b/collects/tests/typed-scheme/unit-tests/type-equal-tests.ss @@ -26,21 +26,21 @@ (define (type-equal-tests) (te-tests - [N N] - [(Un N) N] - [(Un N Sym B) (Un N B Sym)] - [(Un N Sym B) (Un Sym B N)] - [(Un N Sym B) (Un Sym N B)] - [(Un N Sym B) (Un B (Un Sym N))] - [(Un N Sym) (Un Sym N)] - [(-poly (x) (-> (Un Sym N) x)) (-poly (xyz) (-> (Un N Sym) xyz))] - [(-mu x (Un N Sym x)) (-mu y (Un N Sym y))] + [-Number -Number] + [(Un -Number) -Number] + [(Un -Number -Symbol -Boolean) (Un -Number -Boolean -Symbol)] + [(Un -Number -Symbol -Boolean) (Un -Symbol -Boolean -Number)] + [(Un -Number -Symbol -Boolean) (Un -Symbol -Number -Boolean)] + [(Un -Number -Symbol -Boolean) (Un -Boolean (Un -Symbol -Number))] + [(Un -Number -Symbol) (Un -Symbol -Number)] + [(-poly (x) (-> (Un -Symbol -Number) x)) (-poly (xyz) (-> (Un -Number -Symbol) xyz))] + [(-mu x (Un -Number -Symbol x)) (-mu y (Un -Number -Symbol y))] ;; found bug [FAIL (Un (-mu heap-node - (-struct 'heap-node #f (list (-base 'comparator) N (-v a) (Un heap-node (-base 'heap-empty))))) + (-struct 'heap-node #f (list (-base 'comparator) -Number (-v a) (Un heap-node (-base 'heap-empty))))) (-base 'heap-empty)) (Un (-mu heap-node - (-struct 'heap-node #f (list (-base 'comparator) N (-pair N N) (Un heap-node (-base 'heap-empty))))) + (-struct 'heap-node #f (list (-base 'comparator) -Number (-pair -Number -Number) (Un heap-node (-base 'heap-empty))))) (-base 'heap-empty))])) (define-go diff --git a/collects/typed-scheme/private/parse-type.ss b/collects/typed-scheme/private/parse-type.ss index 0818d2a5..b72a67c4 100644 --- a/collects/typed-scheme/private/parse-type.ss +++ b/collects/typed-scheme/private/parse-type.ss @@ -278,6 +278,27 @@ (parameterize ([current-orig-stx stx]) (parse/get stx t type))) +(define (parse-all-type stx parse-type) + (syntax-parse stx + [(All (vars ... v dd) t) + #:when (eq? (syntax-e #'dd) '...) + #:when (andmap identifier? (syntax->list #'(v vars ...))) + (let* ([vars (map syntax-e (syntax->list #'(vars ...)))] + [tvars (map make-F vars)] + [v (syntax-e #'v)] + [tv (make-Dotted (make-F v))]) + (add-type-name-reference #'All) + (parameterize ([current-tvars (extend-env (cons v vars) (cons tv tvars) (current-tvars))]) + (make-PolyDots (append vars (list v)) (parse-type #'t))))] + [(All (vars ...) t) + #:when (andmap identifier? (syntax->list #'(vars ...))) + (let* ([vars (map syntax-e (syntax->list #'(vars ...)))] + [tvars (map make-F vars)]) + (add-type-name-reference #'All) + (parameterize ([current-tvars (extend-env vars tvars (current-tvars))]) + (make-Poly vars (parse-type #'t))))] + [(All . rest) (tc-error "All: bad syntax")])) + (define (parse-type stx) (parameterize ([current-orig-stx stx]) (syntax-case* stx () @@ -423,27 +444,10 @@ [(quot t) (eq? (syntax-e #'quot) 'quote) (-val (syntax-e #'t))] - [(All (vars ... v dd) t) - (and (or (eq? (syntax-e #'All) 'All) - (eq? (syntax-e #'All) '∀)) - (eq? (syntax-e #'dd) '...) - (andmap identifier? (syntax->list #'(v vars ...)))) - (let* ([vars (map syntax-e (syntax->list #'(vars ...)))] - [tvars (map make-F vars)] - [v (syntax-e #'v)] - [tv (make-Dotted (make-F v))]) - (add-type-name-reference #'All) - (parameterize ([current-tvars (extend-env (cons v vars) (cons tv tvars) (current-tvars))]) - (make-PolyDots (append vars (list v)) (parse-values-type #'t))))] - [(All (vars ...) t) - (and (or (eq? (syntax-e #'All) 'All) - (eq? (syntax-e #'All) '∀)) - (andmap identifier? (syntax->list #'(vars ...)))) - (let* ([vars (map syntax-e (syntax->list #'(vars ...)))] - [tvars (map make-F vars)]) - (add-type-name-reference #'All) - (parameterize ([current-tvars (extend-env vars tvars (current-tvars))]) - (make-Poly vars (parse-values-type #'t))))] + [(All . rest) + (or (eq? (syntax-e #'All) 'All) + (eq? (syntax-e #'All) '∀)) + (parse-all-type stx parse-type)] [(Opaque p?) (eq? (syntax-e #'Opaque) 'Opaque) (begin @@ -487,9 +491,7 @@ Err] [else (tc-error/delayed "Unbound type name ~a" (syntax-e #'id)) - Err])] - - [(All . rest) (eq? (syntax-e #'All) 'All) (tc-error "All: bad syntax")] + Err])] [(Opaque . rest) (eq? (syntax-e #'Opaque) 'Opqaue) (tc-error "Opaque: bad syntax")] [(U . rest) (eq? (syntax-e #'U) 'U) (tc-error "Union: bad syntax")] [(Vectorof . rest) (eq? (syntax-e #'Vectorof) 'Vectorof) (tc-error "Vectorof: bad syntax")] @@ -562,6 +564,10 @@ [(values tys ...) #:when (eq? (syntax-e #'values) 'values) (-values (map parse-type (syntax->list #'(tys ...))))] + [(All . rest) + #:when (or (eq? (syntax-e #'All) 'All) + (eq? (syntax-e #'All) '∀)) + (parse-all-type stx parse-values-type)] [t (-values (list (parse-type #'t)))])))