From 53d1d8a15df1be58d23951e492fd97f37d8c0da0 Mon Sep 17 00:00:00 2001
From: Andrew Kent <andmkent@indiana.edu>
Date: Mon, 22 Dec 2014 12:35:15 -0500
Subject: [PATCH] restrict structural recursion

---
 .../typed-racket/infer/restrict.rkt           | 83 +++++++++++++------
 1 file changed, 57 insertions(+), 26 deletions(-)

diff --git a/typed-racket-lib/typed-racket/infer/restrict.rkt b/typed-racket-lib/typed-racket/infer/restrict.rkt
index 84008896..5318e8c8 100644
--- a/typed-racket-lib/typed-racket/infer/restrict.rkt
+++ b/typed-racket-lib/typed-racket/infer/restrict.rkt
@@ -2,36 +2,67 @@
 
 (require "../utils/utils.rkt")
 (require (rep type-rep)
-         (types union subtype remove-intersect resolve)
+         (types abbrev base-abbrev union subtype remove-intersect resolve)
          "signatures.rkt"
-         racket/match)
+         racket/match
+         racket/set)
 
 (import infer^)
 (export restrict^)
 
-;; we don't use union map directly, since that might produce too many elements
-  (define (union-map f l)
-    (match l
-      [(Union: es)
-       (let ([l (map f es)])
-         (apply Un l))]))
 
-;; NEW IMPL
 ;; restrict t1 to be a subtype of t2
-;; if `f' is 'new, use t2 when giving up, otherwise use t1
-(define (restrict* t1 t2 [f 'new])
-  (cond
-    [(subtype t1 t2) t1] ;; already a subtype
-    [(match t2 
-       [(Poly: vars t)
-        (and (infer vars null (list t1) (list t) #f) t1)]
-       [_ #f])]
-    [(Union? t1) (union-map (lambda (e) (restrict* e t2 f)) t1)]
-    [(Union? t2) (union-map (lambda (e) (restrict* t1 e f)) t2)]
-    [(needs-resolving? t1) (restrict* (resolve-once t1) t2 f)]
-    [(needs-resolving? t2) (restrict* t1 (resolve-once t2) f)]
-    [(subtype t2 t1) t2] ;; we don't actually want this - want something that's a part of t1
-    [(not (overlap t1 t2)) (Un)] ;; there's no overlap, so the restriction is empty
-    [else (if (eq? f 'new) t2 t1)])) ;; t2 and t1 have a complex relationship, so we punt
-
-(define restrict restrict*)
+;; if `pref' is 'new, use t2 when giving up, otherwise use t1
+(define (restrict t1 t2 [pref 'new])
+  ;; build-type: build a type while propogating bottom
+  (define (build-type constructor . args)
+    (if (memf Bottom? args) -Bottom (apply constructor args)))
+  ;; resolved is a set tracking previously seen restrict cases
+  ;; (i.e. pairs of t1 t2) to prevent infinite unfolding.
+  ;; subtyping performs a similar check for the same
+  ;; reason
+  (define (restrict* t1 t2 pref resolved)
+    (match* (t1 t2)
+      ;; already a subtype
+      [(_ _) #:when (subtype t1 t2) 
+             t1]
+      
+      ;; polymorphic restrict
+      [(_ (Poly: vars t)) #:when (infer vars null (list t1) (list t) #f)
+                          t1]
+      
+      ;; structural recursion on types
+      [((Pair: a1 d1) (Pair: a2 d2)) 
+       (build-type -pair 
+                   (restrict* a1 a2 pref resolved) 
+                   (restrict* d1 d2 pref resolved))]
+      ;; FIXME: support structural updating for structs when structs are updated to
+      ;; contain not only *if* they are polymorphic, but *which* fields are too  
+      ;;[((Struct: _ _ _ _ _ _)
+      ;; (Struct: _ _ _ _ _ _))]
+      [((Syntax: t1*) (Syntax: t2*))
+       (build-type -Syntax (restrict* t1* t2* pref resolved))]
+      [((Promise: t1*) (Promise: t2*))
+       (build-type -Promise (restrict* t1* t2* pref resolved))]
+      
+      ;; unions
+      [((Union: t1s) _) (apply Un (map (λ (t1*) (restrict* t1* t2 pref resolved)) t1s))]
+      [(_ (Union: t2s)) (apply Un (map (λ (t2*) (restrict* t1 t2* pref resolved)) t2s))]
+      
+      ;; resolve resolvable types if we haven't already done so
+      [((? needs-resolving?) _) #:when (not (set-member? resolved (cons t1 t2)))
+                                (restrict* (resolve-once t1) t2 pref (set-add resolved (cons t1 t2)))]
+      [(_ (? needs-resolving?)) #:when (not (set-member? resolved (cons t1 t2)))
+                                (restrict* t1 (resolve-once t2) pref (set-add resolved (cons t1 t2)))]
+      
+      ;; we don't actually want this - want something that's a part of t1
+      [(_ _) #:when (subtype t2 t1)
+             t2]
+      
+      ;; there's no overlap, so the restriction is empty
+      [(_ _) #:when (not (overlap t1 t2)) 
+             (Un)]
+      
+      ;; t2 and t1 have a complex relationship, so we punt
+      [(_ _) (if (eq? pref 'new) t2 t1)]))
+  (restrict* t1 t2 pref (set)))