(module types-aux mzscheme
  (require "planet-requires.ss"
           "types.ss"
           "type-equal.ss"
           "subtype.ss"
           "effects.ss"
           "tc-utils.ss"
           )
  
  (require-libs) 

  (provide (all-defined) type-equal?)
  
  
  (define (make-union* set)
    (if (= 1 (set:size set))
        (set:select set)
        (make-union set)))
  
  (require (planet "memoize.ss" ("dherman" "memoize.plt" 2)))

  
  (define (Un . args) 
    (define (make-union/one t) (if (union? t) (union-elems t) (set:make-ordered type-compare t)))    
    (define (union2 a b)     
      (cond [(subtype a b) b]
            [(subtype b a) a]
            [(and (values-ty? a) (values-ty? b) (= (length (values-ty-types a)) (length (values-ty-types b))))
             (make-values-ty (map Un (values-ty-types a) (values-ty-types b)))]
            [(or (values-ty? a) (values-ty? b))
             (tc-error "Internal error: wrong values in Un: ~a ~a" a b)]
            [else 
             (make-union* (set:union (make-union/one a) (make-union/one b)))]))
    (foldl union2 (make-union (set:make-ordered type-compare)) args))
    
  (define-syntax -v 
    (syntax-rules ()
      [(_ x) (make-tvar 'x)]))
  
  (define-syntax -poly
    (syntax-rules ()
      [(_ (vars ...) ty)
       (let ([vars (-v vars)] ...)
         (make-poly (list 'vars ...) ty))]))
  
  (define-syntax -mu
    (syntax-rules ()
      [(_ var ty)
       (let ([var (-v var)])
         (make-mu 'var ty))]))
  
  
  (define -values make-values-ty)
  
  ;; produce the appropriate type of a list of types
  ;; that is - if there is exactly one type, just produce it, otherwise produce a values-ty
  ;; list[type] -> type
  (define (list->values-ty l)
    (if (= 1 (length l)) (car l) (make-values-ty l)))

  
  (define -pair make-pair-ty)
  (define -base make-base-type)
  
  (define -struct make-struct-ty)
  
  (define A (Un Sym N B -String))
    
  (define (make-Listof elem) (-mu list-rec (Un (make-value null) (-pair elem list-rec))))
  (define -Listof (-poly (list-elem) (make-Listof list-elem)))
  
  (define -lst make-Listof)
  (define -val make-value)
  (define -Sexp (-mu x (Un Sym N B -String (make-value '()) (-pair x x))))
  
  (define (-lst* . args) (if (null? args)
                             (-val null)
                             (-pair (car args) (apply -lst* (cdr args)))))
  

  #;(define NE (-mu x (Un N (make-Listof x))))
  (define -NE (-mu x (Un N (-pair x (-pair Sym (-pair x (-val null)))))))
  
  (define (Un/eff . args)
    (apply Un (map tc-result-t args)))

  (define -Param make-param-ty)
  
  (define make-pred-ty
    (case-lambda 
      [(in out t)
       (make-funty (list (make-arr in out #f 
                                   (list (make-latent-restrict-effect t))
                                   (list (make-latent-remove-effect t)))))]
      [(t) (make-pred-ty (list Univ) B t)]))
  



  )