From 30f8b22021e72c3e86404825a9aa0f3387b1d2e7 Mon Sep 17 00:00:00 2001 From: Eric Dobson Date: Sun, 11 May 2014 10:18:37 -0700 Subject: [PATCH] Switch input from arities to sequences. original commit: 03ad77afd4b3d2370dce572ff563bff4cfdaaf63 --- .../typed-racket/infer/infer-unit.rkt | 111 ++++++++++-------- .../typed-racket/unit-tests/infer-tests.rkt | 2 + 2 files changed, 67 insertions(+), 46 deletions(-) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt index 7a365fc0..1e725ac9 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt @@ -145,6 +145,15 @@ [(dcon-exact null rest) rest] [_ (int-err "did not get a rest-only dcon when moving to the dmap")]))))) +;; Represents a sequence of types. types are the fixed prefix, and end is the remaining types +;; This is a unification of all of the dotted types that exist ListDots, ->..., and ValuesDots. +;; This allows for one implementation of the cgen algorithm for dotted types to be shared across all +;; of them. +(struct seq (types end) #:transparent) +(struct null-end () #:transparent) +(struct uniform-end (type) #:transparent) +(struct dotted-end (type bound) #:transparent) + ;; Maps dotted vars (combined with dotted types, to ensure global uniqueness) ;; to "fresh" symbols. @@ -201,30 +210,32 @@ (define/cond-contract (cgen/arr V X Y s-arr t-arr) ((listof symbol?) (listof symbol?) (listof symbol?) arr? arr? . -> . (or/c #f cset?)) ;; Loop does not handle the return type or the keywords as they are handled before - (define (loop V X Y s-arr t-arr) + ;; Currently checks is t-seq <: s-seq. Which works because argument list are contravariant. + (define (loop V X Y s-seq t-seq) (define (cg S T) (cgen V X Y S T)) - (match*/early (s-arr t-arr) - ;; the simplest case - no rests, drests, keywords - [((arr: ss _ #f #f _) - (arr: ts _ #f #f _)) - (cgen/list V X Y ts ss)] ;; contravariant - ;; just a rest arg, no drest, no keywords - [((arr: ss _ s-rest #f _) - (arr: ts _ t-rest #f _)) - (cond - ;; both rest args are present, so make them the same length - [(and s-rest t-rest) - (cgen/list V X Y - (cons t-rest (extend ss ts t-rest)) - (cons s-rest (extend ts ss s-rest)))] - ;; no rest arg on the right, so just pad the left and forget the rest arg - [(and s-rest (not t-rest) (<= (length ss) (length ts))) - (cgen/list V X Y ts (extend ts ss s-rest))] - ;; no rest arg on the left, or wrong number = fail - [else #f])] + (match*/early (s-seq t-seq) + ;; The simplest case - both are null-end + [((seq ss (null-end)) + (seq ts (null-end))) + (cgen/list V X Y ts ss)] + ;; One is null-end the other is uniform-end + [((seq ss (null-end)) + (seq ts (uniform-end t-rest))) + #f] + [((seq ss (uniform-end s-rest)) + (seq ts (null-end))) + (and + (<= (length ss) (length ts))) + (cgen/list V X Y ts (extend ts ss s-rest))] + ;; Both are uniform-end + [((seq ss (uniform-end s-rest)) + (seq ts (uniform-end t-rest))) + (cgen/list V X Y + (cons t-rest (extend ss ts t-rest)) + (cons s-rest (extend ts ss s-rest)))] ;; dotted on the left, nothing on the right - [((arr: ss s #f (cons dty dbound) s-kws) - (arr: ts _ #f #f _)) + [((seq ss (dotted-end dty dbound)) + (seq ts (null-end))) #:return-unless (memq dbound Y) #f #:return-unless (<= (length ss) (length ts)) @@ -232,12 +243,12 @@ (let* ([vars (var-store-take dbound dty (- (length ts) (length ss)))] [new-tys (for/list ([var (in-list vars)]) (substitute (make-F var) dbound dty))] - [new-s-arr (make-arr (append ss new-tys) s #f #f s-kws)] - [new-cset (loop V (append vars X) Y new-s-arr t-arr)]) + [new-s-seq (seq (append ss new-tys) (null-end))] + [new-cset (loop V (append vars X) Y new-s-seq t-seq)]) (% move-vars-to-dmap new-cset dbound vars))] ;; dotted on the right, nothing on the left - [((arr: ss _ #f #f _) - (arr: ts t #f (cons dty dbound) t-kws)) + [((seq ss (null-end)) + (seq ts (dotted-end dty dbound))) #:return-unless (memq dbound Y) #f #:return-unless (<= (length ts) (length ss)) @@ -245,12 +256,12 @@ (let* ([vars (var-store-take dbound dty (- (length ss) (length ts)))] [new-tys (for/list ([var (in-list vars)]) (substitute (make-F var) dbound dty))] - [new-t-arr (make-arr (append ts new-tys) t #f #f t-kws)] - [new-cset (loop V (append vars X) Y s-arr new-t-arr)]) + [new-t-seq (seq (append ts new-tys) (null-end))] + [new-cset (loop V (append vars X) Y s-seq new-t-seq)]) (% move-vars-to-dmap new-cset dbound vars))] ;; this case is just for constrainting other variables, not dbound - [((arr: ss _ #f (cons s-dty dbound) _) - (arr: ts _ #f (cons t-dty dbound) _)) + [((seq ss (dotted-end s-dty dbound)) + (seq ts (dotted-end t-dty dbound))) #:return-unless (= (length ss) (length ts)) #f ;; If we want to infer the dotted bound, then why is it in both types? @@ -260,8 +271,8 @@ [darg-mapping (cgen V X Y t-dty s-dty)]) (% cset-meet arg-mapping darg-mapping))] ;; bounds are different - [((arr: ss _ #f (cons s-dty (? (λ (db) (memq db Y)) dbound)) _) - (arr: ts _ #f (cons t-dty dbound*) _)) + [((seq ss (dotted-end s-dty (? (λ (db) (memq db Y)) dbound))) + (seq ts (dotted-end t-dty dbound*))) #:return-unless (= (length ss) (length ts)) #f #:return-when (memq dbound* Y) #f (let* ([arg-mapping (cgen/list V X Y ts ss)] @@ -270,8 +281,8 @@ (extend-tvars (list dbound*) (% move-dotted-rest-to-dmap (cgen V (cons dbound X) Y t-dty s-dty) dbound dbound*))]) (% cset-meet arg-mapping darg-mapping))] - [((arr: ss _ #f (cons s-dty dbound) _) - (arr: ts _ #f (cons t-dty (? (λ (db) (memq db Y)) dbound*)) _)) + [((seq ss (dotted-end s-dty dbound)) + (seq ts (dotted-end t-dty (? (λ (db) (memq db Y)) dbound*)))) #:return-unless (= (length ss) (length ts)) #f (let* ([arg-mapping (cgen/list V X Y ts ss)] ;; just add dbound as something that can be constrained @@ -280,8 +291,8 @@ (% move-dotted-rest-to-dmap (cgen V (cons dbound* X) Y t-dty s-dty) dbound* dbound))]) (% cset-meet arg-mapping darg-mapping))] ;; * <: ... - [((arr: ss _ s-rest #f _) - (arr: ts t #f (cons t-dty dbound) t-kws)) + [((seq ss (uniform-end s-rest)) + (seq ts (dotted-end t-dty dbound))) #:return-unless (memq dbound Y) #f (if (<= (length ss) (length ts)) @@ -294,12 +305,12 @@ (let* ([vars (var-store-take dbound t-dty (- (length ss) (length ts)))] [new-tys (for/list ([var (in-list vars)]) (substitute (make-F var) dbound t-dty))] - [new-t-arr (make-arr (append ts new-tys) t #f (cons t-dty dbound) t-kws)] - [new-cset (loop V (append vars X) Y s-arr new-t-arr)]) + [new-t-seq (seq (append ts new-tys) (dotted-end t-dty dbound))] + [new-cset (loop V (append vars X) Y s-seq new-t-seq)]) (% move-vars+rest-to-dmap new-cset dbound vars)))] ;; If dotted <: starred is correct, add it below. Not sure it is. - [((arr: ss s #f (cons s-dty dbound) s-kws) - (arr: ts _ t-rest #f _)) + [((seq ss (dotted-end s-dty dbound)) + (seq ts (uniform-end t-rest))) #:return-unless (memq dbound Y) #f (cond [(< (length ss) (length ts)) @@ -307,8 +318,8 @@ (let* ([vars (var-store-take dbound s-dty (- (length ts) (length ss)))] [new-tys (for/list ([var (in-list vars)]) (substitute (make-F var) dbound s-dty))] - [new-s-arr (make-arr (append ss new-tys) s #f (cons s-dty dbound) s-kws)] - [new-cset (loop V (append vars X) Y new-s-arr t-arr)]) + [new-s-seq (make-arr (append ss new-tys) (dotted-end s-dty dbound))] + [new-cset (loop V (append vars X) Y new-s-seq t-seq)]) (% move-vars+rest-to-dmap new-cset dbound vars #:exact #t))] [(= (length ss) (length ts)) ;; the simple case @@ -316,15 +327,23 @@ [rest-mapping (cgen V (cons dbound X) Y t-rest s-dty)] [darg-mapping (% move-rest-to-dmap rest-mapping dbound #:exact #t)]) (% cset-meet arg-mapping darg-mapping))] - [else #f])] - [(_ _) #f])) + [else #f])])) + (match* (s-arr t-arr) - [((arr: _ s _ _ s-kws) (arr: _ t _ _ t-kws)) + [((arr: ss s s-rest s-drest s-kws) (arr: ts t t-rest t-drest t-kws)) + (define (rest->end rest drest) + (cond + [rest (uniform-end rest)] + [drest (dotted-end (car drest) (cdr drest))] + [else (null-end)])) + + (define s-seq (seq ss (rest->end s-rest s-drest))) + (define t-seq (seq ts (rest->end t-rest t-drest))) (and (null? s-kws) (null? t-kws) (% cset-meet (cgen V X Y s t) - (loop V X Y s-arr t-arr)))])) + (loop V X Y s-seq t-seq)))])) (define/cond-contract (cgen/flds V X Y flds-s flds-t) ((listof symbol?) (listof symbol?) (listof symbol?) (listof fld?) (listof fld?) diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/infer-tests.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/infer-tests.rkt index d6aacfc7..66fabf0f 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/infer-tests.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/infer-tests.rkt @@ -159,6 +159,7 @@ [i2-t (-lst (-v a)) (-lst* N B) ('a (Un N B))] [i2-t Univ (Un N B)] [i2-t ((-v a) . -> . (-v b)) (-> N N) ('b N) ('a (Un))] + [i2-t (-> (-v a) (-v a)) (->* null B B) ('a B)] [i2-l (list (-v a) (-v a) (-v b)) @@ -175,6 +176,7 @@ '(a) ('a (Un N B))] ;; error tests [i2-f (-lst (-v a)) Univ] + [i2-f (->* null B B) (-> (-v a) (-v b))] ))