From 1880eb4afbbc5044d9643038cec7338f3051bc24 Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Thu, 19 Jun 2008 16:07:12 +0000 Subject: [PATCH] Fix filter type. svn: r10374 --- collects/typed-scheme/private/base-env.ss | 13 ++++++++++- collects/typed-scheme/private/infer-ops.ss | 22 +++++++++++++++++-- collects/typed-scheme/private/subtype.ss | 7 ++++-- .../private/type-effect-convenience.ss | 6 ++--- collects/typed-scheme/private/type-utils.ss | 5 ++++- 5 files changed, 44 insertions(+), 9 deletions(-) diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss index 898796f66f..255b01f19e 100644 --- a/collects/typed-scheme/private/base-env.ss +++ b/collects/typed-scheme/private/base-env.ss @@ -7,10 +7,13 @@ '#%paramz (only-in scheme/match/runtime match:error)) + + ;; these are all for constructing the types given to variables (require (for-syntax scheme/base "init-envs.ss" + "effect-rep.ss" (except-in "type-rep.ss" make-arr) "type-effect-convenience.ss" (only-in "type-effect-convenience.ss" [make-arr* make-arr]) @@ -137,7 +140,15 @@ (cl-> [((a b . -> . b) b (make-lst a)) b] [((a b c . -> . c) c (make-lst a) (make-lst b)) c]))] [foldr (-poly (a b c) ((a b . -> . b) b (-lst a) . -> . b))] - [filter (-poly (a) ((a . -> . B) (-lst a) . -> . (-lst a)))] + [filter (-poly (a b) (cl->* + ((a . -> . B + : + (list (make-Latent-Restrict-Effect b)) + (list (make-Latent-Remove-Effect b))) + (-lst a) + . -> . + (-lst b)) + ((a . -> . B) (-lst a) . -> . (-lst a))))] [take (-poly (a) ((-lst a) -Integer . -> . (-lst a)))] [drop (-poly (a) ((-lst a) -Integer . -> . (-lst a)))] [last (-poly (a) ((-lst a) . -> . a))] diff --git a/collects/typed-scheme/private/infer-ops.ss b/collects/typed-scheme/private/infer-ops.ss index 33fcbddd03..40358e7f93 100644 --- a/collects/typed-scheme/private/infer-ops.ss +++ b/collects/typed-scheme/private/infer-ops.ss @@ -146,6 +146,20 @@ (define (remember s t A) (cons (seen-before s t) A)) (define (seen? s t) (member (seen-before s t) (current-seen))) +;; t and s must be *latent* effects +(define (cgen/eff V X t s) + (match* (t s) + [(e e) (empty-cset X)] + [((Latent-Restrict-Effect: t) (Latent-Restrict-Effect: s)) + (cset-meet (cgen V X t s) (cgen V X s t))] + [((Latent-Remove-Effect: t) (Latent-Remove-Effect: s)) + (cset-meet (cgen V X t s) (cgen V X s t))] + [(_ _) (fail! t s)])) + +(define (cgen/eff/list V X ts ss) + (cset-meet* X (for/list ([t ts] [s ss]) (cgen/eff V X t s)))) + + (define (cgen V X S T) (define empty (empty-cset X)) (define (singleton S X T ) @@ -239,7 +253,11 @@ (with-handlers ([exn:infer? (lambda (_) #f)]) (match* (t-arr s-arr) [((arr: ts t t-rest t-thn-eff t-els-eff) (arr: ss s s-rest s-thn-eff s-els-eff)) - (let ([arg-mapping + (let ([eff-mapping + (cset-meet* X + (list (cgen/eff/list V X t-thn-eff s-thn-eff) + (cgen/eff/list V X t-els-eff s-els-eff)))] + [arg-mapping (cond [(and t-rest s-rest (= (length ts) (length ss))) (cgen/list X V (cons s-rest ss) (cons t-rest ts))] [(and (not t-rest) (not s-rest) (= (length ts) (length ss))) @@ -250,7 +268,7 @@ (cgen/list X V (extend ts ss s-rest) ts)] [else (fail! S T)])] [ret-mapping (cgen V X t s)]) - (cset-meet arg-mapping ret-mapping))])))))] + (cset-meet arg-mapping (cset-meet eff-mapping ret-mapping)))])))))] [(_ _) (cond [(subtype S T) empty] ;; or, nothing worked, and we fail diff --git a/collects/typed-scheme/private/subtype.ss b/collects/typed-scheme/private/subtype.ss index 91f0accfb1..f2114838ff 100644 --- a/collects/typed-scheme/private/subtype.ss +++ b/collects/typed-scheme/private/subtype.ss @@ -107,8 +107,11 @@ (or (and (null? thn-eff*) (null? els-eff*)) (and (effects-equal? thn-eff thn-eff*) (effects-equal? els-eff els-eff*)) - (and (andmap sub-eff thn-eff thn-eff*) - (andmap sub-eff els-eff els-eff*))) + (and + (= (length thn-eff) (length thn-eff*)) + (= (length els-eff) (length els-eff*)) + (andmap sub-eff thn-eff thn-eff*) + (andmap sub-eff els-eff els-eff*))) (fail! s t)) ;; either the effects have to be the same, or the supertype can't have effects (let ([A (subtypes*/varargs A0 t1 s1 s3)]) diff --git a/collects/typed-scheme/private/type-effect-convenience.ss b/collects/typed-scheme/private/type-effect-convenience.ss index bbf6008860..e09caee908 100644 --- a/collects/typed-scheme/private/type-effect-convenience.ss +++ b/collects/typed-scheme/private/type-effect-convenience.ss @@ -38,10 +38,10 @@ (define-syntax -> (syntax-rules (:) - [(_ dom ... rng) - (->* (list dom ...) rng)] [(_ dom ... rng : eff1 eff2) - (->* (list dom ...) : eff1 eff2)])) + (->* (list dom ...) rng : eff1 eff2)] + [(_ dom ... rng) + (->* (list dom ...) rng)])) (define-syntax ->* (syntax-rules (:) [(_ dom rng) diff --git a/collects/typed-scheme/private/type-utils.ss b/collects/typed-scheme/private/type-utils.ss index c4e1fa849a..2d402e112c 100644 --- a/collects/typed-scheme/private/type-utils.ss +++ b/collects/typed-scheme/private/type-utils.ss @@ -68,7 +68,10 @@ ;; equality - good (define tc-result-equal? equal?) -(define (effects-equal? fs1 fs2) (andmap eq? fs1 fs2)) +(define (effects-equal? fs1 fs2) + (and + (= (length fs1) (length fs2)) + (andmap eq? fs1 fs2))) ;; fv : Type -> Listof[Name]