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

This commit is contained in:
Eric Dobson 2014-05-16 21:13:59 -07:00
parent c2fa9d2f73
commit 1aa6c49072
4 changed files with 29 additions and 24 deletions

View File

@ -68,12 +68,6 @@
(define (-opt t) (Un (-val #f) t)) (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 ;; Convenient constructor for Values
;; (wraps arg types with Result) ;; (wraps arg types with Result)
(define/cond-contract (-values args) (define/cond-contract (-values args)

View File

@ -59,10 +59,14 @@
;; Void is needed for Params ;; Void is needed for Params
(define/decl -Void (make-Base 'Void #'void? void? #f)) (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 -pair make-Pair)
(define (-lst* #:tail [tail -Null] . args) (define (-lst* #:tail [tail -Null] . args)
(for/fold ([tl tail]) ([a (in-list (reverse args))]) (-pair a tl))) (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 ;; Simple union type constructor, does not check for overlaps
;; Normalizes representation by sorting types. ;; Normalizes representation by sorting types.

View File

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

View File

@ -10,12 +10,18 @@
(define-syntax-rule (s img var tgt result) (define-syntax-rule (s img var tgt result)
(test-eq? (format "~a" '(img tgt)) (substitute 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) (define-syntax-rule (s... imgs var tgt result)
(test-eq? (format "~a" '(img tgt)) (substitute-dots (list . imgs) #f 'var tgt) result)) (test-eq? (format "~a" '(img tgt)) (substitute-dots (list . imgs) #f 'var tgt) result))
(define tests (define tests
(test-suite "Tests for substitution" (test-suite "Tests for substitution"
(s -Number a (-v a) -Number) (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 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 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) 'a))) (-String (-v b) (-v b) . -> . -Number))