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

Major revision of subtyping code for performance.

Browse Source 
Improves tests/typed-racket/succeed/new-metrics.rkt by about 33% overall runtime.

Major changes include:
 - Handling memoization entirely inside the `subtype*` function.
 - Remembering only previously seen pairs of types when one of them
   might be a recursive type (such as Mu or a structure).
   Thanks to Ryan Newtown for this this idea, which enables the
   previous change as well.
 - Doing as much as possible without touching parameters.
   (Unfortunately, not as much as I hoped was possible here).
 - Replacing uses of => in `match` with #:when (written for this purpose).
 - Significant improvement to the `Type-key` system so that it is
   useful much more often.
 - Use of unsafe operations.
 - Minor optimizations to a few other operations.
This commit is contained in:
Sam Tobin-Hochstadt 2013-10-20 22:37:01 -04:00
parent d13afa0f78
commit 0a6537a6cb
5 changed files with 405 additions and 384 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/rep/rep-utils.rkt
View File

@ -7,6 +7,7 @@
"interning.rkt" "interning.rkt"
racket/lazy-require racket/lazy-require
racket/stxparam racket/stxparam
racket/unsafe/ops
(for-syntax (for-syntax
racket/match racket/match
(except-in syntax/parse id identifier keyword) (except-in syntax/parse id identifier keyword)
@ -353,6 +354,11 @@
[Object def-object #:Object object-case print-object object-name-ht object-rec-id] [Object def-object #:Object object-case print-object object-name-ht object-rec-id]
[PathElem def-pathelem #:PathElem pathelem-case print-pathelem pathelem-name-ht pathelem-rec-id]) [PathElem def-pathelem #:PathElem pathelem-case print-pathelem pathelem-name-ht pathelem-rec-id])
;; NOTE: change these if the definitions above change, or everything will segfault
(define-syntax-rule (unsafe-Rep-seq v) (unsafe-struct*-ref v 0))
(define-syntax-rule (unsafe-Type-key v) (unsafe-struct*-ref v 1))
(provide unsafe-Rep-seq unsafe-Type-key)
(define (Rep-values rep) (define (Rep-values rep)
(match rep (match rep
[(? (lambda (e) (or (Filter? e) [(? (lambda (e) (or (Filter? e)

40
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/rep/type-rep.rkt
View File

@ -8,7 +8,7 @@
;; TODO use contract-req ;; TODO use contract-req
(require (utils tc-utils) (require (utils tc-utils)
"rep-utils.rkt" "object-rep.rkt" "filter-rep.rkt" "free-variance.rkt" "rep-utils.rkt" "object-rep.rkt" "filter-rep.rkt" "free-variance.rkt"
racket/match racket/match racket/list
racket/contract racket/contract
racket/lazy-require racket/lazy-require
(for-syntax racket/base syntax/parse)) (for-syntax racket/base syntax/parse))
@ -100,11 +100,13 @@
;; free type variables ;; free type variables
;; n is a Name ;; n is a Name
(def-type F ([n symbol?]) [#:frees (single-free-var n) empty-free-vars] [#:fold-rhs #:base]) (def-type F ([n symbol?]) [#:frees (single-free-var n) empty-free-vars]
[#:fold-rhs #:base])
;; id is an Identifier ;; id is an Identifier
;; This will always resolve to a struct ;; This will always resolve to a struct
(def-type Name ([id identifier?]) [#:intern (hash-id id)] [#:frees #f] [#:fold-rhs #:base]) (def-type Name ([id identifier?]) [#:intern (hash-id id)] [#:frees #f]
[#:fold-rhs #:base])
;; rator is a type ;; rator is a type
;; rands is a list of types ;; rands is a list of types
@ -180,7 +182,7 @@
;; elem is a Type ;; elem is a Type
(def-type Set ([elem Type/c]) (def-type Set ([elem Type/c])
[#:key 'set]) [#:key #f])
;; result is a Type ;; result is a Type
(def-type Evt ([result Type/c]) (def-type Evt ([result Type/c])
@ -197,7 +199,6 @@
[#:key (if numeric? [#:key (if numeric?
'number 'number
(case name (case name
[(Number Integer) 'number]
[(Boolean) 'boolean] [(Boolean) 'boolean]
[(String) 'string] [(String) 'string]
[(Symbol) 'symbol] [(Symbol) 'symbol]
@ -375,10 +376,13 @@
[#:fold-rhs #:base] [#:key 'continuation-mark-key]) [#:fold-rhs #:base] [#:key 'continuation-mark-key])
;; v : Racket Value ;; v : Racket Value
(def-type Value (v) [#:frees #f] [#:fold-rhs #:base] [#:key (cond [(number? v) 'number] (def-type Value (v) [#:frees #f] [#:fold-rhs #:base]
[(boolean? v) 'boolean] [#:key (cond [(or (eq? v 0) (eq? v 1)) 'number]
[(null? v) 'null] ;; other numbers don't work with the optimizations in subtype.rkt
[else #f])]) ;; which assume that unions of numbers are subtyped in simple ways
[(boolean? v) 'boolean]
[(null? v) 'null]
[else #f])])
;; elems : Listof[Type] ;; elems : Listof[Type]
(def-type Union ([elems (and/c (listof Type/c) (def-type Union ([elems (and/c (listof Type/c)
@ -394,12 +398,18 @@
sorted?))))]) sorted?))))])
[#:frees (λ (f) (combine-frees (map f elems)))] [#:frees (λ (f) (combine-frees (map f elems)))]
[#:fold-rhs (apply Un (map type-rec-id elems))] [#:fold-rhs (apply Un (map type-rec-id elems))]
[#:key (let loop ([res null] [ts elems]) [#:key
(if (null? ts) res (let ()
(let ([k (Type-key (car ts))]) (define d
(cond [(pair? k) (loop (append k res) (cdr ts))] (let loop ([ts elems] [res null])
[k (loop (cons k res) (cdr ts))] (cond [(null? ts) res]
[else #f]))))]) [else
(define k (Type-key (car ts)))
(cond [(not k) (list #f)]
[(pair? k) (loop (cdr ts) (append k res))]
[else (loop (cdr ts) (cons k res))])])))
(define d* (remove-duplicates d))
(if (and (pair? d*) (null? (cdr d*))) (car d*) d*))])
(def-type Univ () [#:frees #f] [#:fold-rhs #:base]) (def-type Univ () [#:frees #f] [#:fold-rhs #:base])

16
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/current-seen.rkt
View File

@ -1,5 +1,5 @@
#lang racket/base #lang racket/base
(require "../utils/utils.rkt") (require "../utils/utils.rkt" racket/unsafe/ops)
(require (rep type-rep) (contract-req)) (require (rep type-rep) (contract-req))
(provide (except-out (all-defined-out) current-seen)) (provide (except-out (all-defined-out) current-seen))
@ -7,8 +7,16 @@
(define current-seen (make-parameter null)) (define current-seen (make-parameter null))
(define (currently-subtyping?) (not (null? (current-seen)))) (define (currently-subtyping?) (not (null? (current-seen))))
(define (seen-before s t) (cons (Type-seq s) (Type-seq t))) (define (seen-before s t) (cons (Type-seq s) (Type-seq t)))
(define (remember s t A) (cons (seen-before s t) A))
(define (seen? s t) (member (seen-before s t) (current-seen))) (define (remember s t A)
(if (or (Mu? s) (Mu? t)
(Name? s) (Name? t)
(Struct? s) (Struct? t)
(App? s) (App? t))
(cons (seen-before s t) A)
A))
(define (seen? ss st cs)
(for/or ([i (in-list cs)])
(and (eq? ss (unsafe-car i)) (eq? st (unsafe-cdr i)))))

725
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/subtype.rkt
View File

@ -1,6 +1,7 @@
#lang racket/base #lang racket/base
(require (except-in "../utils/utils.rkt" infer) (require (except-in "../utils/utils.rkt" infer)
racket/match racket/function racket/lazy-require racket/list racket/match racket/function racket/lazy-require racket/list
racket/unsafe/ops
(prefix-in c: (contract-req)) (prefix-in c: (contract-req))
(rep type-rep filter-rep object-rep rep-utils) (rep type-rep filter-rep object-rep rep-utils)
(utils tc-utils) (utils tc-utils)
@ -13,12 +14,6 @@
("../infer/infer.rkt" (infer))) ("../infer/infer.rkt" (infer)))
(define subtype-cache (make-hash)) (define subtype-cache (make-hash))
(define (cache-types s t)
(cache-keys (Type-seq s) (Type-seq t)))
(define (cache-keys ks kt)
(hash-set! subtype-cache (cons ks kt) #t))
(define (cached? s t)
(hash-ref subtype-cache (cons (Type-seq s) (Type-seq t)) #f))
(define-syntax-rule (handle-failure e) (define-syntax-rule (handle-failure e)
e) e)
@ -27,10 +22,7 @@
;; type type -> boolean ;; type type -> boolean
(define/cond-contract (subtype s t) (define/cond-contract (subtype s t)
(c:-> (c:or/c Type/c SomeValues/c) (c:or/c Type/c SomeValues/c) boolean?) (c:-> (c:or/c Type/c SomeValues/c) (c:or/c Type/c SomeValues/c) boolean?)
(define k (cons (Type-seq s) (Type-seq t))) (and (subtype* (current-seen) s t) #t))
((if (currently-subtyping?) hash-ref hash-ref!)
subtype-cache k
(lambda () (and (subtype* (current-seen) s t) #t))))
;; are all the s's subtypes of all the t's? ;; are all the s's subtypes of all the t's?
;; [type] [type] -> boolean ;; [type] [type] -> boolean
@ -221,366 +213,371 @@
(subtype* s t) (subtype* s t)
(subtype* t s))) (subtype* t s)))
(define-syntax (early-return stx)
(syntax-parse stx
[(_ e:expr ... #:return-when e0:expr e1:expr rest ...)
#'(let ()
e ...
(if e0 e1
(early-return rest ...)))]
[(_ e:expr ...) #'(let () e ...)]))
(define bottom-key (Rep-seq -Bottom))
(define top-key (Rep-seq Univ))
;; the algorithm for recursive types transcribed directly from TAPL, pg 305 ;; the algorithm for recursive types transcribed directly from TAPL, pg 305
;; List[(cons Number Number)] type type -> List[(cons Number Number)] ;; List[(cons Number Number)] type type -> List[(cons Number Number)] or #f
;; potentially raises exn:subtype, when the algorithm fails ;; is s a subtype of t, taking into account previously seen pairs A
;; is s a subtype of t, taking into account constraints A
(define/cond-contract (subtype* A s t) (define/cond-contract (subtype* A s t)
(c:-> list? Type? Type? c:any/c) (c:-> (listof (cons/c fixnum? fixnum?)) Type? Type? c:any/c)
(define =t (lambda (a b) (if (and (Rep? a) (Rep? b)) (type-equal? a b) (equal? a b)))) (define ss (unsafe-Rep-seq s))
(parameterize ([match-equality-test =t] (define st (unsafe-Rep-seq t))
[current-seen A]) (early-return
(let ([ks (Type-key s)] [kt (Type-key t)]) #:return-when (or (eq? ss st) (seen? ss st A)) A
(cond (define cr (hash-ref subtype-cache (cons ss st) 'missing))
[(or (seen? s t) (type-equal? s t)) A] #:return-when (boolean? cr) (and cr A)
[(and (symbol? ks) (symbol? kt) (not (eq? ks kt))) #f] (define ks (unsafe-Type-key s))
[(and (symbol? ks) (pair? kt) (not (memq ks kt))) #f] (define kt (unsafe-Type-key t))
[(and (pair? ks) (pair? kt) #:return-when (and (symbol? ks) (symbol? kt) (not (eq? ks kt))) #f
(for/and ([i (in-list ks)]) (not (memq i kt)))) #:return-when (and (symbol? ks) (pair? kt) (not (memq ks kt))) #f
#f] #:return-when
[else (and (pair? ks) (pair? kt)
(let* ([A0 (remember s t A)]) (for/and ([i (in-list ks)]) (not (memq i kt))))
(parameterize ([current-seen A0]) #f
(match* (s t) #:return-when (eq? ss bottom-key) A
[(_ (Univ:)) A0] #:return-when (eq? st top-key) A
[((or (ValuesDots: _ _ _) (Values: _) (AnyValues:)) (AnyValues:)) A0] (define A0 (remember s t A))
;; error is top and bot (define r
[(_ (Error:)) A0] ;; FIXME -- make this go into only the places that need it -- slows down new-metrics.rkt significantly
[((Error:) _) A0] (parameterize ([current-seen A0])
;; (Un) is bot (match* (s t)
[(_ (Union: (list))) #f] ;; these cases are above as special cases
[((Union: (list)) _) A0] ;; [((Union: (list)) _) A0] ;; this is extremely common, so it goes first
;; value types ;; [(_ (Univ:)) A0]
[((Value: v1) (Value: v2)) (=> unmatch) (if (equal? v1 v2) A0 (unmatch))] [((or (ValuesDots: _ _ _) (Values: _) (AnyValues:)) (AnyValues:)) A0]
;; values are subtypes of their "type" ;; error is top and bot
[((Value: v) (Base: _ _ pred _)) (if (pred v) A0 #f)] [(_ (Error:)) A0]
;; tvars are equal if they are the same variable [((Error:) _) A0]
[((F: t) (F: t*)) (if (eq? t t*) A0 #f)] ;; (Un) is bot
;; Avoid needing to resolve things that refer to different structs. [(_ (Union: (list))) #f]
;; Saves us from non-termination ;; value types
;; Must happen *before* the sequence cases, which sometimes call `resolve' in match expanders [((Value: v1) (Value: v2))
[((or (? Struct? s1) (NameStruct: s1)) (or (? Struct? s2) (NameStruct: s2))) #:when (equal? v1 v2) A0]
(=> unmatch) ;; values are subtypes of their "type"
(cond [(unrelated-structs s1 s2) [((Value: v) (Base: _ _ pred _)) (if (pred v) A0 #f)]
;(dprintf "found unrelated structs: ~a ~a\n" s1 s2) ;; tvars are equal if they are the same variable
#f] [((F: t) (F: t*)) (if (eq? t t*) A0 #f)]
[else (unmatch)])] ;; Avoid needing to resolve things that refer to different structs.
;; similar case for structs and base types, which are obviously unrelated ;; Saves us from non-termination
[((Base: _ _ _ _) (or (? Struct? s1) (NameStruct: s1))) ;; Must happen *before* the sequence cases, which sometimes call `resolve' in match expanders
#f] [((or (? Struct? s1) (NameStruct: s1)) (or (? Struct? s2) (NameStruct: s2)))
[((or (? Struct? s1) (NameStruct: s1)) (Base: _ _ _ _)) #:when (unrelated-structs s1 s2)
#f] #f]
;; same for all values. ;; similar case for structs and base types, which are obviously unrelated
[((Value: (? (negate struct?) _)) (or (? Struct? s1) (NameStruct: s1))) [((Base: _ _ _ _) (or (? Struct? s1) (NameStruct: s1)))
#f] #f]
[((or (? Struct? s1) (NameStruct: s1)) (Value: (? (negate struct?) _))) [((or (? Struct? s1) (NameStruct: s1)) (Base: _ _ _ _))
#f] #f]
;; just checking if s/t is a struct misses recursive/union/etc cases ;; same for all values.
[((? (lambda (_) (eq? ks 'struct))) (Base: _ _ _ _)) #f] [((Value: (? (negate struct?) _)) (or (? Struct? s1) (NameStruct: s1)))
[((Base: _ _ _ _) (? (lambda (_) (eq? kt 'struct)))) #f] #f]
;; sequences are covariant [((or (? Struct? s1) (NameStruct: s1)) (Value: (? (negate struct?) _)))
[((Sequence: ts) (Sequence: ts*)) #f]
(subtypes* A0 ts ts*)] ;; sequences are covariant
[((Listof: t) (Sequence: (list t*))) [((Sequence: ts) (Sequence: ts*))
(subtype* A0 t t*)] (subtypes* A0 ts ts*)]
[((Pair: t1 t2) (Sequence: (list t*))) [((Listof: t) (Sequence: (list t*)))
(subtype-seq A0 (subtype* t1 t*) (subtype* t2 (-lst t*)))] (subtype* A0 t t*)]
[((MListof: t) (Sequence: (list t*))) [((Pair: t1 t2) (Sequence: (list t*)))
(subtype* A0 t t*)] (subtype-seq A0 (subtype* t1 t*) (subtype* t2 (-lst t*)))]
;; To check that mutable pair is a sequence we check that the cdr [((MListof: t) (Sequence: (list t*)))
;; is both an mutable list and a sequence (subtype* A0 t t*)]
[((MPair: t1 t2) (Sequence: (list t*))) ;; To check that mutable pair is a sequence we check that the cdr
(subtype-seq A0 ;; is both an mutable list and a sequence
(subtype* t1 t*) [((MPair: t1 t2) (Sequence: (list t*)))
(subtype* t2 (simple-Un (-val null) (make-MPairTop))) (subtype-seq A0
(subtype* t2 t))] (subtype* t1 t*)
[((List: ts) (Sequence: (list t*))) (subtype* t2 (simple-Un (-val null) (make-MPairTop)))
(subtypes* A0 ts (map (λ (_) t*) ts))] (subtype* t2 t))]
[((HeterogeneousVector: ts) (Sequence: (list t*))) [((List: ts) (Sequence: (list t*)))
(subtypes* A0 ts (map (λ (_) t*) ts))] (subtypes* A0 ts (map (λ (_) t*) ts))]
[((Vector: t) (Sequence: (list t*))) [((HeterogeneousVector: ts) (Sequence: (list t*)))
(subtype* A0 t t*)] (subtypes* A0 ts (map (λ (_) t*) ts))]
[((Base: 'String _ _ _) (Sequence: (list t*))) [((Vector: t) (Sequence: (list t*)))
(subtype* A0 -Char t*)] (subtype* A0 t t*)]
[((Base: 'Bytes _ _ _) (Sequence: (list t*))) [((Base: 'String _ _ _) (Sequence: (list t*)))
(subtype* A0 -Byte t*)] (subtype* A0 -Char t*)]
[((Base: 'Input-Port _ _ _) (Sequence: (list t*))) [((Base: 'Bytes _ _ _) (Sequence: (list t*)))
(subtype* A0 -Nat t*)] (subtype* A0 -Byte t*)]
[((Value: (? exact-nonnegative-integer? n)) (Sequence: (list t*))) [((Base: 'Input-Port _ _ _) (Sequence: (list t*)))
(define possibilities (subtype* A0 -Nat t*)]
(list [((Value: (? exact-nonnegative-integer? n)) (Sequence: (list t*)))
(list byte? -Byte) (define possibilities
(list portable-index? -Index) (list
(list portable-fixnum? -NonNegFixnum) (list byte? -Byte)
(list values -Nat))) (list portable-index? -Index)
(define type (list portable-fixnum? -NonNegFixnum)
(for/or ((pred-type (in-list possibilities))) (list values -Nat)))
(match pred-type (define type
((list pred? type) (for/or ((pred-type (in-list possibilities)))
(and (pred? n) type))))) (match pred-type
(subtype* A0 type t*)] ((list pred? type)
[((Base: _ _ _ #t) (Sequence: (list t*))) (and (pred? n) type)))))
(define type (subtype* A0 type t*)]
;; FIXME: thread the store through here [((Base: _ _ _ #t) (Sequence: (list t*)))
(for/or ((t (in-list (list -Byte -Index -NonNegFixnum -Nat)))) (define type
(or (and (subtype* A0 s t) t)))) ;; FIXME: thread the store through here
(if type (for/or ((t (in-list (list -Byte -Index -NonNegFixnum -Nat))))
(subtype* A0 type t*) (or (and (subtype* A0 s t) t))))
#f)] (if type
[((Hashtable: k v) (Sequence: (list k* v*))) (subtype* A0 type t*)
(subtypes* A0 (list k v) (list k* v*))] #f)]
[((Set: t) (Sequence: (list t*))) [((Hashtable: k v) (Sequence: (list k* v*)))
(subtype* A0 t t*)] (subtypes* A0 (list k v) (list k* v*))]
;; special-case for case-lambda/union with only one argument [((Set: t) (Sequence: (list t*)))
[((Function: arr1) (Function: (list arr2))) (subtype* A0 t t*)]
(cond [(null? arr1) #f] ;; special-case for case-lambda/union with only one argument
[else [((Function: arr1) (Function: (list arr2)))
(define comb (combine-arrs arr1)) (cond [(null? arr1) #f]
(or (and comb (arr-subtype*/no-fail A0 comb arr2)) [else
(supertype-of-one/arr A0 arr2 arr1))])] (define comb (combine-arrs arr1))
;; case-lambda (or (and comb (arr-subtype*/no-fail A0 comb arr2))
[((Function: arr1) (Function: arr2)) (supertype-of-one/arr A0 arr2 arr1))])]
(when (null? arr1) #f) ;; case-lambda
(let loop-arities ([A* A0] [((Function: arr1) (Function: arr2))
[arr2 arr2]) (if (null? arr1) #f
(cond (let loop-arities ([A* A0]
[arr2 arr2])
(cond
[(null? arr2) A*] [(null? arr2) A*]
[(supertype-of-one/arr A* (car arr2) arr1) => (lambda (A) (loop-arities A (cdr arr2)))] [(supertype-of-one/arr A* (car arr2) arr1) => (lambda (A) (loop-arities A (cdr arr2)))]
[else #f]))] [else #f])))]
;; recur structurally on pairs ;; recur structurally on pairs
[((Pair: a d) (Pair: a* d*)) [((Pair: a d) (Pair: a* d*))
(subtypes* A0 (list a d) (list a* d*))] (subtypes* A0 (list a d) (list a* d*))]
;; recur structurally on dotted lists, assuming same bounds ;; recur structurally on dotted lists, assuming same bounds
[((ListDots: s-dty dbound) (ListDots: t-dty dbound)) [((ListDots: s-dty dbound) (ListDots: t-dty dbound*))
(subtype* A0 s-dty t-dty)] (and (eq? dbound dbound*)
;; For dotted lists and regular lists, we check that (All (dbound) s-dty) is a subtype (subtype* A0 s-dty t-dty))]
;; of t-elem, so that no matter what dbound is instatiated with s-dty is still a subtype ;; For dotted lists and regular lists, we check that (All (dbound) s-dty) is a subtype
;; of t-elem. We cannot just replace dbound with Univ because of variance issues. ;; of t-elem, so that no matter what dbound is instatiated with s-dty is still a subtype
[((ListDots: s-dty dbound) (Listof: t-elem)) ;; of t-elem. We cannot just replace dbound with Univ because of variance issues.
(subtype* A0 (-poly (dbound) s-dty) t-elem)] [((ListDots: s-dty dbound) (Listof: t-elem))
;; quantification over two types preserves subtyping (subtype* A0 (-poly (dbound) s-dty) t-elem)]
[((Poly: ns b1) (Poly: ms b2)) ;; quantification over two types preserves subtyping
(=> unmatch) [((Poly: ns b1) (Poly: ms b2))
(unless (= (length ns) (length ms)) #:when (= (length ns) (length ms))
(unmatch)) ;; substitute ns for ms in b2 to make it look like b1
;; substitute ns for ms in b2 to make it look like b1 (subtype* A0 b1 (subst-all (make-simple-substitution ms (map make-F ns)) b2))]
(subtype* A0 b1 (subst-all (make-simple-substitution ms (map make-F ns)) b2))] [((PolyDots: (list ns ... n-dotted) b1)
[((PolyDots: (list ns ... n-dotted) b1) (PolyDots: (list ms ... m-dotted) b2))
(PolyDots: (list ms ... m-dotted) b2)) (cond
(cond [(< (length ns) (length ms))
[(< (length ns) (length ms)) (define-values (short-ms rest-ms) (split-at ms (length ns)))
(define-values (short-ms rest-ms) (split-at ms (length ns))) ;; substitute ms for ns in b1 to make it look like b2
;; substitute ms for ns in b1 to make it look like b2 (define subst
(define subst (hash-set (make-simple-substitution ns (map make-F short-ms))
(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)))
n-dotted (i-subst/dotted (map make-F rest-ms) (make-F m-dotted) m-dotted))) (subtype* A0 (subst-all subst b1) b2)]
(subtype* A0 (subst-all subst b1) b2)] [else
[else (define-values (short-ns rest-ns) (split-at ns (length ms)))
(define-values (short-ns rest-ns) (split-at ns (length ms))) ;; substitute ns for ms in b2 to make it look like b1
;; substitute ns for ms in b2 to make it look like b1 (define subst
(define subst (hash-set (make-simple-substitution ms (map make-F short-ns))
(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)))
m-dotted (i-subst/dotted (map make-F rest-ns) (make-F n-dotted) n-dotted))) (subtype* A0 b1 (subst-all subst b2))])]
(subtype* A0 b1 (subst-all subst b2))])] [((PolyDots: (list ns ... n-dotted) b1)
[((PolyDots: (list ns ... n-dotted) b1) (Poly: (list ms ...) b2))
(Poly: (list ms ...) b2)) #:when (<= (length ns) (length ms))
(=> unmatch) ;; substitute ms for ns in b1 to make it look like b2
(unless (<= (length ns) (length ms)) (define subst
(unmatch)) (hash-set (make-simple-substitution ns (map make-F (take ms (length ns))))
;; substitute ms for ns in b1 to make it look like b2 n-dotted (i-subst (map make-F (drop ms (length ns))))))
(define subst (subtype* A0 (subst-all subst b1) b2)]
(hash-set (make-simple-substitution ns (map make-F (take ms (length ns)))) [((Refinement: par _) t)
n-dotted (i-subst (map make-F (drop ms (length ns)))))) (subtype* A0 par t)]
(subtype* A0 (subst-all subst b1) b2)] ;; use unification to see if we can use the polytype here
[((Refinement: par _) t) [((Poly: vs b) s)
(subtype* A0 par t)] #:when (infer vs null (list b) (list s) Univ)
;; use unification to see if we can use the polytype here A0]
[((Poly: vs b) s) [((PolyDots: (list vs ... vdotted) b) s)
(=> unmatch) #:when (infer vs (list vdotted) (list b) (list s) Univ)
(if (infer vs null (list b) (list s) Univ) A0 (unmatch))] A0]
[((PolyDots: (list vs ... vdotted) b) s) [(s (or (Poly: vs b) (PolyDots: vs b)))
(=> unmatch) #:when (null? (fv b))
(if (infer vs (list vdotted) (list b) (list s) Univ) (subtype* A0 s b)]
A0 ;; rec types, applications and names (that aren't the same)
(unmatch))] [((? needs-resolving? s) other)
[(s (or (Poly: vs b) (PolyDots: vs b))) (let ([s* (resolve-once s)])
(=> unmatch) (if (Type/c? s*) ;; needed in case this was a name that hasn't been resolved yet
(if (null? (fv b)) (subtype* A0 s b) (unmatch))] (subtype* A0 s* other)
;; rec types, applications and names (that aren't the same) #f))]
[((? needs-resolving? s) other) [(other (? needs-resolving? t))
(let ([s* (resolve-once s)]) (let ([t* (resolve-once t)])
(if (Type/c? s*) ;; needed in case this was a name that hasn't been resolved yet (if (Type/c? t*) ;; needed in case this was a name that hasn't been resolved yet
(subtype* A0 s* other) (subtype* A0 other t*)
#f))] #f))]
[(other (? needs-resolving? t)) ;; for unions, we check the cross-product
(let ([t* (resolve-once t)]) ;; some special cases for better performance
(if (Type/c? t*) ;; needed in case this was a name that hasn't been resolved yet ;; first, if both types are numeric, they will be built from the same base types
(subtype* A0 other t*) ;; so we can check for simple set inclusion of the union components
#f))] [((Base: _ _ _ #t) (Union: l2))
;; for unions, we check the cross-product #:when (eq? kt 'number)
;; some special cases for better performance (and (memq s l2) A0)]
;; first, if both types are numeric, they will be built from the same base types ;; this appears to never be called
;; so we can check for simple set inclusion of the union components [((Union: l1) (Union: l2))
[((Base: _ _ _ _) (Union: l2)) #:when (and (eq? ks 'number) (eq? kt 'number))
(=> unmatch) ;; l1 should be a subset of l2
(if (and (eq? ks 'number) (eq? kt 'number)) ;; since union elements are sorted, a linear scan works
(if (memq s l2) A0 #f) (let loop ([l1 l1] [l2 l2])
(unmatch))] (cond [(null? l1)
[((Union: l1) (Union: l2)) A0]
(=> unmatch) [(null? l2)
(if (and (eq? ks 'number) (eq? kt 'number)) #f]
;; l1 should be a subset of l2 [(eq? (car l1) (car l2))
;; since union elements are sorted, a linear scan works (loop (cdr l1) (cdr l2))]
(let loop ([l1 l1] [l2 l2]) [else
(cond [(null? l1) (loop l1 (cdr l2))]))]
A0] [((Union: es) t)
[(null? l2) ;(set! lengths (cons (length es) lengths))
#f] (and
[(eq? (car l1) (car l2)) (for/and ([elem (in-list es)])
(loop (cdr l1) (cdr l2))] (subtype* A0 elem t))
[else A0)]
(loop l1 (cdr l2))])) [(s (Union: es))
(unmatch))] ;(set! lengths (cons (length es) lengths))
[((Union: (list e1 e2)) t) (and (for/or ([elem (in-list es)])
(and (and (subtype* A0 e1 t) (subtype* A0 e2 t)) (subtype* A0 s elem))
A0)] A0)]
[((Union: (list e1 e2 e3)) t) ;; subtyping on immutable structs is covariant
(and (and (subtype* A0 e1 t) (subtype* A0 e2 t) (subtype* A0 e3 t)) [((Struct: nm _ flds proc _ _) (Struct: nm* _ flds* proc* _ _))
A0)] #:when (free-identifier=? nm nm*)
[((Union: es) t) (let ([A (cond [(and proc proc*) (subtype* A0 proc proc*)]
(and (for/and ([elem (in-list es)]) [proc* #f]
(subtype* A0 elem t)) [else A0])])
A0)] (and A (subtype/flds* A flds flds*)))]
[(s (Union: es)) [((Struct: nm _ _ _ _ _) (StructTop: (Struct: nm* _ _ _ _ _)))
(and (for/or ([elem (in-list es)]) #:when (free-identifier=? nm nm*)
(subtype* A0 s elem)) A0]
A0)] ;; Promises are covariant
;; subtyping on immutable structs is covariant [((Promise: s) (Promise: t))
[((Struct: nm _ flds proc _ _) (Struct: nm* _ flds* proc* _ _)) (subtype* A0 s t)]
(=> unmatch) ;ephemerons are covariant
(unless (free-identifier=? nm nm*) (unmatch)) [((Ephemeron: s) (Ephemeron: t))
(let ([A (cond [(and proc proc*) (subtype* A0 proc proc*)] (subtype* A0 s t)]
[proc* #f] [((CustodianBox: s) (CustodianBox: t))
[else A0])]) (subtype* A0 s t)]
(and A (subtype/flds* A flds flds*)))] [((Set: t) (Set: t*)) (subtype* A0 t t*)]
[((Struct: nm _ _ _ _ _) (StructTop: (Struct: nm* _ _ _ _ _))) ;; Evts are covariant
(=> unmatch) [((Evt: t) (Evt: t*)) (subtype* A0 t t*)]
(unless (free-identifier=? nm nm*) (unmatch)) [((Base: 'Semaphore _ _ _) (Evt: t))
A0] (subtype* A0 s t)]
;; Promises are covariant [((Base: 'Output-Port _ _ _) (Evt: t))
[((Promise: s) (Promise: t)) (subtype* A0 s t)]
(subtype* A0 s t)] [((Base: 'Input-Port _ _ _) (Evt: t))
;ephemerons are covariant (subtype* A0 s t)]
[((Ephemeron: s) (Ephemeron: t)) [((Base: 'TCP-Listener _ _ _) (Evt: t))
(subtype* A0 s t)] (subtype* A0 s t)]
[((CustodianBox: s) (CustodianBox: t)) [((Base: 'Thread _ _ _) (Evt: t))
(subtype* A0 s t)] (subtype* A0 s t)]
[((Set: t) (Set: t*)) (subtype* A0 t t*)] [((Base: 'Subprocess _ _ _) (Evt: t))
;; Evts are covariant (subtype* A0 s t)]
[((Evt: t) (Evt: t*)) (subtype* A0 t t*)] [((Base: 'Will-Executor _ _ _) (Evt: t))
[((Base: 'Semaphore _ _ _) (Evt: t)) (subtype* A0 s t)]
(subtype* A0 s t)] [((Base: 'LogReceiver _ _ _) (Evt: t))
[((Base: 'Output-Port _ _ _) (Evt: t)) (subtype* A0
(subtype* A0 s t)] (make-HeterogeneousVector
[((Base: 'Input-Port _ _ _) (Evt: t)) (list -Symbol -String Univ
(subtype* A0 s t)] (Un (-val #f) -Symbol)))
[((Base: 'TCP-Listener _ _ _) (Evt: t)) t)]
(subtype* A0 s t)] [((CustodianBox: t) (Evt: t*))
[((Base: 'Thread _ _ _) (Evt: t)) ;; Note that it's the whole box type that's being
(subtype* A0 s t)] ;; compared against t* here
[((Base: 'Subprocess _ _ _) (Evt: t)) (subtype* A0 s t*)]
(subtype* A0 s t)] [((Channel: t) (Evt: t*)) (subtype* A0 t t*)]
[((Base: 'Will-Executor _ _ _) (Evt: t)) ;; Invariant types
(subtype* A0 s t)] [((Box: s) (Box: t)) (type-equiv? A0 s t)]
[((Base: 'LogReceiver _ _ _) (Evt: t)) [((Box: _) (BoxTop:)) A0]
(subtype* A0 [((ThreadCell: s) (ThreadCell: t)) (type-equiv? A0 s t)]
(make-HeterogeneousVector [((ThreadCell: _) (ThreadCellTop:)) A0]
(list -Symbol -String Univ [((Channel: s) (Channel: t)) (type-equiv? A0 s t)]
(Un (-val #f) -Symbol))) [((Channel: _) (ChannelTop:)) A0]
t)] [((Vector: s) (Vector: t)) (type-equiv? A0 s t)]
[((CustodianBox: t) (Evt: t*)) [((Vector: _) (VectorTop:)) A0]
;; Note that it's the whole box type that's being [((HeterogeneousVector: _) (VectorTop:)) A0]
;; compared against t* here [((HeterogeneousVector: (list e ...)) (Vector: e*))
(subtype* A0 s t*)] (for/fold ((A A0)) ((e (in-list e)) #:break (not A))
[((Channel: t) (Evt: t*)) (subtype* A0 t t*)] (and A (type-equiv? A e e*)))]
;; Invariant types [((HeterogeneousVector: (list s* ...)) (HeterogeneousVector: (list t* ...)))
[((Box: s) (Box: t)) (type-equiv? A0 s t)] (if (= (length s*) (length t*))
[((Box: _) (BoxTop:)) A0] (for/fold ((A A0)) ((s (in-list s*)) (t (in-list t*)) #:break (not A))
[((ThreadCell: s) (ThreadCell: t)) (type-equiv? A0 s t)] (type-equiv? A s t))
[((ThreadCell: _) (ThreadCellTop:)) A0] #f)]
[((Channel: s) (Channel: t)) (type-equiv? A0 s t)] [((MPair: s1 s2) (MPair: t1 t2))
[((Channel: _) (ChannelTop:)) A0] (subtype-seq A0
[((Vector: s) (Vector: t)) (type-equiv? A0 s t)] (type-equiv? s1 t1)
[((Vector: _) (VectorTop:)) A0] (type-equiv? s2 t2))]
[((HeterogeneousVector: _) (VectorTop:)) A0] [((MPair: _ _) (MPairTop:)) A0]
[((HeterogeneousVector: (list e ...)) (Vector: e*)) [((Hashtable: s1 s2) (Hashtable: t1 t2))
(for/fold ((A A0)) ((e (in-list e)) #:break (not A)) (subtype-seq A0
(and A (type-equiv? A e e*)))] (type-equiv? s1 t1)
[((HeterogeneousVector: (list s* ...)) (HeterogeneousVector: (list t* ...))) (type-equiv? s2 t2))]
(if (= (length s*) (length t*)) [((Hashtable: _ _) (HashtableTop:)) A0]
(for/fold ((A A0)) ((s (in-list s*)) (t (in-list t*)) #:break (not A)) [((Prompt-Tagof: s1 s2) (Prompt-Tagof: t1 t2))
(type-equiv? A s t)) (subtype-seq A0
#f)] (type-equiv? s1 t1)
[((MPair: s1 s2) (MPair: t1 t2)) (type-equiv? s2 t2))]
(subtype-seq A0 [((Prompt-Tagof: _ _) (Prompt-TagTop:)) A0]
(type-equiv? s1 t1) [((Continuation-Mark-Keyof: s) (Continuation-Mark-Keyof: t))
(type-equiv? s2 t2))] (type-equiv? A0 s t)]
[((MPair: _ _) (MPairTop:)) A0] [((Continuation-Mark-Keyof: _) (Continuation-Mark-KeyTop:)) A0]
[((Hashtable: s1 s2) (Hashtable: t1 t2)) ;; subtyping on structs follows the declared hierarchy
(subtype-seq A0 [((Struct: nm (? Type/c? parent) _ _ _ _) other)
(type-equiv? s1 t1) ;(dprintf "subtype - hierarchy : ~a ~a ~a\n" nm parent other)
(type-equiv? s2 t2))] (subtype* A0 parent other)]
[((Hashtable: _ _) (HashtableTop:)) A0] ;; subtyping on values is pointwise
[((Prompt-Tagof: s1 s2) (Prompt-Tagof: t1 t2)) [((Values: vals1) (Values: vals2)) (subtypes* A0 vals1 vals2)]
(subtype-seq A0 [((ValuesDots: s-rs s-dty dbound) (ValuesDots: t-rs t-dty dbound))
(type-equiv? s1 t1) (subtype* (subtypes* A0 s-rs t-rs) s-dty t-dty)]
(type-equiv? s2 t2))] [((Result: t (FilterSet: ft ff) o) (Result: t* (FilterSet: ft* ff*) o))
[((Prompt-Tagof: _ _) (Prompt-TagTop:)) A0] (subtype-seq A0
[((Continuation-Mark-Keyof: s) (Continuation-Mark-Keyof: t)) (subtype* t t*)
(type-equiv? A0 s t)] (filter-subtype* ft ft*)
[((Continuation-Mark-Keyof: _) (Continuation-Mark-KeyTop:)) A0] (filter-subtype* ff ff*))]
;; subtyping on structs follows the declared hierarchy [((Result: t (FilterSet: ft ff) o) (Result: t* (FilterSet: ft* ff*) (Empty:)))
[((Struct: nm (? Type/c? parent) _ _ _ _) other) (subtype-seq A0
;(dprintf "subtype - hierarchy : ~a ~a ~a\n" nm parent other) (subtype* t t*)
(subtype* A0 parent other)] (filter-subtype* ft ft*)
;; subtyping on values is pointwise (filter-subtype* ff ff*))]
[((Values: vals1) (Values: vals2)) (subtypes* A0 vals1 vals2)] ;; subtyping on other stuff
[((ValuesDots: s-rs s-dty dbound) (ValuesDots: t-rs t-dty dbound)) [((Syntax: t) (Syntax: t*))
(subtype* (subtypes* A0 s-rs t-rs) s-dty t-dty)] (subtype* A0 t t*)]
[((Result: t (FilterSet: ft ff) o) (Result: t* (FilterSet: ft* ff*) o)) [((Future: t) (Future: t*))
(subtype-seq A0 (subtype* A0 t t*)]
(subtype* t t*) [((Param: s-in s-out) (Param: t-in t-out))
(filter-subtype* ft ft*) (subtype-seq A0
(filter-subtype* ff ff*))] (subtype* t-in s-in)
[((Result: t (FilterSet: ft ff) o) (Result: t* (FilterSet: ft* ff*) (Empty:))) (subtype* s-out t-out))]
(subtype-seq A0 [((Param: in out) t)
(subtype* t t*) (subtype* A0 (cl->* (-> out) (-> in -Void)) t)]
(filter-subtype* ft ft*) [((Instance: t) (Instance: t*))
(filter-subtype* ff ff*))] (subtype* A0 t t*)]
;; subtyping on other stuff [((Class: '() '() (list (and s (list names meths )) ...))
[((Syntax: t) (Syntax: t*)) (Class: '() '() (list (and s* (list names* meths*)) ...)))
(subtype* A0 t t*)] (for/fold ([A A0])
[((Future: t) (Future: t*)) ([n (in-list names*)] [m (in-list meths*)] #:break (not A))
(subtype* A0 t t*)] (and A (cond [(assq n s) => (lambda (spec) (subtype* A (cadr spec) m))]
[((Param: s-in s-out) (Param: t-in t-out)) [else #f])))]
(subtype-seq A0 ;; otherwise, not a subtype
(subtype* t-in s-in) [(_ _) #f])))
(subtype* s-out t-out))] (when (null? A)
[((Param: in out) t) (hash-set! subtype-cache (cons ss st) r))
(subtype* A0 (cl->* (-> out) (-> in -Void)) t)] r))
[((Instance: t) (Instance: t*))
(subtype* A0 t t*)]
[((Class: '() '() (list (and s (list names meths )) ...))
(Class: '() '() (list (and s* (list names* meths*)) ...)))
(for/fold ([A A0])
([n (in-list names*)] [m (in-list meths*)] #:break (not A))
(and A (cond [(assq n s) => (lambda (spec) (subtype* A (cadr spec) m))]
[else #f])))]
;; otherwise, not a subtype
[(_ _) #f #;(dprintf "failed")])))]))))
(define (type-compare? a b) (define (type-compare? a b)
(and (subtype a b) (subtype b a))) (or (type-equal? a b)
(and (subtype a b) (subtype b a))))
;; List[(cons Number Number)] type type -> maybe[List[(cons Number Number)]] ;; List[(cons Number Number)] type type -> maybe[List[(cons Number Number)]]
(define subtype*/no-fail subtype*) (define subtype*/no-fail subtype*)

2
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/utils/utils.rkt
View File

@ -165,7 +165,7 @@ at least theoretically.
(lambda (stx) (lambda (stx)
(syntax-parse stx (syntax-parse stx
[(_ head cnt . body) [(_ head cnt . body)
#'(define head . body)])))) (syntax/loc stx (define head . body))]))))
(define-syntax define-struct/cond-contract (define-syntax define-struct/cond-contract
(if enable-contracts? (if enable-contracts?