suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

many fixes

Browse Source 
svn: r16913
This commit is contained in:
Sam Tobin-Hochstadt 2009-11-20 03:56:57 +00:00
parent 111b71c844
commit 1da2c7cd7d
7 changed files with 100 additions and 80 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
collects/scribblings/reference/pairs.scrbl
View File

@ -3,7 +3,7 @@
scribble/scheme scribble/scheme
scheme/generator scheme/generator
scheme/list scheme/list
(for-syntax scheme/base)) (for-syntax scheme/base unstable/syntax))
@(define (generate-c_r-example proc) @(define (generate-c_r-example proc)
(define (make-it start n) (define (make-it start n)
@ -23,17 +23,12 @@
(proc value) (proc value)
value))) value)))
(example proc)) (example proc))
@(provide defc_r)
@(define-syntax (defc_r stx) @(define-syntax (defc_r stx)
(syntax-case stx () (syntax-case stx ()
[(_ x ... example) [(_ x ... example)
(let ([xs (map syntax-e (syntax->list #'(x ...)))]) (let ([xs (map syntax-e (syntax->list #'(x ...)))])
(let ([name (string->symbol (let ([contract (let loop ([l (reverse xs)])
(string-append
"c"
(apply string-append (map symbol->string xs))
"r"))]
[contract (let loop ([l (reverse xs)])
(cond (cond
[(null? (cdr l)) 'pair?] [(null? (cdr l)) 'pair?]
[(eq? (car l) 'a) `(cons/c ,(loop (cdr l)) any/c)] [(eq? (car l) 'a) `(cons/c ,(loop (cdr l)) any/c)]
@ -43,7 +38,9 @@
[(null? l) 'p] [(null? l) 'p]
[(eq? (car l) 'a) `(car ,(loop (cdr l)))] [(eq? (car l) 'a) `(car ,(loop (cdr l)))]
[(eq? (car l) 'd) `(cdr ,(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]) [contract (let loop ([c contract] [pos 0])
(if (pair? c) (if (pair? c)
(let* ([a (loop (car c) (add1 pos))] (let* ([a (loop (car c) (add1 pos))]
@ -60,8 +57,9 @@
(list (syntax-source stx) 1 pos (add1 pos) 1))))] (list (syntax-source stx) 1 pos (add1 pos) 1))))]
[example (datum->syntax #'here (syntax->datum #'example))] [example (datum->syntax #'here (syntax->datum #'example))]
[equiv equiv]) [equiv equiv])
#'(defproc (name [v contract]) any/c (quasisyntax/loc stx
"Returns " (to-element 'equiv) (mz-examples (name example))))))])) (defproc (name [v contract]) any/c
"Returns " (to-element 'equiv) (mz-examples (#,(syntax-e #'name) #,(syntax->datum #'example))))))))]))
@title[#:tag "pairs"]{Pairs and Lists} @title[#:tag "pairs"]{Pairs and Lists}

124
collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
View File

@ -29,6 +29,9 @@
(define N -Number) (define N -Number)
(define B -Boolean) (define B -Boolean)
(define Sym -Symbol) (define Sym -Symbol)
(define -Pos -ExactPositiveInteger)
(define R -Real)
(define F -Flonum)
(define (g) (run typecheck-tests)) (define (g) (run typecheck-tests))
@ -73,9 +76,9 @@
(syntax-case stx () (syntax-case stx ()
[(_ expr ty) (syntax/loc stx (tc-e expr #:ret (ret ty)))] [(_ expr ty) (syntax/loc stx (tc-e expr #:ret (ret ty)))]
[(_ expr #:proc p) [(_ expr #:proc p)
(syntax/loc stx (quasisyntax/loc stx
(let-values ([(t e) (tc-expr/expand/values expr)]) (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) [(_ expr #:ret r)
(syntax/loc stx (syntax/loc stx
(check-tc-result-equal? (format "~a" 'expr) (tc-expr/expand expr) r))] (check-tc-result-equal? (format "~a" 'expr) (tc-expr/expand expr) r))]
@ -127,24 +130,24 @@
(+ 1 (car x)) (+ 1 (car x))
5)) 5))
N] N]
(tc-e/t (if (let ([y 12]) y) 3 4) -Integer) (tc-e/t (if (let ([y 12]) y) 3 4) -Pos)
(tc-e/t 3 -Integer) (tc-e/t 3 -Pos)
(tc-e/t "foo" -String) (tc-e/t "foo" -String)
(tc-e (+ 3 4) -Integer) (tc-e (+ 3 4) -Pos)
[tc-e/t (lambda: () 3) (t:-> -Integer : (-LFS (list) (list (make-LBot))))] [tc-e/t (lambda: () 3) (t:-> -Pos : (-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]) 3) (t:-> N -Pos : (-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: ([x : Number] [y : Boolean]) 3) (t:-> N B -Pos : (-LFS (list) (list (make-LBot))))]
[tc-e/t (lambda () 3) (t:-> -Integer : (-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 -Integer -Integer) (list (-FS (list) (list (make-Bot))) (-FS (list) (list (make-Bot)))))] [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 -Integer -Integer)] [tc-e (cons 3 4) (-pair -Pos -Pos)]
[tc-e (cons 3 #{'() : (Listof -Integer)}) (make-Listof -Integer)] [tc-e (cons 3 (ann '() : (Listof Integer))) (make-Listof -Integer)]
[tc-e (void) -Void] [tc-e (void) -Void]
[tc-e (void 3 4) -Void] [tc-e (void 3 4) -Void]
[tc-e (void #t #f '(1 2 3)) -Void] [tc-e (void #t #f '(1 2 3)) -Void]
[tc-e/t #(3 4 5) (make-Vector -Integer)] [tc-e/t #(3 4 5) (make-Vector -Pos)]
[tc-e/t '(2 3 4) (-lst* -Integer -Integer -Integer)] [tc-e/t '(2 3 4) (-lst* -Pos -Pos -Pos)]
[tc-e/t '(2 3 #t) (-lst* -Integer -Integer (-val #t))] [tc-e/t '(2 3 #t) (-lst* -Pos -Pos (-val #t))]
[tc-e/t #(2 3 #t) (make-Vector (t:Un -Integer (-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 '(#t #f) (-lst* (-val #t) (-val #f))]
[tc-e/t (plambda: (a) ([l : (Listof a)]) (car l)) [tc-e/t (plambda: (a) ([l : (Listof a)]) (car l))
(make-Poly '(a) (t:-> (make-Listof (-v a)) (-v a)))] (make-Poly '(a) (t:-> (make-Listof (-v a)) (-v a)))]
@ -152,12 +155,12 @@
(make-Poly '(a) (t:-> (make-Listof (-v a)) (-v a)))] (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/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: ([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))) [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))])] #: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) #: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 (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)))))]) [tc-e (letrec: ([fact : (Number -> Number) (lambda: ([n : Number]) (if (zero? n) 1 (* n (fact (- n 1)))))])
(fact 20)) (fact 20))
@ -187,8 +190,8 @@
'bc)) 'bc))
N] N]
[tc-e/t (let: ((x : Number 3)) (if (boolean? x) (not x) #t)) (-val #t)] [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 3) -Pos]
[tc-e/t (begin #f 3) -Integer] [tc-e/t (begin #f 3) -Pos]
[tc-e/t (begin #t) (-val #t)] [tc-e/t (begin #t) (-val #t)]
[tc-e/t (begin0 #t) (-val #t)] [tc-e/t (begin0 #t) (-val #t)]
[tc-e/t (begin0 #t 3) (-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 #f #:ret (ret (-val #f) (-FS (list (make-Bot)) null))]
[tc-e/t '#t (-val #t)] [tc-e/t '#t (-val #t)]
[tc-e '#f #:ret (ret (-val #f) (-FS (list (make-Bot)) null))] [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/t (if #f #f #t) (t:Un (-val #t))]
[tc-e (when #f 3) -Void] [tc-e (when #f 3) -Void]
[tc-e/t '() (-val '())] [tc-e/t '() (-val '())]
[tc-e/t (let: ([x : (Listof Number) '(1)]) [tc-e/t (let: ([x : (Listof Number) '(1)])
(cond [(pair? x) 1] (cond [(pair? x) 1]
[(null? x) 1])) [(null? x) 1]))
-Integer] -Pos]
[tc-e/t (lambda: ([x : Number] . [y : Number *]) (car y)) (->* (list N) N N)] [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) N]
[tc-e ((lambda: ([x : Number] . [y : Number *]) (car y)) 3 4 5) 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]) [tc-e/t (let: ([x : Any 3])
(if (list? x) (if (list? x)
(begin (car x) 1) 2)) (begin (car x) 1)
-Integer] 2))
-Pos]
[tc-e (let: ([x : (U Number Boolean) 3]) [tc-e (let: ([x : (U Number Boolean) 3])
@ -235,7 +239,7 @@
3)) 3))
N] 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 (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))] [tc-e (boolean? number?) #:ret (ret -Boolean (-FS (list (make-Bot)) null))]
@ -257,9 +261,9 @@
(if (eq? x 1) (if (eq? x 1)
12 12
14)) 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 [tc-e
(let-syntax ([a (let-syntax ([a
@ -269,8 +273,8 @@
(string-append "foo" (a v)))) (string-append "foo" (a v))))
-String] -String]
[tc-e (apply (plambda: (a) [x : a *] x) '(5)) (-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 -Integer)] [tc-e (apply append (list '(1 2 3) '(4 5 6))) (-lst -Pos)]
[tc-err ((case-lambda: [([x : Number]) x] [tc-err ((case-lambda: [([x : Number]) x]
[([y : Number] [x : Number]) x]) [([y : Number] [x : Number]) x])
@ -306,9 +310,9 @@
[tc-e (let* ([sym 'squarf] [tc-e (let* ([sym 'squarf]
[x (if (= 1 2) 3 sym)]) [x (if (= 1 2) 3 sym)])
x) 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 ;; eq? as predicate
@ -333,12 +337,12 @@
[x (if (= 1 2) 3 sym)]) [x (if (= 1 2) 3 sym)])
(if (eq? x sym) 3 x)) (if (eq? x sym) 3 x))
#:proc (syntax-parser [(_ _ (_ ([(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] [tc-e (let* ([sym 'squarf]
[x (if (= 1 2) 3 sym)]) [x (if (= 1 2) 3 sym)])
(if (eq? sym x) 3 x)) (if (eq? sym x) 3 x))
#:proc (syntax-parser [(_ _ (_ ([(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 ;; equal? as predicate for symbols
[tc-e (let: ([x : (Un 'foo Number) 'foo]) [tc-e (let: ([x : (Un 'foo Number) 'foo])
(if (equal? x 'foo) 3 x)) (if (equal? x 'foo) 3 x))
@ -351,22 +355,22 @@
[x (if (= 1 2) 3 sym)]) [x (if (= 1 2) 3 sym)])
(if (equal? x sym) 3 x)) (if (equal? x sym) 3 x))
#:proc (syntax-parser [(_ _ (_ ([(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] [tc-e (let* ([sym 'squarf]
[x (if (= 1 2) 3 sym)]) [x (if (= 1 2) 3 sym)])
(if (equal? sym x) 3 x)) (if (equal? sym x) 3 x))
#:proc (syntax-parser [(_ _ (_ ([(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)]) [tc-e (let: ([x : (Listof Symbol)'(a b c)])
(cond [(memq 'a x) => car] (cond [(memq 'a x) => car]
[else 'foo])) [else 'foo]))
Sym] Sym]
[tc-e (list 1 2 3) (-lst* -Integer -Integer -Integer)] [tc-e (list 1 2 3) (-lst* -Pos -Pos -Pos)]
[tc-e (list 1 2 3 'a) (-lst* -Integer -Integer -Integer (-val 'a))] [tc-e (list 1 2 3 'a) (-lst* -Pos -Pos -Pos (-val 'a))]
#;
[tc-e `(1 2 ,(+ 3 4)) (-lst* N N N)] [tc-e `(1 2 ,(+ 3 4)) (-lst* -Pos -Pos -Pos)]
[tc-e (let: ([x : Any 1]) [tc-e (let: ([x : Any 1])
(when (and (list? x) (not (null? x))) (when (and (list? x) (not (null? x)))
@ -385,7 +389,7 @@
'foo)) 'foo))
(t:Un (-val 'foo) (-pair Univ (-lst Univ)))] (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]) [tc-e/t (let: ([x : Any 3])
(if (and (list? x) (not (null? x))) (if (and (list? x) (not (null? x)))
(begin (car x) 1) 2)) (begin (car x) 1) 2))
-Integer] -Pos]
;; set! tests ;; set! tests
[tc-e (let: ([x : Any 3]) [tc-e (let: ([x : Any 3])
@ -457,7 +461,7 @@
[tc-e/t (let* ([z 1] [tc-e/t (let* ([z 1]
[p? (lambda: ([x : Any]) (number? z))]) [p? (lambda: ([x : Any]) (number? z))])
(lambda: ([x : Any]) (if (p? x) 11 12))) (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] [tc-e/t (let* ([z 1]
[p? (lambda: ([x : Any]) (number? z))]) [p? (lambda: ([x : Any]) (number? z))])
(lambda: ([x : Any]) (if (p? x) x 12))) (lambda: ([x : Any]) (if (p? x) x 12)))
@ -469,7 +473,7 @@
[tc-e/t (let* ([z 1] [tc-e/t (let* ([z 1]
[p? (lambda: ([x : Any]) (not (number? z)))]) [p? (lambda: ([x : Any]) (not (number? z)))])
(lambda: ([x : Any]) (if (p? x) x 12))) (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] [tc-e/t (let* ([z 1]
[p? (lambda: ([x : Any]) z)]) [p? (lambda: ([x : Any]) z)])
(lambda: ([x : Any]) (if (p? x) x 12))) (lambda: ([x : Any]) (if (p? x) x 12)))
@ -500,7 +504,7 @@
;; w-c-m ;; w-c-m
[tc-e/t (with-continuation-mark 'key 'mark [tc-e/t (with-continuation-mark 'key 'mark
3) 3)
-Integer] -Pos]
[tc-err (with-continuation-mark (5 4) 1 [tc-err (with-continuation-mark (5 4) 1
3)] 3)]
[tc-err (with-continuation-mark 1 (5 4) [tc-err (with-continuation-mark 1 (5 4)
@ -529,14 +533,14 @@
[tc-err (call-with-values (lambda () (values 2 1)) [tc-err (call-with-values (lambda () (values 2 1))
(lambda: ([x : String] [y : Number]) (+ x y)))] (lambda: ([x : String] [y : Number]) (+ x y)))]
;; quote-syntax ;; quote-syntax
[tc-e/t #'3 (-Syntax -Integer)] [tc-e/t #'3 (-Syntax -Pos)]
[tc-e/t #'(1 2 3) (-Syntax (-lst* -Integer -Integer -Integer))] [tc-e/t #'(1 2 3) (-Syntax (-lst* -Pos -Pos -Pos))]
;; testing some primitives ;; testing some primitives
[tc-e (let ([app apply] [tc-e (let ([app apply]
[f (lambda: [x : Number *] 3)]) [f (lambda: [x : Number *] 3)])
(app f (list 1 2 3))) (app f (list 1 2 3)))
-Integer] -Pos]
[tc-e ((lambda () (call/cc (lambda: ([k : (Number -> (U))]) (if (read) 5 (k 10)))))) [tc-e ((lambda () (call/cc (lambda: ([k : (Number -> (U))]) (if (read) 5 (k 10))))))
N] N]
@ -565,7 +569,7 @@
(define y 2) (define y 2)
(define z (+ x y)) (define z (+ x y))
(* x z)) (* x z))
-Integer] -Pos]
[tc-e/t (let () [tc-e/t (let ()
(define: (f [x : Number]) : Number (define: (f [x : Number]) : Number
@ -574,7 +578,7 @@
(+ z w))) (+ z w)))
(g 4)) (g 4))
5) 5)
-Integer] -Pos]
[tc-err (let () [tc-err (let ()
(define x x) (define x x)
@ -605,11 +609,11 @@
[tc-e/t (if #f 1 'foo) (-val 'foo)] [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-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 1))) (-lst -Pos)]
[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 "foo"))) (-lst (t:Un -String -Pos))]
[tc-err (plambda: (b ...) [y : b ... b] (apply append (map list y)))] [tc-err (plambda: (b ...) [y : b ... b] (apply append (map list y)))]
[tc-e/t (plambda: (b ...) [y : (Listof Integer) ... b] (apply append y)) [tc-e/t (plambda: (b ...) [y : (Listof Integer) ... b] (apply append y))
(-polydots (b) (->... (list) ((-lst -Integer) b) (-lst -Integer)))] (-polydots (b) (->... (list) ((-lst -Integer) b) (-lst -Integer)))]
@ -636,12 +640,12 @@
;; instantiating dotted terms ;; instantiating dotted terms
[tc-e/t (inst (plambda: (a ...) [xs : a ... a] 3) Integer Boolean Integer) [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) [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) (-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)) [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))))] (-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))) [tc-e/t (ann (lambda (x) x) (All (a) (a -> a)))
(-poly (a) (a . t:-> . 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] [tc-e/t (ann (if #t 3 "foo") Integer) -Integer]
@ -749,10 +753,10 @@
) )
(test-suite (test-suite
"tc-literal tests" "tc-literal tests"
(tc-l 5 -Integer) (tc-l 5 -ExactPositiveInteger)
(tc-l 5# N) (tc-l 5# -Flonum)
(tc-l 5.0 N) (tc-l 5.0 -Flonum)
(tc-l 5.1 N) (tc-l 5.1 -Flonum)
(tc-l #t (-val #t)) (tc-l #t (-val #t))
(tc-l "foo" -String) (tc-l "foo" -String)
(tc-l foo (-val 'foo)) (tc-l foo (-val 'foo))

26
collects/typed-scheme/private/base-env-numeric.ss
View File

@ -11,19 +11,31 @@
scheme/promise scheme/system scheme/promise scheme/system
(only-in string-constants/private/only-once maybe-print-message) (only-in string-constants/private/only-once maybe-print-message)
(only-in scheme/match/runtime match:error matchable? match-equality-test) (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 ;; numeric operations
[modulo (cl->* (-Integer -Integer . -> . -Integer))] [modulo (cl->* (-Integer -Integer . -> . -Integer))]
[= (->* (list N N) N B)] [= (->* (list N N) N B)]
[>= (->* (list N N) N B)] [>= (->* (list R R) R B)]
[< (->* (list N N) N B)] [< (->* (list R R) R B)]
[<= (->* (list N N) N B)] [<= (->* (list R R) R B)]
[> (->* (list N N) N B)] [> (->* (list R R) R B)]
[zero? (N . -> . 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->* (->* (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))] [- (cl->* (->* (list -Integer) -Integer -Integer) (->* (list N) N N))]
[max (cl->* (->* (list -Integer) -Integer -Integer) [max (cl->* (->* (list -Integer) -Integer -Integer)
(->* (list N) N N))] (->* (list N) N N))]

2
collects/typed-scheme/typecheck/tc-expr-unit.ss
View File

@ -36,7 +36,7 @@
[(~var i (3d exact-positive-integer?)) -ExactPositiveInteger] [(~var i (3d exact-positive-integer?)) -ExactPositiveInteger]
[(~var i (3d exact-nonnegative-integer?)) -ExactNonnegativeInteger] [(~var i (3d exact-nonnegative-integer?)) -ExactNonnegativeInteger]
[(~var i (3d exact-integer?)) -Integer] [(~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 inexact-real?)) -Flonum]
[(~var i (3d real?)) -Real] [(~var i (3d real?)) -Real]
[(~var i (3d number?)) -Number] [(~var i (3d number?)) -Number]

2
collects/typed-scheme/types/abbrev.ss
View File

@ -113,7 +113,7 @@
(define -Flonum (make-Base 'Flonum #'inexact-real?)) (define -Flonum (make-Base 'Flonum #'inexact-real?))
(define -ExactRational (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 -Integer (make-Base 'Integer #'exact-integer?))
(define -ExactPositiveInteger (define -ExactPositiveInteger
(make-Base 'Exact-Positive-Integer #'exact-positive-integer?)) (make-Base 'Exact-Positive-Integer #'exact-positive-integer?))

1
collects/typed-scheme/types/convenience.ss
View File

@ -30,6 +30,7 @@
(let loop ([t* t]) (let loop ([t* t])
(match t* (match t*
[(Value: '()) (-lst Univ)] [(Value: '()) (-lst Univ)]
[(Value: 0) -Nat]
[(Mu: var (Union: (list (Value: '()) (Pair: _ (F: var))))) t*] [(Mu: var (Union: (list (Value: '()) (Pair: _ (F: var))))) t*]
[(Pair: t1 (Value: '())) (-lst t1)] [(Pair: t1 (Value: '())) (-lst t1)]
[(Pair: t1 t2) [(Pair: t1 t2)

5
collects/typed-scheme/types/subtype.ss
View File

@ -228,6 +228,11 @@
[((Base: 'Exact-Rational _) (Base: 'Number _)) A0] [((Base: 'Exact-Rational _) (Base: 'Number _)) A0]
[((Base: 'Exact-Positive-Integer _) (Base: 'Exact-Rational _)) A0] [((Base: 'Exact-Positive-Integer _) (Base: 'Exact-Rational _)) A0]
[((Base: 'Exact-Positive-Integer _) (Base: 'Number _)) 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" ;; values are subtypes of their "type"
[((Value: (? integer? n)) (Base: 'Integer _)) A0] [((Value: (? integer? n)) (Base: 'Integer _)) A0]