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

checkpoint

Browse Source 
svn: r16931

original commit: 750c971d0727b495c55fb090e38d3fb3001d3624
This commit is contained in:
Sam Tobin-Hochstadt 2009-11-21 00:11:37 +00:00
parent 28890f267f
commit e5c1d9e02b
16 changed files with 208 additions and 224 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
collects/tests/typed-scheme/fail/back-and-forth.ss
View File

@ -1,9 +1,9 @@
#;
(exn-pred exn:fail:contract? #rx".*contract.*\\(-> number\\? number\\?\\).*")
(exn-pred exn:fail:contract? #rx".*contract.*\\(-> Number Number\\).*")
#lang scheme/load
(module m typed-scheme
(module m typed/scheme
(: f (Number -> Number))
(define (f x) (add1 x))
(provide f))

18
collects/tests/typed-scheme/succeed/metrics.ss
View File

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

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

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

2
collects/tests/typed-scheme/succeed/random-bits.ss
View File

@ -351,7 +351,7 @@
(define: w-sqr1 : Nb 209) ; w^2 mod m1
(define: w-sqr2 : Nb 22853) ; w^2 mod m2
(define: (lc [i0 : Nb] [i1 : Nb] [i2 : Nb] [j0 : Nb] [j1 : Nb] [j2 : Nb] [m : Nb ] [w-sqr : Nb ]): Nb ; linear combination
(define: (lc [i0 : Natural] [i1 : Natural] [i2 : Natural] [j0 : Natural] [j1 : Natural] [j2 : Natural] [m : Nb] [w-sqr : Nb ]): Nb ; linear combination
(let ((a0h (quotient (vector-ref A i0) w))
(a0l (modulo (vector-ref A i0) w))
(a1h (quotient (vector-ref A i1) w))

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

@ -1,66 +1,89 @@
#lang s-exp "env-lang.ss"
(require
scheme/tcp
scheme
scheme/unsafe/ops
(only-in rnrs/lists-6 fold-left)
'#%paramz
"extra-procs.ss"
(only-in '#%kernel [apply kernel:apply])
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] [-Real R] [-ExactPositiveInteger -Pos])))
(begin
(require
scheme/tcp
scheme
scheme/unsafe/ops
(only-in rnrs/lists-6 fold-left)
'#%paramz
"extra-procs.ss"
(only-in '#%kernel [apply kernel:apply])
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] [-Real R] [-ExactPositiveInteger -Pos])))
(define-for-syntax all-num-types (list -Pos -Nat -Integer -ExactRational -Flonum -Real N))
;; numeric operations
[modulo (cl->* (-Integer -Integer . -> . -Integer))]
[= (->* (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)]
(define-for-syntax fl-comp (-> -Flonum -Flonum B))
(define-for-syntax fl-op (-> -Flonum -Flonum -Flonum))
(define-for-syntax fl-unop (-> -Flonum -Flonum))
(define-for-syntax real-comp (->* (list R R) R B))
)
;; numeric predicates
[zero? (make-pred-ty (list N) B -Zero)]
[* (apply cl->*
(for/list ([t (list -Pos -Nat -Integer -ExactRational -Flonum -Real N)])
(->* (list) t t)))]
[/ (apply cl->*
(for/list ([t (list -Integer -ExactRational -Flonum -Real N)])
(->* (list t) t t)))]
[+ (apply cl->*
(for/list ([t (list -Pos -Nat -Integer -ExactRational -Flonum -Real N)])
(->* (list) t t)))]
[number? (make-pred-ty N)]
[integer? (Univ . -> . B : (-LFS (list (-filter -Real)) (list (-not-filter -Integer))))]
[exact-integer? (make-pred-ty -Integer)]
[real? (make-pred-ty -Real)]
[complex? (make-pred-ty N)]
[rational? (make-pred-ty -Real)]
[positive? (-> -Real B)]
[negative? (-> -Real B)]
[odd? (-> -Integer B)]
[even? (-> -Integer B)]
[modulo (cl->* (-Integer -Integer . -> . -Integer))]
[= (->* (list N N) N B)]
[>= real-comp]
[< real-comp]
[<= real-comp]
[> real-comp]
[* (apply cl->* (for/list ([t all-num-types]) (->* (list) t t)))]
[+ (apply cl->* (for/list ([t all-num-types]) (->* (list) t t)))]
[- (apply cl->*
(for/list ([t (list -Integer -ExactRational -Flonum -Real N)])
(->* (list t) t t)))]
[max (apply cl->*
(for/list ([t (list -Pos -Nat -Integer -ExactRational -Flonum -Real N)])
(->* (list t) t t)))]
[min (apply cl->*
(for/list ([t (list -Pos -Nat -Integer -ExactRational -Flonum -Real N)])
(->* (list t) t t)))]
[positive? (-> N B)]
[negative? (-> N B)]
[odd? (-> -Integer B)]
[even? (-> -Integer B)]
[/ (apply cl->*
(->* (list -Integer) -Integer -ExactRational)
(for/list ([t (list -ExactRational -Flonum -Real N)])
(->* (list t) t t)))]
[max (apply cl->* (for/list ([t all-num-types]) (->* (list t) t t)))]
[min (apply cl->* (for/list ([t all-num-types]) (->* (list t) t t)))]
[add1 (cl->* (-> -Pos -Pos)
(-> -Nat -Nat)
(-> -Nat -Pos)
(-> -Integer -Integer)
(-> -ExactRational -ExactRational)
(-> -Flonum -Flonum)
(-> -Real -Real)
(-> N N))]
[sub1 (cl->* (-> -Pos -Nat)
(-> -Integer -Integer)
(-> -ExactRational -ExactRational)
(-> -Flonum -Flonum)
(-> -Real -Real)
(-> N N))]
[quotient (-Integer -Integer . -> . -Integer)]
[remainder (-Integer -Integer . -> . -Integer)]
[quotient/remainder
(make-Function (list (make-arr (list -Integer -Integer) (-values (list -Integer -Integer)))))]
;; exactness
[exact? (N . -> . B)]
[inexact? (N . -> . B)]
[exact->inexact (cl->*
@ -70,13 +93,6 @@
(-Real . -> . -ExactRational)
(N . -> . N))]
[number? (make-pred-ty N)]
[integer? (Univ . -> . B : (-LFS (list (-filter N)) (list (-not-filter -Integer))))]
[exact-integer? (make-pred-ty -Integer)]
[real? (make-pred-ty -Real)]
[complex? (make-pred-ty N)]
[rational? (make-pred-ty -Real)]
[floor (-> N N)]
[ceiling (-> N N)]
[truncate (-> N N)]
@ -124,4 +140,17 @@
[sinh (N . -> . N)]
[cosh (N . -> . N)]
[tanh (N . -> . N)]
;; end numeric ops
;; unsafe numeric ops
[unsafe-flabs fl-unop]
[unsafe-fl+ fl-op]
[unsafe-fl- fl-op]
[unsafe-fl* fl-op]
[unsafe-fl/ fl-op]
[unsafe-fl= fl-comp]
[unsafe-fl<= fl-comp]
[unsafe-fl>= fl-comp]
[unsafe-fl> fl-comp]
[unsafe-fl< fl-comp]

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

@ -65,8 +65,7 @@
[eqv? (-> Univ Univ B)]
[equal? (-> Univ Univ B)]
[assert (-poly (a) (-> (Un a (-val #f)) a))]
[gensym (cl-> [(Sym) Sym]
[() Sym])]
[gensym (->opt [Sym] Sym)]
[string-append (->* null -String -String)]
[open-input-string (-> -String -Input-Port)]
[open-output-file
@ -77,15 +76,12 @@
'must-truncate 'truncate/replace)
#f
-Output-Port)]
[read (cl->
[(-Port) -Sexp]
[() -Sexp])]
[read (->opt [-Input-Port] -Sexp)]
[ormap (-polydots (a c b) (->... (list (->... (list a) (b b) c) (-lst a)) ((-lst b) b) c))]
[andmap (-polydots (a c b) (cl->*
;(make-pred-ty (list (make-pred-ty (list a) B d) (-lst a)) B (-lst d))
(->... (list (->... (list a) (b b) c) (-lst a)) ((-lst b) b) c)))]
[newline (cl-> [() -Void]
[(-Port) -Void])]
[newline (->opt [-Output-Port] -Void)]
[not (-> Univ B)]
[box (-poly (a) (a . -> . (-box a)))]
[unbox (-poly (a) ((-box a) . -> . a))]
@ -130,12 +126,9 @@
[remove (-poly (a) (a (-lst a) . -> . (-lst a)))]
[remq (-poly (a) (a (-lst a) . -> . (-lst a)))]
[remv (-poly (a) (a (-lst a) . -> . (-lst a)))]
[remove* (-poly (a b) (cl-> [((-lst a) (-lst a)) (-lst a)]
[((-lst a) (-lst b) (a b . -> . B)) (-lst b)]))]
[remq* (-poly (a b) (cl-> [((-lst a) (-lst a)) (-lst a)]
[((-lst a) (-lst b) (a b . -> . B)) (-lst b)]))]
[remv* (-poly (a b) (cl-> [((-lst a) (-lst a)) (-lst a)]
[((-lst a) (-lst b) (a b . -> . B)) (-lst b)]))]
[remove* (-poly (a b) ((-lst a) (-lst a) [(a b . -> . B)] . ->opt . (-lst b)))]
[remq* (-poly (a b) (cl-> [((-lst a) (-lst a)) (-lst a)]))]
[remv* (-poly (a b) (cl-> [((-lst a) (-lst a)) (-lst a)]))]
(error
(make-Function (list
@ -143,16 +136,14 @@
(make-arr (list -String) (Un) #:rest Univ)
(make-arr (list Sym) (Un)))))
[namespace-variable-value
(cl-> [(Sym) Univ]
[(Sym B -Namespace (-> Univ)) Univ])]
[namespace-variable-value (Sym [Univ (-opt (-> Univ)) -Namespace] . ->opt . Univ)]
[match:error (Univ . -> . (Un))]
[match-equality-test (-Param (Univ Univ . -> . Univ) (Univ Univ . -> . Univ))]
[matchable? (make-pred-ty (Un -String -Bytes))]
[display (cl-> [(Univ) -Void] [(Univ -Port) -Void])]
[write (cl-> [(Univ) -Void] [(Univ -Port) -Void])]
[print (cl-> [(Univ) -Void] [(Univ -Port) -Void])]
[display (Univ [-Output-Port] . ->opt . -Void)]
[write (Univ [-Output-Port] . ->opt . -Void)]
[print (Univ [-Output-Port] . ->opt . -Void)]
[void (->* '() Univ -Void)]
[void? (make-pred-ty -Void)]
[printf (->* (list -String) Univ -Void)]
@ -163,10 +154,10 @@
[sleep (N . -> . -Void)]
[build-list (-poly (a) (-Integer (-Integer . -> . a) . -> . (-lst a)))]
[build-list (-poly (a) (-Nat (-Nat . -> . a) . -> . (-lst a)))]
[reverse (-poly (a) (-> (-lst a) (-lst a)))]
[append (-poly (a) (->* (list) (-lst a) (-lst a)))]
[length (-poly (a) (-> (-lst a) -Integer))]
[length (-poly (a) (-> (-lst a) -Nat))]
[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))))]
@ -212,9 +203,7 @@
[string-copy (-> -String -String)]
[string->immutable-string (-> -String -String)]
[string-ref (-> -String -Nat -Char)]
[substring (cl->*
(-> -String -Nat -String)
(-> -String -Nat -Nat -String))]
[substring (->opt -String -Nat [-Nat] -String)]
[string->path (-> -String -Path)]
[file-exists? (-> -Pathlike B)]
@ -238,8 +227,8 @@
[assf (-poly (a b) ((a . -> . Univ) (-lst (-pair a b))
. -> . (-opt (-pair a b))))]
[list-ref (-poly (a) ((-lst a) -Integer . -> . a))]
[list-tail (-poly (a) ((-lst a) -Integer . -> . (-lst a)))]
[list-ref (-poly (a) ((-lst a) -Nat . -> . a))]
[list-tail (-poly (a) ((-lst a) -Nat . -> . (-lst a)))]
[apply (-poly (a b) (((list) a . ->* . b) (-lst a) . -> . b))]
[kernel:apply (-poly (a b) (((list) a . ->* . b) (-lst a) . -> . b))]
@ -248,7 +237,7 @@
(list (make-arr
(list ((list) (a a) . ->... . b)
(-lst a))
(-values (list (-pair b (-val '())) -Integer -Integer -Integer))))))]
(-values (list (-pair b (-val '())) -Nat -Nat -Nat))))))]
[call/cc (-poly (a b) (((a . -> . (Un)) . -> . b) . -> . (Un a b)))]
[call/ec (-poly (a b) (((a . -> . (Un)) . -> . b) . -> . (Un a b)))]
@ -278,11 +267,9 @@
[pregexp (-String . -> . -PRegexp)]
[byte-regexp (-Bytes . -> . -Byte-Regexp)]
[byte-pregexp (-Bytes . -> . -Byte-PRegexp)]
[regexp-quote (cl-> [(-String) -String]
[(-String -Boolean) -String]
[(-Bytes) -Bytes]
[(-Bytes -Boolean) -Bytes])]
[regexp-quote (cl->*
(-String [-Boolean] . ->opt . -String)
(-Bytes [-Boolean] . ->opt . -Bytes))]
[regexp-match
(let ([?outp (-opt -Output-Port)]
[N -Nat]
@ -291,19 +278,10 @@
[-StrRx (Un -String -Regexp -PRegexp)]
[-BtsRx (Un -Bytes -Byte-Regexp -Byte-PRegexp)]
[-InpBts (Un -Input-Port -Bytes)])
(cl-> [(-StrRx -String ) (optlist -String)]
[(-StrRx -String N ) (optlist -String)]
[(-StrRx -String N ?N ) (optlist -String)]
[(-StrRx -String N ?N ?outp) (optlist -String)]
[(-BtsRx -String ) (optlist -Bytes)]
[(-BtsRx -String N ) (optlist -Bytes)]
[(-BtsRx -String N ?N ) (optlist -Bytes)]
[(-BtsRx -String N ?N ?outp) (optlist -Bytes)]
[(-Pattern -InpBts ) (optlist -Bytes)]
[(-Pattern -InpBts N ) (optlist -Bytes)]
[(-Pattern -InpBts N ?N ) (optlist -Bytes)]
[(-Pattern -InpBts N ?N ?outp) (optlist -Bytes)]))]
(cl->*
(-StrRx -String [N ?N ?outp] . ->opt . (optlist -String))
(-BtsRx -String [N ?N ?outp] . ->opt . (optlist -Bytes))
(-Pattern -InpBts [N ?N ?outp] . ->opt . (optlist -Bytes))))]
[regexp-match*
(let ([N -Nat]
[?N (-opt -Nat)]
@ -354,8 +332,8 @@
[-> -String -String]
[-> -Bytes -Bytes])]
[number->string (cl-> [(N) -String] [(N N) -String])]
[string->number (cl-> [(-String) N] [(-String N) N])]
[number->string (->opt N [N] -String)]
[string->number (->opt -String [N] -String)]
[current-milliseconds (-> -Integer)]
@ -364,7 +342,7 @@
[raise-type-error
(cl->
[(Sym -String Univ) (Un)]
[(Sym -String N (-lst Univ)) (Un)])]
[(Sym -String -Nat (-lst Univ)) (Un)])]
;; this is a hack
@ -376,12 +354,12 @@
[bitwise-not (null -Integer . ->* . -Integer)]
[bitwise-xor (null -Integer . ->* . -Integer)]
[make-string (cl-> [(-Integer) -String] [(-Integer -Char) -String])]
[abs (N . -> . N)]
[substring (cl-> [(-String -Integer) -String]
[(-String -Integer -Integer) -String])]
[string-length (-String . -> . -Integer)]
[string-set! (-String -Integer -Char . -> . -Void)]
[make-string (cl-> [(-Nat) -String] [(-Nat -Char) -String])]
[abs (-Real . -> . -Real)]
[substring (->opt -String [-Nat] -String)]
[string-length (-String . -> . -Nat)]
[unsafe-string-length (-String . -> . -Nat)]
[string-set! (-String -Nat -Char . -> . -Void)]
[file-exists? (-Pathlike . -> . B)]
[string->symbol (-String . -> . Sym)]
@ -391,24 +369,21 @@
;; vectors
[vector? (make-pred-ty (-vec Univ))]
[vector-ref (-poly (a) ((-vec a) N . -> . a))]
[build-vector (-poly (a) (-Integer (-Integer . -> . a) . -> . (-vec a)))]
[vector-ref (-poly (a) ((-vec a) -Nat . -> . a))]
[build-vector (-poly (a) (-Nat (-Nat . -> . a) . -> . (-vec a)))]
[vector-set! (-poly (a) (-> (-vec a) N a -Void))]
[vector-set! (-poly (a) (-> (-vec a) -Nat a -Void))]
[vector->list (-poly (a) (-> (-vec a) (-lst a)))]
[list->vector (-poly (a) (-> (-lst a) (-vec a)))]
[vector-length (-poly (a) ((-vec a) . -> . -Integer))]
[make-vector (-poly (a) (cl-> [(-Integer) (-vec -Integer)]
[(-Integer a) (-vec a)]))]
[vector-length (-poly (a) ((-vec a) . -> . -Nat))]
[make-vector (-poly (a) (cl-> [(-Nat) (-vec -Integer)]
[(-Nat a) (-vec a)]))]
[vector (-poly (a) (->* (list) a (-vec a)))]
[vector-immutable (-poly (a) (->* (list) a (-vec a)))]
[vector->vector-immutable (-poly (a) (-> (-vec a) (-vec a)))]
[vector-fill! (-poly (a) (-> (-vec a) a -Void))]
[vector-copy! (-poly (a)
(cl->* ((-vec a) -Integer (-vec a) . -> . -Void)
((-vec a) -Integer (-vec a) -Integer . -> . -Void)
((-vec a) -Integer (-vec a) -Integer -Integer . -> . -Void)))]
[vector-copy! (-poly (a) ((-vec a) -Nat (-vec a) [-Nat -Nat] . ->opt . -Void))]
;; [vector->values no good type here]
@ -461,51 +436,36 @@
[bytes-ref (-> -Bytes -Integer -Integer)]
[bytes-append (->* (list -Bytes) -Bytes -Bytes)]
[subbytes (cl-> [(-Bytes -Integer) -Bytes] [(-Bytes -Integer -Integer) -Bytes])]
[bytes-length (-> -Bytes -Integer)]
[read-bytes-line (cl-> [() -Bytes]
[(-Input-Port) -Bytes]
[(-Input-Port Sym) -Bytes])]
[bytes-length (-> -Bytes -Nat)]
[unsafe-bytes-length (-> -Bytes -Nat)]
[read-bytes-line (->opt [-Input-Port Sym] -Bytes)]
[open-input-file (->key -Pathlike #:mode (Un (-val 'binary) (-val 'text)) #f -Input-Port)]
[close-input-port (-> -Input-Port -Void)]
[close-output-port (-> -Output-Port -Void)]
[read-line (cl-> [() -String]
[(-Input-Port) -String]
[(-Input-Port Sym) -String])]
[read-line (->opt [-Input-Port Sym] -String)]
[copy-file (-> -Pathlike -Pathlike -Void)]
[bytes->string/utf-8 (-> -Bytes -String)]
[force (-poly (a) (-> (-Promise a) a))]
[bytes<? (->* (list -Bytes) -Bytes B)]
[regexp-replace*
(cl->* (-Pattern (Un -Bytes -String) (Un -Bytes -String) . -> . -Bytes)
(-Pattern -String -String . -> . -String))]
(cl->* (-Pattern -String -String . -> . -String)
(-Pattern (Un -Bytes -String) (Un -Bytes -String) . -> . -Bytes))]
[peek-char
(cl->* [-> (Un -Char (-val eof))]
[-Input-Port . -> . (Un -Char (-val eof))]
[-Input-Port N . -> . (Un -Char (-val eof))])]
(cl->* [->opt [-Input-Port -Nat] (Un -Char (-val eof))])]
[peek-byte
(cl->* [-> (Un -Byte (-val eof))]
[-Input-Port . -> . (Un -Byte (-val eof))]
[-Input-Port N . -> . (Un -Byte (-val eof))])]
(cl->* [->opt [-Input-Port -Nat] (Un -Byte (-val eof))])]
[read-char
(cl->* [-> (Un -Char (-val eof))]
[-Input-Port . -> . (Un -Char (-val eof))])]
(cl->* [->opt [-Input-Port] (Un -Char (-val eof))])]
[read-byte
(cl->* [-> (Un -Byte (-val eof))]
[-Input-Port . -> . (Un -Byte (-val eof))])]
[make-pipe
(cl->* [-> (-values (list -Input-Port -Output-Port))]
[N . -> . (-values (list -Input-Port -Output-Port))])]
(cl->* [->opt [N] (-values (list -Input-Port -Output-Port))])]
[open-output-bytes
(cl->* [-> -Output-Port]
[Univ . -> . -Output-Port])]
[get-output-bytes
(cl->* [-Output-Port . -> . -Bytes]
[-Output-Port Univ . -> . -Bytes]
[-Output-Port Univ N . -> . -Bytes]
[-Output-Port Univ N N . -> . -Bytes]
[-Output-Port N . -> . -Bytes]
[-Output-Port N N . -> . -Bytes])]
(cl->* [[Univ] . ->opt . -Output-Port])]
[get-output-bytes (-Output-Port [Univ N N] . ->opt . -Bytes)]
#;[exn:fail? (-> Univ B)]
#;[exn:fail:read? (-> Univ B)]
@ -519,8 +479,7 @@
(-> (-HT a b) (-> a b c) -Void))]
[delete-file (-> -Pathlike -Void)]
[make-namespace (cl->* (-> -Namespace)
(-> (Un (-val 'empty) (-val 'initial)) -Namespace))]
[make-namespace (->opt [(Un (-val 'empty) (-val 'initial))] -Namespace)]
[make-base-namespace (-> -Namespace)]
[eval (-> -Sexp Univ)]
@ -556,18 +515,9 @@
[prop (-opt S)]
[cert (-opt S)])
(cl->*
(-> ctxt Sym I)
(-> ctxt Pre A)
(-> ctxt Univ S)
(-> ctxt Sym srcloc I)
(-> ctxt Pre srcloc A)
(-> ctxt Univ srcloc S)
(-> ctxt Sym srcloc prop I)
(-> ctxt Pre srcloc prop A)
(-> ctxt Univ srcloc prop S)
(-> ctxt Sym srcloc prop cert I)
(-> ctxt Pre srcloc prop cert A)
(-> ctxt Univ srcloc prop cert S))))]
(->opt ctxt Sym [srcloc prop cert] I)
(->opt ctxt Pre [srcloc prop cert] A)
(->opt ctxt Univ [srcloc prop cert] S))))]
[syntax->datum (cl->* (-> Any-Syntax -Sexp)
(-> (-Syntax Univ) Univ))]
@ -620,14 +570,14 @@
((list a) (b b) . ->... . (-opt c))
(-lst a))
((-lst b) b) . ->... . (-lst c)))]
[take (-poly (a) ((-lst a) -Integer . -> . (-lst a)))]
[drop (-poly (a) ((-lst a) -Integer . -> . (-lst a)))]
[take-right (-poly (a) ((-lst a) -Integer . -> . (-lst a)))]
[drop-right (-poly (a) ((-lst a) -Integer . -> . (-lst a)))]
[take (-poly (a) ((-lst a) -Nat . -> . (-lst a)))]
[drop (-poly (a) ((-lst a) -Nat . -> . (-lst a)))]
[take-right (-poly (a) ((-lst a) -Nat . -> . (-lst a)))]
[drop-right (-poly (a) ((-lst a) -Nat . -> . (-lst a)))]
[split-at
(-poly (a) ((list (-lst a)) -Integer . ->* . (-values (list (-lst a) (-lst a)))))]
(-poly (a) ((list (-lst a)) -Nat . ->* . (-values (list (-lst a) (-lst a)))))]
[split-at-right
(-poly (a) ((list (-lst a)) -Integer . ->* . (-values (list (-lst a) (-lst a)))))]
(-poly (a) ((list (-lst a)) -Nat . ->* . (-values (list (-lst a) (-lst a)))))]
[last (-poly (a) ((-lst a) . -> . a))]
[add-between (-poly (a b) ((-lst a) b . -> . (-lst (Un a b))))]
@ -651,7 +601,9 @@
[tcp-accept (-TCP-Listener . -> . (-values (list -Input-Port -Output-Port)) )]
[tcp-accept/enable-break (-TCP-Listener . -> . (-values (list -Input-Port -Output-Port)) )]
[tcp-accept-ready? (-TCP-Listener . -> . B )]
[tcp-addresses (-Port . -> . (-values (list N N)))]
[tcp-addresses (cl->*
(-Port [(-val #f)] . ->opt . (-values (list -String -String)))
(-Port (-val #t) . -> . (-values (list -String -Nat -String -Nat))))]
[tcp-close (-TCP-Listener . -> . -Void )]
[tcp-connect (-String -Integer . -> . (-values (list -Input-Port -Output-Port)))]
[tcp-connect/enable-break (-String -Integer . -> . (-values (list -Input-Port -Output-Port)))]
@ -672,8 +624,7 @@
[current-continuation-marks (-> -Cont-Mark-Set)]
;; scheme/port
[port->lines (cl->* (-Input-Port . -> . (-lst -String))
(-> (-lst -String)))]
[port->lines (cl->* ([-Input-Port] . ->opt . (-lst -String)))]
[with-output-to-string
(-> (-> Univ) -String)]
[open-output-nowhere (-> -Output-Port)]
@ -683,8 +634,7 @@
[explode-path (-Pathlike . -> . (-lst (Un -Path (-val 'up) (-val 'same))))]
[find-relative-path (-Pathlike -Pathlike . -> . -Path)]
[simple-form-path (-Pathlike . -> . -Path)]
[normalize-path (cl->* (-Pathlike . -> . -Path)
(-Pathlike -Pathlike . -> . -Path))]
[normalize-path (cl->* (-Pathlike [-Pathlike] . ->opt . -Path))]
[filename-extension (-Pathlike . -> . (-opt -Bytes))]
[file-name-from-path (-Pathlike . -> . (-opt -Path))]
[path-only (-Pathlike . -> . -Path)]
@ -699,28 +649,22 @@
(let ([funarg* (-Path (one-of/c 'file 'dir 'link) a . -> . (-values (list a Univ)))]
[funarg (-Path (one-of/c 'file 'dir 'link) a . -> . a)])
(cl->*
(funarg a . -> . a)
(funarg a (-opt -Pathlike) . -> . a)
(funarg a (-opt -Pathlike) Univ . -> . a)
(funarg* a . -> . a)
(funarg* a (-opt -Pathlike) . -> . a)
(funarg* a (-opt -Pathlike) Univ . -> . a))))]
(funarg a [(-opt -Pathlike) Univ]. ->opt . a)
(funarg* a [(-opt -Pathlike) Univ]. ->opt . a))))]
;; scheme/pretty
[pretty-print
(cl->* (Univ . -> . -Void)
(Univ -Output-Port . -> . -Void))]
[pretty-display
(cl->* (Univ . -> . -Void)
(Univ -Output-Port . -> . -Void))]
[pretty-format
(cl->* (Univ . -> . -Void)
(Univ -Integer . -> . -Void))]
[pretty-print (Univ [-Output-Port] . ->opt . -Void)]
[pretty-display (Univ [-Output-Port] . ->opt . -Void)]
[pretty-format (Univ [-Output-Port] . ->opt . -Void)]
;; unsafe
[unsafe-vector-length (-poly (a) ((-vec a) . -> . -Nat))]
[unsafe-car (-poly (a b)
(cl->*
(->acc (list (-pair a b)) a (list -car))))]
[unsafe-cdr (-poly (a b)
(cl->*
(->acc (list (-pair a b)) b (list -cdr))))]
@ -767,3 +711,6 @@
[system* ((list -Pathlike) -String . ->* . -Boolean)]
[system/exit-code (-String . -> . -Integer)]
[system*/exit-code ((list -Pathlike) -String . ->* . -Integer)]
;; mutable pairs

5
collects/typed-scheme/private/base-types-new.ss
View File

@ -1,11 +1,11 @@
#lang s-exp "type-env-lang.ss"
[Number -Number]
[Complex -Number]
[Number -Number]
[Integer -Integer]
[Real -Real]
[Exact-Rational -ExactRational]
[Flonum -Flonum]
[Float -Flonum]
[Exact-Positive-Integer -ExactPositiveInteger]
[Exact-Nonnegative-Integer -ExactNonnegativeInteger]
[Natural -ExactNonnegativeInteger]
@ -41,5 +41,6 @@
[HashTable (-poly (a b) (-HT a b))]
[Promise (-poly (a) (-Promise a))]
[Pair (-poly (a b) (-pair a b))]
[MPair (-poly (a b) (-mpair a b))]
[Boxof (-poly (a) (make-Box a))]
[Continuation-Mark-Set -Cont-Mark-Set]

31
collects/typed-scheme/private/env-lang.ss
View File

@ -4,7 +4,7 @@
(require (for-syntax (utils tc-utils)
(env init-envs)
scheme/base
scheme/base syntax/parse
(r:infer infer)
(only-in (r:infer infer-dummy) infer-param)
(except-in (rep object-rep filter-rep type-rep) make-arr)
@ -12,21 +12,22 @@
(only-in (types convenience) [make-arr* make-arr])))
(define-syntax (#%module-begin stx)
(syntax-case stx (require)
[(mb (require . args) [id ty] ...)
(begin
(unless (andmap identifier? (syntax->list #'(id ...)))
(raise-syntax-error #f "not all ids"))
#'(#%plain-module-begin
(begin
(require . args)
(define-for-syntax e
(parameterize ([infer-param infer])
(make-env [id ty] ...)))
(begin-for-syntax
(initialize-type-env e)))))]
(define-syntax-class clause
#:description "[id type]"
(pattern [id:identifier ty]))
(syntax-parse stx #:literals (require begin)
[(mb (~optional (~and extra (~or (begin . _) (require . args))))
~! :clause ...)
#'(#%plain-module-begin
(begin
extra
(define-for-syntax e
(parameterize ([infer-param infer])
(make-env [id ty] ...)))
(begin-for-syntax
(initialize-type-env e))))]
[(mb . rest)
#'(mb (require) . rest)]))
#'(mb (begin) . rest)]))
(provide #%module-begin
require

5
collects/typed-scheme/rep/type-rep.ss
View File

@ -66,6 +66,11 @@
;; left and right are Types
(dt Pair ([left Type/c] [right Type/c]) [#:key 'pair])
;; *mutable* pairs - distinct from regular pairs
;; left and right are Types
(dt MPair ([left Type/c] [right Type/c]) [#:key 'mpair])
;; elem is a Type
(dt Vector ([elem Type/c])
[#:frees (make-invariant (free-vars* elem)) (make-invariant (free-idxs* elem))]

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

@ -20,6 +20,7 @@
(define -App make-App)
(define -pair make-Pair)
(define -mpair make-MPair)
(define -val make-Value)
(define -Param make-Param)
(define -box make-Box)

6
collects/typed-scheme/utils/tc-utils.ss
View File

@ -58,9 +58,9 @@ don't depend on any other portion of the system
stx))
(define (raise-typecheck-error msg stxs)
(raise (make-exn:fail:syntax (string-append "typecheck: " msg)
(current-continuation-marks)
stxs)))
(if (null? (cdr stxs))
(raise-syntax-error 'typecheck msg (car stxs))
(raise-syntax-error 'typecheck msg #f #f stxs)))
(define delayed-errors null)

4
collects/typed/framework/framework.ss
View File

@ -19,8 +19,8 @@
[last-paragraph (-> Number)]
[delete (Number Number -> Void)]
[auto-wrap (Any -> Void)]
[paragraph-end-position (Number -> Number)]
[paragraph-start-position (Number -> Number)]
[paragraph-end-position (Number -> Natural)]
[paragraph-start-position (Number -> Natural)]
[get-start-position (-> Number)]
[get-end-position (-> Number)]
[insert (String Number Number -> Void)])))

2
collects/typed/mred/mred.ss
View File

@ -23,7 +23,7 @@
()))
(dt Choice% (Class ()
([parent Any] [label String] [choices (Listof Any)] [callback Any])
([get-selection (-> (Option Integer))]
([get-selection (-> (Option Natural))]
[set-selection (Integer -> Any)]
[get-string-selection (-> (Option String))]
[set-string-selection (String -> Void)])))

2
collects/typed/scheme/base.ss
View File

@ -4,7 +4,7 @@
(providing (libs (except scheme/base #%module-begin #%top-interaction with-handlers lambda #%app)
(except typed-scheme/private/prims)
(except typed-scheme/private/base-types)
(except typed-scheme/private/base-types-new)
(except typed-scheme/private/base-types-extra))
(basics #%module-begin
#%top-interaction

2
collects/typed/scheme/base/lang/reader.ss
View File

@ -1,6 +1,6 @@
#lang s-exp syntax/module-reader
typed-scheme
typed/scheme/base
#:read r:read
#:read-syntax r:read-syntax

2
collects/typed/scheme/lang/reader.ss
View File

@ -1,6 +1,6 @@
#lang s-exp syntax/module-reader
typed-scheme
typed/scheme
#:read r:read
#:read-syntax r:read-syntax