(module tc-if-unit (lib "a-unit.ss")
  
  (require "planet-requires.ss"
           "signatures.ss"
           "type-rep.ss" ;; doesn't need tests
           "type-effect-convenience.ss" ;; maybe needs tests
           "lexical-env.ss" ;; maybe needs tests
           "effect-rep.ss"
           "mutated-vars.ss"
           "subtype.ss"
           "remove-intersect.ss"
           "union.ss"
           "type-comparison.ss"
           (lib "kerncase.ss" "syntax")
           (lib "plt-match.ss")
           (lib "trace.ss"))
  
  (require-galore)
    
  ;; 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 effects
  ;; t/f tells us whether this is the true or the false branch of an if
  ;;      neccessary for handling true/false effects
  ;; Boolean Expr listof[Effect] -> TC-Result
  (define (tc-expr/eff t/f 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)])
          ;(printf "new-t ~a~n" new-t)
          ;; if this operation produces an uninhabitable type, then this expression can't be executed
          (when (type-equal? new-t (Un))
            ;(printf "setting flag!~n")
            (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
                  (begin #;(printf "returning ~a ~a~n" (syntax-object->datum expr) ty) ty)))
            ;; recursive case
            (match (car effs)
              ;; these effects have no consequence for the typechecking
              [(True-Effect:)
               (or t/f (set-box! flag #t)) 
               (loop (cdr effs))]
              [(False-Effect:) 
               (and t/f (set-box! flag #t))
               (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)
    ;; 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 #t thn tst-thn-eff)]
                 #;[_ (printf "v is ~a~n" v)]
                 #;[c (current-milliseconds)]
                 [(tc-result: els-ty els-thn-eff els-els-eff) (tc-expr/eff #f els tst-els-eff)])
      #;(printf "v now is ~a~n" (ret els-ty els-thn-eff els-els-eff))
      #;(printf "els-ty ~a ~a~n" 
              els-ty c)
         (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!
           [(list (list (True-Effect:)) (list (True-Effect:)) (list (Restrict-Effect: t v)) (list (Remove-Effect: t v*)))
            (=> unmatch)
            ;(printf "or branch~n")
            (match (list tst-thn-eff tst-els-eff)
              ;; check that the test was also a simple predicate
              [(list (list (Restrict-Effect: s u)) (list (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))
                   ;; 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'
           [(list _ _ (list (False-Effect:)) (list (False-Effect:)))
            ;(printf "and branch~n")
            (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
           [_ 
            #;(printf "els-ty ~a ~a~n" 
                    els-ty c)
            #;(printf "----------------------~nels-ty ~a ~nUn~a~n ~a~n" 
                     els-ty (Un thn-ty els-ty) c)
            (ret (Un thn-ty els-ty))])))

        
  ;(trace tc-expr/eff)

  
  )