everything but or and implies works

This commit is contained in:
Sam Tobin-Hochstadt 2010-04-21 18:13:13 -04:00
parent 2bb2ffc513
commit 0804e64695
2 changed files with 15 additions and 18 deletions

View File

@ -69,12 +69,12 @@
(for/fold ([Γ (replace-props env imps)]) ([f atoms]) (for/fold ([Γ (replace-props env imps)]) ([f atoms])
(match f (match f
[(Bot:) (set-box! flag #f) (env-map (lambda (x) (cons (car x) (Un))) Γ)] [(Bot:) (set-box! flag #f) (env-map (lambda (x) (cons (car x) (Un))) Γ)]
[(ImpFilter: _ _) Γ]
[(or (TypeFilter: _ _ x) (NotTypeFilter: _ _ x)) [(or (TypeFilter: _ _ x) (NotTypeFilter: _ _ x))
(update-type/lexical (lambda (x t) (let ([new-t (update t f)]) (update-type/lexical (lambda (x t) (let ([new-t (update t f)])
(when (type-equal? new-t (Un)) (when (type-equal? new-t (Un))
(set-box! flag #f)) (set-box! flag #f))
new-t)) new-t))
x Γ)]))) x Γ)]
[_ Γ])))
(p/c [env+ (env? (listof Filter/c) (box/c #t). -> . env?)]) (p/c [env+ (env? (listof Filter/c) (box/c #t). -> . env?)])

View File

@ -91,19 +91,16 @@
(provide combine-props tc-results->values) (provide combine-props tc-results->values)
(define (combine-props new-props old-props) (define (combine-props new-props old-props)
(define-values (new-atoms new-formulas) (define (atomic-prop? p) (or (TypeFilter? p) (NotTypeFilter? p)))
(partition (lambda (e) (or (TypeFilter? e) (NotTypeFilter? e))) new-props)) (define-values (new-atoms new-formulas) (partition atomic-prop? new-props))
(values new-formulas new-atoms) (let loop ([derived-props null]
#;#; [derived-atoms new-atoms]
(define-values (derived-imps derived-atoms) [worklist (append old-props new-formulas)])
(for/fold (if (null? worklist)
([derived-imps null] (values derived-props derived-atoms)
[derived-atoms null]) (let ([p (car worklist)])
([o old-props]) (match p
(match o [(AndFilter: ps) (loop derived-props derived-atoms (append ps (cdr worklist)))]
[(ImpFilter: as cs) [(TypeFilter: _ _ _) (loop derived-props (cons p derived-atoms) (cdr worklist))]
(let ([as* (remove* new-atoms as filter-equal?)]) [(NotTypeFilter: _ _ _) (loop derived-props (cons p derived-atoms) (cdr worklist))]
(if (null? as*) [_ (loop (cons p derived-props) derived-atoms (cdr worklist))])))))
(values derived-imps (append cs new-atoms))
(values (cons (make-ImpFilter as* cs) derived-imps) derived-atoms)))])))
(values (append new-imps derived-imps) (append new-atoms derived-atoms)))