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

fix typo

Browse Source 
svn: r17294

original commit: 9b13bbb89cbd55f653a0f2b8c70a19de7c0be3db
This commit is contained in:
Sam Tobin-Hochstadt 2009-12-14 20:00:12 +00:00
commit 53fa4bb8ce
53 changed files with 949 additions and 559 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -1,18 +1,19 @@
#;
(exn-pred exn:fail:contract? #rx".*contract.*\\(-> number\\? number\\?\\).*")
(exn-pred exn:fail:contract? #rx".*violator.*contract.*\\(-> Number Number\\).*f.*")
#lang scheme/load
(module m typed-scheme
(module m typed/scheme
(: f (Number -> Number))
(define (f x) (add1 x))
(provide f))
(define g 17)
(provide f g))
(module n scheme
(module violator scheme
(require 'm)
(f 'foo))
(module o typed-scheme
(require 'n))
(module o typed/scheme
(require 'violator))
(require 'o)

11
collects/tests/typed-scheme/fail/too-many-errors.ss Normal file
View File

@ -0,0 +1,11 @@
#lang typed/scheme
(: f : Number -> Number)
(define (f a b)
(+ a b))
(define: (g [a : Number] [b : Number]) : Number
(+ a b))
(f 1 2)
(g 1 2)

4
collects/tests/typed-scheme/main.ss
View File

@ -46,7 +46,9 @@
(define path (build-path (this-expression-source-directory) dir))
(define tests
(for/list ([p (directory-list path)]
#:when (scheme-file? p))
#:when (scheme-file? p)
;; skip backup files
#:when (not (regexp-match #rx".*~" (path->string p))))
(test-case
(path->string p)
(test

14
collects/tests/typed-scheme/succeed/logic.ss Normal file
View File

@ -0,0 +1,14 @@
#lang typed-scheme
(: f ((U Number #f) (cons Any Any) -> Number))
(define (f x y)
(cond
[(and (number? x) (number? (car y))) (+ x (car y))]
[(number? (car y)) (+ (bool-to-0-or-1 x) (car y))]
[(number? x) x]
[else 0]))
(: bool-to-0-or-1 (Boolean -> Number))
(define (bool-to-0-or-1 b)
(if b 1 0))

6
collects/tests/typed-scheme/succeed/map-nonempty.ss Normal file
View File

@ -0,0 +1,6 @@
#lang typed/scheme
(: x (Pair Number (Listof Number)))
(define x (cons 1 (list 1 2 3 4)))
(apply max (ann (map add1 x) : (Pair Number (Listof Number))))

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

@ -64,7 +64,7 @@
(define: (manual-t-test [avga : number] [avgb : number] [vara : number]
[varb : number] [cta : number] [ctb : number]) : number
(/ (- avga avgb)
(sqrt (+ (/ vara cta) (/ varb ctb)))))
(assert (sqrt (+ (/ vara cta) (/ varb ctb))) number?)))
;; chi-square : (listof [0,1]) (listof [0,1]) -> number
;; chi-square is a simple measure of the extent to which the
@ -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)]

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

@ -41,7 +41,7 @@
(: manual-t-test (Number Number Number Number Number Number -> Number))
(define (manual-t-test avga avgb vara varb cta ctb)
(/ (- avga avgb)
(sqrt (+ (/ vara cta) (/ varb ctb)))))
(assert (sqrt (+ (/ vara cta) (/ varb ctb))) number?)))
(: chi-square ((Listof Number) (Listof Number) -> Number))
;; chi-square is a simple measure of the extent to which the
@ -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))

4
collects/tests/typed-scheme/unit-tests/parse-type-tests.ss
View File

@ -5,8 +5,8 @@
(rep type-rep)
(rename-in (types comparison subtype union utils convenience)
[Un t:Un] [-> t:->])
(private base-types base-types-extra colon)
(for-template (private base-types base-types-extra base-env colon))
(private base-types-new base-types-extra colon)
(for-template (private base-types-new base-types-extra base-env colon))
(private parse-type)
(schemeunit))

2
collects/tests/typed-scheme/unit-tests/subtype-tests.ss
View File

@ -126,7 +126,7 @@
;; polymorphic function types should be subtypes of the function top
[(-poly (a) (a . -> . a)) top-func]
[(cl->* (-Number . -> . -String) (-Boolean . -> . -String)) ((Un -Number -Boolean) . -> . -String)]
[(cl->* (-Number . -> . -String) (-Boolean . -> . -String)) ((Un -Boolean -Number) . -> . -String)]
))
(define-go

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

@ -3,7 +3,10 @@
(require "test-utils.ss" "planet-requires.ss"
(for-syntax scheme/base)
(for-template scheme/base))
(require (private base-env prims type-annotation base-types-extra)
(require (private base-env prims type-annotation
base-types-extra
base-env-numeric
base-env-indexing-old)
(typecheck typechecker)
(rep type-rep filter-rep object-rep)
(rename-in (types utils union convenience)
@ -18,8 +21,11 @@
(require (for-syntax (utils tc-utils)
(typecheck typechecker)
(env type-env)
(private base-env))
(for-template (private base-env base-types base-types-extra)))
(private base-env base-env-numeric
base-env-indexing-old))
(for-template (private base-env base-types-new base-types-extra
base-env-numeric
base-env-indexing-old)))
(require (for-syntax syntax/kerncase syntax/parse))
@ -29,6 +35,9 @@
(define N -Number)
(define B -Boolean)
(define Sym -Symbol)
(define -Pos -ExactPositiveInteger)
(define R -Real)
(define F -Flonum)
(define (g) (run typecheck-tests))
@ -73,9 +82,9 @@
(syntax-case stx ()
[(_ expr ty) (syntax/loc stx (tc-e expr #:ret (ret ty)))]
[(_ expr #:proc p)
(syntax/loc stx
(quasisyntax/loc stx
(let-values ([(t e) (tc-expr/expand/values expr)])
(check-tc-result-equal? (format "~s" 'expr) (t) (p e))))]
#,(syntax/loc stx (check-tc-result-equal? (format "~s" 'expr) (t) (p e)))))]
[(_ expr #:ret r)
(syntax/loc stx
(check-tc-result-equal? (format "~a" 'expr) (tc-expr/expand expr) r))]
@ -127,24 +136,24 @@
(+ 1 (car x))
5))
N]
(tc-e/t (if (let ([y 12]) y) 3 4) -Integer)
(tc-e/t 3 -Integer)
(tc-e/t (if (let ([y 12]) y) 3 4) -Pos)
(tc-e/t 3 -Pos)
(tc-e/t "foo" -String)
(tc-e (+ 3 4) -Integer)
[tc-e/t (lambda: () 3) (t:-> -Integer : (-LFS (list) (list (make-LBot))))]
[tc-e/t (lambda: ([x : Number]) 3) (t:-> N -Integer : (-LFS (list) (list (make-LBot))))]
[tc-e/t (lambda: ([x : Number] [y : Boolean]) 3) (t:-> N B -Integer : (-LFS (list) (list (make-LBot))))]
[tc-e/t (lambda () 3) (t:-> -Integer : (-LFS (list) (list (make-LBot))))]
[tc-e (values 3 4) #:ret (ret (list -Integer -Integer) (list (-FS (list) (list (make-Bot))) (-FS (list) (list (make-Bot)))))]
[tc-e (cons 3 4) (-pair -Integer -Integer)]
[tc-e (cons 3 #{'() : (Listof -Integer)}) (make-Listof -Integer)]
(tc-e (+ 3 4) -Pos)
[tc-e/t (lambda: () 3) (t:-> -Pos : (-LFS (list) (list (make-LBot))))]
[tc-e/t (lambda: ([x : Number]) 3) (t:-> N -Pos : (-LFS (list) (list (make-LBot))))]
[tc-e/t (lambda: ([x : Number] [y : Boolean]) 3) (t:-> N B -Pos : (-LFS (list) (list (make-LBot))))]
[tc-e/t (lambda () 3) (t:-> -Pos : (-LFS (list) (list (make-LBot))))]
[tc-e (values 3 4) #:ret (ret (list -Pos -Pos) (list (-FS (list) (list (make-Bot))) (-FS (list) (list (make-Bot)))))]
[tc-e (cons 3 4) (-pair -Pos -Pos)]
[tc-e (cons 3 (ann '() : (Listof Integer))) (make-Listof -Integer)]
[tc-e (void) -Void]
[tc-e (void 3 4) -Void]
[tc-e (void #t #f '(1 2 3)) -Void]
[tc-e/t #(3 4 5) (make-Vector -Integer)]
[tc-e/t '(2 3 4) (-lst* -Integer -Integer -Integer)]
[tc-e/t '(2 3 #t) (-lst* -Integer -Integer (-val #t))]
[tc-e/t #(2 3 #t) (make-Vector (t:Un -Integer (-val #t)))]
[tc-e/t #(3 4 5) (make-Vector -Pos)]
[tc-e/t '(2 3 4) (-lst* -Pos -Pos -Pos)]
[tc-e/t '(2 3 #t) (-lst* -Pos -Pos (-val #t))]
[tc-e/t #(2 3 #t) (make-Vector (t:Un -Pos (-val #t)))]
[tc-e/t '(#t #f) (-lst* (-val #t) (-val #f))]
[tc-e/t (plambda: (a) ([l : (Listof a)]) (car l))
(make-Poly '(a) (t:-> (make-Listof (-v a)) (-v a)))]
@ -152,13 +161,13 @@
(make-Poly '(a) (t:-> (make-Listof (-v a)) (-v a)))]
[tc-e/t (case-lambda: [([a : Number] [b : Number]) (+ a b)]) (t:-> N N N)]
[tc-e (let: ([x : Number 5]) x) #:proc (get-let-name x 0 (-path -Number #'x))]
[tc-e (let-values ([(x) 4]) (+ x 1)) -Integer]
[tc-e (let-values ([(x) 4]) (+ x 1)) -Pos]
[tc-e (let-values ([(#{x : Number} #{y : Boolean}) (values 3 #t)]) (and (= x 1) (not y)))
#:proc (syntax-parser [(_ ([(_ y) . _]) . _) (ret -Boolean (-FS (list (make-TypeFilter (-val #f) null #'y)) null))])]
[tc-e/t (values 3) -Integer]
[tc-e/t (values 3) -Pos]
[tc-e (values) #:ret (ret null)]
[tc-e (values 3 #f) #:ret (ret (list -Integer (-val #f)) (list (-FS (list) (list (make-Bot))) (-FS (list (make-Bot)) (list))))]
[tc-e (map #{values @ Symbol} '(a b c)) (make-Listof Sym)]
[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)) (-pair Sym (make-Listof Sym))]
[tc-e (letrec: ([fact : (Number -> Number) (lambda: ([n : Number]) (if (zero? n) 1 (* n (fact (- n 1)))))])
(fact 20))
N]
@ -187,8 +196,8 @@
'bc))
N]
[tc-e/t (let: ((x : Number 3)) (if (boolean? x) (not x) #t)) (-val #t)]
[tc-e/t (begin 3) -Integer]
[tc-e/t (begin #f 3) -Integer]
[tc-e/t (begin 3) -Pos]
[tc-e/t (begin #f 3) -Pos]
[tc-e/t (begin #t) (-val #t)]
[tc-e/t (begin0 #t) (-val #t)]
[tc-e/t (begin0 #t 3) (-val #t)]
@ -196,14 +205,14 @@
[tc-e #f #:ret (ret (-val #f) (-FS (list (make-Bot)) null))]
[tc-e/t '#t (-val #t)]
[tc-e '#f #:ret (ret (-val #f) (-FS (list (make-Bot)) null))]
[tc-e/t (if #f 'a 3) -Integer]
[tc-e/t (if #f 'a 3) -Pos]
[tc-e/t (if #f #f #t) (t:Un (-val #t))]
[tc-e (when #f 3) -Void]
[tc-e/t '() (-val '())]
[tc-e/t (let: ([x : (Listof Number) '(1)])
(cond [(pair? x) 1]
[(null? x) 1]))
-Integer]
-Pos]
[tc-e/t (lambda: ([x : Number] . [y : Number *]) (car y)) (->* (list N) N N)]
[tc-e ((lambda: ([x : Number] . [y : Number *]) (car y)) 3) N]
[tc-e ((lambda: ([x : Number] . [y : Number *]) (car y)) 3 4 5) N]
@ -225,8 +234,9 @@
[tc-e/t (let: ([x : Any 3])
(if (list? x)
(begin (car x) 1) 2))
-Integer]
(begin (car x) 1)
2))
-Pos]
[tc-e (let: ([x : (U Number Boolean) 3])
@ -235,7 +245,7 @@
3))
N]
[tc-e (let ([x 1]) x) #:proc (get-let-name x 0 (-path -Integer #'x))]
[tc-e (let ([x 1]) x) #:proc (get-let-name x 0 (-path -Pos #'x))]
[tc-e (let ([x 1]) (boolean? x)) #:ret (ret -Boolean (-FS (list (make-Bot)) null))]
[tc-e (boolean? number?) #:ret (ret -Boolean (-FS (list (make-Bot)) null))]
@ -251,15 +261,15 @@
[tc-err (5 4)]
[tc-err (apply 5 '(2))]
[tc-err (map (lambda: ([x : Any] [y : Any]) 1) '(1))]
[tc-e (map add1 '(1)) (-lst -Integer)]
[tc-e (map add1 '(1)) (-pair -Pos (-lst -Pos))]
[tc-e/t (let ([x 5])
(if (eq? x 1)
12
14))
-Integer]
-Pos]
[tc-e (car (append (list 1 2) (list 3 4))) -Integer]
[tc-e (car (append (list 1 2) (list 3 4))) -Pos]
[tc-e
(let-syntax ([a
@ -269,8 +279,8 @@
(string-append "foo" (a v))))
-String]
[tc-e (apply (plambda: (a) [x : a *] x) '(5)) (-lst -Integer)]
[tc-e (apply append (list '(1 2 3) '(4 5 6))) (-lst -Integer)]
[tc-e (apply (plambda: (a) [x : a *] x) '(5)) (-lst -Pos)]
[tc-e (apply append (list '(1 2 3) '(4 5 6))) (-lst -Pos)]
[tc-err ((case-lambda: [([x : Number]) x]
[([y : Number] [x : Number]) x])
@ -306,9 +316,9 @@
[tc-e (let* ([sym 'squarf]
[x (if (= 1 2) 3 sym)])
x)
#:proc (syntax-parser [(_ _ (_ ([(x) _]) _)) (-path (t:Un (-val 'squarf) -Integer) #'x)])]
#:proc (syntax-parser [(_ _ (_ ([(x) _]) _)) (-path (t:Un (-val 'squarf) -Pos) #'x)])]
[tc-e/t (if #t 1 2) -Integer]
[tc-e/t (if #t 1 2) -Pos]
;; eq? as predicate
@ -333,12 +343,12 @@
[x (if (= 1 2) 3 sym)])
(if (eq? x sym) 3 x))
#:proc (syntax-parser [(_ _ (_ ([(x) _]) _))
(ret -Integer (-FS (list) (list (make-NotTypeFilter (-val 'squarf) null #'x) (make-TypeFilter (-val #f) null #'x))))])]
(ret -Pos (-FS (list) (list (make-NotTypeFilter (-val 'squarf) null #'x) (make-TypeFilter (-val #f) null #'x))))])]
[tc-e (let* ([sym 'squarf]
[x (if (= 1 2) 3 sym)])
(if (eq? sym x) 3 x))
#:proc (syntax-parser [(_ _ (_ ([(x) _]) _))
(ret -Integer (-FS (list) (list (make-NotTypeFilter (-val 'squarf) null #'x) (make-TypeFilter (-val #f) null #'x))))])]
(ret -Pos (-FS (list) (list (make-NotTypeFilter (-val 'squarf) null #'x) (make-TypeFilter (-val #f) null #'x))))])]
;; equal? as predicate for symbols
[tc-e (let: ([x : (Un 'foo Number) 'foo])
(if (equal? x 'foo) 3 x))
@ -351,22 +361,22 @@
[x (if (= 1 2) 3 sym)])
(if (equal? x sym) 3 x))
#:proc (syntax-parser [(_ _ (_ ([(x) _]) _))
(ret -Integer (-FS (list) (list (make-NotTypeFilter (-val 'squarf) null #'x) (make-TypeFilter (-val #f) null #'x))))])]
(ret -Pos (-FS (list) (list (make-NotTypeFilter (-val 'squarf) null #'x) (make-TypeFilter (-val #f) null #'x))))])]
[tc-e (let* ([sym 'squarf]
[x (if (= 1 2) 3 sym)])
(if (equal? sym x) 3 x))
#:proc (syntax-parser [(_ _ (_ ([(x) _]) _))
(ret -Integer (-FS (list) (list (make-NotTypeFilter (-val 'squarf) null #'x) (make-TypeFilter (-val #f) null #'x))))])]
(ret -Pos (-FS (list) (list (make-NotTypeFilter (-val 'squarf) null #'x) (make-TypeFilter (-val #f) null #'x))))])]
[tc-e (let: ([x : (Listof Symbol)'(a b c)])
(cond [(memq 'a x) => car]
[else 'foo]))
Sym]
[tc-e (list 1 2 3) (-lst* -Integer -Integer -Integer)]
[tc-e (list 1 2 3 'a) (-lst* -Integer -Integer -Integer (-val 'a))]
#;
[tc-e `(1 2 ,(+ 3 4)) (-lst* N N N)]
[tc-e (list 1 2 3) (-lst* -Pos -Pos -Pos)]
[tc-e (list 1 2 3 'a) (-lst* -Pos -Pos -Pos (-val 'a))]
[tc-e `(1 2 ,(+ 3 4)) (-lst* -Pos -Pos -Pos)]
[tc-e (let: ([x : Any 1])
(when (and (list? x) (not (null? x)))
@ -385,7 +395,7 @@
'foo))
(t:Un (-val 'foo) (-pair Univ (-lst Univ)))]
[tc-e (cadr (cadr (list 1 (list 1 2 3) 3))) -Integer]
[tc-e (cadr (cadr (list 1 (list 1 2 3) 3))) -Pos]
@ -393,14 +403,28 @@
[tc-e (let: ([x : Any 1]) (and (number? x) (boolean? x)))
#:ret (ret B (-FS (list (make-Bot)) null))]
[tc-e (let: ([x : Any 1]) (and (number? x) x))
#:proc (get-let-name x 0 (ret (t:Un N (-val #f)) (-FS (list (make-TypeFilter N null #'x) (make-NotTypeFilter (-val #f) null #'x)) null)))]
#:proc (get-let-name x 0 (ret (t:Un N (-val #f)) (-FS
(list (make-TypeFilter N null #'x) (make-NotTypeFilter (-val #f) null #'x))
(list (make-ImpFilter
(list (make-NotTypeFilter (-val #f) null #'x))
(list (make-NotTypeFilter N null #'x)))
(make-ImpFilter
(list (make-TypeFilter N null #'x))
(list (make-TypeFilter (-val #f) null #'x)))))))]
[tc-e (let: ([x : Any 1]) (and x (boolean? x)))
#:proc (get-let-name x 0 (ret -Boolean (-FS (list (make-NotTypeFilter (-val #f) null #'x) (make-TypeFilter -Boolean null #'x)) null)))]
#:proc (get-let-name x 0 (ret -Boolean (-FS (list (make-NotTypeFilter (-val #f) null #'x) (make-TypeFilter -Boolean null #'x))
(list
(make-ImpFilter
(list (make-TypeFilter B null #'x))
(list (make-TypeFilter (-val #f) null #'x)))
(make-ImpFilter
(list (make-NotTypeFilter (-val #f) null #'x))
(list (make-NotTypeFilter B null #'x)))))))]
[tc-e/t (let: ([x : Any 3])
(if (and (list? x) (not (null? x)))
(begin (car x) 1) 2))
-Integer]
-Pos]
;; set! tests
[tc-e (let: ([x : Any 3])
@ -457,7 +481,7 @@
[tc-e/t (let* ([z 1]
[p? (lambda: ([x : Any]) (number? z))])
(lambda: ([x : Any]) (if (p? x) 11 12)))
(t:-> Univ -Integer : (-LFS null (list (make-LBot))))]
(t:-> Univ -Pos : (-LFS null (list (make-LBot))))]
[tc-e/t (let* ([z 1]
[p? (lambda: ([x : Any]) (number? z))])
(lambda: ([x : Any]) (if (p? x) x 12)))
@ -469,7 +493,7 @@
[tc-e/t (let* ([z 1]
[p? (lambda: ([x : Any]) (not (number? z)))])
(lambda: ([x : Any]) (if (p? x) x 12)))
(t:-> Univ -Integer : (-LFS null (list (make-LBot))))]
(t:-> Univ -Pos : (-LFS null (list (make-LBot))))]
[tc-e/t (let* ([z 1]
[p? (lambda: ([x : Any]) z)])
(lambda: ([x : Any]) (if (p? x) x 12)))
@ -500,7 +524,7 @@
;; w-c-m
[tc-e/t (with-continuation-mark 'key 'mark
3)
-Integer]
-Pos]
[tc-err (with-continuation-mark (5 4) 1
3)]
[tc-err (with-continuation-mark 1 (5 4)
@ -529,14 +553,14 @@
[tc-err (call-with-values (lambda () (values 2 1))
(lambda: ([x : String] [y : Number]) (+ x y)))]
;; quote-syntax
[tc-e/t #'3 (-Syntax -Integer)]
[tc-e/t #'(1 2 3) (-Syntax (-lst* -Integer -Integer -Integer))]
[tc-e/t #'3 (-Syntax -Pos)]
[tc-e/t #'(1 2 3) (-Syntax (-lst* -Pos -Pos -Pos))]
;; testing some primitives
[tc-e (let ([app apply]
[f (lambda: [x : Number *] 3)])
(app f (list 1 2 3)))
-Integer]
-Pos]
[tc-e ((lambda () (call/cc (lambda: ([k : (Number -> (U))]) (if (read) 5 (k 10))))))
N]
@ -565,7 +589,7 @@
(define y 2)
(define z (+ x y))
(* x z))
-Integer]
-Pos]
[tc-e/t (let ()
(define: (f [x : Number]) : Number
@ -574,7 +598,7 @@
(+ z w)))
(g 4))
5)
-Integer]
-Pos]
[tc-err (let ()
(define x x)
@ -605,11 +629,11 @@
[tc-e/t (if #f 1 'foo) (-val 'foo)]
[tc-e (list* 1 2 3) (-pair -Integer (-pair -Integer -Integer))]
[tc-e (list* 1 2 3) (-pair -Pos (-pair -Pos -Pos))]
[tc-err (apply append (list 1) (list 2) (list 3) (list (list 1) "foo"))]
[tc-e (apply append (list 1) (list 2) (list 3) (list (list 1) (list 1))) (-lst -Integer)]
[tc-e (apply append (list 1) (list 2) (list 3) (list (list 1) (list "foo"))) (-lst (t:Un -String -Integer))]
[tc-e (apply append (list 1) (list 2) (list 3) (list (list 1) (list 1))) (-lst -Pos)]
[tc-e (apply append (list 1) (list 2) (list 3) (list (list 1) (list "foo"))) (-lst (t:Un -String -Pos))]
[tc-err (plambda: (b ...) [y : b ... b] (apply append (map list y)))]
[tc-e/t (plambda: (b ...) [y : (Listof Integer) ... b] (apply append y))
(-polydots (b) (->... (list) ((-lst -Integer) b) (-lst -Integer)))]
@ -636,15 +660,17 @@
;; instantiating dotted terms
[tc-e/t (inst (plambda: (a ...) [xs : a ... a] 3) Integer Boolean Integer)
(-Integer B -Integer . t:-> . -Integer : (-LFS null (list (make-LBot))))]
(-Integer B -Integer . t:-> . -Pos : (-LFS null (list (make-LBot))))]
[tc-e/t (inst (plambda: (a ...) [xs : (a ... a -> Integer) ... a] 3) Integer Boolean Integer)
((-Integer B -Integer . t:-> . -Integer)
(-Integer B -Integer . t:-> . -Integer)
(-Integer B -Integer . t:-> . -Integer)
. t:-> . -Integer : (-LFS null (list (make-LBot))))]
. t:-> . -Pos : (-LFS null (list (make-LBot))))]
[tc-e/t (plambda: (z x y ...) () (inst map z x y ... y))
(-polydots (z x y) (t:-> ((list ((list x) (y y) . ->... . z) (-lst x)) ((-lst y) y) . ->... . (-lst z))))]
(-polydots (z x y) (t:-> (cl->*
((t:-> x z) (-pair x (-lst x)) . t:-> . (-pair z (-lst z)))
((list ((list x) (y y) . ->... . z) (-lst x)) ((-lst y) y) . ->... . (-lst z)))))]
;; error tests
[tc-err (#%variable-reference number?)]
@ -724,7 +750,7 @@
[tc-e/t (ann (lambda (x) x) (All (a) (a -> a)))
(-poly (a) (a . t:-> . a))]
[tc-e (apply values (list 1 2 3)) #:ret (ret (list -Integer -Integer -Integer))]
[tc-e (apply values (list 1 2 3)) #:ret (ret (list -Pos -Pos -Pos))]
[tc-e/t (ann (if #t 3 "foo") Integer) -Integer]
@ -749,10 +775,10 @@
)
(test-suite
"tc-literal tests"
(tc-l 5 -Integer)
(tc-l 5# N)
(tc-l 5.0 N)
(tc-l 5.1 N)
(tc-l 5 -ExactPositiveInteger)
(tc-l 5# -Flonum)
(tc-l 5.0 -Flonum)
(tc-l 5.1 -Flonum)
(tc-l #t (-val #t))
(tc-l "foo" -String)
(tc-l foo (-val 'foo))

5
collects/typed-scheme/env/lexical-env.ss vendored
View File

@ -4,14 +4,15 @@
"type-environments.ss"
"type-env.ss"
unstable/mutated-vars
(only-in scheme/contract ->* ->)
(only-in scheme/contract ->* -> or/c any/c)
(utils tc-utils)
(only-in (rep type-rep) Type/c)
(typecheck tc-metafunctions)
(except-in (types utils convenience) -> ->*))
(provide lexical-env with-lexical-env with-lexical-env/extend with-update-type/lexical)
(p/c
[lookup-type/lexical ((identifier?) (env?) . ->* . Type/c)]
[lookup-type/lexical ((identifier?) (env? #:fail (or/c #f (-> any/c #f))) . ->* . (or/c Type/c #f))]
[update-type/lexical (((identifier? Type/c . -> . Type/c) identifier?) (env?) . ->* . env?)])
;; the current lexical environment

3
collects/typed-scheme/env/type-env.ss vendored
View File

@ -22,7 +22,8 @@
;; add a single type to the mapping
;; identifier type -> void
(define (register-type id type)
;(printf "register-type ~a~n" (syntax-e id))
#;(when (eq? (syntax-e id) 'vector-ref)
(printf "register-type ~a~n" id))
(module-identifier-mapping-put! the-mapping id type))
;; add a single type to the mapping

35
collects/typed-scheme/env/type-environments.ss vendored
View File

@ -2,8 +2,9 @@
(require scheme/contract
(prefix-in r: "../utils/utils.ss")
scheme/match
(except-in (r:utils tc-utils) make-env))
scheme/match (r:rep filter-rep rep-utils) unstable/struct
(except-in (r:utils tc-utils) make-env)
(r:typecheck tc-metafunctions))
(provide current-tvars
extend
@ -17,10 +18,13 @@
env-filter
env-vals
env-keys+vals
env-props
replace-props
with-dotted-env/extend)
;; eq? has the type of equal?, and l is an alist (with conses!)
(r:d-s/c env ([eq? (any/c any/c . -> . boolean?)] [l (listof pair?)]) #:transparent)
;; props is a list of known propositions
(r:d-s/c env ([eq? (any/c any/c . -> . boolean?)] [l (listof pair?)] [props (listof Filter/c)]) #:transparent)
(define (env-vals e)
(map cdr (env-l e)))
@ -30,39 +34,44 @@
(define (env-filter f e)
(match e
[(struct env (eq? l))
(make-env eq? (filter f l))]))
[(struct env (eq? l props))
(make-env eq? (filter f l) props)]))
(define (make-empty-env p?) (make env p? null null))
;; the initial type variable environment - empty
;; this is used in the parsing of types
(define initial-tvar-env (make-env eq? '()))
(define initial-tvar-env (make-empty-env eq?))
;; a parameter for the current type variables
(define current-tvars (make-parameter initial-tvar-env))
(define (make-empty-env p?) (make-env p? '()))
;; the environment for types of ... variables
(define dotted-env (make-parameter (make-empty-env free-identifier=?)))
(define/contract (env-map f env)
(define/contract (env-map f e)
((pair? . -> . pair?) env? . -> . env?)
(make-env (env-eq? env) (map f (env-l env))))
(make env (env-eq? e) (map f (env-l e)) (env-props e)))
;; extend that works on single arguments
(define (extend e k v)
(match e
[(struct env (f l)) (make-env f (cons (cons k v) l))]
[(struct env (f l p)) (make env f (cons (cons k v) l) p)]
[_ (int-err "extend: expected environment, got ~a" e)]))
(define (extend-env ks vs e)
(match e
[(struct env (f l)) (make-env f (append (map cons ks vs) l))]
[(struct env (f l p)) (make env f (append (map cons ks vs) l) p)]
[_ (int-err "extend-env: expected environment, got ~a" e)]))
(define (replace-props e props)
(match e
[(struct env (f l p))
(make env f l props)]))
(define (lookup e key fail)
(match e
[(struct env (f? l))
[(struct env (f? l p))
(let loop ([l l])
(cond [(null? l) (fail key)]
[(f? (caar l) key) (cdar l)]

13
collects/typed-scheme/main.ss
View File

@ -2,7 +2,7 @@
(providing (libs (except scheme/base #%module-begin #%top-interaction with-handlers lambda #%app)
(providing (libs (except scheme/base #%module-begin #%top-interaction with-handlers number? lambda #%app)
(except "private/prims.ss")
(except "private/base-types.ss")
(except "private/base-types-extra.ss"))
@ -10,7 +10,12 @@
#%top-interaction
lambda
#%app))
(require "private/base-env.ss" "private/base-special-env.ss"
(require "private/base-env.ss"
"private/base-special-env.ss"
"private/base-env-numeric.ss"
"private/base-env-indexing-old.ss"
"private/extra-procs.ss"
(for-syntax "private/base-types-extra.ss"))
(provide (rename-out [with-handlers: with-handlers])
(for-syntax (all-from-out "private/base-types-extra.ss")))
(provide (rename-out [with-handlers: with-handlers] [real? number?])
(for-syntax (all-from-out "private/base-types-extra.ss"))
assert)

4
collects/typed-scheme/minimal.ss
View File

@ -1,9 +1,9 @@
#lang scheme/base
(provide #%module-begin provide require rename-in rename-out prefix-in only-in all-from-out except-out except-in
providing begin)
providing begin subtract-in)
(require (for-syntax scheme/base))
(require (for-syntax scheme/base) scheme/require)
(define-for-syntax ts-mod 'typed-scheme/typed-scheme)

113
collects/typed-scheme/private/base-env-indexing-abs.ss Normal file
View File

@ -0,0 +1,113 @@
#lang scheme
(require
"../utils/utils.ss"
scheme/tcp
scheme/unsafe/ops
(only-in rnrs/lists-6 fold-left)
'#%paramz
"extra-procs.ss"
(utils tc-utils )
(types union convenience)
(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-template scheme)
(rename-in (types abbrev) [-Number N] [-Boolean B] [-Symbol Sym] [-Nat -Nat*]))
(provide indexing)
(define-syntax-rule (indexing -Nat)
(make-env
[build-list (-poly (a) (-Nat (-Nat* . -> . a) . -> . (-lst a)))]
[string-ref (-> -String -Nat -Char)]
[substring (->opt -String -Nat [-Nat] -String)]
[make-string (cl-> [(-Nat) -String] [(-Nat -Char) -String])]
[string-set! (-String -Nat -Char . -> . -Void)]
[list-ref (-poly (a) ((-lst a) -Nat . -> . a))]
[list-tail (-poly (a) ((-lst a) -Nat . -> . (-lst a)))]
[regexp-match
(let ([?outp (-opt -Output-Port)]
[N -Nat]
[?N (-opt -Nat)]
[optlist (lambda (t) (-opt (-lst (-opt t))))]
[-StrRx (Un -String -Regexp -PRegexp)]
[-BtsRx (Un -Bytes -Byte-Regexp -Byte-PRegexp)]
[-InpBts (Un -Input-Port -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)]
[-StrRx (Un -String -Regexp -PRegexp)]
[-BtsRx (Un -Bytes -Byte-Regexp -Byte-PRegexp)]
[-InpBts (Un -Input-Port -Bytes)])
(cl->*
(-StrRx -String [N ?N] . ->opt . (-lst -String))
(-BtsRx -String [N ?N] . ->opt . (-lst -Bytes))
(-Pattern -InpBts [N ?N] . ->opt . (-lst -Bytes))))]
[regexp-try-match
(let ([?outp (-opt -Output-Port)]
[?N (-opt -Nat)]
[optlist (lambda (t) (-opt (-lst (-opt t))))])
(->opt -Pattern -Input-Port [-Nat ?N ?outp] (optlist -Bytes)))]
[regexp-match-positions
(let ([?outp (-opt -Output-Port)]
[N -Nat]
[?N (-opt -Nat)]
[optlist (lambda (t) (-opt (-lst (-opt t))))]
[-StrRx (Un -String -Regexp -PRegexp)]
[-BtsRx (Un -Bytes -Byte-Regexp -Byte-PRegexp)]
[-InpBts (Un -Input-Port -Bytes)])
(->opt -Pattern (Un -String -InpBts) [N ?N ?outp] (optlist (-pair -Nat -Nat))))]
[regexp-match-positions*
(let ([?outp (-opt -Output-Port)]
[?N (-opt -Nat)]
[optlist (lambda (t) (-opt (-lst (-opt t))))]
[-StrRx (Un -String -Regexp -PRegexp)]
[-BtsRx (Un -Bytes -Byte-Regexp -Byte-PRegexp)]
[-InpBts (Un -Input-Port -Bytes)])
(->opt -Pattern (Un -String -InpBts) [-Nat ?N ?outp] (-lst (-pair -Nat -Nat))))]
[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)) -Nat . ->* . (-values (list (-lst a) (-lst a)))))]
[split-at-right
(-poly (a) ((list (-lst a)) -Nat . ->* . (-values (list (-lst a) (-lst a)))))]
[vector-ref (-poly (a) ((-vec a) -Nat . -> . a))]
[build-vector (-poly (a) (-Nat (-Nat . -> . a) . -> . (-vec a)))]
[vector-set! (-poly (a) (-> (-vec a) -Nat a -Void))]
[vector-copy! (-poly (a) ((-vec a) -Nat (-vec a) [-Nat -Nat] . ->opt . -Void))]
[make-vector (-poly (a) (cl-> [(-Nat) (-vec -Integer)]
[(-Nat a) (-vec a)]))]
[peek-char
(cl->* [->opt [-Input-Port -Nat] (Un -Char (-val eof))])]
[peek-byte
(cl->* [->opt [-Input-Port -Nat] (Un -Byte (-val eof))])]
;; string.ss
[real->decimal-string (N [-Nat] . ->opt . -String)]
[random (cl-> [(-Nat) -Nat*] [() -Real])]
[raise-type-error
(cl->
[(Sym -String Univ) (Un)]
[(Sym -String -Nat (-lst Univ)) (Un)])]
))

11
collects/typed-scheme/private/base-env-indexing.ss Normal file
View File

@ -0,0 +1,11 @@
#lang scheme
(require
(rename-in "../utils/utils.ss" [infer r:infer])
(for-syntax (types abbrev) (env init-envs) (r:infer infer-dummy infer)
"base-env-indexing-abs.ss"))
(define-for-syntax e (parameterize ([infer-param infer]) (indexing -Nat)))
(begin-for-syntax (initialize-type-env e))

156
collects/typed-scheme/private/base-env-numeric.ss Normal file
View File

@ -0,0 +1,156 @@
#lang s-exp "env-lang.ss"
(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))
(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)]
[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)))]
[/ (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 -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->*
(-Real . -> . -Flonum)
(N . -> . N))]
[inexact->exact (cl->*
(-Real . -> . -ExactRational)
(N . -> . N))]
[floor (-> N N)]
[ceiling (-> N N)]
[truncate (-> N N)]
[make-rectangular (N N . -> . N)]
[make-polar (N N . -> . N)]
[real-part (N . -> . N)]
[imag-part (N . -> . N)]
[magnitude (N . -> . N)]
[angle (N . -> . N)]
[numerator (N . -> . -Integer)]
[denominator (N . -> . -Integer)]
[rationalize (N N . -> . N)]
[expt (cl->* (-Integer -Integer . -> . -Integer) (N N . -> . N))]
[sqrt (cl->*
(-Nat . -> . -Real)
(N . -> . N))]
[log (cl->*
(-Pos . -> . -Real)
(N . -> . N))]
[exp (N . -> . N)]
[cos (N . -> . N)]
[sin (N . -> . N)]
[tan (N . -> . N)]
[acos (N . -> . N)]
[asin (N . -> . N)]
[atan (N . -> . N)]
[gcd (null -Integer . ->* . -Integer)]
[lcm (null -Integer . ->* . -Integer)]
[round (N . -> . -Integer)]
;; scheme/math
[sgn (-Real . -> . -Real)]
[pi N]
[sqr (cl->* (-> -Pos -Pos)
(-> -Nat -Nat)
(-> -Integer -Integer)
(-> -ExactRational -ExactRational)
(-> -Flonum -Flonum)
(-> -Real -Real)
(-> N N))]
[sgn (N . -> . N)]
[conjugate (N . -> . N)]
[sinh (N . -> . N)]
[cosh (N . -> . N)]
[tanh (N . -> . N)]
;; 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]

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

@ -8,7 +8,7 @@
'#%paramz
"extra-procs.ss"
(only-in '#%kernel [apply kernel:apply])
scheme/promise
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])))
@ -55,22 +55,16 @@
[null? (make-pred-ty (-val null))]
[eof-object? (make-pred-ty (-val eof))]
[null (-val null)]
[number? (make-pred-ty N)]
[char? (make-pred-ty -Char)]
[integer? (Univ . -> . B : (-LFS (list (-filter N)) (list (-not-filter -Integer))))]
[exact-integer? (make-pred-ty -Integer)]
[boolean? (make-pred-ty B)]
[add1 (cl->* (-> -Integer -Integer)
(-> N N))]
[sub1 (cl->* (-> -Integer -Integer)
(-> N N))]
[eq? (-> Univ Univ B)]
[eqv? (-> Univ Univ B)]
[equal? (-> Univ Univ B)]
[even? (-> N B)]
[assert (-poly (a) (-> (Un a (-val #f)) a))]
[gensym (cl-> [(Sym) Sym]
[() Sym])]
[assert (-poly (a b) (cl->*
(Univ (make-pred-ty (list a) Univ b) . -> . b)
(-> (Un a (-val #f)) a)))]
[gensym (->opt [Sym] Sym)]
[string-append (->* null -String -String)]
[open-input-string (-> -String -Input-Port)]
[open-output-file
@ -81,15 +75,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))]
@ -99,15 +90,24 @@
[pair? (make-pred-ty (-pair Univ Univ)) #;(-poly (a b) (make-pred-ty (-pair a b)))]
[empty? (make-pred-ty (-val null))]
[empty (-val null)]
[string? (make-pred-ty -String)]
[string (->* '() -Char -String)]
[string-length (-String . -> . -Nat)]
[unsafe-string-length (-String . -> . -Nat)]
[symbol? (make-pred-ty Sym)]
[keyword? (make-pred-ty -Keyword)]
[list? (make-pred-ty (-lst Univ))]
[list (-poly (a) (->* '() a (-lst a)))]
[procedure? (make-pred-ty top-func)]
[map (-polydots (c a b) ((list ((list a) (b b) . ->... . c) (-lst a))
((-lst b) b) . ->... .(-lst c)))]
[map (-polydots (c a b)
(cl->*
(-> (-> a c) (-pair a (-lst a)) (-pair c (-lst c)))
((list
((list a) (b b) . ->... . c)
(-lst a))
((-lst b) b) . ->... .(-lst c))))]
[for-each (-polydots (c a b) ((list ((list a) (b b) . ->... . Univ) (-lst a))
((-lst b) b) . ->... . -Void))]
[fold-left (-polydots (c a b) ((list ((list c a) (b b) . ->... . c) c (-lst a))
@ -134,12 +134,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
@ -147,16 +144,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)]
@ -167,24 +162,9 @@
[sleep (N . -> . -Void)]
[= (->* (list N N) N B)]
[>= (->* (list N N) N B)]
[< (->* (list N N) N B)]
[<= (->* (list N N) N B)]
[> (->* (list N N) N B)]
[zero? (N . -> . B)]
[* (cl->* (->* '() -Integer -Integer) (->* '() N N))]
[/ (cl->* (->* (list N) N N))]
[+ (cl->* (->* '() -Integer -Integer) (->* '() N N))]
[- (cl->* (->* (list -Integer) -Integer -Integer) (->* (list N) N N))]
[max (cl->* (->* (list -Integer) -Integer -Integer)
(->* (list N) N N))]
[min (cl->* (->* (list -Integer) -Integer -Integer)
(->* (list N) N N))]
[build-list (-poly (a) (-Integer (-Integer . -> . 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))))]
@ -229,10 +209,6 @@
[string-copy (-> -String -String)]
[string->immutable-string (-> -String -String)]
[string-ref (-> -String N -Char)]
[substring (cl->*
(-> -String N -String)
(-> -String N N -String))]
[string->path (-> -String -Path)]
[file-exists? (-> -Pathlike B)]
@ -248,7 +224,6 @@
#:mode (one-of/c 'binary 'text) #f
a))]
[random (cl-> [(-Integer) -Integer] [() N])]
[assq (-poly (a b) (a (-lst (-pair a b)) . -> . (-opt (-pair a b))))]
[assv (-poly (a b) (a (-lst (-pair a b)) . -> . (-opt (-pair a b))))]
@ -256,13 +231,6 @@
[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)))]
[positive? (-> N B)]
[negative? (-> N B)]
[odd? (-> -Integer B)]
[even? (-> -Integer B)]
[apply (-poly (a b) (((list) a . ->* . b) (-lst a) . -> . b))]
[kernel:apply (-poly (a b) (((list) a . ->* . b) (-lst a) . -> . b))]
[time-apply (-polydots (b a)
@ -270,7 +238,7 @@
(list (make-arr
(list ((list) (a a) . ->... . b)
(-lst a))
(-values (list (-pair b (-val '())) N N N))))))]
(-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,12 +246,6 @@
[call-with-escape-continuation (-poly (a b) (((a . -> . (Un)) . -> . b) . -> . (Un a b)))]
[struct->vector (Univ . -> . (-vec Univ))]
[quotient (-Integer -Integer . -> . -Integer)]
[remainder (-Integer -Integer . -> . -Integer)]
[quotient/remainder
(make-Function (list (make-arr (list -Integer -Integer) (-values (list -Integer -Integer)))))]
;; parameter stuff
[parameterization-key Sym]
@ -306,66 +268,14 @@
[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-match
(let ([?outp (-opt -Output-Port)]
[?N (-opt N)]
[optlist (lambda (t) (-opt (-lst (-opt t))))]
[-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)]))]
[regexp-match*
(let ([?N (-opt N)]
[-StrRx (Un -String -Regexp -PRegexp)]
[-BtsRx (Un -Bytes -Byte-Regexp -Byte-PRegexp)]
[-InpBts (Un -Input-Port -Bytes)])
(cl->*
(-StrRx -String [N ?N] . ->opt . (-lst -String))
(-BtsRx -String [N ?N] . ->opt . (-lst -Bytes))
(-Pattern -InpBts [N ?N] . ->opt . (-lst -Bytes))))]
[regexp-try-match
(let ([?outp (-opt -Output-Port)]
[?N (-opt N)]
[optlist (lambda (t) (-opt (-lst (-opt t))))])
(->opt -Pattern -Input-Port [N ?N ?outp] (optlist -Bytes)))]
[regexp-quote (cl->*
(-String [-Boolean] . ->opt . -String)
(-Bytes [-Boolean] . ->opt . -Bytes))]
[regexp-match-exact?
(-Pattern (Un -String -Bytes -Input-Port) . -> . B)]
[regexp-match-positions
(let ([?outp (-opt -Output-Port)]
[?N (-opt N)]
[optlist (lambda (t) (-opt (-lst (-opt t))))]
[-StrRx (Un -String -Regexp -PRegexp)]
[-BtsRx (Un -Bytes -Byte-Regexp -Byte-PRegexp)]
[-InpBts (Un -Input-Port -Bytes)])
(->opt -Pattern (Un -String -InpBts) [N ?N ?outp] (optlist (-pair -Nat -Nat))))]
[regexp-match-positions*
(let ([?outp (-opt -Output-Port)]
[?N (-opt N)]
[optlist (lambda (t) (-opt (-lst (-opt t))))]
[-StrRx (Un -String -Regexp -PRegexp)]
[-BtsRx (Un -Bytes -Byte-Regexp -Byte-PRegexp)]
[-InpBts (Un -Input-Port -Bytes)])
(->opt -Pattern (Un -String -InpBts) [N ?N ?outp] (-lst (-pair -Nat -Nat))))]
#;
[regexp-match-peek-positions*]
#;
@ -379,54 +289,16 @@
[-> -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)]
[modulo (cl->* (-Integer -Integer . -> . -Integer))]
;; errors
[raise-type-error
(cl->
[(Sym -String Univ) (Un)]
[(Sym -String N (-lst Univ)) (Un)])]
;; this is a hack
[match:error ((list) Univ . ->* . (Un))]
[exact? (N . -> . B)]
[inexact? (N . -> . B)]
[exact->inexact (N . -> . N)]
[inexact->exact (N . -> . N)]
[real? (Univ . -> . B : (-LFS (list (-filter N)) (list)))]
[complex? (Univ . -> . B : (-LFS (list (-filter N)) (list)))]
[rational? (Univ . -> . B : (-LFS (list (-filter N)) (list)))]
[floor (-> N N)]
[ceiling (-> N N)]
[truncate (-> N N)]
[make-rectangular (N N . -> . N)]
[make-polar (N N . -> . N)]
[real-part (N . -> . N)]
[imag-part (N . -> . N)]
[magnitude (N . -> . N)]
[angle (N . -> . N)]
[numerator (N . -> . -Integer)]
[denominator (N . -> . -Integer)]
[rationalize (N N . -> . N)]
[expt (cl->* (-Integer -Integer . -> . -Integer) (N N . -> . N))]
[sqrt (N . -> . N)]
[log (N . -> . N)]
[exp (N . -> . N)]
[cos (N . -> . N)]
[sin (N . -> . N)]
[tan (N . -> . N)]
[acos (N . -> . N)]
[asin (N . -> . N)]
[atan (N . -> . N)]
[gcd (null -Integer . ->* . -Integer)]
[lcm (null -Integer . ->* . -Integer)]
[arithmetic-shift (-Integer -Integer . -> . -Integer)]
[bitwise-and (null -Integer . ->* . -Integer)]
@ -434,12 +306,7 @@
[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)]
[abs (-Real . -> . -Real)]
[file-exists? (-Pathlike . -> . B)]
[string->symbol (-String . -> . Sym)]
@ -449,24 +316,14 @@
;; 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-set! (-poly (a) (-> (-vec a) N 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))]
[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->values no good type here]
@ -480,7 +337,6 @@
[current-output-port (-Param -Output-Port -Output-Port)]
[current-error-port (-Param -Output-Port -Output-Port)]
[current-input-port (-Param -Input-Port -Input-Port)]
[round (N . -> . -Integer)]
[seconds->date (-Integer . -> . (make-Name #'date))]
[current-seconds (-> -Integer)]
[current-print (-Param (Univ . -> . Univ) (Univ . -> . Univ))]
@ -520,51 +376,32 @@
[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))]
[peek-char
(cl->* [-> (Un -Char (-val eof))]
[-Input-Port . -> . (Un -Char (-val eof))]
[-Input-Port N . -> . (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->* (-Pattern -String -String . -> . -String)
(-Pattern (Un -Bytes -String) (Un -Bytes -String) . -> . -Bytes))]
[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)]
@ -578,8 +415,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)]
@ -615,18 +451,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))]
@ -679,14 +506,6 @@
((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)))]
[split-at
(-poly (a) ((list (-lst a)) -Integer . ->* . (-values (list (-lst a) (-lst a)))))]
[split-at-right
(-poly (a) ((list (-lst a)) -Integer . ->* . (-values (list (-lst a) (-lst a)))))]
[last (-poly (a) ((-lst a) . -> . a))]
[add-between (-poly (a b) ((-lst a) b . -> . (-lst (Un a b))))]
@ -710,7 +529,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)))]
@ -725,14 +546,11 @@
[generate-temporaries ((Un (-Syntax Univ) (-lst Univ)) . -> . (-lst (-Syntax Sym)))]
[check-duplicate-identifier ((-lst (-Syntax Sym)) . -> . (-opt (-Syntax Sym)))]
;; string.ss
[real->decimal-string (N [-Nat] . ->opt . -String)]
[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)]
@ -742,8 +560,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)]
@ -758,38 +575,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/math
[sgn (-Real . -> . -Real)]
[pi N]
[sqr (N . -> . N)]
[sgn (N . -> . N)]
[conjugate (N . -> . N)]
[sinh (N . -> . N)]
[cosh (N . -> . N)]
[tanh (N . -> . N)]
;; 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))))]
@ -830,3 +631,12 @@
[vector-split-at-right
(-poly (a) ((list (-vec a)) -Integer . ->* . (-values (list (-vec a) (-vec a)))))]
;; scheme/system
[system (-String . -> . -Boolean)]
[system* ((list -Pathlike) -String . ->* . -Boolean)]
[system/exit-code (-String . -> . -Integer)]
[system*/exit-code ((list -Pathlike) -String . ->* . -Integer)]
;; mutable pairs

46
collects/typed-scheme/private/base-types-new.ss Normal file
View File

@ -0,0 +1,46 @@
#lang s-exp "type-env-lang.ss"
[Complex -Number]
[Number -Number]
[Integer -Integer]
[Real -Real]
[Exact-Rational -ExactRational]
[Float -Flonum]
[Exact-Positive-Integer -ExactPositiveInteger]
[Exact-Nonnegative-Integer -ExactNonnegativeInteger]
[Natural -ExactNonnegativeInteger]
[Void -Void]
[Boolean -Boolean]
[Symbol -Symbol]
[String -String]
[Any Univ]
[Port -Port]
[Path -Path]
[Path-String -Pathlike]
[Regexp -Regexp]
[PRegexp -PRegexp]
[Char -Char]
[Namespace -Namespace]
[Input-Port -Input-Port]
[Output-Port -Output-Port]
[Bytes -Bytes]
[EOF (-val eof)]
[Sexpof (-poly (a) (-Sexpof a))] ;; recursive union of sexps with a
[Syntaxof (-poly (a) (-Syntax a))] ;; syntax-e yields a
[Syntax-E In-Syntax] ;; possible results of syntax-e on "2D" syntax
[Syntax Any-Syntax] ;; (Syntaxof Syntax-E): "2D" syntax
[Datum Syntax-Sexp] ;; (Sexpof Syntax), datum->syntax yields "2D" syntax
[Sexp -Sexp] ;; (Sexpof (U)), syntax->datum of "2D" syntax
[Identifier Ident]
[Procedure top-func]
[Keyword -Keyword]
[Listof -Listof]
[Vectorof (-poly (a) (make-Vector a))]
[Option (-poly (a) (-opt a))]
[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]

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

@ -1,7 +1,15 @@
#lang s-exp "type-env-lang.ss"
[Number -Number]
[Number -Real]
[Real -Real]
[Complex -Number]
[Integer -Integer]
[Exact-Rational -ExactRational]
[Flonum -Flonum]
[Exact-Positive-Integer -ExactPositiveInteger]
[Exact-Nonnegative-Integer -ExactNonnegativeInteger]
[Natural -ExactNonnegativeInteger]
[Void -Void]
[Boolean -Boolean]
[Symbol -Symbol]

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

@ -4,33 +4,34 @@
(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)
(types convenience union)
(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 (-#%module-begin stx)
(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
(provide (rename-out [-#%module-begin #%module-begin])
require
(all-from-out scheme/base)
(except-out (all-from-out scheme/base) #%module-begin)
types rep private utils
(for-syntax
(types-out convenience union)

15
collects/typed-scheme/private/extra-procs.ss
View File

@ -1,17 +1,8 @@
#lang scheme/base
(provide assert)
(define (assert v)
(unless v
(error "Assertion failed - value was #f"))
(define (assert v [pred values])
(unless (pred v)
(error "Assertion failed"))
v)
#;
(define (fold-right f c as . bss)
(if (or (null? as)
(ormap null? bss))
c
(apply f
(apply fold-right f c (cdr as) (map cdr bss))
(car as) (map car bss))))

24
collects/typed-scheme/private/prims.ss
View File

@ -307,19 +307,29 @@ This file defines two sorts of primitives. All of them are provided into any mod
#t))]))
(define-syntax (define-typed-struct stx)
(syntax-case stx (:)
[(_ nm ([fld : ty] ...) . opts)
(define-syntax-class fld-spec
#:literals (:)
#:description "[field-name : type]"
(pattern [fld:id : ty]))
(define-syntax-class struct-name
#:description "struct name (with optional super-struct name)"
#:attributes (name super)
(pattern (name:id super:id))
(pattern name:id
#:with super #f))
(syntax-parse stx
[(_ nm:struct-name (fs:fld-spec ...) . opts)
(let ([mutable (if (memq '#:mutable (syntax->datum #'opts))
'(#:mutable)
'())])
(with-syntax ([d-s (syntax-property (syntax/loc stx (define-struct nm (fld ...) . opts))
(with-syntax ([d-s (syntax-property (syntax/loc stx (define-struct nm (fs.fld ...) . opts))
'typechecker:ignore #t)]
[dtsi (internal (quasisyntax/loc stx (define-typed-struct-internal nm ([fld : ty] ...) #,@mutable)))])
[dtsi (internal (quasisyntax/loc stx (define-typed-struct-internal nm (fs ...) #,@mutable)))])
#'(begin d-s dtsi)))]
[(_ (vars ...) nm ([fld : ty] ...) . opts)
(with-syntax ([d-s (syntax-property (syntax/loc stx (define-struct nm (fld ...) . opts))
[(_ (vars:id ...) nm:struct-name (fs:fld-spec ...) . opts)
(with-syntax ([d-s (syntax-property (syntax/loc stx (define-struct nm (fs.fld ...) . opts))
'typechecker:ignore #t)]
[dtsi (internal (syntax/loc stx (define-typed-struct-internal (vars ...) nm ([fld : ty] ...))))])
[dtsi (internal (syntax/loc stx (define-typed-struct-internal (vars ...) nm (fs ...))))])
#'(begin d-s dtsi))]))
(define-syntax (require-typed-struct stx)

2
collects/typed-scheme/private/type-contract.ss
View File

@ -57,7 +57,7 @@
[(Mu: var (Union: (list (Value: '()) (Pair: elem-ty (F: var)))))
#`(listof #,(t->c elem-ty))]
[(? (lambda (e) (eq? t:Any-Syntax e))) #'syntax?]
[(Base: sym cnt) cnt]
[(Base: sym cnt) #`(flat-named-contract '#,sym (flat-contract-predicate #,cnt))]
[(Refinement: par p? cert)
#`(and/c #,(t->c par) (flat-contract #,(cert p?)))]
[(Union: elems)

12
collects/typed-scheme/rep/filter-rep.ss
View File

@ -32,7 +32,9 @@
[#:fold-rhs (*NotTypeFilter (type-rec-id t) (map pathelem-rec-id p) v)])
;; implication
(df ImpFilter ([a (listof Filter/c)] [c (listof Filter/c)]))
(df ImpFilter ([a (non-empty-listof Filter/c)] [c (non-empty-listof Filter/c)])
[#:frees (combine-frees (map free-vars* (append a c)))
(combine-frees (map free-idxs* (append a c)))])
(df FilterSet (thn els)
[#:frees (combine-frees (map free-vars* (append thn els)))
@ -68,7 +70,10 @@
[#:fold-rhs (*LNotTypeFilter (type-rec-id t) (map pathelem-rec-id p) idx)])
;; implication
(df LImpFilter ([a (listof LatentFilter/c)] [c (listof LatentFilter/c)]))
(dlf LImpFilter ([a (non-empty-listof LatentFilter/c)] [c (non-empty-listof LatentFilter/c)])
[#:frees (combine-frees (map free-vars* (append a c)))
(combine-frees (map free-idxs* (append a c)))])
(dlf LFilterSet (thn els)
[#:frees (combine-frees (map free-vars* (append thn els)))
@ -96,3 +101,6 @@
(flat-named-contract
'LatentFilterSet
(λ (e) (or (LFilterSet? e)))))
(define filter-equal? eq?)
(provide filter-equal?)

28
collects/typed-scheme/rep/free-variance.ss
View File

@ -1,9 +1,8 @@
#lang scheme/base
(require "../utils/utils.ss")
(require (for-syntax scheme/base)
(utils tc-utils)
mzlib/etc)
(require "../utils/utils.ss"
(for-syntax scheme/base)
(utils tc-utils) scheme/list
mzlib/etc scheme/contract)
;; this file contains support for calculating the free variables/indexes of types
;; actual computation is done in rep-utils.ss and type-rep.ss
@ -22,19 +21,28 @@
(provide Covariant Contravariant Invariant Constant Dotted)
(define (variance? e)
(memq e (list Covariant Contravariant Invariant Constant Dotted)))
;; hashtables for keeping track of free variables and indexes
(define index-table (make-weak-hasheq))
(define index-table (make-weak-hash))
;; maps Type to List[Cons[Number,Variance]]
(define var-table (make-weak-hasheq))
(define var-table (make-weak-hash))
;; maps Type to List[Cons[Symbol,Variance]]
(define (free-idxs* t) (hash-ref index-table t (lambda _ (int-err "type ~a not in index-table" (syntax-e t)))))
(define (free-vars* t) (hash-ref var-table t (lambda _ (int-err "type ~a not in var-table" (syntax-e t)))))
(define ((input/c tbl) val) (hash-ref tbl val #f))
(define (free-idxs* t)
(hash-ref index-table t (lambda _ (int-err "type ~a not in index-table" t))))
(define (free-vars* t)
(hash-ref var-table t (lambda _ (int-err "type ~a not in var-table" t))))
(define empty-hash-table (make-immutable-hasheq null))
(provide free-vars* free-idxs* empty-hash-table make-invariant)
(p/c [free-vars* (-> (input/c var-table) (hash/c symbol? variance?))]
[free-idxs* (-> (input/c index-table) (hash/c exact-nonnegative-integer? variance?))])
(provide empty-hash-table make-invariant)
;; frees = HT[Idx,Variance] where Idx is either Symbol or Number
;; (listof frees) -> frees

7
collects/typed-scheme/rep/rep-utils.ss
View File

@ -143,9 +143,10 @@
(syntax/loc s (struct nm pat))])))
(begin-for-syntax
(hash-set! ht-stx 'kw-stx (list #'ex #'flds.fs bfs-fold-rhs #'#,stx)))
intern
provides
frees))])))
(w/c nm ()
intern
frees)
provides))])))
(define-for-syntax (mk-fold ht type-rec-id rec-ids kws)
(lambda (stx)

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))]

4
collects/typed-scheme/ts-guide.scrbl
View File

@ -155,8 +155,8 @@ typed-scheme
(: tree-height (Tree -> Number))
(define (tree-height t)
(cond [(leaf? t) 1]
[else (max (tree-height (node-left t))
(tree-height (node-right t)))]))
[else (max (+ 1 (tree-height (node-left t)))
(+ 1 (tree-height (node-right t))))]))
(: tree-sum (Tree -> Number))
(define (tree-sum t)

4
collects/typed-scheme/ts-reference.scrbl
View File

@ -90,7 +90,7 @@ The following base types are parameteric in their type arguments.
types @scheme[t ...]. This can only appear as the return type of a
function.}
@defform/none[v]{where @scheme[v] is a number, boolean or string, is the singleton type containing only that value}
@defform/none['val]{where @scheme[val] is a Scheme value, is the singleton type containing only that value}
@defform/none[(quote val)]{where @scheme[val] is a Scheme value, is the singleton type containing only that value}
@defform/none[i]{where @scheme[i] is an identifier can be a reference to a type
name or a type variable}
@defform[(Rec n t)]{is a recursive type where @scheme[n] is bound to the
@ -228,7 +228,7 @@ This is legal only in expression contexts.}
appropriate number of type variables. This is legal only in expression
contexts.}
@schemevarfont|{#{e @ t ...}}| This is identical to @scheme[(inst e t ...)].
@litchar|{#{e @ t ...}}| This is identical to @scheme[(inst e t ...)].
@subsection{Require}

15
collects/typed-scheme/typecheck/provide-handling.ss
View File

@ -8,6 +8,8 @@
(private type-contract typed-renaming)
(rep type-rep)
(utils tc-utils)
scheme/contract/private/provide
unstable/syntax
"def-binding.ss")
(require (for-template scheme/base
@ -31,7 +33,7 @@
(make-typed-renaming (syntax-property id 'not-free-identifier=? #t) alt)
(make-rename-transformer (syntax-property id 'not-free-identifier=? #t))))
(define (generate-prov stx-defs val-defs)
(define (generate-prov stx-defs val-defs pos-blame-id)
(define mapping (make-free-identifier-mapping))
(lambda (form)
(define (mem? i vd)
@ -56,9 +58,16 @@
(cond [(type->contract (def-binding-ty b) (lambda () #f) #:out #t)
=>
(lambda (cnt)
(with-syntax ([(export-id cnt-id) (generate-temporaries #'(id id))])
(with-syntax ([(export-id cnt-id) (generate-temporaries #'(id id))]
[module-source pos-blame-id]
[the-contract (generate-temporary 'generated-contract)])
#`(begin
(define/contract cnt-id #,cnt id)
(define the-contract #,cnt)
(define-syntax cnt-id
(make-provide/contract-transformer
(quote-syntax the-contract)
(quote-syntax id)
(quote-syntax module-source)))
(define-syntax export-id
(if (unbox typed-context?)
(renamer #'id #:alt #'cnt-id)

43
collects/typed-scheme/typecheck/tc-app.ss
View File

@ -606,15 +606,33 @@
#:return (or expected (ret (Un)))
(string-append "No function domains matched in function application:\n"
(domain-mismatches t doms rests drests rngs argtys-t #f #f))))]
;; polymorphic functions without dotted rest, and without mandatory keyword args
;; any kind of polymorphic function
[((tc-result1: (and t (PolyDots:
(and vars (list fixed-vars ... dotted-var))
(Function: (list (and arrs (arr: doms rngs rests drests (list (Keyword: _ _ #f) ...))) ...)))))
(list (tc-result1: argtys-t) ...))
(handle-clauses (doms rngs rests drests arrs) f-stx args-stx
;; only try inference if the argument lengths are appropriate
(lambda (dom _ rest drest a)
(cond [rest (<= (length dom) (length argtys))]
[drest (and (<= (length dom) (length argtys))
(eq? dotted-var (cdr drest)))]
[else (= (length dom) (length argtys))]))
;; only try to infer the free vars of the rng (which includes the vars in filters/objects)
;; note that we have to use argtys-t here, since argtys is a list of tc-results
(lambda (dom rng rest drest a)
(if drest
(infer/dots fixed-vars dotted-var argtys-t dom (car drest) rng (fv rng)
#:expected (and expected (tc-results->values expected)))
(infer/vararg vars argtys-t dom rest rng (fv rng)
(and expected (tc-results->values expected)))))
t argtys expected)]
;; regular polymorphic functions without dotted rest, and without mandatory keyword args
[((tc-result1:
(and t
(or (Poly:
vars
(Function: (list (and arrs (arr: doms rngs rests (and drests #f) (list (Keyword: _ _ #f) ...))) ...)))
(PolyDots:
vars
(Function: (list (and arrs (arr: doms rngs rests (and drests #f) (list (Keyword: _ _ #f) ...))) ...))))))
(Poly:
vars
(Function: (list (and arrs (arr: doms rngs rests (and drests #f) (list (Keyword: _ _ #f) ...))) ...)))))
(list (tc-result1: argtys-t) ...))
(handle-clauses (doms rngs rests arrs) f-stx args-stx
;; only try inference if the argument lengths are appropriate
@ -623,17 +641,6 @@
;; note that we have to use argtys-t here, since argtys is a list of tc-results
(lambda (dom rng rest a) (infer/vararg vars argtys-t dom rest rng (fv rng) (and expected (tc-results->values expected))))
t argtys expected)]
;; polymorphic ... type
[((tc-result1: (and t (PolyDots:
(and vars (list fixed-vars ... dotted-var))
(Function: (list (and arrs (arr: doms rngs (and #f rests) (cons dtys dbounds) (list (Keyword: _ _ #f) ...))) ...)))))
(list (tc-result1: argtys-t) ...))
(handle-clauses (doms dtys dbounds rngs arrs) f-stx args-stx
(lambda (dom dty dbound rng arr) (and (<= (length dom) (length argtys))
(eq? dotted-var dbound)))
(lambda (dom dty dbound rng arr)
(infer/dots fixed-vars dotted-var argtys-t dom dty rng (fv rng) #:expected (and expected (tc-results->values expected))))
t argtys expected)]
;; procedural structs
[((tc-result1: (and sty (Struct: _ _ _ (? Function? proc-ty) _ _ _))) _)
(tc/funapp f-stx #`(#,(syntax/loc f-stx dummy) . #,args-stx) (ret proc-ty) (cons ftype0 argtys) expected)]

7
collects/typed-scheme/typecheck/tc-envops.ss
View File

@ -9,9 +9,10 @@
(rep type-rep)
(utils tc-utils)
(types resolve)
(only-in (env type-environments lexical-env) env? update-type/lexical env-map)
(only-in (env type-environments lexical-env) env? update-type/lexical env-map env-props replace-props)
scheme/contract scheme/match
mzlib/trace
(typecheck tc-metafunctions)
(for-syntax scheme/base))
(provide env+)
@ -57,9 +58,11 @@
;; sets the flag box to #f if anything becomes (U)
(d/c (env+ env fs flag)
(env? (listof Filter/c) (box/c #t). -> . env?)
(for/fold ([Γ env]) ([f fs])
(define-values (imps atoms) (combine-props fs (env-props env)))
(for/fold ([Γ (replace-props env imps)]) ([f atoms])
(match f
[(Bot:) (set-box! flag #f) (env-map (lambda (x) (cons (car x) (Un))) Γ)]
[(ImpFilter: _ _) Γ]
[(or (TypeFilter: _ _ x) (NotTypeFilter: _ _ x))
(update-type/lexical (lambda (x t) (let ([new-t (update t f)])
(when (type-equal? new-t (Un))

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

@ -32,8 +32,14 @@
[i:exp expected]
[i:boolean (-val (syntax-e #'i))]
[i:identifier (-val (syntax-e #'i))]
[i:exact-integer -Integer]
[(~var i (3d real?)) -Number]
[0 -Zero]
[(~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 inexact-real?)) -Flonum]
[(~var i (3d real?)) -Real]
[(~var i (3d number?)) -Number]
[i:str -String]
[i:char -Char]
[i:keyword (-val (syntax-e #'i))]
@ -41,10 +47,26 @@
[i:byte-pregexp -Byte-PRegexp]
[i:byte-regexp -Byte-Regexp]
[i:regexp -Regexp]
[(i ...)
(-Tuple (map tc-literal (syntax->list #'(i ...))))]
[i #:declare i (3d vector?)
(make-Vector (apply Un (map tc-literal (vector->list (syntax-e #'i)))))]
[(i ...)
(match expected
[(Mu: var (Union: (list (Value: '()) (Pair: elem-ty (F: var)))))
(-Tuple
(for/list ([l (in-list (syntax->list #'(i ...)))])
(tc-literal l elem-ty)))]
;; errors are handled elsewhere
[_ (-Tuple
(for/list ([l (in-list (syntax->list #'(i ...)))])
(tc-literal l #f)))])]
[(~var i (3d vector?))
(match expected
[(Vector: t)
(make-Vector (apply Un
(for/list ([l (syntax-e #'i)])
(tc-literal l t))))]
;; errors are handled elsewhere
[_ (make-Vector (apply Un
(for/list ([l (syntax-e #'i)])
(tc-literal l #f))))])]
[_ Univ]))

8
collects/typed-scheme/typecheck/tc-if.ss
View File

@ -41,9 +41,11 @@
[else (ret (Un))]))
(match (single-value tst)
[(tc-result1: _ (and f1 (FilterSet: fs+ fs-)) _)
(let-values ([(flag+ flag-) (values (box #t) (box #t))])
(match-let ([(tc-results: ts fs2 os2) (with-lexical-env (env+ (lexical-env) fs+ flag+) (tc thn (unbox flag+)))]
[(tc-results: us fs3 os3) (with-lexical-env (env+ (lexical-env) fs- flag-) (tc els (unbox flag-)))])
(let*-values ([(flag+ flag-) (values (box #t) (box #t))]
[(derived-imps+ derived-atoms+)
(combine-props fs+ (env-props (lexical-env)))])
(match-let* ([(tc-results: ts fs2 os2) (with-lexical-env (env+ (lexical-env) fs+ flag+) (tc thn (unbox flag+)))]
[(tc-results: us fs3 os3) (with-lexical-env (env+ (lexical-env) fs- flag-) (tc els (unbox flag-)))])
;; if we have the same number of values in both cases
(cond [(= (length ts) (length us))
(let ([r

45
collects/typed-scheme/typecheck/tc-metafunctions.ss
View File

@ -5,11 +5,11 @@
[-> -->]
[->* -->*]
[one-of/c -one-of/c])
(rep type-rep)
(rep type-rep filter-rep) scheme/list
scheme/contract scheme/match unstable/match
(for-syntax scheme/base))
(provide combine-filter apply-filter abstract-filter abstract-filters
(provide combine-filter apply-filter abstract-filter abstract-filters combine-props
split-lfilters merge-filter-sets values->tc-results tc-results->values)
;; this implements the sequence invariant described on the first page relating to Bot
@ -66,7 +66,7 @@
(apply append (for/list ([f f-]) (abo ids keys f))))]))
(d/c (abo xs idxs f)
(-> (listof identifier?) (listof index/c) Filter/c (or/c '() (list/c LatentFilter/c)))
((listof identifier?) (listof index/c) Filter/c . -> . (or/c null? (list/c LatentFilter/c)))
(define (lookup y)
(for/first ([x xs] [i idxs] #:when (free-identifier=? x y)) i))
(define-match-expander lookup:
@ -76,10 +76,12 @@
[(Bot:) (list (make-LBot))]
[(TypeFilter: t p (lookup: idx)) (list (make-LTypeFilter t p idx))]
[(NotTypeFilter: t p (lookup: idx)) (list (make-LNotTypeFilter t p idx))]
[(ImpFilter: a c)
(match* [(abo a) (abo c)]
[((list a*) (list c*)) (list (make-LImpFilter a* c*))]
[(_ _) null])]
[(ImpFilter: as cs)
(let ([a* (apply append (for/list ([f as]) (abo xs idxs f)))]
[c* (apply append (for/list ([f cs]) (abo xs idxs f)))])
(if (< (length a*) (length as)) ;; if we removed some things, we can't be sure
null
(list (make-LImpFilter a* c*))))]
[_ null]))
(define (merge-filter-sets fs)
@ -146,13 +148,13 @@
[((FilterSet: f1+ f1-) (T-FS:) (FilterSet: f3+ f3-)) (mk (combine null (append f1- f3-)))]
;; and
[((FilterSet: f1+ f1-) (FilterSet: f2+ f2-) (F-FS:))
(mk (combine (append f1+ f2+)
null
#;
(append (for/list ([f f1-])
(make-ImpFilter f2+ f))
(for/list ([f f2-])
(make-ImpFilter f1+ f)))))]
(mk (combine (append f1+ f2+)
(append (for/list ([f f1-]
#:when (not (null? f2+)))
(make-ImpFilter f2+ (list f)))
(for/list ([f f2-]
#:when (not (null? f1+)))
(make-ImpFilter f1+ (list f))))))]
[(f f* f*) (mk f*)]
[(_ _ _)
;; could intersect f2 and f3 here
@ -204,3 +206,18 @@
(define (tc-results->values tc)
(match tc
[(tc-results: ts) (-values ts)]))
(define (combine-props new-props old-props)
(define-values (new-imps new-atoms) (partition ImpFilter? new-props))
(define-values (derived-imps derived-atoms)
(for/fold
([derived-imps null]
[derived-atoms null])
([o old-props])
(match o
[(ImpFilter: as cs)
(let ([as* (remove* new-atoms as filter-equal?)])
(if (null? as*)
(values derived-imps (append cs new-atoms))
(values (cons (make-ImpFilter as* cs) derived-imps) derived-atoms)))])))
(values (append new-imps derived-imps) (append new-atoms derived-atoms)))

8
collects/typed-scheme/typecheck/tc-toplevel.ss
View File

@ -3,7 +3,7 @@
(require (rename-in "../utils/utils.ss" [infer r:infer]))
(require syntax/kerncase
unstable/list
unstable/list unstable/syntax
mzlib/etc
scheme/match
"signatures.ss"
@ -253,9 +253,11 @@
;; report delayed errors
(report-all-errors)
;; compute the new provides
(with-syntax
([((new-provs ...) ...) (map (generate-prov stx-defs val-defs) provs)])
(with-syntax*
([the-variable-reference (generate-temporary #'blame)]
[((new-provs ...) ...) (map (generate-prov stx-defs val-defs #'the-variable-reference) provs)])
#`(begin
(define the-variable-reference (#%variable-reference))
#,(env-init-code)
#,(tname-env-init-code)
#,(talias-env-init-code)

29
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)
@ -67,9 +68,6 @@
(define -Listof (-poly (list-elem) (make-Listof list-elem)))
(define -Number (make-Base 'Number #'number?))
(define -Integer (make-Base 'Integer #'exact-integer?))
(define -Boolean (make-Base 'Boolean #'boolean?))
(define -Symbol (make-Base 'Symbol #'symbol?))
(define -Void (make-Base 'Void #'void?))
@ -96,15 +94,11 @@
(define Univ (make-Univ))
(define Err (make-Error))
(define -Nat -Integer)
(define -Real -Number)
(define -Port (*Un -Output-Port -Input-Port))
(define -Pathlike (*Un -String -Path))
(define -Pathlike* (*Un -String -Path (-val 'up) (-val 'same)))
(define -Pattern (*Un -Bytes -Regexp -PRegexp -Byte-Regexp -Byte-PRegexp -String))
(define -Byte -Number)
(define -no-lfilter (make-LFilterSet null null))
(define -no-filter (make-FilterSet null null))
@ -114,6 +108,26 @@
(define -car (make-CarPE))
(define -cdr (make-CdrPE))
;; Numeric hierarchy
(define -Number (make-Base 'Number #'number?))
(define -Flonum (make-Base 'Flonum #'inexact-real?))
(define -ExactRational
(make-Base 'Exact-Rational #'(and/c number? rational? exact?)))
(define -Integer (make-Base 'Integer #'exact-integer?))
(define -ExactPositiveInteger
(make-Base 'Exact-Positive-Integer #'exact-positive-integer?))
(define -Zero (-val 0))
(define -Real (*Un -Flonum -ExactRational))
(define -ExactNonnegativeInteger (*Un -ExactPositiveInteger -Zero))
(define -Nat -ExactNonnegativeInteger)
(define -Byte -Number)
;; convenient syntax
(define-syntax -v
@ -247,7 +261,6 @@
(define true-filter (-FS (list) (list (make-Bot))))
(define false-filter (-FS (list (make-Bot)) (list)))
(define (opt-fn args opt-args result)
(apply cl->* (for/list ([i (in-range (add1 (length opt-args)))])
(make-Function (list (make-arr* (append args (take opt-args i)) result))))))

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

@ -30,6 +30,7 @@
(let loop ([t* t])
(match t*
[(Value: '()) (-lst Univ)]
[(Value: 0) -Nat]
[(Mu: var (Union: (list (Value: '()) (Pair: _ (F: var))))) t*]
[(Pair: t1 (Value: '())) (-lst t1)]
[(Pair: t1 t2)
@ -45,7 +46,7 @@
(define In-Syntax
(-mu e
(*Un -Number -Boolean -Symbol -String -Keyword -Char
(*Un -Boolean -Symbol -String -Keyword -Char -Number
(make-Vector (-Syntax e))
(make-Box (-Syntax e))
(-mu list

17
collects/typed-scheme/types/printer.ss
View File

@ -45,7 +45,9 @@
(fp")")]
[(LNotTypeFilter: type path idx) (fp "(! ~a @ ~a ~a)" type path idx)]
[(LTypeFilter: type path idx) (fp "(~a @ ~a ~a)" type path idx)]
[(LBot:) (fp "LBot")]))
[(LBot:) (fp "LBot")]
[(LImpFilter: a c) (fp "(LImpFilter ~a ~a)" a c)]
[else (fp "(Unknown Latent Filter: ~a)" (struct->vector c))]))
(define (print-filter c port write?)
(define (fp . args) (apply fprintf port args))
@ -57,14 +59,17 @@
[(NoFilter:) (fp "-")]
[(NotTypeFilter: type path id) (fp "(! ~a @ ~a ~a)" type path (syntax-e id))]
[(TypeFilter: type path id) (fp "(~a @ ~a ~a)" type path (syntax-e id))]
[(Bot:) (fp "Bot")]))
[(Bot:) (fp "Bot")]
[(ImpFilter: a c) (fp "(ImpFilter ~a ~a)" a c)]
[else (fp "(Unknown Filter: ~a)" (struct->vector c))]))
(define (print-pathelem c port write?)
(define (fp . args) (apply fprintf port args))
(match c
[(CarPE:) (fp "car")]
[(CdrPE:) (fp "cdr")]
[(StructPE: t i) (fp "(~a ~a)" t i)]))
[(StructPE: t i) (fp "(~a ~a)" t i)]
[else (fp "(Unknown Path Element: ~a)" (struct->vector c))]))
(define (print-latentobject c port write?)
(define (fp . args) (apply fprintf port args))
@ -77,7 +82,8 @@
(match c
[(NoObject:) (fp "-")]
[(Empty:) (fp "")]
[(Path: pes i) (fp "~a" (append pes (list (syntax-e i))))]))
[(Path: pes i) (fp "~a" (append pes (list (syntax-e i))))]
[else (fp "(Unknown Object: ~a)" (struct->vector c))]))
;; print out a type
;; print-type : Type Port Boolean -> Void
@ -119,7 +125,8 @@
(fp/filter "-> ~a : ~a ~a" t lf lo)]
[_
(fp "-> ~a" rng)])
(fp ")")]))
(fp ")")]
[else (fp "(Unknown Function Type: ~a)" (struct->vector a))]))
(define (tuple? t)
(match t
[(Pair: a (? tuple?)) #t]

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

@ -5,8 +5,10 @@
(types utils comparison resolve abbrev)
(env type-name-env)
(only-in (infer infer-dummy) unify)
scheme/match
mzlib/trace
scheme/match unstable/match
mzlib/trace (rename-in scheme/contract
[-> c->]
[->* c->*])
(for-syntax scheme/base syntax/parse))
;; exn representing failure of subtyping
@ -179,7 +181,8 @@
;(trace subtypes*/varargs)
(define (combine-arrs arrs)
(d/c (combine-arrs arrs)
(c-> (listof arr?) (or/c #f arr?))
(match arrs
[(list (arr: dom1 rng1 #f #f '()) (arr: dom rng #f #f '()) ...)
(cond
@ -188,7 +191,7 @@
#f)
((not (foldl type-equal? rng1 rng))
#f)
[else (make-arr (apply map (lambda args (make-Union args)) (cons dom1 dom)) rng1 #f #f '())])]
[else (make-arr (apply map (lambda args (make-Union (sort args type<?))) (cons dom1 dom)) rng1 #f #f '())])]
[_ #f]))
@ -210,34 +213,53 @@
[else
(let* ([A0 (remember s t A)])
(parameterize ([current-seen A0])
(match (list s t)
[(list _ (Univ:)) A0]
(match* (s t)
[(_ (Univ:)) A0]
;; error is top and bot
[(list _ (Error:)) A0]
[(list (Error:) _) A0]
[(_ (Error:)) A0]
[((Error:) _) A0]
;; (Un) is bot
[(list _ (Union: (list))) (fail! s t)]
[(list (Union: (list)) _) A0]
[(_ (Union: (list))) (fail! s t)]
[((Union: (list)) _) A0]
;; value types
[(list (Value: v1) (Value: v2)) (=> unmatch) (if (equal? v1 v2) A0 (unmatch))]
;; integers are numbers too
[(list (Base: 'Integer _) (Base: 'Number _)) A0]
[((Value: v1) (Value: v2)) (=> unmatch) (if (equal? v1 v2) A0 (unmatch))]
;; now we encode the numeric hierarchy - bletch
[((Base: 'Integer _) (Base: 'Number _)) A0]
[((Base: 'Flonum _) (== -Real type-equal?)) A0]
[((Base: 'Integer _) (== -Real type-equal?)) A0]
[((Base: 'Flonum _) (Base: 'Number _)) A0]
[((Base: 'Exact-Rational _) (Base: 'Number _)) A0]
[((Base: 'Integer _) (Base: 'Exact-Rational _)) A0]
[((Base: 'Exact-Positive-Integer _) (Base: 'Exact-Rational _)) A0]
[((Base: 'Exact-Positive-Integer _) (Base: 'Number _)) A0]
[((Base: 'Exact-Positive-Integer _) (== -Nat type-equal?)) A0]
[((Base: 'Exact-Positive-Integer _) (Base: 'Integer _)) A0]
[((== -Nat type-equal?) (Base: 'Number _)) A0]
[((== -Nat type-equal?) (Base: 'Exact-Rational _)) A0]
[((== -Nat type-equal?) (Base: 'Integer _)) A0]
;; values are subtypes of their "type"
[(list (Value: (? integer? n)) (Base: 'Integer _)) A0]
[(list (Value: (? number? n)) (Base: 'Number _)) A0]
[(list (Value: (? boolean? n)) (Base: 'Boolean _)) A0]
[(list (Value: (? symbol? n)) (Base: 'Symbol _)) A0]
[(list (Value: (? string? n)) (Base: 'String _)) A0]
[((Value: (? exact-integer? n)) (Base: 'Integer _)) A0]
[((Value: (and n (? number?) (? exact?) (? rational?))) (Base: 'Exact-Rational _)) A0]
[((Value: (? exact-nonnegative-integer? n)) (== -Nat type-equal?)) A0]
[((Value: (? exact-positive-integer? n)) (Base: 'Exact-Positive-Integer _)) A0]
[((Value: (? inexact-real? n)) (Base: 'Flonum _)) A0]
[((Value: (? real? n)) (== -Real type-equal?)) A0]
[((Value: (? number? n)) (Base: 'Number _)) A0]
[((Value: (? boolean? n)) (Base: 'Boolean _)) A0]
[((Value: (? symbol? n)) (Base: 'Symbol _)) A0]
[((Value: (? string? n)) (Base: 'String _)) A0]
;; tvars are equal if they are the same variable
[(list (F: t) (F: t*)) (if (eq? t t*) A0 (fail! s t))]
[((F: t) (F: t*)) (if (eq? t t*) A0 (fail! s t))]
;; special-case for case-lambda/union
[(list (Function: arr1) (Function: (list arr2)))
[((Function: arr1) (Function: (list arr2)))
(when (null? arr1) (fail! s t))
(or (arr-subtype*/no-fail A0 (combine-arrs arr1) arr2)
(supertype-of-one/arr A0 arr2 arr1)
(fail! s t))]
;; case-lambda
[(list (Function: arr1) (Function: arr2))
[((Function: arr1) (Function: arr2))
(when (null? arr1) (fail! s t))
(let loop-arities ([A* A0]
[arr2 arr2])
@ -246,65 +268,65 @@
[(supertype-of-one/arr A* (car arr2) arr1) => (lambda (A) (loop-arities A (cdr arr2)))]
[else (fail! s t)]))]
;; recur structurally on pairs
[(list (Pair: a d) (Pair: a* d*))
[((Pair: a d) (Pair: a* d*))
(let ([A1 (subtype* A0 a a*)])
(and A1 (subtype* A1 d d*)))]
;; quantification over two types preserves subtyping
[(list (Poly: ns b1) (Poly: ms b2))
[((Poly: ns b1) (Poly: ms b2))
(=> unmatch)
(unless (= (length ns) (length ms))
(unmatch))
;(printf "Poly: ~n~a ~n~a~n" b1 (subst-all (map list ms (map make-F ns)) b2))
(subtype* A0 b1 (subst-all (map list ms (map make-F ns)) b2))]
[(list (Refinement: par _ _) t)
[((Refinement: par _ _) t)
(subtype* A0 par t)]
;; use unification to see if we can use the polytype here
[(list (Poly: vs b) s)
[((Poly: vs b) s)
(=> unmatch)
(if (unify vs (list b) (list s)) A0 (unmatch))]
[(list s (Poly: vs b))
[(s (Poly: vs b))
(=> unmatch)
(if (null? (fv b)) (subtype* A0 s b) (unmatch))]
;; rec types, applications and names (that aren't the same
[(list (? needs-resolving? s) other)
[((? needs-resolving? s) other)
(let ([s* (resolve-once s)])
(if (Type? s*) ;; needed in case this was a name that hasn't been resolved yet
(subtype* A0 s* other)
(fail! s t)))]
[(list other (? needs-resolving? t))
[(other (? needs-resolving? t))
(let ([t* (resolve-once t)])
(if (Type? t*) ;; needed in case this was a name that hasn't been resolved yet
(subtype* A0 other t*)
(fail! s t)))]
;; for unions, we check the cross-product
[(list (Union: es) t) (and (andmap (lambda (elem) (subtype* A0 elem t)) es) A0)]
[(list s (Union: es)) (and (ormap (lambda (elem) (subtype*/no-fail A0 s elem)) es) A0)]
[((Union: es) t) (and (andmap (lambda (elem) (subtype* A0 elem t)) es) A0)]
[(s (Union: es)) (and (ormap (lambda (elem) (subtype*/no-fail A0 s elem)) es) A0)]
;; subtyping on immutable structs is covariant
[(list (Struct: nm _ flds #f _ _ _) (Struct: nm _ flds* #f _ _ _))
[((Struct: nm _ flds #f _ _ _) (Struct: nm _ flds* #f _ _ _))
(subtypes* A0 flds flds*)]
[(list (Struct: nm _ flds proc _ _ _) (Struct: nm _ flds* proc* _ _ _))
[((Struct: nm _ flds proc _ _ _) (Struct: nm _ flds* proc* _ _ _))
(subtypes* A0 (cons proc flds) (cons proc* flds*))]
;; subtyping on structs follows the declared hierarchy
[(list (Struct: nm (? Type? parent) flds proc _ _ _) other)
[((Struct: nm (? Type? parent) flds proc _ _ _) other)
;(printf "subtype - hierarchy : ~a ~a ~a~n" nm parent other)
(subtype* A0 parent other)]
;; Promises are covariant
[(list (Struct: 'Promise _ (list t) _ _ _ _) (Struct: 'Promise _ (list t*) _ _ _ _)) (subtype* A0 t t*)]
[((Struct: 'Promise _ (list t) _ _ _ _) (Struct: 'Promise _ (list t*) _ _ _ _)) (subtype* A0 t t*)]
;; subtyping on values is pointwise
[(list (Values: vals1) (Values: vals2)) (subtypes* A0 vals1 vals2)]
[((Values: vals1) (Values: vals2)) (subtypes* A0 vals1 vals2)]
;; trivial case for Result
[(list (Result: t f o) (Result: t* f o))
[((Result: t f o) (Result: t* f o))
(subtype* A0 t t*)]
;; we can ignore interesting results
[(list (Result: t f o) (Result: t* (LFilterSet: (list) (list)) (LEmpty:)))
[((Result: t f o) (Result: t* (LFilterSet: (list) (list)) (LEmpty:)))
(subtype* A0 t t*)]
;; subtyping on other stuff
[(list (Syntax: t) (Syntax: t*))
[((Syntax: t) (Syntax: t*))
(subtype* A0 t t*)]
[(list (Instance: t) (Instance: t*))
[((Instance: t) (Instance: t*))
(subtype* A0 t t*)]
;; otherwise, not a subtype
[_ (fail! s t) #;(printf "failed")])))]))))
[(_ _) (fail! s t) #;(printf "failed")])))]))))
(define (type-compare? a b)
(and (subtype a b) (subtype b a)))

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)])))

1
collects/typed/net/cgi.ss
View File

@ -3,6 +3,7 @@
(require typed/private/utils)
(require-typed-struct cgi-error () net/cgi)
(require-typed-struct (incomplete-%-suffix cgi-error) ([chars : (Listof Char)]) net/cgi)
(require-typed-struct (invalid-%-suffix cgi-error) ([char : Char]) net/cgi)

10
collects/typed/private/wrap.ss Normal file
View File

@ -0,0 +1,10 @@
#lang scheme
(define-syntax (mb stx)
(syntax-case stx ()
[(_ id)
#'(#%plain-module-begin
(require id)
(provide (all-from-out id)))]))
(provide (rename-out [mb #%module-begin]))

4
collects/typed/scheme.ss Normal file
View File

@ -0,0 +1,4 @@
#lang s-exp typed-scheme/minimal
(require typed/scheme/base (subtract-in scheme typed/scheme/base scheme/contract))
(provide (all-from-out typed/scheme/base scheme))

19
collects/typed/scheme/base.ss Normal file
View File

@ -0,0 +1,19 @@
#lang s-exp typed-scheme/minimal
(providing (libs (except scheme/base #%module-begin #%top-interaction with-handlers lambda #%app)
(except typed-scheme/private/prims)
(except typed-scheme/private/base-types-new)
(except typed-scheme/private/base-types-extra))
(basics #%module-begin
#%top-interaction
lambda
#%app))
(require typed-scheme/private/base-env
typed-scheme/private/base-special-env
typed-scheme/private/base-env-numeric
typed-scheme/private/base-env-indexing
(for-syntax typed-scheme/private/base-types-extra))
(provide (rename-out [with-handlers: with-handlers])
(for-syntax (all-from-out typed-scheme/private/base-types-extra)))

8
collects/typed/scheme/base/lang/reader.ss Normal file
View File

@ -0,0 +1,8 @@
#lang s-exp syntax/module-reader
typed/scheme/base
#:read r:read
#:read-syntax r:read-syntax
(require (prefix-in r: typed-scheme/typed-reader))

8
collects/typed/scheme/lang/reader.ss Normal file
View File

@ -0,0 +1,8 @@
#lang s-exp syntax/module-reader
typed/scheme
#:read r:read
#:read-syntax r:read-syntax
(require (prefix-in r: typed-scheme/typed-reader))

11
collects/typed/scheme/system.ss
View File

@ -1,10 +1 @@
#lang typed-scheme
(require typed/private/utils)
(require/typed/provide
scheme/system
[system (String -> Boolean)]
[system* (Path-String String * -> Boolean)]
[system/exit-code (String -> Integer)]
[system*/exit-code (Path-String String * -> Integer)])
#lang s-exp typed/private/wrap scheme/system