(module parse-type mzscheme
  
  (provide parse-type parse-type/id)
  
  (require (all-except "type-rep.ss" make-arr)
           "type-effect-convenience.ss"
           (rename "type-effect-convenience.ss" make-arr make-arr*)
           "tc-utils.ss"
           "union.ss"
           (all-except "type-environments.ss" Void String)
           "type-name-env.ss"
           (only (lib "list.ss") foldl foldr)
           (all-except (lib "list.ss"  "srfi" "1") unfold remove)
           (lib "plt-match.ss"))
  
  (define enable-mu-parsing (make-parameter #t))
  
  
  (define (parse-type/id loc datum)
    #;(printf "parse-type/id id : ~a~n ty: ~a~n" (syntax-object->datum loc) (syntax-object->datum stx))
    (let* ([stx* (datum->syntax-object loc datum loc loc)])
      (parse-type stx*)))
  
  
  (define (parse-type stx)
    (parameterize ([current-orig-stx stx])
      (syntax-case* stx (-> : U mu Un All case-lambda values pred cons quote Opaque Parameter Tuple)
        symbolic-identifier=?
        [id
         (identifier? #'id)
         (lookup (current-tvars) (syntax-e #'id)
                 (lambda (key)
                   (lookup-type-name #'id
                                     (lambda () (tc-error "unbound type ~a" key)))))]     
        [(fst . rst)
         (not (syntax->list #'rst))
         (-pair (parse-type #'fst) (parse-type #'rst))]
        [(Tuple ts ...)
         (foldr -pair (-val '()) (map parse-type (syntax->list #'(ts ...))))]
        [(cons fst rst) (-pair (parse-type #'fst) (parse-type #'rst))]
        [(pred t) (make-pred-ty (parse-type #'t))]
        [(dom -> rng : pred-ty)
         (make-pred-ty (list (parse-type #'dom)) (parse-type #'rng) (parse-type #'pred-ty))]
        [(dom ... rest ::: -> rng)
         (symbolic-identifier=? #'::: (quote-syntax ..))
         (->* (map parse-type (syntax->list #'(dom ...))) (parse-type #'rest) (parse-type #'rng))]
        ;; has to be below the previous one
        [(dom ... -> rng) 
         (->* (map parse-type (syntax->list #'(dom ...))) (parse-type #'rng))]
        [(values tys ...) (-values (map parse-type (syntax->list #'(tys ...))))]
        [(case-lambda tys ...) (make-Function (map (lambda (ty) 
                                                  (syntax-case* ty (->) symbolic-identifier=?
                                                    [(dom ... -> rng)
                                                     (make-arr 
                                                      (map parse-type (syntax->list #'(dom ...))) 
                                                      (parse-type #'rng))]))
                                                (syntax->list #'(tys ...))))]
        ;; I wish I could write this
        #;[(case-lambda ([dom ... -> rng] ...)) (make-funty (list (make-arr (list (parse-type #'dom) ...) (parse-type #'rng)) ...))]
        #;[(list-of t) (make-lst (parse-type #'t))]
	#;[(Listof t) (make-lst (parse-type #'t))]
	[(Vectorof t) (make-Vector (parse-type #'t))]
        [(mu x t) 
         (and (identifier? #'x)
              (enable-mu-parsing))
         (let* ([var (syntax-e #'x)]
                [tvar (make-F var)])
           (parameterize ([current-tvars (extend-env (list var) (list tvar) (current-tvars))])
             (make-Mu var (parse-type #'t))))]
	[(U ts ...) (apply Un (map parse-type (syntax->list #'(ts ...))))]
        [(Un ts ...) (apply Un (map parse-type (syntax->list #'(ts ...))))]
        [(quote t)
         (-val (syntax-e #'t))]
        [(All (vars ...) t) 
         (andmap identifier? (syntax->list #'(vars ...)))
         (let* ([vars (map syntax-e (syntax->list #'(vars ...)))]
                [tvars (map make-F vars)])
           (parameterize ([current-tvars (extend-env vars tvars (current-tvars))])
             (make-Poly vars (parse-type #'t))))]        
        [(Opaque p?) (make-Opaque #'p? (syntax-local-certifier))]
        [(Parameter t) (let ([ty (parse-type #'t)]) (-Param ty ty))]
        [(Parameter t1 t2) (-Param (parse-type #'t1) (parse-type #'t2))]
        [(All . rest) (tc-error "All: bad syntax")]
        [(Opaque . rest) (tc-error "Opaque: bad syntax")]
        [(U . rest) (tc-error "Union: bad syntax")]
        [(Vectorof . rest) (tc-error "Vectorof: bad syntax")]
        [(mu . rest) (tc-error "mu: bad syntax")]
        [(Un . rest) (tc-error "Union: bad syntax")]
        [(t ... -> . rest) (tc-error "->: bad syntax")]
        [(id arg args ...)
         (identifier? #'id)
         (let ([ty (parse-type #'id)])
           (unless (Poly? ty)
             (tc-error "not a polymorphic type: ~a" (syntax-e #'id)))
           (unless (= (length (syntax->list #'(arg args ...))) (Poly-n ty))
             (tc-error "wrong number of arguments to type constructor ~a: expected ~a, got ~a" 
                       (syntax-e #'id)
                       (Poly-n ty)
                       (length (syntax->list #'(arg args ...)))))
           (instantiate-poly ty (map parse-type (syntax->list #'(arg args ...)))))]
        [t
         (or (boolean? (syntax-e #'t)) (number? (syntax-e #'t))
             (string? (syntax-e #'t)))
         (-val (syntax-e #'t))]
        [_ (tc-error "not a valid type: ~a" stx)])))
  
  )