Fix type of filter, and inference w/ effects.
This commit is contained in:
parent
23aeff8c3b
commit
3fd969651f
|
@ -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))]
|
||||
|
|
|
@ -91,13 +91,29 @@
|
|||
(filter (lambda (te) (not (ormap (lambda (s) (type-equal? s te)) ss))) ts))])
|
||||
(cgen/list V X ss* ts*)))
|
||||
|
||||
;; 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* (for/list ([t ts] [s ss]) (cgen/eff V X t s))))
|
||||
|
||||
(define (cgen/arr V X t-arr s-arr)
|
||||
(define (cg S T) (cgen V X S T))
|
||||
(match* (t-arr s-arr)
|
||||
[((arr: ts t #f #f t-thn-eff t-els-eff)
|
||||
(arr: ss s #f #f s-thn-eff s-els-eff))
|
||||
(cset-meet (cgen/list X V ss ts)
|
||||
(cg t s))]
|
||||
(cset-meet*
|
||||
(list (cgen/list X V ss ts)
|
||||
(cg t s)
|
||||
(cgen/eff/list V X t-thn-eff s-thn-eff)
|
||||
(cgen/eff/list V X t-els-eff s-els-eff)))]
|
||||
[((arr: ts t t-rest #f t-thn-eff t-els-eff)
|
||||
(arr: ss s s-rest #f s-thn-eff s-els-eff))
|
||||
(let ([arg-mapping
|
||||
|
|
|
@ -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)])
|
||||
|
|
|
@ -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]
|
||||
|
|
Loading…
Reference in New Issue
Block a user