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

Correct subst/dots on list-dots and values-dots.

Browse Source 
original commit: 1aa6c490726e575198dff088b3084bd1a6df3fed
This commit is contained in:
Eric Dobson 2014-05-16 21:13:59 -07:00
parent b915674d2b
commit db297fc328
4 changed files with 29 additions and 24 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/abbrev.rkt
View File

@ -68,12 +68,6 @@
(define (-opt t) (Un (-val #f) t))
(define (-Tuple l)
(-Tuple* l -Null))
(define (-Tuple* l b)
(foldr -pair b l))
;; Convenient constructor for Values
;; (wraps arg types with Result)
(define/cond-contract (-values args)

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

@ -59,10 +59,14 @@
;; Void is needed for Params
(define/decl -Void (make-Base 'Void #'void? void? #f))
;; -lst* Type is needed by substitute for ListDots
;; -Tuple Type is needed by substitute for ListDots
(define -pair make-Pair)
(define (-lst* #:tail [tail -Null] . args)
(for/fold ([tl tail]) ([a (in-list (reverse args))]) (-pair a tl)))
(define (-Tuple l)
(-Tuple* l -Null))
(define (-Tuple* l b)
(foldr -pair b l))
;; Simple union type constructor, does not check for overlaps
;; Normalizes representation by sorting types.

23
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/substitute.rkt
View File

@ -4,7 +4,7 @@
racket/match racket/set
racket/lazy-require
(contract-req)
(only-in (types base-abbrev) -lst* -result)
(only-in (types base-abbrev) -Tuple* -lst -Null -result ManyUniv)
(rep type-rep rep-utils)
(utils tc-utils)
(rep free-variance)
@ -99,19 +99,21 @@
(if (eq? name dbound)
;; We need to recur first, just to expand out any dotted usages of this.
(let ([expanded (sb dty)])
(for/fold ([t (make-Value null)])
(for/fold ([t (if rimage (-lst rimage) -Null)])
([img (in-list (reverse images))])
(make-Pair (substitute img name expanded) t)))
(make-ListDots (sb dty) dbound))]
[#:ValuesDots types dty dbound
(if (eq? name dbound)
(make-Values
(append
(map sb types)
;; We need to recur first, just to expand out any dotted usages of this.
(let ([expanded (sb dty)])
(for/list ([img (in-list images)])
(-result (substitute img name expanded))))))
(if rimage
ManyUniv
(make-Values
(append
(map sb types)
;; We need to recur first, just to expand out any dotted usages of this.
(let ([expanded (sb dty)])
(for/list ([img (in-list images)])
(-result (substitute img name expanded)))))))
(make-ValuesDots (map sb types) (sb dty) dbound))]
[#:arr dom rng rest drest kws
(if (and (pair? drest)
@ -148,9 +150,8 @@
(sb dty)
(if (eq? name dbound) image-bound dbound)))]
[#:ListDots dty dbound
(apply -lst*
(-Tuple*
(if (eq? name dbound) pre-image null)
#:tail
(make-ListDots (sb dty)
(if (eq? name dbound) image-bound dbound)))]
[#:F name*

18
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/subst-tests.rkt
View File

@ -10,14 +10,20 @@
(define-syntax-rule (s img var tgt result)
(test-eq? (format "~a" '(img tgt)) (substitute img 'var tgt) result))
(define-syntax-rule (s* imgs rest var tgt result)
(test-eq? (format "~a" '(img tgt)) (substitute-dots (list . imgs) rest 'var tgt) result))
(define-syntax-rule (s... imgs var tgt result)
(test-eq? (format "~a" '(img tgt)) (substitute-dots (list . imgs) #f 'var tgt) result))
(define tests
(test-suite "Tests for substitution"
(s -Number a (-v a) -Number)
(s... (-Number -Boolean) a (make-Function (list (make-arr-dots null -Number (-v a) 'a))) (-Number -Boolean . -> . -Number))
(s... (-Number -Boolean) a (make-Function (list (make-arr-dots (list -String) -Number (-v a) 'a))) (-String -Number -Boolean . -> . -Number))
(s... (-Number -Boolean) a (make-Function (list (make-arr-dots (list -String) -Number (-v b) 'a))) (-String (-v b) (-v b) . -> . -Number))
(s... (-Number -Boolean) a (make-Function (list (make-arr-dots (list -String) -Number (-v b) 'b)))
(make-Function (list (make-arr-dots (list -String) -Number (-v b) 'b))))))
(s -Number a (-v a) -Number)
(s* (-Symbol -String) #f a (make-ListDots (-v a) 'a) (-lst* -Symbol -String))
(s* (-Symbol -String) Univ a (make-ListDots (-v a) 'a) (-lst* -Symbol -String #:tail (-lst Univ)))
(s... (-Number -Boolean) a (make-Function (list (make-arr-dots null -Number (-v a) 'a))) (-Number -Boolean . -> . -Number))
(s... (-Number -Boolean) a (make-Function (list (make-arr-dots (list -String) -Number (-v a) 'a))) (-String -Number -Boolean . -> . -Number))
(s... (-Number -Boolean) a (make-Function (list (make-arr-dots (list -String) -Number (-v b) 'a))) (-String (-v b) (-v b) . -> . -Number))
(s... (-Number -Boolean) a (make-Function (list (make-arr-dots (list -String) -Number (-v b) 'b)))
(make-Function (list (make-arr-dots (list -String) -Number (-v b) 'b))))))