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

Make PolyDots be subtypes even if they have different fixed arguments.

Browse Source 
original commit: 75f89107b1449deda042b62feaebb9b9bf3c92ec
This commit is contained in:
Eric Dobson 2013-02-26 23:25:19 -08:00
parent 57a60ad403
commit 02c4f0dd11
6 changed files with 46 additions and 31 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -206,6 +206,12 @@
[(-polydots (a) (->... null (a a) (make-ListDots a 'a)))
(-poly (a b) (-> a b (-Tuple (list a b))))]
[(-polydots (b a) (-> (->... (list b) (a a) (make-ValuesDots (list (-result b)) a 'a)) Univ))
(-polydots (a) (-> (->... (list) (a a) (make-ValuesDots null a 'a)) Univ))]
[(-polydots (a) (->... (list) (a a) (make-ListDots a 'a)))
(-polydots (b a) (->... (list b) (a a) (-pair b (make-ListDots a 'a))))]
))
(define-go

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

@ -33,7 +33,6 @@
(define -App make-App)
(define -pair make-Pair)
(define -mpair make-MPair)
(define -Param make-Param)
(define -box make-Box)
@ -51,8 +50,6 @@
(define (-lst* #:tail [tail (-val null)] . args)
(for/fold ([tl tail]) ([a (reverse args)]) (-pair a tl)))
(define (-Tuple l)
(foldr -pair (-val '()) l))

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

@ -32,6 +32,11 @@
;; Void is needed for Params
(define -Void (make-Base 'Void #'void? void? #'-Void #f))
;; -lst* Type is needed by substitute for ListDots
(define -pair make-Pair)
(define (-lst* #:tail [tail (-val null)] . args)
(for/fold ([tl tail]) ([a (reverse args)]) (-pair a tl)))
;; Simple union type, does not check for overlaps

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

@ -5,6 +5,7 @@
(utils tc-utils)
(rep free-variance)
(env index-env tvar-env)
(only-in (types base-abbrev) -lst* -result)
racket/match
racket/set
racket/contract
@ -133,31 +134,36 @@
;; implements curly brace substitution from the formalism
;; 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))
(define (substitute-dotted pre-image image image-bound name target)
(define (sb t) (substitute-dotted pre-image image image-bound name t))
(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
(make-ValuesDots (map sb types)
(sb dty)
(if (eq? name dbound) image-bound dbound))]
(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)))]
[#:ListDots dty dbound
(make-ListDots (sb dty)
(if (eq? name dbound) image-bound dbound))]
(apply -lst*
(if (eq? name dbound) pre-image null)
#:tail
(make-ListDots (sb dty)
(if (eq? name dbound) image-bound dbound)))]
[#:F name*
(if (eq? name* name)
image
target)]
[#:arr dom rng rest drest kws
(make-arr (map sb dom)
(sb rng)
(and rest (sb rest))
(and drest
(cons (substitute image (cdr drest) (sb (car drest)))
(if (eq? name (cdr drest)) image-bound (cdr drest))))
(map sb kws))])
(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))
(and drest
(cons (substitute image (cdr drest) (sb (car drest)))
(if (eq? name (cdr drest)) image-bound (cdr drest))))
(map sb kws)))])
target))
;; substitute many variables
@ -174,7 +180,6 @@
[_ acc])))
(define t-substed-ty (substitute-many t-substs ty))
(for/fold ([t t-substed-ty]) ([(v r) (in-hash s)])
(match r
[(t-subst img) t]
@ -182,9 +187,5 @@
(substitute-dots imgs #f v t)]
[(i-subst/starred imgs rest)
(substitute-dots imgs rest v t)]
[(i-subst/dotted null dty dbound)
(substitute-dotted dty dbound v t)]
[(i-subst/dotted imgs dty dbound)
(int-err "i-subst/dotted nyi")
#;
(substitute-dotted imgs rest v t)])))
(substitute-dotted imgs dty dbound v t)])))

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

@ -362,13 +362,19 @@
(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))]
(cond
((< (length ns) (length ms))
(define-values (short-ms rest-ms) (split-at ms (length ns)))
(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
(define-values (short-ns rest-ns) (split-at ns (length ms)))
(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))))]
[((PolyDots: (list ns ... n-dotted) b1)
(Poly: (list ms ...) b2))
(=> unmatch)

2
collects/typed-racket/types/utils.rkt
View File

@ -51,7 +51,7 @@
" types: expected ~a, got ~a, types were ~a")
(length fixed) (length types) types))
(let ([body* (subst-all (make-simple-substitution fixed types) body)])
(substitute-dotted image var dotted body*))]
(substitute-dotted null image var dotted body*))]
[_ (int-err "instantiate-poly-dotted: requires PolyDots type, got ~a" t)]))