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

Make mutable lists be sequences.

Browse Source 
original commit: f6df93ed964e775cdd1734edd9a41d70b98ab0d8
This commit is contained in:
Eric Dobson 2013-02-14 23:37:41 -08:00
parent 75d3e13492
commit b7c3ede8ce
5 changed files with 25 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
collects/tests/typed-racket/unit-tests/subtype-tests.rkt
View File

@ -156,6 +156,10 @@
[(-pair -String (-lst -String)) (-seq -String)]
[FAIL (-pair -String (-lst -Symbol)) (-seq -String)]
[FAIL (-pair -String (-vec -String)) (-seq -String)]
[(-mpair -String (-mlst -String)) (-seq -String)]
[FAIL (-mpair -String (-mlst -Symbol)) (-seq -String)]
[FAIL (-mpair -String (-vec -String)) (-seq -String)]
[(-mpair -String (-mlst (-val "hello"))) (-seq -String)]
[(-Param -Byte -Byte) (-Param (-val 0) -Int)]
[FAIL (-Param -Byte -Byte) (-Param -Int -Int)]

6
collects/typed-racket/infer/infer-unit.rkt
View File

@ -451,6 +451,12 @@
(cg t t*)]
[((Pair: t1 t2) (Sequence: (list t*)))
(cset-meet (cg t1 t*) (cg t2 (-lst t*)))]
[((MListof: t) (Sequence: (list t*)))
(cg t t*)]
;; To check that mutable pair is a sequence we check that the cdr is
;; both an mutable list and a sequence
[((MPair: t1 t2) (Sequence: (list t*)))
(cset-meet* (list (cg t1 t*) (cg t2 T) (cg t2 (Un (-val null) (make-MPairTop)))))]
[((List: ts) (Sequence: (list t*)))
(cset-meet* (for/list ([t (in-list ts)])
(cg t t*)))]

5
collects/typed-racket/types/abbrev.rkt
View File

@ -23,8 +23,7 @@
(provide (except-out (all-defined-out) make-Base)
(all-from-out "base-abbrev.rkt" "match-expanders.rkt")
(rename-out [make-MListof -mlst]))
(all-from-out "base-abbrev.rkt" "match-expanders.rkt"))
;; all the types defined here are not numeric
(define (make-Base name contract predicate marshaled)
@ -52,8 +51,6 @@
(define (make-MListof elem) (-mu mlist-rec (Un (-val null) (-mpair elem mlist-rec))))
(define (-lst* #:tail [tail (-val null)] . args)
(for/fold ([tl tail]) ([a (reverse args)]) (-pair a tl)))

6
collects/typed-racket/types/base-abbrev.rkt
View File

@ -10,7 +10,8 @@
(for-template racket/base))
(provide (all-defined-out)
(rename-out [make-Listof -lst]))
(rename-out [make-Listof -lst]
[make-MListof -mlst]))
;Top and error types
(define Univ (make-Univ))
@ -26,7 +27,8 @@
;; Char type and List type (needed because of how sequences are checked in subtype)
(define -Char (make-Base 'Char #'char? char? #'-Char #f))
(define (make-Listof elem) (-mu list-rec (simple-Un (make-Value null) (make-Pair elem list-rec))))
(define (make-Listof elem) (-mu list-rec (simple-Un (-val null) (make-Pair elem list-rec))))
(define (make-MListof elem) (-mu list-rec (simple-Un (-val null) (make-MPair elem list-rec))))
;; Void is needed for Params
(define -Void (make-Base 'Void #'void? void? #'-Void #f))

13
collects/typed-racket/types/subtype.rkt
View File

@ -284,7 +284,15 @@
(subtype* A0 t t*)]
[((Pair: t1 t2) (Sequence: (list t*)))
(let ([A1 (subtype* A0 t1 t*)])
(and A1 (subtype* A1 t2 (-lst t*))))]
(subtype* A1 t2 (-lst t*)))]
[((MListof: t) (Sequence: (list t*)))
(subtype* A0 t t*)]
;; To check that mutable pair is a sequence we check that the cdr
;; is both an mutable list and a sequence
[((MPair: t1 t2) (Sequence: (list t*)))
(let* ([A1 (subtype* A0 t1 t*)]
[A2 (subtype* A1 t2 (simple-Un (-val null) (make-MPairTop)))])
(subtype* A2 t2 t))]
[((List: ts) (Sequence: (list t*)))
(subtypes* A0 ts (map (λ _ t*) ts))]
[((HeterogeneousVector: ts) (Sequence: (list t*)))
@ -339,8 +347,7 @@
[else (fail! s t)]))]
;; recur structurally on pairs
[((Pair: a d) (Pair: a* d*))
(let ([A1 (subtype* A0 a a*)])
(and A1 (subtype* A1 d d*)))]
(subtypes* A0 (list a d) (list a* d*))]
;; recur structurally on dotted lists, assuming same bounds
[((ListDots: s-dty dbound) (ListDots: t-dty dbound))
(subtype* A0 s-dty t-dty)]