diff --git a/collects/tests/typed-scheme/fail/back-and-forth.ss b/collects/tests/typed-scheme/fail/back-and-forth.ss index f8c00930..eac8be7d 100644 --- a/collects/tests/typed-scheme/fail/back-and-forth.ss +++ b/collects/tests/typed-scheme/fail/back-and-forth.ss @@ -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) diff --git a/collects/tests/typed-scheme/fail/too-many-errors.ss b/collects/tests/typed-scheme/fail/too-many-errors.ss new file mode 100644 index 00000000..6d726847 --- /dev/null +++ b/collects/tests/typed-scheme/fail/too-many-errors.ss @@ -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) diff --git a/collects/tests/typed-scheme/main.ss b/collects/tests/typed-scheme/main.ss index 2b223600..74d68762 100644 --- a/collects/tests/typed-scheme/main.ss +++ b/collects/tests/typed-scheme/main.ss @@ -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 diff --git a/collects/tests/typed-scheme/succeed/logic.ss b/collects/tests/typed-scheme/succeed/logic.ss new file mode 100644 index 00000000..c21abe72 --- /dev/null +++ b/collects/tests/typed-scheme/succeed/logic.ss @@ -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)) \ No newline at end of file diff --git a/collects/tests/typed-scheme/succeed/map-nonempty.ss b/collects/tests/typed-scheme/succeed/map-nonempty.ss new file mode 100644 index 00000000..0fddf079 --- /dev/null +++ b/collects/tests/typed-scheme/succeed/map-nonempty.ss @@ -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)))) \ No newline at end of file diff --git a/collects/tests/typed-scheme/succeed/metrics.ss b/collects/tests/typed-scheme/succeed/metrics.ss index ad067480..0135be32 100644 --- a/collects/tests/typed-scheme/succeed/metrics.ss +++ b/collects/tests/typed-scheme/succeed/metrics.ss @@ -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)] diff --git a/collects/tests/typed-scheme/succeed/new-metrics.ss b/collects/tests/typed-scheme/succeed/new-metrics.ss index cb1218a5..a3316300 100644 --- a/collects/tests/typed-scheme/succeed/new-metrics.ss +++ b/collects/tests/typed-scheme/succeed/new-metrics.ss @@ -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))]) diff --git a/collects/tests/typed-scheme/succeed/random-bits.ss b/collects/tests/typed-scheme/succeed/random-bits.ss index eea51558..d6f1ba20 100644 --- a/collects/tests/typed-scheme/succeed/random-bits.ss +++ b/collects/tests/typed-scheme/succeed/random-bits.ss @@ -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)) diff --git a/collects/tests/typed-scheme/unit-tests/parse-type-tests.ss b/collects/tests/typed-scheme/unit-tests/parse-type-tests.ss index 82f6f91f..973c53ad 100644 --- a/collects/tests/typed-scheme/unit-tests/parse-type-tests.ss +++ b/collects/tests/typed-scheme/unit-tests/parse-type-tests.ss @@ -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)) diff --git a/collects/tests/typed-scheme/unit-tests/subtype-tests.ss b/collects/tests/typed-scheme/unit-tests/subtype-tests.ss index c84dcce5..bb3be770 100644 --- a/collects/tests/typed-scheme/unit-tests/subtype-tests.ss +++ b/collects/tests/typed-scheme/unit-tests/subtype-tests.ss @@ -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 diff --git a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss index 758e98e8..4a7dbb58 100644 --- a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss +++ b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss @@ -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)) diff --git a/collects/typed-scheme/env/lexical-env.ss b/collects/typed-scheme/env/lexical-env.ss index 52b2659d..f3386bd4 100644 --- a/collects/typed-scheme/env/lexical-env.ss +++ b/collects/typed-scheme/env/lexical-env.ss @@ -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 diff --git a/collects/typed-scheme/env/type-env.ss b/collects/typed-scheme/env/type-env.ss index d454e062..37418e41 100644 --- a/collects/typed-scheme/env/type-env.ss +++ b/collects/typed-scheme/env/type-env.ss @@ -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 diff --git a/collects/typed-scheme/env/type-environments.ss b/collects/typed-scheme/env/type-environments.ss index 12c570c2..2ae35bc6 100644 --- a/collects/typed-scheme/env/type-environments.ss +++ b/collects/typed-scheme/env/type-environments.ss @@ -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)] diff --git a/collects/typed-scheme/main.ss b/collects/typed-scheme/main.ss index e2f553da..a072bfdb 100644 --- a/collects/typed-scheme/main.ss +++ b/collects/typed-scheme/main.ss @@ -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) diff --git a/collects/typed-scheme/minimal.ss b/collects/typed-scheme/minimal.ss index 40bcc4c9..f3b6d039 100644 --- a/collects/typed-scheme/minimal.ss +++ b/collects/typed-scheme/minimal.ss @@ -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) diff --git a/collects/typed-scheme/private/base-env-indexing-abs.ss b/collects/typed-scheme/private/base-env-indexing-abs.ss new file mode 100644 index 00000000..63581174 --- /dev/null +++ b/collects/typed-scheme/private/base-env-indexing-abs.ss @@ -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)])] + + )) + \ No newline at end of file diff --git a/collects/typed-scheme/private/base-env-indexing.ss b/collects/typed-scheme/private/base-env-indexing.ss new file mode 100644 index 00000000..57e74fc6 --- /dev/null +++ b/collects/typed-scheme/private/base-env-indexing.ss @@ -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)) + + diff --git a/collects/typed-scheme/private/base-env-numeric.ss b/collects/typed-scheme/private/base-env-numeric.ss new file mode 100644 index 00000000..f0c05718 --- /dev/null +++ b/collects/typed-scheme/private/base-env-numeric.ss @@ -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] diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss index 39c1c2cf..e270e5d2 100644 --- a/collects/typed-scheme/private/base-env.ss +++ b/collects/typed-scheme/private/base-env.ss @@ -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 diff --git a/collects/typed-scheme/private/base-types-new.ss b/collects/typed-scheme/private/base-types-new.ss new file mode 100644 index 00000000..dd8ff7ae --- /dev/null +++ b/collects/typed-scheme/private/base-types-new.ss @@ -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] diff --git a/collects/typed-scheme/private/base-types.ss b/collects/typed-scheme/private/base-types.ss index 32e03043..af91b029 100644 --- a/collects/typed-scheme/private/base-types.ss +++ b/collects/typed-scheme/private/base-types.ss @@ -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] diff --git a/collects/typed-scheme/private/env-lang.ss b/collects/typed-scheme/private/env-lang.ss index 434b5f5a..c1cd3f3b 100644 --- a/collects/typed-scheme/private/env-lang.ss +++ b/collects/typed-scheme/private/env-lang.ss @@ -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) diff --git a/collects/typed-scheme/private/extra-procs.ss b/collects/typed-scheme/private/extra-procs.ss index 19f91a6d..6cd86438 100644 --- a/collects/typed-scheme/private/extra-procs.ss +++ b/collects/typed-scheme/private/extra-procs.ss @@ -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)))) - diff --git a/collects/typed-scheme/private/prims.ss b/collects/typed-scheme/private/prims.ss index 190c832a..5723b612 100644 --- a/collects/typed-scheme/private/prims.ss +++ b/collects/typed-scheme/private/prims.ss @@ -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) diff --git a/collects/typed-scheme/private/type-contract.ss b/collects/typed-scheme/private/type-contract.ss index 79d76095..5ac589a9 100644 --- a/collects/typed-scheme/private/type-contract.ss +++ b/collects/typed-scheme/private/type-contract.ss @@ -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) diff --git a/collects/typed-scheme/rep/filter-rep.ss b/collects/typed-scheme/rep/filter-rep.ss index 8f353d7b..e3a95d30 100644 --- a/collects/typed-scheme/rep/filter-rep.ss +++ b/collects/typed-scheme/rep/filter-rep.ss @@ -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?) \ No newline at end of file diff --git a/collects/typed-scheme/rep/free-variance.ss b/collects/typed-scheme/rep/free-variance.ss index 7e4014e3..6b87ae63 100644 --- a/collects/typed-scheme/rep/free-variance.ss +++ b/collects/typed-scheme/rep/free-variance.ss @@ -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 diff --git a/collects/typed-scheme/rep/rep-utils.ss b/collects/typed-scheme/rep/rep-utils.ss index ca994b19..a0de7c5a 100644 --- a/collects/typed-scheme/rep/rep-utils.ss +++ b/collects/typed-scheme/rep/rep-utils.ss @@ -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) diff --git a/collects/typed-scheme/rep/type-rep.ss b/collects/typed-scheme/rep/type-rep.ss index 1c0784fd..5db6f744 100644 --- a/collects/typed-scheme/rep/type-rep.ss +++ b/collects/typed-scheme/rep/type-rep.ss @@ -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))] diff --git a/collects/typed-scheme/ts-guide.scrbl b/collects/typed-scheme/ts-guide.scrbl index d3af990c..75c0b713 100644 --- a/collects/typed-scheme/ts-guide.scrbl +++ b/collects/typed-scheme/ts-guide.scrbl @@ -155,8 +155,8 @@ typed-scheme (: tree-height (Tree -> Number)) (define (tree-height t) (cond [(leaf? t) 1] - [else (max (tree-height (node-left t)) - (tree-height (node-right t)))])) + [else (max (+ 1 (tree-height (node-left t))) + (+ 1 (tree-height (node-right t))))])) (: tree-sum (Tree -> Number)) (define (tree-sum t) diff --git a/collects/typed-scheme/ts-reference.scrbl b/collects/typed-scheme/ts-reference.scrbl index f52c4a98..09569bf3 100644 --- a/collects/typed-scheme/ts-reference.scrbl +++ b/collects/typed-scheme/ts-reference.scrbl @@ -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} diff --git a/collects/typed-scheme/typecheck/provide-handling.ss b/collects/typed-scheme/typecheck/provide-handling.ss index 5fb645ca..8943cc59 100644 --- a/collects/typed-scheme/typecheck/provide-handling.ss +++ b/collects/typed-scheme/typecheck/provide-handling.ss @@ -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) diff --git a/collects/typed-scheme/typecheck/tc-app.ss b/collects/typed-scheme/typecheck/tc-app.ss index 4c214123..89a37e48 100644 --- a/collects/typed-scheme/typecheck/tc-app.ss +++ b/collects/typed-scheme/typecheck/tc-app.ss @@ -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)] diff --git a/collects/typed-scheme/typecheck/tc-envops.ss b/collects/typed-scheme/typecheck/tc-envops.ss index c6d8a223..9acea43b 100644 --- a/collects/typed-scheme/typecheck/tc-envops.ss +++ b/collects/typed-scheme/typecheck/tc-envops.ss @@ -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)) diff --git a/collects/typed-scheme/typecheck/tc-expr-unit.ss b/collects/typed-scheme/typecheck/tc-expr-unit.ss index b57abb2f..a1af3449 100644 --- a/collects/typed-scheme/typecheck/tc-expr-unit.ss +++ b/collects/typed-scheme/typecheck/tc-expr-unit.ss @@ -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])) diff --git a/collects/typed-scheme/typecheck/tc-if.ss b/collects/typed-scheme/typecheck/tc-if.ss index 94f6aabe..b286b474 100644 --- a/collects/typed-scheme/typecheck/tc-if.ss +++ b/collects/typed-scheme/typecheck/tc-if.ss @@ -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 diff --git a/collects/typed-scheme/typecheck/tc-metafunctions.ss b/collects/typed-scheme/typecheck/tc-metafunctions.ss index 2d703756..39d44def 100644 --- a/collects/typed-scheme/typecheck/tc-metafunctions.ss +++ b/collects/typed-scheme/typecheck/tc-metafunctions.ss @@ -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))) diff --git a/collects/typed-scheme/typecheck/tc-toplevel.ss b/collects/typed-scheme/typecheck/tc-toplevel.ss index 86023b30..1b2a000e 100644 --- a/collects/typed-scheme/typecheck/tc-toplevel.ss +++ b/collects/typed-scheme/typecheck/tc-toplevel.ss @@ -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) diff --git a/collects/typed-scheme/types/abbrev.ss b/collects/typed-scheme/types/abbrev.ss index 27e9ed6e..8d141416 100644 --- a/collects/typed-scheme/types/abbrev.ss +++ b/collects/typed-scheme/types/abbrev.ss @@ -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)))))) diff --git a/collects/typed-scheme/types/convenience.ss b/collects/typed-scheme/types/convenience.ss index 70dce20c..15d818f6 100644 --- a/collects/typed-scheme/types/convenience.ss +++ b/collects/typed-scheme/types/convenience.ss @@ -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 diff --git a/collects/typed-scheme/types/printer.ss b/collects/typed-scheme/types/printer.ss index 33d6602b..b39ccfdb 100644 --- a/collects/typed-scheme/types/printer.ss +++ b/collects/typed-scheme/types/printer.ss @@ -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] diff --git a/collects/typed-scheme/types/subtype.ss b/collects/typed-scheme/types/subtype.ss index 3bbb1d6d..3f6e8303 100644 --- a/collects/typed-scheme/types/subtype.ss +++ b/collects/typed-scheme/types/subtype.ss @@ -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 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))) diff --git a/collects/typed-scheme/utils/tc-utils.ss b/collects/typed-scheme/utils/tc-utils.ss index e6547683..48fd8124 100644 --- a/collects/typed-scheme/utils/tc-utils.ss +++ b/collects/typed-scheme/utils/tc-utils.ss @@ -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) diff --git a/collects/typed/framework/framework.ss b/collects/typed/framework/framework.ss index 513cfa1d..a447016b 100644 --- a/collects/typed/framework/framework.ss +++ b/collects/typed/framework/framework.ss @@ -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)]))) diff --git a/collects/typed/mred/mred.ss b/collects/typed/mred/mred.ss index 053d102a..60e475e4 100644 --- a/collects/typed/mred/mred.ss +++ b/collects/typed/mred/mred.ss @@ -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)]))) diff --git a/collects/typed/net/cgi.ss b/collects/typed/net/cgi.ss index 9318478a..ee070c78 100644 --- a/collects/typed/net/cgi.ss +++ b/collects/typed/net/cgi.ss @@ -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) diff --git a/collects/typed/private/wrap.ss b/collects/typed/private/wrap.ss new file mode 100644 index 00000000..8f2bb87b --- /dev/null +++ b/collects/typed/private/wrap.ss @@ -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])) \ No newline at end of file diff --git a/collects/typed/scheme.ss b/collects/typed/scheme.ss new file mode 100644 index 00000000..37e8e2ad --- /dev/null +++ b/collects/typed/scheme.ss @@ -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)) \ No newline at end of file diff --git a/collects/typed/scheme/base.ss b/collects/typed/scheme/base.ss new file mode 100644 index 00000000..000da9a2 --- /dev/null +++ b/collects/typed/scheme/base.ss @@ -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))) diff --git a/collects/typed/scheme/base/lang/reader.ss b/collects/typed/scheme/base/lang/reader.ss new file mode 100644 index 00000000..f276a7b4 --- /dev/null +++ b/collects/typed/scheme/base/lang/reader.ss @@ -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)) diff --git a/collects/typed/scheme/lang/reader.ss b/collects/typed/scheme/lang/reader.ss new file mode 100644 index 00000000..e5397c57 --- /dev/null +++ b/collects/typed/scheme/lang/reader.ss @@ -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)) diff --git a/collects/typed/scheme/system.ss b/collects/typed/scheme/system.ss index f10fe2e2..61bc8bc1 100644 --- a/collects/typed/scheme/system.ss +++ b/collects/typed/scheme/system.ss @@ -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 \ No newline at end of file