(module typechecker-unit (lib "a-unit.ss")
  
  ;; tests needed
  
  (require (rename (lib "1.ss" "srfi") assoc* assoc)
           (lib "kerncase.ss" "syntax")
           (lib "struct.ss" "syntax")
           (lib "stx.ss" "syntax")
           (lib "etc.ss")
           "signatures.ss"
           "tc-structs.ss"
           "subst.ss" ;; needs tests
           "utils.ss" ;; doesn't need tests
           "types.ss" ;; doesn't need tests
           "infer.ss" ;; needs tests
           "infer2.ss"
           "types-aux.ss" ;; maybe needs tests
           "subtype.ss" ;; has tests
           "internal-forms.ss" ;; doesn't need tests
           "remove-intersect.ss" ;; has tests
           "planet-requires.ss" ;; doesn't need tests
           "type-env.ss" ;; maybe needs tests
           "parse-type.ss" ;; has tests
           "tc-utils.ss" ;; doesn't need tests
           "type-environments.ss" ;; doesn't need tests
           "base-env.ss" ;; doesn't need tests
           "lexical-env.ss" ;; maybe needs tests
           "type-annotation.ss" ;; has tests
           "type-name-env.ss" ;; maybe needs tests
           "init-envs.ss"
           "effects.ss"
           "mutated-vars.ss"
           (lib "match.ss"))
  (require-for-template (lib "match.ss") "internal-forms.ss")
  (require-for-syntax (lib "match.ss") "internal-forms.ss")
  
  (require-libs)
  
  (require (planet "environment.ss" ("cobbe" "environment.plt" 3 0)))  
  
  (require-for-template mzscheme)
  
  (import tc-if^ tc-lambda^ tc-app^ tc-let^)
  (export typechecker^)
  
  ;; check that e-type is compatible with ty in context of stx
  ;; otherwise, error
  ;; syntax type type -> void
  (define (check-type stx e-type ty)
    (parameterize ([current-orig-stx stx])
      (unless (subtype e-type ty)
        (tc-error "body had type ~a, variable had type ~a" e-type ty))))
  
  ;; check that expr has type ty in context of stx
  ;; syntax syntax type -> void
  (define (check-expr stx expr ty)
    (check-type stx (tc-expr/t expr) ty))
  
  ;; return the type of a literal value
  ;; scheme-value -> type
  (define (tc-literal v-stx)
    ;; find the meet of the types of a list of expressions
    ;; list[syntax] -> type
    (define (types-of-literals es)
      (apply Un (map tc-literal es)))
    (define v (syntax-e v-stx))
    (cond
      [(number? v) N]
      [(boolean? v) (make-value v)]
      [(null? v) (make-value null)]
      [(symbol? v) (make-value v)]
      [(string? v) -String]
      [(keyword? v) -Keyword]
      [(bytes? v) -Bytes]
      [(list? v) (make-Listof (types-of-literals v))]
      [(vector? v) (make-vec (types-of-literals (vector->list v)))]
      [else (begin (printf "checking literal : ~a~n" v) Univ)]))
  
  ;; typecheck an identifier
  ;; the identifier has variable effect
  ;; tc-id : identifier -> tc-result
  (define (tc-id id)
    (ret (lookup-type/lexical id) (list (make-var-true-effect id)) (list (make-var-false-effect id))))
  
  ;; typecheck an expression, but throw away the effect
  ;; tc-expr/t : Expr -> Type
  (define (tc-expr/t e) (tc-result-t (tc-expr e)))
  
  ;; type check form in the current type environment
  ;; if there is a type error in form, or if it has the wrong annotation, error
  ;; otherwise, produce the type of form
  ;; syntax[expr] -> type
  (define (tc-expr form)
    (define ty-ann (type-annotation form))    
    ;; do the actual typechecking of form
    ;; internal-tc-expr : syntax -> Type
    (define (internal-tc-expr form)
      (kernel-syntax-case* form #f 
        (letrec-syntaxes+values) ;; letrec-syntaxes+values is not in kernel-syntax-case literals

        ;; data       
        [(#%datum . #f) (ret (-val #f) (list (make-false-effect)) (list (make-false-effect)))]
        [(#%datum . #t) (ret (-val #t) (list (make-true-effect)) (list (make-true-effect)))]
        [(quote #f) (ret (-val #f) (list (make-false-effect)) (list (make-false-effect)))]
        [(quote #t) (ret (-val #t) (list (make-true-effect)) (list (make-true-effect)))]
        
        [(#%datum . val) (ret (tc-literal #'val))]
        [(quote val)  (ret (tc-literal #'val))]
        ;; syntax
        [(quote-syntax datum) (ret -Syntax)]
        ;; w-c-m
        [(with-continuation-mark e1 e2 e3)
         (begin (tc-expr #'e1)
                (tc-expr #'e2)
                (tc-expr #'e3))]
        ;; lambda
        [(lambda formals . body)
         (tc/lambda form #'(formals) #'(body))]         
        [(case-lambda [formals . body] ...)
         (tc/lambda form #'(formals ...) #'(body ...))]      
        ;; let
        [(let-values ([(name ...) expr] ...) . body)
         (tc/let-values #'((name ...) ...) #'(expr ...) #'body form)]
        [(letrec-values ([(name ...) expr] ...) . body)
         (tc/letrec-values #'((name ...) ...) #'(expr ...) #'body form)]        
        ;; mutation!
        [(set! id val)
         (match-let* ([($ tc-result id-t _ _) (tc-id #'id)]
                      [($ tc-result val-t _ _) (tc-expr #'val)])
           (unless (subtype val-t id-t)
             (tc-error "Mutation only allowed with compatible types: ~a is not a subtype of ~a" val-t id-t))
           (ret -Void))]        
        ;; top-level variable reference - occurs at top level
        [(#%top . id) (tc-id #'id)]
        ;; weird
        [(#%variable-reference . _)
         (tc-error "do not use #%variable-reference")]
        ;; identifiers
        [x (identifier? #'x) (tc-id #'x)]                 
        ;; application       
        [(#%app . _) (tc/app form)]
        ;; if
        [(if tst body) (tc/if-onearm #'tst #'body)]               
        [(if tst thn els) (tc/if-twoarm #'tst #'thn #'els)]                          
        
        ;; syntax
        ;; for now, we ignore the rhs of macros
        [(letrec-syntaxes+values stxs vals . body)
         (tc-expr (syntax/loc form (letrec-values vals . body)))]
        
        ;; begin
        [(begin e . es) (tc-exprs (syntax->list #'(e . es)))]
        [(begin0 e . es)
         (begin (tc-exprs (syntax->list #'es))
                (tc-expr #'e))]
        
        ;; #%expression just contains an expression
        [(#%expression e) (tc-expr #'e)]
        ;; other
        [_ (tc-error "cannot typecheck unknown form : ~a~n" (syntax-object->datum form))]))
    
    (parameterize ([current-orig-stx form])
      ;(printf "form: ~a~n" (syntax-object->datum form))
      ;; the argument must be syntax
      (unless (syntax? form) 
        (int-err "bad form input to tc-expr: ~a" form))
      ;; typecheck form
      (match-let ([(and result ($ tc-result result-ty result-thn-eff result-els-eff))
                   (internal-tc-expr form)])
        (cond 
          ;; if we had an annotation, make sure it's appropriate for the actual type
          ;; if it is, return the annotation
          [(and ty-ann (subtype result-ty ty-ann)) (ret ty-ann)]
          ;; if we had an annotation, but it wasn't right, error
          [ty-ann (tc-error "expression had type ~a, but was annotated with type ~a" result-ty ty-ann)]
          ;; otherwise, just return the result
          [else result])))
    )
  
  ;; type-check a list of exprs, producing the type of the last one.
  ;; if the list is empty, the type is Void.
  ;; list[syntax[expr]] -> tc-result
  (define (tc-exprs exprs)
    (cond [(null? exprs) (ret -Void)]
          [(null? (cdr exprs)) (tc-expr (car exprs))]
          [else (tc-expr (car exprs))
                (tc-exprs (cdr exprs))]))
  
  (define (tc-toplevel/pass1 form)
    ;; first, find the mutated variables:
    (find-mutated-vars form)
    (parameterize ([current-orig-stx form])
      (kernel-syntax-case* form #f (define-type-alias-internal define-typed-struct-internal define-type-internal
                                     require/typed-internal :)
        ;; forms that are handled in other ways
        [stx 
         (syntax-property form 'typechecker:ignore)
         (void)]
        
        ;; directives to the typechecker
        [(#%expression (quote-syntax (require/typed-internal nm ty)))
         (register-type #'nm (parse-type #'ty))]
        [(#%expression (quote-syntax (define-type-alias-internal (nm . vars) ty)))
         (register-type-name #'nm (parse-type #'(All vars ty)))]
        [(#%expression (quote-syntax (define-type-alias-internal nm ty)))
         (register-type-name #'nm (parse-type #'ty))]
        
        [(#%expression (quote-syntax (define-typed-struct-internal nm ([fld : ty] ...))))
         (tc/struct #'nm (syntax->list #'(fld ...)) (syntax->list #'(ty ...)))]
        [(#%expression (quote-syntax (define-typed-struct-internal (vars ...) nm ([fld : ty] ...))))
         (tc/poly-struct (syntax->list #'(vars ...)) #'nm (syntax->list #'(fld ...)) (syntax->list #'(ty ...)))]
        
        [(#%expression (quote-syntax (define-type-internal nm top-pred elems ...)))
         (let ([variants0 (map (lambda (stx)
                                 (syntax-case stx ()
                                   [(variant maker (fld ty) ...)
                                    (list #'variant #'maker (map cons (syntax->list #'(ty ...)) (syntax->list #'(fld ...))))]))
                               (syntax->list #'(elems ...)))])
           (tc/define-type #'nm #'top-pred variants0))]
        
        [(define-values (var ...) expr)
         (andmap (lambda (s) (syntax-property s 'type-label)) (syntax->list #'(var ...)))
         (let* ([vars (syntax->list #'(var ...))]
                [ts (map get-type vars)])
           (for-each register-type vars ts))]
        ;; this definition had no type annotations
        [(define-values . _)
         (tc-error "Untyped definition")]
        ;; to handle the top-level, we have to recur into begins
        [(begin . rest)
         (for-each tc-toplevel/pass1 (syntax->list #'rest))]
        ;; otherwise, do nothing in this pass
        [_ (void)])))
  
  ;; typecheck the expressions of a module-top-level form
  ;; no side-effects
  ;; syntax -> void
  (define (tc-toplevel/pass2 form)
    (reverse-begin
     (do-time 
      (if (eq? 'define-values (syntax-e (stx-car form)))
          (format "In Pass 2 : ~a ~a"
                  'define-values 
                  (syntax-object->datum (stx-car (stx-cdr form))))
          (begin0 (format "In Pass 2 : ~a" (syntax-object->datum (stx-car form))) #;(stx-car (stx-cdr form)))))
     (parameterize ([current-orig-stx form])
       (kernel-syntax-case* form #f (define-type-alias-internal define-typed-struct-internal define-type-internal 
                                      require/typed-internal)
         ;; these forms we have been instructed to ignore
         [stx 
          (syntax-property form 'typechecker:ignore)
          (void)]
         
         ;; these forms should always be ignored
         [(require . _) (void)]
         [(require-for-syntax . _) (void)]
         [(require-for-template . _) (void)]
         [(provide . _) (void)]
         [(define-syntaxes . _) (void)]
         
         ;; these forms are handled in pass1
         [(#%expression (quote-syntax (require/typed-internal . rest))) (void)]
         [(#%expression (quote-syntax (define-type-alias-internal . rest))) (void)]
         [(#%expression (quote-syntax (define-typed-struct-internal . rest))) (void)]        
         [(#%expression (quote-syntax (define-type-internal . rest))) (void)]        
         
         ;; definitions just need to typecheck their bodies
         [(define-values (var ...) expr)
          (let* ([vars (syntax->list #'(var ...))]
                 [ts (map get-type vars)])
            (check-expr form #'expr (list->values-ty ts)))]
        ;; to handle the top-level, we have to recur into begins
         [(begin) (void)]
         [(begin . rest)
          (let loop ([l (syntax->list #'rest)])
            (if (null? (cdr l))
                (tc-toplevel/pass2 (car l))
                (begin (tc-toplevel/pass2 (car l))
                       (loop (cdr l)))))]
         
         ;; otherwise, the form was just an expression
         [_ (tc-expr form)]))))
  
  ;; typecheck a top-level form
  ;; used only from #%top-interaction
  ;; syntax -> void
  (define (tc-toplevel-form form)
    (tc-toplevel/pass1 form)
    (tc-toplevel/pass2 form))
  
  
  ;; type check a list of module-level forms
  ;; produce code to add the definitions in this module to the global table of module-level forms
  ;; syntax-list -> syntax
  (define (type-check forms)
    (let ([forms (syntax->list forms)])
      (do-time "Before Pass1")
      ;; install defined names and types in the environment
      (for-each tc-toplevel/pass1 forms)
      (do-time "Before Pass2")
      ;; typecheck the expressions
      (for-each tc-toplevel/pass2 forms)
      (do-time "After Pass2")    
      #`(begin
          #,(env-init-code)
          #,(tname-env-init-code))))
  
  ;(trace subtype-of)
  ;(trace check-expr)
  ;(trace tc-expr)
  ;(trace intersect-ty)
  ;(trace remove-ty)
  ;(trace all-in)
  ;(trace symbolic-identifier=?)
  
  ;(trace parse-type)
  
  
  )