diff --git a/collects/tests/typed-scheme/unit-tests/typecheck-tests.rkt b/collects/tests/typed-scheme/unit-tests/typecheck-tests.rkt index 34776dee..62314b0a 100644 --- a/collects/tests/typed-scheme/unit-tests/typecheck-tests.rkt +++ b/collects/tests/typed-scheme/unit-tests/typecheck-tests.rkt @@ -141,24 +141,24 @@ (+ 1 (car x)) 5)) N] - (tc-e/t (if (let ([y 12]) y) 3 4) -Pos) - (tc-e/t 3 -Pos) + (tc-e/t (if (let ([y 12]) y) 3 4) -PositiveFixnum) + (tc-e/t 3 -PositiveFixnum) (tc-e/t "foo" -String) (tc-e (+ 3 4) -Pos) - [tc-e/t (lambda: () 3) (t:-> -Pos : -true-lfilter)] - [tc-e/t (lambda: ([x : Number]) 3) (t:-> N -Pos : -true-lfilter)] - [tc-e/t (lambda: ([x : Number] [y : Boolean]) 3) (t:-> N B -Pos : -true-lfilter)] - [tc-e/t (lambda () 3) (t:-> -Pos : -true-lfilter)] - [tc-e (values 3 4) #:ret (ret (list -Pos -Pos) (list -true-filter -true-filter))] - [tc-e (cons 3 4) (-pair -Pos -Pos)] + [tc-e/t (lambda: () 3) (t:-> -PositiveFixnum : -true-lfilter)] + [tc-e/t (lambda: ([x : Number]) 3) (t:-> N -PositiveFixnum : -true-lfilter)] + [tc-e/t (lambda: ([x : Number] [y : Boolean]) 3) (t:-> N B -PositiveFixnum : -true-lfilter)] + [tc-e/t (lambda () 3) (t:-> -PositiveFixnum : -true-lfilter)] + [tc-e (values 3 4) #:ret (ret (list -PositiveFixnum -PositiveFixnum) (list -true-filter -true-filter))] + [tc-e (cons 3 4) (-pair -PositiveFixnum -PositiveFixnum)] [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 -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 #(3 4 5) (make-Vector -PositiveFixnum)] + [tc-e/t '(2 3 4) (-lst* -PositiveFixnum -PositiveFixnum -PositiveFixnum)] + [tc-e/t '(2 3 #t) (-lst* -PositiveFixnum -PositiveFixnum (-val #t))] + [tc-e/t #(2 3 #t) (make-Vector (t:Un -PositiveFixnum (-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)))] @@ -169,9 +169,9 @@ [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 -top -top))])] - [tc-e/t (values 3) -Pos] + [tc-e/t (values 3) -PositiveFixnum] [tc-e (values) #:ret (ret null)] - [tc-e (values 3 #f) #:ret (ret (list -Pos (-val #f)) (list (-FS -top -bot) (-FS -bot -top)))] + [tc-e (values 3 #f) #:ret (ret (list -PositiveFixnum (-val #f)) (list (-FS -top -bot) (-FS -bot -top)))] [tc-e (map #{values @ Symbol} '(a b c)) (-pair Sym (make-Listof Sym))] [tc-e (letrec: ([fact : (Number -> Number) (lambda: ([n : Number]) (if (zero? n) 1 (* n (fact (- n 1)))))]) (fact 20)) @@ -201,8 +201,8 @@ 'bc)) N] [tc-e/t (let: ((x : Number 3)) (if (boolean? x) (not x) #t)) (-val #t)] - [tc-e/t (begin 3) -Pos] - [tc-e/t (begin #f 3) -Pos] + [tc-e/t (begin 3) -PositiveFixnum] + [tc-e/t (begin #f 3) -PositiveFixnum] [tc-e/t (begin #t) (-val #t)] [tc-e/t (begin0 #t) (-val #t)] [tc-e/t (begin0 #t 3) (-val #t)] @@ -210,14 +210,14 @@ [tc-e #f #:ret (ret (-val #f) (-FS -bot -top))] [tc-e/t '#t (-val #t)] [tc-e '#f #:ret (ret (-val #f) (-FS -bot -top))] - [tc-e/t (if #f 'a 3) -Pos] + [tc-e/t (if #f 'a 3) -PositiveFixnum] [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])) - -Pos] + -PositiveFixnum] [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] @@ -241,7 +241,7 @@ (if (list? x) (begin (car x) 1) 2)) - -Pos] + -PositiveFixnum] [tc-e (let: ([x : (U Number Boolean) 3]) @@ -250,7 +250,7 @@ 3)) N] - [tc-e (let ([x 1]) x) -Pos] + [tc-e (let ([x 1]) x) -PositiveFixnum] [tc-e (let ([x 1]) (boolean? x)) #:ret (ret -Boolean (-FS -bot -top))] [tc-e (boolean? number?) #:ret (ret -Boolean (-FS -bot -top))] @@ -271,9 +271,9 @@ (if (eq? x 1) 12 14)) - -Pos] + -PositiveFixnum] - [tc-e (car (append (list 1 2) (list 3 4))) -Pos] + [tc-e (car (append (list 1 2) (list 3 4))) -PositiveFixnum] [tc-e (let-syntax ([a @@ -283,8 +283,8 @@ (string-append "foo" (a v)))) -String] - [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-e (apply (plambda: (a) [x : a *] x) '(5)) (-lst -PositiveFixnum)] + [tc-e (apply append (list '(1 2 3) '(4 5 6))) (-lst -PositiveFixnum)] [tc-err ((case-lambda: [([x : Number]) x] [([y : Number] [x : Number]) x]) @@ -320,9 +320,9 @@ [tc-e (let* ([sym 'squarf] [x (if (= 1 2) 3 sym)]) x) - (t:Un (-val 'squarf) -Pos)] + (t:Un (-val 'squarf) -PositiveFixnum)] - [tc-e/t (if #t 1 2) -Pos] + [tc-e/t (if #t 1 2) -PositiveFixnum] ;; eq? as predicate @@ -347,12 +347,12 @@ [x (if (= 1 2) 3 sym)]) (if (eq? x sym) 3 x)) #:proc (syntax-parser [(_ _ (_ ([(x) _]) _)) - (ret -Pos (-FS -top -top))])] + (ret -PositiveFixnum (-FS -top -top))])] [tc-e (let* ([sym 'squarf] [x (if (= 1 2) 3 sym)]) (if (eq? sym x) 3 x)) #:proc (syntax-parser [(_ _ (_ ([(x) _]) _)) - (ret -Pos (-FS -top -top))])] + (ret -PositiveFixnum (-FS -top -top))])] ;; equal? as predicate for symbols [tc-e (let: ([x : (Un 'foo Number) 'foo]) (if (equal? x 'foo) 3 x)) @@ -365,22 +365,22 @@ [x (if (= 1 2) 3 sym)]) (if (equal? x sym) 3 x)) #:proc (syntax-parser [(_ _ (_ ([(x) _]) _)) - (ret -Pos (-FS -top -top))])] + (ret -PositiveFixnum (-FS -top -top))])] [tc-e (let* ([sym 'squarf] [x (if (= 1 2) 3 sym)]) (if (equal? sym x) 3 x)) #:proc (syntax-parser [(_ _ (_ ([(x) _]) _)) - (ret -Pos (-FS -top -top))])] + (ret -PositiveFixnum (-FS -top -top))])] [tc-e (let: ([x : (Listof Symbol)'(a b c)]) (cond [(memq 'a x) => car] [else 'foo])) Sym] - [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 (list 1 2 3) (-lst* -PositiveFixnum -PositiveFixnum -PositiveFixnum)] + [tc-e (list 1 2 3 'a) (-lst* -PositiveFixnum -PositiveFixnum -PositiveFixnum (-val 'a))] - [tc-e `(1 2 ,(+ 3 4)) (-lst* -Pos -Pos -Pos)] + [tc-e `(1 2 ,(+ 3 4)) (-lst* -PositiveFixnum -PositiveFixnum -Pos)] [tc-e (let: ([x : Any 1]) (when (and (list? x) (not (null? x))) @@ -399,7 +399,7 @@ 'foo)) (t:Un (-val 'foo) (-pair Univ (-lst Univ)))] - [tc-e (cadr (cadr (list 1 (list 1 2 3) 3))) -Pos] + [tc-e (cadr (cadr (list 1 (list 1 2 3) 3))) -PositiveFixnum] @@ -414,7 +414,7 @@ [tc-e/t (let: ([x : Any 3]) (if (and (list? x) (not (null? x))) (begin (car x) 1) 2)) - -Pos] + -PositiveFixnum] ;; set! tests [tc-e (let: ([x : Any 3]) @@ -471,7 +471,7 @@ [tc-e/t (let* ([z 1] [p? (lambda: ([x : Any]) (number? z))]) (lambda: ([x : Any]) (if (p? x) 11 12))) - (t:-> Univ -Pos : -true-lfilter)] + (t:-> Univ -PositiveFixnum : -true-lfilter)] [tc-e/t (let* ([z 1] [p? (lambda: ([x : Any]) (number? z))]) (lambda: ([x : Any]) (if (p? x) x 12))) @@ -484,7 +484,7 @@ [tc-e/t (let* ([z 1] [p? (lambda: ([x : Any]) (not (number? z)))]) (lambda: ([x : Any]) (if (p? x) x 12))) - (t:-> Univ -Pos : -true-lfilter)] + (t:-> Univ -PositiveFixnum : -true-lfilter)] [tc-e/t (let* ([z 1] [p? (lambda: ([x : Any]) z)]) (lambda: ([x : Any]) (if (p? x) x 12))) @@ -515,7 +515,7 @@ ;; w-c-m [tc-e/t (with-continuation-mark 'key 'mark 3) - -Pos] + -PositiveFixnum] [tc-err (with-continuation-mark (5 4) 1 3)] [tc-err (with-continuation-mark 1 (5 4) @@ -544,14 +544,14 @@ [tc-err (call-with-values (lambda () (values 2 1)) (lambda: ([x : String] [y : Number]) (+ x y)))] ;; quote-syntax - [tc-e/t #'3 (-Syntax -Pos)] - [tc-e/t #'(1 2 3) (-Syntax (-lst* -Pos -Pos -Pos))] + [tc-e/t #'3 (-Syntax -PositiveFixnum)] + [tc-e/t #'(1 2 3) (-Syntax (-lst* -PositiveFixnum -PositiveFixnum -PositiveFixnum))] ;; testing some primitives [tc-e (let ([app apply] [f (lambda: [x : Number *] 3)]) (app f (list 1 2 3))) - -Pos] + -PositiveFixnum] [tc-e ((lambda () (call/cc (lambda: ([k : (Number -> (U))]) (if (read) 5 (k 10)))))) N] @@ -589,7 +589,7 @@ (+ z w))) (g 4)) 5) - -Pos] + -PositiveFixnum] [tc-err (let () (define x x) @@ -620,11 +620,11 @@ [tc-e/t (if #f 1 'foo) (-val 'foo)] - [tc-e (list* 1 2 3) (-pair -Pos (-pair -Pos -Pos))] + [tc-e (list* 1 2 3) (-pair -PositiveFixnum (-pair -PositiveFixnum -PositiveFixnum))] [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 -Pos)] - [tc-e (apply append (list 1) (list 2) (list 3) (list (list 1) (list "foo"))) (-lst (t:Un -String -Pos))] + [tc-e (apply append (list 1) (list 2) (list 3) (list (list 1) (list 1))) (-lst -PositiveFixnum)] + [tc-e (apply append (list 1) (list 2) (list 3) (list (list 1) (list "foo"))) (-lst (t:Un -String -PositiveFixnum))] [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)))] @@ -652,12 +652,12 @@ ;; instantiating dotted terms [tc-e/t (inst (plambda: (a ...) [xs : a ... a] 3) Integer Boolean Integer) - (-Integer B -Integer . t:-> . -Pos : -true-lfilter)] + (-Integer B -Integer . t:-> . -PositiveFixnum : -true-lfilter)] [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:-> . -Pos : -true-filter)] + . t:-> . -PositiveFixnum : -true-filter)] [tc-e/t (plambda: (z x y ...) () (inst map z x y ... y)) (-polydots (z x y) (t:-> (cl->* @@ -744,7 +744,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 -Pos -Pos -Pos))] + [tc-e (apply values (list 1 2 3)) #:ret (ret (list -PositiveFixnum -PositiveFixnum -PositiveFixnum))] [tc-e/t (ann (if #t 3 "foo") Integer) -Integer] @@ -784,7 +784,7 @@ (tc-e (or (string->number "7") 7) #:ret (ret -Number -true-filter)) [tc-e (let ([x 1]) (if x x (add1 x))) - #:ret (ret -Pos (-FS -top -top))] + #:ret (ret -PositiveFixnum (-FS -top -top))] [tc-e (let: ([x : (U (Vectorof Number) String) (vector 1 2 3)]) (if (vector? x) (vector-ref x 0) (string-length x))) -Number] @@ -835,7 +835,10 @@ (test-not-exn "Doesn't fail on equal types" (lambda () (check-type #'here N N)))) (test-suite "tc-literal tests" - (tc-l 5 -ExactPositiveInteger) + (tc-l 5 -PositiveFixnum) + (tc-l -5 -NegativeFixnum) + (tc-l 0 -Zero) + (tc-l 0.0 -Flonum) (tc-l 5# -Flonum) (tc-l 5.0 -Flonum) (tc-l 5.1 -Flonum) @@ -846,8 +849,8 @@ (tc-l #f (-val #f)) (tc-l #"foo" -Bytes) [tc-l () (-val null)] - [tc-l (3 . 4) (-pair -Pos -Pos)] - [tc-l #hash((1 . 2) (3 . 4)) (make-Hashtable -Pos -Pos)]) + [tc-l (3 . 4) (-pair -PositiveFixnum -PositiveFixnum)] + [tc-l #hash((1 . 2) (3 . 4)) (make-Hashtable -PositiveFixnum -PositiveFixnum)]) )) diff --git a/collects/typed-scheme/private/base-env.rkt b/collects/typed-scheme/private/base-env.rkt index aca51a68..0552101c 100644 --- a/collects/typed-scheme/private/base-env.rkt +++ b/collects/typed-scheme/private/base-env.rkt @@ -217,8 +217,8 @@ [string? (make-pred-ty -String)] [string (->* '() -Char -String)] -[string-length (-String . -> . -Nat)] -[unsafe-string-length (-String . -> . -Nat)] +[string-length (-String . -> . -PositiveFixnum)] +[unsafe-string-length (-String . -> . -PositiveFixnum)] [symbol? (make-pred-ty Sym)] [keyword? (make-pred-ty -Keyword)] @@ -301,7 +301,7 @@ [reverse (-poly (a) (-> (-lst a) (-lst a)))] [append (-poly (a) (->* (list) (-lst a) (-lst a)))] -[length (-poly (a) (-> (-lst a) -Nat))] +[length (-poly (a) (-> (-lst a) -PositiveFixnum))] [memq (-poly (a) (-> a (-lst a) (-opt (-lst a))))] [memv (-poly (a) (-> a (-lst a) (-opt (-lst a))))] [memf (-poly (a) ((a . -> . B) (-lst a) . -> . (-opt (-lst a))))] @@ -354,7 +354,7 @@ [char-downcase (-> -Char -Char)] [char-titlecase (-> -Char -Char)] [char-foldcase (-> -Char -Char)] -[char->integer (-> -Char -Nat)] +[char->integer (-> -Char -PositiveFixnum)] [integer->char (-> -Nat -Char)] [char-utf-8-length (-> -Char (apply Un (map -val '(1 2 3 4 5 6))))] @@ -481,16 +481,16 @@ [vector->list (-poly (a) (-> (-vec a) (-lst a)))] [list->vector (-poly (a) (-> (-lst a) (-vec a)))] -[vector-length ((make-VectorTop) . -> . -Nat)] +[vector-length ((make-VectorTop) . -> . -PositiveFixnum)] [vector (-poly (a) (->* (list) a (-vec a)))] [vector-immutable (-poly (a) (->* (list) a (-vec a)))] [vector->immutable-vector (-poly (a) (-> (-vec a) (-vec a)))] [vector-fill! (-poly (a) (-> (-vec a) a -Void))] [vector-argmax (-poly (a) (-> (-> a -Real) (-vec a) a))] [vector-argmin (-poly (a) (-> (-> a -Real) (-vec a) a))] -[vector-memq (-poly (a) (-> a (-vec a) (-opt -Nat)))] -[vector-memv (-poly (a) (-> a (-vec a) (-opt -Nat)))] -[vector-member (-poly (a) (a (-vec a) . -> . (-opt -Nat)))] +[vector-memq (-poly (a) (-> a (-vec a) (-opt -PositiveFixnum)))] +[vector-memv (-poly (a) (-> a (-vec a) (-opt -PositiveFixnum)))] +[vector-member (-poly (a) (a (-vec a) . -> . (-opt -PositiveFixnum)))] ;; [vector->values no good type here] @@ -548,7 +548,7 @@ [hash-remove! (-poly (a b) ((-HT a b) a . -> . -Void))] [hash-map (-poly (a b c) ((-HT a b) (a b . -> . c) . -> . (-lst c)))] [hash-for-each (-poly (a b c) (-> (-HT a b) (-> a b c) -Void))] -[hash-count (-poly (a b) (-> (-HT a b) -Nat))] +[hash-count (-poly (a b) (-> (-HT a b) -PositiveFixnum))] [hash-copy (-poly (a b) (-> (-HT a b) (-HT a b)))] [eq-hash-code (-poly (a) (-> a -Integer))] [eqv-hash-code (-poly (a) (-> a -Integer))] @@ -570,10 +570,9 @@ [bytes->immutable-bytes (-> -Bytes -Bytes)] [byte? (make-pred-ty -Nat)] [bytes-append (->* (list) -Bytes -Bytes)] -[bytes-length (-> -Bytes -Nat)] -[unsafe-bytes-length (-> -Bytes -Nat)] +[bytes-length (-> -Bytes -PositiveFixnum)] +[unsafe-bytes-length (-> -Bytes -PositiveFixnum)] [bytes-copy (-> -Bytes -Bytes)] -[unsafe-bytes-length (-> -Bytes -Nat)] [bytes->list (-> -Bytes (-lst -Nat))] [list->bytes (-> (-lst -Integer) -Bytes)] [bytes* (list -Bytes) -Bytes B)] @@ -712,7 +711,7 @@ (-lst a)) ((-lst b) b) . ->... . - -Nat))] + -PositiveFixnum))] [filter-map (-polydots (c a b) ((list ((list a) (b b) . ->... . (-opt c)) @@ -809,8 +808,8 @@ ;; unsafe -[unsafe-vector-length (-poly (a) ((-vec a) . -> . -Nat))] -[unsafe-vector*-length (-poly (a) ((-vec a) . -> . -Nat))] +[unsafe-vector-length (-poly (a) ((-vec a) . -> . -PositiveFixnum))] +[unsafe-vector*-length (-poly (a) ((-vec a) . -> . -PositiveFixnum))] [unsafe-car (-poly (a b) (cl->* (->acc (list (-pair a b)) a (list -car)) @@ -828,7 +827,7 @@ (-vec a)) ((-vec b) b) . ->... . - -Nat))] + -PositiveFixnum))] [vector-filter (-poly (a b) (cl->* ((make-pred-ty (list a) Univ b) (-vec a) @@ -905,6 +904,6 @@ (-> (-mlst a) (-mlst a) -Void)))] [mpair? (make-pred-ty (make-MPairTop))] [mlist (-poly (a) (->* (list) a (-mlst a)))] -[mlength (-poly (a) (-> (-mlst a) -Nat))] +[mlength (-poly (a) (-> (-mlst a) -PositiveFixnum))] [mreverse! (-poly (a) (-> (-mlst a) (-mlst a)))] [mappend (-poly (a) (->* (list) (-mlst a) (-mlst a)))] diff --git a/collects/typed-scheme/private/base-types.rkt b/collects/typed-scheme/private/base-types.rkt index 0b9e7b8f..f20b9e4a 100644 --- a/collects/typed-scheme/private/base-types.rkt +++ b/collects/typed-scheme/private/base-types.rkt @@ -8,6 +8,8 @@ [Float -Flonum] [Exact-Positive-Integer -ExactPositiveInteger] [Exact-Nonnegative-Integer -ExactNonnegativeInteger] +[Positive-Fixnum -PositiveFixnum] +[Fixnum -Fixnum] [Natural -ExactNonnegativeInteger] [Zero (-val 0)] diff --git a/collects/typed-scheme/typecheck/tc-expr-unit.rkt b/collects/typed-scheme/typecheck/tc-expr-unit.rkt index 8a55e2d3..522caa3f 100644 --- a/collects/typed-scheme/typecheck/tc-expr-unit.rkt +++ b/collects/typed-scheme/typecheck/tc-expr-unit.rkt @@ -13,6 +13,7 @@ (env lexical-env type-env-structs tvar-env index-env) racket/private/class-internal unstable/debug (except-in syntax/parse id) + unstable/function (only-in srfi/1 split-at)) (require (for-template scheme/base racket/private/class-internal)) @@ -33,10 +34,13 @@ [i:boolean (-val (syntax-e #'i))] [i:identifier (-val (syntax-e #'i))] [0 -Zero] + [(~var i (3d (conjoin number? fixnum? positive?))) -PositiveFixnum] + [(~var i (3d (conjoin number? fixnum? negative?))) -NegativeFixnum] + [(~var i (3d (conjoin number? fixnum?))) -Fixnum] [(~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 (number? e) (exact? e) (rational? e))))) -ExactRational] + [(~var i (3d (conjoin number? exact? rational?))) -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.rkt b/collects/typed-scheme/types/abbrev.rkt index 0ab61f3d..3e353317 100644 --- a/collects/typed-scheme/types/abbrev.rkt +++ b/collects/typed-scheme/types/abbrev.rkt @@ -158,12 +158,18 @@ (define -ExactPositiveInteger (make-Base 'Exact-Positive-Integer #'exact-positive-integer?)) +(define -PositiveFixnum + (make-Base 'Positive-Fixnum #'(and/c number? fixnum? positive?))) +(define -NegativeFixnum + (make-Base 'Negative-Fixnum #'(and/c number? fixnum? negative?))) + (define -Zero (-val 0)) (define -Real (*Un -Flonum -ExactRational)) +(define -Fixnum (*Un -PositiveFixnum -NegativeFixnum -Zero)) (define -ExactNonnegativeInteger (*Un -ExactPositiveInteger -Zero)) (define -Nat -ExactNonnegativeInteger) -(define -Byte -Number) +(define -Byte -Integer) diff --git a/collects/typed-scheme/types/subtype.rkt b/collects/typed-scheme/types/subtype.rkt index fde4c808..a5167c48 100644 --- a/collects/typed-scheme/types/subtype.rkt +++ b/collects/typed-scheme/types/subtype.rkt @@ -237,11 +237,27 @@ [((Base: 'Exact-Positive-Integer _) (Base: 'Number _)) A0] [((Base: 'Exact-Positive-Integer _) (== -Nat =t)) A0] [((Base: 'Exact-Positive-Integer _) (Base: 'Integer _)) A0] + + [((Base: 'Positive-Fixnum _) (Base: 'Exact-Positive-Integer _)) A0] + [((Base: 'Positive-Fixnum _) (Base: 'Exact-Rational _)) A0] + [((Base: 'Positive-Fixnum _) (Base: 'Number _)) A0] + [((Base: 'Positive-Fixnum _) (== -Nat =t)) A0] + [((Base: 'Positive-Fixnum _) (Base: 'Integer _)) A0] + + [((Base: 'Negative-Fixnum _) (Base: 'Exact-Rational _)) A0] + [((Base: 'Negative-Fixnum _) (Base: 'Number _)) A0] + [((Base: 'Negative-Fixnum _) (Base: 'Integer _)) A0] + [((== -Nat =t) (Base: 'Number _)) A0] [((== -Nat =t) (Base: 'Exact-Rational _)) A0] [((== -Nat =t) (Base: 'Integer _)) A0] - ;; values are subtypes of their "type" + [((== -Fixnum =t) (Base: 'Number _)) A0] + [((== -Fixnum =t) (Base: 'Exact-Rational _)) A0] + [((== -Fixnum =t) (Base: 'Integer _)) A0] + + + ;; values are subtypes of their "type" [((Value: (? exact-integer? n)) (Base: 'Integer _)) A0] [((Value: (and n (? number?) (? exact?) (? rational?))) (Base: 'Exact-Rational _)) A0] [((Value: (? exact-nonnegative-integer? n)) (== -Nat =t)) A0]