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

Generalize naturals to integers to minimize annotations on mutated variables.

Browse Source
This commit is contained in:
Vincent St-Amour 2010-08-04 17:13:55 -04:00
parent 4cb7491309
commit b18f2353ca
11 changed files with 122 additions and 123 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

88
collects/tests/racket/benchmarks/common/typed/graphs.rktl
View File

@ -60,7 +60,7 @@
; Given the size of a vector and a procedure which ; Given the size of a vector and a procedure which
; sends indices to desired vector elements, create ; sends indices to desired vector elements, create
; and return the vector. ; and return the vector.
(: proc->vector (All (X) (Natural (Natural -> X) -> (Vectorof X)))) (: proc->vector (All (X) (Integer (Integer -> X) -> (Vectorof X))))
(define proc->vector (define proc->vector
(lambda (size f) (lambda (size f)
'(assert (and (integer? size) '(assert (and (integer? size)
@ -100,21 +100,21 @@
(define vec-map (define vec-map
(lambda (vec proc) (lambda (vec proc)
(proc->vector (vector-length vec) (proc->vector (vector-length vec)
(lambda: ((i : Natural)) (lambda: ((i : Integer))
(proc (vector-ref vec i)))))) (proc (vector-ref vec i))))))
; Given limit, return the list 0, 1, ..., limit-1. ; Given limit, return the list 0, 1, ..., limit-1.
(: giota (Natural -> (Listof Natural))) (: giota (Integer -> (Listof Integer)))
(define giota (define giota
(lambda (limit) (lambda (limit)
'(assert (and (integer? limit) '(assert (and (integer? limit)
(exact? limit) (exact? limit)
(>= limit 0)) (>= limit 0))
limit) limit)
(let: _-*- : (Listof Natural) (let: _-*- : (Listof Integer)
((limit : Natural ((limit : Integer
limit) limit)
(res : (Listof Natural) (res : (Listof Integer)
'())) '()))
(if (zero? limit) (if (zero? limit)
res res
@ -124,7 +124,7 @@
(cons limit res))))))) (cons limit res)))))))
; Fold over the integers [0, limit). ; Fold over the integers [0, limit).
(: gnatural-fold (All (X) (Natural (Natural X -> X) X -> X))) (: gnatural-fold (All (X) (Integer (Integer X -> X) X -> X)))
(define gnatural-fold (define gnatural-fold
(lambda (limit folder state) (lambda (limit folder state)
'(assert (and (integer? limit) '(assert (and (integer? limit)
@ -141,7 +141,7 @@
state)))) state))))
; Iterate over the integers [0, limit). ; Iterate over the integers [0, limit).
(: gnatural-for-each (Natural (Natural -> Any) -> Void)) (: gnatural-for-each (Integer (Integer -> Any) -> Void))
(define gnatural-for-each (define gnatural-for-each
(lambda (limit proc!) (lambda (limit proc!)
'(assert (and (integer? limit) '(assert (and (integer? limit)
@ -151,12 +151,12 @@
'(assert (procedure? proc!) '(assert (procedure? proc!)
proc!) proc!)
(do: : Void (do: : Void
((i : Natural 0 ((i : Integer 0
(+ i 1))) (+ i 1)))
((= i limit)) ((= i limit))
(proc! i)))) (proc! i))))
(: natural-for-all? (Natural (Natural -> Boolean) -> Boolean)) (: natural-for-all? (Integer (Integer -> Boolean) -> Boolean))
(define natural-for-all? (define natural-for-all?
(lambda (limit ok?) (lambda (limit ok?)
'(assert (and (integer? limit) '(assert (and (integer? limit)
@ -171,7 +171,7 @@
(and (ok? i) (and (ok? i)
(_-*- (+ i 1))))))) (_-*- (+ i 1)))))))
(: natural-there-exists? (Natural (Natural -> Boolean) -> Boolean)) (: natural-there-exists? (Integer (Integer -> Boolean) -> Boolean))
(define natural-there-exists? (define natural-there-exists?
(lambda (limit ok?) (lambda (limit ok?)
'(assert (and (integer? limit) '(assert (and (integer? limit)
@ -329,10 +329,10 @@
; 3->2, 2->3 ; 3->2, 2->3
; ... ; ...
(: make-minimal? (All (State) (: make-minimal? (All (State)
(Natural -> (Integer ->
(Natural (Integer
Graph Graph
((Vectorof Natural) ((Vectorof Integer)
Boolean Boolean
(Boolean -> Boolean) (Boolean -> Boolean)
-> Boolean) -> Boolean)
@ -344,10 +344,10 @@
(exact? max-size) (exact? max-size)
(>= max-size 0)) (>= max-size 0))
max-size) max-size)
(let: ((iotas : (Vectorof (Listof Natural)) (let: ((iotas : (Vectorof (Listof Integer))
(proc->vector (+ max-size 1) (proc->vector (+ max-size 1)
giota)) giota))
(perm : (Vectorof Natural) (perm : (Vectorof Integer)
(make-vector max-size 0))) (make-vector max-size 0)))
(lambda (size graph folder state) (lambda (size graph folder state)
'(assert (and (integer? size) '(assert (and (integer? size)
@ -361,10 +361,10 @@
folder) folder)
(fold-over-perm-tree (fold-over-perm-tree
(vector-ref iotas size) (vector-ref iotas size)
(lambda: ((perm-x : Natural) (lambda: ((perm-x : Integer)
(x : Natural) (x : Integer)
(state : Boolean) (state : Boolean)
(deeper : (Natural Boolean (deeper : (Integer Boolean
-> Boolean)) -> Boolean))
(accross : (Boolean (accross : (Boolean
-> Boolean))) -> Boolean)))
@ -380,7 +380,7 @@
(else (else
(error "can't happen")))) (error "can't happen"))))
0 0
(lambda: ((leaf-depth : Natural) (lambda: ((leaf-depth : Integer)
(state : Boolean) (state : Boolean)
(accross : (Boolean -> Boolean))) (accross : (Boolean -> Boolean)))
'(assert (eqv? leaf-depth size) '(assert (eqv? leaf-depth size)
@ -392,7 +392,7 @@
; Given a graph, a partial permutation vector, the next input and the next ; Given a graph, a partial permutation vector, the next input and the next
; output, return 'less, 'equal or 'more depending on the lexicographic ; output, return 'less, 'equal or 'more depending on the lexicographic
; comparison between the permuted and un-permuted graph. ; comparison between the permuted and un-permuted graph.
(: cmp-next-vertex (Graph (Vectorof Natural) Natural Natural (: cmp-next-vertex (Graph (Vectorof Integer) Integer Integer
-> (U 'less 'equal 'more))) -> (U 'less 'equal 'more)))
(define cmp-next-vertex (define cmp-next-vertex
(lambda (graph perm x perm-x) (lambda (graph perm x perm-x)
@ -430,7 +430,7 @@
;;; ==== rdg.ss ==== ;;; ==== rdg.ss ====
(define-type RDG (Vectorof (Listof Natural))) (define-type RDG (Vectorof (Listof Integer)))
; Fold over rooted directed graphs with bounded out-degree. ; Fold over rooted directed graphs with bounded out-degree.
; Size is the number of vertices (including the root). Max-out is the ; Size is the number of vertices (including the root). Max-out is the
@ -440,7 +440,7 @@
; a list of the vertices j for which there is an edge from i to j. ; a list of the vertices j for which there is an edge from i to j.
; The last vertex is the root. ; The last vertex is the root.
(: fold-over-rdg (All (State) (Exact-Positive-Integer (: fold-over-rdg (All (State) (Exact-Positive-Integer
Natural Integer
(RDG State -> State) (RDG State -> State)
State State
-> State))) -> State)))
@ -456,20 +456,20 @@
max-out) max-out)
'(assert (procedure? folder) '(assert (procedure? folder)
folder) folder)
(let*: ((root : Natural (let*: ((root : Integer
(- size 1)) (- size 1))
(edge? : Graph (edge? : Graph
(proc->vector size (proc->vector size
(lambda: ((from : Natural)) (lambda: ((from : Integer))
(ann (make-vector size #f) (ann (make-vector size #f)
(Vectorof Boolean))))) (Vectorof Boolean)))))
(edges : RDG (edges : RDG
(make-vector size '())) (make-vector size '()))
(out-degrees : (Vectorof Natural) (out-degrees : (Vectorof Integer)
(make-vector size 0)) (make-vector size 0))
(minimal-folder : (Natural (minimal-folder : (Integer
Graph Graph
((Vectorof Natural) ((Vectorof Integer)
Boolean Boolean
(Boolean -> Boolean) (Boolean -> Boolean)
-> Boolean) -> Boolean)
@ -478,22 +478,22 @@
;; make-minimal?'s type says it can return #f, but it won't ;; make-minimal?'s type says it can return #f, but it won't
(or (make-minimal? root) (or (make-minimal? root)
(error "can't happen"))) (error "can't happen")))
(non-root-minimal? : (Natural -> Boolean) (non-root-minimal? : (Integer -> Boolean)
(let ((cont (let ((cont
(lambda: ((perm : (Vectorof Natural)) (lambda: ((perm : (Vectorof Integer))
(state : Boolean) (state : Boolean)
(accross : (Boolean -> Boolean))) (accross : (Boolean -> Boolean)))
'(assert (eq? state #t) '(assert (eq? state #t)
state) state)
(accross #t)))) (accross #t))))
(lambda: ((size : Natural)) (lambda: ((size : Integer))
(minimal-folder size (minimal-folder size
edge? edge?
cont cont
#t)))) #t))))
(root-minimal? : ( -> Boolean) (root-minimal? : ( -> Boolean)
(let ((cont (let ((cont
(lambda: ((perm : (Vectorof Natural)) (lambda: ((perm : (Vectorof Integer))
(state : Boolean) (state : Boolean)
(accross : (Boolean -> Boolean))) (accross : (Boolean -> Boolean)))
'(assert (eq? state #t) '(assert (eq? state #t)
@ -511,7 +511,7 @@
cont cont
#t))))) #t)))))
(let: _-*- : State (let: _-*- : State
((vertex : Natural ((vertex : Integer
0) 0)
(state : State (state : State
state)) state))
@ -533,11 +533,11 @@
(from-root (from-root
(vector-ref edge? root))) (vector-ref edge? root)))
(let: _-*- : State (let: _-*- : State
((v : Natural ((v : Integer
0) 0)
(outs : Natural (outs : Integer
0) 0)
(efr : (Listof Natural) (efr : (Listof Integer)
'()) '())
(efrr : (Listof (Vectorof Boolean)) (efrr : (Listof (Vectorof Boolean))
'()) '())
@ -568,7 +568,7 @@
(vector-set! edges root efr) (vector-set! edges root efr)
(folder (folder
(proc->vector size (proc->vector size
(lambda: ((i : Natural)) (lambda: ((i : Integer))
(vector-ref edges i))) (vector-ref edges i)))
state)) state))
(else (else
@ -658,32 +658,32 @@
; Given a vector which maps vertex to out-going-edge list, ; Given a vector which maps vertex to out-going-edge list,
; return a vector which gives reachability. ; return a vector which gives reachability.
(: make-reach? (Natural RDG -> Graph)) (: make-reach? (Integer RDG -> Graph))
(define make-reach? (define make-reach?
(lambda (size vertex->out) (lambda (size vertex->out)
(let ((res (let ((res
(proc->vector size (proc->vector size
(lambda: ((v : Natural)) (lambda: ((v : Integer))
(let: ((from-v : (Vectorof Boolean) (let: ((from-v : (Vectorof Boolean)
(make-vector size #f))) (make-vector size #f)))
(vector-set! from-v v #t) (vector-set! from-v v #t)
(for-each (for-each
(lambda: ((x : Natural)) (lambda: ((x : Integer))
(vector-set! from-v x #t)) (vector-set! from-v x #t))
(vector-ref vertex->out v)) (vector-ref vertex->out v))
from-v))))) from-v)))))
(gnatural-for-each size (gnatural-for-each size
(lambda: ((m : Natural)) (lambda: ((m : Integer))
(let ((from-m (let ((from-m
(vector-ref res m))) (vector-ref res m)))
(gnatural-for-each size (gnatural-for-each size
(lambda: ((f : Natural)) (lambda: ((f : Integer))
(let ((from-f (let ((from-f
(vector-ref res f))) (vector-ref res f)))
(if (vector-ref from-f m); [wdc - was when] (if (vector-ref from-f m); [wdc - was when]
(begin (begin
(gnatural-for-each size (gnatural-for-each size
(lambda: ((t : Natural)) (lambda: ((t : Integer))
(if (vector-ref from-m t) (if (vector-ref from-m t)
(begin ; [wdc - was when] (begin ; [wdc - was when]
(vector-set! from-f t #t)) (vector-set! from-f t #t))
@ -707,7 +707,7 @@
(let ((input (with-input-from-file "input.txt" read))) (let ((input (with-input-from-file "input.txt" read)))
(time (time
(let: loop : (Listof RDG) (let: loop : (Listof RDG)
((n : Natural 45) (v : (Listof RDG) '())) ((n : Integer 45) (v : (Listof RDG) '()))
(if (zero? n) (if (zero? n)
v v
(loop (- n 1) (loop (- n 1)

48
collects/tests/racket/benchmarks/common/typed/puzzle.rktl
View File

@ -10,11 +10,11 @@
; Status: Public Domain ; Status: Public Domain
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(: iota (Natural -> (Listof Natural))) (: iota (Integer -> (Listof Integer)))
(define (iota n) (define (iota n)
(do: : (Listof Natural) (do: : (Listof Integer)
((n : Natural n (- n 1)) ((n : Integer n (- n 1))
(list : (Listof Natural) '() (cons (- n 1) list))) (list : (Listof Integer) '() (cons (- n 1) list)))
((zero? n) list))) ((zero? n) list)))
;;; PUZZLE -- Forest Baskett's Puzzle benchmark, originally written in Pascal. ;;; PUZZLE -- Forest Baskett's Puzzle benchmark, originally written in Pascal.
@ -23,17 +23,17 @@
(define classmax 3) (define classmax 3)
(define typemax 12) (define typemax 12)
(: *iii* Natural) (: *iii* Integer)
(define *iii* 0) (define *iii* 0)
(: *kount* Natural) (: *kount* Integer)
(define *kount* 0) (define *kount* 0)
(define *d* 8) (define *d* 8)
(: *piececount* (Vectorof Integer)) (: *piececount* (Vectorof Integer))
(define *piececount* (make-vector (+ classmax 1) 0)) (define *piececount* (make-vector (+ classmax 1) 0))
(: *class* (Vectorof Natural)) (: *class* (Vectorof Integer))
(define *class* (make-vector (+ typemax 1) 0)) (define *class* (make-vector (+ typemax 1) 0))
(: *piecemax* (Vectorof Natural)) (: *piecemax* (Vectorof Integer))
(define *piecemax* (make-vector (+ typemax 1) 0)) (define *piecemax* (make-vector (+ typemax 1) 0))
(: *puzzle* (Vectorof Boolean)) (: *puzzle* (Vectorof Boolean))
(define *puzzle* (make-vector (+ size 1) #f)) (define *puzzle* (make-vector (+ size 1) #f))
@ -44,13 +44,13 @@
(ann (vector #f) (ann (vector #f)
(Vectorof Boolean)))) (Vectorof Boolean))))
(define nothing (define nothing
(for-each (lambda: ((i : Natural)) (for-each (lambda: ((i : Integer))
(vector-set! *p* i (vector-set! *p* i
(ann (make-vector (+ size 1) #f) (ann (make-vector (+ size 1) #f)
(Vectorof Boolean)))) (Vectorof Boolean))))
(iota (+ typemax 1)))) (iota (+ typemax 1))))
(: fit (Natural Natural -> Boolean)) (: fit (Integer Integer -> Boolean))
(define (fit i j) (define (fit i j)
(let ((end (vector-ref *piecemax* i))) (let ((end (vector-ref *piecemax* i)))
(do ((k 0 (+ k 1))) (do ((k 0 (+ k 1)))
@ -59,7 +59,7 @@
(vector-ref *puzzle* (+ j k)))) (vector-ref *puzzle* (+ j k))))
(if (> k end) #t #f))))) (if (> k end) #t #f)))))
(: place (Natural Natural -> Natural)) (: place (Integer Integer -> Integer))
(define (place i j) (define (place i j)
(let ((end (vector-ref *piecemax* i))) (let ((end (vector-ref *piecemax* i)))
(do ((k 0 (+ k 1))) (do ((k 0 (+ k 1)))
@ -76,7 +76,7 @@
; (display "*Puzzle* filled") ; (display "*Puzzle* filled")
(if (> k size) 0 k))))) (if (> k size) 0 k)))))
(: puzzle-remove (Natural Natural -> Void)) (: puzzle-remove (Integer Integer -> Void))
(define (puzzle-remove i j) (define (puzzle-remove i j)
(let ((end (vector-ref *piecemax* i))) (let ((end (vector-ref *piecemax* i)))
(do ((k 0 (+ k 1))) (do ((k 0 (+ k 1)))
@ -89,13 +89,13 @@
(+ (vector-ref *piececount* (vector-ref *class* i)) 1)))) (+ (vector-ref *piececount* (vector-ref *class* i)) 1))))
(: trial (Natural -> Any)) (: trial (Integer -> Any))
(define (trial j) (define (trial j)
(let: ((k : Natural 0)) (let: ((k : Integer 0))
(call-with-current-continuation (call-with-current-continuation
(lambda: ((return : (Boolean -> Nothing))) (lambda: ((return : (Boolean -> Nothing)))
(do: : Any (do: : Any
((i : Natural 0 (+ i 1))) ((i : Integer 0 (+ i 1)))
((> i typemax) (set! *kount* (+ *kount* 1)) '()) ((> i typemax) (set! *kount* (+ *kount* 1)) '())
(cond (cond
((not ((not
@ -111,7 +111,7 @@
(return #t)) (return #t))
(else (puzzle-remove i j)))))))))))) (else (puzzle-remove i j))))))))))))
(: trial-output (Natural Natural -> Void)) (: trial-output (Integer Integer -> Void))
(define (trial-output x y) (define (trial-output x y)
(newline) (newline)
(display (string-append "Piece " (display (string-append "Piece "
@ -120,17 +120,17 @@
(number->string y #;'(int)) (number->string y #;'(int))
"."))) ".")))
(: definePiece (Natural Natural Natural Natural -> Void)) (: definePiece (Integer Integer Integer Integer -> Void))
(define (definePiece iclass ii jj kk) (define (definePiece iclass ii jj kk)
(let: ((index : Natural 0)) (let: ((index : Integer 0))
(do: : Void (do: : Void
((i : Natural 0 (+ i 1))) ((i : Integer 0 (+ i 1)))
((> i ii)) ((> i ii))
(do: : Void (do: : Void
((j : Natural 0 (+ j 1))) ((j : Integer 0 (+ j 1)))
((> j jj)) ((> j jj))
(do: : Void (do: : Void
((k : Natural 0 (+ k 1))) ((k : Integer 0 (+ k 1)))
((> k kk)) ((> k kk))
(set! index (+ i (* *d* (+ j (* *d* k))))) (set! index (+ i (* *d* (+ j (* *d* k)))))
(vector-set! (vector-ref *p* *iii*) index #t)))) (vector-set! (vector-ref *p* *iii*) index #t))))
@ -178,8 +178,8 @@
(vector-set! *piececount* 1 3) (vector-set! *piececount* 1 3)
(vector-set! *piececount* 2 1) (vector-set! *piececount* 2 1)
(vector-set! *piececount* 3 1) (vector-set! *piececount* 3 1)
(let: ((m : Natural (+ (* *d* (+ *d* 1)) 1)) (let: ((m : Integer (+ (* *d* (+ *d* 1)) 1))
(n : Natural 0)) (n : Integer 0))
(cond ((fit 0 m) (set! n (place 0 m))) (cond ((fit 0 m) (set! n (place 0 m)))
(else (begin (newline) (display "Error.")))) (else (begin (newline) (display "Error."))))
(cond ((trial n) (cond ((trial n)
@ -192,7 +192,7 @@
;;; call: (start) ;;; call: (start)
(time (let: loop : Void ((n : Natural 50) (v : Void (void))) (time (let: loop : Void ((n : Integer 50) (v : Void (void)))
(if (zero? n) (if (zero? n)
v v
(loop (- n 1) (loop (- n 1)

28
collects/tests/racket/benchmarks/common/typed/triangle.rktl
View File

@ -13,28 +13,28 @@
;;; TRIANG -- Board game benchmark. ;;; TRIANG -- Board game benchmark.
(: *board* (Vectorof Natural)) (: *board* (Vectorof Integer))
(define *board* (make-vector 16 1)) (define *board* (make-vector 16 1))
(: *sequence* (Vectorof Natural)) (: *sequence* (Vectorof Integer))
(define *sequence* (make-vector 14 0)) (define *sequence* (make-vector 14 0))
(: *a* (Vectorof Natural)) (: *a* (Vectorof Integer))
(define *a* (make-vector 37)) (define *a* (make-vector 37))
(: *b* (Vectorof Natural)) (: *b* (Vectorof Integer))
(define *b* (make-vector 37)) (define *b* (make-vector 37))
(: *c* (Vectorof Natural)) (: *c* (Vectorof Integer))
(define *c* (make-vector 37)) (define *c* (make-vector 37))
(: *answer* (Listof (Listof Natural))) (: *answer* (Listof (Listof Integer)))
(define *answer* '()) (define *answer* '())
(: *final* (Listof Natural)) (: *final* (Listof Integer))
(define *final* '()) (define *final* '())
(: last-position ( -> Natural)) (: last-position ( -> Integer))
(define (last-position) (define (last-position)
(do ((i 1 (+ i 1))) (do ((i 1 (+ i 1)))
((or (= i 16) (= 1 (vector-ref *board* i))) ((or (= i 16) (= 1 (vector-ref *board* i)))
(if (= i 16) 0 i)))) (if (= i 16) 0 i))))
(: ttry (Natural Natural -> Any)) (: ttry (Integer Integer -> Any))
(define (ttry i depth) (define (ttry i depth)
(cond ((= depth 14) (cond ((= depth 14)
(let ((lp (last-position))) (let ((lp (last-position)))
@ -59,27 +59,27 @@
(vector-set! *board* (vector-ref *c* i) 0) '()) (vector-set! *board* (vector-ref *c* i) 0) '())
(else #f))) (else #f)))
(: gogogo (Natural -> Any)) (: gogogo (Integer -> Any))
(define (gogogo i) (define (gogogo i)
(let ((*answer* '()) (let ((*answer* '())
(*final* '())) (*final* '()))
(ttry i 1))) (ttry i 1)))
(for-each (lambda: ((i : Natural) (x : Natural)) (vector-set! *a* i x)) (for-each (lambda: ((i : Integer) (x : Integer)) (vector-set! *a* i x))
'(0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 '(0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20
21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36) 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36)
'(1 2 4 3 5 6 1 3 6 2 5 4 11 12 '(1 2 4 3 5 6 1 3 6 2 5 4 11 12
13 7 8 4 4 7 11 8 12 13 6 10 13 7 8 4 4 7 11 8 12 13 6 10
15 9 14 13 13 14 15 9 10 15 9 14 13 13 14 15 9 10
6 6)) 6 6))
(for-each (lambda: ((i : Natural) (x : Natural)) (vector-set! *b* i x)) (for-each (lambda: ((i : Integer) (x : Integer)) (vector-set! *b* i x))
'(0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 '(0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20
21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36) 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36)
'(2 4 7 5 8 9 3 6 10 5 9 8 '(2 4 7 5 8 9 3 6 10 5 9 8
12 13 14 8 9 5 2 4 7 5 8 12 13 14 8 9 5 2 4 7 5 8
9 3 6 10 5 9 8 12 13 14 9 3 6 10 5 9 8 12 13 14
8 9 5 5)) 8 9 5 5))
(for-each (lambda: ((i : Natural) (x : Natural)) (vector-set! *c* i x)) (for-each (lambda: ((i : Integer) (x : Integer)) (vector-set! *c* i x))
'(0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 '(0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20
21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36) 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36)
'(4 7 11 8 12 13 6 10 15 9 14 13 '(4 7 11 8 12 13 6 10 15 9 14 13
@ -89,7 +89,7 @@
;;; call: (gogogo 22)) ;;; call: (gogogo 22))
(time (let: loop : 'done ((n : Natural 1000000)) (time (let: loop : 'done ((n : Integer 1000000))
(if (zero? n) (if (zero? n)
'done 'done
(begin (begin

8
collects/tests/racket/benchmarks/shootout/typed/nsieve.rktl
View File

@ -9,7 +9,7 @@
(require scheme/cmdline) (require scheme/cmdline)
(: nsieve (Natural -> Natural)) (: nsieve (Integer -> Integer))
(define (nsieve m) (define (nsieve m)
(let: ((a : (Vectorof Boolean) (make-vector m #t))) (let: ((a : (Vectorof Boolean) (make-vector m #t)))
(let loop ((i 2) (n 0)) (let loop ((i 2) (n 0))
@ -24,9 +24,9 @@
(loop (+ 1 i) n)) (loop (+ 1 i) n))
n)))) n))))
(: string-pad (String Natural -> String)) (: string-pad (String Integer -> String))
(define (string-pad s len) (define (string-pad s len)
(string-append (make-string (assert (- len (string-length s)) exact-nonnegative-integer?) #\space) (string-append (make-string (- len (string-length s)))
s)) s))
(: test (Natural -> Void)) (: test (Natural -> Void))
@ -37,7 +37,7 @@
(string-pad (number->string m) 8) (string-pad (number->string m) 8)
(string-pad (number->string count) 8)))) (string-pad (number->string count) 8))))
(: main (Natural -> Void)) (: main (Integer -> Void))
(define (main n) (define (main n)
(when (>= n 0) (test n)) (when (>= n 0) (test n))
(when (>= n 1) (test (assert (- n 1) exact-nonnegative-integer?))) (when (>= n 1) (test (assert (- n 1) exact-nonnegative-integer?)))

18
collects/tests/racket/benchmarks/shootout/typed/nsievebits.rktl
View File

@ -7,7 +7,7 @@
(require scheme/cmdline) (require scheme/cmdline)
(: make-bit-vector (Natural -> Bytes)) (: make-bit-vector (Integer -> Bytes))
(define (make-bit-vector size) (define (make-bit-vector size)
(let* ((len (quotient (+ size 7) 8)) (let* ((len (quotient (+ size 7) 8))
(res (make-bytes len #b11111111))) (res (make-bytes len #b11111111)))
@ -16,7 +16,7 @@
(bytes-set! res (- len 1) (- (arithmetic-shift 1 off) 1)))) (bytes-set! res (- len 1) (- (arithmetic-shift 1 off) 1))))
res)) res))
(: bit-vector-ref (Bytes Natural -> Boolean)) (: bit-vector-ref (Bytes Integer -> Boolean))
(define (bit-vector-ref vec i) (define (bit-vector-ref vec i)
(let ((byte (arithmetic-shift i -3)) (let ((byte (arithmetic-shift i -3))
(off (bitwise-and i #x7))) (off (bitwise-and i #x7)))
@ -24,7 +24,7 @@
(not (zero? (bitwise-and (bytes-ref vec byte) (not (zero? (bitwise-and (bytes-ref vec byte)
(arithmetic-shift 1 off))))))) (arithmetic-shift 1 off)))))))
(: bit-vector-set! (Bytes Natural Boolean -> Void)) (: bit-vector-set! (Bytes Integer Boolean -> Void))
(define (bit-vector-set! vec i x) (define (bit-vector-set! vec i x)
(let ((byte (arithmetic-shift i -3)) (let ((byte (arithmetic-shift i -3))
(off (bitwise-and i #x7))) (off (bitwise-and i #x7)))
@ -36,23 +36,23 @@
(bitwise-ior val mask) (bitwise-ior val mask)
(bitwise-and val (bitwise-not mask))))))) (bitwise-and val (bitwise-not mask)))))))
(: nsievebits (Natural -> Natural)) (: nsievebits (Integer -> Integer))
(define (nsievebits m) (define (nsievebits m)
(let ((a (make-bit-vector m))) (let ((a (make-bit-vector m)))
(: clear (Natural -> Void)) (: clear (Integer -> Void))
(define (clear i) (define (clear i)
(do: : Void (do: : Void
([j : Natural (+ i i) (+ j i)]) ([j : Integer (+ i i) (+ j i)])
((>= j m)) ((>= j m))
(bit-vector-set! a j #f))) (bit-vector-set! a j #f)))
(let: ([c : Natural 0]) (let: ([c : Integer 0])
(do ([i 2 (add1 i)]) (do ([i 2 (add1 i)])
((>= i m) c) ((>= i m) c)
(when (bit-vector-ref a i) (when (bit-vector-ref a i)
(clear i) (clear i)
(set! c (add1 c))))))) (set! c (add1 c)))))))
(: string-pad (String Natural -> String)) (: string-pad (String Integer -> String))
(define (string-pad s len) (define (string-pad s len)
(string-append (make-string (- len (string-length s)) #\space) (string-append (make-string (- len (string-length s)) #\space)
s)) s))
@ -65,7 +65,7 @@
(string-pad (number->string m) 8) (string-pad (number->string m) 8)
(string-pad (number->string count) 8)))) (string-pad (number->string count) 8))))
(: main (Natural -> Void)) (: main (Integer -> Void))
(define (main n) (define (main n)
(when (>= n 0) (test n)) (when (>= n 0) (test n))
(when (>= n 1) (test (assert (- n 1) exact-nonnegative-integer?))) (when (>= n 1) (test (assert (- n 1) exact-nonnegative-integer?)))

16
collects/tests/racket/benchmarks/shootout/typed/spectralnorm.rktl
View File

@ -5,15 +5,15 @@
(require racket/cmdline racket/trace racket/contract (require racket/cmdline racket/trace racket/contract
racket/unsafe/ops racket/flonum) racket/unsafe/ops racket/flonum)
(let* ([A (lambda: ((i : Natural) (j : Natural)) (let* ([A (lambda: ((i : Integer) (j : Integer))
(let ([ij (unsafe-fx+ i j)]) (let ([ij (unsafe-fx+ i j)])
(unsafe-fl/ 1.0 (unsafe-fl+ (unsafe-fl* (unsafe-fl* (unsafe-fx->fl ij) (unsafe-fl/ 1.0 (unsafe-fl+ (unsafe-fl* (unsafe-fl* (unsafe-fx->fl ij)
(unsafe-fx->fl (unsafe-fx+ ij 1))) (unsafe-fx->fl (unsafe-fx+ ij 1)))
0.5) 0.5)
(unsafe-fx->fl (unsafe-fx+ i 1))))))] (unsafe-fx->fl (unsafe-fx+ i 1))))))]
[Av [Av
(lambda: ((x : FlVector) (y : FlVector) (N : Natural)) (lambda: ((x : FlVector) (y : FlVector) (N : Integer))
(for: ([i : Natural (in-range N)]) (for: ([i : Integer (in-range N)])
(unsafe-flvector-set! (unsafe-flvector-set!
y i y i
(let L ([a 0.0] [j 0]) (let L ([a 0.0] [j 0])
@ -21,26 +21,26 @@
(L (unsafe-fl+ a (unsafe-fl* (unsafe-flvector-ref x j) (A i j))) (L (unsafe-fl+ a (unsafe-fl* (unsafe-flvector-ref x j) (A i j)))
(unsafe-fx+ j 1)))))))] (unsafe-fx+ j 1)))))))]
[Atv [Atv
(lambda: ((x : FlVector) (y : FlVector) (N : Natural)) (lambda: ((x : FlVector) (y : FlVector) (N : Integer))
(for: ([i : Natural (in-range N)]) (for: ([i : Integer (in-range N)])
(unsafe-flvector-set! (unsafe-flvector-set!
y i y i
(let L ([a 0.0] [j 0]) (let L ([a 0.0] [j 0])
(if (unsafe-fx= j N) a (if (unsafe-fx= j N) a
(L (unsafe-fl+ a (unsafe-fl* (unsafe-flvector-ref x j) (A j i))) (L (unsafe-fl+ a (unsafe-fl* (unsafe-flvector-ref x j) (A j i)))
(unsafe-fx+ j 1)))))))] (unsafe-fx+ j 1)))))))]
[AtAv (lambda: ((x : FlVector) (y : FlVector) (t : FlVector) (N : Natural)) [AtAv (lambda: ((x : FlVector) (y : FlVector) (t : FlVector) (N : Integer))
(Av x t N) (Atv t y N))] (Av x t N) (Atv t y N))]
[N (command-line #:args (#{n : String}) (assert (string->number n) exact-nonnegative-integer?))] [N (command-line #:args (#{n : String}) (assert (string->number n) exact-nonnegative-integer?))]
[u (make-flvector N 1.0)] [u (make-flvector N 1.0)]
[v (make-flvector N)] [v (make-flvector N)]
[t (make-flvector N)]) [t (make-flvector N)])
(for: ([i : Natural (in-range 10)]) (for: ([i : Integer (in-range 10)])
(AtAv u v t N) (AtAv u v t N)
(AtAv v u t N)) (AtAv v u t N))
(displayln (real->decimal-string (displayln (real->decimal-string
(unsafe-flsqrt (unsafe-flsqrt
(let: L : Float ([vBv : Float 0.0] [vv : Float 0.0] [i : Natural 0]) (let: L : Float ([vBv : Float 0.0] [vv : Float 0.0] [i : Integer 0])
(if (unsafe-fx= i N) (unsafe-fl/ vBv vv) (if (unsafe-fx= i N) (unsafe-fl/ vBv vv)
(let ([ui (unsafe-flvector-ref u i)] [vi (unsafe-flvector-ref v i)]) (let ([ui (unsafe-flvector-ref u i)] [vi (unsafe-flvector-ref v i)])
(L (unsafe-fl+ vBv (unsafe-fl* ui vi)) (L (unsafe-fl+ vBv (unsafe-fl* ui vi))

16
collects/tests/typed-scheme/succeed/metrics.rkt
View File

@ -84,11 +84,11 @@
[table [table
`((,a-hits ,b-hits) `((,a-hits ,b-hits)
(,a-misses ,b-misses))] (,a-misses ,b-misses))]
[expected (lambda: ([i : Natural] [j : Natural]) [expected (lambda: ([i : Integer] [j : Integer])
(/ (* (row-total i table) (col-total j table)) total-subjects))]) (/ (* (row-total i table) (col-total j table)) total-subjects))])
(exact->inexact (exact->inexact
(table-sum (table-sum
(lambda: ([i : Natural] [j : Natural]) (lambda: ([i : Integer] [j : Integer])
(/ (sqr (- (expected i j) (table-ref i j table))) (expected i j))) (/ (sqr (- (expected i j) (table-ref i j table))) (expected i j)))
table))))) table)))))
@ -473,7 +473,7 @@
(show result )))) (show result ))))
;; applies only to the combined metric [or more generally to listof-answer results] ;; applies only to the combined metric [or more generally to listof-answer results]
(pdefine: (a b c) (total [experiment-number : Natural] [result : (Result (Listof number) b c)]) : (Listof number) (pdefine: (a b c) (total [experiment-number : Integer] [result : (Result (Listof number) b c)]) : (Listof number)
(define: (total/s [s : Table]) : number (apply + (list-ref (pivot s) experiment-number))) (define: (total/s [s : Table]) : number (apply + (list-ref (pivot s) experiment-number)))
(list (total/s (result-seqA result)) (total/s (result-seqB result)))) (list (total/s (result-seqA result)) (total/s (result-seqB result))))
@ -491,7 +491,7 @@
[(null? l) '()] [(null? l) '()]
[else [else
(let ([n (length (car l))]) (let ([n (length (car l))])
(build-list n (lambda: ([i : Natural]) (map (lambda: ([j : (Listof X)]) (list-ref j i)) l))))])) (build-list n (lambda: ([i : Integer]) (map (lambda: ([j : (Listof X)]) (list-ref j i)) l))))]))
(define: (sqr [x : Real]) : Real (* x x)) (define: (sqr [x : Real]) : Real (* x x))
(define: (variance [xs : (Listof Real)]): Real (define: (variance [xs : (Listof Real)]): Real
@ -499,13 +499,13 @@
(/ (apply + (map (lambda: ([x : number]) (sqr (- x avg))) xs)) (/ (apply + (map (lambda: ([x : number]) (sqr (- x avg))) xs))
(sub1 (length xs))))) (sub1 (length xs)))))
(define: (table-ref [i : Natural] [j : Natural] [table : Table]): number (define: (table-ref [i : Integer] [j : Integer] [table : Table]): number
(list-ref (list-ref table i) j)) (list-ref (list-ref table i) j))
(define: (row-total [i : Natural] [table : Table]) : number (define: (row-total [i : Integer] [table : Table]) : number
(apply + (list-ref table i))) (apply + (list-ref table i)))
(define: (col-total [j : Natural] [table : Table]) : number (define: (col-total [j : Integer] [table : Table]) : number
(apply + (map (lambda: ([x : (Listof number)]) (list-ref x j)) table))) (apply + (map (lambda: ([x : (Listof number)]) (list-ref x j)) table)))
(define: (table-sum [f : (Natural Natural -> Real)] [table : Table]) : number (define: (table-sum [f : (Integer Integer -> Real)] [table : Table]) : number
(let ([rows (length table)] (let ([rows (length table)]
[cols (length (car table))]) [cols (length (car table))])
(let loop ([i 0] [j 0] [#{sum : Real} 0]) (let loop ([i 0] [j 0] [#{sum : Real} 0])

14
collects/tests/typed-scheme/succeed/new-metrics.rkt
View File

@ -61,7 +61,7 @@
[table [table
`((,a-hits ,b-hits) `((,a-hits ,b-hits)
(,a-misses ,b-misses))] (,a-misses ,b-misses))]
[expected (λ: ([i : Natural] [j : Natural]) [expected (λ: ([i : Integer] [j : Integer])
(/ (* (row-total i table) (col-total j table)) total-subjects))]) (/ (* (row-total i table) (col-total j table)) total-subjects))])
(exact->inexact (exact->inexact
(table-sum (table-sum
@ -425,7 +425,7 @@
(show result)))) (show result))))
;; applies only to the combined metric [or more generally to listof-answer results] ;; applies only to the combined metric [or more generally to listof-answer results]
(: total (All (b c) (Natural (result (Listof Number) b c) -> (Listof Number)))) (: total (All (b c) (Integer (result (Listof Number) b c) -> (Listof Number))))
(define (total experiment-number result) (define (total experiment-number result)
(: total/s (Table -> Number)) (: total/s (Table -> Number))
(define (total/s s) (apply + (list-ref (pivot s) experiment-number))) (define (total/s s) (apply + (list-ref (pivot s) experiment-number)))
@ -447,7 +447,7 @@
[(null? l) '()] [(null? l) '()]
[else [else
(let ([n (length (car l))]) (let ([n (length (car l))])
(build-list n (λ: ([i : Natural]) (map (λ: ([j : (Listof X)]) (list-ref j i)) l))))])) (build-list n (λ: ([i : Integer]) (map (λ: ([j : (Listof X)]) (list-ref j i)) l))))]))
(: variance ((Listof Number) -> Number)) (: variance ((Listof Number) -> Number))
(define (variance xs) (define (variance xs)
@ -455,16 +455,16 @@
(/ (apply + (map (λ: ([x : Number]) (sqr (- x avg))) xs)) (/ (apply + (map (λ: ([x : Number]) (sqr (- x avg))) xs))
(sub1 (length xs))))) (sub1 (length xs)))))
(: table-ref (Natural Natural Table -> Number)) (: table-ref (Integer Integer Table -> Number))
(define (table-ref i j table) (define (table-ref i j table)
(list-ref (list-ref table i) j)) (list-ref (list-ref table i) j))
(: row-total (Natural Table -> Number)) (: row-total (Integer Table -> Number))
(define (row-total i table) (define (row-total i table)
(apply + (list-ref table i))) (apply + (list-ref table i)))
(: col-total (Natural Table -> Number)) (: col-total (Integer Table -> Number))
(define (col-total j table) (define (col-total j table)
(apply + (map (λ: ([x : (Listof Number)]) (list-ref x j)) table))) (apply + (map (λ: ([x : (Listof Number)]) (list-ref x j)) table)))
(: table-sum ((Natural Natural -> Number) Table -> Number)) (: table-sum ((Integer Integer -> Number) Table -> Number))
(define (table-sum f table) (define (table-sum f table)
(let ([rows (length table)] (let ([rows (length table)]
[cols (length (car table))]) [cols (length (car table))])

4
collects/tests/typed-scheme/unit-tests/typecheck-tests.rkt
View File

@ -154,10 +154,10 @@
[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-HeterogenousVector (list -Nat -Nat -Nat))] [tc-e/t #(3 4 5) (make-HeterogenousVector (list -Integer -Integer -Integer))]
[tc-e/t '(2 3 4) (-lst* -PositiveFixnum -PositiveFixnum -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) (-lst* -PositiveFixnum -PositiveFixnum (-val #t))]
[tc-e/t #(2 3 #t) (make-HeterogenousVector (list -Nat -Nat (-val #t)))] [tc-e/t #(2 3 #t) (make-HeterogenousVector (list -Integer -Integer (-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)))]

2
collects/typed-scheme/private/base-env-indexing-abs.rkt
View File

@ -137,7 +137,7 @@
[unsafe-vector-set! (-poly (a) (-> (-vec a) index-type a -Void))] [unsafe-vector-set! (-poly (a) (-> (-vec a) index-type a -Void))]
[unsafe-vector*-set! (-poly (a) (-> (-vec a) index-type a -Void))] [unsafe-vector*-set! (-poly (a) (-> (-vec a) index-type a -Void))]
[vector-copy! (-poly (a) ((-vec a) index-type (-vec a) [index-type index-type] . ->opt . -Void))] [vector-copy! (-poly (a) ((-vec a) index-type (-vec a) [index-type index-type] . ->opt . -Void))]
[make-vector (-poly (a) (cl-> [(index-type) (-vec (Un -Nat a))] [make-vector (-poly (a) (cl-> [(index-type) (-vec (Un -Integer a))]
[(index-type a) (-vec a)]))] [(index-type a) (-vec a)]))]
[bytes-ref (-> -Bytes index-type -NonnegativeFixnum)] [bytes-ref (-> -Bytes index-type -NonnegativeFixnum)]

3
collects/typed-scheme/types/convenience.rkt
View File

@ -30,9 +30,8 @@
(let loop ([t* t]) (let loop ([t* t])
(match t* (match t*
[(Value: '()) (-lst Univ)] [(Value: '()) (-lst Univ)]
[(Value: 0) -Nat] [(Value: 0) -Integer]
[(List: ts) (-lst (apply Un ts))] [(List: ts) (-lst (apply Un ts))]
[(? (lambda (t) (subtype t -Nat))) -Nat]
[(? (lambda (t) (subtype t -Integer))) -Integer] [(? (lambda (t) (subtype t -Integer))) -Integer]
[(? (lambda (t) (subtype t -Flonum))) -Flonum] [(? (lambda (t) (subtype t -Flonum))) -Flonum]
[(Mu: var (Union: (list (Value: '()) (Pair: _ (F: var))))) t*] [(Mu: var (Union: (list (Value: '()) (Pair: _ (F: var))))) t*]