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

a new branch of the whole tree

Browse Source 
svn: r18648
This commit is contained in:
Sam Tobin-Hochstadt 2010-03-27 14:49:58 +00:00
parent 752e93fc88
commit d4e0c16d55
28 changed files with 533 additions and 404 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -1,4 +1,4 @@
#lang typed-scheme #lang typed/scheme/base ;/no-check
(require typed/mred/mred (require typed/mred/mred
typed/framework/framework typed/framework/framework
@ -172,7 +172,7 @@
(max raw-th h))) (max raw-th h)))
(define tmp-color (make-object color%)) (define tmp-color (make-object color%))
(: get-char (Number Number -> Char)) (: get-char (Real Real -> Char))
(define (get-char x y) (define (get-char x y)
(send bdc get-pixel x y tmp-color) (send bdc get-pixel x y tmp-color)
(let ([red (send tmp-color red)]) (let ([red (send tmp-color red)])
@ -185,9 +185,9 @@
(inexact->exact th) (inexact->exact th)
#t)) #t))
(: fetch-line (Number -> String)) (: fetch-line (Real -> String))
(define (fetch-line y) (define (fetch-line y)
(let: loop : String ([x : Number (send bitmap get-width)] (let: loop : String ([x : Real (send bitmap get-width)]
[chars : (Listof Char) null]) [chars : (Listof Char) null])
(cond (cond
[(zero? x) (apply string chars)] [(zero? x) (apply string chars)]

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

@ -9,8 +9,9 @@
base-env-indexing) base-env-indexing)
(typecheck typechecker) (typecheck typechecker)
(rep type-rep filter-rep object-rep) (rep type-rep filter-rep object-rep)
(rename-in (types utils union convenience) (rename-in (types utils union convenience abbrev)
[Un t:Un] [Un t:Un]
[true-filter -true-filter]
[-> t:->]) [-> t:->])
(utils tc-utils utils) (utils tc-utils utils)
unstable/mutated-vars unstable/mutated-vars
@ -137,11 +138,11 @@
(tc-e/t 3 -Pos) (tc-e/t 3 -Pos)
(tc-e/t "foo" -String) (tc-e/t "foo" -String)
(tc-e (+ 3 4) -Pos) (tc-e (+ 3 4) -Pos)
[tc-e/t (lambda: () 3) (t:-> -Pos : (-LFS (list) (list (make-LBot))))] [tc-e/t (lambda: () 3) (t:-> -Pos : -true-filter)]
[tc-e/t (lambda: ([x : Number]) 3) (t:-> N -Pos : (-LFS (list) (list (make-LBot))))] [tc-e/t (lambda: ([x : Number]) 3) (t:-> N -Pos : -true-filter)]
[tc-e/t (lambda: ([x : Number] [y : Boolean]) 3) (t:-> N B -Pos : (-LFS (list) (list (make-LBot))))] [tc-e/t (lambda: ([x : Number] [y : Boolean]) 3) (t:-> N B -Pos : -true-filter)]
[tc-e/t (lambda () 3) (t:-> -Pos : (-LFS (list) (list (make-LBot))))] [tc-e/t (lambda () 3) (t:-> -Pos : -true-filter)]
[tc-e (values 3 4) #:ret (ret (list -Pos -Pos) (list (-FS (list) (list (make-Bot))) (-FS (list) (list (make-Bot)))))] [tc-e (values 3 4) #:ret (ret (list -Pos -Pos) (list -true-filter -true-filter))]
[tc-e (cons 3 4) (-pair -Pos -Pos)] [tc-e (cons 3 4) (-pair -Pos -Pos)]
[tc-e (cons 3 (ann '() : (Listof Integer))) (make-Listof -Integer)] [tc-e (cons 3 (ann '() : (Listof Integer))) (make-Listof -Integer)]
[tc-e (void) -Void] [tc-e (void) -Void]
@ -474,15 +475,15 @@
(t:-> Univ N)] (t:-> Univ N)]
[tc-e/t (let ([p? (lambda: ([x : Any]) (not (number? x)))]) [tc-e/t (let ([p? (lambda: ([x : Any]) (not (number? x)))])
(lambda: ([x : Any]) (if (p? x) 12 (add1 x)))) (lambda: ([x : Any]) (if (p? x) 12 (add1 x))))
(t:-> Univ N : (-LFS null (list (make-LTypeFilter -Number null 0))))] (t:-> Univ N : (-FS -top (-filter -Number #'x)))]
[tc-e/t (let* ([z 1] [tc-e/t (let* ([z 1]
[p? (lambda: ([x : Any]) (number? z))]) [p? (lambda: ([x : Any]) (number? z))])
(lambda: ([x : Any]) (if (p? x) 11 12))) (lambda: ([x : Any]) (if (p? x) 11 12)))
(t:-> Univ -Pos : (-LFS null (list (make-LBot))))] (t:-> Univ -Pos : -true-filter)]
[tc-e/t (let* ([z 1] [tc-e/t (let* ([z 1]
[p? (lambda: ([x : Any]) (number? z))]) [p? (lambda: ([x : Any]) (number? z))])
(lambda: ([x : Any]) (if (p? x) x 12))) (lambda: ([x : Any]) (if (p? x) x 12)))
(t:-> Univ Univ : (-LFS (list (-not-filter (-val #f))) (list (-filter (-val #f)))) : (make-LPath null 0))] (make-pred-ty Univ Univ (-val #f) 0 null)]
[tc-e/t (let* ([z (ann 1 : Any)] [tc-e/t (let* ([z (ann 1 : Any)]
[p? (lambda: ([x : Any]) (not (number? z)))]) [p? (lambda: ([x : Any]) (not (number? z)))])
(lambda: ([x : Any]) (if (p? x) x 12))) (lambda: ([x : Any]) (if (p? x) x 12)))
@ -490,7 +491,7 @@
[tc-e/t (let* ([z 1] [tc-e/t (let* ([z 1]
[p? (lambda: ([x : Any]) (not (number? z)))]) [p? (lambda: ([x : Any]) (not (number? z)))])
(lambda: ([x : Any]) (if (p? x) x 12))) (lambda: ([x : Any]) (if (p? x) x 12)))
(t:-> Univ -Pos : (-LFS null (list (make-LBot))))] (t:-> Univ -Pos : -true-filter)]
[tc-e/t (let* ([z 1] [tc-e/t (let* ([z 1]
[p? (lambda: ([x : Any]) z)]) [p? (lambda: ([x : Any]) z)])
(lambda: ([x : Any]) (if (p? x) x 12))) (lambda: ([x : Any]) (if (p? x) x 12)))
@ -650,19 +651,21 @@
;; instantiating non-dotted terms ;; instantiating non-dotted terms
[tc-e/t (inst (plambda: (a) ([x : a]) x) Integer) [tc-e/t (inst (plambda: (a) ([x : a]) x) Integer)
(make-Function (list (make-arr* (list -Integer) -Integer (make-Function (list (make-arr* (list -Integer) -Integer
#:filters (-LFS (list (-not-filter (-val #f))) (list (-filter (-val #f)))) #:names (list #'x)
#:object (make-LPath null 0))))] #:filters (-FS (-not-filter (-val #f) #'x)
(-filter (-val #f) #'x))
#:object (make-Path null #'x))))]
[tc-e/t (inst (plambda: (a) [x : a *] (apply list x)) Integer) [tc-e/t (inst (plambda: (a) [x : a *] (apply list x)) Integer)
((list) -Integer . ->* . (-lst -Integer))] ((list) -Integer . ->* . (-lst -Integer))]
;; instantiating dotted terms ;; instantiating dotted terms
[tc-e/t (inst (plambda: (a ...) [xs : a ... a] 3) Integer Boolean Integer) [tc-e/t (inst (plambda: (a ...) [xs : a ... a] 3) Integer Boolean Integer)
(-Integer B -Integer . t:-> . -Pos : (-LFS null (list (make-LBot))))] (-Integer B -Integer . t:-> . -Pos : -true-filter)]
[tc-e/t (inst (plambda: (a ...) [xs : (a ... a -> Integer) ... a] 3) Integer Boolean Integer) [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) (-Integer B -Integer . t:-> . -Integer)
(-Integer B -Integer . t:-> . -Integer) (-Integer B -Integer . t:-> . -Integer)
. t:-> . -Pos : (-LFS null (list (make-LBot))))] . t:-> . -Pos : -true-filter)]
[tc-e/t (plambda: (z x y ...) () (inst map z x y ... y)) [tc-e/t (plambda: (z x y ...) () (inst map z x y ... y))
(-polydots (z x y) (t:-> (cl->* (-polydots (z x y) (t:-> (cl->*
@ -722,13 +725,13 @@
(lambda: ([y : (a ... a -> Number)]) (lambda: ([y : (a ... a -> Number)])
(apply y zs)) (apply y zs))
ys))) ys)))
(-polydots (a) ((list) ((list) (a a) . ->... . N) . ->* . ((list) (a a) . ->... . (-lst N)) : (-LFS null (list (make-LBot)))))] (-polydots (a) ((list) ((list) (a a) . ->... . N) . ->* . ((list) (a a) . ->... . (-lst N)) : -true-filter))]
[tc-e/t (plambda: (a ...) [ys : (a ... a -> Number) *] [tc-e/t (plambda: (a ...) [ys : (a ... a -> Number) *]
(lambda: [zs : a ... a] (lambda: [zs : a ... a]
(map (lambda: ([y : (a ... a -> Number)]) (map (lambda: ([y : (a ... a -> Number)])
(apply y zs)) (apply y zs))
ys))) ys)))
(-polydots (a) ((list) ((list) (a a) . ->... . N) . ->* . ((list) (a a) . ->... . (-lst N)) : (-LFS null (list (make-LBot)))))] (-polydots (a) ((list) ((list) (a a) . ->... . N) . ->* . ((list) (a a) . ->... . (-lst N)) : -true-filter))]
[tc-e/t (lambda: ((x : (All (t) t))) [tc-e/t (lambda: ((x : (All (t) t)))
((inst (inst x (All (t) (t -> t))) ((inst (inst x (All (t) (t -> t)))
@ -779,16 +782,16 @@
[user : Number] [user : Number]
[gc : Number]) [gc : Number])
'whatever)) 'whatever))
#:ret (ret (-val 'whatever) (-FS (list) (list (make-Bot))))] #:ret (ret (-val 'whatever) -true-filter)]
[tc-e (let: ([l : (Listof Any) (list 1 2 3)]) [tc-e (let: ([l : (Listof Any) (list 1 2 3)])
(if (andmap number? l) (if (andmap number? l)
(+ 1 (car l)) (+ 1 (car l))
7)) 7))
-Number] -Number]
(tc-e (or (string->number "7") 7) (tc-e (or (string->number "7") 7)
#:ret (ret -Number (-FS (list) (list (make-Bot))))) #:ret (ret -Number -true-filter))
[tc-e (let ([x 1]) (if x x (add1 x))) [tc-e (let ([x 1]) (if x x (add1 x)))
#:ret (ret -Pos (-FS (list) (list (make-Bot))))] #:ret (ret -Pos -true-filter)]
[tc-e (let: ([x : (U (Vectorof Number) String) (vector 1 2 3)]) [tc-e (let: ([x : (U (Vectorof Number) String) (vector 1 2 3)])
(if (vector? x) (vector-ref x 0) (string-length x))) (if (vector? x) (vector-ref x 0) (string-length x)))
-Number] -Number]

13
collects/typed-scheme/env/init-envs.ss vendored
View File

@ -38,8 +38,17 @@
[(Mu-name: n b) `(make-Mu ,(sub n) ,(sub b))] [(Mu-name: n b) `(make-Mu ,(sub n) ,(sub b))]
[(Poly-names: ns b) `(make-Poly (list ,@(map sub ns)) ,(sub b))] [(Poly-names: ns b) `(make-Poly (list ,@(map sub ns)) ,(sub b))]
[(PolyDots-names: ns b) `(make-PolyDots (list ,@(map sub ns)) ,(sub b))] [(PolyDots-names: ns b) `(make-PolyDots (list ,@(map sub ns)) ,(sub b))]
[(? (lambda (e) (or (LatentFilter? e) [(arr: dom rng rest drest kws names)
(LatentObject? e) `(make-arr ,(sub dom) ,(sub rng) ,(sub rest) ,(sub drest) ,(sub kws)
(list ,@(for/list ([i names]) `(quote-syntax ,i))))]
[(TypeFilter: t p i)
`(make-TypeFilter ,(sub t) ,(sub p) (quote-syntax ,i))]
[(NotTypeFilter: t p i)
`(make-NotTypeFilter ,(sub t) ,(sub p) (quote-syntax ,i))]
[(Path: p i)
`(make-Path ,(sub p) (quote-syntax ,i))]
[(? (lambda (e) (or (Filter? e)
(Object? e)
(PathElem? e))) (PathElem? e)))
(app (lambda (v) (vector->list (struct->vector v))) (list-rest tag seq fv fi stx vals))) (app (lambda (v) (vector->list (struct->vector v))) (list-rest tag seq fv fi stx vals)))
`(,(gen-constructor tag) ,@(map sub vals))] `(,(gen-constructor tag) ,@(map sub vals))]

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

@ -4,7 +4,7 @@
"type-environments.ss" "type-environments.ss"
"type-env.ss" "type-env.ss"
unstable/mutated-vars unstable/mutated-vars
(only-in scheme/contract ->* -> or/c any/c) (only-in scheme/contract ->* -> or/c any/c listof cons/c)
(utils tc-utils) (utils tc-utils)
(only-in (rep type-rep) Type/c) (only-in (rep type-rep) Type/c)
(typecheck tc-metafunctions) (typecheck tc-metafunctions)

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

@ -2,7 +2,7 @@
(require scheme/contract (require scheme/contract
(prefix-in r: "../utils/utils.ss") (prefix-in r: "../utils/utils.ss")
scheme/match (r:rep filter-rep rep-utils) unstable/struct scheme/match (r:rep filter-rep rep-utils type-rep) unstable/struct
(except-in (r:utils tc-utils) make-env) (except-in (r:utils tc-utils) make-env)
(r:typecheck tc-metafunctions)) (r:typecheck tc-metafunctions))
@ -49,7 +49,7 @@
;; the environment for types of ... variables ;; the environment for types of ... variables
(define dotted-env (make-parameter (make-empty-env free-identifier=?))) (define dotted-env (make-parameter (make-empty-env free-identifier=?)))
(define/contract (env-map f e) (r:d/c (env-map f e)
((pair? . -> . pair?) env? . -> . env?) ((pair? . -> . pair?) env? . -> . env?)
(make env (env-eq? e) (map f (env-l e)) (env-props e))) (make env (env-eq? e) (map f (env-l e)) (env-props e)))
@ -95,4 +95,4 @@
(syntax-rules () (syntax-rules ()
[(_ i t v . b) (parameterize ([dotted-env (extend/values (list i) (list (cons t v)) (dotted-env))]) . b)])) [(_ i t v . b) (parameterize ([dotted-env (extend/values (list i) (list (cons t v)) (dotted-env))]) . b)]))
(provide/contract [make-empty-env ((-> any/c any/c any/c) . -> . env?)]) (r:p/c [make-empty-env ((-> any/c any/c any/c) . -> . env?)])

50
collects/typed-scheme/infer/infer-unit.ss
View File

@ -1,14 +1,17 @@
#lang scheme/unit #lang scheme/unit
(require "../utils/utils.ss" (require scheme/require
(rep free-variance type-rep filter-rep rep-utils) (except-in
(types convenience union subtype remove-intersect resolve) (path-up
(except-in (utils tc-utils) make-env) "utils/utils.ss" "utils/tc-utils.ss"
(env type-name-env) "rep/free-variance.ss" "rep/type-rep.ss" "rep/filter-rep.ss" "rep/rep-utils.ss"
(except-in (types utils) Dotted) "types/convenience.ss" "types/union.ss" "types/subtype.ss" "types/remove-intersect.ss" "types/resolve.ss"
"env/type-name-env.ss")
make-env)
(except-in (path-up "types/utils.ss") Dotted)
(only-in (path-up "env/type-environments.ss") lookup current-tvars)
"constraint-structs.ss" "constraint-structs.ss"
"signatures.ss" "signatures.ss"
(only-in (env type-environments) lookup current-tvars)
scheme/match scheme/match
mzlib/etc mzlib/etc
mzlib/trace mzlib/trace
@ -101,11 +104,13 @@
(define (cgen/filter V X t s) (define (cgen/filter V X t s)
(match* (t s) (match* (t s)
[(e e) (empty-cset X)] [(e e) (empty-cset X)]
;; FIXME - is there something to be said about LBot? [(e (Top:)) (empty-cset X)]
[((LTypeFilter: t p i) (LTypeFilter: s p i)) (cset-meet (cgen V X t s) (cgen V X s t))] ;; FIXME - is there something to be said about the logical ones?
[((LNotTypeFilter: t p i) (LNotTypeFilter: s p i)) (cset-meet (cgen V X t s) (cgen V X s t))] [((TypeFilter: t p i) (TypeFilter: s p i)) (cset-meet (cgen V X t s) (cgen V X s t))]
[((NotTypeFilter: t p i) (NotTypeFilter: s p i)) (cset-meet (cgen V X t s) (cgen V X s t))]
[(_ _) (fail! t s)])) [(_ _) (fail! t s)]))
#;
(define (cgen/filters V X ts ss) (define (cgen/filters V X ts ss)
(cond (cond
[(null? ss) (empty-cset X)] [(null? ss) (empty-cset X)]
@ -119,14 +124,14 @@
(define (cgen/filter-set V X t s) (define (cgen/filter-set V X t s)
(match* (t s) (match* (t s)
[(e e) (empty-cset X)] [(e e) (empty-cset X)]
[((LFilterSet: t+ t-) (LFilterSet: s+ s-)) [((FilterSet: t+ t-) (FilterSet: s+ s-))
(cset-meet (cgen/filters V X t+ s+) (cgen/filters V X t- s-))] (cset-meet (cgen/filter V X t+ s+) (cgen/filter V X t- s-))]
[(_ _) (fail! t s)])) [(_ _) (fail! t s)]))
(define (cgen/object V X t s) (define (cgen/object V X t s)
(match* (t s) (match* (t s)
[(e e) (empty-cset X)] [(e e) (empty-cset X)]
[(e (LEmpty:)) (empty-cset X)] [(e (Empty:)) (empty-cset X)]
;; FIXME - do something here ;; FIXME - do something here
[(_ _) (fail! t s)])) [(_ _) (fail! t s)]))
@ -153,8 +158,8 @@
[ret-mapping (cg t s)]) [ret-mapping (cg t s)])
(cset-meet* (cset-meet*
(list arg-mapping ret-mapping)))] (list arg-mapping ret-mapping)))]
[((arr: ts t #f (cons dty dbound) '()) [((arr: ts t #f (cons dty dbound) '() names)
(arr: ss s #f #f '())) (arr: ss s #f #f '() names*))
(unless (memq dbound X) (unless (memq dbound X)
(fail! S T)) (fail! S T))
(unless (<= (length ts) (length ss)) (unless (<= (length ts) (length ss))
@ -164,10 +169,11 @@
(gensym dbound))] (gensym dbound))]
[new-tys (for/list ([var vars]) [new-tys (for/list ([var vars])
(substitute (make-F var) dbound dty))] (substitute (make-F var) dbound dty))]
[new-cset (cgen/arr V (append vars X) (make-arr (append ts new-tys) t #f #f null) s-arr)]) [new-names (generate-temporaries new-tys)]
[new-cset (cgen/arr V (append vars X) (make-arr (append ts new-tys) t #f #f null (append names new-names)) s-arr)])
(move-vars-to-dmap new-cset dbound vars))] (move-vars-to-dmap new-cset dbound vars))]
[((arr: ts t #f #f '()) [((arr: ts t #f #f '())
(arr: ss s #f (cons dty dbound) '())) (arr: ss s #f (cons dty dbound) '() names*))
(unless (memq dbound X) (unless (memq dbound X)
(fail! S T)) (fail! S T))
(unless (<= (length ss) (length ts)) (unless (<= (length ss) (length ts))
@ -177,7 +183,8 @@
(gensym dbound))] (gensym dbound))]
[new-tys (for/list ([var vars]) [new-tys (for/list ([var vars])
(substitute (make-F var) dbound dty))] (substitute (make-F var) dbound dty))]
[new-cset (cgen/arr V (append vars X) t-arr (make-arr (append ss new-tys) s #f #f null))]) [new-names (generate-temporaries new-tys)]
[new-cset (cgen/arr V (append vars X) t-arr (make-arr (append ss new-tys) s #f #f null (append names* new-names)))])
(move-vars-to-dmap new-cset dbound vars))] (move-vars-to-dmap new-cset dbound vars))]
[((arr: ts t #f (cons t-dty dbound) '()) [((arr: ts t #f (cons t-dty dbound) '())
(arr: ss s #f (cons s-dty dbound) '())) (arr: ss s #f (cons s-dty dbound) '()))
@ -201,7 +208,7 @@
(cset-meet* (cset-meet*
(list arg-mapping darg-mapping ret-mapping)))] (list arg-mapping darg-mapping ret-mapping)))]
[((arr: ts t t-rest #f '()) [((arr: ts t t-rest #f '())
(arr: ss s #f (cons s-dty dbound) '())) (arr: ss s #f (cons s-dty dbound) '() names*))
(unless (memq dbound X) (unless (memq dbound X)
(fail! S T)) (fail! S T))
(if (<= (length ts) (length ss)) (if (<= (length ts) (length ss))
@ -216,8 +223,9 @@
(gensym dbound))] (gensym dbound))]
[new-tys (for/list ([var vars]) [new-tys (for/list ([var vars])
(substitute (make-F var) dbound s-dty))] (substitute (make-F var) dbound s-dty))]
[new-names (generate-temporaries new-tys)]
[new-cset (cgen/arr V (append vars X) t-arr [new-cset (cgen/arr V (append vars X) t-arr
(make-arr (append ss new-tys) s #f (cons s-dty dbound) null))]) (make-arr (append ss new-tys) s #f (cons s-dty dbound) null (append names* new-names)))])
(move-vars+rest-to-dmap new-cset dbound vars)))] (move-vars+rest-to-dmap new-cset dbound vars)))]
;; If dotted <: starred is correct, add it below. Not sure it is. ;; If dotted <: starred is correct, add it below. Not sure it is.
[((arr: ts t #f (cons t-dty dbound) '()) [((arr: ts t #f (cons t-dty dbound) '())
@ -506,4 +514,4 @@
(define (i s t r) (define (i s t r)
(infer/simple (list s) (list t) r)) (infer/simple (list s) (list t) r))
;(trace subst-gen cgen) ;(trace cgen cgen/arr)

24
collects/typed-scheme/infer/promote-demote.ss
View File

@ -30,9 +30,9 @@
Univ Univ
(make-Hashtable (vp k) v))] (make-Hashtable (vp k) v))]
[#:Param in out [#:Param in out
(make-Param (var-demote in V) (make-Param (var-demote in V)
(vp out))] (vp out))]
[#:arr dom rng rest drest kws [#:arr dom rng rest drest kws names
(cond (cond
[(apply V-in? V (get-filters rng)) [(apply V-in? V (get-filters rng))
(make-top-arr)] (make-top-arr)]
@ -41,7 +41,8 @@
(vp rng) (vp rng)
(var-demote (car drest) V) (var-demote (car drest) V)
#f #f
(for/list ([k kws]) (var-demote k V)))] (for/list ([k kws]) (var-demote k V))
names)]
[else [else
(make-arr (for/list ([d dom]) (var-demote d V)) (make-arr (for/list ([d dom]) (var-demote d V))
(vp rng) (vp rng)
@ -49,7 +50,8 @@
(and drest (and drest
(cons (var-demote (car drest) V) (cons (var-demote (car drest) V)
(cdr drest))) (cdr drest)))
(for/list ([k kws]) (var-demote k V)))])])) (for/list ([k kws]) (var-demote k V))
names)])]))
(define (var-demote T V) (define (var-demote T V)
(define (vd t) (var-demote t V)) (define (vd t) (var-demote t V))
@ -63,9 +65,9 @@
(Un) (Un)
(make-Hashtable (vd k) v))] (make-Hashtable (vd k) v))]
[#:Param in out [#:Param in out
(make-Param (var-promote in V) (make-Param (var-promote in V)
(vd out))] (vd out))]
[#:arr dom rng rest drest kws [#:arr dom rng rest drest kws names
(cond (cond
[(apply V-in? V (get-filters rng)) [(apply V-in? V (get-filters rng))
(make-top-arr)] (make-top-arr)]
@ -74,7 +76,8 @@
(vd rng) (vd rng)
(var-promote (car drest) V) (var-promote (car drest) V)
#f #f
(for/list ([k kws]) (var-demote k V)))] (for/list ([k kws]) (var-demote k V))
names)]
[else [else
(make-arr (for/list ([d dom]) (var-promote d V)) (make-arr (for/list ([d dom]) (var-promote d V))
(vd rng) (vd rng)
@ -82,4 +85,5 @@
(and drest (and drest
(cons (var-promote (car drest) V) (cons (var-promote (car drest) V)
(cdr drest))) (cdr drest)))
(for/list ([k kws]) (var-demote k V)))])])) (for/list ([k kws]) (var-demote k V))
names)])]))

1
collects/typed-scheme/no-check.ss
View File

@ -8,6 +8,7 @@
(all-defined-out) (all-defined-out)
(all-from-out "private/prims.ss")) (all-from-out "private/prims.ss"))
(define-syntax (require/typed stx) (define-syntax (require/typed stx)
(define-syntax-class opt-rename (define-syntax-class opt-rename
#:attributes (nm spec) #:attributes (nm spec)

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

@ -41,15 +41,16 @@
;; numeric predicates ;; numeric predicates
[zero? (make-pred-ty (list N) B -Zero)] [zero? (make-pred-ty (list N) B -Zero)]
[number? (make-pred-ty N)] [number? (make-pred-ty N)]
[integer? (Univ . -> . B : (-LFS (list (-filter (Un -Integer -Flonum))) (list (-not-filter -Integer))))] [integer? (asym-pred (x) Univ B (-FS (-filter (Un -Integer -Flonum) x)
(-not-filter -Integer x)))]
[exact-integer? (make-pred-ty -Integer)] [exact-integer? (make-pred-ty -Integer)]
[real? (make-pred-ty -Real)] [real? (make-pred-ty -Real)]
[inexact-real? (make-pred-ty -Flonum)] [inexact-real? (make-pred-ty -Flonum)]
[complex? (make-pred-ty N)] [complex? (make-pred-ty N)]
[rational? (make-pred-ty -Real)] [rational? (make-pred-ty -Real)]
[exact? (N . -> . B : (-LFS (list) (list (-not-filter -ExactRational))))] [exact? (asym-pred (x) N B (-FS -top (-not-filter -ExactRational x)))]
[inexact? (N . -> . B : (-LFS (list) (list (-not-filter -Flonum))))] [inexact? (asym-pred (x) N B (-FS -top (-not-filter -Flonum x)))]
[fixnum? (Univ . -> . B : (-LFS (list (-filter -Integer)) null))] [fixnum? (asym-pred (x) Univ B (-FS (-filter -Integer x) -top))]
[positive? (-> -Real B)] [positive? (-> -Real B)]
[negative? (-> -Real B)] [negative? (-> -Real B)]
[exact-positive-integer? (make-pred-ty -Pos)] [exact-positive-integer? (make-pred-ty -Pos)]
@ -185,7 +186,6 @@
[unsafe-fllog fl-unop] [unsafe-fllog fl-unop]
[unsafe-flexp fl-unop] [unsafe-flexp fl-unop]
[unsafe-flsqrt fl-unop] [unsafe-flsqrt fl-unop]
[unsafe-fx->fl (-Integer . -> . -Flonum)]
[unsafe-fx+ fx-op] [unsafe-fx+ fx-op]
[unsafe-fx- fx-intop] [unsafe-fx- fx-intop]
@ -262,7 +262,6 @@
[fllog fl-unop] [fllog fl-unop]
[flexp fl-unop] [flexp fl-unop]
[flsqrt fl-unop] [flsqrt fl-unop]
[->fl (-Integer . -> . -Flonum)]
;; safe flvector ops ;; safe flvector ops

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

@ -704,40 +704,3 @@
;; mutable pairs ;; mutable pairs
;; Byte and String Output (Section 12.3 of the Reference)
[write-char (cl-> [(-Char) -Void]
[(-Char -Output-Port) -Void])]
[write-byte (cl-> [(-Nat) -Void]
[(-Nat -Output-Port) -Void])]
[newline (cl-> [() -Void]
[(-Output-Port) -Void])]
[write-string (cl-> [(-String) -Nat]
[(-String -Output-Port) -Nat]
[(-String -Output-Port -Nat) -Nat]
[(-String -Output-Port -Nat -Nat) -Nat])]
[write-bytes (cl-> [(-Bytes) -Nat]
[(-Bytes -Output-Port) -Nat]
[(-Bytes -Output-Port -Nat) -Nat]
[(-Bytes -Output-Port -Nat -Nat) -Nat])]
[write-bytes-avail (cl-> [(-Bytes) -Nat]
[(-Bytes -Output-Port) -Nat]
[(-Bytes -Output-Port -Nat) -Nat]
[(-Bytes -Output-Port -Nat -Nat) -Nat])]
[write-bytes-avail* (cl-> [(-Bytes) (-opt -Nat)]
[(-Bytes -Output-Port) (-opt -Nat)]
[(-Bytes -Output-Port -Nat) (-opt -Nat)]
[(-Bytes -Output-Port -Nat -Nat) (-opt -Nat)])]
[write-bytes-avail/enable-break (cl-> [(-Bytes) -Nat]
[(-Bytes -Output-Port) -Nat]
[(-Bytes -Output-Port -Nat) -Nat]
[(-Bytes -Output-Port -Nat -Nat) -Nat])]
[write-special (cl-> [(Univ) -Boolean]
[(Univ -Output-Port) -Boolean])]
;; Need event type before we can include these
;;write-special-avail*
;;write-bytes-avail-evt
;;write-special-evt
[port-writes-atomic? (-Output-Port . -> . -Boolean)]
[port-writes-special? (-Output-Port . -> . -Boolean)]

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

@ -68,7 +68,7 @@
(define-values (dom* opt-dom* rngs* rst) (define-values (dom* opt-dom* rngs* rst)
(match a (match a
;; functions with no filters or objects ;; functions with no filters or objects
[(arr: dom (Values: (list (Result: rngs (LFilterSet: '() '()) (LEmpty:)) ...)) rst #f kws) [(arr: dom (Values: (list (Result: rngs (FilterSet: (Top:) (Top:)) (Empty:)) ...)) rst #f kws)
(let-values ([(mand-kws opt-kws) (partition (match-lambda [(Keyword: _ _ mand?) mand?]) kws)] (let-values ([(mand-kws opt-kws) (partition (match-lambda [(Keyword: _ _ mand?) mand?]) kws)]
[(conv) (match-lambda [(Keyword: kw kty _) (list kw (t->c/neg kty))])]) [(conv) (match-lambda [(Keyword: kw kty _) (list kw (t->c/neg kty))])])
(values (append (map t->c/neg dom) (append-map conv mand-kws)) (values (append (map t->c/neg dom) (append-map conv mand-kws))

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

@ -9,15 +9,22 @@
(λ (e) (λ (e)
(and (Filter? e) (not (NoFilter? e)) (not (FilterSet? e)))))) (and (Filter? e) (not (NoFilter? e)) (not (FilterSet? e))))))
(define LatentFilter/c (define FilterSet/c
(flat-named-contract
'FilterSet
(λ (e) (or (FilterSet? e) (NoFilter? e)))))
#;(define LatentFilter/c
(flat-named-contract (flat-named-contract
'LatentFilter 'LatentFilter
(λ (e) (λ (e)
(and (LatentFilter? e) (not (LFilterSet? e)))))) (and (LatentFilter? e) (not (LFilterSet? e))))))
(provide Filter/c LatentFilter/c FilterSet/c LatentFilterSet/c index/c) (provide Filter/c FilterSet/c); LatentFilter/c LatentFilterSet/c index/c)
(df Bot () [#:fold-rhs #:base]) (df Bot () [#:fold-rhs #:base])
(df Top () [#:fold-rhs #:base])
(df TypeFilter ([t Type?] [p (listof PathElem?)] [v identifier?]) (df TypeFilter ([t Type?] [p (listof PathElem?)] [v identifier?])
[#:intern (list t p (hash-id v))] [#:intern (list t p (hash-id v))]
@ -32,24 +39,29 @@
[#:fold-rhs (*NotTypeFilter (type-rec-id t) (map pathelem-rec-id p) v)]) [#:fold-rhs (*NotTypeFilter (type-rec-id t) (map pathelem-rec-id p) v)])
;; implication ;; implication
(df ImpFilter ([a (non-empty-listof Filter/c)] [c (non-empty-listof Filter/c)]) (df ImpFilter ([a Filter/c] [c Filter/c]))
[#:frees (combine-frees (map free-vars* (append a c)))
(combine-frees (map free-idxs* (append a c)))]) (df AndFilter ([fs (non-empty-listof Filter/c)])
[#:fold-rhs (*AndFilter (map filter-rec-id fs))]
[#:frees (combine-frees (map free-vars* fs))
(combine-frees (map free-idxs* fs))])
(df OrFilter ([fs (non-empty-listof Filter/c)])
[#:fold-rhs (*OrFilter (map filter-rec-id fs))]
[#:frees (combine-frees (map free-vars* fs))
(combine-frees (map free-idxs* fs))])
(df FilterSet (thn els) (df FilterSet (thn els)
[#:frees (combine-frees (map free-vars* (append thn els))) [#:contract (->d ([t (cond [(Bot? t)
(combine-frees (map free-idxs* (append thn els)))] Bot?]
[#:fold-rhs (*FilterSet (map filter-rec-id thn) (map filter-rec-id els))] [(Bot? e)
[#:contract (->d ([t (cond [(ormap Bot? t) Top?]
(list/c Bot?)] [else Filter/c])]
[(ormap Bot? e) [e (cond [(Bot? e)
(flat-named-contract "e was Bot" (list/c))] Bot?]
[else (listof Filter/c)])] [(Bot? t)
[e (cond [(ormap Bot? e) Top?]
(list/c Bot?)] [else Filter/c])])
[(ormap Bot? t)
(flat-named-contract "t was Bot" (list/c))]
[else (listof Filter/c)])])
(#:syntax [stx #f]) (#:syntax [stx #f])
[result FilterSet?])]) [result FilterSet?])])
@ -57,6 +69,7 @@
;; should only be used for parsing type annotations and expected types ;; should only be used for parsing type annotations and expected types
(df NoFilter () [#:fold-rhs #:base]) (df NoFilter () [#:fold-rhs #:base])
#|
(define index/c (or/c natural-number/c keyword?)) (define index/c (or/c natural-number/c keyword?))
(dlf LBot () [#:fold-rhs #:base]) (dlf LBot () [#:fold-rhs #:base])
@ -69,6 +82,8 @@
[#:frees (lambda (frees*) (combine-frees (map (compose make-invariant frees*) (cons t p))))] [#:frees (lambda (frees*) (combine-frees (map (compose make-invariant frees*) (cons t p))))]
[#:fold-rhs (*LNotTypeFilter (type-rec-id t) (map pathelem-rec-id p) idx)]) [#:fold-rhs (*LNotTypeFilter (type-rec-id t) (map pathelem-rec-id p) idx)])
;; implication ;; implication
(dlf LImpFilter ([a (non-empty-listof LatentFilter/c)] [c (non-empty-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))) [#:frees (combine-frees (map free-vars* (append a c)))
@ -92,15 +107,11 @@
(#:syntax [stx #f]) (#:syntax [stx #f])
[result LFilterSet?])]) [result LFilterSet?])])
(define FilterSet/c
(flat-named-contract
'FilterSet
(λ (e) (or (FilterSet? e) (NoFilter? e)))))
(define LatentFilterSet/c (define LatentFilterSet/c
(flat-named-contract (flat-named-contract
'LatentFilterSet 'LatentFilterSet
(λ (e) (or (LFilterSet? e))))) (λ (e) (or (LFilterSet? e)))))
|#
(define filter-equal? eq?) (define (filter-equal? a b) (= (Rep-seq a) (Rep-seq b)))
(provide filter-equal?) (provide filter-equal?)

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

@ -1,6 +1,7 @@
#lang scheme/base #lang scheme/base
(require scheme/match scheme/contract "rep-utils.ss" "free-variance.ss" "filter-rep.ss") (require scheme/match scheme/contract "rep-utils.ss" "free-variance.ss" "filter-rep.ss")
(provide object-equal?)
(dpe CarPE () [#:fold-rhs #:base]) (dpe CarPE () [#:fold-rhs #:base])
(dpe CdrPE () [#:fold-rhs #:base]) (dpe CdrPE () [#:fold-rhs #:base])
@ -16,12 +17,16 @@
[#:frees (combine-frees (map free-vars* p)) (combine-frees (map free-idxs* p))] [#:frees (combine-frees (map free-vars* p)) (combine-frees (map free-idxs* p))]
[#:fold-rhs (*Path (map pathelem-rec-id p) v)]) [#:fold-rhs (*Path (map pathelem-rec-id p) v)])
;; represents no info about the filters of this expression ;; represents no info about the object of this expression
;; should only be used for parsing type annotations and expected types ;; should only be used for parsing type annotations and expected types
(do NoObject () [#:fold-rhs #:base]) (do NoObject () [#:fold-rhs #:base])
(define (object-equal? o1 o2) (= (Rep-seq o1) (Rep-seq o2)))
#|
(dlo LEmpty () [#:fold-rhs #:base]) (dlo LEmpty () [#:fold-rhs #:base])
(dlo LPath ([p (listof PathElem?)] [idx index/c]) (dlo LPath ([p (listof PathElem?)] [idx index/c])
[#:frees (combine-frees (map free-vars* p)) (combine-frees (map free-idxs* p))] [#:frees (combine-frees (map free-vars* p)) (combine-frees (map free-idxs* p))]
[#:fold-rhs (*LPath (map pathelem-rec-id p) idx)]) [#:fold-rhs (*LPath (map pathelem-rec-id p) idx)])
|#

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

@ -5,7 +5,7 @@
"rep-utils.ss" "object-rep.ss" "filter-rep.ss" "free-variance.ss" "rep-utils.ss" "object-rep.ss" "filter-rep.ss" "free-variance.ss"
mzlib/trace scheme/match mzlib/trace scheme/match
scheme/contract scheme/contract
(for-syntax scheme/base)) (for-syntax scheme/base syntax/parse))
(define name-table (make-weak-hasheq)) (define name-table (make-weak-hasheq))
@ -132,9 +132,9 @@
[#:frees (λ (f) (f ty))] [#:frees (λ (f) (f ty))]
[#:fold-rhs (*Keyword kw (type-rec-id ty) required?)]) [#:fold-rhs (*Keyword kw (type-rec-id ty) required?)])
(dt Result ([t Type/c] [f LFilterSet?] [o LatentObject?]) (dt Result ([t Type/c] [f FilterSet?] [o Object?])
[#:frees (λ (frees) (combine-frees (map frees (list t f o))))] [#:frees (λ (frees) (combine-frees (map frees (list t f o))))]
[#:fold-rhs (*Result (type-rec-id t) (latentfilter-rec-id f) (latentobject-rec-id o))]) [#:fold-rhs (*Result (type-rec-id t) (filter-rec-id f) (object-rec-id o))])
;; types : Listof[Type] ;; types : Listof[Type]
(dt Values ([rs (listof Result?)]) (dt Values ([rs (listof Result?)])
@ -150,7 +150,11 @@
[rng (or/c Values? ValuesDots?)] [rng (or/c Values? ValuesDots?)]
[rest (or/c #f Type/c)] [rest (or/c #f Type/c)]
[drest (or/c #f (cons/c Type/c (or/c natural-number/c symbol?)))] [drest (or/c #f (cons/c Type/c (or/c natural-number/c symbol?)))]
[kws (listof Keyword?)]) [kws (listof Keyword?)]
;; order is: fixed, rest/drest, keywords
[names (listof identifier?)])
#:no-provide
[#:intern (list dom rng rest drest kws (map hash-id names))]
[#:frees (combine-frees [#:frees (combine-frees
(append (map (compose flip-variances free-vars*) (append (map (compose flip-variances free-vars*)
(append (if rest (list rest) null) (append (if rest (list rest) null)
@ -179,7 +183,8 @@
(type-rec-id rng) (type-rec-id rng)
(and rest (type-rec-id rest)) (and rest (type-rec-id rest))
(and drest (cons (type-rec-id (car drest)) (cdr drest))) (and drest (cons (type-rec-id (car drest)) (cdr drest)))
(map type-rec-id kws))]) (map type-rec-id kws)
names)])
;; top-arr is the supertype of all function types ;; top-arr is the supertype of all function types
(dt top-arr () [#:fold-rhs #:base]) (dt top-arr () [#:fold-rhs #:base])
@ -396,7 +401,7 @@
;; necessary to avoid infinite loops ;; necessary to avoid infinite loops
[#:Union elems (*Union (remove-dups (sort (map sb elems) type<?)))] [#:Union elems (*Union (remove-dups (sort (map sb elems) type<?)))]
;; functions ;; functions
[#:arr dom rng rest drest kws [#:arr dom rng rest drest kws names
(*arr (map sb dom) (*arr (map sb dom)
(sb rng) (sb rng)
(if rest (sb rest) #f) (if rest (sb rest) #f)
@ -404,7 +409,8 @@
(cons (sb (car drest)) (cons (sb (car drest))
(if (eq? (cdr drest) name) (+ count outer) (cdr drest))) (if (eq? (cdr drest) name) (+ count outer) (cdr drest)))
#f) #f)
(map sb kws))] (map sb kws)
names)]
[#:ValuesDots rs dty dbound [#:ValuesDots rs dty dbound
(*ValuesDots (map sb rs) (*ValuesDots (map sb rs)
(sb dty) (sb dty)
@ -441,7 +447,7 @@
;; necessary to avoid infinite loops ;; necessary to avoid infinite loops
[#:Union elems (*Union (remove-dups (sort (map sb elems) type<?)))] [#:Union elems (*Union (remove-dups (sort (map sb elems) type<?)))]
;; functions ;; functions
[#:arr dom rng rest drest kws [#:arr dom rng rest drest kws names
(*arr (map sb dom) (*arr (map sb dom)
(sb rng) (sb rng)
(if rest (sb rest) #f) (if rest (sb rest) #f)
@ -449,7 +455,8 @@
(cons (sb (car drest)) (cons (sb (car drest))
(if (eqv? (cdr drest) (+ count outer)) (F-n image) (cdr drest))) (if (eqv? (cdr drest) (+ count outer)) (F-n image) (cdr drest)))
#f) #f)
(map sb kws))] (map sb kws)
names)]
[#:ValuesDots rs dty dbound [#:ValuesDots rs dty dbound
(*ValuesDots (map sb rs) (*ValuesDots (map sb rs)
(sb dty) (sb dty)
@ -604,6 +611,13 @@
(list syms (PolyDots-body* syms t)))) (list syms (PolyDots-body* syms t))))
(list nps bp)))]))) (list nps bp)))])))
(define-match-expander arr:*
(lambda (stx)
(syntax-parse stx
[(_ dom rng rest drest kws names)
(syntax/loc stx (arr: dom rng rest drest kws names))]
[(_ dom rng rest drest kws)
(syntax/loc stx (arr: dom rng rest drest kws _))])))
;(trace subst subst-all) ;(trace subst subst-all)
(provide (provide
@ -614,6 +628,7 @@
PolyDots-unsafe: PolyDots-unsafe:
Mu? Poly? PolyDots? Mu? Poly? PolyDots?
arr arr
arr?
Type? Filter? LatentFilter? Object? LatentObject? Type? Filter? LatentFilter? Object? LatentObject?
Type/c Type/c
Poly-n Poly-n
@ -631,7 +646,9 @@
[PolyDots* make-PolyDots] [PolyDots* make-PolyDots]
[Mu-body* Mu-body] [Mu-body* Mu-body]
[Poly-body* Poly-body] [Poly-body* Poly-body]
[PolyDots-body* PolyDots-body])) [PolyDots-body* PolyDots-body]
[*arr make-arr]
[arr:* arr:]))
(p/c [type-equal? (Rep? Rep? . -> . boolean?)]) (p/c [type-equal? (Rep? Rep? . -> . boolean?)])

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

@ -52,36 +52,24 @@
(alt equal? equal?-able))) (alt equal? equal?-able)))
(match* ((single-value v1) (single-value v2)) (match* ((single-value v1) (single-value v2))
[((tc-result1: t _ o) (tc-result1: (Value: (? ok? val)))) [((tc-result1: t _ o) (tc-result1: (Value: (? ok? val))))
(ret -Boolean (apply-filter (make-LFilterSet (list (make-LTypeFilter (-val val) null 0)) (list (make-LNotTypeFilter (-val val) null 0))) t o))] (ret -Boolean
(-FS (-filter-at (-val val) o)
(-not-filter-at (-val val) o)))]
[((tc-result1: (Value: (? ok? val))) (tc-result1: t _ o)) [((tc-result1: (Value: (? ok? val))) (tc-result1: t _ o))
(ret -Boolean (apply-filter (make-LFilterSet (list (make-LTypeFilter (-val val) null 0)) (list (make-LNotTypeFilter (-val val) null 0))) t o))] (ret -Boolean
(-FS (-filter-at (-val val) o)
(-not-filter-at (-val val) o)))]
[((tc-result1: t _ o) [((tc-result1: t _ o)
(and (? (lambda _ (free-identifier=? #'member comparator))) (or (and (? (lambda _ (free-identifier=? #'member comparator)))
(tc-result1: (app untuple (list (and ts (Value: _)) ...))))) (tc-result1: (app untuple (list (and ts (Value: _)) ...))))
(and (? (lambda _ (free-identifier=? #'memv comparator)))
(tc-result1: (app untuple (list (and ts (Value: (? eqv?-able))) ...))))
(and (? (lambda _ (free-identifier=? #'memq comparator)))
(tc-result1: (app untuple (list (and ts (Value: (? eq?-able))) ...))))))
(let ([ty (apply Un ts)]) (let ([ty (apply Un ts)])
(ret (Un (-val #f) t) (ret (Un (-val #f) t)
(apply-filter (-FS (-filter-at ty o)
(make-LFilterSet (list (make-LTypeFilter ty null 0)) (-not-filter-at ty o))))]
(list (make-LNotTypeFilter ty null 0)))
t o)))]
[((tc-result1: t _ o)
(and (? (lambda _ (free-identifier=? #'memv comparator)))
(tc-result1: (app untuple (list (and ts (Value: (? eqv?-able))) ...)))))
(let ([ty (apply Un ts)])
(ret (Un (-val #f) t)
(apply-filter
(make-LFilterSet (list (make-LTypeFilter ty null 0))
(list (make-LNotTypeFilter ty null 0)))
t o)))]
[((tc-result1: t _ o)
(and (? (lambda _ (free-identifier=? #'memq comparator)))
(tc-result1: (app untuple (list (and ts (Value: (? eq?-able))) ...)))))
(let ([ty (apply Un ts)])
(ret (Un (-val #f) t)
(apply-filter
(make-LFilterSet (list (make-LTypeFilter ty null 0))
(list (make-LNotTypeFilter ty null 0)))
t o)))]
[(_ _) (ret -Boolean)])) [(_ _) (ret -Boolean)]))
@ -609,7 +597,7 @@
(= (length d) (= (length d)
(length (syntax->list #'args)))) (length (syntax->list #'args))))
dom) dom)
(Values: (list (Result: v (LFilterSet: '() '()) (LEmpty:)))) (Values: (list (Result: v (FilterSet: (Top:) (Top:)) (Empty:))))
#f #f (list (Keyword: _ _ #f) ...))))))) #f #f (list (Keyword: _ _ #f) ...)))))))
;(printf "f dom: ~a ~a~n" (syntax->datum #'f) dom) ;(printf "f dom: ~a ~a~n" (syntax->datum #'f) dom)
(let ([arg-tys (map (lambda (a t) (tc-expr/check a (ret t))) (let ([arg-tys (map (lambda (a t) (tc-expr/check a (ret t)))
@ -740,10 +728,13 @@
;; syntax? syntax? arr? (listof tc-results?) (or/c #f tc-results) [boolean?] -> tc-results? ;; syntax? syntax? arr? (listof tc-results?) (or/c #f tc-results) [boolean?] -> tc-results?
(define (tc/funapp1 f-stx args-stx ftype0 argtys expected #:check [check? #t]) (define (tc/funapp1 f-stx args-stx ftype0 argtys expected #:check [check? #t])
;(printf "got to here 0~a~n" args-stx)
(match* (ftype0 argtys) (match* (ftype0 argtys)
;; we check that all kw args are optional ;; we check that all kw args are optional
[((arr: dom (Values: (list (Result: t-r lf-r lo-r) ...)) rest #f (list (Keyword: _ _ #f) ...)) [((arr: dom (Values: (list (Result: t-r f-r o-r) ...)) rest #f (list (Keyword: _ _ #f) ...)
names)
(list (tc-result1: t-a phi-a o-a) ...)) (list (tc-result1: t-a phi-a o-a) ...))
;(printf "got to here 1~a~n" args-stx)
(when check? (when check?
(cond [(and (not rest) (not (= (length dom) (length t-a)))) (cond [(and (not rest) (not (= (length dom) (length t-a))))
(tc-error/expr #:return (ret t-r) (tc-error/expr #:return (ret t-r)
@ -751,26 +742,27 @@
[(and rest (< (length t-a) (length dom))) [(and rest (< (length t-a) (length dom)))
(tc-error/expr #:return (ret t-r) (tc-error/expr #:return (ret t-r)
"Wrong number of arguments, expected at least ~a and got ~a" (length dom) (length t-a))]) "Wrong number of arguments, expected at least ~a and got ~a" (length dom) (length t-a))])
(for ([dom-t (if rest (in-sequence-forever dom rest) (in-list dom))] [a (syntax->list args-stx)] [arg-t (in-list t-a)]) (for ([dom-t (if rest (in-sequence-forever dom rest) (in-list dom))]
[a (in-list (syntax->list args-stx))]
[arg-t (in-list t-a)])
(parameterize ([current-orig-stx a]) (check-below arg-t dom-t)))) (parameterize ([current-orig-stx a]) (check-below arg-t dom-t))))
(let* (;; Listof[Listof[LFilterSet]] ;(printf "got to here 2 ~a ~a ~a ~n" dom names o-a)
[lfs-f (for/list ([lf lf-r]) (let-values ([(names o-a)
(for/list ([i (in-indexes dom)]) (for/lists (n o) ([d (in-list dom)]
(split-lfilters lf i)))] [nm (in-list names)]
;; Listof[FilterSet] [oa (in-list o-a)])
[f-r (for/list ([lfs lfs-f]) (values nm oa))])
(merge-filter-sets ;(printf "got to here 3~a~n" args-stx)
(for/list ([lf lfs] [t t-a] [o o-a]) (let* (;; Listof[FilterSet]
(apply-filter lf t o))))] [f-r (for/list ([f f-r])
;; Listof[Object] (apply-filter f names o-a))]
[o-r (for/list ([lo lo-r]) ;; Listof[Object]
(match lo [o-r (for/list ([o o-r])
[(LPath: pi* i) (apply-object o names o-a))]
(match (object-index o-a i) ;; Listof[Type]
[(Path: pi x) (make-Path (append pi* pi) x)] [t-r (for/list ([t t-r])
[_ (make-Empty)])] (apply-type t names o-a))])
[_ (make-Empty)]))]) (ret t-r f-r o-r)))]
(ret t-r f-r o-r))]
[((arr: _ _ _ drest '()) _) [((arr: _ _ _ drest '()) _)
(int-err "funapp with drest args NYI")] (int-err "funapp with drest args NYI")]
[((arr: _ _ _ _ kws) _) [((arr: _ _ _ _ kws) _)

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

@ -15,8 +15,6 @@
(typecheck tc-metafunctions) (typecheck tc-metafunctions)
(for-syntax scheme/base)) (for-syntax scheme/base))
(provide env+)
(define (replace-nth l i f) (define (replace-nth l i f)
(cond [(null? l) (error 'replace-nth "list not long enough" l i f)] (cond [(null? l) (error 'replace-nth "list not long enough" l i f)]
[(zero? i) (cons (f (car l)) (cdr l))] [(zero? i) (cons (f (car l)) (cdr l))]
@ -75,3 +73,5 @@
(set-box! flag #f)) (set-box! flag #f))
new-t)) new-t))
x Γ)]))) x Γ)])))
(p/c [env+ (env? (listof Filter/c) (box/c #t). -> . env?)])

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

@ -135,8 +135,8 @@
(define (tc-id id) (define (tc-id id)
(let* ([ty (lookup-type/lexical id)]) (let* ([ty (lookup-type/lexical id)])
(ret ty (ret ty
(make-FilterSet (list (make-NotTypeFilter (-val #f) null id)) (make-FilterSet (make-NotTypeFilter (-val #f) null id)
(list (make-TypeFilter (-val #f) null id))) (make-TypeFilter (-val #f) null id))
(make-Path null id)))) (make-Path null id))))
;; typecheck an expression, but throw away the effect ;; typecheck an expression, but throw away the effect
@ -174,7 +174,7 @@
(if (= (length ts) (length ts2)) (if (= (length ts) (length ts2))
(ret ts2 fs os) (ret ts2 fs os)
(ret ts2))] (ret ts2))]
[((tc-result1: t1 f1 o1) (tc-result1: t2 (FilterSet: (list) (list)) (Empty:))) [((tc-result1: t1 f1 o1) (tc-result1: t2 (FilterSet: (Top:) (Top:)) (Empty:)))
(cond (cond
[(not (subtype t1 t2)) [(not (subtype t1 t2))
(tc-error/expr "Expected ~a, but got ~a" t2 t1)]) (tc-error/expr "Expected ~a, but got ~a" t2 t1)])
@ -183,6 +183,9 @@
(cond (cond
[(not (subtype t1 t2)) [(not (subtype t1 t2))
(tc-error/expr "Expected ~a, but got ~a" t2 t1)] (tc-error/expr "Expected ~a, but got ~a" t2 t1)]
[(and (not (filter-equal? f1 f2))
(object-equal? o1 o2))
(tc-error/expr "Expected result with filter ~a, got filter ~a" f2 f1)]
[(not (and (equal? f1 f2) (equal? o1 o2))) [(not (and (equal? f1 f2) (equal? o1 o2)))
(tc-error/expr "Expected result with filter ~a and ~a, got filter ~a and ~a" f2 (print-object o2) f1 (print-object o1))]) (tc-error/expr "Expected result with filter ~a and ~a, got filter ~a and ~a" f2 (print-object o2) f1 (print-object o1))])
expected] expected]
@ -254,6 +257,7 @@
(add-typeof-expr form t) (add-typeof-expr form t)
t)])))) t)]))))
#;
(define (tc-or e1 e2 or-part [expected #f]) (define (tc-or e1 e2 or-part [expected #f])
(match (single-value e1) (match (single-value e1)
[(tc-result1: t1 (and f1 (FilterSet: fs+ fs-)) o1) [(tc-result1: t1 (and f1 (FilterSet: fs+ fs-)) o1)
@ -346,13 +350,6 @@
(let-values (((_ _) (#%plain-app find-method/who _ rcvr _))) (let-values (((_ _) (#%plain-app find-method/who _ rcvr _)))
(#%plain-app _ _ args ...))) (#%plain-app _ _ args ...)))
(tc/send #'rcvr #'meth #'(args ...) expected)] (tc/send #'rcvr #'meth #'(args ...) expected)]
;; or
[(let-values ([(or-part) e1]) (if op1 op2 e2))
(and
(identifier? #'op1) (identifier? #'op2)
(free-identifier=? #'or-part #'op1)
(free-identifier=? #'or-part #'op2))
(tc-or #'e1 #'e2 #'or-part expected)]
;; let ;; let
[(let-values ([(name ...) expr] ...) . body) [(let-values ([(name ...) expr] ...) . body)
(tc/let-values #'((name ...) ...) #'(expr ...) #'body form expected)] (tc/let-values #'((name ...) ...) #'(expr ...) #'body form expected)]
@ -415,12 +412,6 @@
(let-values (((_ _) (#%plain-app find-method/who _ rcvr _))) (let-values (((_ _) (#%plain-app find-method/who _ rcvr _)))
(#%plain-app _ _ args ...))) (#%plain-app _ _ args ...)))
(tc/send #'rcvr #'meth #'(args ...))] (tc/send #'rcvr #'meth #'(args ...))]
;; or
[(let-values ([(or-part) e1]) (if op1 op2 e2))
(and (identifier? #'op1) (identifier? #'op2)
(free-identifier=? #'or-part #'op1)
(free-identifier=? #'or-part #'op2))
(tc-or #'e1 #'e2 #'or-part)]
;; let ;; let
[(let-values ([(name ...) expr] ...) . body) [(let-values ([(name ...) expr] ...) . body)
(tc/let-values #'((name ...) ...) #'(expr ...) #'body form)] (tc/let-values #'((name ...) ...) #'(expr ...) #'body form)]

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

@ -4,14 +4,14 @@
(require (rename-in "../utils/utils.ss" [infer r:infer])) (require (rename-in "../utils/utils.ss" [infer r:infer]))
(require "signatures.ss" (require "signatures.ss"
(rep type-rep filter-rep object-rep) (rep type-rep filter-rep object-rep)
(rename-in (types convenience subtype union utils comparison remove-intersect) (rename-in (types convenience subtype union utils comparison remove-intersect abbrev)
[remove *remove]) [remove *remove])
(env lexical-env type-environments) (env lexical-env type-environments)
(r:infer infer) (r:infer infer)
(utils tc-utils) (utils tc-utils)
(typecheck tc-envops tc-metafunctions) (typecheck tc-envops tc-metafunctions)
syntax/kerncase syntax/kerncase
mzlib/trace mzlib/trace unstable/debug
scheme/match) scheme/match)
;; if typechecking ;; if typechecking
@ -43,18 +43,27 @@
[(tc-result1: _ (and f1 (FilterSet: fs+ fs-)) _) [(tc-result1: _ (and f1 (FilterSet: fs+ fs-)) _)
(let*-values ([(flag+ flag-) (values (box #t) (box #t))] (let*-values ([(flag+ flag-) (values (box #t) (box #t))]
[(derived-imps+ derived-atoms+) [(derived-imps+ derived-atoms+)
(combine-props fs+ (env-props (lexical-env)))]) (combine-props (list fs+) (env-props (lexical-env)))])
(match-let* ([(tc-results: ts fs2 os2) (with-lexical-env (env+ (lexical-env) fs+ flag+) (tc thn (unbox flag+)))] (match-let* ([(tc-results: ts fs2 os2) (with-lexical-env (env+ (lexical-env) (list fs+) flag+) (tc thn (unbox flag+)))]
[(tc-results: us fs3 os3) (with-lexical-env (env+ (lexical-env) fs- flag-) (tc els (unbox flag-)))]) [(tc-results: us fs3 os3) (with-lexical-env (env+ (lexical-env) (list fs-) flag-) (tc els (unbox flag-)))])
;; if we have the same number of values in both cases ;; if we have the same number of values in both cases
(cond [(= (length ts) (length us)) (cond [(= (length ts) (length us))
(let ([r (let ([r (combine-results
(combine-results (for/list ([f2 fs2] [f3 fs3] [t2 ts] [t3 us] [o2 os2] [o3 os3])
(for/list ([t ts] [u us] [o2 os2] [o3 os3] [f2 fs2] [f3 fs3]) (let ([filter
(combine-filter f1 f2 f3 t u o2 o3)))]) (match* (f2 f3)
(if expected [((NoFilter:) _)
(check-below r expected) (-FS -top -top)]
r))] [(_ (NoFilter:))
(-FS -top -top)]
[((FilterSet: f2+ f2-) (FilterSet: f3+ f3-))
(-FS (-or (-and fs+ f2+) (-and fs- f3+))
(-or (-and fs+ f2-) (-and fs- f3-)))])]
[type (Un t2 t3)]
[object (if (object-equal? o2 o3) o2 (make-Empty))])
;(printf "result filter is: ~a\n" filter)
(ret type filter object))))])
(if expected (check-below r expected) r))]
;; special case if one of the branches is unreachable ;; special case if one of the branches is unreachable
[(and (= 1 (length us)) (type-equal? (car us) (Un))) [(and (= 1 (length us)) (type-equal? (car us) (Un)))
(if expected (check-below (ret ts fs2 os2) expected) (ret ts fs2 os2))] (if expected (check-below (ret ts fs2 os2) expected) (ret ts fs2 os2))]
@ -63,7 +72,7 @@
;; otherwise, error ;; otherwise, error
[else [else
(tc-error/expr #:return (ret (or expected Err)) (tc-error/expr #:return (ret (or expected Err))
"Expected the same number of values from both branches of if expression, but got ~a and ~a" "Expected the same number of values from both branches of `if' expression, but got ~a and ~a"
(length ts) (length us))])))] (length ts) (length us))])))]
[(tc-results: t _ _) [(tc-results: t _ _)
(tc-error/expr #:return (ret (or expected Err)) (tc-error/expr #:return (ret (or expected Err))

9
collects/typed-scheme/typecheck/tc-lambda-unit.ss
View File

@ -14,7 +14,8 @@
(types abbrev utils) (types abbrev utils)
(env type-environments lexical-env) (env type-environments lexical-env)
(utils tc-utils) (utils tc-utils)
mzlib/plt-match) unstable/debug
scheme/match)
(require (for-template scheme/base "internal-forms.ss")) (require (for-template scheme/base "internal-forms.ss"))
(import tc-expr^) (import tc-expr^)
@ -32,9 +33,7 @@
[(struct lam-result ((list (list arg-ids arg-tys) ...) (list (list kw kw-id kw-ty req?) ...) rest drest body)) [(struct lam-result ((list (list arg-ids arg-tys) ...) (list (list kw kw-id kw-ty req?) ...) rest drest body))
(make-arr (make-arr
arg-tys arg-tys
(abstract-filters (append (for/list ([i (in-naturals)] [_ arg-ids]) i) kw) (abstract-filters body)
(append arg-ids kw-id)
body)
#:kws (map make-Keyword kw kw-ty req?) #:kws (map make-Keyword kw kw-ty req?)
#:rest rest #:rest rest
#:drest drest)])) #:drest drest)]))
@ -200,7 +199,7 @@
[(tc-result1: (Function: (list (arr: argss rets rests drests '()) ...))) [(tc-result1: (Function: (list (arr: argss rets rests drests '()) ...)))
(for/list ([args argss] [ret rets] [rest rests] [drest drests]) (for/list ([args argss] [ret rets] [rest rests] [drest drests])
(tc/lambda-clause/check (car (syntax->list formals)) (car (syntax->list bodies)) (tc/lambda-clause/check (car (syntax->list formals)) (car (syntax->list bodies))
args (values->tc-results ret (formals->list (car (syntax->list formals)))) rest drest))] args (values->tc-results ret) rest drest))]
[_ (go (syntax->list formals) (syntax->list bodies) null null null)]))] [_ (go (syntax->list formals) (syntax->list bodies) null null null)]))]
;; otherwise ;; otherwise
[else (go (syntax->list formals) (syntax->list bodies) null null null)])) [else (go (syntax->list formals) (syntax->list bodies) null null null)]))

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

@ -5,14 +5,18 @@
[-> -->] [-> -->]
[->* -->*] [->* -->*]
[one-of/c -one-of/c]) [one-of/c -one-of/c])
(rep type-rep filter-rep) scheme/list (rep type-rep filter-rep rep-utils) scheme/list
scheme/contract scheme/match unstable/match scheme/contract scheme/match unstable/match
(for-syntax scheme/base)) (for-syntax scheme/base))
(provide combine-filter apply-filter abstract-filter abstract-filters combine-props ;(provide (all-defined-out))
split-lfilters merge-filter-sets values->tc-results tc-results->values)
(define-syntax-rule (d/c/p (name . args) c . body)
(begin (d/c (name . args) c . body)
(p/c [name c])))
;; this implements the sequence invariant described on the first page relating to Bot ;; this implements the sequence invariant described on the first page relating to Bot
#;
(define (lcombine l1 l2) (define (lcombine l1 l2)
(cond [(memq (make-LBot) l1) (cond [(memq (make-LBot) l1)
(make-LFilterSet (list (make-LBot)) null)] (make-LFilterSet (list (make-LBot)) null)]
@ -21,31 +25,25 @@
[else (make-LFilterSet l1 l2)])) [else (make-LFilterSet l1 l2)]))
(define (combine l1 l2) (define (combine l1 l2)
(cond [(memq (make-Bot) l1) (match* (l1 l2)
(make-FilterSet (list (make-Bot)) null)] [(_ (Bot:)) (-FS -top -bot)]
[(memq (make-Bot) l2) [((Bot:) _) (-FS -bot -top)]
(make-FilterSet null (list (make-Bot)))] [(_ _) (-FS l1 l2)]))
[else (make-FilterSet l1 l2)]))
(d/c (abstract-filters keys ids results) (d/c/p (abstract-filters results)
((listof index/c) (listof identifier?) tc-results? . -> . (or/c Values? ValuesDots?)) (tc-results? . -> . (or/c Values? ValuesDots?))
(define (mk l [drest #f])
(if drest (make-ValuesDots l (car drest) (cdr drest)) (make-Values l)))
(match results (match results
[(tc-results: ts fs os dty dbound) [(tc-results: ts fs os dty dbound)
(make-ValuesDots (make-ValuesDots
(for/list ([t ts] (for/list ([t ts] [f fs] [o os])
[f fs] (make-Result t f o))
[o os])
(make-Result t (abstract-filter ids keys f) (abstract-object ids keys o)))
dty dbound)] dty dbound)]
[(tc-results: ts fs os) [(tc-results: ts fs os)
(make-Values (make-Values
(for/list ([t ts] (for/list ([t ts] [f fs] [o os])
[f fs] (make-Result t f o)))]))
[o os])
(make-Result t (abstract-filter ids keys f) (abstract-object ids keys o))))]))
#;
(define/contract (abstract-object ids keys o) (define/contract (abstract-object ids keys o)
(-> (listof identifier?) (listof index/c) Object? LatentObject?) (-> (listof identifier?) (listof index/c) Object? LatentObject?)
(define (lookup y) (define (lookup y)
@ -57,15 +55,17 @@
[(Path: p (lookup: idx)) (make-LPath p idx)] [(Path: p (lookup: idx)) (make-LPath p idx)]
[_ (make-LEmpty)])) [_ (make-LEmpty)]))
#;
(d/c (abstract-filter ids keys fs) (d/c (abstract-filter ids keys fs)
(-> (listof identifier?) (listof index/c) FilterSet/c LatentFilterSet/c) (-> (listof identifier?) (listof index/c) FilterSet/c LatentFilterSet/c)
(match fs (match fs
[(FilterSet: f+ f-) [(FilterSet: f+ f-)
(lcombine (combine
(apply append (for/list ([f f+]) (abo ids keys f))) (apply append (for/list ([f f+]) (abo ids keys f)))
(apply append (for/list ([f f-]) (abo ids keys f))))] (apply append (for/list ([f f-]) (abo ids keys f))))]
[(NoFilter:) (lcombine null null)])) [(NoFilter:) (combine -top -top)]))
#;
(d/c (abo xs idxs f) (d/c (abo xs idxs f)
((listof identifier?) (listof index/c) Filter/c . -> . (or/c null? (list/c LatentFilter/c))) ((listof identifier?) (listof index/c) Filter/c . -> . (or/c null? (list/c LatentFilter/c)))
(define (lookup y) (define (lookup y)
@ -91,32 +91,116 @@
(define (merge-filter-sets fs) (define (merge-filter-sets fs)
(match fs (match fs
[(list (FilterSet: f+ f-) ...) [(list (FilterSet: f+ f-) ...)
(make-FilterSet (remove-duplicates (apply append f+)) (remove-duplicates (apply append f-)))])) (make-FilterSet (make-AndFilter f+) (make-AndFilter f-))]))
(d/c (apply-filter lfs t o) (d/c/p (apply-filter fs ids os [polarity #t])
(-> LatentFilterSet/c Type/c Object? FilterSet/c) (->* (FilterSet/c (listof identifier?) (listof Object?)) (boolean?) FilterSet/c)
(match lfs (match fs
[(LFilterSet: lf+ lf-) [(FilterSet: f+ f-)
(combine (combine (subst-filter* f+ ids os polarity)
(apply append (for/list ([lf lf+]) (apo lf t o))) (subst-filter* f- ids os polarity))]))
(apply append (for/list ([lf lf-]) (apo lf t o))))]))
(d/c (apo lf s o) (d/c/p (apply-type t ids os [polarity #t])
(-> LatentFilter/c Type/c Object? (or/c '() (list/c Filter/c))) (->* (Type/c (listof identifier?) (listof Object?)) (boolean?) Type/c)
(match* (lf s o) (for/fold ([t t]) ([i (in-list ids)] [o (in-list os)])
[((ImpFilter: as cs) _ _) (subst-type t i o polarity)))
(match* [(for/list ([a as]) (apo a s o))
(for/list ([c cs]) (apo c s o))]
[((list (list a*) ...)
(list (list c*) ...)) (list (make-ImpFilter a* c*))]
[(_ _) null])]
[((LBot:) _ _) (list (make-Bot))]
[((LNotTypeFilter: (? (lambda (t) (subtype s t)) t) (list) _) _ _) (list (make-Bot))]
[((LTypeFilter: (? (lambda (t) (not (overlap s t))) t) (list) _) _ _) (list (make-Bot))]
[(_ _ (Empty:)) null]
[((LTypeFilter: t pi* _) _ (Path: pi x)) (list (make-TypeFilter t (append pi* pi) x))]
[((LNotTypeFilter: t pi* _) _ (Path: pi x)) (list (make-NotTypeFilter t (append pi* pi) x))]))
(d/c/p (apply-object t ids os [polarity #t])
(->* (Object? (listof identifier?) (listof Object?)) (boolean?) Object?)
(for/fold ([t t]) ([i (in-list ids)] [o (in-list os)])
(subst-object t i o polarity)))
(define (subst-filter* f ids os polarity)
(-> Filter/c (listof identifier?) (listof Object?) boolean? Filter/c)
(for/fold ([f f]) ([i (in-list ids)] [o (in-list os)])
(subst-filter f i o polarity)))
(d/c/p (subst-filter-set fs id o polarity)
(-> FilterSet? identifier? Object? boolean? FilterSet?)
(match fs
[(FilterSet: f+ f-)
(combine (subst-filter f+ id o polarity)
(subst-filter f- id o polarity))]))
(define (subst-type t id o polarity)
(define (st t) (subst-type t id o polarity))
(d/c (sf fs) (FilterSet? . -> . FilterSet?) (subst-filter-set fs id o polarity))
(type-case (#:Type st
#:Filter sf
#:Object (lambda (f) (subst-object f id o polarity)))
t))
(define (subst-object t id o polarity)
(match t
[(NoObject:) t]
[(Empty:) t]
[(Path: p i)
(if (free-identifier=? i id)
(match o
[(Empty:) (make-Empty)]
;; the result is not from an annotation, so it isn't a NoObject
[(NoObject:) (make-Empty)]
[(Path: p* i*) (make-Path (append p p*) i*)])
t)]))
;; this is the substitution metafunction
(d/c/p (subst-filter f id o polarity)
(-> Filter/c identifier? Object? boolean? Filter/c)
(define (ap f) (subst-filter f o polarity))
(define (tf-matcher t p i id o polarity maker)
(match o
[(or (Empty:) (NoObject:)) (if polarity -top -bot)]
[(Path: p* i*)
(cond [(free-identifier=? i id)
(maker
(subst-type t id o polarity)
(append p p*)
i*)]
[(id-free-in? id t) (if polarity -top -bot)]
[else f])]))
(match f
[(ImpFilter: ant consq)
(make-ImpFilter (subst-filter ant id o (not polarity)) (ap consq))]
[(AndFilter: fs) (make-AndFilter (map ap fs))]
[(OrFilter: fs) (make-OrFilter (map ap fs))]
[(Bot:) -bot]
[(Top:) -top]
[(TypeFilter: t p i)
(tf-matcher t p i id o polarity make-TypeFilter)]
[(NotTypeFilter: t p i)
(tf-matcher t p i id o polarity make-NotTypeFilter)]))
(define (id-free-in? id type)
(let/ec
return
(define (for-object o)
(object-case (#:Type for-type)
o
[#:Path p i
(if (free-identifier=? i id)
(return #t)
o)]))
(define (for-filter o)
(filter-case (#:Type for-type
#:Filter for-filter)
o
[#:NotTypeFilter t p i
(if (free-identifier=? i id)
(return #t)
o)]
[#:TypeFilter t p i
(if (free-identifier=? i id)
(return #t)
o)]))
(define (for-type t)
(type-case (#:Type for-type
#:Filter for-filter
#:Object for-object)
t))
(for-type type)))
#|
#;
(define/contract (split-lfilters lf idx) (define/contract (split-lfilters lf idx)
(LatentFilterSet/c index/c . -> . LatentFilterSet/c) (LatentFilterSet/c index/c . -> . LatentFilterSet/c)
(define (idx= lf) (define (idx= lf)
@ -133,6 +217,7 @@
(define-match-expander F-FS: (define-match-expander F-FS:
(lambda (stx) #'(FilterSet: (list (Bot:)) _))) (lambda (stx) #'(FilterSet: (list (Bot:)) _)))
#;
(d/c (combine-filter f1 f2 f3 t2 t3 o2 o3) (d/c (combine-filter f1 f2 f3 t2 t3 o2 o3)
(FilterSet/c FilterSet/c FilterSet/c Type? Type? Object? Object? . -> . tc-results?) (FilterSet/c FilterSet/c FilterSet/c Type? Type? Object? Object? . -> . tc-results?)
(define (mk f) (ret (Un t2 t3) f (make-Empty))) (define (mk f) (ret (Un t2 t3) f (make-Empty)))
@ -163,56 +248,28 @@
[(_ _ _) [(_ _ _)
;; could intersect f2 and f3 here ;; could intersect f2 and f3 here
(mk (make-FilterSet null null))])) (mk (make-FilterSet null null))]))
|#
;; (or/c Values? ValuesDots?) listof[identifier] -> tc-results? ;; (or/c Values? ValuesDots?) listof[identifier] -> tc-results?
(define (values->tc-results tc formals) (d/c/p (values->tc-results tc)
((or/c Values? ValuesDots?) . -> . tc-results?)
(match tc (match tc
[(ValuesDots: (list (Result: ts lfs los) ...) dty dbound) [(ValuesDots: (list (Result: ts fs os) ...) dty dbound)
(ret ts (ret ts fs os dty dbound)]
(for/list ([lf lfs]) [(Values: (list (Result: ts fs os) ...))
(or (ret ts fs os)]))
(and (null? formals)
(match lf
[(LFilterSet: lf+ lf-)
(combine (if (memq (make-LBot) lf+) (list (make-Bot)) (list))
(if (memq (make-LBot) lf-) (list (make-Bot)) (list)))]))
(merge-filter-sets
(for/list ([x formals] [i (in-naturals)])
(apply-filter (split-lfilters lf i) Univ (make-Path null x))))))
(for/list ([lo los])
(or
(for/or ([x formals] [i (in-naturals)])
(match lo
[(LEmpty:) #f]
[(LPath: p (== i)) (make-Path p x)]))
(make-Empty)))
dty dbound)]
[(Values: (list (Result: ts lfs los) ...))
(ret ts
(for/list ([lf lfs])
(or
(and (null? formals)
(match lf
[(LFilterSet: lf+ lf-)
(combine (if (memq (make-LBot) lf+) (list (make-Bot)) (list))
(if (memq (make-LBot) lf-) (list (make-Bot)) (list)))]))
(merge-filter-sets
(for/list ([x formals] [i (in-naturals)])
(apply-filter (split-lfilters lf i) Univ (make-Path null x))))))
(for/list ([lo los])
(or
(for/or ([x formals] [i (in-naturals)])
(match lo
[(LEmpty:) #f]
[(LPath: p (== i)) (make-Path p x)]))
(make-Empty))))]))
(define (tc-results->values tc) (define (tc-results->values tc)
(match tc (match tc
[(tc-results: ts) (-values ts)])) [(tc-results: ts) (-values ts)]))
(provide combine-props tc-results->values subst-object subst-type)
(define (combine-props new-props old-props) (define (combine-props new-props old-props)
(define-values (new-imps new-atoms) (partition ImpFilter? new-props)) (define-values (new-atoms new-formulas)
(partition (lambda (e) (or (TypeFilter? e) (NotTypeFilter? e))) new-props))
(values new-formulas new-atoms)
#;#;
(define-values (derived-imps derived-atoms) (define-values (derived-imps derived-atoms)
(for/fold (for/fold
([derived-imps null] ([derived-imps null]

4
collects/typed-scheme/typecheck/tc-structs.ss
View File

@ -143,9 +143,7 @@
(for/list ([g (in-list getters)] [t (in-list external-fld-types/no-parent)] [i (in-naturals)]) (for/list ([g (in-list getters)] [t (in-list external-fld-types/no-parent)] [i (in-naturals)])
(let ([func (if setters? (let ([func (if setters?
(->* (list name) t) (->* (list name) t)
(make-Function (->acc (list name) t (list (make-StructPE name i))))])
(list (make-arr* (list name) t
#:object (make-LPath (list (make-StructPE name i)) 0)))))])
(cons g (wrapper func)))) (cons g (wrapper func))))
(if setters? (if setters?
(map (lambda (g t) (cons g (wrapper (->* (list name t) -Void)))) setters external-fld-types/no-parent) (map (lambda (g t) (cons g (wrapper (->* (list name t) -Void)))) setters external-fld-types/no-parent)

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

@ -42,7 +42,7 @@
[with-handlers [with-handlers
([(lambda (e) (and catch-errors? (exn:fail? e) (not (exn:fail:syntax? e)))) ([(lambda (e) (and catch-errors? (exn:fail? e) (not (exn:fail:syntax? e))))
(lambda (e) (tc-error "Internal error: ~a" e))])] (lambda (e) (tc-error "Internal error: ~a" e))])]
[parameterize (;; disable fancy printing [parameterize (;; enable fancy printing?
[custom-printer #t] [custom-printer #t]
;; a cheat to avoid units ;; a cheat to avoid units
[infer-param infer] [infer-param infer]
@ -99,7 +99,9 @@
[(_ . form) [(_ . form)
(nest (nest
([begin (set-box! typed-context? #t)] ([begin (set-box! typed-context? #t)]
[parameterize (;; a cheat to avoid units [parameterize (;; disable fancy printing
[custom-printer #t]
;; a cheat to avoid units
[infer-param infer] [infer-param infer]
;; this paramter is for parsing types ;; this paramter is for parsing types
[current-tvars initial-tvar-env] [current-tvars initial-tvar-env]

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

@ -9,6 +9,7 @@
scheme/match scheme/match
scheme/promise scheme/promise
scheme/flonum scheme/flonum
unstable/syntax
(prefix-in c: scheme/contract) (prefix-in c: scheme/contract)
(for-syntax scheme/base syntax/parse) (for-syntax scheme/base syntax/parse)
(for-template scheme/base scheme/contract scheme/promise scheme/tcp scheme/flonum)) (for-template scheme/base scheme/contract scheme/promise scheme/tcp scheme/flonum))
@ -26,8 +27,6 @@
(define -Param make-Param) (define -Param make-Param)
(define -box make-Box) (define -box make-Box)
(define -vec make-Vector) (define -vec make-Vector)
(define -LFS make-LFilterSet)
(define-syntax -FS (make-rename-transformer #'make-FilterSet))
(define-syntax *Un (define-syntax *Un
(syntax-rules () (syntax-rules ()
@ -62,8 +61,8 @@
#'(app untuple (? values elem-pats))]))) #'(app untuple (? values elem-pats))])))
(d/c (-result t [f -no-lfilter] [o -no-lobj]) (d/c (-result t [f -no-filter] [o -no-obj])
(c:->* (Type/c) (LFilterSet? LatentObject?) Result?) (c:->* (Type/c) (FilterSet? Object?) Result?)
(make-Result t f o)) (make-Result t f o))
(d/c (-values args) (d/c (-values args)
@ -115,11 +114,19 @@
(define -Pathlike* (*Un -String -Path (-val 'up) (-val 'same))) (define -Pathlike* (*Un -String -Path (-val 'up) (-val 'same)))
(define -Pattern (*Un -Bytes -Regexp -PRegexp -Byte-Regexp -Byte-PRegexp -String)) (define -Pattern (*Un -Bytes -Regexp -PRegexp -Byte-Regexp -Byte-PRegexp -String))
(define -no-lfilter (make-LFilterSet null null)) (define -top (make-Top))
(define -no-filter (make-FilterSet null null)) (define -bot (make-Bot))
(define -no-lobj (make-LEmpty)) (define -no-filter (make-FilterSet -top -top))
(define -no-obj (make-Empty)) (define -no-obj (make-Empty))
(d/c (-FS + -)
(c:-> Filter/c Filter/c FilterSet?)
(match* (+ -)
[((Bot:) _) (make-FilterSet -bot -top)]
[(_ (Bot:)) (make-FilterSet -top -bot)]
[(+ -) (make-FilterSet + -)]))
(define -car (make-CarPE)) (define -car (make-CarPE))
(define -cdr (make-CdrPE)) (define -cdr (make-CdrPE))
(define -syntax-e (make-SyntaxPE)) (define -syntax-e (make-SyntaxPE))
@ -175,18 +182,24 @@
(d/c (make-arr* dom rng (d/c (make-arr* dom rng
#:rest [rest #f] #:drest [drest #f] #:kws [kws null] #:rest [rest #f] #:drest [drest #f] #:kws [kws null]
#:filters [filters -no-lfilter] #:object [obj -no-lobj]) #:filters [filters -no-filter] #:object [obj -no-obj]
#:names [names (append
(generate-temporaries dom)
(if (or drest rest) (list (generate-temporary)) null)
(generate-temporaries kws))])
(c:->* ((listof Type/c) (or/c Values? ValuesDots? Type/c)) (c:->* ((listof Type/c) (or/c Values? ValuesDots? Type/c))
(#:rest (or/c #f Type/c) (#:rest (or/c #f Type/c)
#:drest (or/c #f (cons/c Type/c symbol?)) #:drest (or/c #f (cons/c Type/c symbol?))
#:kws (listof Keyword?) #:kws (listof Keyword?)
#:filters LFilterSet? #:filters FilterSet?
#:object LatentObject?) #:object Object?
#:names (listof identifier?))
arr?) arr?)
(make-arr dom (if (or (Values? rng) (ValuesDots? rng)) (make-arr dom (if (or (Values? rng) (ValuesDots? rng))
rng rng
(make-Values (list (-result rng filters obj)))) (make-Values (list (-result rng filters obj))))
rest drest (sort #:key Keyword-kw kws keyword<?))) rest drest (sort #:key Keyword-kw kws keyword<?)
names))
(define-syntax (->* stx) (define-syntax (->* stx)
(define-syntax-class c (define-syntax-class c
@ -228,10 +241,12 @@
(make-Function (list (make-arr* dom rng #:drest (cons dty 'dbound) #:filters filters)))])) (make-Function (list (make-arr* dom rng #:drest (cons dty 'dbound) #:filters filters)))]))
(define (->acc dom rng path) (define (->acc dom rng path)
(define x (generate-temporary 'x))
(make-Function (list (make-arr* dom rng (make-Function (list (make-arr* dom rng
#:filters (-LFS (list (-not-filter (-val #f) path)) #:names (list x)
(list (-filter (-val #f) path))) #:filters (-FS (-not-filter (-val #f) x path)
#:object (make-LPath path 0))))) (-filter (-val #f) x path))
#:object (make-Path path x)))))
(define (cl->* . args) (define (cl->* . args)
(define (funty-arities f) (define (funty-arities f)
@ -259,12 +274,70 @@
(define (-struct name parent flds accs [proc #f] [poly #f] [pred #'dummy] [cert values]) (define (-struct name parent flds accs [proc #f] [poly #f] [pred #'dummy] [cert values])
(make-Struct name parent flds proc poly pred cert accs)) (make-Struct name parent flds proc poly pred cert accs))
(define (-filter t [p null] [i 0]) (d/c (-filter t i [p null])
(make-LTypeFilter t p i)) (c:->* (Type/c identifier?) ((listof PathElem?)) Filter/c)
(make-TypeFilter t p i))
(define (-not-filter t [p null] [i 0]) (define (-filter-at t o)
(make-LNotTypeFilter t p i)) (match o
[(Path: p i) (-filter t i p)]
[_ -top]))
(define (-not-filter-at t o)
(match o
[(Path: p i) (-not-filter t i p)]
[_ -top]))
(define (opposite? f1 f2)
(match* (f1 f2)
[((TypeFilter: t1 p1 i1)
(NotTypeFilter: t2 p1 i2))
(and (type-equal? t1 t2)
(free-identifier=? i1 i2))]
[((NotTypeFilter: t2 p1 i2)
(TypeFilter: t1 p1 i1))
(and (type-equal? t1 t2)
(free-identifier=? i1 i2))]
[(_ _) #f]))
(define (-or . args)
(let loop ([fs args] [result null])
(if (null? fs)
(match result
[(list) -bot]
[(list f) f]
[(list f1 f2) (opposite? f1 f2) -top]
[_ (make-OrFilter result)])
(match (car fs)
[(and t (Top:)) t]
[(OrFilter: fs*) (loop (cdr fs) (append fs* result))]
[(Bot:) (loop (cdr fs) result)]
[t (loop (cdr fs) (cons t result))]))))
(define (-and . args)
(let loop ([fs args] [result null])
(if (null? fs)
(match result
[(list) -top]
[(list f) f]
;; don't think this is useful here
#;[(list f1 f2) (opposite? f1 f2) -bot]
[_ (make-AndFilter result)])
(match (car fs)
[(and t (Bot:)) t]
[(AndFilter: fs*) (loop (cdr fs) (append fs* result))]
[(Top:) (loop (cdr fs) result)]
[t (loop (cdr fs) (cons t result))]))))
(d/c (-not-filter t i [p null])
(c:->* (Type/c identifier?) ((listof PathElem?)) Filter/c)
(make-NotTypeFilter t p i))
(define-syntax-rule (with-names (vars ...) . e)
(let-values ([(vars ...) (apply values (generate-temporaries '(vars ...)))])
. e))
(define-syntax-rule (asym-pred (var) dom rng filter)
(with-names (var) (make-Function (list (make-arr* (list dom) rng #:names (list var) #:filters filter)))))
(d/c make-pred-ty (d/c make-pred-ty
(case-> (c:-> Type/c Type/c) (case-> (c:-> Type/c Type/c)
@ -273,15 +346,22 @@
(c:-> (listof Type/c) Type/c Type/c integer? (listof PathElem?) Type/c)) (c:-> (listof Type/c) Type/c Type/c integer? (listof PathElem?) Type/c))
(case-lambda (case-lambda
[(in out t n p) [(in out t n p)
(->* in out : (-LFS (list (-filter t p n)) (list (-not-filter t p n))))] (define xs (generate-temporaries in))
(make-Function
(list
(make-arr*
in out
#:names xs
#:filters (-FS (-filter t (list-ref xs n) p) (-not-filter t (list-ref xs n) p)))))]
[(in out t n) [(in out t n)
(->* in out : (-LFS (list (-filter t null n)) (list (-not-filter t null n))))] (make-pred-ty in out t n null)]
[(in out t) [(in out t)
(make-pred-ty in out t 0)] (make-pred-ty in out t 0 null)]
[(t) (make-pred-ty (list Univ) -Boolean t 0)])) [(t)
(make-pred-ty (list Univ) -Boolean t 0 null)]))
(define true-filter (-FS (list) (list (make-Bot)))) (define true-filter (-FS -top -bot))
(define false-filter (-FS (list (make-Bot)) (list))) (define false-filter (-FS -bot -top))
(define (opt-fn args opt-args result) (define (opt-fn args opt-args result)
(apply cl->* (for/list ([i (in-range (add1 (length opt-args)))]) (apply cl->* (for/list ([i (in-range (add1 (length opt-args)))])

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

@ -29,40 +29,20 @@
ns) ns)
#f)) #f))
;; print out an effect
;; print-effect : Effect Port Boolean -> Void
(define (print-latentfilter c port write?)
(define (fp . args) (apply fprintf port args))
(match c
[(LFilterSet: thn els) (fp "(")
(if (null? thn)
(fp "LTop")
(for ([i thn]) (fp "~a " i)))
(fp "|")
(if (null? els)
(fp "LTop")
(for ([i els]) (fp " ~a" i)))
(fp")")]
[(LNotTypeFilter: type path 0) (fp "(! ~a @ ~a)" type path)]
[(LTypeFilter: type path 0) (fp "(~a @ ~a)" type path)]
[(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")]
[(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 (print-filter c port write?)
(define (fp . args) (apply fprintf port args)) (define (fp . args) (apply fprintf port args))
(match c (match c
[(FilterSet: thn els) (fp "(") [(FilterSet: thn els) (fp "(~a | ~a)" thn els)]
(for ([i thn]) (fp "~a " i)) (fp "|")
(for ([i els]) (fp " ~a" i))
(fp")")]
[(NoFilter:) (fp "-")] [(NoFilter:) (fp "-")]
[(NotTypeFilter: type (list) id) (fp "(! ~a @ ~a)" type (syntax-e id))]
[(NotTypeFilter: type path id) (fp "(! ~a @ ~a ~a)" type path (syntax-e id))] [(NotTypeFilter: type path id) (fp "(! ~a @ ~a ~a)" type path (syntax-e id))]
[(TypeFilter: type (list) id) (fp "(~a @ ~a)" type (syntax-e id))]
[(TypeFilter: 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")]
[(Top:) (fp "Top")]
[(ImpFilter: a c) (fp "(ImpFilter ~a ~a)" a c)] [(ImpFilter: a c) (fp "(ImpFilter ~a ~a)" a c)]
[(AndFilter: a) (fp "(AndFilter") (for ([a0 a]) (fp " ~a" a0)) (fp ")")]
[(OrFilter: a) (fp "(OrFilter") (for ([a0 a]) (fp " ~a" a0)) (fp ")")]
[else (fp "(Unknown Filter: ~a)" (struct->vector c))])) [else (fp "(Unknown Filter: ~a)" (struct->vector c))]))
(define (print-pathelem c port write?) (define (print-pathelem c port write?)
@ -73,12 +53,6 @@
[(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))])) [else (fp "(Unknown Path Element: ~a)" (struct->vector c))]))
(define (print-latentobject c port write?)
(define (fp . args) (apply fprintf port args))
(match c
[(LEmpty:) (fp "")]
[(LPath: pes i) (fp "~a" (append pes (list i)))]))
(define (print-object c port write?) (define (print-object c port write?)
(define (fp . args) (apply fprintf port args)) (define (fp . args) (apply fprintf port args))
(match c (match c
@ -114,17 +88,17 @@
(fp "~a ...~a~a " (fp "~a ...~a~a "
(car drest) (if (special-dots-printing?) "" " ") (cdr drest))) (car drest) (if (special-dots-printing?) "" " ") (cdr drest)))
(match rng (match rng
[(Values: (list (Result: t (LFilterSet: (list) (list)) (LEmpty:)))) [(Values: (list (Result: t (FilterSet: (Top:) (Top:)) (Empty:))))
(fp "-> ~a" t)] (fp "-> ~a" t)]
[(Values: (list (Result: t [(Values: (list (Result: t
(LFilterSet: (list (LTypeFilter: ft pth 0)) (FilterSet: (TypeFilter: ft pth id)
(list (LNotTypeFilter: ft pth 0))) (NotTypeFilter: ft pth id))
(LEmpty:)))) (Empty:))))
(if (null? pth) (if (null? pth)
(fp "-> ~a : ~a" t ft) (fp "-> ~a : ~a" t ft)
(begin (fp "-> ~a : ~a @" t ft) (begin (fp "-> ~a : ~a @" t ft)
(for ([pe pth]) (fp " ~a" pe))))] (for ([pe pth]) (fp " ~a" pe))))]
[(Values: (list (Result: t fs (LEmpty:)))) [(Values: (list (Result: t fs (Empty:))))
(fp/filter "-> ~a : ~a" t fs)] (fp/filter "-> ~a : ~a" t fs)]
[(Values: (list (Result: t lf lo))) [(Values: (list (Result: t lf lo)))
(fp/filter "-> ~a : ~a ~a" t lf lo)] (fp/filter "-> ~a : ~a ~a" t lf lo)]
@ -142,10 +116,15 @@
[(Pair: a e) (cons a (tuple-elems e))] [(Pair: a e) (cons a (tuple-elems e))]
[(Value: '()) null])) [(Value: '()) null]))
(match c (match c
;; if we know how it was written, print that
[(? Rep-stx a)
(fp "~a" (syntax->datum (Rep-stx a)))]
[(Univ:) (fp "Any")] [(Univ:) (fp "Any")]
;; special case number until something better happens ;; special case number until something better happens
;;[(Base: 'Number _) (fp "Number")] ;;[(Base: 'Number _) (fp "Number")]
[(? has-name?) (fp "~a" (has-name? c))] [(? has-name?)
#;(printf "has a name\n")
(fp "~a" (has-name? c))]
[(StructTop: st) (fp "~a" st)] [(StructTop: st) (fp "~a" st)]
[(BoxTop:) (fp "Box")] [(BoxTop:) (fp "Box")]
[(VectorTop:) (fp "Vector")] [(VectorTop:) (fp "Vector")]
@ -183,7 +162,7 @@
(lambda (e) (fp " ") (print-arr e)) (lambda (e) (fp " ") (print-arr e))
b) b)
(fp ")")]))] (fp ")")]))]
[(arr: _ _ _ _ _) (print-arr c)] [(arr: _ _ _ _ _) (fp "(arr ") (print-arr c) (fp ")")]
[(Vector: e) (fp "(Vectorof ~a)" e)] [(Vector: e) (fp "(Vectorof ~a)" e)]
[(Box: e) (fp "(Boxof ~a)" e)] [(Box: e) (fp "(Boxof ~a)" e)]
[(Union: elems) (fp "~a" (cons 'U elems))] [(Union: elems) (fp "~a" (cons 'U elems))]
@ -227,8 +206,8 @@
[(Syntax: t) (fp "(Syntaxof ~a)" t)] [(Syntax: t) (fp "(Syntaxof ~a)" t)]
[(Instance: t) (fp "(Instance ~a)" t)] [(Instance: t) (fp "(Instance ~a)" t)]
[(Class: pf nf ms) (fp "(Class)")] [(Class: pf nf ms) (fp "(Class)")]
[(Result: t (LFilterSet: (list) (list)) (LEmpty:)) (fp "~a" t)] [(Result: t (FilterSet: (Top:) (Top:)) (Empty:)) (fp "~a" t)]
[(Result: t fs (LEmpty:)) (fp "(~a : ~a)" t fs)] [(Result: t fs (Empty:)) (fp "(~a : ~a)" t fs)]
[(Result: t fs lo) (fp "(~a : ~a : ~a)" t fs lo)] [(Result: t fs lo) (fp "(~a : ~a : ~a)" t fs lo)]
[(Refinement: parent p? _) [(Refinement: parent p? _)
(fp "(Refinement ~a ~a)" parent (syntax-e p?))] (fp "(Refinement ~a ~a)" parent (syntax-e p?))]
@ -238,7 +217,7 @@
(set-box! print-type* print-type) (set-box! print-type* print-type)
(set-box! print-filter* print-filter) (set-box! print-filter* print-filter)
(set-box! print-latentfilter* print-latentfilter) ;(set-box! print-latentfilter* print-latentfilter)
(set-box! print-object* print-object) (set-box! print-object* print-object)
(set-box! print-latentobject* print-latentobject) ;(set-box! print-latentobject* print-latentobject)
(set-box! print-pathelem* print-pathelem) (set-box! print-pathelem* print-pathelem)

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

@ -184,14 +184,12 @@
(d/c (combine-arrs arrs) (d/c (combine-arrs arrs)
(c-> (listof arr?) (or/c #f arr?)) (c-> (listof arr?) (or/c #f arr?))
(match arrs (match arrs
[(list (arr: dom1 rng1 #f #f '()) (arr: dom rng #f #f '()) ...) [(list (and a1 (arr: dom1 rng1 #f #f '() names)) (arr: dom rng #f #f '()) ...)
(cond (cond
[(null? dom) (make-arr dom1 rng1 #f #f '())] [(null? dom) a1]
((not (apply = (length dom1) (map length dom))) [(not (apply = (length dom1) (map length dom))) #f]
#f) [(not (foldl type-equal? rng1 rng)) #f]
((not (foldl type-equal? rng1 rng)) [else (make-arr (apply map (lambda args (make-Union (sort args type<?))) (cons dom1 dom)) rng1 #f #f '() names)])]
#f)
[else (make-arr (apply map (lambda args (make-Union (sort args type<?))) (cons dom1 dom)) rng1 #f #f '())])]
[_ #f])) [_ #f]))
@ -328,7 +326,7 @@
[((Result: t f o) (Result: t* f o)) [((Result: t f o) (Result: t* f o))
(subtype* A0 t t*)] (subtype* A0 t t*)]
;; we can ignore interesting results ;; we can ignore interesting results
[((Result: t f o) (Result: t* (LFilterSet: (list) (list)) (LEmpty:))) [((Result: t f o) (Result: t* (FilterSet: (Top:) (Top:)) (Empty:)))
(subtype* A0 t t*)] (subtype* A0 t t*)]
;; subtyping on other stuff ;; subtyping on other stuff
[((Syntax: t) (Syntax: t*)) [((Syntax: t) (Syntax: t*))

24
collects/typed-scheme/types/utils.ss
View File

@ -43,7 +43,7 @@
target target
[#:Union tys (Un (map sb tys))] [#:Union tys (Un (map sb tys))]
[#:F name* (if (eq? name* name) image target)] [#:F name* (if (eq? name* name) image target)]
[#:arr dom rng rest drest kws [#:arr dom rng rest drest kws names
(begin (begin
(when (and (pair? drest) (when (and (pair? drest)
(eq? name (cdr drest)) (eq? name (cdr drest))
@ -53,7 +53,8 @@
(sb rng) (sb rng)
(and rest (sb rest)) (and rest (sb rest))
(and drest (cons (sb (car drest)) (cdr drest))) (and drest (cons (sb (car drest)) (cdr drest)))
(map sb kws)))] (map sb kws)
names))]
[#:ValuesDots types dty dbound [#:ValuesDots types dty dbound
(begin (begin
(when (eq? name dbound) (when (eq? name dbound)
@ -76,10 +77,10 @@
(for/list ([img images]) (for/list ([img images])
(make-Result (make-Result
(substitute img name expanded) (substitute img name expanded)
(make-LFilterSet null null) (make-FilterSet (make-Top) (make-Top))
(make-LEmpty)))))) (make-Empty))))))
(make-ValuesDots (map sb types) (sb dty) dbound))] (make-ValuesDots (map sb types) (sb dty) dbound))]
[#:arr dom rng rest drest kws [#:arr dom rng rest drest kws names
(if (and (pair? drest) (if (and (pair? drest)
(eq? name (cdr drest))) (eq? name (cdr drest)))
(make-arr (append (make-arr (append
@ -90,12 +91,14 @@
(sb rng) (sb rng)
rimage rimage
#f #f
(map sb kws)) (map sb kws)
names)
(make-arr (map sb dom) (make-arr (map sb dom)
(sb rng) (sb rng)
(and rest (sb rest)) (and rest (sb rest))
(and drest (cons (sb (car drest)) (cdr drest))) (and drest (cons (sb (car drest)) (cdr drest)))
(map sb kws)))]) (map sb kws)
names))])
target)) target))
;; implements sd from the formalism ;; implements sd from the formalism
@ -113,14 +116,15 @@
(if (eq? name* name) (if (eq? name* name)
image image
target)] target)]
[#:arr dom rng rest drest kws [#:arr dom rng rest drest kws names
(make-arr (map sb dom) (make-arr (map sb dom)
(sb rng) (sb rng)
(and rest (sb rest)) (and rest (sb rest))
(and drest (and drest
(cons (sb (car drest)) (cons (sb (car drest))
(if (eq? name (cdr drest)) image-bound (cdr drest)))) (if (eq? name (cdr drest)) image-bound (cdr drest))))
(map sb kws))]) (map sb kws)
names)])
target)) target))
;; substitute many variables ;; substitute many variables
@ -210,7 +214,7 @@
;; convenience function for returning the result of typechecking an expression ;; convenience function for returning the result of typechecking an expression
(define ret (define ret
(case-lambda [(t) (case-lambda [(t)
(let ([mk (lambda (t) (make-FilterSet null null))]) (let ([mk (lambda (t) (make-FilterSet (make-Top) (make-Top)))])
(make-tc-results (make-tc-results
(cond [(Type? t) (cond [(Type? t)
(list (make-tc-result t (mk t) (make-Empty)))] (list (make-tc-result t (mk t) (make-Empty)))]

2
collects/typed-scheme/utils/utils.ss
View File

@ -161,7 +161,7 @@ at least theoretically.
;; turn contracts on and off - off by default for performance. ;; turn contracts on and off - off by default for performance.
(define-for-syntax enable-contracts? #f) (define-for-syntax enable-contracts? #t)
(provide (for-syntax enable-contracts?) p/c w/c cnt d-s/c d/c) (provide (for-syntax enable-contracts?) p/c w/c cnt d-s/c d/c)
;; these are versions of the contract forms conditionalized by `enable-contracts?' ;; these are versions of the contract forms conditionalized by `enable-contracts?'

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

@ -49,7 +49,7 @@
[draw-text (String Number Number -> Void)]))) [draw-text (String Number Number -> Void)])))
(dt Color% (Class () () ([red (-> Number)]))) (dt Color% (Class () () ([red (-> Number)])))
(dt Snip% (Class () () ())) (dt Snip% (Class () () ([get-count (-> Integer)])))
(dt Text% (Class () (dt Text% (Class ()
() ()