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

Whitespace fixes, small optimizations of union cases.

Browse Source
This commit is contained in:
Sam Tobin-Hochstadt 2011-09-06 08:02:12 -04:00
parent 43c0177895
commit 64a1aee65d
1 changed files with 94 additions and 78 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

172
collects/typed-racket/types/subtype.rkt
View File

@ -2,14 +2,14 @@
(require "../utils/utils.rkt" (require "../utils/utils.rkt"
(rep type-rep filter-rep object-rep rep-utils) (rep type-rep filter-rep object-rep rep-utils)
(utils tc-utils) (utils tc-utils)
(types utils comparison resolve abbrev numeric-tower substitute) (types utils comparison resolve abbrev numeric-tower substitute)
(env type-name-env) (env type-name-env)
(only-in (infer infer-dummy) unify) (only-in (infer infer-dummy) unify)
racket/match unstable/match racket/match unstable/match
racket/function racket/function
(rename-in racket/contract (rename-in racket/contract
[-> c->] [->* c->*]) [-> c->] [->* c->*])
(for-syntax racket/base syntax/parse)) (for-syntax racket/base syntax/parse))
;; exn representing failure of subtyping ;; exn representing failure of subtyping
;; s,t both types ;; s,t both types
@ -91,13 +91,13 @@
[(_ init (s1:sub* . args1) (s:sub* . args) ...) [(_ init (s1:sub* . args1) (s:sub* . args) ...)
(with-syntax ([(A* ... A-last) (generate-temporaries #'(s1 s ...))]) (with-syntax ([(A* ... A-last) (generate-temporaries #'(s1 s ...))])
(with-syntax ([(clauses ...) (with-syntax ([(clauses ...)
(for/list ([s (syntax->list #'(s1 s ...))] (for/list ([s (syntax->list #'(s1 s ...))]
[args (syntax->list #'(args1 args ...))] [args (syntax->list #'(args1 args ...))]
[A (syntax->list #'(init A* ...))] [A (syntax->list #'(init A* ...))]
[A-next (syntax->list #'(A* ... A-last))]) [A-next (syntax->list #'(A* ... A-last))])
#`[#,A-next (#,s #,A . #,args)])]) #`[#,A-next (#,s #,A . #,args)])])
#'(let* (clauses ...) #'(let* (clauses ...)
A-last)))])) A-last)))]))
(define (kw-subtypes* A0 t-kws s-kws) (define (kw-subtypes* A0 t-kws s-kws)
(let loop ([A A0] [t t-kws] [s s-kws]) (let loop ([A A0] [t t-kws] [s s-kws])
@ -245,25 +245,25 @@
[(and (symbol? ks) (symbol? kt) (not (eq? ks kt))) (fail! s t)] [(and (symbol? ks) (symbol? kt) (not (eq? ks kt))) (fail! s t)]
[(and (symbol? ks) (pair? kt) (not (memq ks kt))) (fail! s t)] [(and (symbol? ks) (pair? kt) (not (memq ks kt))) (fail! s t)]
[(and (pair? ks) (pair? kt) [(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))))
(fail! s t)] (fail! s t)]
[else [else
(let* ([A0 (remember s t A)]) (let* ([A0 (remember s t A)])
(parameterize ([current-seen A0]) (parameterize ([current-seen A0])
(match* (s t) (match* (s t)
[(_ (Univ:)) A0] [(_ (Univ:)) 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))) (fail! s t)] [(_ (Union: (list))) (fail! s t)]
[((Union: (list)) _) A0] [((Union: (list)) _) A0]
;; value types ;; value types
[((Value: v1) (Value: v2)) (=> unmatch) (if (equal? v1 v2) A0 (unmatch))] [((Value: v1) (Value: v2)) (=> unmatch) (if (equal? v1 v2) A0 (unmatch))]
;; values are subtypes of their "type" ;; values are subtypes of their "type"
[((Value: v) (Base: _ _ pred _)) (if (pred v) A0 (fail! s t))] [((Value: v) (Base: _ _ pred _)) (if (pred v) A0 (fail! s t))]
;; tvars are equal if they are the same variable ;; tvars are equal if they are the same variable
[((F: t) (F: t*)) (if (eq? t t*) A0 (fail! s t))] [((F: t) (F: t*)) (if (eq? t t*) A0 (fail! s t))]
;; Avoid needing to resolve things that refer to different structs. ;; Avoid needing to resolve things that refer to different structs.
;; 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
@ -311,57 +311,73 @@
(or (arr-subtype*/no-fail A0 (combine-arrs arr1) arr2) (or (arr-subtype*/no-fail A0 (combine-arrs arr1) arr2)
(supertype-of-one/arr A0 arr2 arr1) (supertype-of-one/arr A0 arr2 arr1)
(fail! s t))] (fail! s t))]
;; case-lambda ;; case-lambda
[((Function: arr1) (Function: arr2)) [((Function: arr1) (Function: arr2))
(when (null? arr1) (fail! s t)) (when (null? arr1) (fail! s t))
(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 (fail! s t)]))] [else (fail! s t)]))]
;; recur structurally on pairs ;; recur structurally on pairs
[((Pair: a d) (Pair: a* d*)) [((Pair: a d) (Pair: a* d*))
(let ([A1 (subtype* A0 a a*)]) (let ([A1 (subtype* A0 a a*)])
(and A1 (subtype* A1 d d*)))] (and A1 (subtype* A1 d 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)] (subtype* A0 s-dty t-dty)]
[((ListDots: s-dty dbound) (Listof: t-elem)) [((ListDots: s-dty dbound) (Listof: t-elem))
(subtype* A0 (substitute Univ dbound s-dty) t-elem)] (subtype* A0 (substitute Univ 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) (=> unmatch)
(unless (= (length ns) (length ms)) (unless (= (length ns) (length ms))
(unmatch)) (unmatch))
(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))]
[((Refinement: par _ _) t) [((Refinement: par _ _) t)
(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) (=> unmatch)
(if (unify vs (list b) (list s)) A0 (unmatch))] (if (unify vs (list b) (list s)) A0 (unmatch))]
[(s (Poly: vs b)) [(s (Poly: vs b))
(=> unmatch) (=> unmatch)
(if (null? (fv b)) (subtype* A0 s b) (unmatch))] (if (null? (fv b)) (subtype* A0 s b) (unmatch))]
;; 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)])
(if (Type? s*) ;; needed in case this was a name that hasn't been resolved yet (if (Type? s*) ;; needed in case this was a name that hasn't been resolved yet
(subtype* A0 s* other) (subtype* A0 s* other)
(fail! s t)))] (fail! s t)))]
[(other (? needs-resolving? t)) [(other (? needs-resolving? t))
(let ([t* (resolve-once t)]) (let ([t* (resolve-once t)])
(if (Type? t*) ;; needed in case this was a name that hasn't been resolved yet (if (Type? t*) ;; needed in case this was a name that hasn't been resolved yet
(subtype* A0 other t*) (subtype* A0 other t*)
(fail! s t)))] (fail! s t)))]
;; for unions, we check the cross-product ;; for unions, we check the cross-product
[((Union: es) t) (or (and (andmap (lambda (elem) (subtype* A0 elem t)) es) A0) ;; some special cases for better performance
(fail! s t))] [((Union: (list e1 e2)) t)
[(s (Union: es)) (or (and (ormap (lambda (elem) (subtype*/no-fail A0 s elem)) es) A0) (if (and (subtype* A0 e1 t) (subtype* A0 e2 t))
(fail! s t))] A0
;; subtyping on immutable structs is covariant (fail! s t))]
[((Struct: nm _ flds proc _ _ _ _) (Struct: nm* _ flds* proc* _ _ _ _)) (=> nevermind) [((Union: (list e1 e2 e3)) t)
(if (and (subtype* A0 e1 t) (subtype* A0 e2 t) (subtype* A0 e3 t))
A0
(fail! s t))]
[((Union: es) t)
(if (for/and ([elem (in-list es)])
(subtype* A0 elem t))
A0
(fail! s t))]
[(s (Union: es))
(if (for/or ([elem (in-list es)])
(with-handlers ([exn:subtype? (lambda _ #f)])
(subtype* A0 s elem)))
A0
(fail! s t))]
;; subtyping on immutable structs is covariant
[((Struct: nm _ flds proc _ _ _ _) (Struct: nm* _ flds* proc* _ _ _ _)) (=> nevermind)
(unless (free-identifier=? nm nm*) (nevermind)) (unless (free-identifier=? nm nm*) (nevermind))
(let ([A (cond [(and proc proc*) (subtype* proc proc*)] (let ([A (cond [(and proc proc*) (subtype* proc proc*)]
[proc* (fail! proc proc*)] [proc* (fail! proc proc*)]
@ -384,37 +400,37 @@
(if (andmap (lambda (e0) (type-equal? e0 e*)) e) A0 (fail! s t))] (if (andmap (lambda (e0) (type-equal? e0 e*)) e) A0 (fail! s t))]
[((MPair: _ _) (MPairTop:)) A0] [((MPair: _ _) (MPairTop:)) A0]
[((Hashtable: _ _) (HashtableTop:)) A0] [((Hashtable: _ _) (HashtableTop:)) A0]
;; subtyping on structs follows the declared hierarchy ;; subtyping on structs follows the declared hierarchy
[((Struct: nm (? Type? parent) flds proc _ _ _ _) other) [((Struct: nm (? Type? parent) flds proc _ _ _ _) other)
;(dprintf "subtype - hierarchy : ~a ~a ~a\n" nm parent other) ;(dprintf "subtype - hierarchy : ~a ~a ~a\n" nm parent other)
(subtype* A0 parent other)] (subtype* A0 parent other)]
;; Promises are covariant ;; Promises are covariant
[((Struct: (? (lambda (n) (free-identifier=? n promise-id))) _ (list t) _ _ _ _ _) [((Struct: (? (lambda (n) (free-identifier=? n promise-id))) _ (list t) _ _ _ _ _)
(Struct: (? (lambda (n) (free-identifier=? n promise-id))) _ (list t*) _ _ _ _ _)) (Struct: (? (lambda (n) (free-identifier=? n promise-id))) _ (list t*) _ _ _ _ _))
(subtype* A0 t t*)] (subtype* A0 t t*)]
;; subtyping on values is pointwise ;; subtyping on values is pointwise
[((Values: vals1) (Values: vals2)) (subtypes* A0 vals1 vals2)] [((Values: vals1) (Values: vals2)) (subtypes* A0 vals1 vals2)]
;; trivial case for Result ;; trivial case for Result
[((Result: t f o) (Result: t* f o)) [((Result: t f o) (Result: t* f o))
(subtype* A0 t t*)] (subtype* A0 t t*)]
;; we can ignore interesting results ;; we can ignore interesting results
[((Result: t f o) (Result: t* (FilterSet: (Top:) (Top:)) (Empty:))) [((Result: t f o) (Result: t* (FilterSet: (Top:) (Top:)) (Empty:)))
(subtype* A0 t t*)] (subtype* A0 t t*)]
;; subtyping on other stuff ;; subtyping on other stuff
[((Syntax: t) (Syntax: t*)) [((Syntax: t) (Syntax: t*))
(subtype* A0 t t*)] (subtype* A0 t t*)]
[((Future: t) (Future: t*)) [((Future: t) (Future: t*))
(subtype* A0 t t*)] (subtype* A0 t t*)]
[((Instance: t) (Instance: t*)) [((Instance: t) (Instance: t*))
(subtype* A0 t t*)] (subtype* A0 t t*)]
[((Class: '() '() (list (and s (list names meths )) ...)) [((Class: '() '() (list (and s (list names meths )) ...))
(Class: '() '() (list (and s* (list names* meths*)) ...))) (Class: '() '() (list (and s* (list names* meths*)) ...)))
(for/fold ([A A0]) (for/fold ([A A0])
([n names*] [m meths*]) ([n names*] [m meths*])
(cond [(assq n s) => (lambda (spec) (subtype* A (cadr spec) m))] (cond [(assq n s) => (lambda (spec) (subtype* A (cadr spec) m))]
[else (fail! s t)]))] [else (fail! s t)]))]
;; otherwise, not a subtype ;; otherwise, not a subtype
[(_ _) (fail! s t) #;(dprintf "failed")])))])))) [(_ _) (fail! s t) #;(dprintf "failed")])))]))))
(define (type-compare? a b) (define (type-compare? a b)
(and (subtype a b) (subtype b a))) (and (subtype a b) (subtype b a)))