From d51769c39f853e2b1c6d7a8e438b34b08508ebad Mon Sep 17 00:00:00 2001
From: Asumu Takikawa <asumu@ccs.neu.edu>
Date: Wed, 29 Oct 2014 18:29:23 -0400
Subject: [PATCH] Add suppport for weak boxes in TR

Closes PR 14771

original commit: 7829776f728432f6c3642c4282e4731500953ac1
---
 .../typed-racket/scribblings/reference/types.scrbl | 14 ++++++++++++++
 .../typed-racket/base-env/base-env.rkt             |  9 +++++++++
 .../typed-racket/base-env/base-types.rkt           |  2 ++
 .../typed-racket/infer/infer-unit.rkt              |  2 ++
 .../typed-racket-lib/typed-racket/rep/type-rep.rkt |  5 +++++
 .../typed-racket-lib/typed-racket/types/abbrev.rkt |  2 ++
 .../typed-racket/types/printer.rkt                 |  2 ++
 .../typed-racket/types/subtype.rkt                 |  2 ++
 .../typed-racket/unit-tests/typecheck-tests.rkt    | 14 ++++++++++++++
 9 files changed, 52 insertions(+)

diff --git a/pkgs/typed-racket-pkgs/typed-racket-doc/typed-racket/scribblings/reference/types.scrbl b/pkgs/typed-racket-pkgs/typed-racket-doc/typed-racket/scribblings/reference/types.scrbl
index a70399a2..2a3896e8 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-doc/typed-racket/scribblings/reference/types.scrbl
+++ b/pkgs/typed-racket-pkgs/typed-racket-doc/typed-racket/scribblings/reference/types.scrbl
@@ -454,6 +454,20 @@ type @racket[_t] on each iteration.}
 @ex[(lambda: ([x : Any]) (if (thread-cell? x) x (error "not a thread cell!")))]
 }
 
+@defform[(Weak-Boxof t)]{
+  The type for a @rtech{weak box} whose value is of type @racket[t].
+
+  @ex[(make-weak-box 5)
+      (weak-box-value (make-weak-box 5))]
+}
+
+@defidform[Weak-BoxTop]{is the type of a @rtech{weak box} with an unknown element
+  type and is the supertype of all weak box types. This type
+  typically appears in programs via the combination of occurrence
+  typing and @racket[weak-box?].
+@ex[(lambda: ([x : Any]) (if (weak-box? x) x (error "not a box!")))]
+}
+
 @defform[(Ephemeronof t)]{An @rtech{ephemeron} whose value is of type @racket[t].}
 
 @defform[(Evtof t)]{A @rtech{synchronizable event} whose @rtech{synchronization result}
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 ce5d0921..da862824 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
@@ -2855,6 +2855,15 @@
                       (-lst -String)
                       . -> . b))))]
 
+;; Section 16.1 (Weak Boxes)
+[make-weak-box (-poly (a) (-> a (-weak-box a)))]
+[weak-box-value
+ (-poly (a b)
+   (cl->* (-> (-weak-box a) (-opt a))
+          (-> (-weak-box a) b (Un b a))
+          (->opt -Weak-BoxTop [Univ] Univ)))]
+[weak-box? (make-pred-ty -Weak-BoxTop)]
+
 ;; Section 16.2 (Ephemerons)
 [make-ephemeron (-poly (k v) (-> k v (make-Ephemeron v)))]
 [ephemeron? (make-pred-ty (make-Ephemeron Univ))]
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-types.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-types.rkt
index cff177c5..ff389c9a 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-types.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-types.rkt
@@ -114,6 +114,7 @@
 [Identifier Ident]
 [Procedure top-func]
 [BoxTop -BoxTop]
+[Weak-BoxTop -Weak-BoxTop]
 [ChannelTop -ChannelTop]
 [Async-ChannelTop -Async-ChannelTop]
 [VectorTop -VectorTop]
@@ -168,6 +169,7 @@
 [Promise (-poly (a) (-Promise a))]
 [Pair (-poly (a b) (-pair a b))]
 [Boxof (-poly (a) (make-Box a))]
+[Weak-Boxof (-poly (a) (-weak-box a))]
 [Channelof (-poly (a) (make-Channel a))]
 [Async-Channelof (-poly (a) (make-Async-Channel a))]
 [Ephemeronof (-poly (a) (make-Ephemeron a))]
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt
index f1acfa4b..3ee52e22 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt
@@ -638,6 +638,8 @@
           ;; boxes are invariant - generate constraints *both* ways
           [((Box: e) (Box: e*))
            (cg/inv e e*)]
+          [((Weak-Box: e) (Weak-Box: e*))
+           (cg/inv e e*)]
           [((MPair: s t) (MPair: s* t*))
            (% cset-meet (cg/inv s s*) (cg/inv t t*))]
           [((Channel: e) (Channel: e*))
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/rep/type-rep.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/rep/type-rep.rkt
index e01ed3c0..ce7a711b 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/rep/type-rep.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/rep/type-rep.rkt
@@ -204,6 +204,10 @@
 (def-type Ephemeron ([elem Type/c])
   [#:key 'ephemeron])
 
+;; elem is a Type
+(def-type Weak-Box ([elem Type/c])
+  [#:key 'weak-box])
+
 ;; elem is a Type
 (def-type CustodianBox ([elem Type/c])
   [#:key 'custodian-box])
@@ -405,6 +409,7 @@
 
 ;; the supertype of all of these values
 (def-type BoxTop () [#:fold-rhs #:base] [#:key 'box])
+(def-type Weak-BoxTop () [#:fold-rhs #:base] [#:key 'weak-box])
 (def-type ChannelTop () [#:fold-rhs #:base] [#:key 'channel])
 (def-type Async-ChannelTop () [#:fold-rhs #:base] [#:key 'async-channel])
 (def-type VectorTop () [#:fold-rhs #:base] [#:key 'vector])
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/abbrev.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/abbrev.rkt
index 82351c8d..a436720a 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/abbrev.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/abbrev.rkt
@@ -61,6 +61,7 @@
 (define -vec make-Vector)
 (define -future make-Future)
 (define -evt make-Evt)
+(define -weak-box make-Weak-Box)
 
 (define (-seq . args) (make-Sequence args))
 
@@ -176,6 +177,7 @@
 (define Ident (-Syntax -Symbol))
 (define -HT make-Hashtable)
 (define/decl -BoxTop (make-BoxTop))
+(define/decl -Weak-BoxTop (make-Weak-BoxTop))
 (define/decl -ChannelTop (make-ChannelTop))
 (define/decl -Async-ChannelTop (make-Async-ChannelTop))
 (define/decl -HashTop (make-HashtableTop))
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/printer.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/printer.rkt
index 6b059a64..1b273d1a 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/printer.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/printer.rkt
@@ -403,6 +403,7 @@
     [(StructTypeTop:) 'Struct-TypeTop]
     [(StructTop: (Struct: nm _ _ _ _ _)) `(Struct ,(syntax-e nm))]
     [(BoxTop:) 'BoxTop]
+    [(Weak-BoxTop:) 'Weak-BoxTop]
     [(ChannelTop:) 'ChannelTop]
     [(Async-ChannelTop:) 'Async-ChannelTop]
     [(ThreadCellTop:) 'ThreadCellTop]
@@ -441,6 +442,7 @@
     [(Vector: e) `(Vectorof ,(t->s e))]
     [(HeterogeneousVector: e) `(Vector ,@(map t->s e))]
     [(Box: e) `(Boxof ,(t->s e))]
+    [(Weak-Box: e) `(Weak-Boxof ,(t->s e))]
     [(Future: e) `(Futureof ,(t->s e))]
     [(Channel: e) `(Channelof ,(t->s e))]
     [(Async-Channel: e) `(Async-Channelof ,(t->s e))]
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/subtype.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/subtype.rkt
index fd70379a..3e0b570b 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/subtype.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/subtype.rkt
@@ -514,6 +514,8 @@
          ;; Invariant types
          [((Box: s) (Box: t)) (type-equiv? A0 s t)]
          [((Box: _) (BoxTop:)) A0]
+         [((Weak-Box: s) (Weak-Box: t)) (type-equiv? A0 s t)]
+         [((Weak-Box: _) (Weak-BoxTop:)) A0]
          [((ThreadCell: s) (ThreadCell: t)) (type-equiv? A0 s t)]
          [((ThreadCell: _) (ThreadCellTop:)) A0]
          [((Channel: s) (Channel: t)) (type-equiv? A0 s t)]
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 b93de79e..d85ed733 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
@@ -1832,6 +1832,20 @@
                (struct-type-property? prop))
               #:ret (ret -Boolean -true-filter))
 
+        ;; Weak boxes
+        [tc-e (make-weak-box "foo") (-weak-box -String)]
+        [tc-e (weak-box-value (make-weak-box "foo")) (-opt -String)]
+        [tc-e (weak-box-value (ann (make-weak-box "foo") Weak-BoxTop))
+              Univ]
+        [tc-e (weak-box-value (make-weak-box "foo") 'bar)
+              (t:Un (-val 'bar) -String)]
+        [tc-err (let ()
+                  (define b1 (make-weak-box "foo"))
+                  (: b2 (Weak-Boxof (U Symbol String)))
+                  (define b2 b1)
+                  (error "foo"))
+                #:msg #rx"expected: \\(Weak-Boxof \\(U Symbol String\\)\\)"]
+
         ;Wills
         (tc-e (make-will-executor) -Will-Executor)
         ;; FIXME: Broken because ManyUniv doesn't have a corresponding tc-result