From f2c0187b0739208cc45ac4b3cc3cad8de8bb5b5a Mon Sep 17 00:00:00 2001
From: Vincent St-Amour <stamourv@racket-lang.org>
Date: Fri, 18 Feb 2011 17:35:12 -0500
Subject: [PATCH] Add a helper function to add filters en masse to express
 propositions that are true about a function's arguments if the function
 returns.

original commit: bf6379c36346e061031fe2916a1f6aece2367fb1
---
 collects/typed-scheme/private/env-lang.rkt |  4 ++--
 collects/typed-scheme/types/filter-ops.rkt | 23 ++++++++++++++++++++++
 2 files changed, 25 insertions(+), 2 deletions(-)

diff --git a/collects/typed-scheme/private/env-lang.rkt b/collects/typed-scheme/private/env-lang.rkt
index eb5ff44b..1cb997e7 100644
--- a/collects/typed-scheme/private/env-lang.rkt
+++ b/collects/typed-scheme/private/env-lang.rkt
@@ -8,7 +8,7 @@
          (r:infer infer)
          (only-in (r:infer infer-dummy) infer-param)
          (except-in (rep object-rep filter-rep type-rep) make-arr)
-         (types convenience union)
+         (types convenience union filter-ops)
          (only-in (types convenience) [make-arr* make-arr]))
 
 (define-syntax (-#%module-begin stx)
@@ -34,4 +34,4 @@
          require
          (except-out (all-from-out scheme/base) #%module-begin)
          types rep private utils         
-         (types-out convenience union))
+         (types-out convenience union filter-ops))
diff --git a/collects/typed-scheme/types/filter-ops.rkt b/collects/typed-scheme/types/filter-ops.rkt
index d20a32f4..954fb5e9 100644
--- a/collects/typed-scheme/types/filter-ops.rkt
+++ b/collects/typed-scheme/types/filter-ops.rkt
@@ -162,3 +162,26 @@
                     (loop (cdr fs) result)]
                    [else
                     (loop (cdr fs) (cons t result))])]))))
+
+;; ands the given type filter to both sides of the given arr for each argument
+;; useful to express properties of the form: if this function returns at all,
+;; we learn this about its arguments (like fx primitives, or car/cdr, etc.)
+(define (add-unconditional-filter-all-args arr type)
+  (match arr
+    [(Function: (list (arr: dom rng rest drest kws)))
+     (match rng
+       [(Values: (list (Result: tp (FilterSet: true-filter
+                                               false-filter)
+                                op)))
+        (let ([new-filters (apply -and (build-list (length dom)
+                                                   (lambda (i)
+                                                     (-filter type i))))])
+          (make-Function
+           (list (make-arr
+                  dom
+                  (make-Values
+                   (list (-result tp
+                                  (-FS (-and true-filter new-filters)
+                                       (-and false-filter new-filters))
+                                  op)))
+                  rest drest kws))))])]))