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

Fix handling of logical props in `tc-if'.

Browse Source 
New numeric hierarchy.
Quoted lists and vectors now use the expected type, and quoted lists have (List a b c) type.  
Fix some contracts.
More general handling of polymorphic function application.
Use `make-provide/contract-transformer' to generate correct blame for typed provided identifiers.
Add mutable pairs. 
Use `raise-syntax-error' for better error messages in mzscheme.
Use `match*' instead of `list'
Some fixes to appease the contract checking.
Catch-all printing cases.
Use names in Base contract generation.
Types for lots of new primitives.
Move numeric primitives to their own file.
Move indexing primites to their own abstracted file.
Better error message from `define-struct:'
Fix 'insert-large-letters.ss' for new Number hierarchy.
Add `typed/scheme' and `typed/scheme/base', which use new number hierarcy types, stricter indexing types.

svn: r17284
This commit is contained in:
Sam Tobin-Hochstadt 2009-12-13 04:45:17 +00:00
commit 22903bffcd
54 changed files with 960 additions and 559 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
collects/drscheme/private/insert-large-letters.ss
View File

@ -153,10 +153,10 @@
(format " (~a)" (floor (inexact->exact w))))))
(: get-max-line-width ((Instance Scheme:Text%) -> Number))
(: get-max-line-width ((Instance Scheme:Text%) -> Real))
(define (get-max-line-width txt)
(let loop ([i (+ (send txt last-paragraph) 1)]
[m #{0 :: Number}])
[#{m : Integer} 0])
(cond
[(zero? i) m]
[else (loop (- i 1)

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-old.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 -Integer)))
(begin-for-syntax (initialize-type-env e))

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