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

Cleanup of subtyping, additional comments, and improved short circuting.

Browse Source 
original commit: 71d6189132cecffc75b4d2fdb41c985a1a763380
This commit is contained in:
Eric Dobson 2013-03-13 22:56:13 -07:00
parent 5fbd396787
commit b8c9e1f63f
4 changed files with 21 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
collects/tests/typed-racket/succeed/pr12644.rkt
View File

@ -9,14 +9,14 @@
(: v (Listof (U inf Byte)))
(define v
(list
(list
(with-handlers ((void values)) 2)
(with-handlers ((void add1)) 3)
(with-handlers ((void f)) 4)
(with-handlers ((void g)) 5)))
(list
(list
(with-handlers ((void values)) 6)
(with-handlers ((void add1)) 7)
(with-handlers ((void f)) 8)

2
collects/typed-racket/base-env/base-env.rkt
View File

@ -1392,7 +1392,7 @@
[values (-polydots (a b) (cl->*
[values (-polydots (a b) (cl->*
(-> (-values null))
(->acc (list a) a null)
((list a) (b b) . ->... . (make-ValuesDots (list (-result a)) b 'b))))]

12
collects/typed-racket/types/substitute.rkt
View File

@ -34,7 +34,7 @@
(for/hash ([v (in-list vs)] [t (in-list ts)])
(values v (t-subst t))))
;; TODO: Figure out if free var checking/short circuiting is actually a performance improvement.
;; substitute-many : Hash[Name,Type] Type -> Type
(define/cond-contract (substitute-many subst target #:Un [Un (lambda (args) (apply Un args))])
@ -132,16 +132,18 @@
(map sb kws)))])
target))
;; implements curly brace substitution from the formalism
;; substitute-dotted : Type Name Name Type -> Type
;; implements curly brace substitution from the formalism, with the addition
;; that a substitution can include fixed args in addition to a different dotted arg
;; substitute-dotted : Listof[Type] Type Name Name Type -> Type
(define (substitute-dotted pre-image image image-bound name target)
(define (sb t) (substitute-dotted pre-image image image-bound name t))
;; We do a quick check on the free variables to see if we can short circuit the substitution
(if (or (set-member? (free-vars-names (free-idxs* target)) name)
(set-member? (free-vars-names (free-vars* target)) name))
(type-case (#:Type sb #:Filter (sub-f sb))
target
[#:ValuesDots types dty dbound
(let ((extra-types (if (eq? name dbound) pre-image null)))
(let ([extra-types (if (eq? name dbound) pre-image null)])
(make-ValuesDots (append (map sb types) (map -result extra-types))
(sb dty)
(if (eq? name dbound) image-bound dbound)))]
@ -156,7 +158,7 @@
image
target)]
[#:arr dom rng rest drest kws
(let ((extra-types (if (and drest (eq? name (cdr drest))) pre-image null)))
(let ([extra-types (if (and drest (eq? name (cdr drest))) pre-image null)])
(make-arr (append (map sb dom) extra-types)
(sb rng)
(and rest (sb rest))

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

@ -244,6 +244,7 @@
(parameterize ([current-seen A0])
(match* (s t)
[(_ (Univ:)) A0]
[((or (ValuesDots: _ _ _) (Values: _) (AnyValues:)) (AnyValues:)) A0]
;; error is top and bot
[(_ (Error:)) A0]
[((Error:) _) A0]
@ -359,27 +360,31 @@
(=> unmatch)
(unless (= (length ns) (length ms))
(unmatch))
;; substitute ns for ms in b2 to make it look like b1
(subtype* A0 b1 (subst-all (make-simple-substitution ms (map make-F ns)) b2))]
[((PolyDots: (list ns ... n-dotted) b1)
(PolyDots: (list ms ... m-dotted) b2))
(cond
((< (length ns) (length ms))
[(< (length ns) (length ms))
(define-values (short-ms rest-ms) (split-at ms (length ns)))
;; substitute ms for ns in b1 to make it look like b2
(define subst
(hash-set (make-simple-substitution ns (map make-F short-ms))
n-dotted (i-subst/dotted (map make-F rest-ms) (make-F m-dotted) m-dotted)))
(subtype* A0 (subst-all subst b1) b2))
(else
(subtype* A0 (subst-all subst b1) b2)]
[else
(define-values (short-ns rest-ns) (split-at ns (length ms)))
;; substitute ns for ms in b2 to make it look like b1
(define subst
(hash-set (make-simple-substitution ms (map make-F short-ns))
m-dotted (i-subst/dotted (map make-F rest-ns) (make-F n-dotted) n-dotted)))
(subtype* A0 b1 (subst-all subst b2))))]
(subtype* A0 b1 (subst-all subst b2))])]
[((PolyDots: (list ns ... n-dotted) b1)
(Poly: (list ms ...) b2))
(=> unmatch)
(unless (<= (length ns) (length ms))
(unmatch))
;; substitute ms for ns in b1 to make it look like b2
(define subst
(hash-set (make-simple-substitution ns (map make-F (take ms (length ns))))
n-dotted (i-subst (map make-F (drop ms (length ns))))))
@ -389,10 +394,10 @@
;; use unification to see if we can use the polytype here
[((Poly: vs b) s)
(=> unmatch)
(if (infer vs null (list b) (list s) (make-Univ)) A0 (unmatch))]
(if (infer vs null (list b) (list s) Univ) A0 (unmatch))]
[((PolyDots: (list vs ... vdotted) b) s)
(=> unmatch)
(if (infer vs (list vdotted) (list b) (list s) (make-Univ) )
(if (infer vs (list vdotted) (list b) (list s) Univ)
A0
(unmatch))]
[(s (or (Poly: vs b) (PolyDots: vs b)))
@ -509,7 +514,6 @@
[((Values: vals1) (Values: vals2)) (subtypes* A0 vals1 vals2)]
[((ValuesDots: s-rs s-dty dbound) (ValuesDots: t-rs t-dty dbound))
(subtype* (subtypes* A0 s-rs t-rs) s-dty t-dty)]
[((or (ValuesDots: _ _ _) (Values: _) (AnyValues:)) (AnyValues:)) A0]
;; trivial case for Result
[((Result: t f o) (Result: t* f o))
(subtype* A0 t t*)]