Major revision of subtyping code for performance.
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:
parent
d13afa0f78
commit
0a6537a6cb
|
@ -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)
|
||||||
|
|
|
@ -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,7 +376,10 @@
|
||||||
[#: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]
|
||||||
|
[#:key (cond [(or (eq? v 0) (eq? v 1)) 'number]
|
||||||
|
;; other numbers don't work with the optimizations in subtype.rkt
|
||||||
|
;; which assume that unions of numbers are subtyped in simple ways
|
||||||
[(boolean? v) 'boolean]
|
[(boolean? v) 'boolean]
|
||||||
[(null? v) 'null]
|
[(null? v) 'null]
|
||||||
[else #f])])
|
[else #f])])
|
||||||
|
@ -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])
|
||||||
|
|
||||||
|
|
|
@ -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)))))
|
||||||
|
|
||||||
|
|
|
@ -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,37 +213,57 @@
|
||||||
(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
|
||||||
|
#:return-when (and (symbol? ks) (pair? kt) (not (memq ks kt))) #f
|
||||||
|
#:return-when
|
||||||
|
(and (pair? ks) (pair? kt)
|
||||||
(for/and ([i (in-list ks)]) (not (memq i kt))))
|
(for/and ([i (in-list ks)]) (not (memq i kt))))
|
||||||
#f]
|
#f
|
||||||
[else
|
#:return-when (eq? ss bottom-key) A
|
||||||
(let* ([A0 (remember s t A)])
|
#:return-when (eq? st top-key) A
|
||||||
|
(define A0 (remember s t A))
|
||||||
|
(define r
|
||||||
|
;; FIXME -- make this go into only the places that need it -- slows down new-metrics.rkt significantly
|
||||||
(parameterize ([current-seen A0])
|
(parameterize ([current-seen A0])
|
||||||
(match* (s t)
|
(match* (s t)
|
||||||
[(_ (Univ:)) A0]
|
;; these cases are above as special cases
|
||||||
|
;; [((Union: (list)) _) A0] ;; this is extremely common, so it goes first
|
||||||
|
;; [(_ (Univ:)) A0]
|
||||||
[((or (ValuesDots: _ _ _) (Values: _) (AnyValues:)) (AnyValues:)) A0]
|
[((or (ValuesDots: _ _ _) (Values: _) (AnyValues:)) (AnyValues:)) A0]
|
||||||
;; error is top and bot
|
;; error is top and bot
|
||||||
[(_ (Error:)) A0]
|
[(_ (Error:)) A0]
|
||||||
[((Error:) _) A0]
|
[((Error:) _) A0]
|
||||||
;; (Un) is bot
|
;; (Un) is bot
|
||||||
[(_ (Union: (list))) #f]
|
[(_ (Union: (list))) #f]
|
||||||
[((Union: (list)) _) A0]
|
|
||||||
;; value types
|
;; value types
|
||||||
[((Value: v1) (Value: v2)) (=> unmatch) (if (equal? v1 v2) A0 (unmatch))]
|
[((Value: v1) (Value: v2))
|
||||||
|
#:when (equal? v1 v2) A0]
|
||||||
;; values are subtypes of their "type"
|
;; values are subtypes of their "type"
|
||||||
[((Value: v) (Base: _ _ pred _)) (if (pred v) A0 #f)]
|
[((Value: v) (Base: _ _ pred _)) (if (pred v) A0 #f)]
|
||||||
;; tvars are equal if they are the same variable
|
;; tvars are equal if they are the same variable
|
||||||
|
@ -260,11 +272,8 @@
|
||||||
;; Saves us from non-termination
|
;; Saves us from non-termination
|
||||||
;; Must happen *before* the sequence cases, which sometimes call `resolve' in match expanders
|
;; Must happen *before* the sequence cases, which sometimes call `resolve' in match expanders
|
||||||
[((or (? Struct? s1) (NameStruct: s1)) (or (? Struct? s2) (NameStruct: s2)))
|
[((or (? Struct? s1) (NameStruct: s1)) (or (? Struct? s2) (NameStruct: s2)))
|
||||||
(=> unmatch)
|
#:when (unrelated-structs s1 s2)
|
||||||
(cond [(unrelated-structs s1 s2)
|
|
||||||
;(dprintf "found unrelated structs: ~a ~a\n" s1 s2)
|
|
||||||
#f]
|
#f]
|
||||||
[else (unmatch)])]
|
|
||||||
;; similar case for structs and base types, which are obviously unrelated
|
;; similar case for structs and base types, which are obviously unrelated
|
||||||
[((Base: _ _ _ _) (or (? Struct? s1) (NameStruct: s1)))
|
[((Base: _ _ _ _) (or (? Struct? s1) (NameStruct: s1)))
|
||||||
#f]
|
#f]
|
||||||
|
@ -275,9 +284,6 @@
|
||||||
#f]
|
#f]
|
||||||
[((or (? Struct? s1) (NameStruct: s1)) (Value: (? (negate struct?) _)))
|
[((or (? Struct? s1) (NameStruct: s1)) (Value: (? (negate struct?) _)))
|
||||||
#f]
|
#f]
|
||||||
;; just checking if s/t is a struct misses recursive/union/etc cases
|
|
||||||
[((? (lambda (_) (eq? ks 'struct))) (Base: _ _ _ _)) #f]
|
|
||||||
[((Base: _ _ _ _) (? (lambda (_) (eq? kt 'struct)))) #f]
|
|
||||||
;; sequences are covariant
|
;; sequences are covariant
|
||||||
[((Sequence: ts) (Sequence: ts*))
|
[((Sequence: ts) (Sequence: ts*))
|
||||||
(subtypes* A0 ts ts*)]
|
(subtypes* A0 ts ts*)]
|
||||||
|
@ -340,19 +346,20 @@
|
||||||
(supertype-of-one/arr A0 arr2 arr1))])]
|
(supertype-of-one/arr A0 arr2 arr1))])]
|
||||||
;; case-lambda
|
;; case-lambda
|
||||||
[((Function: arr1) (Function: arr2))
|
[((Function: arr1) (Function: arr2))
|
||||||
(when (null? arr1) #f)
|
(if (null? arr1) #f
|
||||||
(let loop-arities ([A* A0]
|
(let loop-arities ([A* A0]
|
||||||
[arr2 arr2])
|
[arr2 arr2])
|
||||||
(cond
|
(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*)
|
||||||
|
(subtype* A0 s-dty t-dty))]
|
||||||
;; For dotted lists and regular lists, we check that (All (dbound) s-dty) is a subtype
|
;; For dotted lists and regular lists, we check that (All (dbound) s-dty) is a subtype
|
||||||
;; of t-elem, so that no matter what dbound is instatiated with s-dty is still a subtype
|
;; of t-elem, so that no matter what dbound is instatiated with s-dty is still a subtype
|
||||||
;; of t-elem. We cannot just replace dbound with Univ because of variance issues.
|
;; of t-elem. We cannot just replace dbound with Univ because of variance issues.
|
||||||
|
@ -360,9 +367,7 @@
|
||||||
(subtype* A0 (-poly (dbound) s-dty) t-elem)]
|
(subtype* A0 (-poly (dbound) s-dty) t-elem)]
|
||||||
;; quantification over two types preserves subtyping
|
;; quantification over two types preserves subtyping
|
||||||
[((Poly: ns b1) (Poly: ms b2))
|
[((Poly: ns b1) (Poly: ms b2))
|
||||||
(=> unmatch)
|
#:when (= (length ns) (length ms))
|
||||||
(unless (= (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)
|
||||||
|
@ -384,9 +389,7 @@
|
||||||
(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))
|
||||||
(=> unmatch)
|
#:when (<= (length ns) (length ms))
|
||||||
(unless (<= (length ns) (length ms))
|
|
||||||
(unmatch))
|
|
||||||
;; 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 (take ms (length ns))))
|
(hash-set (make-simple-substitution ns (map make-F (take ms (length ns))))
|
||||||
|
@ -396,16 +399,14 @@
|
||||||
(subtype* A0 par t)]
|
(subtype* A0 par t)]
|
||||||
;; use unification to see if we can use the polytype here
|
;; use unification to see if we can use the polytype here
|
||||||
[((Poly: vs b) s)
|
[((Poly: vs b) s)
|
||||||
(=> unmatch)
|
#:when (infer vs null (list b) (list s) Univ)
|
||||||
(if (infer vs null (list b) (list s) Univ) A0 (unmatch))]
|
A0]
|
||||||
[((PolyDots: (list vs ... vdotted) b) s)
|
[((PolyDots: (list vs ... vdotted) b) s)
|
||||||
(=> unmatch)
|
#:when (infer vs (list vdotted) (list b) (list s) Univ)
|
||||||
(if (infer vs (list vdotted) (list b) (list s) Univ)
|
A0]
|
||||||
A0
|
|
||||||
(unmatch))]
|
|
||||||
[(s (or (Poly: vs b) (PolyDots: vs b)))
|
[(s (or (Poly: vs b) (PolyDots: vs b)))
|
||||||
(=> unmatch)
|
#:when (null? (fv b))
|
||||||
(if (null? (fv b)) (subtype* A0 s b) (unmatch))]
|
(subtype* A0 s b)]
|
||||||
;; rec types, applications and names (that aren't the same)
|
;; rec types, applications and names (that aren't the same)
|
||||||
[((? needs-resolving? s) other)
|
[((? needs-resolving? s) other)
|
||||||
(let ([s* (resolve-once s)])
|
(let ([s* (resolve-once s)])
|
||||||
|
@ -421,14 +422,12 @@
|
||||||
;; some special cases for better performance
|
;; some special cases for better performance
|
||||||
;; first, if both types are numeric, they will be built from the same base types
|
;; first, if both types are numeric, they will be built from the same base types
|
||||||
;; so we can check for simple set inclusion of the union components
|
;; so we can check for simple set inclusion of the union components
|
||||||
[((Base: _ _ _ _) (Union: l2))
|
[((Base: _ _ _ #t) (Union: l2))
|
||||||
(=> unmatch)
|
#:when (eq? kt 'number)
|
||||||
(if (and (eq? ks 'number) (eq? kt 'number))
|
(and (memq s l2) A0)]
|
||||||
(if (memq s l2) A0 #f)
|
;; this appears to never be called
|
||||||
(unmatch))]
|
|
||||||
[((Union: l1) (Union: l2))
|
[((Union: l1) (Union: l2))
|
||||||
(=> unmatch)
|
#:when (and (eq? ks 'number) (eq? kt 'number))
|
||||||
(if (and (eq? ks 'number) (eq? kt 'number))
|
|
||||||
;; l1 should be a subset of l2
|
;; l1 should be a subset of l2
|
||||||
;; since union elements are sorted, a linear scan works
|
;; since union elements are sorted, a linear scan works
|
||||||
(let loop ([l1 l1] [l2 l2])
|
(let loop ([l1 l1] [l2 l2])
|
||||||
|
@ -439,33 +438,27 @@
|
||||||
[(eq? (car l1) (car l2))
|
[(eq? (car l1) (car l2))
|
||||||
(loop (cdr l1) (cdr l2))]
|
(loop (cdr l1) (cdr l2))]
|
||||||
[else
|
[else
|
||||||
(loop l1 (cdr l2))]))
|
(loop l1 (cdr l2))]))]
|
||||||
(unmatch))]
|
|
||||||
[((Union: (list e1 e2)) t)
|
|
||||||
(and (and (subtype* A0 e1 t) (subtype* A0 e2 t))
|
|
||||||
A0)]
|
|
||||||
[((Union: (list e1 e2 e3)) t)
|
|
||||||
(and (and (subtype* A0 e1 t) (subtype* A0 e2 t) (subtype* A0 e3 t))
|
|
||||||
A0)]
|
|
||||||
[((Union: es) t)
|
[((Union: es) t)
|
||||||
(and (for/and ([elem (in-list es)])
|
;(set! lengths (cons (length es) lengths))
|
||||||
|
(and
|
||||||
|
(for/and ([elem (in-list es)])
|
||||||
(subtype* A0 elem t))
|
(subtype* A0 elem t))
|
||||||
A0)]
|
A0)]
|
||||||
[(s (Union: es))
|
[(s (Union: es))
|
||||||
|
;(set! lengths (cons (length es) lengths))
|
||||||
(and (for/or ([elem (in-list es)])
|
(and (for/or ([elem (in-list es)])
|
||||||
(subtype* A0 s elem))
|
(subtype* A0 s elem))
|
||||||
A0)]
|
A0)]
|
||||||
;; subtyping on immutable structs is covariant
|
;; subtyping on immutable structs is covariant
|
||||||
[((Struct: nm _ flds proc _ _) (Struct: nm* _ flds* proc* _ _))
|
[((Struct: nm _ flds proc _ _) (Struct: nm* _ flds* proc* _ _))
|
||||||
(=> unmatch)
|
#:when (free-identifier=? nm nm*)
|
||||||
(unless (free-identifier=? nm nm*) (unmatch))
|
|
||||||
(let ([A (cond [(and proc proc*) (subtype* A0 proc proc*)]
|
(let ([A (cond [(and proc proc*) (subtype* A0 proc proc*)]
|
||||||
[proc* #f]
|
[proc* #f]
|
||||||
[else A0])])
|
[else A0])])
|
||||||
(and A (subtype/flds* A flds flds*)))]
|
(and A (subtype/flds* A flds flds*)))]
|
||||||
[((Struct: nm _ _ _ _ _) (StructTop: (Struct: nm* _ _ _ _ _)))
|
[((Struct: nm _ _ _ _ _) (StructTop: (Struct: nm* _ _ _ _ _)))
|
||||||
(=> unmatch)
|
#:when (free-identifier=? nm nm*)
|
||||||
(unless (free-identifier=? nm nm*) (unmatch))
|
|
||||||
A0]
|
A0]
|
||||||
;; Promises are covariant
|
;; Promises are covariant
|
||||||
[((Promise: s) (Promise: t))
|
[((Promise: s) (Promise: t))
|
||||||
|
@ -577,10 +570,14 @@
|
||||||
(and A (cond [(assq n s) => (lambda (spec) (subtype* A (cadr spec) m))]
|
(and A (cond [(assq n s) => (lambda (spec) (subtype* A (cadr spec) m))]
|
||||||
[else #f])))]
|
[else #f])))]
|
||||||
;; otherwise, not a subtype
|
;; otherwise, not a subtype
|
||||||
[(_ _) #f #;(dprintf "failed")])))]))))
|
[(_ _) #f])))
|
||||||
|
(when (null? A)
|
||||||
|
(hash-set! subtype-cache (cons ss st) r))
|
||||||
|
r))
|
||||||
|
|
||||||
(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*)
|
||||||
|
|
|
@ -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?
|
||||||
|
|
Loading…
Reference in New Issue
Block a user