Fix filter type.
svn: r10374
This commit is contained in:
parent
08015efba8
commit
1880eb4afb
|
@ -7,10 +7,13 @@
|
||||||
'#%paramz
|
'#%paramz
|
||||||
(only-in scheme/match/runtime match:error))
|
(only-in scheme/match/runtime match:error))
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
;; these are all for constructing the types given to variables
|
;; these are all for constructing the types given to variables
|
||||||
(require (for-syntax
|
(require (for-syntax
|
||||||
scheme/base
|
scheme/base
|
||||||
"init-envs.ss"
|
"init-envs.ss"
|
||||||
|
"effect-rep.ss"
|
||||||
(except-in "type-rep.ss" make-arr)
|
(except-in "type-rep.ss" make-arr)
|
||||||
"type-effect-convenience.ss"
|
"type-effect-convenience.ss"
|
||||||
(only-in "type-effect-convenience.ss" [make-arr* make-arr])
|
(only-in "type-effect-convenience.ss" [make-arr* make-arr])
|
||||||
|
@ -137,7 +140,15 @@
|
||||||
(cl-> [((a b . -> . b) b (make-lst a)) b]
|
(cl-> [((a b . -> . b) b (make-lst a)) b]
|
||||||
[((a b c . -> . c) c (make-lst a) (make-lst b)) c]))]
|
[((a b c . -> . c) c (make-lst a) (make-lst b)) c]))]
|
||||||
[foldr (-poly (a b c) ((a b . -> . b) b (-lst a) . -> . b))]
|
[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)))]
|
[take (-poly (a) ((-lst a) -Integer . -> . (-lst a)))]
|
||||||
[drop (-poly (a) ((-lst a) -Integer . -> . (-lst a)))]
|
[drop (-poly (a) ((-lst a) -Integer . -> . (-lst a)))]
|
||||||
[last (-poly (a) ((-lst a) . -> . a))]
|
[last (-poly (a) ((-lst a) . -> . a))]
|
||||||
|
|
|
@ -146,6 +146,20 @@
|
||||||
(define (remember s t A) (cons (seen-before s t) A))
|
(define (remember s t A) (cons (seen-before s t) A))
|
||||||
(define (seen? s t) (member (seen-before s t) (current-seen)))
|
(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 (cgen V X S T)
|
||||||
(define empty (empty-cset X))
|
(define empty (empty-cset X))
|
||||||
(define (singleton S X T )
|
(define (singleton S X T )
|
||||||
|
@ -239,7 +253,11 @@
|
||||||
(with-handlers ([exn:infer? (lambda (_) #f)])
|
(with-handlers ([exn:infer? (lambda (_) #f)])
|
||||||
(match* (t-arr s-arr)
|
(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))
|
[((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)))
|
(cond [(and t-rest s-rest (= (length ts) (length ss)))
|
||||||
(cgen/list X V (cons s-rest ss) (cons t-rest ts))]
|
(cgen/list X V (cons s-rest ss) (cons t-rest ts))]
|
||||||
[(and (not t-rest) (not s-rest) (= (length ts) (length ss)))
|
[(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)]
|
(cgen/list X V (extend ts ss s-rest) ts)]
|
||||||
[else (fail! S T)])]
|
[else (fail! S T)])]
|
||||||
[ret-mapping (cgen V X t s)])
|
[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]
|
(cond [(subtype S T) empty]
|
||||||
;; or, nothing worked, and we fail
|
;; or, nothing worked, and we fail
|
||||||
|
|
|
@ -107,8 +107,11 @@
|
||||||
(or (and (null? thn-eff*) (null? els-eff*))
|
(or (and (null? thn-eff*) (null? els-eff*))
|
||||||
(and (effects-equal? thn-eff thn-eff*)
|
(and (effects-equal? thn-eff thn-eff*)
|
||||||
(effects-equal? els-eff els-eff*))
|
(effects-equal? els-eff els-eff*))
|
||||||
(and (andmap sub-eff thn-eff thn-eff*)
|
(and
|
||||||
(andmap sub-eff els-eff els-eff*)))
|
(= (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))
|
(fail! s t))
|
||||||
;; either the effects have to be the same, or the supertype can't have effects
|
;; either the effects have to be the same, or the supertype can't have effects
|
||||||
(let ([A (subtypes*/varargs A0 t1 s1 s3)])
|
(let ([A (subtypes*/varargs A0 t1 s1 s3)])
|
||||||
|
|
|
@ -38,10 +38,10 @@
|
||||||
|
|
||||||
(define-syntax ->
|
(define-syntax ->
|
||||||
(syntax-rules (:)
|
(syntax-rules (:)
|
||||||
[(_ dom ... rng)
|
|
||||||
(->* (list dom ...) rng)]
|
|
||||||
[(_ dom ... rng : eff1 eff2)
|
[(_ dom ... rng : eff1 eff2)
|
||||||
(->* (list dom ...) : eff1 eff2)]))
|
(->* (list dom ...) rng : eff1 eff2)]
|
||||||
|
[(_ dom ... rng)
|
||||||
|
(->* (list dom ...) rng)]))
|
||||||
(define-syntax ->*
|
(define-syntax ->*
|
||||||
(syntax-rules (:)
|
(syntax-rules (:)
|
||||||
[(_ dom rng)
|
[(_ dom rng)
|
||||||
|
|
|
@ -68,7 +68,10 @@
|
||||||
;; equality - good
|
;; equality - good
|
||||||
|
|
||||||
(define tc-result-equal? equal?)
|
(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]
|
;; fv : Type -> Listof[Name]
|
||||||
|
|
Loading…
Reference in New Issue
Block a user