diff --git a/collects/typed-scheme/typecheck/tc-envops.ss b/collects/typed-scheme/typecheck/tc-envops.ss index c6264d9fb5..e3d94c7d6b 100644 --- a/collects/typed-scheme/typecheck/tc-envops.ss +++ b/collects/typed-scheme/typecheck/tc-envops.ss @@ -65,7 +65,7 @@ ;; sets the flag box to #f if anything becomes (U) (d/c (env+ env fs flag) (env? (listof Filter/c) (box/c #t). -> . env?) - (define-values (imps atoms) (debug combine-props fs (env-props env))) + (define-values (imps atoms) (debug combine-props fs (env-props env) flag)) (for/fold ([Γ (replace-props env imps)]) ([f atoms]) (match f [(Bot:) (set-box! flag #f) (env-map (lambda (x) (cons (car x) (Un))) Γ)] diff --git a/collects/typed-scheme/typecheck/tc-metafunctions.ss b/collects/typed-scheme/typecheck/tc-metafunctions.ss index e18bf9c99d..98bd6ba654 100644 --- a/collects/typed-scheme/typecheck/tc-metafunctions.ss +++ b/collects/typed-scheme/typecheck/tc-metafunctions.ss @@ -90,7 +90,21 @@ (provide combine-props tc-results->values) -(define (combine-props new-props old-props) +(define (resolve atoms prop) + (for/fold ([prop prop]) + ([a (in-list atoms)]) + (match prop + [(AndFilter: ps) + (let loop ([ps ps] [result null]) + (if (null? ps) + (-and result) + (let ([p (car ps)]) + (cond [(opposite? a p) -bot] + [(implied-atomic? p a) (loop (cdr ps) result)] + [else (loop (cdr ps) (cons p result))]))))] + [_ prop]))) + +(define (combine-props new-props old-props flag) (define (atomic-prop? p) (or (TypeFilter? p) (NotTypeFilter? p))) (define-values (new-atoms new-formulas) (partition atomic-prop? new-props)) (let loop ([derived-props null] @@ -98,9 +112,12 @@ [worklist (append old-props new-formulas)]) (if (null? worklist) (values derived-props derived-atoms) - (let ([p (car worklist)]) + (let* ([p (car worklist)] + [p (resolve derived-atoms p)]) (match p [(AndFilter: ps) (loop derived-props derived-atoms (append ps (cdr worklist)))] [(TypeFilter: _ _ _) (loop derived-props (cons p derived-atoms) (cdr worklist))] [(NotTypeFilter: _ _ _) (loop derived-props (cons p derived-atoms) (cdr worklist))] + [(Top:) (loop derived-props derived-atoms (cdr worklist))] + [(Bot:) (set-box! flag #f) (values derived-props derived-atoms)] [_ (loop (cons p derived-props) derived-atoms (cdr worklist))]))))) diff --git a/collects/typed-scheme/types/abbrev.ss b/collects/typed-scheme/types/abbrev.ss index 8347d9b0a7..94f8597e7d 100644 --- a/collects/typed-scheme/types/abbrev.ss +++ b/collects/typed-scheme/types/abbrev.ss @@ -279,55 +279,6 @@ [(Path: p i) (-not-filter t i p)] [_ -top])) -(define (opposite? f1 f2) - (match* (f1 f2) - [((TypeFilter: t1 p1 i1) - (NotTypeFilter: t2 p1 i2)) - (and (type-equal? t1 t2) - (free-identifier=? i1 i2))] - [((NotTypeFilter: t2 p1 i2) - (TypeFilter: t1 p1 i1)) - (and (type-equal? t1 t2) - (free-identifier=? i1 i2))] - [(_ _) #f])) - -(define (-or . args) - (let loop ([fs args] [result null]) - (if (null? fs) - (match result - [(list) -bot] - [(list f) f] - [(list f1 f2) - (if (opposite? f1 f2) - -top - (if (filter-equal? f1 f2) - f1 - (make-OrFilter (list f1 f2))))] - [_ (make-OrFilter result)]) - (match (car fs) - [(and t (Top:)) t] - [(OrFilter: fs*) (loop (cdr fs) (append fs* result))] - [(Bot:) (loop (cdr fs) result)] - [t (loop (cdr fs) (cons t result))])))) - -(define (-and . args) - (let loop ([fs args] [result null]) - (if (null? fs) - (match result - [(list) -top] - [(list f) f] - ;; don't think this is useful here - [(list f1 f2) (if (opposite? f1 f2) - -bot - (if (filter-equal? f1 f2) - f1 - (make-AndFilter (list f1 f2))))] - [_ (make-AndFilter result)]) - (match (car fs) - [(and t (Bot:)) t] - [(AndFilter: fs*) (loop (cdr fs) (append fs* result))] - [(Top:) (loop (cdr fs) result)] - [t (loop (cdr fs) (cons t result))])))) (d/c (-not-filter t i [p null]) (c:->* (Type/c name-ref/c) ((listof PathElem?)) Filter/c) diff --git a/collects/typed-scheme/types/convenience.ss b/collects/typed-scheme/types/convenience.ss index ae5fbb4ed4..715bed3060 100644 --- a/collects/typed-scheme/types/convenience.ss +++ b/collects/typed-scheme/types/convenience.ss @@ -68,3 +68,68 @@ (define Syntax-Sexp (-Sexpof Any-Syntax)) (define Ident (-Syntax -Symbol)) + +(define (opposite? f1 f2) + (match* (f1 f2) + [((TypeFilter: t1 p1 i1) + (NotTypeFilter: t2 p1 i2)) + (and (free-identifier=? i1 i2) + (subtype t1 t2))] + [((NotTypeFilter: t2 p1 i2) + (TypeFilter: t1 p1 i1)) + (and (free-identifier=? i1 i2) + (subtype t1 t2))] + [(_ _) #f])) + +;; is f1 implied by f2? +(define (implied-atomic? f1 f2) + (if (filter-equal? f1 f2) + #t + (match* (f1 f2) + [((TypeFilter: t1 p1 i1) + (TypeFilter: t2 p1 i2)) + (and (free-identifier=? i1 i2) + (subtype t1 t2))] + [((NotTypeFilter: t2 p1 i2) + (NotTypeFilter: t1 p1 i1)) + (and (free-identifier=? i1 i2) + (subtype t1 t2))] + [(_ _) #f]))) + +(define (-or . args) + (let loop ([fs args] [result null]) + (if (null? fs) + (match result + [(list) -bot] + [(list f) f] + [(list f1 f2) + (if (opposite? f1 f2) + -top + (if (filter-equal? f1 f2) + f1 + (make-OrFilter (list f1 f2))))] + [_ (make-OrFilter result)]) + (match (car fs) + [(and t (Top:)) t] + [(OrFilter: fs*) (loop (cdr fs) (append fs* result))] + [(Bot:) (loop (cdr fs) result)] + [t (loop (cdr fs) (cons t result))])))) + +(define (-and . args) + (let loop ([fs args] [result null]) + (if (null? fs) + (match result + [(list) -top] + [(list f) f] + ;; don't think this is useful here + [(list f1 f2) (if (opposite? f1 f2) + -bot + (if (filter-equal? f1 f2) + f1 + (make-AndFilter (list f1 f2))))] + [_ (make-AndFilter result)]) + (match (car fs) + [(and t (Bot:)) t] + [(AndFilter: fs*) (loop (cdr fs) (append fs* result))] + [(Top:) (loop (cdr fs) result)] + [t (loop (cdr fs) (cons t result))]))))