From a8ee1063206ca8baa4429d823d1d8d6e3f11ce02 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. original commit: 80a9027f1eee6ea56a29aa73c65675f6cf86cdb2 --- .../tests/typed-scheme/fail/values-dots.rkt | 2 +- .../typed-scheme/xfail/ann-map-funcs.rkt | 21 +++++++++++ .../{succeed => xfail}/unholy-terror.rkt | 3 ++ collects/typed-scheme/infer/infer-unit.rkt | 37 +++++++++++++------ 4 files changed, 50 insertions(+), 13 deletions(-) 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 f92743fa..d12b885d 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/xfail/ann-map-funcs.rkt b/collects/tests/typed-scheme/xfail/ann-map-funcs.rkt new file mode 100644 index 00000000..5a87b8cf --- /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 7fbf8c79..2166707a 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 6d13c892..9ea79cec 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)