(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) )