From 4092df1cca9002a9ab9f54c09a407d9d0e421bc3 Mon Sep 17 00:00:00 2001
From: Asumu Takikawa <asumu@ccs.neu.edu>
Date: Thu, 21 Nov 2013 21:12:40 -0500
Subject: [PATCH] Improve type of `negate`

Now for functions with simple filters, it'll negate the
filters so that, e.g., (negate string?) can be used with
occurrence typing.

Please merge to v6.0
(cherry picked from commit 0f8ee738142c8e253c638c836fc1c5c893751d32)
---
 .../typed-racket/base-env/base-env.rkt          | 13 +++++++++++--
 .../typed-racket/unit-tests/typecheck-tests.rkt | 17 +++++++++++++++++
 2 files changed, 28 insertions(+), 2 deletions(-)

diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-env.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-env.rkt
index 5c5eab71e4..2f38508e49 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-env.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-env.rkt
@@ -873,8 +873,17 @@
 ;; Section 4.17.3 (racket/function)
 [identity (-poly (a) (->acc (list a) a null))]
 [const (-poly (a) (-> a (->* '() Univ a)))]
-[negate (-polydots (b) (-> ((list) [b b] . ->... . Univ)
-                           ((list) [b b] . ->... . -Boolean)))]
+[negate (-polydots (a b c d)
+          (cl->* (-> (-> c Univ : (-FS (-filter a 0 null) (-not-filter b 0 null)))
+                     (-> c -Boolean : (-FS (-not-filter b 0 null) (-filter a 0 null))))
+                 (-> (-> c Univ : (-FS (-filter a 0 null) (-filter b 0 null)))
+                     (-> c -Boolean : (-FS (-filter b 0 null) (-filter a 0 null))))
+                 (-> (-> c Univ : (-FS (-not-filter a 0 null) (-filter b 0 null)))
+                     (-> c -Boolean : (-FS (-filter b 0 null) (-not-filter a 0 null))))
+                 (-> (-> c Univ : (-FS (-not-filter a 0 null) (-not-filter b 0 null)))
+                     (-> c -Boolean : (-FS (-not-filter b 0 null) (-not-filter a 0 null))))
+                 (-> ((list) [d d] . ->... . Univ)
+                     ((list) [d d] . ->... . -Boolean))))]
 ;; probably the most useful cases
 ;; doesn't cover cases where we pass multiple of the function's arguments to curry,
 ;; also doesn't express that the returned function is itself curried
diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt
index 11e87a5827..ebc14a2227 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt
@@ -161,6 +161,7 @@
   racket/file
   racket/fixnum
   racket/flonum
+  racket/function
   racket/list
   racket/math
   racket/path
@@ -1828,6 +1829,22 @@
           (define (f s) (if (set? s) s (set)))
           (void))
         -Void]
+
+       ;; negate
+       [tc-e
+        (let ()
+          (: x (U Symbol Void))
+          (define x 'foo)
+          (if ((negate void?) x) (symbol->string x) "foo"))
+        -String]
+       [tc-e
+        (let ()
+          (: pos? (Real -> Boolean : #:+ (Positive-Real @ 0) #:- (Nonpositive-Real @ 0)))
+          (define pos? (lambda: ([x : Real]) (positive? x)))
+          (: x Real)
+          (define x 3)
+          (if ((negate pos?) x) x -5))
+        #:ret (ret -NonPosReal (-FS -top -bot))]
         )
   (test-suite
    "tc-literal tests"