From 1da2c7cd7d45b7f8a53d1892609e135820ef4301 Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Fri, 20 Nov 2009 03:56:57 +0000 Subject: [PATCH] many fixes svn: r16913 --- collects/scribblings/reference/pairs.scrbl | 20 ++- .../unit-tests/typecheck-tests.ss | 124 +++++++++--------- .../typed-scheme/private/base-env-numeric.ss | 26 +++- .../typed-scheme/typecheck/tc-expr-unit.ss | 2 +- collects/typed-scheme/types/abbrev.ss | 2 +- collects/typed-scheme/types/convenience.ss | 1 + collects/typed-scheme/types/subtype.ss | 5 + 7 files changed, 100 insertions(+), 80 deletions(-) diff --git a/collects/scribblings/reference/pairs.scrbl b/collects/scribblings/reference/pairs.scrbl index 0f0fff21d6..aea5846ffb 100644 --- a/collects/scribblings/reference/pairs.scrbl +++ b/collects/scribblings/reference/pairs.scrbl @@ -3,7 +3,7 @@ scribble/scheme scheme/generator scheme/list - (for-syntax scheme/base)) + (for-syntax scheme/base unstable/syntax)) @(define (generate-c_r-example proc) (define (make-it start n) @@ -23,17 +23,12 @@ (proc value) value))) (example proc)) - +@(provide defc_r) @(define-syntax (defc_r stx) (syntax-case stx () [(_ x ... example) (let ([xs (map syntax-e (syntax->list #'(x ...)))]) - (let ([name (string->symbol - (string-append - "c" - (apply string-append (map symbol->string xs)) - "r"))] - [contract (let loop ([l (reverse xs)]) + (let ([contract (let loop ([l (reverse xs)]) (cond [(null? (cdr l)) 'pair?] [(eq? (car l) 'a) `(cons/c ,(loop (cdr l)) any/c)] @@ -43,7 +38,9 @@ [(null? l) 'p] [(eq? (car l) 'a) `(car ,(loop (cdr l)))] [(eq? (car l) 'd) `(cdr ,(loop (cdr l)))]))]) - (with-syntax ([name name] + (with-syntax ([name (format-id + stx #:source stx + "c~ar" (apply string-append (map symbol->string xs)))] [contract (let loop ([c contract] [pos 0]) (if (pair? c) (let* ([a (loop (car c) (add1 pos))] @@ -60,8 +57,9 @@ (list (syntax-source stx) 1 pos (add1 pos) 1))))] [example (datum->syntax #'here (syntax->datum #'example))] [equiv equiv]) - #'(defproc (name [v contract]) any/c - "Returns " (to-element 'equiv) (mz-examples (name example))))))])) + (quasisyntax/loc stx + (defproc (name [v contract]) any/c + "Returns " (to-element 'equiv) (mz-examples (#,(syntax-e #'name) #,(syntax->datum #'example))))))))])) @title[#:tag "pairs"]{Pairs and Lists} diff --git a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss index 758e98e8ba..e3b2e2105f 100644 --- a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss +++ b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss @@ -29,6 +29,9 @@ (define N -Number) (define B -Boolean) (define Sym -Symbol) +(define -Pos -ExactPositiveInteger) +(define R -Real) +(define F -Flonum) (define (g) (run typecheck-tests)) @@ -73,9 +76,9 @@ (syntax-case stx () [(_ expr ty) (syntax/loc stx (tc-e expr #:ret (ret ty)))] [(_ expr #:proc p) - (syntax/loc stx + (quasisyntax/loc stx (let-values ([(t e) (tc-expr/expand/values expr)]) - (check-tc-result-equal? (format "~s" 'expr) (t) (p e))))] + #,(syntax/loc stx (check-tc-result-equal? (format "~s" 'expr) (t) (p e)))))] [(_ expr #:ret r) (syntax/loc stx (check-tc-result-equal? (format "~a" 'expr) (tc-expr/expand expr) r))] @@ -127,24 +130,24 @@ (+ 1 (car x)) 5)) N] - (tc-e/t (if (let ([y 12]) y) 3 4) -Integer) - (tc-e/t 3 -Integer) + (tc-e/t (if (let ([y 12]) y) 3 4) -Pos) + (tc-e/t 3 -Pos) (tc-e/t "foo" -String) - (tc-e (+ 3 4) -Integer) - [tc-e/t (lambda: () 3) (t:-> -Integer : (-LFS (list) (list (make-LBot))))] - [tc-e/t (lambda: ([x : Number]) 3) (t:-> N -Integer : (-LFS (list) (list (make-LBot))))] - [tc-e/t (lambda: ([x : Number] [y : Boolean]) 3) (t:-> N B -Integer : (-LFS (list) (list (make-LBot))))] - [tc-e/t (lambda () 3) (t:-> -Integer : (-LFS (list) (list (make-LBot))))] - [tc-e (values 3 4) #:ret (ret (list -Integer -Integer) (list (-FS (list) (list (make-Bot))) (-FS (list) (list (make-Bot)))))] - [tc-e (cons 3 4) (-pair -Integer -Integer)] - [tc-e (cons 3 #{'() : (Listof -Integer)}) (make-Listof -Integer)] + (tc-e (+ 3 4) -Pos) + [tc-e/t (lambda: () 3) (t:-> -Pos : (-LFS (list) (list (make-LBot))))] + [tc-e/t (lambda: ([x : Number]) 3) (t:-> N -Pos : (-LFS (list) (list (make-LBot))))] + [tc-e/t (lambda: ([x : Number] [y : Boolean]) 3) (t:-> N B -Pos : (-LFS (list) (list (make-LBot))))] + [tc-e/t (lambda () 3) (t:-> -Pos : (-LFS (list) (list (make-LBot))))] + [tc-e (values 3 4) #:ret (ret (list -Pos -Pos) (list (-FS (list) (list (make-Bot))) (-FS (list) (list (make-Bot)))))] + [tc-e (cons 3 4) (-pair -Pos -Pos)] + [tc-e (cons 3 (ann '() : (Listof Integer))) (make-Listof -Integer)] [tc-e (void) -Void] [tc-e (void 3 4) -Void] [tc-e (void #t #f '(1 2 3)) -Void] - [tc-e/t #(3 4 5) (make-Vector -Integer)] - [tc-e/t '(2 3 4) (-lst* -Integer -Integer -Integer)] - [tc-e/t '(2 3 #t) (-lst* -Integer -Integer (-val #t))] - [tc-e/t #(2 3 #t) (make-Vector (t:Un -Integer (-val #t)))] + [tc-e/t #(3 4 5) (make-Vector -Pos)] + [tc-e/t '(2 3 4) (-lst* -Pos -Pos -Pos)] + [tc-e/t '(2 3 #t) (-lst* -Pos -Pos (-val #t))] + [tc-e/t #(2 3 #t) (make-Vector (t:Un -Pos (-val #t)))] [tc-e/t '(#t #f) (-lst* (-val #t) (-val #f))] [tc-e/t (plambda: (a) ([l : (Listof a)]) (car l)) (make-Poly '(a) (t:-> (make-Listof (-v a)) (-v a)))] @@ -152,12 +155,12 @@ (make-Poly '(a) (t:-> (make-Listof (-v a)) (-v a)))] [tc-e/t (case-lambda: [([a : Number] [b : Number]) (+ a b)]) (t:-> N N N)] [tc-e (let: ([x : Number 5]) x) #:proc (get-let-name x 0 (-path -Number #'x))] - [tc-e (let-values ([(x) 4]) (+ x 1)) -Integer] + [tc-e (let-values ([(x) 4]) (+ x 1)) -Pos] [tc-e (let-values ([(#{x : Number} #{y : Boolean}) (values 3 #t)]) (and (= x 1) (not y))) #:proc (syntax-parser [(_ ([(_ y) . _]) . _) (ret -Boolean (-FS (list (make-TypeFilter (-val #f) null #'y)) null))])] - [tc-e/t (values 3) -Integer] + [tc-e/t (values 3) -Pos] [tc-e (values) #:ret (ret null)] - [tc-e (values 3 #f) #:ret (ret (list -Integer (-val #f)) (list (-FS (list) (list (make-Bot))) (-FS (list (make-Bot)) (list))))] + [tc-e (values 3 #f) #:ret (ret (list -Pos (-val #f)) (list (-FS (list) (list (make-Bot))) (-FS (list (make-Bot)) (list))))] [tc-e (map #{values @ Symbol} '(a b c)) (make-Listof Sym)] [tc-e (letrec: ([fact : (Number -> Number) (lambda: ([n : Number]) (if (zero? n) 1 (* n (fact (- n 1)))))]) (fact 20)) @@ -187,8 +190,8 @@ 'bc)) N] [tc-e/t (let: ((x : Number 3)) (if (boolean? x) (not x) #t)) (-val #t)] - [tc-e/t (begin 3) -Integer] - [tc-e/t (begin #f 3) -Integer] + [tc-e/t (begin 3) -Pos] + [tc-e/t (begin #f 3) -Pos] [tc-e/t (begin #t) (-val #t)] [tc-e/t (begin0 #t) (-val #t)] [tc-e/t (begin0 #t 3) (-val #t)] @@ -196,14 +199,14 @@ [tc-e #f #:ret (ret (-val #f) (-FS (list (make-Bot)) null))] [tc-e/t '#t (-val #t)] [tc-e '#f #:ret (ret (-val #f) (-FS (list (make-Bot)) null))] - [tc-e/t (if #f 'a 3) -Integer] + [tc-e/t (if #f 'a 3) -Pos] [tc-e/t (if #f #f #t) (t:Un (-val #t))] [tc-e (when #f 3) -Void] [tc-e/t '() (-val '())] [tc-e/t (let: ([x : (Listof Number) '(1)]) (cond [(pair? x) 1] [(null? x) 1])) - -Integer] + -Pos] [tc-e/t (lambda: ([x : Number] . [y : Number *]) (car y)) (->* (list N) N N)] [tc-e ((lambda: ([x : Number] . [y : Number *]) (car y)) 3) N] [tc-e ((lambda: ([x : Number] . [y : Number *]) (car y)) 3 4 5) N] @@ -225,8 +228,9 @@ [tc-e/t (let: ([x : Any 3]) (if (list? x) - (begin (car x) 1) 2)) - -Integer] + (begin (car x) 1) + 2)) + -Pos] [tc-e (let: ([x : (U Number Boolean) 3]) @@ -235,7 +239,7 @@ 3)) N] - [tc-e (let ([x 1]) x) #:proc (get-let-name x 0 (-path -Integer #'x))] + [tc-e (let ([x 1]) x) #:proc (get-let-name x 0 (-path -Pos #'x))] [tc-e (let ([x 1]) (boolean? x)) #:ret (ret -Boolean (-FS (list (make-Bot)) null))] [tc-e (boolean? number?) #:ret (ret -Boolean (-FS (list (make-Bot)) null))] @@ -257,9 +261,9 @@ (if (eq? x 1) 12 14)) - -Integer] + -Pos] - [tc-e (car (append (list 1 2) (list 3 4))) -Integer] + [tc-e (car (append (list 1 2) (list 3 4))) -Pos] [tc-e (let-syntax ([a @@ -269,8 +273,8 @@ (string-append "foo" (a v)))) -String] - [tc-e (apply (plambda: (a) [x : a *] x) '(5)) (-lst -Integer)] - [tc-e (apply append (list '(1 2 3) '(4 5 6))) (-lst -Integer)] + [tc-e (apply (plambda: (a) [x : a *] x) '(5)) (-lst -Pos)] + [tc-e (apply append (list '(1 2 3) '(4 5 6))) (-lst -Pos)] [tc-err ((case-lambda: [([x : Number]) x] [([y : Number] [x : Number]) x]) @@ -306,9 +310,9 @@ [tc-e (let* ([sym 'squarf] [x (if (= 1 2) 3 sym)]) x) - #:proc (syntax-parser [(_ _ (_ ([(x) _]) _)) (-path (t:Un (-val 'squarf) -Integer) #'x)])] + #:proc (syntax-parser [(_ _ (_ ([(x) _]) _)) (-path (t:Un (-val 'squarf) -Pos) #'x)])] - [tc-e/t (if #t 1 2) -Integer] + [tc-e/t (if #t 1 2) -Pos] ;; eq? as predicate @@ -333,12 +337,12 @@ [x (if (= 1 2) 3 sym)]) (if (eq? x sym) 3 x)) #:proc (syntax-parser [(_ _ (_ ([(x) _]) _)) - (ret -Integer (-FS (list) (list (make-NotTypeFilter (-val 'squarf) null #'x) (make-TypeFilter (-val #f) null #'x))))])] + (ret -Pos (-FS (list) (list (make-NotTypeFilter (-val 'squarf) null #'x) (make-TypeFilter (-val #f) null #'x))))])] [tc-e (let* ([sym 'squarf] [x (if (= 1 2) 3 sym)]) (if (eq? sym x) 3 x)) #:proc (syntax-parser [(_ _ (_ ([(x) _]) _)) - (ret -Integer (-FS (list) (list (make-NotTypeFilter (-val 'squarf) null #'x) (make-TypeFilter (-val #f) null #'x))))])] + (ret -Pos (-FS (list) (list (make-NotTypeFilter (-val 'squarf) null #'x) (make-TypeFilter (-val #f) null #'x))))])] ;; equal? as predicate for symbols [tc-e (let: ([x : (Un 'foo Number) 'foo]) (if (equal? x 'foo) 3 x)) @@ -351,22 +355,22 @@ [x (if (= 1 2) 3 sym)]) (if (equal? x sym) 3 x)) #:proc (syntax-parser [(_ _ (_ ([(x) _]) _)) - (ret -Integer (-FS (list) (list (make-NotTypeFilter (-val 'squarf) null #'x) (make-TypeFilter (-val #f) null #'x))))])] + (ret -Pos (-FS (list) (list (make-NotTypeFilter (-val 'squarf) null #'x) (make-TypeFilter (-val #f) null #'x))))])] [tc-e (let* ([sym 'squarf] [x (if (= 1 2) 3 sym)]) (if (equal? sym x) 3 x)) #:proc (syntax-parser [(_ _ (_ ([(x) _]) _)) - (ret -Integer (-FS (list) (list (make-NotTypeFilter (-val 'squarf) null #'x) (make-TypeFilter (-val #f) null #'x))))])] + (ret -Pos (-FS (list) (list (make-NotTypeFilter (-val 'squarf) null #'x) (make-TypeFilter (-val #f) null #'x))))])] [tc-e (let: ([x : (Listof Symbol)'(a b c)]) (cond [(memq 'a x) => car] [else 'foo])) Sym] - [tc-e (list 1 2 3) (-lst* -Integer -Integer -Integer)] - [tc-e (list 1 2 3 'a) (-lst* -Integer -Integer -Integer (-val 'a))] - #; - [tc-e `(1 2 ,(+ 3 4)) (-lst* N N N)] + [tc-e (list 1 2 3) (-lst* -Pos -Pos -Pos)] + [tc-e (list 1 2 3 'a) (-lst* -Pos -Pos -Pos (-val 'a))] + + [tc-e `(1 2 ,(+ 3 4)) (-lst* -Pos -Pos -Pos)] [tc-e (let: ([x : Any 1]) (when (and (list? x) (not (null? x))) @@ -385,7 +389,7 @@ 'foo)) (t:Un (-val 'foo) (-pair Univ (-lst Univ)))] - [tc-e (cadr (cadr (list 1 (list 1 2 3) 3))) -Integer] + [tc-e (cadr (cadr (list 1 (list 1 2 3) 3))) -Pos] @@ -400,7 +404,7 @@ [tc-e/t (let: ([x : Any 3]) (if (and (list? x) (not (null? x))) (begin (car x) 1) 2)) - -Integer] + -Pos] ;; set! tests [tc-e (let: ([x : Any 3]) @@ -457,7 +461,7 @@ [tc-e/t (let* ([z 1] [p? (lambda: ([x : Any]) (number? z))]) (lambda: ([x : Any]) (if (p? x) 11 12))) - (t:-> Univ -Integer : (-LFS null (list (make-LBot))))] + (t:-> Univ -Pos : (-LFS null (list (make-LBot))))] [tc-e/t (let* ([z 1] [p? (lambda: ([x : Any]) (number? z))]) (lambda: ([x : Any]) (if (p? x) x 12))) @@ -469,7 +473,7 @@ [tc-e/t (let* ([z 1] [p? (lambda: ([x : Any]) (not (number? z)))]) (lambda: ([x : Any]) (if (p? x) x 12))) - (t:-> Univ -Integer : (-LFS null (list (make-LBot))))] + (t:-> Univ -Pos : (-LFS null (list (make-LBot))))] [tc-e/t (let* ([z 1] [p? (lambda: ([x : Any]) z)]) (lambda: ([x : Any]) (if (p? x) x 12))) @@ -500,7 +504,7 @@ ;; w-c-m [tc-e/t (with-continuation-mark 'key 'mark 3) - -Integer] + -Pos] [tc-err (with-continuation-mark (5 4) 1 3)] [tc-err (with-continuation-mark 1 (5 4) @@ -529,14 +533,14 @@ [tc-err (call-with-values (lambda () (values 2 1)) (lambda: ([x : String] [y : Number]) (+ x y)))] ;; quote-syntax - [tc-e/t #'3 (-Syntax -Integer)] - [tc-e/t #'(1 2 3) (-Syntax (-lst* -Integer -Integer -Integer))] + [tc-e/t #'3 (-Syntax -Pos)] + [tc-e/t #'(1 2 3) (-Syntax (-lst* -Pos -Pos -Pos))] ;; testing some primitives [tc-e (let ([app apply] [f (lambda: [x : Number *] 3)]) (app f (list 1 2 3))) - -Integer] + -Pos] [tc-e ((lambda () (call/cc (lambda: ([k : (Number -> (U))]) (if (read) 5 (k 10)))))) N] @@ -565,7 +569,7 @@ (define y 2) (define z (+ x y)) (* x z)) - -Integer] + -Pos] [tc-e/t (let () (define: (f [x : Number]) : Number @@ -574,7 +578,7 @@ (+ z w))) (g 4)) 5) - -Integer] + -Pos] [tc-err (let () (define x x) @@ -605,11 +609,11 @@ [tc-e/t (if #f 1 'foo) (-val 'foo)] - [tc-e (list* 1 2 3) (-pair -Integer (-pair -Integer -Integer))] + [tc-e (list* 1 2 3) (-pair -Pos (-pair -Pos -Pos))] [tc-err (apply append (list 1) (list 2) (list 3) (list (list 1) "foo"))] - [tc-e (apply append (list 1) (list 2) (list 3) (list (list 1) (list 1))) (-lst -Integer)] - [tc-e (apply append (list 1) (list 2) (list 3) (list (list 1) (list "foo"))) (-lst (t:Un -String -Integer))] + [tc-e (apply append (list 1) (list 2) (list 3) (list (list 1) (list 1))) (-lst -Pos)] + [tc-e (apply append (list 1) (list 2) (list 3) (list (list 1) (list "foo"))) (-lst (t:Un -String -Pos))] [tc-err (plambda: (b ...) [y : b ... b] (apply append (map list y)))] [tc-e/t (plambda: (b ...) [y : (Listof Integer) ... b] (apply append y)) (-polydots (b) (->... (list) ((-lst -Integer) b) (-lst -Integer)))] @@ -636,12 +640,12 @@ ;; instantiating dotted terms [tc-e/t (inst (plambda: (a ...) [xs : a ... a] 3) Integer Boolean Integer) - (-Integer B -Integer . t:-> . -Integer : (-LFS null (list (make-LBot))))] + (-Integer B -Integer . t:-> . -Pos : (-LFS null (list (make-LBot))))] [tc-e/t (inst (plambda: (a ...) [xs : (a ... a -> Integer) ... a] 3) Integer Boolean Integer) ((-Integer B -Integer . t:-> . -Integer) (-Integer B -Integer . t:-> . -Integer) (-Integer B -Integer . t:-> . -Integer) - . t:-> . -Integer : (-LFS null (list (make-LBot))))] + . t:-> . -Pos : (-LFS null (list (make-LBot))))] [tc-e/t (plambda: (z x y ...) () (inst map z x y ... y)) (-polydots (z x y) (t:-> ((list ((list x) (y y) . ->... . z) (-lst x)) ((-lst y) y) . ->... . (-lst z))))] @@ -724,7 +728,7 @@ [tc-e/t (ann (lambda (x) x) (All (a) (a -> a))) (-poly (a) (a . t:-> . a))] - [tc-e (apply values (list 1 2 3)) #:ret (ret (list -Integer -Integer -Integer))] + [tc-e (apply values (list 1 2 3)) #:ret (ret (list -Pos -Pos -Pos))] [tc-e/t (ann (if #t 3 "foo") Integer) -Integer] @@ -749,10 +753,10 @@ ) (test-suite "tc-literal tests" - (tc-l 5 -Integer) - (tc-l 5# N) - (tc-l 5.0 N) - (tc-l 5.1 N) + (tc-l 5 -ExactPositiveInteger) + (tc-l 5# -Flonum) + (tc-l 5.0 -Flonum) + (tc-l 5.1 -Flonum) (tc-l #t (-val #t)) (tc-l "foo" -String) (tc-l foo (-val 'foo)) diff --git a/collects/typed-scheme/private/base-env-numeric.ss b/collects/typed-scheme/private/base-env-numeric.ss index 682cb7a203..daf138b721 100644 --- a/collects/typed-scheme/private/base-env-numeric.ss +++ b/collects/typed-scheme/private/base-env-numeric.ss @@ -11,19 +11,31 @@ scheme/promise scheme/system (only-in string-constants/private/only-once maybe-print-message) (only-in scheme/match/runtime match:error matchable? match-equality-test) - (for-syntax (only-in (types abbrev) [-Number N] [-Boolean B] [-Symbol Sym]))) + (for-syntax (only-in (types abbrev) [-Number N] [-Boolean B] [-Symbol Sym] [-Real R]))) ;; numeric operations [modulo (cl->* (-Integer -Integer . -> . -Integer))] [= (->* (list N N) N B)] -[>= (->* (list N N) N B)] -[< (->* (list N N) N B)] -[<= (->* (list N N) N B)] -[> (->* (list N N) N B)] +[>= (->* (list R R) R B)] +[< (->* (list R R) R B)] +[<= (->* (list R R) R B)] +[> (->* (list R R) R B)] [zero? (N . -> . B)] -[* (cl->* (->* '() -Integer -Integer) (->* '() N N))] +[* (cl->* (->* '() -ExactPositiveInteger -ExactPositiveInteger) + (->* '() -Nat -Nat) + (->* '() -Integer -Integer) + (->* '() -ExactRational -ExactRational) + ;; Reals are just Rat + Int + (->* '() -Real -Flonum) + (->* '() N N))] [/ (cl->* (->* (list N) N N))] -[+ (cl->* (->* '() -Integer -Integer) (->* '() N N))] +[+ (cl->* (->* '() -ExactPositiveInteger -ExactPositiveInteger) + (->* '() -Nat -Nat) + (->* '() -Integer -Integer) + (->* '() -ExactRational -ExactRational) + ;; Reals are just Rat + Int + (->* '() -Real -Flonum) + (->* '() N N))] [- (cl->* (->* (list -Integer) -Integer -Integer) (->* (list N) N N))] [max (cl->* (->* (list -Integer) -Integer -Integer) (->* (list N) N N))] diff --git a/collects/typed-scheme/typecheck/tc-expr-unit.ss b/collects/typed-scheme/typecheck/tc-expr-unit.ss index 85a5b9d820..0cbdb44b6e 100644 --- a/collects/typed-scheme/typecheck/tc-expr-unit.ss +++ b/collects/typed-scheme/typecheck/tc-expr-unit.ss @@ -36,7 +36,7 @@ [(~var i (3d exact-positive-integer?)) -ExactPositiveInteger] [(~var i (3d exact-nonnegative-integer?)) -ExactNonnegativeInteger] [(~var i (3d exact-integer?)) -Integer] - [(~var i (3d (lambda (e) (and (exact? e) (rational? e))))) -ExactRational] + [(~var i (3d (lambda (e) (and (number? e) (exact? e) (rational? e))))) -ExactRational] [(~var i (3d inexact-real?)) -Flonum] [(~var i (3d real?)) -Real] [(~var i (3d number?)) -Number] diff --git a/collects/typed-scheme/types/abbrev.ss b/collects/typed-scheme/types/abbrev.ss index 164483b096..0a390beb8f 100644 --- a/collects/typed-scheme/types/abbrev.ss +++ b/collects/typed-scheme/types/abbrev.ss @@ -113,7 +113,7 @@ (define -Flonum (make-Base 'Flonum #'inexact-real?)) (define -ExactRational - (make-Base 'Exact-Rational #'(and/c rational? exact?))) + (make-Base 'Exact-Rational #'(and/c number? rational? exact?))) (define -Integer (make-Base 'Integer #'exact-integer?)) (define -ExactPositiveInteger (make-Base 'Exact-Positive-Integer #'exact-positive-integer?)) diff --git a/collects/typed-scheme/types/convenience.ss b/collects/typed-scheme/types/convenience.ss index 70dce20c67..f281022b9d 100644 --- a/collects/typed-scheme/types/convenience.ss +++ b/collects/typed-scheme/types/convenience.ss @@ -30,6 +30,7 @@ (let loop ([t* t]) (match t* [(Value: '()) (-lst Univ)] + [(Value: 0) -Nat] [(Mu: var (Union: (list (Value: '()) (Pair: _ (F: var))))) t*] [(Pair: t1 (Value: '())) (-lst t1)] [(Pair: t1 t2) diff --git a/collects/typed-scheme/types/subtype.ss b/collects/typed-scheme/types/subtype.ss index 04de5214d0..a2e961e338 100644 --- a/collects/typed-scheme/types/subtype.ss +++ b/collects/typed-scheme/types/subtype.ss @@ -228,6 +228,11 @@ [((Base: 'Exact-Rational _) (Base: 'Number _)) A0] [((Base: 'Exact-Positive-Integer _) (Base: 'Exact-Rational _)) A0] [((Base: 'Exact-Positive-Integer _) (Base: 'Number _)) A0] + [((Base: 'Exact-Positive-Integer _) (Base: 'Exact-Nonnegative-Integer _)) A0] + [((Base: 'Exact-Positive-Integer _) (Base: 'Integer _)) A0] + [((Base: 'Exact-Nonnegative-Integer _) (Base: 'Number _)) A0] + [((Base: 'Exact-Nonnegative-Integer _) (Base: 'Exact-Rational _)) A0] + [((Base: 'Exact-Nonnegative-Integer _) (Base: 'Integer _)) A0] ;; values are subtypes of their "type" [((Value: (? integer? n)) (Base: 'Integer _)) A0]