(module tc-if-unit (lib "a-unit.ss")
  
  (require "planet-requires.ss"
           "signatures.ss"
           "types.ss" ;; doesn't need tests
           "types-aux.ss" ;; maybe needs tests
           "lexical-env.ss" ;; maybe needs tests
           "effects.ss"
           "mutated-vars.ss"
           "subtype.ss"
           "remove-intersect.ss"
           (lib "kerncase.ss" "syntax")
           (lib "match.ss"))
  
  (require-libs)
    
  ;; necessary for creating (#%app void) in tc-if/onearm
  (require-for-template mzscheme)
  
  ;; if typechecking  
  (import typechecker^)
  (export tc-if^)
       
  
  ;; combinators for typechecking in the context of an effect
  ;; Expr Effect -> TC-Result
  (define (tc-expr/eff expr effs)
    ;; this flag represents whether the refinement proves that this expression cannot be executed
    (let ([flag (box #f)])
      ;; this does the operation on the old type
      ;; type-op : (Type Type -> Type) Type -> _ Type -> Type
      (define ((type-op f t) _ old)
        (let ([new-t (f old t)])
          ;; if this operation produces an uninhabitable type, then this expression can't be executed
          (when (subtype new-t (Un)) (set-box! flag #t))
          ;; have to return something here, so that we can continue typechecking
          new-t))
      ;; loop : listof[effect] -> tc-result
      (let loop ([effs effs])
        ;; convenience macro for checking the rest of the list
        (define-syntax check-rest
          (syntax-rules ()
            [(check-rest f v)
             (with-update-type/lexical f v (loop (cdr effs)))]
            [(check-rest f t v) (check-rest (type-op f t) v)]))
        (if (null? effs)
            ;; base case
            (let ([ty (tc-expr expr)])
              (if (unbox flag) 
                  ;; the expr can't be executed, return the empty type
                  (ret (Un)) 
                  ;; this is already a tc-result
                  ty))
            ;; recursive case
            (match (car effs)
              ;; these effects have no consequence for the typechecking
              [($ true-effect) (loop (cdr effs))]
              [($ false-effect) (loop (cdr effs))]
              ;; restrict v to have a type that's a subtype of t
              [($ restrict-effect t v) (check-rest restrict t v)]
              ;; remove t from the type of v
              [($ remove-effect t v) (check-rest remove t v)]
               ;; just replace the type of v with (-val #f)
              [($ var-false-effect v) (check-rest (lambda (_ old) (-val #f)) v)]
              ;; v cannot have type (-val #f)
              [($ var-true-effect v) (check-rest remove (-val #f) v)])))))
  
  ;; create a dummy else branch for typechecking
  (define (tc/if-onearm tst body) (tc/if-twoarm tst body (syntax/loc body (#%app void))))  

  ;; the main function
  (define (tc/if-twoarm tst thn els)
    (kernel-syntax-case* tst #f ()      
      ;; check in the context of the effects, and return
      [_ 
       (match-let* ([($ tc-result tst-ty tst-thn-eff tst-els-eff) (tc-expr tst)]
                    [($ tc-result thn-ty thn-thn-eff thn-els-eff) (tc-expr/eff thn tst-thn-eff)]
                    [($ tc-result els-ty els-thn-eff els-els-eff) (tc-expr/eff els tst-els-eff)])
         (match (list thn-thn-eff thn-els-eff els-thn-eff els-els-eff) 
           ;; this is the case for `or'
           ;; the then branch has to be #t
           ;; the else branch has to be a simple predicate
           ;; FIXME - can something simpler be done by using demorgan's law?
           ;; note that demorgan's law doesn't hold for scheme `and' and `or' because they can produce arbitrary values
           ;; FIXME - mzscheme's or macro doesn't match this!
           [((($ true-effect)) (($ true-effect)) (($ restrict-effect t v)) (($ remove-effect t* v*)))
            (=> unmatch)
            (match (list tst-thn-eff tst-els-eff)
              ;; check that the test was also a simple predicate
              [((($ restrict-effect s u)) (($ remove-effect s* u*)))
               (if (and 
                    ;; check that all the predicates are for the for the same identifier
                    (module-identifier=? u u*)
                    (module-identifier=? v v*)
                    (module-identifier=? v u)
                    ;; check that then and else branches are for the same type
                    (type-equal? t t*)
                    (type-equal? s s*))
                   ;; this is just a very simple or
                   (ret (Un (-val #t) els-ty)
                        ;; the then and else effects are just the union of the two types
                        (list (make-restrict-effect (Un s t) v))
                        (list (make-remove-effect (Un s t) v)))
                   ;; otherwise, something complicated is happening and we bail
                   (unmatch))]
              ;; similarly, bail here
              [_ (unmatch)])]
           ;; this is the case for `and'
           [(_ _(($ false-effect)) (($ false-effect)))
            (ret (Un (-val #f) thn-ty) 
                 ;; we change variable effects to type effects in the test,
                 ;; because only the boolean result of the test is used
                 ;; whereas, the actual value of the then branch is returned, not just the boolean result
                 (append (map var->type-eff tst-thn-eff) thn-thn-eff)
                 ;; no else effects for and, because any branch could have been false
                 (list))]
           ;; otherwise this expression has no effects
           [_ (ret (Un thn-ty els-ty))]))]))

        
  ;(trace tc/if-twoarm)

  
  )