Fix type of filter, and inference w/ effects.

original commit: 3fd969651fbb7c90983ae76542c80391624e1f39
This commit is contained in:
Sam Tobin-Hochstadt 2008-06-19 11:57:07 -04:00
parent 7f4b1a5cd1
commit 3ea5cf0e61
3 changed files with 21 additions and 4 deletions

View File

@ -9,10 +9,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])
@ -132,7 +135,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))]

View File

@ -108,8 +108,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)])

View File

@ -130,7 +130,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]