diff --git a/typed-racket-lib/typed-racket/infer/constraints.rkt b/typed-racket-lib/typed-racket/infer/constraints.rkt index 7be1ecf7..4ac4ac25 100644 --- a/typed-racket-lib/typed-racket/infer/constraints.rkt +++ b/typed-racket-lib/typed-racket/infer/constraints.rkt @@ -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* diff --git a/typed-racket-lib/typed-racket/infer/infer.rkt b/typed-racket-lib/typed-racket/infer/infer.rkt index d497745c..806c4d9b 100644 --- a/typed-racket-lib/typed-racket/infer/infer.rkt +++ b/typed-racket-lib/typed-racket/infer/infer.rkt @@ -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@)) diff --git a/typed-racket-lib/typed-racket/infer/intersect.rkt b/typed-racket-lib/typed-racket/infer/intersect.rkt new file mode 100644 index 00000000..4c755651 --- /dev/null +++ b/typed-racket-lib/typed-racket/infer/intersect.rkt @@ -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))) diff --git a/typed-racket-lib/typed-racket/infer/restrict.rkt b/typed-racket-lib/typed-racket/infer/restrict.rkt deleted file mode 100644 index c3e62452..00000000 --- a/typed-racket-lib/typed-racket/infer/restrict.rkt +++ /dev/null @@ -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))) diff --git a/typed-racket-lib/typed-racket/infer/signatures.rkt b/typed-racket-lib/typed-racket/infer/signatures.rkt index 19bd935f..47899503 100644 --- a/typed-racket-lib/typed-racket/infer/signatures.rkt +++ b/typed-racket-lib/typed-racket/infer/signatures.rkt @@ -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 diff --git a/typed-racket-lib/typed-racket/private/parse-type.rkt b/typed-racket-lib/typed-racket/private/parse-type.rkt index cef67ae4..22fd0500 100644 --- a/typed-racket-lib/typed-racket/private/parse-type.rkt +++ b/typed-racket-lib/typed-racket/private/parse-type.rkt @@ -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) diff --git a/typed-racket-lib/typed-racket/rep/type-rep.rkt b/typed-racket-lib/typed-racket/rep/type-rep.rkt index 0b79e2e8..880b063d 100644 --- a/typed-racket-lib/typed-racket/rep/type-rep.rkt +++ b/typed-racket-lib/typed-racket/rep/type-rep.rkt @@ -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)] diff --git a/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt b/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt index f7faf3d8..8f145a4e 100644 --- a/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt +++ b/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt @@ -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))] diff --git a/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt b/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt index b4ad0099..0ba725f5 100644 --- a/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt +++ b/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt @@ -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)))) diff --git a/typed-racket-lib/typed-racket/typecheck/tc-literal.rkt b/typed-racket-lib/typed-racket/typecheck/tc-literal.rkt index ae992a71..30648fbc 100644 --- a/typed-racket-lib/typed-racket/typecheck/tc-literal.rkt +++ b/typed-racket-lib/typed-racket/typecheck/tc-literal.rkt @@ -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)))] diff --git a/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt b/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt index 8c4a9085..029bff92 100644 --- a/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt +++ b/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt @@ -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 diff --git a/typed-racket-lib/typed-racket/types/prop-ops.rkt b/typed-racket-lib/typed-racket/types/prop-ops.rkt index f70b58a2..aa3ee306 100644 --- a/typed-racket-lib/typed-racket/types/prop-ops.rkt +++ b/typed-racket-lib/typed-racket/types/prop-ops.rkt @@ -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)) diff --git a/typed-racket-test/unit-tests/remove-intersect-tests.rkt b/typed-racket-test/unit-tests/remove-intersect-tests.rkt index 468075d7..3e0a4ed5 100644 --- a/typed-racket-test/unit-tests/remove-intersect-tests.rkt +++ b/typed-racket-test/unit-tests/remove-intersect-tests.rkt @@ -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)) diff --git a/typed-racket-test/unit-tests/typecheck-tests.rkt b/typed-racket-test/unit-tests/typecheck-tests.rkt index 569bde14..299be712 100644 --- a/typed-racket-test/unit-tests/typecheck-tests.rkt +++ b/typed-racket-test/unit-tests/typecheck-tests.rkt @@ -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)])