From b2c66548da5c028e4370e0cfc0e4f40f08d0d75e Mon Sep 17 00:00:00 2001 From: Andrew Kent Date: Fri, 27 Jul 2018 13:15:55 -0400 Subject: [PATCH 1/7] more complete function application MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit i.e. when applying a case->, the result is the intersection of each applicable range. Here are some quickly gathered performance results from this change: Compile time ratio (old time / new time): schml-specify-rep: 0.99 (i.e. slower, 8.63s (σ 0.09) to 8.72s (σ 0.05)) schml-interp-casts-help: 1.01 (i.e. faster, 20.05s (σ 0.24) to 19.77s (σ 0.01)) parser: 0.95 (i.e. slower, 2.22s (σ 0.05) to 2.33s (σ 0.09)) old-metrics: 0.96 (i.e. slower, 2.68s (σ 0.04) to 2.78s (σ 0.09)) new-metrics: 0.98 (i.e. slower, 3.61s (σ 0.02) to 3.7s (σ 0.08)) math-flonum: 0.98 (i.e. slower, 3.76s (σ 0.02) to 3.83s (σ 0.08)) fsm: 0.94 (i.e. slower, 4.91s (σ 0.09) to 5.22s (σ 0.19)) forth: 0.97 (i.e. slower, 4.87s (σ 0.18) to 5.01s (σ 0.01)) dungeon: 0.95 (i.e. slower, 8.64s (σ 0.11) to 9.11s (σ 0.18)) bernoulli: 0.95 (i.e. slower, 3.95s (σ 0.04) to 4.16s (σ 0.09)) acquire: 0.96 (i.e. slower, 15.53s (σ 0.23) to 16.2s (σ 0.08)) And for the math library, compile time increased from 2m28.281s to 2m40.492s. Note that some primtives (i.e. like those which operate on the numeric tower) currently have quite verbose function types which can be greatly simplified after this change is adopted. --- .../base-env/base-env-numeric.rkt | 2 +- .../typed-racket/env/lexical-env.rkt | 2 +- .../typecheck/check-subforms-unit.rkt | 2 +- .../typed-racket/typecheck/tc-app-helper.rkt | 9 ++- .../typed-racket/typecheck/tc-funapp.rkt | 48 ++++++++++---- .../typed-racket/typecheck/tc-if.rkt | 2 +- .../typecheck/tc-metafunctions.rkt | 66 ++++++++++++++++--- .../typed-racket/typecheck/tc-send.rkt | 2 +- .../typed-racket/types/type-table.rkt | 4 +- .../unit-tests/metafunction-tests.rkt | 20 +++--- .../unit-tests/typecheck-tests.rkt | 4 +- 11 files changed, 117 insertions(+), 44 deletions(-) diff --git a/typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt b/typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt index 7422d9bc0..5d740b7eb 100644 --- a/typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt +++ b/typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt @@ -1498,7 +1498,7 @@ ;; no positive / negative cases, possible underflow (-NonNegReal . -> . -NonNegSingleFlonum) (-NonPosReal . -> . -NonPosSingleFlonum) - (-Real . -> . -SingleFlonumZero))] + (-Real . -> . -SingleFlonum))] [real->double-flonum (from-cases (map unop all-flonum-types) (-SingleFlonumPosZero . -> . -FlonumPosZero) diff --git a/typed-racket-lib/typed-racket/env/lexical-env.rkt b/typed-racket-lib/typed-racket/env/lexical-env.rkt index eb12f4f30..5beb01517 100644 --- a/typed-racket-lib/typed-racket/env/lexical-env.rkt +++ b/typed-racket-lib/typed-racket/env/lexical-env.rkt @@ -33,7 +33,7 @@ [lookup-obj-type/lexical ((Object?) (env? #:fail (or/c #f Type? (-> any/c (or/c Type? #f)))) . ->* . (or/c Type? #f))] - [lookup-alias/lexical ((identifier?) (env?) . ->* . (or/c Path? Empty?))]) + [lookup-alias/lexical ((identifier?) (env?) . ->* . OptObject?)]) ;; used at the top level (define (add-props-to-current-lexical! ps) diff --git a/typed-racket-lib/typed-racket/typecheck/check-subforms-unit.rkt b/typed-racket-lib/typed-racket/typecheck/check-subforms-unit.rkt index 2cb6cb6a2..d2b323667 100644 --- a/typed-racket-lib/typed-racket/typecheck/check-subforms-unit.rkt +++ b/typed-racket-lib/typed-racket/typecheck/check-subforms-unit.rkt @@ -136,7 +136,7 @@ [stx:exn-body^ (set! body-results (tc-expr/check #'stx expected))]) (define handler-results (get-handler-results)) - (merge-tc-results (cons body-results handler-results))) + (union-tc-results (cons body-results handler-results))) ;; typecheck the expansion of a with-handlers form ;; syntax -> void diff --git a/typed-racket-lib/typed-racket/typecheck/tc-app-helper.rkt b/typed-racket-lib/typed-racket/typecheck/tc-app-helper.rkt index 78f8b9d68..8d87f1569 100644 --- a/typed-racket-lib/typed-racket/typecheck/tc-app-helper.rkt +++ b/typed-racket-lib/typed-racket/typecheck/tc-app-helper.rkt @@ -15,11 +15,14 @@ (provide/cond-contract [tc/funapp1 ((syntax? stx-list? Arrow? (listof tc-results/c) (or/c #f tc-results/c)) - (#:check boolean?) + (#:check boolean? #:tooltip? boolean?) . ->* . full-tc-results/c)]) -(define (tc/funapp1 f-stx args-stx ftype0 arg-ress expected #:check [check? #t]) +(define (tc/funapp1 f-stx args-stx ftype0 arg-ress expected + #:check [check? #t] + #:tooltip? [tooltip? #t]) ;; update tooltip-table with inferred function type - (add-typeof-expr f-stx (ret (make-Fun (list ftype0)))) + (when tooltip? + (add-typeof-expr f-stx (ret (make-Fun (list ftype0))))) (match* (ftype0 arg-ress) ;; we check that all kw args are optional [((Arrow: dom rst (list (Keyword: _ _ #f) ...) rng) diff --git a/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt b/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt index 9d1d74f89..8bb129320 100644 --- a/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt +++ b/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt @@ -6,7 +6,7 @@ (utils tc-utils identifier) (env tvar-env lexical-env) (for-syntax syntax/parse racket/base) - (types utils subtype resolve abbrev + (types utils subtype resolve abbrev type-table substitute classes prop-ops) (typecheck tc-metafunctions tc-app-helper tc-subst tc-envops check-below) @@ -115,17 +115,14 @@ ;; check there are no RestDots #:when (not (for/or ([a (in-list arrows)]) (RestDots? (Arrow-rst a)))) - (cond - ;; find the first function where the argument types match - [(ormap (match-lambda - [(and a (Arrow: dom rst _ _)) - (and (subtypes/varargs argtys dom rst) a)]) - arrows) - => (λ (a) - ;; then typecheck here -- we call the separate function so that we get - ;; the appropriate props/objects - (tc/funapp1 f-stx args-stx a args-res expected #:check #f))] - [else + (define applicable-arrows + (filter (match-lambda + [(Arrow: dom rst _ _) + (subtypes/varargs argtys dom rst)]) + arrows)) + + (match applicable-arrows + [(list) ;; if nothing matched, error (match arrows [(list (Arrow: doms rsts _ rngs) ...) @@ -135,7 +132,30 @@ #:msg-thunk (lambda (dom) (string-append "No function domains matched in function application:\n" - dom)))])])] + dom)))])] + [(list a) (tc/funapp1 f-stx args-stx a args-res expected #:check #f)] + [_ + ;; call a separate function so that we get + ;; the appropriate props/objects + (define app-result + (intersect-tc-results + (for/list ([a (in-list applicable-arrows)]) + (tc/funapp1 f-stx args-stx a args-res expected + #:check #f + #:tooltip? #f)))) + (define applicable-domain + ;; gather and intersect applicable domains to report to user + ;; generally what class of inputs produces the resulting output + (for/fold ([domtys (build-list (length argtys) (λ (_) Univ))]) + ([a (in-list applicable-arrows)]) + (match a + [(Arrow: dom rst _ _) (for/list ([domty (in-list domtys)] + [idx (in-naturals)]) + (intersect domty (dom+rst-ref dom rst idx)))]))) + (add-typeof-expr + f-stx + (ret (make-Fun (list (-Arrow applicable-domain (tc-results->values app-result)))))) + app-result])] ;; any kind of dotted polymorphic function without mandatory keyword args [(PolyDots: (list fixed-vars ... dotted-var) (Fun: arrows)) @@ -308,7 +328,7 @@ ;; a union of functions can be applied if we can apply all of the elements [(Union: (? Bottom?) ts) #:when (for/and ([t (in-list ts)]) (subtype t top-func)) - (merge-tc-results + (union-tc-results (for/list ([fty (in-list ts)]) (tc/funapp f-stx args-stx fty args-res expected)))] ;; bottom or error type is a perfectly good fcn type diff --git a/typed-racket-lib/typed-racket/typecheck/tc-if.rkt b/typed-racket-lib/typed-racket/typecheck/tc-if.rkt index 057699b00..9dc9ddbe7 100644 --- a/typed-racket-lib/typed-racket/typecheck/tc-if.rkt +++ b/typed-racket-lib/typed-racket/typecheck/tc-if.rkt @@ -30,7 +30,7 @@ ;; if there was not any expected results, then merge the 'then' ;; and 'else' results so we propogate the correct info upwards [(or #f (tc-any-results: #f)) - (merge-tc-results (list thn-res els-res))] + (union-tc-results (list thn-res els-res))] ;; otherwise, the subcomponents have already been checked and ;; we just return the expected result 'fixed' to replace any ;; missing fields (i.e. #f props or objects) diff --git a/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt b/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt index 72f324132..22c0b6599 100644 --- a/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt +++ b/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt @@ -5,6 +5,7 @@ racket/match racket/list (except-in (types abbrev utils prop-ops) -> ->* one-of/c) + (only-in (infer infer) intersect) (rep type-rep prop-rep object-rep values-rep rep-utils) (typecheck tc-subst) (logic ineq) @@ -12,7 +13,8 @@ (provide abstract-results combine-props - merge-tc-results + union-tc-results + intersect-tc-results tc-results->values erase-existentials) @@ -145,7 +147,7 @@ (-or p+ p-)]) tcrs))])) -(define (merge-tc-results results [ignore-propositions? #f]) +(define (union-tc-results results [ignore-propositions? #f]) (define/match (merge-tc-result r1 r2) [((tc-result: t1 (and ps1 (PropSet: p1+ p1-)) o1) (tc-result: t2 (PropSet: p2+ p2-) o2)) @@ -165,13 +167,13 @@ (make-RestDots (Un t1 t2) dbound)]) - (define/match (merge-two-results res1 res2) + (define/match (union-two-results res1 res2) [((tc-result1: (== -Bottom)) res2) res2] [(res1 (tc-result1: (== -Bottom))) res1] - [((tc-any-results: f1) res2) - (-tc-any-results (-or f1 (unconditional-prop res2)))] - [(res1 (tc-any-results: f2)) - (-tc-any-results (-or (unconditional-prop res1) f2))] + [((tc-any-results: p1) res2) + (-tc-any-results (-or p1 (unconditional-prop res2)))] + [(res1 (tc-any-results: p2)) + (-tc-any-results (-or (unconditional-prop res1) p2))] [((tc-results: results1 dty1) (tc-results: results2 dty2)) ;; if we have the same number of values in both cases @@ -188,7 +190,55 @@ (format "~a and ~a." (length results2) (length results1))))])]) (for/fold ([res (ret -Bottom)]) ([res2 (in-list results)]) - (merge-two-results res res2))) + (union-two-results res res2))) + +(define (intersect-tc-results results) + (define/match (merge-tc-result r1 r2) + [((tc-result: t1 (PropSet: p1+ p1-) o1) + (tc-result: t2 (PropSet: p2+ p2-) o2)) + (-tc-result (intersect t1 t2) + (-PS (-and p1+ p2+) (-and p1- p2-)) + (match* (o1 o2) + [(o o) o] + [((Empty:) _) o2] + [(_ (Empty:)) o1] + [(_ _) -empty-obj]))]) + + (define/match (same-dty? r1 r2) + [(#f #f) #t] + [((RestDots: t1 dbound) (RestDots: t2 dbound)) #t] + [(_ _) #f]) + (define/match (merge-dty r1 r2) + [(#f #f) #f] + [((RestDots: t1 dbound) (RestDots: t2 dbound)) + (make-RestDots (intersect t1 t2) dbound)]) + + + (define/match (intersect-two-results res1 res2) + [((tc-result1: (== -Bottom)) res2) (ret -Bottom)] + [(res1 (tc-result1: (== -Bottom))) (ret -Bottom)] + [((tc-any-results: p1) res2) (add-unconditional-prop res2 p1)] + [(res1 (tc-any-results: p2)) (add-unconditional-prop res1 p2)] + [((tc-results: results1 dty1) (tc-results: results2 dty2)) + ;; if we have the same number of values in both cases + (cond + [(and (= (length results1) (length results2)) + (same-dty? dty1 dty2)) + (-tc-results (map merge-tc-result results1 results2) + (merge-dty dty1 dty2))] + ;; otherwise, error + [else + (tc-error/expr "Expected the same number of values, but got ~a" + (if (< (length results1) (length results2)) + (format "~a and ~a." (length results1) (length results2)) + (format "~a and ~a." (length results2) (length results1))))])]) + + (match results + [(list r) r] + [(cons r rs) + (for/fold ([r-acc r]) + ([r (in-list rs)]) + (intersect-two-results r-acc r))])) (define (erase-existentials rep) diff --git a/typed-racket-lib/typed-racket/typecheck/tc-send.rkt b/typed-racket-lib/typed-racket/typecheck/tc-send.rkt index 12333de89..a0f1975aa 100644 --- a/typed-racket-lib/typed-racket/typecheck/tc-send.rkt +++ b/typed-racket-lib/typed-racket/typecheck/tc-send.rkt @@ -42,7 +42,7 @@ rcvr-type)])] ;; union of objects, check pointwise and union the results [(Union: (? Bottom?) objs) #:when (andmap Instance? objs) - (merge-tc-results (map do-check objs))] + (union-tc-results (map do-check objs))] [_ (tc-error/expr/fields "send: type mismatch" "expected" "an object" diff --git a/typed-racket-lib/typed-racket/types/type-table.rkt b/typed-racket-lib/typed-racket/types/type-table.rkt index ba354330f..565e9eeba 100644 --- a/typed-racket-lib/typed-racket/types/type-table.rkt +++ b/typed-racket-lib/typed-racket/types/type-table.rkt @@ -67,13 +67,13 @@ ;; the car should be the latest stx for the location (if (equal? e (car seen)) ;; combine types seen at the latest - (tooltip seen (merge-tc-results (list t results) #t)) + (tooltip seen (union-tc-results (list t results) #t)) old) (tooltip (cons e seen) t))])) #f)) (hash-update! type-table e (λ (prev) (cond - [prev (merge-tc-results (list t prev) #t)] + [prev (union-tc-results (list t prev) #t)] [else t])) #f)) diff --git a/typed-racket-test/unit-tests/metafunction-tests.rkt b/typed-racket-test/unit-tests/metafunction-tests.rkt index 4dde69dad..01a3c7c8d 100644 --- a/typed-racket-test/unit-tests/metafunction-tests.rkt +++ b/typed-racket-test/unit-tests/metafunction-tests.rkt @@ -75,33 +75,33 @@ #t) ) - (test-suite "merge-tc-results" + (test-suite "union-tc-results" (check-equal? - (merge-tc-results (list)) + (union-tc-results (list)) (ret -Bottom)) (check-equal? - (merge-tc-results (list (ret Univ))) + (union-tc-results (list (ret Univ))) (ret Univ)) (check-equal? - (merge-tc-results (list (ret Univ -tt-propset (make-Path null #'x)))) + (union-tc-results (list (ret Univ -tt-propset (make-Path null #'x)))) (ret Univ -tt-propset (make-Path null #'x))) (check-equal? - (merge-tc-results (list (ret -Bottom) (ret -Symbol -tt-propset (make-Path null #'x)))) + (union-tc-results (list (ret -Bottom) (ret -Symbol -tt-propset (make-Path null #'x)))) (ret -Symbol -tt-propset (make-Path null #'x))) (check-equal? - (merge-tc-results (list (ret -String) (ret -Symbol))) + (union-tc-results (list (ret -String) (ret -Symbol))) (ret (Un -Symbol -String))) (check-equal? - (merge-tc-results (list (ret -String -true-propset) (ret -Symbol -true-propset))) + (union-tc-results (list (ret -String -true-propset) (ret -Symbol -true-propset))) (ret (Un -Symbol -String) -true-propset)) (check-equal? - (merge-tc-results (list (ret (-val #f) -false-propset) (ret -Symbol -true-propset))) + (union-tc-results (list (ret (-val #f) -false-propset) (ret -Symbol -true-propset))) (ret (Un -Symbol (-val #f)) -tt-propset)) (check-equal? - (merge-tc-results (list (ret (list (-val 0) (-val 1))) (ret (list (-val 1) (-val 2))))) + (union-tc-results (list (ret (list (-val 0) (-val 1))) (ret (list (-val 1) (-val 2))))) (ret (list (Un (-val 0) (-val 1)) (Un (-val 1) (-val 2))))) (check-equal? - (merge-tc-results (list (ret null null null -Symbol 'x) (ret null null null -String 'x))) + (union-tc-results (list (ret null null null -Symbol 'x) (ret null null null -String 'x))) (ret null null null (Un -Symbol -String) 'x)) ) diff --git a/typed-racket-test/unit-tests/typecheck-tests.rkt b/typed-racket-test/unit-tests/typecheck-tests.rkt index 7cb49dd38..9fe4667f3 100644 --- a/typed-racket-test/unit-tests/typecheck-tests.rkt +++ b/typed-racket-test/unit-tests/typecheck-tests.rkt @@ -465,7 +465,7 @@ (tc-e (lcm (ann 3 Integer) 1/2) -NonNegRat) (tc-e (lcm (ann 3 Integer) -1/2) -NonNegRat) (tc-e (expt 0.5 0.3) -NonNegFlonum) - (tc-e (expt 0.5 2) (t:Un -NonNegFlonum -One)) + (tc-e (expt 0.5 2) -NonNegFlonum) (tc-e (expt 0.5 0) -One) (tc-e (expt -1/2 -1/2) -Number) (tc-e (expt (ann 0.5 Float) (ann 2 Natural)) -Real) @@ -535,7 +535,7 @@ (tc-e (/ (round (exact-round -2.7393196f0)) (real->double-flonum (inexact->exact (real->single-flonum -0.0)))) -Real) (tc-e (bitwise-and (exact-round 1.7976931348623157e+308) (exact-round -29)) -Int) (tc-e (flexpt -0.0 -1.0) -Flonum) - (tc-e (expt -0.0f0 -3.0) -Real) + (tc-e (expt -0.0f0 -3.0) -InexactReal) (tc-e (expt -8.665778974912815f+107 -677460115195106837726964554590085563061636191189747) -Number) (tc-e (expt (sin +inf.f) +nan.0+nan.0i) -Number) (tc-e (/ (gcd 1 0) -0.0f0 2.718281828459045) -Real) From 9c90969067a9cf2af06dcfc715b5b838d1f603ad Mon Sep 17 00:00:00 2001 From: Andrew Kent Date: Thu, 2 Aug 2018 11:46:36 -0400 Subject: [PATCH 2/7] simplify add1 type --- .../base-env/base-env-numeric.rkt | 22 ++++++------------- 1 file changed, 7 insertions(+), 15 deletions(-) diff --git a/typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt b/typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt index 5d740b7eb..33ed4b28e 100644 --- a/typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt +++ b/typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt @@ -1268,24 +1268,16 @@ [add1 (from-cases (-> -Zero -One) - (-> -One -PosByte) - (-> -Byte -PosIndex) - (-> -Index -PosFixnum) - (-> -NegFixnum -NonPosFixnum) + (-> -One -Byte) + (-> -Byte -Index) + (-> -Index -Fixnum) (-> -NonPosFixnum -Fixnum) - (-> -Nat -Pos) (-> -NegInt -NonPosInt) - (unop -Int) - (-> -NonNegRat -PosRat) - (unop -Rat) - (-> -NonNegFlonum -PosFlonum) - (unop -Flonum) - (-> -NonNegSingleFlonum -PosSingleFlonum) - (unop -SingleFlonum) - (-> -NonNegInexactReal -PosInexactReal) - (unop -InexactReal) (-> -NonNegReal -PosReal) - (map unop (list -Real -FloatComplex -SingleFlonumComplex -InexactComplex N)))] + (-> -InexactReal -InexactReal) + (map unop (list -Int -Rat -Flonum -SingleFlonum + -FloatComplex -SingleFlonumComplex + -Real -InexactReal -InexactComplex N)))] [sub1 (from-cases (-> -One -Zero) From 4859c465a8d00d4c6b4e697d37b039df4ce1ec4f Mon Sep 17 00:00:00 2001 From: Andrew Kent Date: Thu, 2 Aug 2018 11:51:18 -0400 Subject: [PATCH 3/7] simplify sub1 type --- .../typed-racket/base-env/base-env-numeric.rkt | 17 ++++------------- 1 file changed, 4 insertions(+), 13 deletions(-) diff --git a/typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt b/typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt index 33ed4b28e..5d591f758 100644 --- a/typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt +++ b/typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt @@ -1283,22 +1283,13 @@ (-> -One -Zero) (-> -PosByte -Byte) (-> -PosIndex -Index) - (-> -Index -Fixnum) - (-> -PosFixnum -NonNegFixnum) (-> -NonNegFixnum -Fixnum) (-> -Pos -Nat) - (-> -NonPosInt -NegInt) - (unop -Int) - (-> -NonPosRat -NegRat) - (unop -Rat) - (-> -NonPosFlonum -NegFlonum) - (unop -Flonum) - (-> -NonPosSingleFlonum -NegSingleFlonum) - (unop -SingleFlonum) - (-> -NonPosInexactReal -NegInexactReal) - (unop -InexactReal) (-> -NonPosReal -NegReal) - (map unop (list -Real -FloatComplex -SingleFlonumComplex -InexactComplex N)))] + (map unop (list -Int -Rat -Flonum -SingleFlonum + -Real -InexactReal -FloatComplex + -SingleFlonumComplex -InexactComplex + N)))] [quotient (from-cases From ccb69f2170aa8f369a0ac516d6741380f2b84ccb Mon Sep 17 00:00:00 2001 From: Andrew Kent Date: Thu, 2 Aug 2018 12:12:39 -0400 Subject: [PATCH 4/7] simplify abs type --- .../base-env/base-env-numeric.rkt | 20 ++++--------------- 1 file changed, 4 insertions(+), 16 deletions(-) diff --git a/typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt b/typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt index 5d591f758..877cbf48a 100644 --- a/typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt +++ b/typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt @@ -664,22 +664,10 @@ (define abs-cases ; used both for abs and magnitude (list ;; abs is not the identity on negative zeros. - ((Un -Zero -PosReal) . -> . (Un -Zero -PosReal) : -true-propset : (-arg-path 0)) - ;; but we know that we at least get *some* zero, and that it preserves exactness - (map unop (list -FlonumZero -SingleFlonumZero -RealZero)) - ;; abs may not be closed on fixnums. (abs min-fixnum) is not a fixnum - ((Un -PosInt -NegInt) . -> . -PosInt) - (-Int . -> . -Nat) - ((Un -PosRat -NegRat) . -> . -PosRat) - (-Rat . -> . -NonNegRat) - ((Un -PosFlonum -NegFlonum) . -> . -PosFlonum) - (-Flonum . -> . -NonNegFlonum) - ((Un -PosSingleFlonum -NegSingleFlonum) . -> . -PosSingleFlonum) - (-SingleFlonum . -> . -NonNegSingleFlonum) - ((Un -PosInexactReal -NegInexactReal) . -> . -PosInexactReal) - (-InexactReal . -> . -NonNegInexactReal) - ((Un -PosReal -NegReal) . -> . -PosReal) - (-Real . -> . -NonNegReal))) + (-> (Un -Zero -PosReal) (Un -Zero -PosReal) : -true-propset : (-arg-path 0)) + (map unop (list -RealZero -Int -Rat -Flonum -SingleFlonum)) + (-> (Un -PosReal -NegReal) -PosReal) + (-> -Real -NonNegReal))) ;Check to ensure we fail fast if the flonum bindings change (define-namespace-anchor anchor) From 6e0e97581830e464a4f899ccdd5f595142060978 Mon Sep 17 00:00:00 2001 From: Andrew Kent Date: Thu, 2 Aug 2018 12:59:18 -0400 Subject: [PATCH 5/7] simplify + type --- .../base-env/base-env-numeric.rkt | 83 +++++++------------ 1 file changed, 31 insertions(+), 52 deletions(-) diff --git a/typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt b/typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt index 877cbf48a..5700d9f27 100644 --- a/typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt +++ b/typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt @@ -1019,65 +1019,44 @@ (commutative-case -InexactComplex (Un -InexactComplex -InexactReal -PosRat -NegRat) -InexactComplex) (varop N))] [+ (from-cases - (-> -Zero) (-> N N : -true-propset : (-arg-path 0)) - (binop -Zero) (-> N -Zero N : -true-propset : (-arg-path 0)) (-> -Zero N N : -true-propset : (-arg-path 1)) - (-> -PosByte -PosByte -PosIndex) (-> -Byte -Byte -Index) - (-> -PosByte -PosByte -PosByte -PosIndex) (-> -Byte -Byte -Byte -Index) - (commutative-binop -PosIndex -Index -PosFixnum) - (-> -PosIndex -Index -Index -PosFixnum) - (-> -Index -PosIndex -Index -PosFixnum) - (-> -Index -Index -PosIndex -PosFixnum) (-> -Index -Index -NonNegFixnum) (-> -Index -Index -Index -NonNegFixnum) - (commutative-binop -NegFixnum -One -NonPosFixnum) - (commutative-binop -NonPosFixnum -NonNegFixnum -Fixnum) - (commutative-case -PosInt -Nat -PosInt) - (commutative-case -NegInt -NonPosInt -NegInt) - (map varop (list -Nat -NonPosInt -Int)) - (commutative-case -PosRat -NonNegRat -PosRat) - (commutative-case -NegRat -NonPosRat -NegRat) - (map varop (list -NonNegRat -NonPosRat -Rat)) - ;; flonum + real -> flonum - (commutative-case -PosFlonum -NonNegReal -PosFlonum) - (commutative-case -PosReal -NonNegFlonum -PosFlonum) - (commutative-case -NegFlonum -NonPosReal -NegFlonum) - (commutative-case -NegReal -NonPosFlonum -NegFlonum) - (commutative-case -NonNegFlonum -NonNegReal -NonNegFlonum) - (commutative-case -NonPosFlonum -NonPosReal -NonPosFlonum) - (commutative-case -Flonum -Real -Flonum) - (varop-1+ -Flonum) - ;; single-flonum + rat -> single-flonum - (commutative-case -PosSingleFlonum (Un -NonNegRat -NonNegSingleFlonum) -PosSingleFlonum) - (commutative-case (Un -PosRat -PosSingleFlonum) -NonNegSingleFlonum -PosSingleFlonum) - (commutative-case -NegSingleFlonum (Un -NonPosRat -NonPosSingleFlonum) -NegSingleFlonum) - (commutative-case (Un -NegRat -NegSingleFlonum) -NonPosSingleFlonum -NegSingleFlonum) - (commutative-case -NonNegSingleFlonum (Un -NonNegRat -NonNegSingleFlonum) -NonNegSingleFlonum) - (commutative-case -NonPosSingleFlonum (Un -NonPosRat -NonPosSingleFlonum) -NonPosSingleFlonum) - (commutative-case -SingleFlonum (Un -Rat -SingleFlonum) -SingleFlonum) - (varop-1+ -SingleFlonum) - ;; inexact-real + real -> inexact-real - (commutative-case -PosInexactReal -NonNegReal -PosInexactReal) - (commutative-case -PosReal -NonNegInexactReal -PosInexactReal) - (commutative-case -NegInexactReal -NonPosReal -NegInexactReal) - (commutative-case -NegReal -NonPosInexactReal -NegInexactReal) - (commutative-case -NonNegInexactReal -NonNegReal -NonNegInexactReal) - (commutative-case -NonPosInexactReal -NonPosReal -NonPosInexactReal) - (commutative-case -InexactReal -Real -InexactReal) - ;; real - (commutative-case -PosReal -NonNegReal -PosReal) - (commutative-case -NegReal -NonPosReal -NegReal) - (map varop (list -NonNegReal -NonPosReal -Real -ExactNumber)) - ;; complex - (commutative-case -FloatComplex N -FloatComplex) - (commutative-case -Flonum -InexactComplex -FloatComplex) - (commutative-case -SingleFlonumComplex (Un -Rat -SingleFlonum -SingleFlonumComplex) -SingleFlonumComplex) - (commutative-case -InexactComplex (Un -Rat -InexactReal -InexactComplex) -InexactComplex) - (varop N))] + (-> -NegFixnum -One -NonPosFixnum) + (-> -One -NegFixnum -NonPosFixnum) + (-> -NonPosFixnum -NonNegFixnum -Fixnum) + (-> -NonNegFixnum -NonPosFixnum -Fixnum) + (-> -Flonum -Real -Flonum) + (-> -Real -Flonum -Flonum) + (-> -SingleFlonum (Un -Rat -SingleFlonum) -SingleFlonum) + (-> (Un -Rat -SingleFlonum) -SingleFlonum -SingleFlonum) + (-> -InexactReal -Real -InexactReal) + (-> -Real -InexactReal -InexactReal) + (-> -FloatComplex N -FloatComplex) + (-> N -FloatComplex -FloatComplex) + (-> -Flonum -InexactComplex -FloatComplex) + (-> -InexactComplex -Flonum -FloatComplex) + (-> -SingleFlonumComplex (Un -Rat -SingleFlonum -SingleFlonumComplex) -SingleFlonumComplex) + (-> (Un -Rat -SingleFlonum -SingleFlonumComplex) -SingleFlonumComplex -SingleFlonumComplex) + (-> -InexactComplex (Un -Rat -InexactReal -InexactComplex) -InexactComplex) + (-> (Un -Rat -InexactReal -InexactComplex) -InexactComplex -InexactComplex) + (-> -PosReal -NonNegReal -PosReal) + (-> -NonNegReal -PosReal -PosReal) + (-> -PosReal -NonNegReal -NonNegReal -PosReal) + (-> -NonNegReal -PosReal -NonNegReal -PosReal) + (-> -NonNegReal -NonNegReal -PosReal -PosReal) + (-> -NegReal -NonPosReal -NegReal) + (-> -NonPosReal -NegReal -NegReal) + (-> -NegReal -NonPosReal -NonPosReal -NegReal) + (-> -NonPosReal -NegReal -NonPosReal -NegReal) + (-> -NonPosReal -NonPosReal -NegReal -NegReal) + (map varop (list -Zero -Nat -Int -PosReal -NegReal + -NonNegReal -NonPosReal -Real -ExactNumber N)) + (map varop-1+ (list -Flonum -SingleFlonum)))] [- (from-cases (binop -Zero) From b17ef076e4f37d764133b89cfd263d03540c3544 Mon Sep 17 00:00:00 2001 From: Andrew Kent Date: Wed, 15 Aug 2018 21:27:40 -0400 Subject: [PATCH 6/7] improve subtyping --- .../typed-racket/rep/object-rep.rkt | 11 ++- .../typed-racket/types/subtype.rkt | 89 ++++++++++++++++--- 2 files changed, 88 insertions(+), 12 deletions(-) diff --git a/typed-racket-lib/typed-racket/rep/object-rep.rkt b/typed-racket-lib/typed-racket/rep/object-rep.rkt index ff6ebf243..516967f65 100644 --- a/typed-racket-lib/typed-racket/rep/object-rep.rkt +++ b/typed-racket-lib/typed-racket/rep/object-rep.rkt @@ -37,6 +37,7 @@ obj-seq-next scale-obj uninterpreted-PE? + intersect-objects (rename-out [make-LExp* make-LExp] [make-LExp raw-make-LExp]) (all-from-out "fme-utils.rkt")) @@ -395,4 +396,12 @@ (define (add-path-to-lexp p l) (match l [(LExp: const terms) - (make-LExp* const (terms-set terms p (add1 (terms-ref terms p))))])) \ No newline at end of file + (make-LExp* const (terms-set terms p (add1 (terms-ref terms p))))])) + + +(define (intersect-objects o1 o2) + (match* (o1 o2) + [(o o) o] + [((Empty:) _) o2] + [(_ (Empty:)) o1] + [(_ _) o1])) \ No newline at end of file diff --git a/typed-racket-lib/typed-racket/types/subtype.rkt b/typed-racket-lib/typed-racket/types/subtype.rkt index 09834e3b0..8036312a8 100644 --- a/typed-racket-lib/typed-racket/types/subtype.rkt +++ b/typed-racket-lib/typed-racket/types/subtype.rkt @@ -21,7 +21,7 @@ one-of/c)) (lazy-require - ("../infer/infer.rkt" (infer)) + ("../infer/infer.rkt" (infer intersect)) ("prop-ops.rkt" (-and)) ("../typecheck/tc-subst.rkt" (instantiate-obj+simplify)) ("../typecheck/tc-envops.rkt" (env+ implies-in-env?))) @@ -186,7 +186,7 @@ ;; NOTE: This function takes into account that domains are ;; contravariant w.r.t. subtyping, i.e. callers should NOT ;; flip argument order. -(define/cond-contract (Arrow-domain-subtypes* A dom1 rst1 dom2 rst2 [objs #f]) +(define/cond-contract (positional-domain-subtypes* A dom1 rst1 dom2 rst2 [objs #f]) (->* (list? (listof Type?) (or/c #f Rest? RestDots?) @@ -198,12 +198,26 @@ [((cons t1 ts1) (cons t2 ts2)) (subtype-seq A (subtype* t2 t1 (and objs (car objs))) - (Arrow-domain-subtypes* ts1 rst1 ts2 rst2 (and objs (cdr objs))))] + (positional-domain-subtypes* ts1 rst1 ts2 rst2 (and objs (cdr objs))))] [(_ _) (subtype* A (-Tuple* dom2 (Rest->Type rst2)) (-Tuple* dom1 (Rest->Type rst1)))])) +(define/cond-contract (Arrow-domain-subtypes* A dom1 rst1 kws1 dom2 rst2 kws2 [objs #f]) + (->* (list? + (listof Type?) + (or/c #f Rest? RestDots?) + (listof Keyword?) + (listof Type?) + (or/c #f Rest? RestDots?) + (listof Keyword?)) + ((listof Object?)) + (or/c #f list?)) + (subtype-seq A + (positional-domain-subtypes* dom1 rst1 dom2 rst2 objs) + (kw-subtypes* kws1 kws2))) + (define-syntax-rule (with-fresh-ids len ids . body) (let-values ([(ids seq) (for/fold ([ids '()] [seq (temp-ids)]) @@ -220,7 +234,7 @@ [((Arrow: dom1 rst1 kws1 raw-rng1) (Arrow: dom2 rst2 kws2 raw-rng2)) (define A* (subtype-seq A - (Arrow-domain-subtypes* dom1 rst1 dom2 rst2) + (positional-domain-subtypes* dom1 rst1 dom2 rst2) (kw-subtypes* kws1 kws2))) (cond [(not A*) #f] @@ -254,7 +268,7 @@ (instantiate-obj d ids))) (define A* (subtype-seq A (kw-subtypes* kws1 '()) - (Arrow-domain-subtypes* dom1 rst1 dom2 #f (map -id-path ids)))) + (positional-domain-subtypes* dom1 rst1 dom2 #f (map -id-path ids)))) (cond [(not A*) #f] [else @@ -310,7 +324,7 @@ (define rst (match raw-rst [(? Type?) (make-Rest (list raw-rst))] [_ raw-rst])) - (Arrow-domain-subtypes* A dom rst argtys #f)) + (positional-domain-subtypes* A dom rst argtys #f)) ;;************************************************************ @@ -812,11 +826,35 @@ [((Fun: arrows2) _) (cond [(null? arrows1) #f] - [else (for/fold ([A A]) - ([a2 (in-list arrows2)] - #:break (not A)) - (for/or ([a1 (in-list arrows1)]) - (arrow-subtype* A a1 a2)))])] + [else + (for/fold ([A A]) + ([a2 (in-list arrows2)] + #:break (not A)) + (match-define (Arrow: dom2 rst2 kws2 raw-cdom2) a2) + ;; A <: C₁ ∩ ... ∩ Cₙ + ;; D₁ ∩ ... ∩ Dₙ <: B + ;; ------------------------ + ;; (C₁→D₁∩...∩Cₙ→Dₙ) <: A→B + (define raw-cdom1 + (for/fold ([cdom #f]) + ([a1 (in-list arrows1)]) + (match-define (Arrow: dom1 rst1 kws1 raw-cdom1) a1) + (cond + [(Arrow-domain-subtypes* A dom1 rst1 kws1 dom2 rst2 kws2) + (if cdom (intersect-values cdom raw-cdom1) raw-cdom1)] + [else cdom]))) + (cond + [(not raw-cdom1) #f] + [else + (with-fresh-ids (length dom2) ids + (define mapping + (for/list ([idx (in-naturals)] + [id (in-list ids)] + [t (in-list dom2)]) + (list* idx id t))) + (subval* A + (instantiate-obj+simplify raw-cdom1 mapping) + (instantiate-obj raw-cdom2 ids)))]))])] [((? DepFun? dfun) _) (for/or ([a1 (in-list arrows1)]) (arrow-subtype-dfun* A a1 dfun))] @@ -1229,3 +1267,32 @@ #false] [_ (continue<: A t1 t2 obj)])] [else: (continue<: A t1 t2 obj)]) + + +;; intersects two monomorphic Values (i.e. see rep/values-rep) +;; if the values are strictly incompatible, we return ⊥, +(define (intersect-values v1 v2) + (match* (v1 v2) + [(v v) v] + [((ValuesDots: rs1 dty1 dbound) + (ValuesDots: rs2 dty2 dbound)) + (make-ValuesDots (map intersect-results rs1 rs2) (intersect dty1 dty2) dbound)] + [((? ValuesDots?) _) v1] + [(_ (? ValuesDots?)) v2] + [((AnyValues: p1) (AnyValues: p2)) (make-AnyValues (-and p1 p2))] + [((AnyValues: p) (Values: (cons (Result: t (PropSet: p+ p-) o) rst))) + (make-Values (cons (make-Result t (-PS (-and p p+) (-and p p-)) o) rst))] + [((Values: (cons (Result: t (PropSet: p+ p-) o) rst)) (AnyValues: p)) + (make-Values (cons (make-Result t (-PS (-and p p+) (-and p p-)) o) rst))] + [((Values: rs1) (Values: rs2)) + (cond + [(= (length rs1) (length rs2)) + (make-Values (map intersect-results rs1 rs2))] + [else (make-AnyValues -ff)])])) + +;; intersects two Results (i.e. see rep/core-rep.rkt) pointwise +(define (intersect-results r1 r2) + (match* (r1 r2) + [((Result: t1 (PropSet: p1+ p1-) o1) + (Result: t2 (PropSet: p2+ p2-) o2)) + (make-Result (intersect t1 t2) (-PS (-and p1+ p2+) (-and p1- p2-)) (intersect-objects o1 o2))])) From 3691f966796c235aacdd801cf44a83fd86e9abeb Mon Sep 17 00:00:00 2001 From: Andrew Kent Date: Thu, 16 Aug 2018 17:03:51 -0400 Subject: [PATCH 7/7] initial, really slow inference --- .../typed-racket/infer/infer-unit.rkt | 49 +++++-- .../typed-racket/infer/intersect.rkt | 3 + .../typed-racket/types/subtype.rkt | 121 ++++++++++-------- typed-racket-lib/typed-racket/types/utils.rkt | 1 + 4 files changed, 115 insertions(+), 59 deletions(-) diff --git a/typed-racket-lib/typed-racket/infer/infer-unit.rkt b/typed-racket-lib/typed-racket/infer/infer-unit.rkt index 4f6fbd7b4..9fb28e8c9 100644 --- a/typed-racket-lib/typed-racket/infer/infer-unit.rkt +++ b/typed-racket-lib/typed-racket/infer/infer-unit.rkt @@ -420,6 +420,19 @@ (cgen context s t) (cgen/seq context t-seq s-seq)))])) +(define/cond-contract (cgen/arrow-pair/arrow context s-arr-pair t-arr) + (context? (cons/c Type? Values?) Arrow? . -> . (or/c #f cset?)) + (match* (s-arr-pair t-arr) + [((cons dom1 cdom1) + (Arrow: dom2 rst2 kws2 cdom2)) + (and + (null? kws2) + (% cset-meet + (cgen context cdom1 cdom2) + (cgen context + (positional-domain->Tuple dom2 rst2) + dom1)))])) + (define/cond-contract (cgen/flds context flds-s flds-t) (context? (listof fld?) (listof fld?) . -> . (or/c #f cset?)) (% cset-meet* @@ -812,17 +825,35 @@ (% cset-meet (cg in2 in1) (cg out1 out2))] [((Fun: s-arr) (Fun: t-arr)) + (define s-arrow-combinations + (let loop ([arrows s-arr] + [acc #f]) + (match arrows + ['() (if acc (list acc) '())] + [(cons a rst) + (define a* (if acc + (intersect-arrows a acc) + (match a + [(Arrow: dom rst kws cdom) + (and (for/and ([kw (in-list kws)]) + (not (Keyword-required? kw))) + (cons (positional-domain->Tuple dom rst) + cdom))]))) + (if a* + (append (loop rst a*) + (loop rst acc)) + (loop rst acc))]))) (% cset-meet* (for/list/fail - ([t-arr (in-list t-arr)]) - ;; for each element of t-arr, we need to get at least one element of s-arr that works - (let ([results (for*/list ([s-arr (in-list s-arr)] - [v (in-value (cgen/arrow context s-arr t-arr))] - #:when v) - v)]) - ;; ensure that something produces a constraint set - (and (not (null? results)) - (cset-join results)))))] + ([t-arr (in-list t-arr)]) + ;; for each element of t-arr, we need to get at least one element of s-arr that works + (let ([results (for*/list ([s-arr-pair (in-list s-arrow-combinations)] + [v (in-value (cgen/arrow-pair/arrow context s-arr-pair t-arr))] + #:when v) + v)]) + ;; ensure that something produces a constraint set + (and (not (null? results)) + (cset-join results)))))] [(_ _) ;; nothing worked, and we fail #f]))])) diff --git a/typed-racket-lib/typed-racket/infer/intersect.rkt b/typed-racket-lib/typed-racket/infer/intersect.rkt index 7ca62ea81..64f2d3d68 100644 --- a/typed-racket-lib/typed-racket/infer/intersect.rkt +++ b/typed-racket-lib/typed-racket/infer/intersect.rkt @@ -236,3 +236,6 @@ [else (internal-restrict t1 t2 '() obj)])) (define internal-restrict (intersect-types #f)) + + + diff --git a/typed-racket-lib/typed-racket/types/subtype.rkt b/typed-racket-lib/typed-racket/types/subtype.rkt index 8036312a8..6527d7b41 100644 --- a/typed-racket-lib/typed-racket/types/subtype.rkt +++ b/typed-racket-lib/typed-racket/types/subtype.rkt @@ -27,7 +27,7 @@ ("../typecheck/tc-envops.rkt" (env+ implies-in-env?))) -(provide NameStruct:) +(provide NameStruct: positional-domain->Tuple) (provide/cond-contract [subtype (->* (Type? Type?) ((or/c #f OptObject?)) boolean?)] @@ -39,7 +39,8 @@ (listof Type?) (or/c Type? Rest? #f) boolean?)] - [unrelated-structs (-> Struct? Struct? boolean?)]) + [unrelated-structs (-> Struct? Struct? boolean?)] + [intersect-arrows (-> Arrow? Arrow? (or/c #f (cons/c Type? Values?)))]) ;; When subtype is called w/ no object, we @@ -227,27 +228,33 @@ (parameterize ([temp-ids seq]) . body))) -;; simple co/contra-variance for -> -(define/cond-contract (arrow-subtype* A arr1 arr2) - (-> list? Arrow? Arrow? (or/c #f list?)) - (match* (arr1 arr2) - [((Arrow: dom1 rst1 kws1 raw-rng1) - (Arrow: dom2 rst2 kws2 raw-rng2)) - (define A* (subtype-seq A - (positional-domain-subtypes* dom1 rst1 dom2 rst2) - (kw-subtypes* kws1 kws2))) - (cond - [(not A*) #f] - [else - (with-fresh-ids (length dom2) ids - (define mapping - (for/list ([idx (in-naturals)] - [id (in-list ids)] - [t (in-list dom2)]) - (list* idx id t))) - (subval* A* - (instantiate-obj+simplify raw-rng1 mapping) - (instantiate-obj raw-rng2 ids)))])])) +;; A <: C₁ ∩ ... ∩ Cₙ +;; D₁ ∩ ... ∩ Dₙ <: B +;; ------------------------ +;; (C₁→D₁∩...∩Cₙ→Dₙ) <: A→B +(define/cond-contract (arrows/arrow-subtype* A arrows1 arrow2) + (-> list? (listof Arrow?) Arrow? (or/c #f list?)) + (match-define (Arrow: dom2 rst2 kws2 raw-cdom2) arrow2) + (define raw-cdom1 + (for/fold ([cdom #f]) + ([a1 (in-list arrows1)]) + (match-define (Arrow: dom1 rst1 kws1 raw-cdom1) a1) + (cond + [(Arrow-domain-subtypes* A dom1 rst1 kws1 dom2 rst2 kws2) + (if cdom (intersect-values cdom raw-cdom1) raw-cdom1)] + [else cdom]))) + (cond + [(not raw-cdom1) #f] + [else + (with-fresh-ids (length dom2) ids + (define mapping + (for/list ([idx (in-naturals)] + [id (in-list ids)] + [t (in-list dom2)]) + (list* idx id t))) + (subval* A + (instantiate-obj+simplify raw-cdom1 mapping) + (instantiate-obj raw-cdom2 ids)))])) ;; is an Arrow a subtype of a DepFun? @@ -819,7 +826,7 @@ (match* (t2 arrows1) ;; special case when t1 can be collapsed into simpler arrow [((Fun: (list arrow2)) (app collapsable-arrows? (? Arrow? arrow1))) - (arrow-subtype* A arrow1 arrow2)] + (arrows/arrow-subtype* A (list arrow1) arrow2)] ;; special case when t1 can be collapsed into simpler arrow [((? DepFun? dfun) (app collapsable-arrows? (? Arrow? arrow1))) (arrow-subtype-dfun* A arrow1 dfun)] @@ -830,31 +837,7 @@ (for/fold ([A A]) ([a2 (in-list arrows2)] #:break (not A)) - (match-define (Arrow: dom2 rst2 kws2 raw-cdom2) a2) - ;; A <: C₁ ∩ ... ∩ Cₙ - ;; D₁ ∩ ... ∩ Dₙ <: B - ;; ------------------------ - ;; (C₁→D₁∩...∩Cₙ→Dₙ) <: A→B - (define raw-cdom1 - (for/fold ([cdom #f]) - ([a1 (in-list arrows1)]) - (match-define (Arrow: dom1 rst1 kws1 raw-cdom1) a1) - (cond - [(Arrow-domain-subtypes* A dom1 rst1 kws1 dom2 rst2 kws2) - (if cdom (intersect-values cdom raw-cdom1) raw-cdom1)] - [else cdom]))) - (cond - [(not raw-cdom1) #f] - [else - (with-fresh-ids (length dom2) ids - (define mapping - (for/list ([idx (in-naturals)] - [id (in-list ids)] - [t (in-list dom2)]) - (list* idx id t))) - (subval* A - (instantiate-obj+simplify raw-cdom1 mapping) - (instantiate-obj raw-cdom2 ids)))]))])] + (arrows/arrow-subtype* A arrows1 a2))])] [((? DepFun? dfun) _) (for/or ([a1 (in-list arrows1)]) (arrow-subtype-dfun* A a1 dfun))] @@ -1288,7 +1271,7 @@ (cond [(= (length rs1) (length rs2)) (make-Values (map intersect-results rs1 rs2))] - [else (make-AnyValues -ff)])])) + [else (-values -Bottom (-PS -ff -ff) -empty-obj)])])) ;; intersects two Results (i.e. see rep/core-rep.rkt) pointwise (define (intersect-results r1 r2) @@ -1296,3 +1279,41 @@ [((Result: t1 (PropSet: p1+ p1-) o1) (Result: t2 (PropSet: p2+ p2-) o2)) (make-Result (intersect t1 t2) (-PS (-and p1+ p2+) (-and p1- p2-)) (intersect-objects o1 o2))])) + + +(define (positional-domain->Tuple dom rst) + (-Tuple* dom (or (and rst (Rest->Type rst)) + -Null))) + +(define (intersect-arrows arrow1 arrow2) + (match* (arrow1 arrow2) + [((cons dom1 cdom1) (cons dom2 cdom2)) + (define dom (intersect dom1 dom2)) + (cond + [(Bottom? dom) #f] + [else (cons dom (intersect-values cdom1 cdom2))])] + [((Arrow: dom1 rst1 kws1 cdom1) + (Arrow: dom2 rst2 kws2 cdom2)) + #:when (and (andmap (λ (kw) (not (Keyword-required? kw))) kws1) + (andmap (λ (kw) (not (Keyword-required? kw))) kws2)) + (define dom (intersect (positional-domain->Tuple dom1 rst1) + (positional-domain->Tuple dom2 rst2))) + (cond + [(Bottom? dom) #f] + [else (cons dom (intersect-values cdom1 cdom2))])] + [((cons dom1 cdom1) + (Arrow: dom2 rst2 kws2 cdom2)) + #:when (andmap (λ (kw) (not (Keyword-required? kw))) kws2) + (define dom (intersect dom1 (positional-domain->Tuple dom2 rst2))) + (cond + [(Bottom? dom) #f] + [else (cons dom (intersect-values cdom1 cdom2))])] + [((Arrow: dom1 rst1 kws1 cdom1) + (cons dom2 cdom2)) + #:when (andmap (λ (kw) (not (Keyword-required? kw))) kws1) + (define dom (intersect (positional-domain->Tuple dom1 rst1) + dom2)) + (cond + [(Bottom? dom) #f] + [else (cons dom (intersect-values cdom1 cdom2))])] + [(_ _) #f])) diff --git a/typed-racket-lib/typed-racket/types/utils.rkt b/typed-racket-lib/typed-racket/types/utils.rkt index 139f3ac77..acd2508d4 100644 --- a/typed-racket-lib/typed-racket/types/utils.rkt +++ b/typed-racket-lib/typed-racket/types/utils.rkt @@ -34,6 +34,7 @@ [(Rest: rst-ts) (list-ref rst-ts (remainder idx (length rst-ts)))] [_ (if (procedure? default) (default) default)])])) + (define (Rest->Type r) (match r [#f -Null]