use match*/no-order to reduce manual code duplication
This commit is contained in:
parent
71f17f5cb2
commit
d66816cf76
|
@ -2,7 +2,7 @@
|
|||
|
||||
(require "../utils/utils.rkt")
|
||||
(require (rep type-rep)
|
||||
(types abbrev base-abbrev union subtype remove-intersect resolve)
|
||||
(types abbrev base-abbrev union subtype resolve)
|
||||
"signatures.rkt"
|
||||
racket/match
|
||||
racket/set)
|
||||
|
@ -21,54 +21,51 @@
|
|||
;; (i.e. pairs of t1 t2) to prevent infinite unfolding.
|
||||
;; subtyping performs a similar check for the same
|
||||
;; reason
|
||||
(define (intersect* t1 t2 resolved)
|
||||
(match* (t1 t2)
|
||||
(let intersect
|
||||
([t1 t1] [t2 t2] [resolved (set)])
|
||||
(match*/no-order
|
||||
(t1 t2)
|
||||
;; already a subtype
|
||||
[(_ _) #:when (subtype t1 t2) t1]
|
||||
[(_ _) #:when (subtype t2 t1) t2]
|
||||
[(t1 t2) #:no-order #:when (subtype t1 t2) t1]
|
||||
|
||||
;; polymorphic intersect
|
||||
[(_ (Poly: vars t))
|
||||
[(t1 (Poly: vars t))
|
||||
#:no-order
|
||||
#:when (infer vars null (list t1) (list t) #f)
|
||||
t1]
|
||||
|
||||
;; structural recursion on types
|
||||
[((Pair: a1 d1) (Pair: a2 d2))
|
||||
(build-type -pair
|
||||
(intersect* a1 a2 resolved)
|
||||
(intersect* d1 d2 resolved))]
|
||||
(intersect a1 a2 resolved)
|
||||
(intersect d1 d2 resolved))]
|
||||
;; FIXME: support structural updating for structs when structs are updated to
|
||||
;; contain not only *if* they are polymorphic, but *which* fields are too
|
||||
;;[((Struct: _ _ _ _ _ _)
|
||||
;; (Struct: _ _ _ _ _ _))]
|
||||
[((Syntax: t1*) (Syntax: t2*))
|
||||
(build-type -Syntax (intersect* t1* t2* resolved))]
|
||||
(build-type -Syntax (intersect t1* t2* resolved))]
|
||||
[((Promise: t1*) (Promise: t2*))
|
||||
(build-type -Promise (intersect* t1* t2* resolved))]
|
||||
(build-type -Promise (intersect t1* t2* resolved))]
|
||||
|
||||
;; unions
|
||||
[((Union: t1s) _) (apply Un (map (λ (t1*) (intersect* t1* t2 resolved)) t1s))]
|
||||
[(_ (Union: t2s)) (apply Un (map (λ (t2*) (intersect* t1 t2* resolved)) t2s))]
|
||||
[((Union: t1s) t2)
|
||||
#:no-order
|
||||
(apply Un (map (λ (t1) (intersect t1 t2 resolved)) t1s))]
|
||||
|
||||
;; intersections
|
||||
[((Intersection: t1s) _)
|
||||
[((Intersection: t1s) t2)
|
||||
#:no-order
|
||||
(apply -unsafe-intersect (for/list ([t1 (in-immutable-set t1s)])
|
||||
(intersect* t1 t2 resolved)))]
|
||||
[(_ (Intersection: t2s))
|
||||
(apply -unsafe-intersect (for/list ([t2 (in-immutable-set t2s)])
|
||||
(intersect* t1 t2 resolved)))]
|
||||
(intersect t1 t2 resolved)))]
|
||||
|
||||
;; resolve resolvable types if we haven't already done so
|
||||
[((? needs-resolving?) _)
|
||||
#:when (and (not (set-member? resolved (cons t1 t2)))
|
||||
(not (set-member? resolved (cons t2 t1))))
|
||||
(intersect* (resolve t1) t2 (set-add resolved (cons t1 t2)))]
|
||||
[(_ (? needs-resolving?))
|
||||
#:when (and (not (set-member? resolved (cons t1 t2)))
|
||||
(not (set-member? resolved (cons t2 t1))))
|
||||
(intersect* t1 (resolve t2) (set-add resolved (cons t1 t2)))]
|
||||
[((? needs-resolving? t1) t2)
|
||||
#:no-order
|
||||
#:when (not (or (set-member? resolved (cons t1 t2))
|
||||
(set-member? resolved (cons t2 t1))))
|
||||
(intersect (resolve t1) t2 (set-add resolved (cons t1 t2)))]
|
||||
|
||||
;; t2 and t1 have a complex relationship, so we build an intersection
|
||||
;; (note: intersection checks for overlap)
|
||||
[(_ _) (-unsafe-intersect t1 t2)]))
|
||||
(intersect* t1 t2 (set)))
|
||||
[(t1 t2) (-unsafe-intersect t1 t2)])))
|
||||
|
|
|
@ -55,7 +55,7 @@
|
|||
;; Ugly hack - should use units
|
||||
(lazy-require
|
||||
("../types/union.rkt" (Un))
|
||||
("../types/remove-intersect.rkt" (overlap))
|
||||
("../types/overlap.rkt" (overlap?))
|
||||
("../types/resolve.rkt" (resolve-app)))
|
||||
|
||||
(define name-table (make-weak-hasheq))
|
||||
|
@ -495,7 +495,7 @@
|
|||
[(Univ:) (loop elems ts)]
|
||||
[(Intersection: ts*) (loop (set-union elems ts*) ts)]
|
||||
[t (cond
|
||||
[(for/or ([elem (in-immutable-set elems)]) (not (overlap elem t)))
|
||||
[(for/or ([elem (in-immutable-set elems)]) (not (overlap? elem t)))
|
||||
(*Union (list))]
|
||||
[else (loop (set-add elems t) ts)])])])))
|
||||
|
||||
|
|
|
@ -1,13 +1,12 @@
|
|||
#lang racket/base
|
||||
|
||||
(require (rename-in "../utils/utils.rkt" [infer infer-in]))
|
||||
(require racket/match racket/list
|
||||
(require "../utils/utils.rkt"
|
||||
racket/match racket/list
|
||||
(for-syntax racket/base syntax/parse)
|
||||
(contract-req)
|
||||
(infer-in infer)
|
||||
(rep type-rep prop-rep object-rep rep-utils)
|
||||
(utils tc-utils)
|
||||
(types tc-result resolve subtype remove-intersect union prop-ops)
|
||||
(types tc-result resolve subtype remove update union prop-ops)
|
||||
(env type-env-structs lexical-env)
|
||||
(rename-in (types abbrev)
|
||||
[-> -->]
|
||||
|
@ -17,70 +16,6 @@
|
|||
|
||||
(provide with-lexical-env/extend-props)
|
||||
|
||||
|
||||
(define/cond-contract (update t new-t pos? lo)
|
||||
(Type/c Type/c boolean? (listof PathElem?) . -> . Type/c)
|
||||
;; build-type: build a type while propogating bottom
|
||||
(define (build-type constructor . args)
|
||||
(if (memf Bottom? args) -Bottom (apply constructor args)))
|
||||
(match* ((resolve t) lo)
|
||||
;; pair ops
|
||||
[((Pair: t s) (list rst ... (CarPE:)))
|
||||
(build-type -pair (update t new-t pos? rst) s)]
|
||||
[((Pair: t s) (list rst ... (CdrPE:)))
|
||||
(build-type -pair t (update s new-t pos? rst))]
|
||||
|
||||
;; syntax ops
|
||||
[((Syntax: t) (list rst ... (SyntaxPE:)))
|
||||
(build-type -Syntax (update t new-t pos? rst))]
|
||||
|
||||
;; promise op
|
||||
[((Promise: t) (list rst ... (ForcePE:)))
|
||||
(build-type -Promise (update t new-t pos? rst))]
|
||||
|
||||
;; struct ops
|
||||
[((Struct: nm par flds proc poly pred)
|
||||
(list rst ... (StructPE: (? (lambda (s) (subtype t s)) s) idx)))
|
||||
;; note: this updates fields regardless of whether or not they are
|
||||
;; a polymorphic field. Because subtyping is nominal and accessor
|
||||
;; functions do not reflect this, this behavior is unobservable
|
||||
;; except when an a variable aliases the field in a let binding
|
||||
(let*-values ([(lhs rhs) (split-at flds idx)]
|
||||
[(ty* acc-id) (match rhs
|
||||
[(cons (fld: ty acc-id #f) _)
|
||||
(values (update ty new-t pos? rst) acc-id)]
|
||||
[_ (int-err "update on mutable struct field")])])
|
||||
(cond
|
||||
[(Bottom? ty*) ty*]
|
||||
[else (let ([flds* (append lhs (cons (make-fld ty* acc-id #f) (cdr rhs)))])
|
||||
(make-Struct nm par flds* proc poly pred))]))]
|
||||
|
||||
;; class field ops
|
||||
;;
|
||||
;; A refinement of a private field in a class is really a refinement of the
|
||||
;; return type of the accessor function for that field (rather than a variable).
|
||||
;; We cannot just refine the type of the argument to the accessor, since that
|
||||
;; is an object type that doesn't mention private fields. Thus we use the
|
||||
;; FieldPE path element as a marker to refine the result of the accessor
|
||||
;; function.
|
||||
[((Function: (list (arr: doms (Values: (list (Result: rng _ _))) _ _ _)))
|
||||
(list rst ... (FieldPE:)))
|
||||
(make-Function
|
||||
(list (make-arr* doms (update rng new-t pos? rst))))]
|
||||
|
||||
;; otherwise
|
||||
[(t '())
|
||||
(if pos?
|
||||
(intersect t new-t)
|
||||
(remove t new-t))]
|
||||
[((Union: ts) lo)
|
||||
(apply Un (map (λ (t) (update t new-t pos? lo)) ts))]
|
||||
[(t* lo)
|
||||
;; This likely comes up with (-lst t) and we need to improve the system to make sure this case
|
||||
;; dosen't happen
|
||||
;;(int-err "update along ill-typed path: ~a ~a ~a" t t* lo)
|
||||
t]))
|
||||
|
||||
;; Returns #f if anything becomes (U)
|
||||
(define (env+ env ps)
|
||||
(let/ec exit*
|
||||
|
|
|
@ -6,7 +6,7 @@
|
|||
"signatures.rkt"
|
||||
"check-below.rkt" "../types/kw-types.rkt"
|
||||
(types utils abbrev union subtype type-table path-type
|
||||
prop-ops remove-intersect resolve generalize)
|
||||
prop-ops overlap resolve generalize)
|
||||
(private-in syntax-properties)
|
||||
(rep type-rep prop-rep object-rep)
|
||||
(only-in (infer infer) intersect)
|
||||
|
@ -54,7 +54,7 @@
|
|||
(define ty (path-type alias-path (lookup-type/lexical alias-id)))
|
||||
|
||||
(ret ty
|
||||
(if (overlap ty (-val #f))
|
||||
(if (overlap? ty (-val #f))
|
||||
(-PS (-not-type obj (-val #f)) (-is-type obj (-val #f)))
|
||||
-true-propset)
|
||||
obj))
|
||||
|
|
|
@ -1,7 +1,7 @@
|
|||
#lang racket/unit
|
||||
|
||||
(require "../utils/utils.rkt"
|
||||
(except-in (types utils abbrev prop-ops remove-intersect type-table)
|
||||
(except-in (types utils abbrev prop-ops overlap type-table)
|
||||
-> ->* one-of/c)
|
||||
(only-in (types abbrev) (-> t:->) [->* t:->*])
|
||||
(private type-annotation parse-type syntax-properties)
|
||||
|
@ -65,7 +65,7 @@
|
|||
[f- (in-list fs-)]
|
||||
[o (in-list os)])
|
||||
(cond
|
||||
[(not (overlap t (-val #f)))
|
||||
[(not (overlap? t (-val #f)))
|
||||
(list f+)]
|
||||
[(is-var-mutated? n)
|
||||
(list)]
|
||||
|
|
106
typed-racket-lib/typed-racket/types/overlap.rkt
Normal file
106
typed-racket-lib/typed-racket/types/overlap.rkt
Normal file
|
@ -0,0 +1,106 @@
|
|||
#lang racket/base
|
||||
|
||||
(require "../utils/utils.rkt"
|
||||
(rep type-rep rep-utils)
|
||||
(types abbrev subtype resolve utils)
|
||||
racket/match racket/set)
|
||||
|
||||
|
||||
(provide overlap?)
|
||||
|
||||
(define (simple-datum? v)
|
||||
(or (null? v)
|
||||
(symbol? v)
|
||||
(number? v)
|
||||
(boolean? v)
|
||||
(pair? v)
|
||||
(string? v)
|
||||
(keyword? v)
|
||||
(char? v)
|
||||
(void? v)
|
||||
(eof-object? v)))
|
||||
|
||||
;; overlap?
|
||||
;; Type Type -> Boolean
|
||||
;; a conservative check to see if two types
|
||||
;; have a non-empty intersection
|
||||
(define/cond-contract (overlap? t1 t2)
|
||||
(-> Type/c Type/c boolean?)
|
||||
(define k1 (Type-key t1))
|
||||
(define k2 (Type-key t2))
|
||||
(cond
|
||||
[(type-equal? t1 t2) #t]
|
||||
[(and (symbol? k1) (symbol? k2) (not (eq? k1 k2))) #f]
|
||||
[(and (symbol? k1) (pair? k2) (not (memq k1 k2))) #f]
|
||||
[(and (symbol? k2) (pair? k1) (not (memq k2 k1))) #f]
|
||||
[(and (pair? k1) (pair? k2)
|
||||
(for/and ([i (in-list k1)]) (not (memq i k2))))
|
||||
#f]
|
||||
[else
|
||||
(match*/no-order
|
||||
(t1 t2)
|
||||
[((Univ:) _) #:no-order #t]
|
||||
[((or (B: _) (F: _)) _) #:no-order #t]
|
||||
[((Opaque: _) _) #:no-order #t]
|
||||
[((Name/simple: n) (Name/simple: n*))
|
||||
(or (free-identifier=? n n*)
|
||||
(overlap? (resolve-once t1) (resolve-once t2)))]
|
||||
[(t (? Name? s))
|
||||
#:no-order
|
||||
(overlap? t (resolve-once s))]
|
||||
[((? Mu? t) s) #:no-order (overlap? (unfold t) s)]
|
||||
[((Refinement: t _) s) #:no-order (overlap? t s)]
|
||||
[((Union: ts) s)
|
||||
#:no-order
|
||||
(ormap (λ (t) (overlap? t s)) ts)]
|
||||
[((Intersection: ts) s)
|
||||
#:no-order
|
||||
(for/and ([t (in-immutable-set ts)])
|
||||
(overlap? t s))]
|
||||
[((? Poly?) _) #:no-order #t] ;; conservative
|
||||
[((Base: s1 _ _ _) (Base: s2 _ _ _)) (or (subtype t1 t2) (subtype t2 t1))]
|
||||
[((? Base? t) (? Value? s)) #:no-order (subtype s t)] ;; conservative
|
||||
[((Syntax: t) (Syntax: t*)) (overlap? t t*)]
|
||||
[((Syntax: _) _) #:no-order #f]
|
||||
[((Base: _ _ _ _) _) #:no-order #f]
|
||||
[((Value: (? pair?)) (Pair: _ _)) #:no-order #t]
|
||||
[((Pair: a b) (Pair: a* b*)) (and (overlap? a a*)
|
||||
(overlap? b b*))]
|
||||
;; lots of things are sequences, but not values where sequence? produces #f
|
||||
[((Sequence: _) (Value: v)) #:no-order (sequence? v)]
|
||||
[((Sequence: _) _) #:no-order #t]
|
||||
;; Values where evt? produces #f cannot be Evt
|
||||
[((Evt: _) (Value: v)) #:no-order (evt? v)]
|
||||
[((Pair: _ _) _) #:no-order #f]
|
||||
[((Value: (? simple-datum? v1))
|
||||
(Value: (? simple-datum? v2)))
|
||||
(equal? v1 v2)]
|
||||
[((Value: (? simple-datum?))
|
||||
(or (? Struct?) (? StructTop?) (? Function?)))
|
||||
#:no-order
|
||||
#f]
|
||||
[((Value: (not (? hash?)))
|
||||
(or (? Hashtable?) (? HashtableTop?)))
|
||||
#:no-order
|
||||
#f]
|
||||
[((Struct: n _ flds _ _ _)
|
||||
(Struct: n* _ flds* _ _ _))
|
||||
#:when (free-identifier=? n n*)
|
||||
(for/and ([f (in-list flds)] [f* (in-list flds*)])
|
||||
(match* (f f*)
|
||||
[((fld: t _ _) (fld: t* _ _)) (overlap? t t*)]))]
|
||||
[((Struct: n #f _ _ _ _)
|
||||
(StructTop: (Struct: n* #f _ _ _ _)))
|
||||
#:when (free-identifier=? n n*)
|
||||
#t]
|
||||
;; n and n* must be different, so there's no overlap
|
||||
[((Struct: n #f flds _ _ _)
|
||||
(Struct: n* #f flds* _ _ _))
|
||||
#f]
|
||||
[((Struct: n #f flds _ _ _)
|
||||
(StructTop: (Struct: n* #f flds* _ _ _)))
|
||||
#f]
|
||||
[((and t1 (Struct: _ _ _ _ #f _))
|
||||
(and t2 (Struct: _ _ _ _ #f _)))
|
||||
(or (subtype t1 t2) (subtype t2 t1))]
|
||||
[(_ _) #t])]))
|
|
@ -5,7 +5,7 @@
|
|||
(prefix-in c: (contract-req))
|
||||
(rep type-rep prop-rep object-rep rep-utils)
|
||||
(only-in (infer infer) intersect)
|
||||
(types union subtype remove-intersect abbrev tc-result))
|
||||
(types union subtype overlap abbrev tc-result))
|
||||
|
||||
(provide/cond-contract
|
||||
[-and (c:->* () #:rest (c:listof Prop?) Prop?)]
|
||||
|
@ -80,7 +80,7 @@
|
|||
(subtype t2 t1)]
|
||||
;; t1 ∩ t2 = ∅ ?
|
||||
[((TypeProp: o t1) (NotTypeProp: o t2))
|
||||
(not (overlap t1 t2))]
|
||||
(not (overlap? t1 t2))]
|
||||
;; otherwise we give up
|
||||
[(_ _) #f]))
|
||||
|
||||
|
|
|
@ -1,120 +0,0 @@
|
|||
#lang racket/base
|
||||
|
||||
(require "../utils/utils.rkt"
|
||||
(rep type-rep rep-utils)
|
||||
(types union subtype resolve utils)
|
||||
racket/match racket/set)
|
||||
|
||||
(provide (rename-out [*remove remove]) overlap)
|
||||
|
||||
(define (simple-datum? v)
|
||||
(or (null? v)
|
||||
(symbol? v)
|
||||
(number? v)
|
||||
(boolean? v)
|
||||
(pair? v)
|
||||
(string? v)
|
||||
(keyword? v)
|
||||
(char? v)
|
||||
(void? v)
|
||||
(eof-object? v)))
|
||||
|
||||
|
||||
(define (overlap t1 t2)
|
||||
(let ([ks (Type-key t1)] [kt (Type-key t2)])
|
||||
(cond
|
||||
[(type-equal? t1 t2) #t]
|
||||
[(and (symbol? ks) (symbol? kt) (not (eq? ks kt))) #f]
|
||||
[(and (symbol? ks) (pair? kt) (not (memq ks kt))) #f]
|
||||
[(and (symbol? kt) (pair? ks) (not (memq kt ks))) #f]
|
||||
[(and (pair? ks) (pair? kt)
|
||||
(for/and ([i (in-list ks)]) (not (memq i kt))))
|
||||
#f]
|
||||
[else
|
||||
(match (list t1 t2)
|
||||
[(list-no-order (Univ:) _) #t]
|
||||
[(list-no-order (or (B: _) (F: _)) _) #t]
|
||||
[(list-no-order (Opaque: _) _) #t]
|
||||
[(list (Name/simple: n) (Name/simple: n*))
|
||||
(or (free-identifier=? n n*)
|
||||
(overlap (resolve-once t1) (resolve-once t2)))]
|
||||
[(list-no-order t (? Name? s))
|
||||
(overlap t (resolve-once s))]
|
||||
[(list-no-order (? Mu? t) s) (overlap (unfold t) s)]
|
||||
[(list-no-order (Refinement: t _) s) (overlap t s)]
|
||||
[(list-no-order (Union: ts) s)
|
||||
(ormap (lambda (t*) (overlap t* s)) ts)]
|
||||
[(list-no-order (Intersection: ts) s)
|
||||
(for/and ([t (in-immutable-set ts)])
|
||||
(overlap t s))]
|
||||
[(list-no-order (? Poly?) _) #t] ;; conservative
|
||||
[(list (Base: s1 _ _ _) (Base: s2 _ _ _)) (or (subtype t1 t2) (subtype t2 t1))]
|
||||
[(list-no-order (? Base? t) (? Value? s)) (subtype s t)] ;; conservative
|
||||
[(list (Syntax: t) (Syntax: t*)) (overlap t t*)]
|
||||
[(list-no-order (Syntax: _) _) #f]
|
||||
[(list-no-order (Base: _ _ _ _) _) #f]
|
||||
[(list-no-order (Value: (? pair?)) (Pair: _ _)) #t]
|
||||
[(list (Pair: a b) (Pair: a* b*)) (and (overlap a a*)
|
||||
(overlap b b*))]
|
||||
;; lots of things are sequences, but not values where sequence? produces #f
|
||||
[(list-no-order (Sequence: _) (Value: v)) (sequence? v)]
|
||||
[(list-no-order (Sequence: _) _) #t]
|
||||
;; Values where evt? produces #f cannot be Evt
|
||||
[(list-no-order (Evt: _) (Value: v)) (evt? v)]
|
||||
[(list-no-order (Pair: _ _) _) #f]
|
||||
[(list (Value: (? simple-datum? v1))
|
||||
(Value: (? simple-datum? v2)))
|
||||
(equal? v1 v2)]
|
||||
[(list-no-order (Value: (? simple-datum?))
|
||||
(or (? Struct?) (? StructTop?) (? Function?)))
|
||||
#f]
|
||||
[(list-no-order (Value: (not (? hash?)))
|
||||
(or (? Hashtable?) (? HashtableTop?)))
|
||||
#f]
|
||||
[(list (Struct: n _ flds _ _ _)
|
||||
(Struct: n* _ flds* _ _ _))
|
||||
#:when (free-identifier=? n n*)
|
||||
(for/and ([f (in-list flds)] [f* (in-list flds*)])
|
||||
(match* (f f*)
|
||||
[((fld: t _ _) (fld: t* _ _)) (overlap t t*)]))]
|
||||
[(list (Struct: n #f _ _ _ _)
|
||||
(StructTop: (Struct: n* #f _ _ _ _)))
|
||||
#:when (free-identifier=? n n*)
|
||||
#t]
|
||||
;; n and n* must be different, so there's no overlap
|
||||
[(list (Struct: n #f flds _ _ _)
|
||||
(Struct: n* #f flds* _ _ _))
|
||||
#f]
|
||||
[(list (Struct: n #f flds _ _ _)
|
||||
(StructTop: (Struct: n* #f flds* _ _ _)))
|
||||
#f]
|
||||
[(list (and t1 (Struct: _ _ _ _ #f _))
|
||||
(and t2 (Struct: _ _ _ _ #f _)))
|
||||
(or (subtype t1 t2) (subtype t2 t1))]
|
||||
[else #t])])))
|
||||
|
||||
|
||||
;(trace overlap)
|
||||
|
||||
;; also not yet correct
|
||||
;; produces old without the contents of rem
|
||||
(define (*remove old rem)
|
||||
(define initial
|
||||
(if (subtype old rem)
|
||||
(Un) ;; the empty type
|
||||
(match (list old rem)
|
||||
[(list (or (App: _ _ _) (? Name?)) t)
|
||||
;; must be different, since they're not subtypes
|
||||
;; and n must refer to a distinct struct type
|
||||
old]
|
||||
[(list (Union: l) rem)
|
||||
(apply Un (map (lambda (e) (*remove e rem)) l))]
|
||||
[(list (Intersection: ts) rem)
|
||||
(apply -unsafe-intersect
|
||||
(for/list ([t (in-immutable-set ts)]) (*remove t rem)))]
|
||||
[(list (? Mu? old) t) (*remove (unfold old) t)]
|
||||
[(list (Poly: vs b) t) (make-Poly vs (*remove b rem))]
|
||||
[_ old])))
|
||||
(if (subtype old initial) old initial))
|
||||
|
||||
;(trace *remove)
|
32
typed-racket-lib/typed-racket/types/remove.rkt
Normal file
32
typed-racket-lib/typed-racket/types/remove.rkt
Normal file
|
@ -0,0 +1,32 @@
|
|||
#lang racket/base
|
||||
|
||||
(require "../utils/utils.rkt"
|
||||
(rep type-rep rep-utils)
|
||||
(types abbrev union subtype resolve utils)
|
||||
racket/match racket/set)
|
||||
|
||||
(provide remove)
|
||||
|
||||
|
||||
;; remove
|
||||
;; Type Type -> Type
|
||||
;; conservatively calculates set subtraction
|
||||
;; between the types (i.e. t - s)
|
||||
(define (remove t s)
|
||||
(define result
|
||||
(let rem ([t t])
|
||||
(match t
|
||||
[_ #:when (subtype t s) -Bottom]
|
||||
[(or (App: _ _ _) (? Name?))
|
||||
;; must be different, since they're not subtypes
|
||||
;; and n must refer to a distinct struct type
|
||||
t]
|
||||
[(Union: elems) (apply Un (map rem elems))]
|
||||
[(Intersection: ts)
|
||||
(apply -unsafe-intersect (set-map ts rem))]
|
||||
[(? Mu?) (rem (unfold t))]
|
||||
[(Poly: vs b) (make-Poly vs (rem b))]
|
||||
[_ t])))
|
||||
(cond
|
||||
[(subtype t result) t]
|
||||
[else result]))
|
|
@ -480,14 +480,12 @@
|
|||
(loop (cdr l1) (cdr l2))]
|
||||
[else
|
||||
(loop l1 (cdr l2))]))]
|
||||
[((Union: es) t)
|
||||
[((Union: elems) t)
|
||||
(and
|
||||
(for/and ([elem (in-list es)])
|
||||
(subtype* A0 elem t))
|
||||
(andmap (λ (elem) (subtype* A0 elem t)) elems)
|
||||
A0)]
|
||||
[(s (Union: es))
|
||||
(and (for/or ([elem (in-list es)])
|
||||
(subtype* A0 s elem))
|
||||
[(s (Union: elems))
|
||||
(and (ormap (λ (elem) (subtype* A0 s elem)) elems)
|
||||
A0)]
|
||||
;; subtyping on immutable structs is covariant
|
||||
[((Struct: nm _ flds proc _ _) (Struct: nm* _ flds* proc* _ _))
|
||||
|
|
91
typed-racket-lib/typed-racket/types/update.rkt
Normal file
91
typed-racket-lib/typed-racket/types/update.rkt
Normal file
|
@ -0,0 +1,91 @@
|
|||
#lang racket/base
|
||||
|
||||
(require (rename-in "../utils/utils.rkt" [infer infer-in]))
|
||||
(require racket/match racket/list
|
||||
(contract-req)
|
||||
(infer-in infer)
|
||||
(rep type-rep prop-rep object-rep rep-utils)
|
||||
(utils tc-utils)
|
||||
(types abbrev resolve subtype remove union))
|
||||
|
||||
|
||||
(provide update)
|
||||
|
||||
;; update
|
||||
;; t : type being updated
|
||||
;; new-t : new type
|
||||
;; pos? : whether the update is positive or negative
|
||||
;; path-elems : which fields we're traversing to update,
|
||||
;; in *syntactic order* (e.g. (car (cdr x)) -> '(car cdr))
|
||||
(define/cond-contract (update t new-t pos? path-elems)
|
||||
(Type/c Type/c boolean? (listof PathElem?) . -> . Type/c)
|
||||
;; build-type: build a type while propogating bottom
|
||||
(define (build constructor . args)
|
||||
(if (memf Bottom? args) -Bottom (apply constructor args)))
|
||||
;; update's inner recursive loop
|
||||
;; puts path in *accessed* order
|
||||
;; (i.e. (car (cdr x)) --> (list cdr car))
|
||||
(let update
|
||||
([t t] [path (reverse path-elems)])
|
||||
(match path
|
||||
;; path is empty (base case)
|
||||
[(list) (cond
|
||||
[pos? (intersect (resolve t) new-t)]
|
||||
[else (remove (resolve t) new-t)])]
|
||||
;; path is non-empty
|
||||
;; (i.e. there is some field access we'll try and traverse)
|
||||
[(cons path-elem rst)
|
||||
(match* ((resolve t) path-elem)
|
||||
;; pair ops
|
||||
[((Pair: t s) (CarPE:))
|
||||
(build -pair (update t rst) s)]
|
||||
[((Pair: t s) (CdrPE:))
|
||||
(build -pair t (update s rst))]
|
||||
;; syntax ops
|
||||
[((Syntax: t) (SyntaxPE:))
|
||||
(build -Syntax (update t rst))]
|
||||
;; promise op
|
||||
[((Promise: t) (ForcePE:))
|
||||
(build -Promise (update t rst))]
|
||||
|
||||
;; struct ops
|
||||
[((Struct: nm par flds proc poly pred)
|
||||
(StructPE: (? (λ (s) (subtype t s))) idx))
|
||||
;; Note: this updates fields even if they are not polymorphic.
|
||||
;; Because subtyping is nominal and accessor functions do not
|
||||
;; reflect this, this behavior is unobservable except when a
|
||||
;; variable aliases the field in a let binding
|
||||
(define-values (lhs rhs) (split-at flds idx))
|
||||
(define-values (ty* acc-id)
|
||||
(match rhs
|
||||
[(cons (fld: ty acc-id #f) _)
|
||||
(values (update ty rst) acc-id)]
|
||||
[_ (int-err "update on mutable struct field")]))
|
||||
(cond
|
||||
[(Bottom? ty*) ty*]
|
||||
[else
|
||||
(define flds*
|
||||
(append lhs (cons (make-fld ty* acc-id #f) (cdr rhs))))
|
||||
(make-Struct nm par flds* proc poly pred)])]
|
||||
|
||||
;; class field ops
|
||||
;;
|
||||
;; A refinement of a private field in a class is really a refinement of the
|
||||
;; return type of the accessor function for that field (rather than a variable).
|
||||
;; We cannot just refine the type of the argument to the accessor, since that
|
||||
;; is an object type that doesn't mention private fields. Thus we use the
|
||||
;; FieldPE path element as a marker to refine the result of the accessor
|
||||
;; function.
|
||||
[((Function: (list (arr: doms (Values: (list (Result: rng _ _))) _ _ _)))
|
||||
(FieldPE:))
|
||||
(make-Function
|
||||
(list (make-arr* doms (update rng rst))))]
|
||||
|
||||
[((Union: ts) _)
|
||||
(apply Un (map (λ (t) (update t path)) ts))]
|
||||
|
||||
[(_ _)
|
||||
;; This likely comes up with (-lst t) and we need to improve the system to make sure this case
|
||||
;; dosen't happen
|
||||
;;(int-err "update along ill-typed path: ~a ~a ~a" t t* lo)
|
||||
t])])))
|
|
@ -7,6 +7,7 @@ at least theoretically.
|
|||
|
||||
(require (for-syntax racket/base syntax/parse/pre racket/string)
|
||||
racket/require-syntax racket/provide-syntax
|
||||
racket/match
|
||||
racket/struct-info "timing.rkt")
|
||||
|
||||
(provide
|
||||
|
@ -20,7 +21,8 @@ at least theoretically.
|
|||
list-extend
|
||||
filter-multiple
|
||||
syntax-length
|
||||
in-sequence-forever)
|
||||
in-sequence-forever
|
||||
match*/no-order)
|
||||
|
||||
(define optimize? (make-parameter #t))
|
||||
(define-for-syntax enable-contracts? (and (getenv "PLT_TR_CONTRACTS") #t))
|
||||
|
@ -232,3 +234,22 @@ at least theoretically.
|
|||
(λ (_) #t)
|
||||
(λ _ #t)
|
||||
(λ _ #t))))))
|
||||
|
||||
(define-syntax (match*/no-order stx)
|
||||
(define (parse-clauses clauses)
|
||||
(syntax-parse clauses
|
||||
[() #'()]
|
||||
[([(lpat rpat) #:no-order . body]
|
||||
. rst)
|
||||
#`([(lpat rpat) . body]
|
||||
[(rpat lpat) . body]
|
||||
. #,(parse-clauses #'rst))]
|
||||
[((~and cl [(lpat rpat) . body])
|
||||
. rst)
|
||||
#`(#,(syntax/loc #'cl [(lpat rpat) . body])
|
||||
. #,(parse-clauses #'rst))]))
|
||||
(syntax-parse stx
|
||||
[(_ (val1:expr val2:expr)
|
||||
. clauses)
|
||||
#`(match* (val1 val2)
|
||||
. #,(parse-clauses #'clauses))]))
|
||||
|
|
|
@ -3,7 +3,7 @@
|
|||
(for-syntax racket/base)
|
||||
(r:infer infer)
|
||||
(rep type-rep)
|
||||
(types abbrev numeric-tower subtype union remove-intersect)
|
||||
(types abbrev numeric-tower subtype union remove overlap)
|
||||
rackunit)
|
||||
(provide tests)
|
||||
(gen-test-main)
|
||||
|
@ -12,7 +12,9 @@
|
|||
(syntax-case stx ()
|
||||
[(_ [t1 t2 res] ...)
|
||||
#'(test-suite "Tests for overlap"
|
||||
(test-check (format "~a ~a" 't1 't2) (lambda (a b) (eq? (not (not a)) b)) (overlap t1 t2) res) ...)]))
|
||||
(test-check (format "~a ~a" 't1 't2)
|
||||
(lambda (a b) (eq? (not (not a)) b))
|
||||
(overlap? t1 t2) res) ...)]))
|
||||
|
||||
(define overlap-tests
|
||||
(over-tests
|
||||
|
@ -22,7 +24,9 @@
|
|||
(syntax-case stx ()
|
||||
[(_ [t1 t2 res] ...)
|
||||
#'(test-suite "Tests for intersect"
|
||||
(test-check (format "~a ~a" 't1 't2) type-compare? (intersect t1 t2) res) ...)]))
|
||||
(test-check (format "~a ~a" 't1 't2)
|
||||
type-compare?
|
||||
(intersect t1 t2) res) ...)]))
|
||||
|
||||
|
||||
(define intersect-tests
|
||||
|
@ -61,14 +65,20 @@
|
|||
(remo-tests
|
||||
[(Un -Number -Symbol) -Number -Symbol]
|
||||
[-Number -Number (Un)]
|
||||
[(-mu x (Un -Number -Symbol (make-Listof x))) -Number (Un -Symbol (make-Listof (-mu x (Un -Number -Symbol (make-Listof x)))))]
|
||||
[(-mu x (Un -Number -Symbol -Boolean (make-Listof x))) -Number (Un -Symbol -Boolean (make-Listof (-mu x (Un -Number -Symbol -Boolean (make-Listof x)))))]
|
||||
[(-mu x (Un -Number -Symbol (make-Listof x)))
|
||||
-Number
|
||||
(Un -Symbol (make-Listof (-mu x (Un -Number -Symbol (make-Listof x)))))]
|
||||
[(-mu x (Un -Number -Symbol -Boolean (make-Listof x)))
|
||||
-Number
|
||||
(Un -Symbol -Boolean (make-Listof (-mu x (Un -Number -Symbol -Boolean (make-Listof x)))))]
|
||||
[(Un (-val #f) (-mu x (Un -Number -Symbol (make-Listof (-v x)))))
|
||||
(Un -Boolean -Number)
|
||||
(Un -Symbol (make-Listof (-mu x (Un -Number -Symbol (make-Listof x)))))]
|
||||
[(Un (-val 'foo) (-val 6)) (Un -Number -Symbol) (Un)]
|
||||
[(-> (Un -Symbol -Number) -Number) (-> -Number -Number) (Un)]
|
||||
[(Un (-poly (a) (make-Listof a)) (-> -Number -Number)) (-> -Number -Number) (-poly (a) (make-Listof a))]
|
||||
[(Un (-poly (a) (make-Listof a)) (-> -Number -Number))
|
||||
(-> -Number -Number)
|
||||
(-poly (a) (make-Listof a))]
|
||||
[(Un -Symbol -Number) (-poly (a) -Number) -Symbol]
|
||||
[(-pair -Number (-v a)) (-pair Univ Univ) (Un)]
|
||||
))
|
||||
|
|
Loading…
Reference in New Issue
Block a user