(module remove-intersect mzscheme
  
  #;(require "types.ss" "types-aux.ss" "infer.ss" "subtype.ss" "planet-requires.ss" "subst.ss" "infer2.ss")
  
  #;(require-libs)
  
  (require "type-rep.ss" "unify.ss" "union.ss" "infer2.ss" "subtype.ss" (lib "plt-match.ss") (only (lib "list.ss") filter))
  
  (define (overlap t1 t2)
    (match (list t1 t2)
      
      [(list (Univ:) _) #t]
      [(list _ (Univ:)) #t]
      [(list (F: _) _) #t]
      [(list _ (F: _)) #t]
      [(list (? Mu?) _) (overlap (unfold t1) t2)]
      [(list _ (? Mu?)) (overlap t1 (unfold t2))]
      [(list (Union: e) t)
       (ormap (lambda (t*) (overlap t* t)) e)]
      [(list t (Union: e))
       (ormap (lambda (t*) (overlap t t*)) e)]
      [(or (list _ (? Poly?)) (list (? Poly?) _))
       #t] ;; these can have overlap, conservatively
      [(list (Base: s1) (Base: s2)) (eq? s1 s2)]
      [(list (Base: _) (Value: _)) (subtype t2 t1)] ;; conservative
      [(list (Value: _) (Base: _)) (subtype t1 t2)] ;; conservative
      [(list (Base: _) _) #f]
      [(list _ (Base: _)) #f]
      #;[]
      [(list (Value: '()) (Pair: _ _)) #f]
      [(list (Pair: _ _) (Value: '())) #f]
      [else #t]))
  
  ;; this is *definitely* not yet correct
  
  ;; NEW IMPL
  ;; restrict t1 to be a subtype of t2
  (define (restrict t1 t2)     
    ;; we don't use union map directly, since that might produce too many elements
    (define (union-map f l)
      (match l
        [(Union: es) (apply Un (map f es))]))
    (cond [(subtype t1 t2) t1] ;; already a subtype         
          [(match t2
             [(Poly: vars t)
              (let ([subst (infer t t1 vars)])
                (and subst (restrict t1 (subst-all subst t1))))]
             [_ #f])]           
          [(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
          ))
  #;
  (trace restrict)
  
  ;; 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)
                  [(list (Mu: v b) t) (make-Mu v (intersect b t))]
                  [(list (Union: l1) (Union: l2))
                   (apply Un (filter (lambda (e) (member e l2)) l1))]
                  [(list (Union: l) t)
                   (apply Un (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)
            [(list (Union: l) rem)
             (apply Un (map (lambda (e) (remove e rem)) l))]                  
            [(list (? Mu? old) t) (remove (unfold old) t)]
            [(list (Poly: vs b) t) (make-Poly vs (remove b rem))]
            [_ old])))
    (if (subtype old initial) old initial))
    
  ;(trace remove)
  ;(trace restrict)
  
  (provide restrict remove overlap)

  )