rename restrict to intersect
since 'restrict' will now create intersections when there is a complex relationship between the two types, calling it 'intersect' makes a lot more sense.
This commit is contained in:
Andrew Kent
parent
b4a4c174e4
commit
c7a3fb0cf1
typed-racket-lib/typed-racket
infer
private
rep
typecheck
types
typed-racket-test/unit-tests
|
|
@ -7,7 +7,7 @@
|
|||
racket/match
|
||||
racket/list)
|
||||
|
||||
(import restrict^ dmap^)
|
||||
(import intersect^ dmap^)
|
||||
(export constraints^)
|
||||
|
||||
;; Widest constraint possible
|
||||
|
|
@ -34,7 +34,7 @@
|
|||
;; intersect the given types. produces a lower bound on both, but
|
||||
;; perhaps not the GLB
|
||||
(define (meet S T)
|
||||
(let ([s* (restrict S T)])
|
||||
(let ([s* (intersect S T)])
|
||||
(if (and (subtype s* S)
|
||||
(subtype s* T))
|
||||
s*
|
||||
|
|
|
|||
|
|
@ -1,11 +1,11 @@
|
|||
#lang racket/base
|
||||
|
||||
(require "infer-unit.rkt" "constraints.rkt" "dmap.rkt" "signatures.rkt"
|
||||
"restrict.rkt"
|
||||
"intersect.rkt"
|
||||
(only-in racket/unit provide-signature-elements
|
||||
define-values/invoke-unit/infer link))
|
||||
|
||||
(provide-signature-elements restrict^ infer^)
|
||||
(provide-signature-elements intersect^ infer^)
|
||||
|
||||
(define-values/invoke-unit/infer
|
||||
(link infer@ constraints@ dmap@ restrict@))
|
||||
(link infer@ constraints@ dmap@ intersect@))
|
||||
|
|
|
|||
74
typed-racket-lib/typed-racket/infer/intersect.rkt
Normal file
74
typed-racket-lib/typed-racket/infer/intersect.rkt
Normal file
|
|
@ -0,0 +1,74 @@
|
|||
#lang racket/unit
|
||||
|
||||
(require "../utils/utils.rkt")
|
||||
(require (rep type-rep)
|
||||
(types abbrev base-abbrev union subtype remove-intersect resolve)
|
||||
"signatures.rkt"
|
||||
racket/match
|
||||
racket/set)
|
||||
|
||||
(import infer^)
|
||||
(export intersect^)
|
||||
|
||||
|
||||
;; compute the intersection of two types
|
||||
;; (note: previously called restrict)
|
||||
(define (intersect t1 t2)
|
||||
;; build-type: build a type while propogating bottom
|
||||
(define (build-type constructor . args)
|
||||
(if (memf Bottom? args) -Bottom (apply constructor args)))
|
||||
;; resolved is a set tracking previously seen intersect cases
|
||||
;; (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)
|
||||
;; already a subtype
|
||||
[(_ _) #:when (subtype t1 t2) t1]
|
||||
[(_ _) #:when (subtype t2 t1) t2]
|
||||
|
||||
;; polymorphic intersect
|
||||
[(_ (Poly: vars t))
|
||||
#: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))]
|
||||
;; 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))]
|
||||
[((Promise: t1*) (Promise: t2*))
|
||||
(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))]
|
||||
|
||||
;; intersections
|
||||
[((Intersection: t1s) _)
|
||||
(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)))]
|
||||
|
||||
;; 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)))]
|
||||
|
||||
;; 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)))
|
||||
|
|
@ -1,72 +0,0 @@
|
|||
#lang racket/unit
|
||||
|
||||
(require "../utils/utils.rkt")
|
||||
(require (rep type-rep)
|
||||
(types abbrev base-abbrev union subtype remove-intersect resolve)
|
||||
"signatures.rkt"
|
||||
racket/match
|
||||
racket/set)
|
||||
|
||||
(import infer^)
|
||||
(export restrict^)
|
||||
|
||||
|
||||
;; restrict t1 to be a subtype of t2
|
||||
(define (restrict t1 t2)
|
||||
;; build-type: build a type while propogating bottom
|
||||
(define (build-type constructor . args)
|
||||
(if (memf Bottom? args) -Bottom (apply constructor args)))
|
||||
;; resolved is a set tracking previously seen restrict cases
|
||||
;; (i.e. pairs of t1 t2) to prevent infinite unfolding.
|
||||
;; subtyping performs a similar check for the same
|
||||
;; reason
|
||||
(define (restrict* t1 t2 resolved)
|
||||
(match* (t1 t2)
|
||||
;; already a subtype
|
||||
[(_ _) #:when (subtype t1 t2)
|
||||
t1]
|
||||
|
||||
;; polymorphic restrict
|
||||
[(_ (Poly: vars t)) #:when (infer vars null (list t1) (list t) #f)
|
||||
t1]
|
||||
|
||||
;; structural recursion on types
|
||||
[((Pair: a1 d1) (Pair: a2 d2))
|
||||
(build-type -pair
|
||||
(restrict* a1 a2 resolved)
|
||||
(restrict* 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 (restrict* t1* t2* resolved))]
|
||||
[((Promise: t1*) (Promise: t2*))
|
||||
(build-type -Promise (restrict* t1* t2* resolved))]
|
||||
|
||||
;; unions
|
||||
[((Union: t1s) _) (apply Un (map (λ (t1*) (restrict* t1* t2 resolved)) t1s))]
|
||||
[(_ (Union: t2s)) (apply Un (map (λ (t2*) (restrict* t1 t2* resolved)) t2s))]
|
||||
|
||||
;; intersections
|
||||
[((Intersection: t1s) _)
|
||||
(apply -unsafe-intersect (for/list ([t1 (in-immutable-set t1s)])
|
||||
(restrict* t1 t2 resolved)))]
|
||||
[(_ (Intersection: t2s))
|
||||
(apply -unsafe-intersect (for/list ([t2 (in-immutable-set t2s)])
|
||||
(restrict* t1 t2 resolved)))]
|
||||
|
||||
;; resolve resolvable types if we haven't already done so
|
||||
[((? needs-resolving?) _) #:when (not (set-member? resolved (cons t1 t2)))
|
||||
(restrict* (resolve t1) t2 (set-add resolved (cons t1 t2)))]
|
||||
[(_ (? needs-resolving?)) #:when (not (set-member? resolved (cons t1 t2)))
|
||||
(restrict* t1 (resolve t2) (set-add resolved (cons t1 t2)))]
|
||||
|
||||
;; we don't actually want this - want something that's a part of t1
|
||||
[(_ _) #:when (subtype t2 t1)
|
||||
t2]
|
||||
|
||||
;; t2 and t1 have a complex relationship, so we intersect
|
||||
;; (note: intersection checks for overlap)
|
||||
[(_ _) (-unsafe-intersect t1 t2)]))
|
||||
(restrict* t1 t2 (set)))
|
||||
|
|
@ -20,8 +20,8 @@
|
|||
[cond-contracted cset-join ((listof cset?) . -> . cset?)]
|
||||
[cond-contracted c-meet ((c? c?) (symbol?) . ->* . (or/c #f c?))]))
|
||||
|
||||
(define-signature restrict^
|
||||
([cond-contracted restrict ((Type/c Type/c) ((or/c 'new 'orig)) . ->* . Type/c)]))
|
||||
(define-signature intersect^
|
||||
([cond-contracted intersect (Type/c Type/c . -> . Type/c)]))
|
||||
|
||||
(define-signature infer^
|
||||
([cond-contracted infer ((;; variables from the forall
|
||||
|
|
|
|||
|
|
@ -7,7 +7,7 @@
|
|||
(rename-in (types abbrev union utils prop-ops resolve
|
||||
classes prefab signatures)
|
||||
[make-arr* make-arr])
|
||||
(only-in (infer-in infer) restrict)
|
||||
(only-in (infer-in infer) intersect)
|
||||
(utils tc-utils stxclass-util literal-syntax-class)
|
||||
syntax/stx (prefix-in c: (contract-req))
|
||||
syntax/parse racket/sequence
|
||||
|
|
@ -471,7 +471,7 @@
|
|||
[(:∩^ ts ...)
|
||||
(for/fold ([ty Univ])
|
||||
([t (in-list (parse-types #'(ts ...)))])
|
||||
(restrict ty t))]
|
||||
(intersect ty t))]
|
||||
[(:quote^ t)
|
||||
(parse-quoted-type #'t)]
|
||||
[(:All^ . rest)
|
||||
|
|
|
|||
|
|
@ -476,7 +476,7 @@
|
|||
|
||||
;; constructor for intersections
|
||||
;; in general, intersections should be built
|
||||
;; using the 'restrict' operator, which worries
|
||||
;; using the 'intersect' operator, which worries
|
||||
;; about actual subtyping, etc...
|
||||
(define (-unsafe-intersect . ts)
|
||||
(let loop ([elems (set)]
|
||||
|
|
|
|||
|
|
@ -71,7 +71,7 @@
|
|||
;; otherwise
|
||||
[(t '())
|
||||
(if pos?
|
||||
(restrict t new-t)
|
||||
(intersect t new-t)
|
||||
(remove t new-t))]
|
||||
[((Union: ts) lo)
|
||||
(apply Un (map (λ (t) (update t new-t pos? lo)) ts))]
|
||||
|
|
|
|||
|
|
@ -9,7 +9,7 @@
|
|||
prop-ops remove-intersect resolve generalize)
|
||||
(private-in syntax-properties)
|
||||
(rep type-rep prop-rep object-rep)
|
||||
(only-in (infer infer) restrict)
|
||||
(only-in (infer infer) intersect)
|
||||
(utils tc-utils)
|
||||
(env lexical-env)
|
||||
racket/list
|
||||
|
|
@ -366,18 +366,18 @@
|
|||
(define (find-stx-type datum-stx [expected #f])
|
||||
(match datum-stx
|
||||
[(? syntax? (app syntax-e stx-e))
|
||||
(match (and expected (resolve (restrict expected (-Syntax Univ))))
|
||||
(match (and expected (resolve (intersect expected (-Syntax Univ))))
|
||||
[(Syntax: t) (-Syntax (find-stx-type stx-e t))]
|
||||
[_ (-Syntax (find-stx-type stx-e))])]
|
||||
[(or (? symbol?) (? null?) (? number?) (? extflonum?) (? boolean?) (? string?) (? char?)
|
||||
(? bytes?) (? regexp?) (? byte-regexp?) (? keyword?))
|
||||
(tc-literal #`#,datum-stx expected)]
|
||||
[(cons car cdr)
|
||||
(match (and expected (resolve (restrict expected (-pair Univ Univ))))
|
||||
(match (and expected (resolve (intersect expected (-pair Univ Univ))))
|
||||
[(Pair: car-t cdr-t) (-pair (find-stx-type car car-t) (find-stx-type cdr cdr-t))]
|
||||
[_ (-pair (find-stx-type car) (find-stx-type cdr))])]
|
||||
[(vector xs ...)
|
||||
(match (and expected (resolve (restrict expected -VectorTop)))
|
||||
(match (and expected (resolve (intersect expected -VectorTop)))
|
||||
[(Vector: t)
|
||||
(make-Vector
|
||||
(check-below
|
||||
|
|
@ -393,11 +393,11 @@
|
|||
[_ (make-HeterogeneousVector (for/list ([x (in-list xs)])
|
||||
(generalize (find-stx-type x #f))))])]
|
||||
[(box x)
|
||||
(match (and expected (resolve (restrict expected -BoxTop)))
|
||||
(match (and expected (resolve (intersect expected -BoxTop)))
|
||||
[(Box: t) (-box (check-below (find-stx-type x t) t))]
|
||||
[_ (-box (generalize (find-stx-type x)))])]
|
||||
[(? hash? h)
|
||||
(match (and expected (resolve (restrict expected -HashTop)))
|
||||
(match (and expected (resolve (intersect expected -HashTop)))
|
||||
[(Hashtable: kt vt)
|
||||
(define kts (hash-map h (lambda (x y) (find-stx-type x kt))))
|
||||
(define vts (hash-map h (lambda (x y) (find-stx-type y vt))))
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@
|
|||
(types abbrev numeric-tower resolve subtype union generalize
|
||||
prefab)
|
||||
(rep type-rep)
|
||||
(only-in (infer infer) restrict)
|
||||
(only-in (infer infer) intersect)
|
||||
(utils stxclass-util)
|
||||
syntax/parse
|
||||
racket/function
|
||||
|
|
@ -89,7 +89,7 @@
|
|||
[i:regexp -Regexp]
|
||||
[() -Null]
|
||||
[(i . r)
|
||||
(match (and expected (resolve (restrict expected (-pair Univ Univ))))
|
||||
(match (and expected (resolve (intersect expected (-pair Univ Univ))))
|
||||
[(Pair: a-ty d-ty)
|
||||
(-pair
|
||||
(tc-literal #'i a-ty)
|
||||
|
|
@ -97,7 +97,7 @@
|
|||
[t
|
||||
(-pair (tc-literal #'i) (tc-literal #'r))])]
|
||||
[(~var i (3d vector?))
|
||||
(match (and expected (resolve (restrict expected -VectorTop)))
|
||||
(match (and expected (resolve (intersect expected -VectorTop)))
|
||||
[(Vector: t)
|
||||
(make-Vector
|
||||
(check-below
|
||||
|
|
@ -113,7 +113,7 @@
|
|||
[_ (make-HeterogeneousVector (for/list ([l (in-vector (syntax-e #'i))])
|
||||
(generalize (tc-literal l #f))))])]
|
||||
[(~var i (3d hash?))
|
||||
(match (and expected (resolve (restrict expected -HashTop)))
|
||||
(match (and expected (resolve (intersect expected -HashTop)))
|
||||
[(Hashtable: k v)
|
||||
(let* ([h (syntax-e #'i)]
|
||||
[ks (hash-map h (lambda (x y) (tc-literal x k)))]
|
||||
|
|
|
|||
|
|
@ -8,7 +8,7 @@
|
|||
(contract-req)
|
||||
(except-in (types abbrev utils prop-ops path-type)
|
||||
-> ->* one-of/c)
|
||||
(only-in (infer infer) restrict)
|
||||
(only-in (infer infer) intersect)
|
||||
(rep type-rep object-rep prop-rep rep-utils))
|
||||
|
||||
(provide add-scope)
|
||||
|
|
@ -76,8 +76,8 @@
|
|||
(tc-result
|
||||
(if (equal? argument-side Err)
|
||||
(subst-type r-t k o polarity t)
|
||||
(restrict argument-side
|
||||
(subst-type r-t k o polarity t)))
|
||||
(intersect argument-side
|
||||
(subst-type r-t k o polarity t)))
|
||||
(subst-prop-set r-fs k o polarity t)
|
||||
(subst-object r-o k o polarity)))
|
||||
|
||||
|
|
@ -164,11 +164,11 @@
|
|||
(define ty/path (path-type pes ty))
|
||||
(maker
|
||||
(-acc-path pes o)
|
||||
;; don't restrict if the path doesn't match the type
|
||||
;; don't intersect if the path doesn't match the type
|
||||
(if (equal? ty/path Err)
|
||||
(subst-type t k o polarity ty)
|
||||
(restrict ty/path
|
||||
(subst-type t k o polarity ty))))])]
|
||||
(intersect ty/path
|
||||
(subst-type t k o polarity ty))))])]
|
||||
[else p]))
|
||||
|
||||
(match p
|
||||
|
|
|
|||
|
|
@ -4,7 +4,7 @@
|
|||
racket/list racket/match
|
||||
(prefix-in c: (contract-req))
|
||||
(rep type-rep prop-rep object-rep rep-utils)
|
||||
(only-in (infer infer) restrict)
|
||||
(only-in (infer infer) intersect)
|
||||
(types union subtype remove-intersect abbrev tc-result))
|
||||
|
||||
(provide/cond-contract
|
||||
|
|
@ -92,7 +92,7 @@
|
|||
;; or? : is this an Or (alternative is And)
|
||||
;;
|
||||
;; This combines all the TypeProps at the same path into one TypeProp. If it is an Or the
|
||||
;; combination is done using Un, otherwise, restrict. The reverse is done for NotTypeProps. If it is
|
||||
;; combination is done using Un, otherwise, intersect. The reverse is done for NotTypeProps. If it is
|
||||
;; an Or this simplifies to -tt if any of the atomic props simplified to -tt, and removes
|
||||
;; any -ff values. The reverse is done if this is an And.
|
||||
;;
|
||||
|
|
@ -100,8 +100,8 @@
|
|||
((c:listof Prop?) boolean? . c:-> . (c:listof Prop?))
|
||||
(define tf-map (make-hash))
|
||||
(define ntf-map (make-hash))
|
||||
(define (restrict-update dict t1 p)
|
||||
(hash-update! dict p (λ (t2) (restrict t1 t2)) Univ))
|
||||
(define (intersect-update dict t1 p)
|
||||
(hash-update! dict p (λ (t2) (intersect t1 t2)) Univ))
|
||||
(define (union-update dict t1 p)
|
||||
(hash-update! dict p (λ (t2) (Un t1 t2)) -Bottom))
|
||||
|
||||
|
|
@ -109,9 +109,9 @@
|
|||
(for ([prop (in-list atomics)])
|
||||
(match prop
|
||||
[(TypeProp: o t1)
|
||||
((if or? union-update restrict-update) tf-map t1 o) ]
|
||||
((if or? union-update intersect-update) tf-map t1 o) ]
|
||||
[(NotTypeProp: o t1)
|
||||
((if or? restrict-update union-update) ntf-map t1 o) ]))
|
||||
((if or? intersect-update union-update) ntf-map t1 o) ]))
|
||||
(define raw-results
|
||||
(append others
|
||||
(for/list ([(k v) (in-hash tf-map)]) (-is-type k v))
|
||||
|
|
|
|||
|
|
@ -18,15 +18,15 @@
|
|||
(over-tests
|
||||
[-Number -Integer #t]))
|
||||
|
||||
(define-syntax (restr-tests stx)
|
||||
(define-syntax (inter-tests stx)
|
||||
(syntax-case stx ()
|
||||
[(_ [t1 t2 res] ...)
|
||||
#'(test-suite "Tests for restrict"
|
||||
(test-check (format "~a ~a" 't1 't2) type-compare? (restrict t1 t2) res) ...)]))
|
||||
#'(test-suite "Tests for intersect"
|
||||
(test-check (format "~a ~a" 't1 't2) type-compare? (intersect t1 t2) res) ...)]))
|
||||
|
||||
|
||||
(define restrict-tests
|
||||
(restr-tests
|
||||
(define intersect-tests
|
||||
(inter-tests
|
||||
[-Number (Un -Number -Symbol) -Number]
|
||||
[-Number -Number -Number]
|
||||
[(Un (-val 'foo) (-val 6)) (Un -Number -Symbol) (Un (-val 'foo) (-val 6))]
|
||||
|
|
@ -36,7 +36,7 @@
|
|||
[(Un -Number -String -Symbol -Boolean) -Number -Number]
|
||||
|
||||
[(-lst -Number) (-pair Univ Univ) (-pair -Number (-lst -Number))]
|
||||
[(-lst -Number) (-poly (a) (-lst a)) (-lst -Number)]
|
||||
[(-lst -Number) (-poly (a) (-lst a)) (-poly (a) (-lst a))]
|
||||
;; FIXME
|
||||
#;
|
||||
[-Listof -Sexp (-lst (Un B N -String Sym))]
|
||||
|
|
@ -76,5 +76,5 @@
|
|||
(define tests
|
||||
(test-suite "Remove Intersect"
|
||||
remove-tests
|
||||
restrict-tests
|
||||
intersect-tests
|
||||
overlap-tests))
|
||||
|
|
|
|||
|
|
@ -711,7 +711,7 @@
|
|||
[tc-e ((inst add-between Positive-Byte Symbol) '(1 2 3) 'a #:splice? #t #:before-first '(b))
|
||||
(-lst (t:Un -PosByte -Symbol))]
|
||||
|
||||
[tc-e (apply (plambda: (a) [x : a *] x) '(5)) (unfold (-lst -PosByte))]
|
||||
[tc-e (apply (plambda: (a) [x : a *] x) '(5)) (-lst -PosByte)]
|
||||
[tc-e (apply append (list '(1 2 3) '(4 5 6))) (-pair -PosByte (-lst -PosByte))]
|
||||
|
||||
[tc-err ((case-lambda: [([x : Number]) x]
|
||||
|
|
@ -1934,10 +1934,10 @@
|
|||
#:ret (ret (t:Un -Symbol (make-Evt Univ))))
|
||||
(tc-err (let: ([a : (U (Evtof Any) String) always-evt])
|
||||
(if (channel-put-evt? a) a (string->symbol a)))
|
||||
#:ret (ret (t:Un -Symbol (make-Evt (-mu x (make-Evt x))))))
|
||||
#:ret (ret (t:Un -Symbol (-mu x (make-Evt x)))))
|
||||
(tc-err (let: ([a : (U (Evtof Any) String) always-evt])
|
||||
(if (semaphore-peek-evt? a) a (string->symbol a)))
|
||||
#:ret (ret (t:Un -Symbol (make-Evt (-mu x (make-Evt x))))))
|
||||
#:ret (ret (t:Un -Symbol (-mu x (make-Evt x)))))
|
||||
|
||||
;Semaphores
|
||||
(tc-e (make-semaphore) -Semaphore)
|
||||
|
|
@ -3730,7 +3730,7 @@
|
|||
[tc-e/t (lambda: ([x : One])
|
||||
(let ([f (lambda: [w : Any *] w)])
|
||||
(f x "hello" #\c)))
|
||||
(t:-> -One (unfold (-lst Univ)) : -true-propset)]
|
||||
(t:-> -One (-lst Univ) : -true-propset)]
|
||||
|
||||
[tc-e/t (lambda: ([x : One])
|
||||
(let ([f (plambda: (a ...) [w : a ... a] w)])
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user