diff --git a/collects/typed-scheme/module-info.ss b/collects/typed-scheme/language-info.ss similarity index 73% rename from collects/typed-scheme/module-info.ss rename to collects/typed-scheme/language-info.ss index 864540fe..ebecb8e2 100644 --- a/collects/typed-scheme/module-info.ss +++ b/collects/typed-scheme/language-info.ss @@ -1,10 +1,10 @@ #lang scheme/base (require typed-scheme/typed-reader) -(provide module-info configure) +(provide get-info configure) -(define ((module-info arg) key default) +(define ((get-info arg) key default) (case key - [(configure-runtime) `(#(typed-scheme/module-info configure ()))] + [(configure-runtime) `(#(typed-scheme/language-info configure ()))] [else default])) ;; options currently always empty diff --git a/collects/typed-scheme/typecheck/tc-app.ss b/collects/typed-scheme/typecheck/tc-app.ss index 8f501b49..e2ed7237 100644 --- a/collects/typed-scheme/typecheck/tc-app.ss +++ b/collects/typed-scheme/typecheck/tc-app.ss @@ -467,9 +467,9 @@ kw-list (#%plain-app list . kw-arg-list) . pos-args) - #:declare cpce (id-from 'checked-procedure-check-and-extract 'scheme/private/kw) - #:declare s-kp (id-from 'struct:keyword-procedure 'scheme/private/kw) - #:declare kpe (id-from 'keyword-procedure-extract 'scheme/private/kw) + #:declare cpce (id-from 'checked-procedure-check-and-extract 'racket/private/kw) + #:declare s-kp (id-from 'struct:keyword-procedure 'racket/private/kw) + #:declare kpe (id-from 'keyword-procedure-extract 'racket/private/kw) (match (tc-expr #'fn) [(tc-result1: (Poly: vars (Function: (list (and ar (arr: dom rng (and rest #f) (and drest #f) kw-formals)))))) diff --git a/collects/typed-scheme/typecheck/tc-envops.ss b/collects/typed-scheme/typecheck/tc-envops.ss index c6264d9f..e3d94c7d 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 e18bf9c9..98bd6ba6 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 8347d9b0..94f8597e 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 ae5fbb4e..715bed30 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))])))) diff --git a/collects/typed/scheme/base/lang/reader.ss b/collects/typed/scheme/base/lang/reader.ss index ce8f8d0f..b0982890 100644 --- a/collects/typed/scheme/base/lang/reader.ss +++ b/collects/typed/scheme/base/lang/reader.ss @@ -5,14 +5,14 @@ typed/scheme/base #:read r:read #:read-syntax r:read-syntax #:info make-info -#:module-info make-module-info +#:language-info make-language-info (define (make-info key default use-default) (case key [else (use-default key default)])) -(define make-module-info - `#(typed-scheme/module-info module-info ())) +(define make-language-info + `#(typed-scheme/language-info get-info ())) (require (prefix-in r: typed-scheme/typed-reader)) diff --git a/collects/typed/scheme/lang/reader.ss b/collects/typed/scheme/lang/reader.ss index 3a91f1a7..0c7fbe6b 100644 --- a/collects/typed/scheme/lang/reader.ss +++ b/collects/typed/scheme/lang/reader.ss @@ -5,14 +5,14 @@ typed/scheme #:read r:read #:read-syntax r:read-syntax #:info make-info -#:module-info make-module-info +#:language-info make-language-info (define (make-info key default use-default) (case key [else (use-default key default)])) -(define make-module-info - `#(typed-scheme/module-info module-info ())) +(define make-language-info + `#(typed-scheme/language-info get-info ())) (require (prefix-in r: typed-scheme/typed-reader))