(module type-printer-unit mzscheme
  
  (require "signatures.ss" (lib "unit.ss") "planet-requires.ss" "type-def-structs.ss" "tc-utils.ss" "effect-structs.ss")
  (require-libs)
  (require (planet "environment.ss" ("cobbe" "environment.plt" 3 0)))
  
  (provide (all-defined))
  
  (define-unit type-printer@
    (import type-structs^ infer^ subst^ effect-structs^)
    (export type-printer^)
    
    (define print-poly-types? #f)
    (define print-aliases #t)
    
    ;; check whether type t has an alias that can be used in printing
    ;; if a list is returned, it is the name of the polymorphic alias, plus the necessary type arguments
    ;; has-name : type -> (list symbol type ...) or #f
    (define (has-name t)    
      (define ns ((current-type-names)))
      (let/cc return
        (define (lookup v l)
          (let ([x (assoc v l)])
            (if x (cadr x) (return #f))))
        (for-each
         (lambda (pair)
           (cond [(and print-aliases (equiv? t (cdr pair)))
                  (return (car pair))]
                 [(and 
                   print-poly-types?
                   (poly? (cdr pair))
                   ;; fix in case when variable names are the same!
                   (unify1 (poly-type (cdr pair)) t))
                  => (lambda (s)
                       #;(printf "succeded in unifying! ~a~n" s)
                       (return
                        #;(printf "vars are: ~a~n subst-vars are:~a~n" (poly-var (cdr pair)) (map car s))
                          (let ([args (map (lambda (v) (lookup v s))
                                           (poly-var (cdr pair)))])
                            `(,(car pair) ,@args))))]))
         ns)
        #f))
    
    ;; print out an effect
    (define (print-effect c port write?)
      (define (fp . args) (apply fprintf port args))    
      (match c
        [($ restrict-effect t v) (fp "(restrict ~a ~a)" t (syntax-e v))]
        [($ remove-effect t v) (fp "(remove ~a ~a)" t (syntax-e v))]
        [($ latent-restrict-effect t) (fp "(restrict ~a)" t)]
        [($ latent-remove-effect t) (fp "(remove ~a)" t)]
        [($ latent-var-true-effect) (fp "(var #t)")]
        [($ latent-var-false-effect) (fp "(var #f)")]
        [($ true-effect) (fp "T")]
        [($ false-effect) (fp "F")]
        [($ var-true-effect v) (fp "(var #t ~a)" (syntax-e v))]
        [($ var-false-effect v) (fp "(var #f ~a)" (syntax-e v))]))
    
    ;; print out a type
    (define (print-type c port write?)
      (define (fp . args) (apply fprintf port args))    
      (cond 
        [(univ? c) (fp "Any")]
        [(has-name c) => (lambda (x) (fp "~a" x))]
        [(base-type? c) (fp "~a" (base-type-name c))]
        [(opaque-ty? c) (fp "(Opaque ~a)" (syntax-object->datum (opaque-ty-pred c)))]
        [(struct-ty? c) (fp "#<struct:~a ~a>" (struct-ty-name c) (struct-ty-flds c))]
        #;[(pred-ty? c) (fp "(pred ~a)" (pred-ty-type c))]
        [(arr? c) (fp "(")
                  (for-each (lambda (t) (fp "~a " t)) (arr-dom c))
                  (when (arr-rest c)
                    (fp "~a .. " (arr-rest c)))
                  (fp "-> ~a" (arr-rng c))
                  (unless (and (null? (arr-thn-eff c)) (null? (arr-els-eff c)))
                    (fp " : ~a ~a" (arr-thn-eff c) (arr-els-eff c)))
                  (fp ")")]
        [(funty? c) (let ([arities (funty-arities c)])
                      (if (= 1 (length arities))
                          (fp "~a" (car arities))
                          (begin
                            (fp "(case-lambda ")
                            (for-each (lambda (x) (fp "~a " x)) (funty-arities c))
                            (fp ")"))))]                        
        [(value? c) (let ([v (value-v c)])
                      (cond [(or (symbol? v) (null? v))
                             (fp "'~a" v)]
                            [else (fp "~a" v)]))]
        [(vec? c) (fp "(vector-of ~a)" (vec-elem c))]
        [(union? c) (fp "~a" (cons 'Un (set:elements (union-elems c))))]
        [(pair-ty? c) (fp "(cons ~a ~a)" (pair-ty-car c) (pair-ty-cdr c))]
        [(dynamic? c) (fp "*")]
        [(tvar? c) (fp "<~a>" (tvar-name c))]
        [(poly? c) (fp "(All ~a. ~a)" (poly-var c) (poly-type c))]
        [(mu? c) (fp "(mu ~a ~a)" (mu-var c) (mu-type c))]
        [(values-ty? c) (fp "~a" (cons 'values (values-ty-types c)))]
        [(param-ty? c) (fp "(Parameter ~a ~a)" (param-ty-in c) (param-ty-out c))]
        [else (fp "Unknown Type")]
        )))
  )