From 80a9027f1eee6ea56a29aa73c65675f6cf86cdb2 Mon Sep 17 00:00:00 2001 From: Vincent St-Amour Date: Tue, 1 Mar 2011 13:49:31 -0500 Subject: [PATCH] Take the meet of constraints earlier in the inference process. This avoids constraint explosions in some cases, notably when working with polydots and plain variable arity functions at the same time. However, this also weakens inference a bit (breaks it for unholy-terror and related tests), but not in a way that affects any practical use cases that I know of. --- .../tests/typed-scheme/fail/values-dots.rkt | 2 +- .../typed-scheme/succeed/ann-map-funcs.rkt | 11 ------ .../typed-scheme/xfail/ann-map-funcs.rkt | 21 +++++++++++ .../{succeed => xfail}/unholy-terror.rkt | 3 ++ collects/typed-scheme/infer/infer-unit.rkt | 37 +++++++++++++------ 5 files changed, 50 insertions(+), 24 deletions(-) delete mode 100644 collects/tests/typed-scheme/succeed/ann-map-funcs.rkt create mode 100644 collects/tests/typed-scheme/xfail/ann-map-funcs.rkt rename collects/tests/typed-scheme/{succeed => xfail}/unholy-terror.rkt (94%) diff --git a/collects/tests/typed-scheme/fail/values-dots.rkt b/collects/tests/typed-scheme/fail/values-dots.rkt index f92743faf3..d12b885d26 100644 --- a/collects/tests/typed-scheme/fail/values-dots.rkt +++ b/collects/tests/typed-scheme/fail/values-dots.rkt @@ -1,5 +1,5 @@ #; -(exn-pred 7) +(exn-pred 10) #lang typed-scheme (require typed-scheme/private/extra-procs) diff --git a/collects/tests/typed-scheme/succeed/ann-map-funcs.rkt b/collects/tests/typed-scheme/succeed/ann-map-funcs.rkt deleted file mode 100644 index b46f167666..0000000000 --- a/collects/tests/typed-scheme/succeed/ann-map-funcs.rkt +++ /dev/null @@ -1,11 +0,0 @@ -#lang typed/racket - -(: map-with-funcs (All (b a ...) ((a ... a -> b) * -> (a ... a -> (Listof b))))) - -(define (map-with-funcs . fs) - (lambda as - (map (lambda: ([f : (a ... a -> b)]) - (apply f as)) - fs))) - -(ann (map-with-funcs + - * /) (Number Number * -> (Listof Number))) diff --git a/collects/tests/typed-scheme/xfail/ann-map-funcs.rkt b/collects/tests/typed-scheme/xfail/ann-map-funcs.rkt new file mode 100644 index 0000000000..5a87b8cf91 --- /dev/null +++ b/collects/tests/typed-scheme/xfail/ann-map-funcs.rkt @@ -0,0 +1,21 @@ +#lang typed/racket + +;; This test is similar to unholy-terror. +;; Recent changes to the numeric tower makes this generate a ridiculous amount +;; of inference contraints. +;; Changes to the inference engine breaks inference on this test, but unlike +;; unholy terror, this one fails quite fast, so it's not as bad. +;; Reverting these changes would make inference work again, given enough time +;; and memory (on the order of hours, and gigabytes of memory). +;; For future reference, ~600k inference constraints were generated (due to a +;; repeated cross product) before I killed it. + +(: map-with-funcs (All (b a ...) ((a ... a -> b) * -> (a ... a -> (Listof b))))) + +(define (map-with-funcs . fs) + (lambda as + (map (lambda: ([f : (a ... a -> b)]) + (apply f as)) + fs))) + +(ann (map-with-funcs + - * /) (Number Number * -> (Listof Number))) diff --git a/collects/tests/typed-scheme/succeed/unholy-terror.rkt b/collects/tests/typed-scheme/xfail/unholy-terror.rkt similarity index 94% rename from collects/tests/typed-scheme/succeed/unholy-terror.rkt rename to collects/tests/typed-scheme/xfail/unholy-terror.rkt index 7fbf8c7961..2166707a68 100644 --- a/collects/tests/typed-scheme/succeed/unholy-terror.rkt +++ b/collects/tests/typed-scheme/xfail/unholy-terror.rkt @@ -1,5 +1,8 @@ #lang typed-scheme +;; Changes to the numeric tower cause this test to generate a ridiculous +;; number of inference constraints. Inference takes 5+ minutes. + (apply (plambda: (a ...) [ys : (a ... a -> Number) *] (lambda: [zs : a ... a] (map (lambda: ([y : (a ... a -> Number)]) diff --git a/collects/typed-scheme/infer/infer-unit.rkt b/collects/typed-scheme/infer/infer-unit.rkt index 6d13c89293..9ea79cec6a 100644 --- a/collects/typed-scheme/infer/infer-unit.rkt +++ b/collects/typed-scheme/infer/infer-unit.rkt @@ -640,12 +640,21 @@ ;; Y : the set of index variables to be constrained ;; S : a list of types to be the subtypes of T ;; T : a list of types +;; expected-cset : a cset representing the expected type, to meet early and +;; keep the number of constraints in check. (empty by default) ;; produces a cset which determines a substitution that makes the Ss subtypes of the Ts -(d/c (cgen/list V X Y S T) - ((listof symbol?) (listof symbol?) (listof symbol?) (listof Type?) (listof Type?) . -> . cset?) +(d/c (cgen/list V X Y S T + #:expected-cset [expected-cset (empty-cset '() '())]) + (((listof symbol?) (listof symbol?) (listof symbol?) (listof Type?) (listof Type?)) + (#:expected-cset cset?) . ->* . cset?) (unless (= (length S) (length T)) (fail! S T)) - (cset-meet* (for/list ([s S] [t T]) (cgen V X Y s t)))) + (cset-meet* + (for/list ([s S] [t T]) + ;; We meet early to prune the csets to a reasonable size. + ;; This weakens the inference a bit, but sometimes avoids + ;; constraint explosion. + (cset-meet (cgen V X Y s t) expected-cset)))) ;; X : variables to infer ;; Y : indices to infer @@ -658,10 +667,11 @@ ;; just return a boolean result (define (infer X Y S T R [expected #f]) (with-handlers ([exn:infer? (lambda _ #f)]) - (let* ([cs (cgen/list null X Y S T)] - [cs* (if expected - (cset-meet cs (cgen null X Y R expected)) - cs)]) + (let* ([expected-cset (if expected + (cgen null X Y R expected) + (empty-cset '() '()))] + [cs (cgen/list null X Y S T #:expected-cset expected-cset)] + [cs* (cset-meet cs expected-cset)]) (if R (subst-gen cs* Y R) #t)))) ;; like infer, but T-var is the vararg type: @@ -676,16 +686,19 @@ (with-handlers ([exn:infer? (lambda _ #f)]) (let* ([short-S (take S (length T))] [rest-S (drop S (length T))] - [cs-short (cgen/list null X (list dotted-var) short-S T)] + [expected-cset (if expected + (cgen null X (list dotted-var) R expected) + (empty-cset '() '()))] + [cs-short (cgen/list null X (list dotted-var) short-S T + #:expected-cset expected-cset)] [new-vars (var-store-take dotted-var T-dotted (length rest-S))] [new-Ts (for/list ([v new-vars]) (substitute (make-F v) dotted-var (substitute-dots (map make-F new-vars) #f dotted-var T-dotted)))] - [cs-dotted (cgen/list null (append new-vars X) (list dotted-var) rest-S new-Ts)] + [cs-dotted (cgen/list null (append new-vars X) (list dotted-var) rest-S new-Ts + #:expected-cset expected-cset)] [cs-dotted* (move-vars-to-dmap cs-dotted dotted-var new-vars)] [cs (cset-meet cs-short cs-dotted*)]) - (if (not expected) - (subst-gen cs (list dotted-var) R) - (subst-gen (cset-meet cs (cgen null X (list dotted-var) R expected)) (list dotted-var) R))))) + (subst-gen (cset-meet cs expected-cset) (list dotted-var) R)))) ;(trace cgen)