(module remove-intersect mzscheme
  
  (require "types.ss" "types-aux.ss" "infer.ss" "subtype.ss" "planet-requires.ss" "subst.ss" "infer2.ss")
  
  (require-libs)
  
  (define (overlap t1 t2)
    (match (list t1 t2)
      [(($ univ) _) #t]
      [(_ ($ univ)) #t]
      [((? mu?) _) (overlap (unfold t1) t2)]
      [(_ (? mu?)) (overlap t1 (unfold t2))]
      [(($ union e) t)
       (ormap (lambda (t*) (overlap t* t)) (set:elements e))]
      [(t ($ union e))
       (ormap (lambda (t*) (overlap t t*)) (set:elements e))]
      [((or ($ poly _ _)) 
        (or ($ poly _ _))) #t] ;; these can have overlap, conservatively
      [(($ base-type s1) ($ base-type s2)) (eq? s1 s2)]
      [(($ base-type _) ($ value _)) (subtype t2 t1)] ;; conservative
      [(($ value _) ($ base-type _)) (subtype t1 t2)] ;; conservative
      [(($ base-type _) _) #f]
      [(_ ($ base-type _)) #f]
      [else #t]))
  
  ;; this is *definitely* not yet correct
  
  ;; NEW IMPL
  ;; restrict t1 to be a subtype of t2
  (define (restrict t1 t2)
    #;(define (unify/poly a b)
      (if (poly? b)
          (let* ([vs (poly-var b)]
                 [vs* (map gensym vs)]
                 [body* (subst-all (map (lambda (v v*) (list v (make-tvar v*))) vs vs*) (poly-type b))]
                 [subst (unify (list (list a body*)))])
            (if subst a #f))
          #f))    
    ;; we don't use union map directly, since that might produce too many elements
    (define (union-map f l)
      (apply Un (map f (set:elements (union-elems l)))))
    (cond [(subtype t1 t2) t1] ;; already a subtype         
          [(and (poly? t2)
                (let* ([vars (poly-var t2)]
                       [t (poly-type t2)]
                       [subst (infer t t1 vars)])
                  (if subst
                      (restrict t1 (subst-all subst t))
                      #f)))]
          #;[(unify/poly t1 t2)]
          [(union? t1) (union-map (lambda (e) (restrict e t2)) t1)]
          [(mu? t1)
           (restrict (unfold t1) t2)]
          [(mu? t2) (restrict t1 (unfold t2))]
          [(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 t2] ;; t2 and t1 have a complex relationship, so we punt
          ))

  ;; this is really restrict: restrict t1 to be a subtype of t2
  (define (intersect t1 t2)
    (cond [(subtype t1 t2) t1]
          [(subtype t2 t1) t2]
          [else (match (list t1 t2)
                  [(($ mu v b) t) (intersect b t)]
                  [(($ union l1) ($ union l2))
                   (make-union* (set:filter (lambda (e) (set:member? e l2)) l1))]
                  [(($ union l) t)
                   (make-union* (set:filter (lambda (e) (subtype e t)) l))]
                  [_ t1])]
        ))
  
  ;; also not yet correct
  ;; produces old without the contents of rem
  (define (remove old rem)
    (define initial
      (if (subtype old rem) 
          (Un) ;; the empty type
          (match (list old rem)
            [(($ union l) rem)
             (apply Un (map (lambda (e) (remove e rem)) (set:elements l)))]
            #;[(($ union l) t)
               (make-union* (set:filter (lambda (e) (not (type-equal? e t))) l))]
            #;[(t ($ union l2))
               (set:fold remove t l2)]      
            [((? mu? old) t) (remove (unfold old) t)]
            [(($ poly v b) t) (make-poly v (remove b rem))]
            [_ old])))
    (if (subtype old initial) old initial))
    
  ;(trace remove)
  ;(trace restrict)
  
  (provide restrict remove overlap)

  )