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

Make PolyDots actually subtype correctly.

Browse Source 
original commit: 6335de099e7161447ec444ad320c6751f2c2af4d
This commit is contained in:
Eric Dobson 2013-02-26 22:25:28 -08:00
parent b151df08bc
commit 57a60ad403
4 changed files with 57 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -185,6 +185,27 @@
[FAIL -Fixnum (-seq -Fixnum)]
[FAIL -NonNegFixnum (-seq -Index)]
[FAIL (-val 5.0) (-seq -Nat)]
[(-polydots (a) (->... (list Univ) (a a) (make-ValuesDots null a 'a)))
(-polydots (a) (->... (list -String) (a a) (make-ValuesDots null a 'a)))]
[(-polydots (a) (->... null (Univ a) (make-ValuesDots (list (-result a)) a 'a)))
(-polydots (a) (->... null (-String a) (make-ValuesDots (list (-result a)) a 'a)))]
[(-polydots (a) (->... null (a a) (make-ValuesDots (list (-result -String)) -String 'a)))
(-polydots (a) (->... null (a a) (make-ValuesDots (list (-result Univ)) Univ 'a)))]
[(-polydots (a) (->... null (Univ a) (-values (list Univ))))
(->* null Univ Univ)]
[(-polydots (a) (->... null (a a) (make-ListDots a 'a)))
(-> -String -Symbol (-Tuple (list -String -Symbol)))]
[(-> -String -Symbol (-Tuple (list -String -Symbol)))
(-polydots (a) (-> -String -Symbol (-lst (Un -String -Symbol))))]
[(-polydots (a) (->... null (a a) (make-ListDots a 'a)))
(-poly (a b) (-> a b (-Tuple (list a b))))]
))
(define-go

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

@ -1392,8 +1392,10 @@
[values (-polydots (b a) (cl->* (->acc (list b) b null)
(null (a a) . ->... . (make-ValuesDots null a 'a))))]
[values (-polydots (a b) (cl->*
(-> (-values null))
(->acc (list a) a null)
((list a) (b b) . ->... . (make-ValuesDots (list (-result a)) b 'b))))]
[call-with-values (-polydots (b a) ((-> (make-ValuesDots null a 'a)) (null (a a) . ->... . b) . -> . b))]
[read-accept-reader (-Param B B)]

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

@ -135,7 +135,8 @@
;; substitute-dotted : Type Name Name Type -> Type
(define (substitute-dotted image image-bound name target)
(define (sb t) (substitute-dotted image image-bound name t))
(if (set-member? (free-vars-names (free-idxs* target)) name)
(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

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

@ -7,6 +7,7 @@
(env type-name-env)
racket/match unstable/match
racket/function
racket/list
racket/lazy-require
(prefix-in c: racket/contract)
(for-syntax racket/base syntax/parse))
@ -357,15 +358,38 @@
[((Poly: ns b1) (Poly: ms b2))
(=> unmatch)
(unless (= (length ns) (length ms))
(unmatch))
(unmatch))
(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))
(=> unmatch)
(unless (= (length ns) (length ms))
(unmatch))
(define subst
(hash-set (make-simple-substitution ms (map make-F ns))
m-dotted (i-subst/dotted null (make-F n-dotted) n-dotted)))
(subtype* A0 b1 (subst-all subst b2))]
[((PolyDots: (list ns ... n-dotted) b1)
(Poly: (list ms ...) b2))
(=> unmatch)
(unless (<= (length ns) (length ms))
(unmatch))
(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))))))
(subtype* A0 (subst-all subst b1) b2)]
[((Refinement: par _ _) t)
(subtype* A0 par t)]
;; 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))]
[(s (Poly: vs b))
[((PolyDots: (list vs ... vdotted) b) s)
(=> unmatch)
(if (infer vs (list vdotted) (list b) (list s) (make-Univ) )
A0
(unmatch))]
[(s (or (Poly: vs b) (PolyDots: vs b)))
(=> unmatch)
(if (null? (fv b)) (subtype* A0 s b) (unmatch))]
;; rec types, applications and names (that aren't the same)
@ -477,7 +501,9 @@
(subtype* A0 parent other)]
;; subtyping on values is pointwise
[((Values: vals1) (Values: vals2)) (subtypes* A0 vals1 vals2)]
[((or (Values: _) (AnyValues:)) (AnyValues:)) A0]
[((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*)]
@ -513,6 +539,7 @@
(provide
type-compare? subtypes/varargs subtypes)
;(require racket/trace)
;(trace subtype*)
;(trace supertype-of-one/arr)
;(trace arr-subtype*/no-fail)